size-constraint.sml 9 KB
Newer Older
1
2
structure SizeConstraint : sig
   type size_constraint
Axel Simon's avatar
Axel Simon committed
3
4
5
6

   (*create a constraint of the form a = b+...z+42*)
   val equality : TVar.tvar * TVar.tvar list * int -> size_constraint

7
   type size_constraint_set
Axel Simon's avatar
Axel Simon committed
8
9

   datatype instantiation
Axel Simon's avatar
Axel Simon committed
10
      = RESULT of (TVar.tvar * int) list * size_constraint_set
Axel Simon's avatar
Axel Simon committed
11
12
13
14
      | UNSATISFIABLE
      | FRACTIONAL
      | NEGATIVE
   
Axel Simon's avatar
Axel Simon committed
15
16
17
18
19
   val empty : size_constraint_set
   val add : size_constraint * size_constraint_set -> instantiation
   val fromList : size_constraint list -> size_constraint_set
   val listItems : size_constraint_set -> size_constraint list

Axel Simon's avatar
Axel Simon committed
20
   val filter : TVar.set * size_constraint_set -> size_constraint_set
Axel Simon's avatar
Axel Simon committed
21
22
23
24
25
26
   val merge : size_constraint_set * size_constraint_set ->
               size_constraint_set
   val rename : TVar.tvar * TVar.tvar * size_constraint_set ->
                size_constraint_set
   val getVarset : size_constraint_set -> TVar.set
   val toStringSI : size_constraint_set * TVar.set option * TVar.varmap ->
Axel Simon's avatar
Axel Simon committed
27
28
                    string * TVar.varmap

29
30
31
end = struct

   type size_constraint = {
Axel Simon's avatar
Axel Simon committed
32
      terms : (int * TVar.tvar) list,
33
34
      const : int
   }
Axel Simon's avatar
Axel Simon committed
35
   type size_constraint_set = size_constraint list
36

Axel Simon's avatar
Axel Simon committed
37
38
39
40
41
   datatype instantiation
      = RESULT of (TVar.tvar * int) list * size_constraint_set
      | UNSATISFIABLE
      | FRACTIONAL
      | NEGATIVE
Axel Simon's avatar
Axel Simon committed
42

Axel Simon's avatar
Axel Simon committed
43
44
45
46
47
48
   fun filter (vs, scs) = List.filter
      (fn {terms = ts, const} =>
         List.exists (fn (_,v) => TVar.member (vs,v)) ts)
      scs

   fun toStringSI (scs, filterSet, si) =
Axel Simon's avatar
Axel Simon committed
49
50
51
52
53
54
55
56
57
58
59
60
61
62
      let
         val siRef = ref si
         fun showVar v = case TVar.varToString (v,!siRef) of
            (str,si) => (siRef := si; str)
         fun showFac f = if f=1 then "" else Int.toString f
         fun showTS ({terms=[], const=c},psep,pos,nsep,neg) =
            if c=0 then pos ^ "=" ^ neg else
            if c<0 then pos ^ "=" ^ neg ^ nsep ^ Int.toString(~c)
            else pos ^ psep ^ Int.toString(c) ^ "=" ^ neg
           | showTS ({terms=((fac,var)::ts), const=c},psep,pos,nsep,neg) =
               if fac>=0 then showTS ({terms = ts, const = c},
                  "+", pos ^ psep ^ showFac fac ^ showVar var, nsep, neg)
               else  showTS ({terms = ts, const = c},
                  psep, pos, "+", neg ^ nsep ^ showFac (~fac) ^ showVar var)
Axel Simon's avatar
Axel Simon committed
63
64
         val scs = case filterSet of NONE => scs
                                   | SOME vs => filter (vs, scs)
Axel Simon's avatar
Axel Simon committed
65
66
67
68
69
70
         val (res,_) = List.foldl (fn (sc,(res,sep)) =>
               (res ^ sep ^ showTS (sc,"","","",""), ", ")) ("", "") scs
      in
         (res, !siRef)
      end
         
Axel Simon's avatar
Axel Simon committed
71
72
73
74
   val empty = []

   exception SizeConstraintBug

