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