1(*****************************************************************************)
2(* FILE          : sup-inf.sml                                               *)
3(* DESCRIPTION   : SUP-INF method for deciding a subset of Presburger        *)
4(*                 arithmetic (R.E.Shostak, JACM Vol.24 No.4 Pages 529-543)  *)
5(*                                                                           *)
6(* READS FILES   : <none>                                                    *)
7(* WRITES FILES  : <none>                                                    *)
8(*                                                                           *)
9(* AUTHOR        : R.J.Boulton, University of Cambridge                      *)
10(* DATE          : 4th March 1991                                            *)
11(*                                                                           *)
12(* TRANSLATOR    : R.J.Boulton, University of Cambridge                      *)
13(* DATE          : 16th February 1993                                        *)
14(*                                                                           *)
15(* LAST MODIFIED : R.J.Boulton                                               *)
16(* DATE          : 16th February 1993                                        *)
17(*****************************************************************************)
18
19structure Sup_Inf :> Sup_Inf =
20struct
21  open Arbint
22  val op << = String.<
23  infix <<
24
25
26open Rationals;
27open Lib; infix ##;
28open Feedback;
29
30fun failwith function = raise HOL_ERR{origin_structure = "Sup_Inf",
31                                      origin_function = function,
32                                      message = ""};
33
34
35(*===========================================================================*)
36(* SUP-INF algorithm                                                         *)
37(*===========================================================================*)
38
39(*---------------------------------------------------------------------------*)
40(* Datatype for representing the bounds of a normalised expression           *)
41(*---------------------------------------------------------------------------*)
42
43datatype bound = Bound of rat * (string * rat) list
44               | Max_bound of bound list
45               | Min_bound of bound list
46               | Pos_inf
47               | Neg_inf;
48
49(*---------------------------------------------------------------------------*)
50(* Datatype for representing the bounds of an non-normalised expression      *)
51(*---------------------------------------------------------------------------*)
52
53datatype internal_bound = Ibound of bound
54                        | Mult_ibound of rat * internal_bound
55                        | Plus_ibound of internal_bound * internal_bound
56                        | Max_ibound of internal_bound list
57                        | Min_ibound of internal_bound list;
58
59(*---------------------------------------------------------------------------*)
60(* solve_ineqs :                                                             *)
61(*    (int * (string * int) list) list ->                                    *)
62(*    string ->                                                              *)
63(*    ((rat * (string * rat) list) list * (rat * (string * rat) list) list)  *)
64(*---------------------------------------------------------------------------*)
65
66fun solve_ineqs ineqs var =
67   if (null ineqs)
68   then ([],[])
69   else let val (const,bind) = hd ineqs
70            and (restl,restr) = solve_ineqs (tl ineqs) var
71        in  (let val i = assoc var bind
72                 val const' = Rat (const,(~i))
73                 and bind' = map (I ## (fn n => Rat (n,(~i))))
74                                (filter (fn (name,_) => not (name = var)) bind)
75             in  if (i < zero)
76                 then (((const',bind')::restl),restr)
77                 else (restl,((const',bind')::restr))
78             end)
79            handle _ => (restl,restr)
80        end;
81
82(*---------------------------------------------------------------------------*)
83(* UPPER : (int * (string * int) list) list -> string -> bound               *)
84(*---------------------------------------------------------------------------*)
85
86fun UPPER s x =
87   let val uppers = fst (solve_ineqs s x)
88   in  if (null uppers)
89       then Pos_inf
90       else if (null (tl uppers))
91            then Bound (hd uppers)
92            else Min_bound (map Bound uppers)
93   end;
94
95(*---------------------------------------------------------------------------*)
96(* LOWER : (int * (string * int) list) list -> string -> bound               *)
97(*---------------------------------------------------------------------------*)
98
99fun LOWER s x =
100   let val lowers = snd (solve_ineqs s x)
101   in  if (null lowers)
102       then Neg_inf
103       else if (null (tl lowers))
104            then Bound (hd lowers)
105            else Max_bound (map Bound lowers)
106   end;
107
108(*---------------------------------------------------------------------------*)
109(* SIMP_mult : rat -> bound -> bound                                         *)
110(*---------------------------------------------------------------------------*)
111
112fun SIMP_mult r (Bound (const,bind)) =
113       Bound (rat_mult r const,map (I ## (rat_mult r)) bind)
114  | SIMP_mult r (Max_bound bl) =
115       (if ((Numerator r) < zero)
116        then (Min_bound (map (SIMP_mult r) bl))
117        else (Max_bound (map (SIMP_mult r) bl)))
118  | SIMP_mult r (Min_bound bl) =
119       (if ((Numerator r) < zero)
120        then (Max_bound (map (SIMP_mult r) bl))
121        else (Min_bound (map (SIMP_mult r) bl)))
122  | SIMP_mult r Pos_inf = if ((Numerator r) < zero) then Neg_inf else Pos_inf
123  | SIMP_mult r Neg_inf = if ((Numerator r) < zero) then Pos_inf else Neg_inf;
124
125(*---------------------------------------------------------------------------*)
126(* sum_bindings :                                                            *)
127(*    (string * rat) list -> (string * rat) list -> (string * rat) list      *)
128(*---------------------------------------------------------------------------*)
129
130fun sum_bindings bind1 bind2 =
131   if (null bind1) then bind2
132   else if (null bind2) then bind1
133   else (let val (name1:string,coeff1) = hd bind1
134             and (name2,coeff2) = hd bind2
135         in  if (name1 = name2) then
136                (let val coeff = rat_plus coeff1 coeff2
137                     and bind = sum_bindings (tl bind1) (tl bind2)
138                 in  if ((Numerator coeff) = zero)
139                     then bind
140                     else (name1,coeff)::bind
141                 end)
142             else if (name1 << name2) then
143                (name1,coeff1)::(sum_bindings (tl bind1) bind2)
144             else (name2,coeff2)::(sum_bindings bind1 (tl bind2))
145         end);
146
147(*---------------------------------------------------------------------------*)
148(* SIMP_plus : bound -> bound -> bound                                       *)
149(*---------------------------------------------------------------------------*)
150
151fun SIMP_plus (Bound (const1,bind1)) (Bound (const2,bind2)) =
152       Bound (rat_plus const1 const2,sum_bindings bind1 bind2)
153  | SIMP_plus (b1 as Bound _) (Max_bound bl) =
154       Max_bound (map (SIMP_plus b1) bl)
155  | SIMP_plus (b1 as Bound _) (Min_bound bl) =
156       Min_bound (map (SIMP_plus b1) bl)
157  | SIMP_plus (Bound _) Pos_inf = Pos_inf
158  | SIMP_plus (Bound _) Neg_inf = Neg_inf
159  | SIMP_plus (Max_bound bl) b2 = Max_bound (map (fn b => SIMP_plus b b2) bl)
160  | SIMP_plus (Min_bound bl) b2 = Min_bound (map (fn b => SIMP_plus b b2) bl)
161  | SIMP_plus Pos_inf Pos_inf = Pos_inf
162  | SIMP_plus Pos_inf Neg_inf = failwith "SIMP_plus"
163  | SIMP_plus (b1 as Pos_inf) b2 = SIMP_plus b2 b1
164  | SIMP_plus Neg_inf Neg_inf = Neg_inf
165  | SIMP_plus Neg_inf Pos_inf = failwith "SIMP_plus"
166  | SIMP_plus (b1 as Neg_inf) b2 = SIMP_plus b2 b1;
167
168(*---------------------------------------------------------------------------*)
169(* SIMP : internal_bound -> bound                                            *)
170(*---------------------------------------------------------------------------*)
171
172fun SIMP (Ibound b) = b
173  | SIMP (Mult_ibound (r,ib')) = SIMP_mult r (SIMP ib')
174  | SIMP (Plus_ibound (ib1,ib2)) = SIMP_plus (SIMP ib1) (SIMP ib2)
175  | SIMP (Max_ibound ibl) = Max_bound (map SIMP ibl)
176  | SIMP (Min_ibound ibl) = Min_bound (map SIMP ibl);
177
178(*---------------------------------------------------------------------------*)
179(* SUPP : (string * bound) -> bound                                          *)
180(* INFF : (string * bound) -> bound                                          *)
181(*---------------------------------------------------------------------------*)
182
183fun SUPP (x,y) =
184   case y
185   of (Bound (_,[])) => y
186    | Pos_inf => y
187    | Neg_inf => y
188    | (Min_bound bl) => (Min_bound (map (fn y => SUPP (x,y)) bl))
189    | (Bound (const,bind)) =>
190         (let val b = (assoc x bind) handle NOT_FOUND => rat_zero
191              and bind' = filter (fn p => not (fst p = x)) bind
192          in  if ((null bind') andalso (const = rat_zero) andalso
193                  (b = rat_one))
194              then Pos_inf
195              else let val b' = rat_minus rat_one b
196                   in  if (Numerator b' < zero) then Pos_inf
197                       else if (Numerator b' > zero) then
198                          (Bound (rat_div const b',
199                                  map (I ## (fn r => rat_div r b')) bind'))
200                       else if (not (null bind')) then Pos_inf
201                            else if (Numerator const < zero) then Neg_inf
202                            else Pos_inf
203                   end
204          end)
205    | _ => failwith "SUPP";
206
207fun INFF (x,y) =
208   case y
209   of (Bound (_,[])) => y
210    | Pos_inf => y
211    | Neg_inf => y
212    | (Max_bound bl) => (Max_bound (map (fn y => INFF (x,y)) bl))
213    | (Bound (const,bind)) =>
214         (let val b = (assoc x bind) handle NOT_FOUND => rat_zero
215              and bind' = filter (fn p => not (fst p = x)) bind
216          in  if ((null bind') andalso (const = rat_zero) andalso
217                  (b = rat_one))
218              then Neg_inf
219              else let val b' = rat_minus rat_one b
220                   in  if (Numerator b' < zero) then Neg_inf
221                       else if (Numerator b' > zero) then
222                          (Bound (rat_div const b',
223                                  map (I ## (fn r => rat_div r b')) bind'))
224                       else if (not (null bind')) then Neg_inf
225                            else if (Numerator const > zero) then Pos_inf
226                            else Neg_inf
227                   end
228          end)
229    | _ => failwith "INFF";
230
231(*---------------------------------------------------------------------------*)
232(* occurs_in_bound : string -> bound -> bool                                 *)
233(*---------------------------------------------------------------------------*)
234
235fun occurs_in_bound v (Bound (_,bind)) = Lib.mem v (map fst bind)
236  | occurs_in_bound v (Max_bound bl) =
237       itlist (fn x => fn y => x orelse y) (map (occurs_in_bound v) bl) false
238  | occurs_in_bound v (Min_bound bl) =
239       itlist (fn x => fn y => x orelse y) (map (occurs_in_bound v) bl) false
240  | occurs_in_bound _ _ = false;
241
242(*---------------------------------------------------------------------------*)
243(* occurs_in_ibound : string -> internal_bound -> bool                       *)
244(*---------------------------------------------------------------------------*)
245
246fun occurs_in_ibound v (Ibound b) = occurs_in_bound v b
247  | occurs_in_ibound v (Mult_ibound (_,ib')) = occurs_in_ibound v ib'
248  | occurs_in_ibound v (Plus_ibound (ib1,ib2)) =
249       (occurs_in_ibound v ib1) orelse (occurs_in_ibound v ib2)
250  | occurs_in_ibound v (Max_ibound ibl) =
251       itlist (fn x => fn y => x orelse y) (map (occurs_in_ibound v) ibl) false
252  | occurs_in_ibound v (Min_ibound ibl) =
253       itlist (fn x => fn y => x orelse y) (map (occurs_in_ibound v) ibl)
254                                                                         false;
255
256(*---------------------------------------------------------------------------*)
257(* SUP : (int * (string * int) list) list ->                                 *)
258(*       (bound * (string list)) ->                                          *)
259(*       internal_bound                                                      *)
260(* INF : (int * (string * int) list) list ->                                 *)
261(*       (bound * (string list)) ->                                          *)
262(*       internal_bound                                                      *)
263(*---------------------------------------------------------------------------*)
264
265fun SUP s (J,H) =
266   case J
267   of (Bound (_,[])) => Ibound J
268    | Pos_inf => Ibound J
269    | Neg_inf => Ibound J
270    | (Min_bound bl) => Min_ibound (map (fn j => SUP s (j,H)) bl)
271    | (Bound (const,(rv as (v,r))::bind')) =>
272         (if ((const = rat_zero) andalso (null bind'))
273          then (if (r = rat_one) then
274                   (if (Lib.mem v H)
275                    then Ibound J
276                    else let val Q = UPPER s v
277                             val Z = SUP s (Q,Lib.union H [v])
278                         in  Ibound (SUPP (v,SIMP Z))
279                         end)
280                else if (Numerator r < zero) then
281                   (Mult_ibound (r,INF s (Bound (rat_zero,[(v,rat_one)]),H)))
282                else Mult_ibound (r,SUP s (Bound (rat_zero,[(v,rat_one)]),H))
283               )
284          else let val B' = SUP s (Bound (const,bind'),Lib.union H [v])
285                   and rvb = Bound (rat_zero,[rv])
286               in  if (occurs_in_ibound v B')
287                   then let val J' = SIMP (Plus_ibound (Ibound rvb,B'))
288                        in  SUP s (J',H)
289                        end
290                   else Plus_ibound (SUP s (rvb,H),B')
291               end)
292    | _ => failwith "SUP"
293
294and INF s (J,H) =
295   case J
296   of (Bound (_,[])) => Ibound J
297    | Pos_inf => Ibound J
298    | Neg_inf => Ibound J
299    | (Max_bound bl) => Max_ibound (map (fn j => INF s (j,H)) bl)
300    | (Bound (const,(rv as (v,r))::bind')) =>
301         (if ((const = rat_zero) andalso (null bind'))
302          then (if (r = rat_one) then
303                   (if (Lib.mem v H)
304                    then Ibound J
305                    else let val Q = LOWER s v
306                             val Z = INF s (Q,Lib.union H [v])
307                         in  Ibound (INFF (v,SIMP Z))
308                         end)
309                else if (Numerator r < zero) then
310                   (Mult_ibound (r,SUP s (Bound (rat_zero,[(v,rat_one)]),H)))
311                else Mult_ibound (r,INF s (Bound (rat_zero,[(v,rat_one)]),H))
312               )
313          else let val B' = INF s (Bound (const,bind'),Lib.union H [v])
314                   and rvb = Bound (rat_zero,[rv])
315               in  if (occurs_in_ibound v B')
316                   then let val J' = SIMP (Plus_ibound (Ibound rvb,B'))
317                        in  INF s (J',H)
318                        end
319                   else Plus_ibound (INF s (rvb,H),B')
320               end)
321    | _ => failwith "INF";
322
323(*---------------------------------------------------------------------------*)
324(* eval_max_bound : bound list -> bound                                      *)
325(*---------------------------------------------------------------------------*)
326
327fun eval_max_bound bl =
328   if (null bl) then failwith "eval_max_bound"
329   else if (null (tl bl)) then (hd bl)
330   else let val b = hd bl
331            and max = eval_max_bound (tl bl)
332        in  case (b,max)
333            of (Pos_inf,_) => Pos_inf
334             | (_,Pos_inf) => Pos_inf
335             | (Neg_inf,_) => max
336             | (_,Neg_inf) => b
337             | (Bound (r1,[]),Bound (r2,[])) =>
338                  (if (Numerator (rat_minus r1 r2) < zero) then max else b)
339             | _ => failwith "eval_max_bound"
340        end;
341
342(*---------------------------------------------------------------------------*)
343(* eval_min_bound : bound list -> bound                                      *)
344(*---------------------------------------------------------------------------*)
345
346fun eval_min_bound bl =
347   if (null bl) then failwith "eval_min_bound"
348   else if (null (tl bl)) then (hd bl)
349   else let val b = hd bl
350            and min = eval_min_bound (tl bl)
351        in  case (b,min)
352            of (Pos_inf,_) => min
353             | (_,Pos_inf) => b
354             | (_,Neg_inf) => Neg_inf
355             | (Neg_inf,_) => Neg_inf
356             | (Bound (r1,[]),Bound (r2,[])) =>
357                  (if (Numerator (rat_minus r1 r2) < zero) then b else min)
358             | _ => failwith "eval_min_bound"
359        end;
360
361(*---------------------------------------------------------------------------*)
362(* eval_bound : bound -> bound                                               *)
363(*---------------------------------------------------------------------------*)
364
365fun eval_bound (b as Bound (_,[])) = b
366  | eval_bound (Max_bound bl) = eval_max_bound (map eval_bound bl)
367  | eval_bound (Min_bound bl) = eval_min_bound (map eval_bound bl)
368  | eval_bound (b as Pos_inf) = b
369  | eval_bound (b as Neg_inf) = b
370  | eval_bound _ = failwith "eval_bound";
371
372(*---------------------------------------------------------------------------*)
373(* SUP_INF :                                                                 *)
374(*    (int * (string * int) list) list -> (string * bound * bound) list      *)
375(*---------------------------------------------------------------------------*)
376
377fun SUP_INF set =
378   let fun vars_of_coeffs coeffsl =
379          Lib.mk_set (flatten (map ((map fst) o snd) coeffsl))
380       val vars = vars_of_coeffs set
381       and eval = eval_bound o SIMP
382       fun make_bound v = Bound (rat_zero,[(v,rat_one)])
383   in  map (fn v => let val b = make_bound v
384                    in  (v,eval (INF set (b,[])),eval (SUP set (b,[])))
385                    end) vars
386   end;
387
388end
389