Axel Simon's avatar
Axel Simon committed
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
   fun addTermToSC (f,v,{terms = ts, const = c}) =
      let
         fun aTSC (res,[]) = res @ [(f,v)]
           | aTSC (res, (fac,var)::ts) = (case TVar.compare (v,var) of
                EQUAL => let val newF = fac+f in
                           if newF=0 then res @ ts else res @ (newF,v) :: ts
                         end
              | LESS => res @ (f,v) :: (fac,var)::ts
              | GREATER => aTSC (res @ [(fac,var)], ts))
      in
         {terms = aTSC ([],ts), const = c}
      end

   fun lookupVarSC (v, {terms = ts, const = c}) =
      case List.find (fn (fac,var) => TVar.eq (v,var)) ts of
           NONE => 0
         | SOME (fac,_) => fac

93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
   fun mergeSC (_,0,sc1,sc2) = sc1
     | mergeSC (0,_,sc1,sc2) = sc2
     | mergeSC (mul1,mul2,{terms = ts1, const = n1},
               {terms = ts2, const = n2}) =
      let
         fun m ((f1,v1)::ts1, (f2,v2)::ts2) =
            (case TVar.compare (v1,v2) of
                 LESS => (mul1*f1,v1) :: m (ts1, (f2,v2)::ts2)
               | GREATER => (mul2*f2,v2) :: m ((f1,v1)::ts1, ts2)
               | EQUAL => 
                  let
                     val f = mul1*f1+mul2*f2
                  in
                     if f=0 then m (ts1,ts2) else (f,v1) :: m (ts1,ts2)
                  end)
           | m ((f1,v1)::ts1, []) = (mul1*f1,v1) :: m (ts1, [])
           | m ([], (f2,v2)::ts2) = (mul2*f2,v2) :: m ([], ts2)
           | m ([], []) = []
      in
         {terms = m (ts1,ts2), const = mul1*n1+mul2*n2}
      end

   fun add (eq,scs) =
      let
         fun inline (sc as {terms = (f,v) :: _, const = n2}, eq) =
               mergeSC (~f, lookupVarSC (v, eq), eq, sc)
           | inline (_, eq) = eq
         fun eqsIntoEq (eq, scs) = List.foldl inline eq scs
         fun eqIntoEqs (eq, scs) = List.map (fn sc => inline (eq,sc)) scs
         fun insert (eq as {terms = [], const}, scs) = eq :: scs
           | insert (eq as {terms = (_,v1) :: _, const = n1},
                    (sc as {terms = (_,v2) :: _, const = n2}) :: scs) =
               (case TVar.compare (v1,v2) of
                    LESS => eq :: sc :: scs
                  | GREATER => sc :: insert (eq, scs)
                  | EQUAL => raise SizeConstraintBug)
           | insert (eq, []) = [eq]
           | insert (eq, sc :: scs) = sc :: insert (eq, scs)
         fun gatherFun ({terms = [], const = 0}, res) = res
           | gatherFun ({terms = [], const = _}, res) = UNSATISFIABLE
           | gatherFun ({terms = [(f,v)], const = n}, RESULT (is,eqs)) = 
               if Int.rem (~n, f) <> 0 then FRACTIONAL
               else if Int.quot (~n, f) < 0 then NEGATIVE
               else RESULT ((v,Int.quot (~n, f))::is, eqs)
           | gatherFun (eq, RESULT (is,eqs)) = RESULT (is,eqs @ [eq])
           | gatherFun (eq, res) = res
         val eq = eqsIntoEq (eq, scs)
         val scs = eqIntoEqs (eq, scs)
         (*val (eStr, si) = toStringSI ([eq], NONE, TVar.emptyShowInfo)
         val (sStr, si) = toStringSI (scs, NONE, si)
         val _ = TextIO.print ("inserting " ^ eStr ^ " into " ^ sStr ^ "\n")*)
         val scs = insert (eq,scs)
         val res = List.foldl gatherFun (RESULT ([],[])) scs
         (*val nStr = case res of
              RESULT (is, scs) =>
              let
                 val (scsStr, si) = (toStringSI (scs, NONE, si))
                 val (vsStr, si) = List.foldl (fn ((v,f),(str, si)) =>
                   let val (vStr, si) = TVar.varToString (v,si) in
                      (str ^ " " ^ vStr ^ "=" ^ Int.toString(f), si)
                   end) ("", si) is
              in
155
                 "result : " ^ scsStr ^ " and" ^ vsStr ^ " instantiated\n"
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
              end
            | UNSATISFIABLE => "unsatisfiabilitiy"
            | FRACTIONAL => "non-integrality"
            | NEGATIVE => "negativitiy"
         val _ = TextIO.print ("new system is " ^ nStr ^ "\n")*)
      in
         res
      end

   fun fromList eqs =
      let
         fun fL ([], scs) = scs
           | fL (eq :: eqs, scs) = case add (eq, scs) of
                RESULT ([], scs) => fL (eqs, scs)
              | _ => raise SizeConstraintBug
      in
         fL (eqs, empty)
      end

   fun listItems scs = scs

