# HG changeset patch # User boehmes # Date 1484942711 -3600 # Node ID a5a09855e4246bfd3d8ccd5b1d80f01479130d75 # Parent 75ee8475c37e87390c58bc53faa90f45628172a7 less complex rewriting of Argo expressions: select candidate rewrite rules by analyzing only on the kind of the head expression, then select the applicable rewrite rule using ML pattern matching; keep all normalization code in a single place: modules of decision procedures focus on their core aspects; more normalization for non-linear arithmetic diff -r 75ee8475c37e -r a5a09855e424 src/HOL/Tools/Argo/argo_real.ML --- a/src/HOL/Tools/Argo/argo_real.ML Fri Jan 20 17:22:54 2017 +0100 +++ b/src/HOL/Tools/Argo/argo_real.ML Fri Jan 20 21:05:11 2017 +0100 @@ -90,6 +90,7 @@ val add_nums_conv = nums_conv mk_plus (op +) val mul_nums_conv = nums_conv mk_times (op *) val div_nums_conv = nums_conv mk_divide (op /) +fun inv_num_conv ctxt = nums_conv mk_divide (fn (_, n) => Rat.inv n) ctxt @1 fun cmp_nums_conv ctxt b ct = let val t = if b then @{const HOL.True} else @{const HOL.False} @@ -192,9 +193,15 @@ end -val mul_sum_thm = mk_rewr @{lemma "(x::real) * (y + z) = x * y + x * z" by (rule ring_distribs)} -fun mul_sum_conv ct = - Conv.try_conv (Conv.rewr_conv mul_sum_thm then_conv Conv.binop_conv mul_sum_conv) ct +val mul_suml_thm = mk_rewr @{lemma "((x::real) + y) * z = x * z + y * z" by (rule ring_distribs)} +val mul_sumr_thm = mk_rewr @{lemma "(x::real) * (y + z) = x * y + x * z" by (rule ring_distribs)} +fun mul_sum_conv thm ct = + Conv.try_conv (Conv.rewr_conv thm then_conv Conv.binop_conv (mul_sum_conv thm)) ct + +val div_sum_thm = mk_rewr @{lemma "((x::real) + y) / z = x / z + y / z" + by (rule add_divide_distrib)} +fun div_sum_conv ct = + Conv.try_conv (Conv.rewr_conv div_sum_thm then_conv Conv.binop_conv div_sum_conv) ct fun var_of_add_cmp (_ $ _ $ (_ $ _ $ (_ $ _ $ Var v))) = v | var_of_add_cmp t = raise TERM ("var_of_add_cmp", [t]) @@ -212,16 +219,28 @@ val mul_zero_thm = mk_rewr @{lemma "0 * (x::real) = 0" by (rule mult_zero_left)} val mul_one_thm = mk_rewr @{lemma "1 * (x::real) = x" by (rule mult_1)} val mul_comm_thm = mk_rewr @{lemma "(x::real) * y = y * x" by simp} -val mul_assoc_thm = mk_rewr @{lemma "(x::real) * (y * z) = (x * y) * z" by simp} -val div_zero_thm = mk_rewr @{lemma "0 / (x::real) = 0" by simp} -val div_one_thm = mk_rewr @{lemma "(x::real) / 1 = x" by simp} -val div_mul_thm = mk_rewr @{lemma "(x::real) / y = x * (1 / y)" by simp} -val div_inv_thm = mk_rewr @{lemma "(x::real) / y = (1 / y) * x" by simp} -val div_left_thm = mk_rewr @{lemma "((x::real) * y) / z = x * (y / z)" by simp} -val div_right_thm = mk_rewr @{lemma "(x::real) / (y * z) = (1 / y) * (x / z)" by simp} -val min_thm = mk_rewr @{lemma "min (x::real) y = (if x <= y then x else y)" by (rule min_def)} -val max_thm = mk_rewr @{lemma "max (x::real) y = (if x <= y then y else x)" by (rule max_def)} +val mul_assocl_thm = mk_rewr @{lemma "((x::real) * y) * z = x * (y * z)" by simp} +val mul_assocr_thm = mk_rewr @{lemma "(x::real) * (y * z) = (x * y) * z" by simp} +val mul_divl_thm = mk_rewr @{lemma "((x::real) / y) * z = (x * z) / y" by simp} +val mul_divr_thm = mk_rewr @{lemma "(x::real) * (y / z) = (x * y) / z" by simp} +val div_zero_thm = mk_rewr @{lemma "0 / (x::real) = 0" by (rule div_0)} +val div_one_thm = mk_rewr @{lemma "(x::real) / 1 = x" by (rule div_by_1)} +val div_numl_thm = mk_rewr @{lemma "(x::real) / y = x * (1 / y)" by simp} +val div_numr_thm = mk_rewr @{lemma "(x::real) / y = (1 / y) * x" by simp} +val div_mull_thm = mk_rewr @{lemma "((x::real) * y) / z = x * (y / z)" by simp} +val div_mulr_thm = mk_rewr @{lemma "(x::real) / (y * z) = (1 / y) * (x / z)" by simp} +val div_divl_thm = mk_rewr @{lemma "((x::real) / y) / z = x / (y * z)" by simp} +val div_divr_thm = mk_rewr @{lemma "(x::real) / (y / z) = (x * z) / y" by simp} +val min_eq_thm = mk_rewr @{lemma "min (x::real) x = x" by (simp add: min_def)} +val min_lt_thm = mk_rewr @{lemma "min (x::real) y = (if x <= y then x else y)" by (rule min_def)} +val min_gt_thm = mk_rewr @{lemma "min (x::real) y = (if y <= x then y else x)" + by (simp add: min_def)} +val max_eq_thm = mk_rewr @{lemma "max (x::real) x = x" by (simp add: max_def)} +val max_lt_thm = mk_rewr @{lemma "max (x::real) y = (if x <= y then y else x)" by (rule max_def)} +val max_gt_thm = mk_rewr @{lemma "max (x::real) y = (if y <= x then x else y)" + by (simp add: max_def)} val abs_thm = mk_rewr @{lemma "abs (x::real) = (if 0 <= x then x else -x)" by simp} +val sub_eq_thm = mk_rewr @{lemma "((x::real) = y) = (x - y = 0)" by simp} val eq_le_thm = mk_rewr @{lemma "((x::real) = y) = ((x <= y) & (y <= x))" by (rule order_eq_iff)} val add_le_thm = mk_rewr @{lemma "((x::real) <= y) = (x + n <= y + n)" by simp} val add_lt_thm = mk_rewr @{lemma "((x::real) < y) = (x + n < y + n)" by simp} @@ -241,18 +260,33 @@ | replay_rewr _ Argo_Proof.Rewr_Mul_One = Conv.rewr_conv mul_one_thm | replay_rewr ctxt (Argo_Proof.Rewr_Mul_Nums (n, m)) = mul_nums_conv ctxt n m | replay_rewr _ Argo_Proof.Rewr_Mul_Comm = Conv.rewr_conv mul_comm_thm - | replay_rewr _ Argo_Proof.Rewr_Mul_Assoc = Conv.rewr_conv mul_assoc_thm - | replay_rewr _ Argo_Proof.Rewr_Mul_Sum = mul_sum_conv - | replay_rewr ctxt (Argo_Proof.Rewr_Div_Nums (n, m)) = div_nums_conv ctxt n m + | replay_rewr _ (Argo_Proof.Rewr_Mul_Assoc Argo_Proof.Left) = Conv.rewr_conv mul_assocl_thm + | replay_rewr _ (Argo_Proof.Rewr_Mul_Assoc Argo_Proof.Right) = Conv.rewr_conv mul_assocr_thm + | replay_rewr _ (Argo_Proof.Rewr_Mul_Sum Argo_Proof.Left) = mul_sum_conv mul_suml_thm + | replay_rewr _ (Argo_Proof.Rewr_Mul_Sum Argo_Proof.Right) = mul_sum_conv mul_sumr_thm + | replay_rewr _ (Argo_Proof.Rewr_Mul_Div Argo_Proof.Left) = Conv.rewr_conv mul_divl_thm + | replay_rewr _ (Argo_Proof.Rewr_Mul_Div Argo_Proof.Right) = Conv.rewr_conv mul_divr_thm | replay_rewr _ Argo_Proof.Rewr_Div_Zero = Conv.rewr_conv div_zero_thm | replay_rewr _ Argo_Proof.Rewr_Div_One = Conv.rewr_conv div_one_thm - | replay_rewr _ Argo_Proof.Rewr_Div_Mul = Conv.rewr_conv div_mul_thm - | replay_rewr _ Argo_Proof.Rewr_Div_Inv = Conv.rewr_conv div_inv_thm - | replay_rewr _ Argo_Proof.Rewr_Div_Left = Conv.rewr_conv div_left_thm - | replay_rewr _ Argo_Proof.Rewr_Div_Right = Conv.rewr_conv div_right_thm - | replay_rewr _ Argo_Proof.Rewr_Min = Conv.rewr_conv min_thm - | replay_rewr _ Argo_Proof.Rewr_Max = Conv.rewr_conv max_thm + | replay_rewr ctxt (Argo_Proof.Rewr_Div_Nums (n, m)) = div_nums_conv ctxt n m + | replay_rewr _ (Argo_Proof.Rewr_Div_Num (Argo_Proof.Left, _)) = Conv.rewr_conv div_numl_thm + | replay_rewr ctxt (Argo_Proof.Rewr_Div_Num (Argo_Proof.Right, n)) = + Conv.rewr_conv div_numr_thm then_conv Conv.arg1_conv (inv_num_conv ctxt n) + | replay_rewr _ (Argo_Proof.Rewr_Div_Mul (Argo_Proof.Left, _)) = Conv.rewr_conv div_mull_thm + | replay_rewr ctxt (Argo_Proof.Rewr_Div_Mul (Argo_Proof.Right, n)) = + Conv.rewr_conv div_mulr_thm then_conv Conv.arg1_conv (inv_num_conv ctxt n) + | replay_rewr _ (Argo_Proof.Rewr_Div_Div Argo_Proof.Left) = Conv.rewr_conv div_divl_thm + | replay_rewr _ (Argo_Proof.Rewr_Div_Div Argo_Proof.Right) = Conv.rewr_conv div_divr_thm + | replay_rewr _ Argo_Proof.Rewr_Div_Sum = div_sum_conv + | replay_rewr _ Argo_Proof.Rewr_Min_Eq = Conv.rewr_conv min_eq_thm + | replay_rewr _ Argo_Proof.Rewr_Min_Lt = Conv.rewr_conv min_lt_thm + | replay_rewr _ Argo_Proof.Rewr_Min_Gt = Conv.rewr_conv min_gt_thm + | replay_rewr _ Argo_Proof.Rewr_Max_Eq = Conv.rewr_conv max_eq_thm + | replay_rewr _ Argo_Proof.Rewr_Max_Lt = Conv.rewr_conv max_lt_thm + | replay_rewr _ Argo_Proof.Rewr_Max_Gt = Conv.rewr_conv max_gt_thm | replay_rewr _ Argo_Proof.Rewr_Abs = Conv.rewr_conv abs_thm + | replay_rewr ctxt (Argo_Proof.Rewr_Eq_Nums b) = cmp_nums_conv ctxt b + | replay_rewr _ Argo_Proof.Rewr_Eq_Sub = Conv.rewr_conv sub_eq_thm | replay_rewr _ Argo_Proof.Rewr_Eq_Le = Conv.rewr_conv eq_le_thm | replay_rewr ctxt (Argo_Proof.Rewr_Ineq_Nums (_, b)) = cmp_nums_conv ctxt b | replay_rewr ctxt (Argo_Proof.Rewr_Ineq_Add (Argo_Proof.Le, n)) = diff -r 75ee8475c37e -r a5a09855e424 src/HOL/ex/Argo_Examples.thy --- a/src/HOL/ex/Argo_Examples.thy Fri Jan 20 17:22:54 2017 +0100 +++ b/src/HOL/ex/Argo_Examples.thy Fri Jan 20 21:05:11 2017 +0100 @@ -145,6 +145,10 @@ and "~(d | False) | c" and "~(c | (~p & (p | (q & ~q))))" then have "False" by argo +next + have "(True & True & True) = True" by argo +next + have "(False | False | False) = False" by argo end @@ -322,11 +326,16 @@ "2 * a = a * 2" "2 * a * 3 = 6 * a" "2 * a * 3 * 5 = 30 * a" + "2 * (a * (3 * 5)) = 30 * a" "a * 0 * b = 0" "a * (0 * b) = 0" + "a * b = b * a" + "a * b * a = b * a * a" "a * (b * c) = (a * b) * c" "a * (b * (c * d)) = ((a * b) * c) * d" + "a * (b * (c * d)) = ((d * c) * b) * a" "a * (b + c + d) = a * b + a * c + a * d" + "(a + b + c) * d = a * d + b * d + c * d" by argo+ end @@ -335,7 +344,7 @@ notepad begin - fix a b c :: real + fix a b c d :: real have "(6::real) / 2 = 3" "a / 0 = a / 0" @@ -345,12 +354,19 @@ "a / 1 = a" "a / 3 = 1/3 * a" "6 * a / 2 = 3 * a" + "(6 * a) / 2 = 3 * a" "a / ((5 * b) / 2) = 2/5 * a / b" "a / (5 * (b / 2)) = 2/5 * a / b" "(a / 5) * (b / 2) = 1/10 * a * b" "a / (3 * b) = 1/3 * a / b" "(a + b) / 5 = 1/5 * a + 1/5 * b" "a / (5 * 1/5) = a" + "a * (b / c) = (b * a) / c" + "(a / b) * c = (c * a) / b" + "(a / b) / (c / d) = (a * d) / (c * b)" + "1 / (a * b) = 1 / (b * a)" + "a / (3 * b) = 1 / 3 * a / b" + "(a + b + c) / d = a / d + b / d + c / d" by argo+ end diff -r 75ee8475c37e -r a5a09855e424 src/Tools/Argo/argo_cc.ML --- a/src/Tools/Argo/argo_cc.ML Fri Jan 20 17:22:54 2017 +0100 +++ b/src/Tools/Argo/argo_cc.ML Fri Jan 20 21:05:11 2017 +0100 @@ -33,9 +33,6 @@ type context val context: context - (* simplification *) - val simplify: Argo_Rewr.context -> Argo_Rewr.context - (* enriching the context *) val add_atom: Argo_Term.term -> context -> Argo_Lit.literal option * context @@ -467,27 +464,6 @@ end -(* simplification *) - -(* - Only equalities are subject to normalizations. An equality between two expressions e1 and e2 - is normalized, if e1 is less than e2 based on the expression ordering. If e1 and e2 are - syntactically equal, the equality between these two expressions is normalized to the true - expression. -*) - -fun norm_eq env = - let val e1 = Argo_Rewr.get env 1 and e2 = Argo_Rewr.get env 2 - in - (case Argo_Expr.expr_ord (e1, e2) of - EQUAL => SOME (Argo_Proof.Rewr_Eq_Refl, Argo_Rewr.E Argo_Expr.true_expr) - | LESS => NONE - | GREATER => SOME (Argo_Proof.Rewr_Eq_Symm, Argo_Rewr.E (Argo_Expr.mk_eq e2 e1))) - end - -val simplify = Argo_Rewr.func "(eq (? 1) (? 2))" norm_eq - - (* declaring atoms *) (* diff -r 75ee8475c37e -r a5a09855e424 src/Tools/Argo/argo_expr.ML --- a/src/Tools/Argo/argo_expr.ML Fri Jan 20 17:22:54 2017 +0100 +++ b/src/Tools/Argo/argo_expr.ML Fri Jan 20 21:05:11 2017 +0100 @@ -55,6 +55,9 @@ exception EXPR of expr val type_of: expr -> typ (* raises EXPR *) val check: expr -> bool (* raises TYPE and EXPR *) + + (* testers *) + val is_nary: kind -> bool end structure Argo_Expr: ARGO_EXPR = @@ -239,6 +242,11 @@ | raw_check (e as E (Abs, [_])) = all_real e | raw_check e = raise EXPR e + +(* testers *) + +fun is_nary k = member (op =) [And, Or, Add] k + end structure Argo_Exprtab = Table(type key = Argo_Expr.expr val ord = Argo_Expr.expr_ord) diff -r 75ee8475c37e -r a5a09855e424 src/Tools/Argo/argo_proof.ML --- a/src/Tools/Argo/argo_proof.ML Fri Jan 20 17:22:54 2017 +0100 +++ b/src/Tools/Argo/argo_proof.ML Fri Jan 20 21:05:11 2017 +0100 @@ -20,6 +20,7 @@ datatype tautology = Taut_And_1 of int | Taut_And_2 of int * int | Taut_Or_1 of int * int | Taut_Or_2 of int | Taut_Iff_1 | Taut_Iff_2 | Taut_Iff_3 | Taut_Iff_4 | Taut_Ite_Then | Taut_Ite_Else + datatype side = Left | Right datatype inequality = Le | Lt datatype rewrite = Rewr_Not_True | Rewr_Not_False | Rewr_Not_Not | Rewr_Not_And of int | Rewr_Not_Or of int | @@ -32,11 +33,14 @@ Rewr_Eq_Refl | Rewr_Eq_Symm | Rewr_Neg | Rewr_Add of (Rat.rat * int option) list * (Rat.rat * int option) list | Rewr_Sub | Rewr_Mul_Nums of Rat.rat * Rat.rat | Rewr_Mul_Zero | Rewr_Mul_One | Rewr_Mul_Comm | - Rewr_Mul_Assoc | Rewr_Mul_Sum | Rewr_Div_Nums of Rat.rat * Rat.rat | Rewr_Div_Zero | - Rewr_Div_One | Rewr_Div_Mul | Rewr_Div_Inv | Rewr_Div_Left | Rewr_Div_Right | Rewr_Min | - Rewr_Max | Rewr_Abs | Rewr_Eq_Le | Rewr_Ineq_Nums of inequality * bool | - Rewr_Ineq_Add of inequality * Rat.rat | Rewr_Ineq_Sub of inequality | - Rewr_Ineq_Mul of inequality * Rat.rat | Rewr_Not_Ineq of inequality + Rewr_Mul_Assoc of side | Rewr_Mul_Sum of side | Rewr_Mul_Div of side | + Rewr_Div_Zero | Rewr_Div_One | Rewr_Div_Nums of Rat.rat * Rat.rat | + Rewr_Div_Num of side * Rat.rat | Rewr_Div_Mul of side * Rat.rat | Rewr_Div_Div of side | + Rewr_Div_Sum | Rewr_Min_Eq | Rewr_Min_Lt | Rewr_Min_Gt | Rewr_Max_Eq | Rewr_Max_Lt | + Rewr_Max_Gt | Rewr_Abs | Rewr_Eq_Nums of bool | Rewr_Eq_Sub | Rewr_Eq_Le | + Rewr_Ineq_Nums of inequality * bool | Rewr_Ineq_Add of inequality * Rat.rat | + Rewr_Ineq_Sub of inequality | Rewr_Ineq_Mul of inequality * Rat.rat | + Rewr_Not_Ineq of inequality datatype conv = Keep_Conv | Then_Conv of conv * conv | Args_Conv of conv list | Rewr_Conv of rewrite datatype rule = @@ -101,6 +105,8 @@ Taut_And_1 of int | Taut_And_2 of int * int | Taut_Or_1 of int * int | Taut_Or_2 of int | Taut_Iff_1 | Taut_Iff_2 | Taut_Iff_3 | Taut_Iff_4 | Taut_Ite_Then | Taut_Ite_Else +datatype side = Left | Right + datatype inequality = Le | Lt datatype rewrite = @@ -114,11 +120,14 @@ Rewr_Eq_Refl | Rewr_Eq_Symm | Rewr_Neg | Rewr_Add of (Rat.rat * int option) list * (Rat.rat * int option) list | Rewr_Sub | Rewr_Mul_Nums of Rat.rat * Rat.rat | Rewr_Mul_Zero | Rewr_Mul_One | Rewr_Mul_Comm | - Rewr_Mul_Assoc | Rewr_Mul_Sum | Rewr_Div_Nums of Rat.rat * Rat.rat | Rewr_Div_Zero | - Rewr_Div_One | Rewr_Div_Mul | Rewr_Div_Inv | Rewr_Div_Left | Rewr_Div_Right | Rewr_Min | - Rewr_Max | Rewr_Abs | Rewr_Eq_Le | Rewr_Ineq_Nums of inequality * bool | - Rewr_Ineq_Add of inequality * Rat.rat | Rewr_Ineq_Sub of inequality | - Rewr_Ineq_Mul of inequality * Rat.rat | Rewr_Not_Ineq of inequality + Rewr_Mul_Assoc of side | Rewr_Mul_Sum of side | Rewr_Mul_Div of side | + Rewr_Div_Zero | Rewr_Div_One | Rewr_Div_Nums of Rat.rat * Rat.rat | + Rewr_Div_Num of side * Rat.rat | Rewr_Div_Mul of side * Rat.rat | Rewr_Div_Div of side | + Rewr_Div_Sum | Rewr_Min_Eq | Rewr_Min_Lt | Rewr_Min_Gt | Rewr_Max_Eq | Rewr_Max_Lt | + Rewr_Max_Gt | Rewr_Abs | Rewr_Eq_Nums of bool | Rewr_Eq_Sub | Rewr_Eq_Le | + Rewr_Ineq_Nums of inequality * bool | Rewr_Ineq_Add of inequality * Rat.rat | + Rewr_Ineq_Sub of inequality | Rewr_Ineq_Mul of inequality * Rat.rat | + Rewr_Not_Ineq of inequality datatype conv = Keep_Conv | Then_Conv of conv * conv | Args_Conv of conv list | Rewr_Conv of rewrite @@ -326,19 +335,37 @@ | string_of_rewr Rewr_Mul_Zero = "0 * e = 0" | string_of_rewr Rewr_Mul_One = "1 * e = e" | string_of_rewr Rewr_Mul_Comm = "e1 * e2 = e2 * e1" - | string_of_rewr Rewr_Mul_Assoc = "n1 * (n2 * e) = (n1 * n2) * e" - | string_of_rewr Rewr_Mul_Sum = "n * (e1 + ... + em) = n * e1 + ... n * em" - | string_of_rewr (Rewr_Div_Nums (n1, n2)) = - Rat.string_of_rat n1 ^ " / " ^ Rat.string_of_rat n2 ^ " = " ^ Rat.string_of_rat (n1 / n2) + | string_of_rewr (Rewr_Mul_Assoc Left) = "(e1 * e2) * e3 = e1 * (e2 * e3)" + | string_of_rewr (Rewr_Mul_Assoc Right) = "e1 * (n * e2) = (e1 * n) * e2" + | string_of_rewr (Rewr_Mul_Sum Left) = "(e1 + ... + em) * e = e1 * e + ... em * e" + | string_of_rewr (Rewr_Mul_Sum Right) = "e * (e1 + ... + em) = e * e1 + ... e * em" + | string_of_rewr (Rewr_Mul_Div Left) = "(e1 / e2) * e3 = (e1 * e3) / e2" + | string_of_rewr (Rewr_Mul_Div Right) = "e1 * (e2 / * e3) = (e1 * e2) / e3" | string_of_rewr Rewr_Div_Zero = "0 / e = 0" | string_of_rewr Rewr_Div_One = "e / 1 = e" - | string_of_rewr Rewr_Div_Mul = "n / e = n * (1 / e)" - | string_of_rewr Rewr_Div_Inv = "e / n = 1/n * e" - | string_of_rewr Rewr_Div_Left = "(n * e1) / e2 = n * (e1 / e2)" - | string_of_rewr Rewr_Div_Right = "e1 / (n * e2) = 1/n * (e1 / e2)" - | string_of_rewr Rewr_Min = "min e1 e2 = (if e1 <= e2 then e1 else e2)" - | string_of_rewr Rewr_Max = "max e1 e2 = (if e1 < e2 then e2 else e1)" + | string_of_rewr (Rewr_Div_Nums (n1, n2)) = + Rat.string_of_rat n1 ^ " / " ^ Rat.string_of_rat n2 ^ " = " ^ Rat.string_of_rat (n1 / n2) + | string_of_rewr (Rewr_Div_Num (Left, n)) = + Rat.string_of_rat n ^ " / e = " ^ Rat.string_of_rat n ^ " * (1 / e)" + | string_of_rewr (Rewr_Div_Num (Right, n)) = + "e / " ^ Rat.string_of_rat n ^ " = " ^ Rat.string_of_rat (Rat.inv n) ^ " * e" + | string_of_rewr (Rewr_Div_Mul (Left, n)) = + "(" ^ Rat.string_of_rat n ^ " * e1) / e2 = " ^ Rat.string_of_rat n ^ " * (e1 / e2)" + | string_of_rewr (Rewr_Div_Mul (Right, n)) = + "e1 / (" ^ Rat.string_of_rat n ^ " * e2) = " ^ Rat.string_of_rat (Rat.inv n) ^ " * (e1 / e2)" + | string_of_rewr (Rewr_Div_Div Left) = "(e1 / e2) / e3 = e1 / (e2 * e3)" + | string_of_rewr (Rewr_Div_Div Right) = "e1 / (e2 / e3) = (e1 * e3) / e2" + | string_of_rewr Rewr_Div_Sum = "(e1 + ... + em) / e = e1 / e + ... + em / e" + | string_of_rewr Rewr_Min_Eq = "min e e = e" + | string_of_rewr Rewr_Min_Lt = "min e1 e2 = (if e1 <= e2 then e1 else e2)" + | string_of_rewr Rewr_Min_Gt = "min e1 e2 = (if e2 <= e1 then e2 else e1)" + | string_of_rewr Rewr_Max_Eq = "max e e = e" + | string_of_rewr Rewr_Max_Lt = "max e1 e2 = (if e1 < e2 then e2 else e1)" + | string_of_rewr Rewr_Max_Gt = "max e1 e2 = (if e2 < e1 then e1 else e2)" | string_of_rewr Rewr_Abs = "abs e = (if 0 <= e then e else -e)" + | string_of_rewr (Rewr_Eq_Nums true) = "(n1 = n2) = true" + | string_of_rewr (Rewr_Eq_Nums false) = "(n1 ~= n2) = false" + | string_of_rewr Rewr_Eq_Sub = "(e1 = e2) = (e1 - e2 = 0)" | string_of_rewr Rewr_Eq_Le = "(e1 = e2) = (and (e1 <= e2) (e2 <= e1))" | string_of_rewr (Rewr_Ineq_Nums (Le, true)) = "(n1 <= n2) = true" | string_of_rewr (Rewr_Ineq_Nums (Le, false)) = "(n1 <= n2) = false" diff -r 75ee8475c37e -r a5a09855e424 src/Tools/Argo/argo_rewr.ML --- a/src/Tools/Argo/argo_rewr.ML Fri Jan 20 17:22:54 2017 +0100 +++ b/src/Tools/Argo/argo_rewr.ML Fri Jan 20 21:05:11 2017 +0100 @@ -6,23 +6,6 @@ signature ARGO_REWR = sig - (* patterns *) - datatype pattern = - V of int | - E of Argo_Expr.expr | - A of Argo_Expr.kind | - P of Argo_Expr.kind * pattern list | - M of pattern | - X - - (* scanning patterns from strings *) - val scan: string -> pattern - - (* pattern matching *) - type env - val get_all: env -> Argo_Expr.expr list - val get: env -> int -> Argo_Expr.expr - (* conversions *) type conv = Argo_Expr.expr -> Argo_Expr.expr * Argo_Proof.conv val keep: conv @@ -33,132 +16,31 @@ (* context *) type context val context: context - val flat: string -> - (int -> Argo_Expr.expr list -> (Argo_Proof.rewrite * Argo_Expr.expr) option) -> - context -> context - val func: string -> (env -> (Argo_Proof.rewrite * pattern) option) -> context -> context - val rule: Argo_Proof.rewrite -> string -> string -> context -> context (* rewriting *) val rewrite: context -> conv val rewrite_top: context -> conv val with_proof: conv -> Argo_Expr.expr * Argo_Proof.proof -> Argo_Proof.context -> (Argo_Expr.expr * Argo_Proof.proof) * Argo_Proof.context + + (* normalizations *) + val nnf: context -> context + val norm_prop: context -> context + val norm_ite: context -> context + val norm_eq: context -> context + val norm_add: context -> context + val norm_mul: context -> context + val norm_arith: context -> context end structure Argo_Rewr: ARGO_REWR = struct -(* patterns *) - -(* - Patterns are used for matching against expressions and as a schema to construct - expressions. For matching, only V, E, A and P must be used. For the schema, - additionally M and X can be used. -*) - -datatype pattern = - V of int | (* indexed placeholder where the index must be greater than 0 *) - E of Argo_Expr.expr | (* expression without placeholders *) - A of Argo_Expr.kind | (* placeholder for the arguments of an n-ary expression *) - P of Argo_Expr.kind * pattern list | (* expression with optional placeholders *) - M of pattern | (* mapping operator to iterate over an argument list of an n-ary expression *) - X (* closure argument under a mapping operator representing an expression *) - -fun int_of_pattern (E _) = 0 - | int_of_pattern (P _) = 1 - | int_of_pattern (A _) = 2 - | int_of_pattern (V _) = 3 - | int_of_pattern _ = raise Fail "bad pattern" - -(* - Specific patterns are ordered before generic patterns, since pattern matching - performs a linear search for the most suitable pattern. -*) - -fun pattern_ord (E e1, E e2) = Argo_Expr.expr_ord (e1, e2) - | pattern_ord (P (k1, ps1), P (k2, ps2)) = - (case Argo_Expr.kind_ord (k1, k2) of EQUAL => list_ord pattern_ord (ps1, ps2) | x => x) - | pattern_ord (A k1, A k2) = Argo_Expr.kind_ord (k1, k2) - | pattern_ord (V i1, V i2) = int_ord (i1, i2) - | pattern_ord (p1, p2) = int_ord (int_of_pattern p1, int_of_pattern p2) - - -(* scanning patterns from strings *) - -(* - The pattern language is cumbersome to use in other structures. Strings are a more - lightweight representation. Scanning patterns from strings should be performed at - compile time to avoid the parsing overhead at runtime. -*) - -val kind = Scan.many1 Symbol.is_ascii_letter >> (Argo_Expr.kind_of_string o implode) -val num = Scan.many1 Symbol.is_ascii_digit >> (the o Int.fromString o implode) -val integer = $$ "-" |-- num >> ~ || num -val blank = Scan.many1 Symbol.is_ascii_blank >> K () - -fun pattern xs = ( - kind >> (P o rpair []) || - $$ "!" >> K X || - $$ "(" -- $$ "#" -- blank |-- pattern --| $$ ")" >> M || - $$ "(" -- $$ "?" -- blank |-- num --| $$ ")" >> V || - $$ "(" -- Scan.this_string "num" -- blank |-- integer --| $$ ")" >> - (E o Argo_Expr.mk_num o Rat.of_int) || - $$ "(" |-- kind --| blank --| $$ "_" --| $$ ")" >> A || - $$ "(" |-- kind -- Scan.repeat1 (blank |-- pattern) --| $$ ")" >> P) xs - -fun scan s = fst (pattern (map str (String.explode s) @ [""])) - - -(* pattern matching *) - -exception PATTERN of unit - -(* - The environment stores the matched expressions for the pattern placeholders. - The expression for an indexed placeholder (V i) can be retrieved by "get env i". - The argument expressions for an n-ary placeholder (A k) can be retrieved by "get_all env". -*) - -type env = Argo_Expr.expr list Inttab.table - -val empty_env: env = Inttab.empty -fun get_all env = Inttab.lookup_list env 0 -fun get env i = hd (Inttab.lookup_list env i) - -fun depth_of (V _) = 0 - | depth_of (E _) = 0 - | depth_of (A _) = 1 - | depth_of (P (_, ps)) = 1 + fold (Integer.max o depth_of) ps 0 - | depth_of (M p) = depth_of p - | depth_of X = 0 - -fun match_list f k k' env = if k = k' then f env else raise PATTERN () - -fun match (V i) e env = Inttab.update_new (i, [e]) env - | match (A k) (Argo_Expr.E (k', es)) env = match_list (Inttab.update_new (0, es)) k k' env - | match (P (k, ps)) (Argo_Expr.E (k', es)) env = match_list (fold2 match ps es) k k' env - | match _ _ _ = raise Fail "bad pattern" - -fun unfold_index env (V i) _ = get env i - | unfold_index _ (E e) _ = e - | unfold_index env (P (k, ps)) e = Argo_Expr.E (k, map (fn p => unfold_index env p e) ps) - | unfold_index _ X e = e - | unfold_index _ _ _ = raise Fail "bad pattern" - -fun unfold_pattern env (V i) = get env i - | unfold_pattern _ (E e) = e - | unfold_pattern env (A k) = Argo_Expr.E (k, get_all env) - | unfold_pattern env (P (k, [M p])) = Argo_Expr.E (k, map (unfold_index env p) (get_all env)) - | unfold_pattern env (P (k, ps)) = Argo_Expr.E (k, map (unfold_pattern env) ps) - | unfold_pattern _ _ = raise Fail "bad pattern" - - (* conversions *) (* - Conversions are atomic rewrite steps. For every conversion there is a corresponding - inference step. + Conversions are atomic rewrite steps. + For every conversion there is a corresponding inference step. *) type conv = Argo_Expr.expr -> Argo_Expr.expr * Argo_Proof.conv @@ -171,91 +53,93 @@ let val ((e, c2), c1) = cv e |>> seq cvs in (e, Argo_Proof.mk_then_conv c1 c2) end -fun args cv (Argo_Expr.E (k, es)) = - let val (es, cs) = split_list (map cv es) +fun on_args f (Argo_Expr.E (k, es)) = + let val (es, cs) = split_list (f es) in (Argo_Expr.E (k, es), Argo_Proof.mk_args_conv cs) end +fun args cv e = on_args (map cv) e + +fun all_args cv k (e as Argo_Expr.E (k', _)) = if k = k' then args (all_args cv k) e else cv e + fun rewr r e _ = (e, Argo_Proof.mk_rewr_conv r) +(* rewriting result *) + +(* + After rewriting an expression, further rewritings might be applicable. The result type is + a simple means to control which parts of the rewriting result should be rewritten further. + Only the top-most part of a result marked by R constructors is amenable to further rewritings. +*) + +datatype result = + E of Argo_Expr.expr | + R of Argo_Expr.kind * result list + +fun expr_of (E e) = e + | expr_of (R (k, ps)) = Argo_Expr.E (k, map expr_of ps) + +fun top_most _ (E _) e = keep e + | top_most cv (R (_, ps)) e = seq [on_args (map2 (top_most cv) ps), cv] e + + (* context *) (* - The context stores functions to flatten expressions and functions to rewrite expressions. - Flattening an n-ary expression of kind k produces an expression whose arguments are not - of kind k. For instance, flattening (and p (and q r)) produces (and p q r) where p, q and r - are not conjunctions. + The context stores lists of rewritings for every expression kind. A rewriting maps the + arguments of an expression with matching kind to an optional rewriting result. Each + rewriting might decide whether it is applicable to the given expression arguments and + might return no result. The first rewriting that produces a result is applied. *) -structure Pattab = Table(type key = pattern val ord = pattern_ord) +structure Kindtab = Table(type key = Argo_Expr.kind val ord = Argo_Expr.kind_ord) -type context = { - flats: - (Argo_Expr.kind * (int -> Argo_Expr.expr list -> (Argo_Proof.rewrite * Argo_Expr.expr) option)) - list, (* expressions that should be flattened before rewriting *) - rewrs: (env -> (Argo_Proof.rewrite * pattern) option) list Pattab.table} - (* Looking up matching rules is O(n). This could be optimized. *) +type context = + (int -> Argo_Expr.expr list -> (Argo_Proof.rewrite * result) option) list Kindtab.table + +val context: context = Kindtab.empty -fun mk_context flats rewrs: context = {flats=flats, rewrs=rewrs} -val context = mk_context [] Pattab.empty - -fun map_context map_flats map_rewrs ({flats, rewrs}: context) = - mk_context (map_flats flats) (map_rewrs rewrs) +fun add_func k f = Kindtab.map_default (k, []) (fn fs => fs @ [f]) +fun add_func' k f = add_func k (fn _ => f) -fun flat lhs f = - (case scan lhs of - A k => map_context (cons (k, f)) I - | _ => raise Fail "bad pattern") - -fun func lhs f = map_context I (Pattab.map_default (scan lhs, []) (fn fs => fs @ [f])) -fun rule r lhs rhs = func lhs (K (SOME (r, scan rhs))) +fun unary k f = add_func' k (fn [e] => f e | _ => raise Fail "not unary") +fun binary k f = add_func' k (fn [e1, e2] => f e1 e2 | _ => raise Fail "not binary") +fun ternary k f = add_func' k (fn [e1, e2, e3] => f e1 e2 e3 | _ => raise Fail "not ternary") +fun nary k f = add_func k f (* rewriting *) (* - Rewriting proceeds bottom-up. Whenever a rewrite rule with placeholders is used, - the arguments are again rewritten, but only up to depth of the placeholders within the - matched pattern. + Rewriting proceeds bottom-up. The top-most result of a rewriting step is rewritten again + bottom-up, if necessary. Only the first rewriting that produces a result for a given + expression is applied. N-ary expressions are flattened before they are rewritten. For + instance, flattening (and p (and q r)) produces (and p q r) where p, q and r are no + conjunctions. *) -fun rewr_rule r env p = rewr r (unfold_pattern env p) +fun first_rewr cv cx k n es e = + (case get_first (fn f => f n es) (Kindtab.lookup_list cx k) of + NONE => keep e + | SOME (r, res) => seq [rewr r (expr_of res), top_most cv res] e) -fun try_apply p e f = - let val env = match p e empty_env - in (case f env of NONE => NONE | SOME (r, p) => SOME (r, env, p)) end - handle PATTERN () => NONE - -fun all_args cv k (e as Argo_Expr.E (k', _)) = if k = k' then args (all_args cv k) e else cv e fun all_args_of k (e as Argo_Expr.E (k', es)) = if k = k' then maps (all_args_of k) es else [e] fun kind_depth_of k (Argo_Expr.E (k', es)) = if k = k' then 1 + fold (Integer.max o kind_depth_of k) es 0 else 0 -fun descend cv flats (e as Argo_Expr.E (k, _)) = - if AList.defined Argo_Expr.eq_kind flats k then all_args cv k e - else args cv e +fun norm_kind cv cx (e as Argo_Expr.E (k, es)) = + let val (n, es) = if Argo_Expr.is_nary k then (kind_depth_of k e, all_args_of k e) else (1, es) + in first_rewr cv cx k n es e end -fun flatten flats (e as Argo_Expr.E (k, _)) = - (case AList.lookup Argo_Expr.eq_kind flats k of - NONE => keep e - | SOME f => - (case f (kind_depth_of k e) (all_args_of k e) of - NONE => keep e - | SOME (r, e') => rewr r e' e)) +fun norm_args cv d (e as Argo_Expr.E (k, _)) = + if d = 0 then keep e + else if Argo_Expr.is_nary k then all_args (cv (d - 1)) k e + else args (cv (d - 1)) e -fun exhaust cv rewrs e = - (case Pattab.get_first (fn (p, fs) => get_first (try_apply p e) fs) rewrs of - NONE => keep e - | SOME (r, env, p) => seq [rewr_rule r env p, cv (depth_of p)] e) - -fun norm (cx as {flats, rewrs}: context) d e = - seq [ - if d = 0 then keep else descend (norm cx (d - 1)) flats, - flatten flats, - exhaust (norm cx) rewrs] e +fun norm cx d e = seq [norm_args (norm cx) d, norm_kind (norm cx 0) cx] e fun rewrite cx = norm cx ~1 (* bottom-up rewriting *) -fun rewrite_top cx = norm cx 0 (* top-down rewriting *) +fun rewrite_top cx = norm cx 0 (* top-most rewriting *) fun with_proof cv (e, p) prf = let @@ -263,4 +147,395 @@ val (p, prf) = Argo_Proof.mk_rewrite c p prf in ((e, p), prf) end + +(* result constructors *) + +fun mk_nary _ e [] = e + | mk_nary _ _ [e] = e + | mk_nary k _ es = R (k, es) + +val e_true = E Argo_Expr.true_expr +val e_false = E Argo_Expr.false_expr +fun mk_not e = R (Argo_Expr.Not, [e]) +fun mk_and es = mk_nary Argo_Expr.And e_true es +fun mk_or es = mk_nary Argo_Expr.Or e_false es +fun mk_iff e1 e2 = R (Argo_Expr.Iff, [e1, e2]) +fun mk_ite e1 e2 e3 = R (Argo_Expr.Ite, [e1, e2, e3]) +fun mk_num n = E (Argo_Expr.mk_num n) +fun mk_neg e = R (Argo_Expr.Neg, [e]) +fun mk_add [] = raise Fail "bad addition" + | mk_add [e] = e + | mk_add es = R (Argo_Expr.Add, es) +fun mk_sub e1 e2 = R (Argo_Expr.Sub, [e1, e2]) +fun mk_mul e1 e2 = R (Argo_Expr.Mul, [e1, e2]) +fun mk_div e1 e2 = R (Argo_Expr.Div, [e1, e2]) +fun mk_le e1 e2 = R (Argo_Expr.Le, [e1, e2]) +fun mk_le' e1 e2 = mk_le (E e1) (E e2) +fun mk_eq e1 e2 = R (Argo_Expr.Eq, [e1, e2]) + + +(* rewriting to negation normal form *) + +fun rewr_not (Argo_Expr.E exp) = + (case exp of + (Argo_Expr.True, _) => SOME (Argo_Proof.Rewr_Not_True, e_false) + | (Argo_Expr.False, _) => SOME (Argo_Proof.Rewr_Not_False, e_true) + | (Argo_Expr.Not, [e]) => SOME (Argo_Proof.Rewr_Not_Not, E e) + | (Argo_Expr.And, es) => SOME (Argo_Proof.Rewr_Not_And (length es), mk_or (map (mk_not o E) es)) + | (Argo_Expr.Or, es) => SOME (Argo_Proof.Rewr_Not_Or (length es), mk_and (map (mk_not o E) es)) + | (Argo_Expr.Iff, [Argo_Expr.E (Argo_Expr.Not, [e1]), e2]) => + SOME (Argo_Proof.Rewr_Not_Iff, mk_iff (E e1) (E e2)) + | (Argo_Expr.Iff, [e1, Argo_Expr.E (Argo_Expr.Not, [e2])]) => + SOME (Argo_Proof.Rewr_Not_Iff, mk_iff (E e1) (E e2)) + | (Argo_Expr.Iff, [e1, e2]) => + SOME (Argo_Proof.Rewr_Not_Iff, mk_iff (mk_not (E e1)) (E e2)) + | _ => NONE) + +val nnf = unary Argo_Expr.Not rewr_not + + +(* propositional normalization *) + +(* + Propositional expressions are transformed into literals in the clausifier. Having + fewer literals results in faster solver execution. Normalizing propositional expressions + turns similar expressions into equal expressions, for which the same literal can be used. + The clausifier expects that only negation, disjunction, conjunction and equivalence form + propositional expressions. Expressions may be simplified to truth or falsity, but both + truth and falsity eventually occur nowhere inside expressions. +*) + +fun first_index pred xs = + let val i = find_index pred xs + in if i >= 0 then SOME i else NONE end + +fun rewr_zero r zero _ es = + Option.map (fn i => (r i, E zero)) (first_index (curry Argo_Expr.eq_expr zero) es) + +fun rewr_dual r zero _ = + let + fun duals _ [] = NONE + | duals _ [_] = NONE + | duals i (e :: es) = + (case first_index (Argo_Expr.dual_expr e) es of + NONE => duals (i + 1) es + | SOME i' => SOME (r (i, i + i' + 1), zero)) + in duals 0 end + +fun rewr_sort r one mk n es = + let + val l = length es + fun add (i, e) = if Argo_Expr.eq_expr (e, one) then I else Argo_Exprtab.cons_list (e, i) + fun dest (e, i) (es, is) = (e :: es, i :: is) + val (es, iss) = Argo_Exprtab.fold_rev dest (fold_index add es Argo_Exprtab.empty) ([], []) + fun identity is = length is = l andalso forall (op =) (map_index I is) + in + if null iss then SOME (r (l, [[0]]), E one) + else if n = 1 andalso identity (map hd iss) then NONE + else (SOME (r (l, iss), mk (map E es))) + end + +fun rewr_imp e1 e2 = SOME (Argo_Proof.Rewr_Imp, mk_or [mk_not (E e1), E e2]) + +fun rewr_iff (e1 as Argo_Expr.E exp1) (e2 as Argo_Expr.E exp2) = + (case (exp1, exp2) of + ((Argo_Expr.True, _), _) => SOME (Argo_Proof.Rewr_Iff_True, E e2) + | ((Argo_Expr.False, _), _) => SOME (Argo_Proof.Rewr_Iff_False, mk_not (E e2)) + | (_, (Argo_Expr.True, _)) => SOME (Argo_Proof.Rewr_Iff_True, E e1) + | (_, (Argo_Expr.False, _)) => SOME (Argo_Proof.Rewr_Iff_False, mk_not (E e1)) + | ((Argo_Expr.Not, [e1']), (Argo_Expr.Not, [e2'])) => + SOME (Argo_Proof.Rewr_Iff_Not_Not, mk_iff (E e1') (E e2')) + | _ => + if Argo_Expr.dual_expr e1 e2 then SOME (Argo_Proof.Rewr_Iff_Dual, e_false) + else + (case Argo_Expr.expr_ord (e1, e2) of + EQUAL => SOME (Argo_Proof.Rewr_Iff_Refl, e_true) + | GREATER => SOME (Argo_Proof.Rewr_Iff_Symm, mk_iff (E e2) (E e1)) + | LESS => NONE)) + +val norm_prop = + nary Argo_Expr.And (rewr_zero Argo_Proof.Rewr_And_False Argo_Expr.false_expr) #> + nary Argo_Expr.And (rewr_dual Argo_Proof.Rewr_And_Dual e_false) #> + nary Argo_Expr.And (rewr_sort Argo_Proof.Rewr_And_Sort Argo_Expr.true_expr mk_and) #> + nary Argo_Expr.Or (rewr_zero Argo_Proof.Rewr_Or_True Argo_Expr.true_expr) #> + nary Argo_Expr.Or (rewr_dual Argo_Proof.Rewr_Or_Dual e_true) #> + nary Argo_Expr.Or (rewr_sort Argo_Proof.Rewr_Or_Sort Argo_Expr.false_expr mk_or) #> + binary Argo_Expr.Imp rewr_imp #> + binary Argo_Expr.Iff rewr_iff + + +(* normalization of if-then-else expressions *) + +fun rewr_ite (Argo_Expr.E (Argo_Expr.True, _)) e _ = SOME (Argo_Proof.Rewr_Ite_True, E e) + | rewr_ite (Argo_Expr.E (Argo_Expr.False, _)) _ e = SOME (Argo_Proof.Rewr_Ite_False, E e) + | rewr_ite e1 e2 e3 = + if Argo_Expr.type_of e2 = Argo_Expr.Bool then + SOME (Argo_Proof.Rewr_Ite_Prop, + mk_and (map mk_or [[mk_not (E e1), E e2], [E e1, E e3], [E e2, E e3]])) + else if Argo_Expr.eq_expr (e2, e3) then SOME (Argo_Proof.Rewr_Ite_Eq, E e2) + else NONE + +val norm_ite = ternary Argo_Expr.Ite rewr_ite + + +(* normalization of equality *) + +(* + In a normalized equality, the left-hand side is less than the right-hand side with respect to + the expression order. +*) + +fun rewr_eq e1 e2 = + (case Argo_Expr.expr_ord (e1, e2) of + EQUAL => SOME (Argo_Proof.Rewr_Eq_Refl, e_true) + | GREATER => SOME (Argo_Proof.Rewr_Eq_Symm, mk_eq (E e2) (E e1)) + | LESS => NONE) + +val norm_eq = binary Argo_Expr.Eq rewr_eq + + +(* arithmetic normalization *) + +(* expression functions *) + +fun scale n e = + if n = @0 then mk_num @0 + else if n = @1 then e + else mk_mul (mk_num n) e + +fun dest_factor (Argo_Expr.E (Argo_Expr.Mul, [Argo_Expr.E (Argo_Expr.Num n, _), _])) = n + | dest_factor _ = @1 + + +(* + Products are normalized either to a number or to the monomial form + a * x + where a is a non-zero number and is a variable or a product of variables. + If x is a product, it contains no number factors. If x is a product, it is sorted + based on the expression order. Hence, the product z * y * x will be rewritten + to x * y * z. The coefficient a is dropped if it is equal to one; + instead of 1 * x the expression x is used. +*) + +fun mk_mul_comm e1 e2 = (Argo_Proof.Rewr_Mul_Comm, mk_mul (E e2) (E e1)) +fun mk_mul_assocr e1 e2 e3 = + (Argo_Proof.Rewr_Mul_Assoc Argo_Proof.Right, mk_mul (mk_mul (E e1) (E e2)) (E e3)) + + (* commute numbers to the left *) +fun rewr_mul (Argo_Expr.E (Argo_Expr.Num n1, _)) (Argo_Expr.E (Argo_Expr.Num n2, _)) = + SOME (Argo_Proof.Rewr_Mul_Nums (n1, n2), mk_num (n1 * n2)) + | rewr_mul e1 (e2 as Argo_Expr.E (Argo_Expr.Num _, _)) = SOME (mk_mul_comm e1 e2) + | rewr_mul e1 (Argo_Expr.E (Argo_Expr.Mul, [e2 as Argo_Expr.E (Argo_Expr.Num _, _), e3])) = + SOME (mk_mul_assocr e1 e2 e3) + (* apply distributivity *) + | rewr_mul (Argo_Expr.E (Argo_Expr.Add, es)) e = + SOME (Argo_Proof.Rewr_Mul_Sum Argo_Proof.Left, mk_add (map (fn e' => mk_mul (E e') (E e)) es)) + | rewr_mul e (Argo_Expr.E (Argo_Expr.Add, es)) = + SOME (Argo_Proof.Rewr_Mul_Sum Argo_Proof.Right, mk_add (map (mk_mul (E e) o E) es)) + (* commute non-numerical factors to the right *) + | rewr_mul (Argo_Expr.E (Argo_Expr.Mul, [e1, e2])) e3 = + SOME (Argo_Proof.Rewr_Mul_Assoc Argo_Proof.Left, mk_mul (E e1) (mk_mul (E e2) (E e3))) + (* reduce special products *) + | rewr_mul (e1 as Argo_Expr.E (Argo_Expr.Num n, _)) e2 = + if n = @0 then SOME (Argo_Proof.Rewr_Mul_Zero, E e1) + else if n = @1 then SOME (Argo_Proof.Rewr_Mul_One, E e2) + else NONE + (* combine products with quotients *) + | rewr_mul (Argo_Expr.E (Argo_Expr.Div, [e1, e2])) e3 = + SOME (Argo_Proof.Rewr_Mul_Div Argo_Proof.Left, mk_div (mk_mul (E e1) (E e3)) (E e2)) + | rewr_mul e1 (Argo_Expr.E (Argo_Expr.Div, [e2, e3])) = + SOME (Argo_Proof.Rewr_Mul_Div Argo_Proof.Right, mk_div (mk_mul (E e1) (E e2)) (E e3)) + (* sort non-numerical factors *) + | rewr_mul e1 (Argo_Expr.E (Argo_Expr.Mul, [e2, e3])) = + (case Argo_Expr.expr_ord (e1, e2) of + GREATER => SOME (mk_mul_assocr e1 e2 e3) + | _ => NONE) + | rewr_mul e1 e2 = + (case Argo_Expr.expr_ord (e1, e2) of + GREATER => SOME (mk_mul_comm e1 e2) + | _ => NONE) + +(* + Quotients are normalized either to a number or to the monomial form + a * x + where a is a non-zero number and x is a variable. If x is a quotient, + both dividend and divisor are not a number. The dividend and the divisor may both + be products. If so, neither dividend nor divisor contains a numerical factor. + Both dividend and divisor are not themselves quotients again. The dividend is never + a sum; distributivity is applied to such quotients. The coefficient a is dropped + if it is equal to one; instead of 1 * x the expression x is used. + + Several non-linear expressions can be rewritten to the described normal form. + For example, the expressions (x * z) / y and x * (z / y) will be treated as equal + variables by the arithmetic decision procedure. Yet, non-linear expression rewriting + is incomplete and keeps several other expressions unchanged. +*) + +fun rewr_div (Argo_Expr.E (Argo_Expr.Div, [e1, e2])) e3 = + SOME (Argo_Proof.Rewr_Div_Div Argo_Proof.Left, mk_div (E e1) (mk_mul (E e2) (E e3))) + | rewr_div e1 (Argo_Expr.E (Argo_Expr.Div, [e2, e3])) = + SOME (Argo_Proof.Rewr_Div_Div Argo_Proof.Right, mk_div (mk_mul (E e1) (E e3)) (E e2)) + | rewr_div (Argo_Expr.E (Argo_Expr.Num n1, _)) (Argo_Expr.E (Argo_Expr.Num n2, _)) = + if n2 = @0 then NONE + else SOME (Argo_Proof.Rewr_Div_Nums (n1, n2), mk_num (n1 / n2)) + | rewr_div (Argo_Expr.E (Argo_Expr.Num n, _)) e = + if n = @0 then SOME (Argo_Proof.Rewr_Div_Zero, mk_num @0) + else if n = @1 then NONE + else SOME (Argo_Proof.Rewr_Div_Num (Argo_Proof.Left, n), scale n (mk_div (mk_num @1) (E e))) + | rewr_div (Argo_Expr.E (Argo_Expr.Mul, [Argo_Expr.E (Argo_Expr.Num n, _), e1])) e2 = + SOME (Argo_Proof.Rewr_Div_Mul (Argo_Proof.Left, n), scale n (mk_div (E e1) (E e2))) + | rewr_div e (Argo_Expr.E (Argo_Expr.Num n, _)) = + if n = @0 then NONE + else if n = @1 then SOME (Argo_Proof.Rewr_Div_One, E e) + else SOME (Argo_Proof.Rewr_Div_Num (Argo_Proof.Right, n), scale (Rat.inv n) (E e)) + | rewr_div e1 (Argo_Expr.E (Argo_Expr.Mul, [Argo_Expr.E (Argo_Expr.Num n, _), e2])) = + SOME (Argo_Proof.Rewr_Div_Mul (Argo_Proof.Right, n), scale (Rat.inv n) (mk_div (E e1) (E e2))) + | rewr_div (Argo_Expr.E (Argo_Expr.Add, es)) e = + SOME (Argo_Proof.Rewr_Div_Sum, mk_add (map (fn e' => mk_div (E e') (E e)) es)) + | rewr_div _ _ = NONE + + +(* + Sums are flattened and normalized to the polynomial form + a_0 + a_1 * x_1 + ... + a_n * x_n + where all variables x_i are disjoint and where all coefficients a_i are + non-zero numbers. Coefficients equal to one are dropped; instead of 1 * x_i + the reduced monom x_i is used. The variables x_i are ordered based on the + expression order to reduce the number of problem literals by sharing equal + expressions. +*) + +fun add_monom_expr i n e (p, s, etab) = + let val etab = Argo_Exprtab.map_default (e, (i, @0)) (apsnd (Rat.add n)) etab + in ((n, Option.map fst (Argo_Exprtab.lookup etab e)) :: p, s, etab) end + +fun add_monom (_, Argo_Expr.E (Argo_Expr.Num n, _)) (p, s, etab) = ((n, NONE) :: p, s + n, etab) + | add_monom (i, Argo_Expr.E (Argo_Expr.Mul, [Argo_Expr.E (Argo_Expr.Num n, _), e])) x = + add_monom_expr i n e x + | add_monom (i, e) x = add_monom_expr i @1 e x + +fun rewr_add d es = + let + val (p1, s, etab) = fold_index add_monom es ([], @0, Argo_Exprtab.empty) + val (p2, es) = + [] + |> Argo_Exprtab.fold_rev (fn (e, (i, n)) => n <> @0 ? cons ((n, SOME i), scale n (E e))) etab + |> s <> @0 ? cons ((s, NONE), mk_num s) + |> (fn [] => [((@0, NONE), mk_num @0)] | xs => xs) + |> split_list + val ps = (rev p1, p2) + in + if d = 1 andalso eq_list (op =) ps then NONE + else SOME (Argo_Proof.Rewr_Add ps, mk_add es) + end + + +(* + Equations are normalized to the normal form + a_0 + a_1 * x_1 + ... + a_n * x_n = b + or + b = a_0 + a_1 * x_1 + ... + a_n * x_n + An equation in normal form is rewritten to a conjunction of two non-strict inequalities. +*) + +fun rewr_eq_le e1 e2 = SOME (Argo_Proof.Rewr_Eq_Le, mk_and [mk_le' e1 e2, mk_le' e2 e1]) + +fun rewr_arith_eq (Argo_Expr.E (Argo_Expr.Num n1, _)) (Argo_Expr.E (Argo_Expr.Num n2, _)) = + let val b = (n1 = n2) + in SOME (Argo_Proof.Rewr_Eq_Nums b, if b then e_true else e_false) end + | rewr_arith_eq (e1 as Argo_Expr.E (Argo_Expr.Num _, _)) e2 = rewr_eq_le e1 e2 + | rewr_arith_eq e1 (e2 as Argo_Expr.E (Argo_Expr.Num _, _)) = rewr_eq_le e1 e2 + | rewr_arith_eq e1 e2 = SOME (Argo_Proof.Rewr_Eq_Sub, mk_eq (mk_sub (E e1) (E e2)) (mk_num @0)) + +fun is_arith e = member (op =) [Argo_Expr.Real] (Argo_Expr.type_of e) + +fun rewr_eq e1 e2 = if is_arith e1 then rewr_arith_eq e1 e2 else NONE + + +(* + Arithmetic inequalities (less and less-than) are normalized to the normal form + a_0 + a_1 * x_1 + ... + a_n * x_n ~ b + or + b ~ a_0 + a_1 * x_1 + ... + a_n * x_n + such that most of the coefficients a_i are positive. + + Arithmetic inequalities of the form + a * x ~ b + or + b ~ a * x + are normalized to the form + x ~ c + or + c ~ x + where c is a number. +*) + +fun norm_cmp_mul k r f e1 e2 n = + let val es = if n > @0 then [e1, e2] else [e2, e1] + in SOME (Argo_Proof.Rewr_Ineq_Mul (r, n), R (k, f (map (scale n o E) es))) end + +fun count_factors pred es = fold (fn e => if pred (dest_factor e) then Integer.add 1 else I) es 0 + +fun norm_cmp_swap k r f e1 e2 es = + let + val pos = count_factors (fn n => n > @0) es + val neg = count_factors (fn n => n < @0) es + val keep = pos > neg orelse (pos = neg andalso dest_factor (hd es) > @0) + in if keep then NONE else norm_cmp_mul k r f e1 e2 @~1 end + +fun norm_cmp1 k r f e1 (e2 as Argo_Expr.E (Argo_Expr.Mul, [Argo_Expr.E (Argo_Expr.Num n, _), _])) = + norm_cmp_mul k r f e1 e2 (Rat.inv n) + | norm_cmp1 k r f e1 (e2 as Argo_Expr.E (Argo_Expr.Add, Argo_Expr.E (Argo_Expr.Num n, _) :: _)) = + let fun mk e = mk_add [E e, mk_num (~ n)] + in SOME (Argo_Proof.Rewr_Ineq_Add (r, ~ n), R (k, f [mk e1, mk e2])) end + | norm_cmp1 k r f e1 (e2 as Argo_Expr.E (Argo_Expr.Add, es)) = norm_cmp_swap k r f e1 e2 es + | norm_cmp1 _ _ _ _ _ = NONE + +fun rewr_cmp _ r pred (Argo_Expr.E (Argo_Expr.Num n1, _)) (Argo_Expr.E (Argo_Expr.Num n2, _)) = + let val b = pred n1 n2 + in SOME (Argo_Proof.Rewr_Ineq_Nums (r, b), if b then e_true else e_false) end + | rewr_cmp k r _ (e1 as Argo_Expr.E (Argo_Expr.Num _, _)) e2 = norm_cmp1 k r I e1 e2 + | rewr_cmp k r _ e1 (e2 as Argo_Expr.E (Argo_Expr.Num _, _)) = norm_cmp1 k r rev e2 e1 + | rewr_cmp k r _ e1 e2 = + SOME (Argo_Proof.Rewr_Ineq_Sub r, R (k, [mk_sub (E e1) (E e2), mk_num @0])) + + +(* + Arithmetic expressions are normalized in order to reduce the number of + problem literals. Arithmetically equal expressions are normalized to + syntactically equal expressions as much as possible. +*) + +fun rewr_neg e = SOME (Argo_Proof.Rewr_Neg, scale @~1 (E e)) +fun rewr_sub e1 e2 = SOME (Argo_Proof.Rewr_Sub, mk_add [E e1, scale @~1 (E e2)]) +fun rewr_abs e = SOME (Argo_Proof.Rewr_Abs, mk_ite (mk_le (mk_num @0) (E e)) (E e) (mk_neg (E e))) + +fun rewr_min e1 e2 = + (case Argo_Expr.expr_ord (e1, e2) of + LESS => SOME (Argo_Proof.Rewr_Min_Lt, mk_ite (mk_le' e1 e2) (E e1) (E e2)) + | EQUAL => SOME (Argo_Proof.Rewr_Min_Eq, E e1) + | GREATER => SOME (Argo_Proof.Rewr_Min_Gt, mk_ite (mk_le' e2 e1) (E e2) (E e1))) + +fun rewr_max e1 e2 = + (case Argo_Expr.expr_ord (e1, e2) of + LESS => SOME (Argo_Proof.Rewr_Max_Lt, mk_ite (mk_le' e1 e2) (E e2) (E e1)) + | EQUAL => SOME (Argo_Proof.Rewr_Max_Eq, E e1) + | GREATER => SOME (Argo_Proof.Rewr_Max_Gt, mk_ite (mk_le' e2 e1) (E e1) (E e2))) + +val norm_add = nary Argo_Expr.Add rewr_add +val norm_mul = binary Argo_Expr.Mul rewr_mul + +val norm_arith = + unary Argo_Expr.Neg rewr_neg #> + binary Argo_Expr.Sub rewr_sub #> + norm_mul #> + binary Argo_Expr.Div rewr_div #> + norm_add #> + binary Argo_Expr.Min rewr_min #> + binary Argo_Expr.Max rewr_max #> + unary Argo_Expr.Abs rewr_abs #> + binary Argo_Expr.Eq rewr_eq #> + binary Argo_Expr.Le (rewr_cmp Argo_Expr.Le Argo_Proof.Le Rat.le) #> + binary Argo_Expr.Lt (rewr_cmp Argo_Expr.Lt Argo_Proof.Lt Rat.lt) + end diff -r 75ee8475c37e -r a5a09855e424 src/Tools/Argo/argo_simplex.ML --- a/src/Tools/Argo/argo_simplex.ML Fri Jan 20 17:22:54 2017 +0100 +++ b/src/Tools/Argo/argo_simplex.ML Fri Jan 20 21:05:11 2017 +0100 @@ -21,9 +21,6 @@ signature ARGO_SIMPLEX = sig - (* simplification *) - val simplify: Argo_Rewr.context -> Argo_Rewr.context - (* context *) type context val context: context @@ -43,235 +40,6 @@ structure Argo_Simplex: ARGO_SIMPLEX = struct -(* expression functions *) - -fun mk_mul n e = - if n = @0 then Argo_Expr.mk_num n - else if n = @1 then e - else Argo_Expr.mk_mul (Argo_Expr.mk_num n) e - -fun dest_mul (Argo_Expr.E (Argo_Expr.Mul, [Argo_Expr.E (Argo_Expr.Num n, _), e])) = (n, e) - | dest_mul e = (@1, e) - -fun dest_factor e = fst (dest_mul e) - -fun mk_add [] = raise Fail "bad addition" - | mk_add [e] = e - | mk_add es = Argo_Expr.mk_add es - -fun dest_ineq (Argo_Expr.E (Argo_Expr.Le, [e1, e2])) = SOME (false, e1, e2) - | dest_ineq (Argo_Expr.E (Argo_Expr.Lt, [e1, e2])) = SOME (true, e1, e2) - | dest_ineq _ = NONE - - -(* simplification *) - -(* - Products are normalized either to a number or to the monomial form - a * x - where a is a non-zero number and x is a variable. If x is a product, - it contains no number factors. The coefficient a is dropped if it is equal - to one; instead of 1 * x the expression x is used. - - No further normalization to non-linear products is applied. Hence, the - products x * y and y * x will be treated as two different variables by the - arithmetic decision procedure. -*) - -val mul_comm_rhs = Argo_Rewr.scan "(mul (? 2) (? 1))" - -fun norm_mul env = - (case apply2 (Argo_Rewr.get env) (1, 2) of - (Argo_Expr.E (Argo_Expr.Num n1, _), Argo_Expr.E (Argo_Expr.Num n2, _)) => - SOME (Argo_Proof.Rewr_Mul_Nums (n1, n2), Argo_Rewr.E (Argo_Expr.mk_num (n1 * n2))) - | (Argo_Expr.E (Argo_Expr.Num n, _), _) => - if n = @0 then SOME (Argo_Proof.Rewr_Mul_Zero, Argo_Rewr.V 1) - else if n = @1 then SOME (Argo_Proof.Rewr_Mul_One, Argo_Rewr.V 2) - else NONE - | (_, Argo_Expr.E (Argo_Expr.Num _, _)) => SOME (Argo_Proof.Rewr_Mul_Comm, mul_comm_rhs) - | _ => NONE) - -(* - Quotients are normalized either to a number or to the monomial form - a * x - where a is a non-zero number and x is a variable. If x is a quotient, - both divident and divisor are not a number. The coefficient a is dropped - if it is equal to one; instead of 1 * x the expression x is used. - - No further normalization to quotients is applied. Hence, the - expressions (x * z) / y and x * (z / y) will be treated as two different - variables by the arithmetic decision procedure. -*) - -fun div_mul_rhs n e = - let val pat = Argo_Rewr.P (Argo_Expr.Div, [Argo_Rewr.E e, Argo_Rewr.V 2]) - in Argo_Rewr.P (Argo_Expr.Mul, [Argo_Rewr.E (Argo_Expr.mk_num n), pat]) end - -fun div_inv_rhs n pat = - let val inv_pat = Argo_Rewr.P (Argo_Expr.Div, map (Argo_Rewr.E o Argo_Expr.mk_num) [@1, n]) - in Argo_Rewr.P (Argo_Expr.Mul, [inv_pat, pat]) end - -fun norm_div env = - (case apply2 (Argo_Rewr.get env) (1, 2) of - (Argo_Expr.E (Argo_Expr.Num n1, _), Argo_Expr.E (Argo_Expr.Num n2, _)) => - if n2 = @0 then NONE - else SOME (Argo_Proof.Rewr_Div_Nums (n1, n2), Argo_Rewr.E (Argo_Expr.mk_num (n1 / n2))) - | (Argo_Expr.E (Argo_Expr.Num n, _), _) => - if n = @0 then SOME (Argo_Proof.Rewr_Div_Zero, Argo_Rewr.E (Argo_Expr.mk_num @0)) - else if n = @1 then NONE - else SOME (Argo_Proof.Rewr_Div_Mul, div_mul_rhs n (Argo_Expr.mk_num @1)) - | (Argo_Expr.E (Argo_Expr.Mul, [Argo_Expr.E (Argo_Expr.Num n, _), e]), _) => - if n = @1 then NONE - else SOME (Argo_Proof.Rewr_Div_Left, div_mul_rhs n e) - | (_, Argo_Expr.E (Argo_Expr.Num n, _)) => - if n = @0 then NONE - else if n = @1 then SOME (Argo_Proof.Rewr_Div_One, Argo_Rewr.V 1) - else SOME (Argo_Proof.Rewr_Div_Inv, div_inv_rhs n (Argo_Rewr.V 1)) - | (_, Argo_Expr.E (Argo_Expr.Mul, [Argo_Expr.E (Argo_Expr.Num n, _), e])) => - let val pat = Argo_Rewr.P (Argo_Expr.Div, [Argo_Rewr.V 1, Argo_Rewr.E e]) - in SOME (Argo_Proof.Rewr_Div_Right, div_inv_rhs n pat) end - | _ => NONE) - -(* - Sums are flatten and normalized to the polynomial form - a_0 + a_1 * x_1 + ... + a_n * x_n - where all variables x_i are disjoint and where all coefficients a_i are - non-zero numbers. Coefficients equal to one are dropped; instead of 1 * x_i - the reduced monom x_i is used. The variables x_i are ordered based on the - expression order to reduce the number of problem literals by sharing equal - expressions. -*) - -fun add_monom_expr i n e (p, s, etab) = - let val etab = Argo_Exprtab.map_default (e, (i, @0)) (apsnd (Rat.add n)) etab - in ((n, Option.map fst (Argo_Exprtab.lookup etab e)) :: p, s, etab) end - -fun add_monom (_, Argo_Expr.E (Argo_Expr.Num n, _)) (p, s, etab) = ((n, NONE) :: p, s + n, etab) - | add_monom (i, Argo_Expr.E (Argo_Expr.Mul, [Argo_Expr.E (Argo_Expr.Num n, _), e])) x = - add_monom_expr i n e x - | add_monom (i, e) x = add_monom_expr i @1 e x - -fun norm_add d es = - let - val (p1, s, etab) = fold_index add_monom es ([], @0, Argo_Exprtab.empty) - val (p2, es) = - [] - |> Argo_Exprtab.fold_rev (fn (e, (i, n)) => n <> @0 ? cons ((n, SOME i), mk_mul n e)) etab - |> s <> @0 ? cons ((s, NONE), Argo_Expr.mk_num s) - |> (fn [] => [((@0, NONE), Argo_Expr.mk_num @0)] | xs => xs) - |> split_list - val ps = (rev p1, p2) - in - if d = 1 andalso eq_list (op =) ps then NONE - else SOME (Argo_Proof.Rewr_Add ps, mk_add es) - end - -(* - An equation between two arithmetic expressions is rewritten to a conjunction of two - non-strict inequalities. -*) - -val eq_rhs = Argo_Rewr.scan "(and (le (? 1) (? 2)) (le (? 2) (? 1)))" -fun is_arith e = member (op =) [Argo_Expr.Real] (Argo_Expr.type_of e) - -fun norm_eq env = - if is_arith (Argo_Rewr.get env 1) then SOME (Argo_Proof.Rewr_Eq_Le, eq_rhs) - else NONE - -(* - Arithmetic inequalities (less and less-than) are normalized to the normal form - a_0 + a_1 * x_1 + ... + a_n * x_n ~ b - or - b ~ a_0 + a_1 * x_1 + ... + a_n * x_n - such that most of the coefficients a_i are positive. - - Arithmetic inequalities of the form - a * x ~ b - or - b ~ a * x - are normalized to the form - x ~ c - or - c ~ x - where c is a number. -*) - -fun mk_num_pat n = Argo_Rewr.E (Argo_Expr.mk_num n) -fun mk_cmp_pat k ps = Argo_Rewr.P (k, ps) - -fun norm_cmp_mul k r n = - let - fun mult i = Argo_Rewr.P (Argo_Expr.Mul, [mk_num_pat n, Argo_Rewr.V i]) - val ps = if n > @0 then [mult 1, mult 2] else [mult 2, mult 1] - in SOME (Argo_Proof.Rewr_Ineq_Mul (r, n), mk_cmp_pat k ps) end - -fun count_factors pred es = fold (fn e => if pred (dest_factor e) then Integer.add 1 else I) es 0 - -fun norm_cmp_swap k r es = - let - val pos = count_factors (fn n => n > @0) es - val neg = count_factors (fn n => n < @0) es - val keep = pos > neg orelse (pos = neg andalso dest_factor (hd es) > @0) - in if keep then NONE else norm_cmp_mul k r @~1 end - -fun norm_cmp1 k r (Argo_Expr.E (Argo_Expr.Mul, [Argo_Expr.E (Argo_Expr.Num n, _), _])) = - norm_cmp_mul k r (Rat.inv n) - | norm_cmp1 k r (Argo_Expr.E (Argo_Expr.Add, Argo_Expr.E (Argo_Expr.Num n, _) :: _)) = - let fun mk i = Argo_Rewr.P (Argo_Expr.Add, [Argo_Rewr.V i, mk_num_pat (~ n)]) - in SOME (Argo_Proof.Rewr_Ineq_Add (r, ~ n), mk_cmp_pat k [mk 1, mk 2]) end - | norm_cmp1 k r (Argo_Expr.E (Argo_Expr.Add, es)) = norm_cmp_swap k r es - | norm_cmp1 _ _ _ = NONE - -val nums_true_rhs = Argo_Rewr.scan "true" -val nums_false_rhs = Argo_Rewr.scan "false" - -val cmp_sub_rhs = map Argo_Rewr.scan ["(sub (? 1) (? 2))", "(num 0)"] - -fun norm_cmp k r pred env = - (case apply2 (Argo_Rewr.get env) (1, 2) of - (Argo_Expr.E (Argo_Expr.Num n1, _), Argo_Expr.E (Argo_Expr.Num n2, _)) => - let val b = pred n1 n2 - in SOME (Argo_Proof.Rewr_Ineq_Nums (r, b), if b then nums_true_rhs else nums_false_rhs) end - | (Argo_Expr.E (Argo_Expr.Num _, _), e) => norm_cmp1 k r e - | (e, Argo_Expr.E (Argo_Expr.Num _, _)) => norm_cmp1 k r e - | _ => SOME (Argo_Proof.Rewr_Ineq_Sub r, mk_cmp_pat k cmp_sub_rhs)) - -(* - Arithmetic expressions are normalized in order to reduce the number of - problem literals. Arithmetically equal expressions are normalized into - syntactically equal expressions as much as possible. -*) - -val simplify = - Argo_Rewr.rule Argo_Proof.Rewr_Neg - "(neg (? 1))" - "(mul (num -1) (? 1))" #> - Argo_Rewr.rule Argo_Proof.Rewr_Sub - "(sub (? 1) (? 2))" - "(add (? 1) (mul (num -1) (? 2)))" #> - Argo_Rewr.func "(mul (? 1) (? 2))" norm_mul #> - Argo_Rewr.rule Argo_Proof.Rewr_Mul_Assoc - "(mul (? 1) (mul (? 2) (? 3)))" - "(mul (mul (? 1) (? 2)) (? 3))" #> - Argo_Rewr.rule Argo_Proof.Rewr_Mul_Sum - "(mul (? 1) (add _))" - "(add (# (mul (? 1) !)))" #> - Argo_Rewr.func "(div (? 1) (? 2))" norm_div #> - Argo_Rewr.flat "(add _)" norm_add #> - Argo_Rewr.rule Argo_Proof.Rewr_Min - "(min (? 1) (? 2))" - "(ite (le (? 1) (? 2)) (? 1) (? 2))" #> - Argo_Rewr.rule Argo_Proof.Rewr_Max - "(max (? 1) (? 2))" - "(ite (le (? 1) (? 2)) (? 2) (? 1))" #> - Argo_Rewr.rule Argo_Proof.Rewr_Abs - "(abs (? 1))" - "(ite (le (num 0) (? 1)) (? 1) (neg (? 1)))" #> - Argo_Rewr.func "(eq (? 1) (? 2))" norm_eq #> - Argo_Rewr.func "(le (? 1) (? 2))" (norm_cmp Argo_Expr.Le Argo_Proof.Le Rat.le) #> - Argo_Rewr.func "(lt (? 1) (? 2))" (norm_cmp Argo_Expr.Lt Argo_Proof.Lt Rat.lt) - - (* extended rationals *) (* @@ -339,18 +107,16 @@ Argo_Rewr.rewr (Argo_Proof.Rewr_Not_Ineq Argo_Proof.Lt) (Argo_Expr.mk_le e2 e1) e | unnegate_conv e = Argo_Rewr.keep e -val norm_scale_conv = rewrite_top ( - Argo_Rewr.rule Argo_Proof.Rewr_Mul_Sum - "(mul (? 1) (add _))" - "(add (# (mul (? 1) !)))" #> - Argo_Rewr.func "(mul (? 1) (? 2))" norm_mul) - fun scale_conv r mk n e1 e2 = let fun scale e = Argo_Expr.mk_mul (Argo_Expr.mk_num n) e val (e1, e2) = if n > @0 then (scale e1, scale e2) else (scale e2, scale e1) val conv = Argo_Rewr.rewr (Argo_Proof.Rewr_Ineq_Mul (r, n)) (mk e1 e2) - in Argo_Rewr.seq [conv, Argo_Rewr.args norm_scale_conv] end + in Argo_Rewr.seq [conv, Argo_Rewr.args (rewrite_top Argo_Rewr.norm_mul)] end + +fun dest_ineq (Argo_Expr.E (Argo_Expr.Le, [e1, e2])) = SOME (false, e1, e2) + | dest_ineq (Argo_Expr.E (Argo_Expr.Lt, [e1, e2])) = SOME (true, e1, e2) + | dest_ineq _ = NONE fun scale_ineq_conv n e = if n = @1 then Argo_Rewr.keep e @@ -363,7 +129,7 @@ let val conv = Argo_Rewr.seq [unnegate_conv, scale_ineq_conv n] in Argo_Rewr.with_proof conv (Argo_Lit.signed_expr_of lit, p) end -val combine_conv = rewrite_top (Argo_Rewr.flat "(add _)" norm_add) +val combine_conv = rewrite_top Argo_Rewr.norm_add fun reduce_conv r = Argo_Rewr.rewr (Argo_Proof.Rewr_Ineq_Nums (r, false)) Argo_Expr.false_expr fun simp_combine es p prf = diff -r 75ee8475c37e -r a5a09855e424 src/Tools/Argo/argo_solver.ML --- a/src/Tools/Argo/argo_solver.ML Fri Jan 20 17:22:54 2017 +0100 +++ b/src/Tools/Argo/argo_solver.ML Fri Jan 20 21:05:11 2017 +0100 @@ -32,117 +32,16 @@ val context = mk_context 0 Argo_Proof.solver_context Argo_Core.context -(* negation normal form *) - -fun nnf_nary r rhs env = SOME (r (length (Argo_Rewr.get_all env)), rhs) - -val not_and_rhs = Argo_Rewr.scan "(or (# (not !)))" -val not_or_rhs = Argo_Rewr.scan "(and (# (not !)))" - -val nnf = - Argo_Rewr.rule Argo_Proof.Rewr_Not_True "(not true)" "false" #> - Argo_Rewr.rule Argo_Proof.Rewr_Not_False "(not false)" "true" #> - Argo_Rewr.rule Argo_Proof.Rewr_Not_Not "(not (not (? 1)))" "(? 1)" #> - Argo_Rewr.func "(not (and _))" (nnf_nary Argo_Proof.Rewr_Not_And not_and_rhs) #> - Argo_Rewr.func "(not (or _))" (nnf_nary Argo_Proof.Rewr_Not_Or not_or_rhs) #> - Argo_Rewr.rule Argo_Proof.Rewr_Not_Iff "(not (iff (not (? 1)) (? 2)))" "(iff (? 1) (? 2))" #> - Argo_Rewr.rule Argo_Proof.Rewr_Not_Iff "(not (iff (? 1) (not (? 2))))" "(iff (? 1) (? 2))" #> - Argo_Rewr.rule Argo_Proof.Rewr_Not_Iff "(not (iff (? 1) (? 2)))" "(iff (not (? 1)) (? 2))" - - -(* propositional normalization *) - -(* - Propositional expressions are transformed into literals in the clausifier. Having - fewer literals results in faster solver execution. Normalizing propositional expressions - turns similar expressions into equal expressions, for which the same literal can be used. - The clausifier expects that only negation, disjunction, conjunction and equivalence form - propositional expressions. Expressions may be simplified to truth or falsity, but both - truth and falsity eventually occur nowhere inside expressions. -*) - -val e_true = Argo_Expr.true_expr -val e_false = Argo_Expr.false_expr - -fun first_index pred xs = - let val i = find_index pred xs - in if i >= 0 then SOME i else NONE end - -fun find_zero r_zero zero es = - Option.map (fn i => (r_zero i, zero)) (first_index (curry Argo_Expr.eq_expr zero) es) - -fun find_duals _ _ _ [] = NONE - | find_duals _ _ _ [_] = NONE - | find_duals r_dual zero i (e :: es) = - (case first_index (Argo_Expr.dual_expr e) es of - SOME i' => SOME (r_dual (i, i + i' + 1), zero) - | NONE => find_duals r_dual zero (i + 1) es) - -fun sort_nary r_sort one mk l es = - let - val n = length es - fun add (i, e) = if Argo_Expr.eq_expr (e, one) then I else Argo_Exprtab.cons_list (e, i) - fun dest (e, i) (es, is) = (e :: es, i :: is) - val (es, iss) = Argo_Exprtab.fold_rev dest (fold_index add es Argo_Exprtab.empty) ([], []) - fun identity is = length is = n andalso forall (op =) (map_index I is) - in if l = 1 andalso identity (map hd iss) then NONE else (SOME (r_sort (n, iss), mk es)) end - -fun apply_first fs es = get_first (fn f => f es) fs - -fun norm_nary r_zero r_dual r_sort zero one mk l = - apply_first [find_zero r_zero zero, find_duals r_dual zero 0, sort_nary r_sort one mk l] - -val norm_and = norm_nary Argo_Proof.Rewr_And_False Argo_Proof.Rewr_And_Dual Argo_Proof.Rewr_And_Sort - e_false e_true Argo_Expr.mk_and -val norm_or = norm_nary Argo_Proof.Rewr_Or_True Argo_Proof.Rewr_Or_Dual Argo_Proof.Rewr_Or_Sort - e_true e_false Argo_Expr.mk_or - -fun norm_iff env = - let val e1 = Argo_Rewr.get env 1 and e2 = Argo_Rewr.get env 2 - in - if Argo_Expr.dual_expr e1 e2 then SOME (Argo_Proof.Rewr_Iff_Dual, Argo_Rewr.E e_false) - else - (case Argo_Expr.expr_ord (e1, e2) of - EQUAL => SOME (Argo_Proof.Rewr_Iff_Refl, Argo_Rewr.E e_true) - | LESS => NONE - | GREATER => SOME (Argo_Proof.Rewr_Iff_Symm, Argo_Rewr.E (Argo_Expr.mk_iff e2 e1))) - end - -val norm_prop = - Argo_Rewr.flat "(and _)" norm_and #> - Argo_Rewr.flat "(or _)" norm_or #> - Argo_Rewr.rule Argo_Proof.Rewr_Imp "(imp (? 1) (? 2))" "(or (not (? 1)) (? 2))" #> - Argo_Rewr.rule Argo_Proof.Rewr_Iff_True "(iff true (? 1))" "(? 1)" #> - Argo_Rewr.rule Argo_Proof.Rewr_Iff_False "(iff false (? 1))" "(not (? 1))" #> - Argo_Rewr.rule Argo_Proof.Rewr_Iff_True "(iff (? 1) true)" "(? 1)" #> - Argo_Rewr.rule Argo_Proof.Rewr_Iff_False "(iff (? 1) false)" "(not (? 1))" #> - Argo_Rewr.rule Argo_Proof.Rewr_Iff_Not_Not "(iff (not (? 1)) (not (? 2)))" "(iff (? 1) (? 2))" #> - Argo_Rewr.func "(iff (? 1) (? 2))" norm_iff - - -(* normalization of if-then-else expressions *) - -val simp_prop_ite_result = - Argo_Rewr.scan "(and (or (not (? 1)) (? 2)) (or (? 1) (? 3)) (or (? 2) (? 3)))" - -val simp_ite_eq_result = Argo_Rewr.scan "(? 2)" - -fun simp_ite env = - if Argo_Expr.type_of (Argo_Rewr.get env 2) = Argo_Expr.Bool then - SOME (Argo_Proof.Rewr_Ite_Prop, simp_prop_ite_result) - else if Argo_Expr.eq_expr (Argo_Rewr.get env 2, Argo_Rewr.get env 3) then - SOME (Argo_Proof.Rewr_Ite_Eq, simp_ite_eq_result) - else NONE - -val norm_ite = - Argo_Rewr.rule Argo_Proof.Rewr_Ite_True "(ite true (? 1) (? 2))" "(? 1)" #> - Argo_Rewr.rule Argo_Proof.Rewr_Ite_False "(ite false (? 1) (? 2))" "(? 2)" #> - Argo_Rewr.func "(ite (? 1) (? 2) (? 3))" simp_ite - - (* rewriting and normalizing axioms *) -val simp_context = Argo_Rewr.context |> nnf |> norm_prop |> norm_ite |> Argo_Thy.simplify +val simp_context = + Argo_Rewr.context + |> Argo_Rewr.nnf + |> Argo_Rewr.norm_prop + |> Argo_Rewr.norm_ite + |> Argo_Rewr.norm_eq + |> Argo_Rewr.norm_arith + val simp_axiom = Argo_Rewr.with_proof (Argo_Rewr.rewrite simp_context) diff -r 75ee8475c37e -r a5a09855e424 src/Tools/Argo/argo_thy.ML --- a/src/Tools/Argo/argo_thy.ML Fri Jan 20 17:22:54 2017 +0100 +++ b/src/Tools/Argo/argo_thy.ML Fri Jan 20 21:05:11 2017 +0100 @@ -19,9 +19,6 @@ type context val context: context - (* simplification *) - val simplify: Argo_Rewr.context -> Argo_Rewr.context - (* enriching the context *) val add_atom: Argo_Term.term -> context -> Argo_Lit.literal option * context @@ -52,11 +49,6 @@ in (x, (cc, simplex)) end -(* simplification *) - -val simplify = Argo_Cc.simplify #> Argo_Simplex.simplify - - (* enriching the context *) fun add_atom t (cc, simplex) =