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