Axel Simon's avatar
Axel Simon committed
177
178
179
180
181
   fun equality (lhs, terms, c) =
      List.foldl (fn ((f,v), sc) => addTermToSC (f,v,sc))
         { terms = [], const = c}
         ((~1,lhs) :: List.map (fn v => (1,v)) terms)

Axel Simon's avatar
Axel Simon committed
182
183
184
185
186
187
188
   fun getVarset scs =
      let
         fun gV ({terms = ts, const}, vs) =
            List.foldl (fn ((fac,var), vs) => TVar.add (var,vs)) vs ts
      in
         List.foldl gV TVar.empty scs
      end
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
   
   fun diff (scs1, scs2) =
      let
         fun cmp ({terms=(_,v1)::_, const=_},{terms=(_,v2)::_, const=_}) =
                  TVar.compare (v1,v2)
           | cmp _ = raise SizeConstraintBug
         fun genDiff (sc1 :: scs1, sc2 :: scs2) =
            (case cmp (sc1,sc2) of
                 LESS => sc1 :: genDiff (scs1, sc2 :: scs2)
               | GREATER => genDiff (sc1 :: scs1, scs2)
               | EQUAL => genDiff (scs1, scs2)
            )
           | genDiff (scs1, _) = scs1
      in
         genDiff (scs1, scs2)
      end

Axel Simon's avatar
Axel Simon committed
206
207
   fun merge (scs1, scs2) =
      let
208
         val scs1 = diff (scs1,scs2)
Axel Simon's avatar
Axel Simon committed
209
210
211
212
         fun m ([], scs) = scs
           | m (eq :: eqs, scs) = case add (eq, scs) of
                RESULT (_, scs) => m (eqs, scs)
              | _ => raise SizeConstraintBug
213
214
215
216
217
218
         val scs = m (scs1, scs2)
         (*val (sStr1, si) = toStringSI (scs1, NONE, TVar.emptyShowInfo)
         val (sStr2, si) = toStringSI (scs2, NONE, si)
         val (sStr3, si) = toStringSI (scs, NONE, si)
         val _ = TextIO.print ("merging " ^ sStr1 ^ " with " ^ sStr2 ^ 
                               " resulting in " ^ sStr3 ^ "\n")*)
Axel Simon's avatar
Axel Simon committed
219
      in
220
         scs
Axel Simon's avatar
Axel Simon committed
221
      end
222

Axel Simon's avatar
Axel Simon committed
223
224
   fun rename (v1,v2,scs) =
      let
225
         (*val (tVar1, si) = TVar.varToString (v1, TVar.emptyShowInfo)
Axel Simon's avatar
Axel Simon committed
226
227
         val (tVar2, si) = TVar.varToString (v2, si)
         val (sStr, si) = toStringSI (scs, NONE, si)
228
         val _ = TextIO.print ("renaming " ^ tVar1 ^ " to " ^ tVar2 ^ " in " ^ sStr ^ "\n")*)
Axel Simon's avatar
Axel Simon committed
229
230
231
232
233
234
         fun hasV1 {terms = ts,const} =
            List.exists (fn (_,v) => TVar.eq(v,v1)) ts
         val (withVar, retained) = List.partition hasV1 scs
         fun renameVar sc = case lookupVarSC (v1,sc) of f1 =>
               addTermToSC (f1,v2, addTermToSC (~f1,v1, sc))
         val renamed = List.map renameVar withVar
235
236
         val renamed = List.filter
               (fn {terms=ts,const} => not (List.null ts)) renamed
Axel Simon's avatar
Axel Simon committed
237
238
239
      in
         merge (renamed, retained)
      end
240
end