1(* Title: Tools/Argo/argo_rewr.ML 2 Author: Sascha Boehme 3 4Bottom-up rewriting of expressions based on rewrite rules and rewrite functions. 5*) 6 7signature ARGO_REWR = 8sig 9 (* conversions *) 10 type conv = Argo_Expr.expr -> Argo_Expr.expr * Argo_Proof.conv 11 val keep: conv 12 val seq: conv list -> conv 13 val args: conv -> conv 14 val rewr: Argo_Proof.rewrite -> Argo_Expr.expr -> conv 15 16 (* context *) 17 type context 18 val context: context 19 20 (* rewriting *) 21 val rewrite: context -> conv 22 val rewrite_top: context -> conv 23 val with_proof: conv -> Argo_Expr.expr * Argo_Proof.proof -> Argo_Proof.context -> 24 (Argo_Expr.expr * Argo_Proof.proof) * Argo_Proof.context 25 26 (* normalizations *) 27 val nnf: context -> context 28 val norm_prop: context -> context 29 val norm_ite: context -> context 30 val norm_eq: context -> context 31 val norm_add: context -> context 32 val norm_mul: context -> context 33 val norm_arith: context -> context 34end 35 36structure Argo_Rewr: ARGO_REWR = 37struct 38 39(* conversions *) 40 41(* 42 Conversions are atomic rewrite steps. 43 For every conversion there is a corresponding inference step. 44*) 45 46type conv = Argo_Expr.expr -> Argo_Expr.expr * Argo_Proof.conv 47 48fun keep e = (e, Argo_Proof.keep_conv) 49 50fun seq [] e = keep e 51 | seq [cv] e = cv e 52 | seq (cv :: cvs) e = 53 let val ((e, c2), c1) = cv e |>> seq cvs 54 in (e, Argo_Proof.mk_then_conv c1 c2) end 55 56fun on_args f (Argo_Expr.E (k, es)) = 57 let val (es, cs) = split_list (f es) 58 in (Argo_Expr.E (k, es), Argo_Proof.mk_args_conv k cs) end 59 60fun args cv e = on_args (map cv) e 61 62fun all_args cv k (e as Argo_Expr.E (k', _)) = if k = k' then args (all_args cv k) e else cv e 63 64fun rewr r e _ = (e, Argo_Proof.mk_rewr_conv r) 65 66 67(* rewriting result *) 68 69(* 70 After rewriting an expression, further rewritings might be applicable. The result type is 71 a simple means to control which parts of the rewriting result should be rewritten further. 72 Only the top-most part of a result marked by R constructors is amenable to further rewritings. 73*) 74 75datatype result = 76 E of Argo_Expr.expr | 77 R of Argo_Expr.kind * result list 78 79fun expr_of (E e) = e 80 | expr_of (R (k, ps)) = Argo_Expr.E (k, map expr_of ps) 81 82fun top_most _ (E _) e = keep e 83 | top_most cv (R (_, ps)) e = seq [on_args (map2 (top_most cv) ps), cv] e 84 85 86(* context *) 87 88(* 89 The context stores lists of rewritings for every expression kind. A rewriting maps the 90 arguments of an expression with matching kind to an optional rewriting result. Each 91 rewriting might decide whether it is applicable to the given expression arguments and 92 might return no result. The first rewriting that produces a result is applied. 93*) 94 95structure Kindtab = Table(type key = Argo_Expr.kind val ord = Argo_Expr.kind_ord) 96 97type context = 98 (int -> Argo_Expr.expr list -> (Argo_Proof.rewrite * result) option) list Kindtab.table 99 100val context: context = Kindtab.empty 101 102fun add_func k f = Kindtab.map_default (k, []) (fn fs => fs @ [f]) 103fun add_func' k f = add_func k (fn _ => f) 104 105fun unary k f = add_func' k (fn [e] => f e | _ => raise Fail "not unary") 106fun binary k f = add_func' k (fn [e1, e2] => f e1 e2 | _ => raise Fail "not binary") 107fun ternary k f = add_func' k (fn [e1, e2, e3] => f e1 e2 e3 | _ => raise Fail "not ternary") 108fun nary k f = add_func k f 109 110 111(* rewriting *) 112 113(* 114 Rewriting proceeds bottom-up. The top-most result of a rewriting step is rewritten again 115 bottom-up, if necessary. Only the first rewriting that produces a result for a given 116 expression is applied. N-ary expressions are flattened before they are rewritten. For 117 instance, flattening (and p (and q r)) produces (and p q r) where p, q and r are no 118 conjunctions. 119*) 120 121fun first_rewr cv cx k n es e = 122 (case get_first (fn f => f n es) (Kindtab.lookup_list cx k) of 123 NONE => keep e 124 | SOME (r, res) => seq [rewr r (expr_of res), top_most cv res] e) 125 126fun all_args_of k (e as Argo_Expr.E (k', es)) = if k = k' then maps (all_args_of k) es else [e] 127fun kind_depth_of k (Argo_Expr.E (k', es)) = 128 if k = k' then 1 + fold (Integer.max o kind_depth_of k) es 0 else 0 129 130fun norm_kind cv cx (e as Argo_Expr.E (k, es)) = 131 let val (n, es) = if Argo_Expr.is_nary k then (kind_depth_of k e, all_args_of k e) else (1, es) 132 in first_rewr cv cx k n es e end 133 134fun norm_args cv d (e as Argo_Expr.E (k, _)) = 135 if d = 0 then keep e 136 else if Argo_Expr.is_nary k then all_args (cv (d - 1)) k e 137 else args (cv (d - 1)) e 138 139fun norm cx d e = seq [norm_args (norm cx) d, norm_kind (norm cx 0) cx] e 140 141fun rewrite cx = norm cx ~1 (* bottom-up rewriting *) 142fun rewrite_top cx = norm cx 0 (* top-most rewriting *) 143 144fun with_proof cv (e, p) prf = 145 let 146 val (e, c) = cv e 147 val (p, prf) = Argo_Proof.mk_rewrite c p prf 148 in ((e, p), prf) end 149 150 151(* result constructors *) 152 153fun mk_nary _ e [] = e 154 | mk_nary _ _ [e] = e 155 | mk_nary k _ es = R (k, es) 156 157val e_true = E Argo_Expr.true_expr 158val e_false = E Argo_Expr.false_expr 159fun mk_not e = R (Argo_Expr.Not, [e]) 160fun mk_and es = mk_nary Argo_Expr.And e_true es 161fun mk_or es = mk_nary Argo_Expr.Or e_false es 162fun mk_iff e1 e2 = R (Argo_Expr.Iff, [e1, e2]) 163fun mk_ite e1 e2 e3 = R (Argo_Expr.Ite, [e1, e2, e3]) 164fun mk_num n = E (Argo_Expr.mk_num n) 165fun mk_neg e = R (Argo_Expr.Neg, [e]) 166fun mk_add [] = raise Fail "bad addition" 167 | mk_add [e] = e 168 | mk_add es = R (Argo_Expr.Add, es) 169fun mk_sub e1 e2 = R (Argo_Expr.Sub, [e1, e2]) 170fun mk_mul e1 e2 = R (Argo_Expr.Mul, [e1, e2]) 171fun mk_div e1 e2 = R (Argo_Expr.Div, [e1, e2]) 172fun mk_le e1 e2 = R (Argo_Expr.Le, [e1, e2]) 173fun mk_le' e1 e2 = mk_le (E e1) (E e2) 174fun mk_eq e1 e2 = R (Argo_Expr.Eq, [e1, e2]) 175 176 177(* rewriting to negation normal form *) 178 179fun rewr_not (Argo_Expr.E exp) = 180 (case exp of 181 (Argo_Expr.True, _) => SOME (Argo_Proof.Rewr_Not_True, e_false) 182 | (Argo_Expr.False, _) => SOME (Argo_Proof.Rewr_Not_False, e_true) 183 | (Argo_Expr.Not, [e]) => SOME (Argo_Proof.Rewr_Not_Not, E e) 184 | (Argo_Expr.And, es) => SOME (Argo_Proof.Rewr_Not_And (length es), mk_or (map (mk_not o E) es)) 185 | (Argo_Expr.Or, es) => SOME (Argo_Proof.Rewr_Not_Or (length es), mk_and (map (mk_not o E) es)) 186 | (Argo_Expr.Iff, [Argo_Expr.E (Argo_Expr.Not, [e1]), e2]) => 187 SOME (Argo_Proof.Rewr_Not_Iff, mk_iff (E e1) (E e2)) 188 | (Argo_Expr.Iff, [e1, Argo_Expr.E (Argo_Expr.Not, [e2])]) => 189 SOME (Argo_Proof.Rewr_Not_Iff, mk_iff (E e1) (E e2)) 190 | (Argo_Expr.Iff, [e1, e2]) => 191 SOME (Argo_Proof.Rewr_Not_Iff, mk_iff (mk_not (E e1)) (E e2)) 192 | _ => NONE) 193 194val nnf = unary Argo_Expr.Not rewr_not 195 196 197(* propositional normalization *) 198 199(* 200 Propositional expressions are transformed into literals in the clausifier. Having 201 fewer literals results in faster solver execution. Normalizing propositional expressions 202 turns similar expressions into equal expressions, for which the same literal can be used. 203 The clausifier expects that only negation, disjunction, conjunction and equivalence form 204 propositional expressions. Expressions may be simplified to truth or falsity, but both 205 truth and falsity eventually occur nowhere inside expressions. 206*) 207 208fun first_index pred xs = 209 let val i = find_index pred xs 210 in if i >= 0 then SOME i else NONE end 211 212fun rewr_zero r zero _ es = 213 Option.map (fn i => (r i, E zero)) (first_index (curry Argo_Expr.eq_expr zero) es) 214 215fun rewr_dual r zero _ = 216 let 217 fun duals _ [] = NONE 218 | duals _ [_] = NONE 219 | duals i (e :: es) = 220 (case first_index (Argo_Expr.dual_expr e) es of 221 NONE => duals (i + 1) es 222 | SOME i' => SOME (r (i, i + i' + 1), zero)) 223 in duals 0 end 224 225fun rewr_sort r one mk n es = 226 let 227 val l = length es 228 fun add (i, e) = if Argo_Expr.eq_expr (e, one) then I else Argo_Exprtab.cons_list (e, i) 229 fun dest (e, i) (es, is) = (e :: es, i :: is) 230 val (es, iss) = Argo_Exprtab.fold_rev dest (fold_index add es Argo_Exprtab.empty) ([], []) 231 fun identity is = length is = l andalso forall (op =) (map_index I is) 232 in 233 if null iss then SOME (r (l, [[0]]), E one) 234 else if n = 1 andalso identity (map hd iss) then NONE 235 else (SOME (r (l, iss), mk (map E es))) 236 end 237 238fun rewr_imp e1 e2 = SOME (Argo_Proof.Rewr_Imp, mk_or [mk_not (E e1), E e2]) 239 240fun rewr_iff (e1 as Argo_Expr.E exp1) (e2 as Argo_Expr.E exp2) = 241 (case (exp1, exp2) of 242 ((Argo_Expr.True, _), _) => SOME (Argo_Proof.Rewr_Iff_True, E e2) 243 | ((Argo_Expr.False, _), _) => SOME (Argo_Proof.Rewr_Iff_False, mk_not (E e2)) 244 | (_, (Argo_Expr.True, _)) => SOME (Argo_Proof.Rewr_Iff_True, E e1) 245 | (_, (Argo_Expr.False, _)) => SOME (Argo_Proof.Rewr_Iff_False, mk_not (E e1)) 246 | ((Argo_Expr.Not, [e1']), (Argo_Expr.Not, [e2'])) => 247 SOME (Argo_Proof.Rewr_Iff_Not_Not, mk_iff (E e1') (E e2')) 248 | _ => 249 if Argo_Expr.dual_expr e1 e2 then SOME (Argo_Proof.Rewr_Iff_Dual, e_false) 250 else 251 (case Argo_Expr.expr_ord (e1, e2) of 252 EQUAL => SOME (Argo_Proof.Rewr_Iff_Refl, e_true) 253 | GREATER => SOME (Argo_Proof.Rewr_Iff_Symm, mk_iff (E e2) (E e1)) 254 | LESS => NONE)) 255 256val norm_prop = 257 nary Argo_Expr.And (rewr_zero Argo_Proof.Rewr_And_False Argo_Expr.false_expr) #> 258 nary Argo_Expr.And (rewr_dual Argo_Proof.Rewr_And_Dual e_false) #> 259 nary Argo_Expr.And (rewr_sort Argo_Proof.Rewr_And_Sort Argo_Expr.true_expr mk_and) #> 260 nary Argo_Expr.Or (rewr_zero Argo_Proof.Rewr_Or_True Argo_Expr.true_expr) #> 261 nary Argo_Expr.Or (rewr_dual Argo_Proof.Rewr_Or_Dual e_true) #> 262 nary Argo_Expr.Or (rewr_sort Argo_Proof.Rewr_Or_Sort Argo_Expr.false_expr mk_or) #> 263 binary Argo_Expr.Imp rewr_imp #> 264 binary Argo_Expr.Iff rewr_iff 265 266 267(* normalization of if-then-else expressions *) 268 269fun rewr_ite (Argo_Expr.E (Argo_Expr.True, _)) e _ = SOME (Argo_Proof.Rewr_Ite_True, E e) 270 | rewr_ite (Argo_Expr.E (Argo_Expr.False, _)) _ e = SOME (Argo_Proof.Rewr_Ite_False, E e) 271 | rewr_ite e1 e2 e3 = 272 if Argo_Expr.type_of e2 = Argo_Expr.Bool then 273 SOME (Argo_Proof.Rewr_Ite_Prop, 274 mk_and (map mk_or [[mk_not (E e1), E e2], [E e1, E e3], [E e2, E e3]])) 275 else if Argo_Expr.eq_expr (e2, e3) then SOME (Argo_Proof.Rewr_Ite_Eq, E e2) 276 else NONE 277 278val norm_ite = ternary Argo_Expr.Ite rewr_ite 279 280 281(* normalization of equality *) 282 283(* 284 In a normalized equality, the left-hand side is less than the right-hand side with respect to 285 the expression order. 286*) 287 288fun rewr_eq e1 e2 = 289 (case Argo_Expr.expr_ord (e1, e2) of 290 EQUAL => SOME (Argo_Proof.Rewr_Eq_Refl, e_true) 291 | GREATER => SOME (Argo_Proof.Rewr_Eq_Symm, mk_eq (E e2) (E e1)) 292 | LESS => NONE) 293 294val norm_eq = binary Argo_Expr.Eq rewr_eq 295 296 297(* arithmetic normalization *) 298 299(* expression functions *) 300 301fun scale n e = 302 if n = @0 then mk_num @0 303 else if n = @1 then e 304 else mk_mul (mk_num n) e 305 306fun dest_factor (Argo_Expr.E (Argo_Expr.Mul, [Argo_Expr.E (Argo_Expr.Num n, _), _])) = n 307 | dest_factor _ = @1 308 309 310(* 311 Products are normalized either to a number or to the monomial form 312 a * x 313 where a is a non-zero number and is a variable or a product of variables. 314 If x is a product, it contains no number factors. If x is a product, it is sorted 315 based on the expression order. Hence, the product z * y * x will be rewritten 316 to x * y * z. The coefficient a is dropped if it is equal to one; 317 instead of 1 * x the expression x is used. 318*) 319 320fun mk_mul_comm e1 e2 = (Argo_Proof.Rewr_Mul_Comm, mk_mul (E e2) (E e1)) 321fun mk_mul_assocr e1 e2 e3 = 322 (Argo_Proof.Rewr_Mul_Assoc Argo_Proof.Right, mk_mul (mk_mul (E e1) (E e2)) (E e3)) 323 324 (* commute numbers to the left *) 325fun rewr_mul (Argo_Expr.E (Argo_Expr.Num n1, _)) (Argo_Expr.E (Argo_Expr.Num n2, _)) = 326 SOME (Argo_Proof.Rewr_Mul_Nums (n1, n2), mk_num (n1 * n2)) 327 | rewr_mul e1 (e2 as Argo_Expr.E (Argo_Expr.Num _, _)) = SOME (mk_mul_comm e1 e2) 328 | rewr_mul e1 (Argo_Expr.E (Argo_Expr.Mul, [e2 as Argo_Expr.E (Argo_Expr.Num _, _), e3])) = 329 SOME (mk_mul_assocr e1 e2 e3) 330 (* apply distributivity *) 331 | rewr_mul (Argo_Expr.E (Argo_Expr.Add, es)) e = 332 SOME (Argo_Proof.Rewr_Mul_Sum Argo_Proof.Left, mk_add (map (fn e' => mk_mul (E e') (E e)) es)) 333 | rewr_mul e (Argo_Expr.E (Argo_Expr.Add, es)) = 334 SOME (Argo_Proof.Rewr_Mul_Sum Argo_Proof.Right, mk_add (map (mk_mul (E e) o E) es)) 335 (* commute non-numerical factors to the right *) 336 | rewr_mul (Argo_Expr.E (Argo_Expr.Mul, [e1, e2])) e3 = 337 SOME (Argo_Proof.Rewr_Mul_Assoc Argo_Proof.Left, mk_mul (E e1) (mk_mul (E e2) (E e3))) 338 (* reduce special products *) 339 | rewr_mul (e1 as Argo_Expr.E (Argo_Expr.Num n, _)) e2 = 340 if n = @0 then SOME (Argo_Proof.Rewr_Mul_Zero, E e1) 341 else if n = @1 then SOME (Argo_Proof.Rewr_Mul_One, E e2) 342 else NONE 343 (* combine products with quotients *) 344 | rewr_mul (Argo_Expr.E (Argo_Expr.Div, [e1, e2])) e3 = 345 SOME (Argo_Proof.Rewr_Mul_Div Argo_Proof.Left, mk_div (mk_mul (E e1) (E e3)) (E e2)) 346 | rewr_mul e1 (Argo_Expr.E (Argo_Expr.Div, [e2, e3])) = 347 SOME (Argo_Proof.Rewr_Mul_Div Argo_Proof.Right, mk_div (mk_mul (E e1) (E e2)) (E e3)) 348 (* sort non-numerical factors *) 349 | rewr_mul e1 (Argo_Expr.E (Argo_Expr.Mul, [e2, e3])) = 350 (case Argo_Expr.expr_ord (e1, e2) of 351 GREATER => SOME (mk_mul_assocr e1 e2 e3) 352 | _ => NONE) 353 | rewr_mul e1 e2 = 354 (case Argo_Expr.expr_ord (e1, e2) of 355 GREATER => SOME (mk_mul_comm e1 e2) 356 | _ => NONE) 357 358(* 359 Quotients are normalized either to a number or to the monomial form 360 a * x 361 where a is a non-zero number and x is a variable. If x is a quotient, 362 both dividend and divisor are not a number. The dividend and the divisor may both 363 be products. If so, neither dividend nor divisor contains a numerical factor. 364 Both dividend and divisor are not themselves quotients again. The dividend is never 365 a sum; distributivity is applied to such quotients. The coefficient a is dropped 366 if it is equal to one; instead of 1 * x the expression x is used. 367 368 Several non-linear expressions can be rewritten to the described normal form. 369 For example, the expressions (x * z) / y and x * (z / y) will be treated as equal 370 variables by the arithmetic decision procedure. Yet, non-linear expression rewriting 371 is incomplete and keeps several other expressions unchanged. 372*) 373 374fun rewr_div (Argo_Expr.E (Argo_Expr.Div, [e1, e2])) e3 = 375 SOME (Argo_Proof.Rewr_Div_Div Argo_Proof.Left, mk_div (E e1) (mk_mul (E e2) (E e3))) 376 | rewr_div e1 (Argo_Expr.E (Argo_Expr.Div, [e2, e3])) = 377 SOME (Argo_Proof.Rewr_Div_Div Argo_Proof.Right, mk_div (mk_mul (E e1) (E e3)) (E e2)) 378 | rewr_div (Argo_Expr.E (Argo_Expr.Num n1, _)) (Argo_Expr.E (Argo_Expr.Num n2, _)) = 379 if n2 = @0 then NONE 380 else SOME (Argo_Proof.Rewr_Div_Nums (n1, n2), mk_num (n1 / n2)) 381 | rewr_div (Argo_Expr.E (Argo_Expr.Num n, _)) e = 382 if n = @0 then SOME (Argo_Proof.Rewr_Div_Zero, mk_num @0) 383 else if n = @1 then NONE 384 else SOME (Argo_Proof.Rewr_Div_Num (Argo_Proof.Left, n), scale n (mk_div (mk_num @1) (E e))) 385 | rewr_div (Argo_Expr.E (Argo_Expr.Mul, [Argo_Expr.E (Argo_Expr.Num n, _), e1])) e2 = 386 SOME (Argo_Proof.Rewr_Div_Mul (Argo_Proof.Left, n), scale n (mk_div (E e1) (E e2))) 387 | rewr_div e (Argo_Expr.E (Argo_Expr.Num n, _)) = 388 if n = @0 then NONE 389 else if n = @1 then SOME (Argo_Proof.Rewr_Div_One, E e) 390 else SOME (Argo_Proof.Rewr_Div_Num (Argo_Proof.Right, n), scale (Rat.inv n) (E e)) 391 | rewr_div e1 (Argo_Expr.E (Argo_Expr.Mul, [Argo_Expr.E (Argo_Expr.Num n, _), e2])) = 392 SOME (Argo_Proof.Rewr_Div_Mul (Argo_Proof.Right, n), scale (Rat.inv n) (mk_div (E e1) (E e2))) 393 | rewr_div (Argo_Expr.E (Argo_Expr.Add, es)) e = 394 SOME (Argo_Proof.Rewr_Div_Sum, mk_add (map (fn e' => mk_div (E e') (E e)) es)) 395 | rewr_div _ _ = NONE 396 397 398(* 399 Sums are flattened and normalized to the polynomial form 400 a_0 + a_1 * x_1 + ... + a_n * x_n 401 where all variables x_i are disjoint and where all coefficients a_i are 402 non-zero numbers. Coefficients equal to one are dropped; instead of 1 * x_i 403 the reduced monom x_i is used. The variables x_i are ordered based on the 404 expression order to reduce the number of problem literals by sharing equal 405 expressions. 406*) 407 408fun add_monom_expr i n e (p, s, etab) = 409 let val etab = Argo_Exprtab.map_default (e, (i, @0)) (apsnd (Rat.add n)) etab 410 in ((n, Option.map fst (Argo_Exprtab.lookup etab e)) :: p, s, etab) end 411 412fun add_monom (_, Argo_Expr.E (Argo_Expr.Num n, _)) (p, s, etab) = ((n, NONE) :: p, s + n, etab) 413 | add_monom (i, Argo_Expr.E (Argo_Expr.Mul, [Argo_Expr.E (Argo_Expr.Num n, _), e])) x = 414 add_monom_expr i n e x 415 | add_monom (i, e) x = add_monom_expr i @1 e x 416 417fun rewr_add d es = 418 let 419 val (p1, s, etab) = fold_index add_monom es ([], @0, Argo_Exprtab.empty) 420 val (p2, es) = 421 [] 422 |> Argo_Exprtab.fold_rev (fn (e, (i, n)) => n <> @0 ? cons ((n, SOME i), scale n (E e))) etab 423 |> s <> @0 ? cons ((s, NONE), mk_num s) 424 |> (fn [] => [((@0, NONE), mk_num @0)] | xs => xs) 425 |> split_list 426 val ps = (rev p1, p2) 427 in 428 if d = 1 andalso eq_list (op =) ps then NONE 429 else SOME (Argo_Proof.Rewr_Add ps, mk_add es) 430 end 431 432 433(* 434 Equations are normalized to the normal form 435 a_0 + a_1 * x_1 + ... + a_n * x_n = b 436 or 437 b = a_0 + a_1 * x_1 + ... + a_n * x_n 438 An equation in normal form is rewritten to a conjunction of two non-strict inequalities. 439*) 440 441fun rewr_eq_le e1 e2 = SOME (Argo_Proof.Rewr_Eq_Le, mk_and [mk_le' e1 e2, mk_le' e2 e1]) 442 443fun rewr_arith_eq (Argo_Expr.E (Argo_Expr.Num n1, _)) (Argo_Expr.E (Argo_Expr.Num n2, _)) = 444 let val b = (n1 = n2) 445 in SOME (Argo_Proof.Rewr_Eq_Nums b, if b then e_true else e_false) end 446 | rewr_arith_eq (e1 as Argo_Expr.E (Argo_Expr.Num _, _)) e2 = rewr_eq_le e1 e2 447 | rewr_arith_eq e1 (e2 as Argo_Expr.E (Argo_Expr.Num _, _)) = rewr_eq_le e1 e2 448 | rewr_arith_eq e1 e2 = SOME (Argo_Proof.Rewr_Eq_Sub, mk_eq (mk_sub (E e1) (E e2)) (mk_num @0)) 449 450fun is_arith e = member (op =) [Argo_Expr.Real] (Argo_Expr.type_of e) 451 452fun rewr_eq e1 e2 = if is_arith e1 then rewr_arith_eq e1 e2 else NONE 453 454 455(* 456 Arithmetic inequalities (less and less-than) are normalized to the normal form 457 a_0 + a_1 * x_1 + ... + a_n * x_n ~ b 458 or 459 b ~ a_0 + a_1 * x_1 + ... + a_n * x_n 460 such that most of the coefficients a_i are positive. 461 462 Arithmetic inequalities of the form 463 a * x ~ b 464 or 465 b ~ a * x 466 are normalized to the form 467 x ~ c 468 or 469 c ~ x 470 where c is a number. 471*) 472 473fun norm_cmp_mul k r f e1 e2 n = 474 let val es = if n > @0 then [e1, e2] else [e2, e1] 475 in SOME (Argo_Proof.Rewr_Ineq_Mul (r, n), R (k, f (map (scale n o E) es))) end 476 477fun count_factors pred es = fold (fn e => if pred (dest_factor e) then Integer.add 1 else I) es 0 478 479fun norm_cmp_swap k r f e1 e2 es = 480 let 481 val pos = count_factors (fn n => n > @0) es 482 val neg = count_factors (fn n => n < @0) es 483 val keep = pos > neg orelse (pos = neg andalso dest_factor (hd es) > @0) 484 in if keep then NONE else norm_cmp_mul k r f e1 e2 @~1 end 485 486fun norm_cmp1 k r f e1 (e2 as Argo_Expr.E (Argo_Expr.Mul, [Argo_Expr.E (Argo_Expr.Num n, _), _])) = 487 norm_cmp_mul k r f e1 e2 (Rat.inv n) 488 | norm_cmp1 k r f e1 (e2 as Argo_Expr.E (Argo_Expr.Add, Argo_Expr.E (Argo_Expr.Num n, _) :: _)) = 489 let fun mk e = mk_add [E e, mk_num (~ n)] 490 in SOME (Argo_Proof.Rewr_Ineq_Add (r, ~ n), R (k, f [mk e1, mk e2])) end 491 | norm_cmp1 k r f e1 (e2 as Argo_Expr.E (Argo_Expr.Add, es)) = norm_cmp_swap k r f e1 e2 es 492 | norm_cmp1 _ _ _ _ _ = NONE 493 494fun rewr_cmp _ r pred (Argo_Expr.E (Argo_Expr.Num n1, _)) (Argo_Expr.E (Argo_Expr.Num n2, _)) = 495 let val b = pred n1 n2 496 in SOME (Argo_Proof.Rewr_Ineq_Nums (r, b), if b then e_true else e_false) end 497 | rewr_cmp k r _ (e1 as Argo_Expr.E (Argo_Expr.Num _, _)) e2 = norm_cmp1 k r I e1 e2 498 | rewr_cmp k r _ e1 (e2 as Argo_Expr.E (Argo_Expr.Num _, _)) = norm_cmp1 k r rev e2 e1 499 | rewr_cmp k r _ e1 e2 = 500 SOME (Argo_Proof.Rewr_Ineq_Sub r, R (k, [mk_sub (E e1) (E e2), mk_num @0])) 501 502 503(* 504 Arithmetic expressions are normalized in order to reduce the number of 505 problem literals. Arithmetically equal expressions are normalized to 506 syntactically equal expressions as much as possible. 507*) 508 509fun rewr_neg e = SOME (Argo_Proof.Rewr_Neg, scale @~1 (E e)) 510fun rewr_sub e1 e2 = SOME (Argo_Proof.Rewr_Sub, mk_add [E e1, scale @~1 (E e2)]) 511fun rewr_abs e = SOME (Argo_Proof.Rewr_Abs, mk_ite (mk_le (mk_num @0) (E e)) (E e) (mk_neg (E e))) 512 513fun rewr_min e1 e2 = 514 (case Argo_Expr.expr_ord (e1, e2) of 515 LESS => SOME (Argo_Proof.Rewr_Min_Lt, mk_ite (mk_le' e1 e2) (E e1) (E e2)) 516 | EQUAL => SOME (Argo_Proof.Rewr_Min_Eq, E e1) 517 | GREATER => SOME (Argo_Proof.Rewr_Min_Gt, mk_ite (mk_le' e2 e1) (E e2) (E e1))) 518 519fun rewr_max e1 e2 = 520 (case Argo_Expr.expr_ord (e1, e2) of 521 LESS => SOME (Argo_Proof.Rewr_Max_Lt, mk_ite (mk_le' e1 e2) (E e2) (E e1)) 522 | EQUAL => SOME (Argo_Proof.Rewr_Max_Eq, E e1) 523 | GREATER => SOME (Argo_Proof.Rewr_Max_Gt, mk_ite (mk_le' e2 e1) (E e1) (E e2))) 524 525val norm_add = nary Argo_Expr.Add rewr_add 526val norm_mul = binary Argo_Expr.Mul rewr_mul 527 528val norm_arith = 529 unary Argo_Expr.Neg rewr_neg #> 530 binary Argo_Expr.Sub rewr_sub #> 531 norm_mul #> 532 binary Argo_Expr.Div rewr_div #> 533 norm_add #> 534 binary Argo_Expr.Min rewr_min #> 535 binary Argo_Expr.Max rewr_max #> 536 unary Argo_Expr.Abs rewr_abs #> 537 binary Argo_Expr.Eq rewr_eq #> 538 binary Argo_Expr.Le (rewr_cmp Argo_Expr.Le Argo_Proof.Le Rat.le) #> 539 binary Argo_Expr.Lt (rewr_cmp Argo_Expr.Lt Argo_Proof.Lt Rat.lt) 540 541end 542