1(* Title: Tools/Argo/argo_clausify.ML 2 Author: Sascha Boehme 3 4Conversion of propositional formulas to definitional CNF. 5 6The clausification implementation is based on: 7 8 G. S. Tseitin. On the complexity of derivation in propositional 9 calculus. In A. O. Slisenko (editor) Structures in Constructive 10 Mathematics and Mathematical Logic, Part II, Seminars in Mathematics, 11 pages 115-125. Steklov Mathematic Institute, 1968. 12 13 D. A. Plaisted and S. Greenbaum. A Structure-Preserving Clause Form 14 Translation. Journal of Symbolic Computation, 1986. 15 16 L. de Moura and N. Bj\orner. Proofs and Refutations, and Z3. In 17 P. Rudnicki and G. Sutcliffe and B. Konev and R. A. Schmidt and 18 S. Schulz (editors) International Workshop on the Implementation of 19 Logics. CEUR Workshop Proceedings, 2008. 20*) 21 22signature ARGO_CLAUSIFY = 23sig 24 val clausify: Argo_Rewr.context -> Argo_Expr.expr * Argo_Proof.proof -> 25 Argo_Proof.context * Argo_Core.context -> Argo_Proof.context * Argo_Core.context 26end 27 28structure Argo_Clausify: ARGO_CLAUSIFY = 29struct 30 31(* lifting of if-then-else expressions *) 32 33(* 34 It is assumed that expressions are free of if-then-else expressions whose then- and else-branch 35 have boolean type. Such if-then-else expressions can be rewritten to expressions using only 36 negation, conjunction and disjunction. 37 38 All other modules treat if-then-else expressions as constant expressions. They do not analyze or 39 decend into sub-expressions of an if-then-else expression. 40 41 Lifting an if-then-else expression (ite P t u) introduces two new clauses 42 (or (not P) (= (ite P t u) t)) and 43 (or P (= (ite P t u) u)) 44*) 45 46fun ite_clause simp k es (eps, (prf, core)) = 47 let 48 val e = Argo_Expr.mk_or es 49 val (p, prf) = Argo_Proof.mk_taut k e prf 50 val (ep, prf) = Argo_Rewr.with_proof (Argo_Rewr.args (Argo_Rewr.rewrite_top simp)) (e, p) prf 51 in (ep :: eps, (prf, core)) end 52 53fun check_ite simp t (e as Argo_Expr.E (Argo_Expr.Ite, [e1, e2, e3])) (eps, (prf, core)) = 54 (case Argo_Core.identify (Argo_Term.Term t) core of 55 (Argo_Term.Known _, core) => (eps, (prf, core)) 56 | (Argo_Term.New _, core) => 57 (eps, (prf, core)) 58 |> ite_clause simp Argo_Proof.Taut_Ite_Then [Argo_Expr.mk_not e1, Argo_Expr.mk_eq e e2] 59 |> ite_clause simp Argo_Proof.Taut_Ite_Else [e1, Argo_Expr.mk_eq e e3]) 60 | check_ite _ _ _ cx = cx 61 62fun lift_ites simp (t as Argo_Term.T (_, _, ts)) = 63 check_ite simp t (Argo_Term.expr_of t) #> 64 fold (lift_ites simp) ts 65 66 67(* tagged expressions and terms *) 68 69fun pos x = (true, x) 70fun neg x = (false, x) 71 72fun mk_lit true t = Argo_Lit.Pos t 73 | mk_lit false t = Argo_Lit.Neg t 74 75fun expr_of (true, t) = Argo_Term.expr_of t 76 | expr_of (false, t) = Argo_Expr.mk_not (Argo_Term.expr_of t) 77 78 79(* adding literals *) 80 81fun lit_for (polarity, x) (new_atoms, core) = 82 (case Argo_Core.add_atom x core of 83 (Argo_Term.Known t, core) => (mk_lit polarity t, (new_atoms, core)) 84 | (Argo_Term.New t, core) => (mk_lit polarity t, (t :: new_atoms, core))) 85 86fun lit_of (Argo_Expr.E (Argo_Expr.Not, [e])) = lit_for (neg (Argo_Term.Expr e)) 87 | lit_of e = lit_for (pos (Argo_Term.Expr e)) 88 89fun lit_of' (pol, Argo_Term.T (_, Argo_Expr.Not, [t])) = lit_for (not pol, Argo_Term.Term t) 90 | lit_of' (pol, t) = lit_for (pol, Argo_Term.Term t) 91 92 93(* adding clauses *) 94 95fun add_clause f xs p (new_atoms, (prf, core)) = 96 let val (lits, (new_atoms, core)) = fold_map f xs (new_atoms, core) 97 in (new_atoms, (prf, Argo_Core.add_axiom (lits, p) core)) end 98 99fun simp_lit (e as Argo_Expr.E (Argo_Expr.Not, [Argo_Expr.E (Argo_Expr.Not, [e'])])) = 100 Argo_Rewr.rewr Argo_Proof.Rewr_Not_Not e' e 101 | simp_lit e = Argo_Rewr.keep e 102 103fun simp_clause (e as Argo_Expr.E (Argo_Expr.Or, _)) = Argo_Rewr.args simp_lit e 104 | simp_clause e = Argo_Rewr.keep e 105 106fun new_clause k ls (new_atoms, (prf, core)) = 107 let 108 val e = Argo_Expr.mk_or (map expr_of ls) 109 val (p, prf) = Argo_Proof.mk_taut k e prf 110 val ((_, p), prf) = Argo_Rewr.with_proof simp_clause (e, p) prf 111 in add_clause lit_of' ls p (new_atoms, (prf, core)) end 112 113 114(* clausifying propositions *) 115 116fun clausify_and t ts cx = 117 let 118 val n = length ts 119 val k1 = Argo_Proof.Taut_And_1 n and k2 = Argo_Proof.Taut_And_2 o rpair n 120 in 121 cx 122 |> new_clause k1 (pos t :: map neg ts) 123 |> fold_index (fn (i, t') => new_clause (k2 i) [neg t, pos t']) ts 124 end 125 126fun clausify_or t ts cx = 127 let 128 val n = length ts 129 val k1 = Argo_Proof.Taut_Or_1 o rpair n and k2 = Argo_Proof.Taut_Or_2 n 130 in 131 cx 132 |> fold_index (fn (i, t') => new_clause (k1 i) [pos t, neg t']) ts 133 |> new_clause k2 (neg t :: map pos ts) 134 end 135 136fun clausify_iff t t1 t2 cx = 137 cx 138 |> new_clause Argo_Proof.Taut_Iff_1 [pos t, pos t1, pos t2] 139 |> new_clause Argo_Proof.Taut_Iff_2 [pos t, neg t1, neg t2] 140 |> new_clause Argo_Proof.Taut_Iff_3 [neg t, neg t1, pos t2] 141 |> new_clause Argo_Proof.Taut_Iff_4 [neg t, pos t1, neg t2] 142 143fun clausify_lit (t as Argo_Term.T (_, Argo_Expr.And, ts)) = clausify_and t ts 144 | clausify_lit (t as Argo_Term.T (_, Argo_Expr.Or, ts)) = clausify_or t ts 145 | clausify_lit (t as Argo_Term.T (_, Argo_Expr.Iff, [t1, t2])) = clausify_iff t t1 t2 146 | clausify_lit _ = I 147 148fun exhaust_new_atoms ([], cx) = cx 149 | exhaust_new_atoms (t :: new_atoms, cx) = exhaust_new_atoms (clausify_lit t (new_atoms, cx)) 150 151fun clausify_expr _ (Argo_Expr.E (Argo_Expr.True, _), _) cx = cx 152 | clausify_expr _ (Argo_Expr.E (Argo_Expr.False, _), p) _ = Argo_Proof.unsat p 153 | clausify_expr f (Argo_Expr.E (Argo_Expr.And, es), p) cx = 154 fold_index (clausify_conj f (length es) p) es cx 155 | clausify_expr f (Argo_Expr.E (Argo_Expr.Or, es), p) cx = add_clausify f es p cx 156 | clausify_expr f (e, p) cx = add_clausify f [e] p cx 157 158and clausify_conj f n p (i, e) (prf, core) = 159 let val (p, prf) = Argo_Proof.mk_conj i n p prf 160 in clausify_expr f (e, p) (prf, core) end 161 162and add_clausify f es p cx = 163 let val ecx as (new_atoms, _) = add_clause lit_of es p ([], cx) 164 in fold f new_atoms ([], exhaust_new_atoms ecx) |-> fold (clausify_expr (K I)) end 165 166fun clausify simp ep cx = clausify_expr (lift_ites simp) ep cx 167 168end 169