(*  Title:      Tools/Argo/argo_clausify.ML
    Author:     Sascha Boehme

Conversion of propositional formulas to definitional CNF.

The clausification implementation is based on:

  G. S. Tseitin. On the complexity of derivation in propositional
  calculus.  In A. O. Slisenko (editor) Structures in Constructive
  Mathematics and Mathematical Logic, Part II, Seminars in Mathematics,
  pages 115-125. Steklov Mathematic Institute, 1968.

  D. A. Plaisted and S. Greenbaum. A Structure-Preserving Clause Form
  Translation. Journal of Symbolic Computation, 1986.

  L. de Moura and N. Bj\orner. Proofs and Refutations, and Z3. In
  P. Rudnicki and G. Sutcliffe and B. Konev and R. A. Schmidt and
  S. Schulz (editors) International Workshop on the Implementation of
  Logics. CEUR Workshop Proceedings, 2008.
*)

signature ARGO_CLAUSIFY =
sig
  val clausify: Argo_Rewr.context -> Argo_Expr.expr * Argo_Proof.proof ->
    Argo_Proof.context * Argo_Core.context -> Argo_Proof.context * Argo_Core.context
end

structure Argo_Clausify: ARGO_CLAUSIFY =
struct

(* lifting of if-then-else expressions *)

(*
  It is assumed that expressions are free of if-then-else expressions whose then- and else-branch
  have boolean type. Such if-then-else expressions can be rewritten to expressions using only
  negation, conjunction and disjunction.

  All other modules treat if-then-else expressions as constant expressions. They do not analyze or
  decend into sub-expressions of an if-then-else expression.

  Lifting an if-then-else expression (ite P t u) introduces two new clauses
    (or (not P) (= (ite P t u) t)) and
    (or P (= (ite P t u) u))
*)

fun ite_clause simp k es (eps, (prf, core)) =
  let
    val e = Argo_Expr.mk_or es
    val (p, prf) = Argo_Proof.mk_taut k e prf 
    val (ep, prf) = Argo_Rewr.with_proof (Argo_Rewr.args (Argo_Rewr.rewrite_top simp)) (e, p) prf
  in (ep :: eps, (prf, core)) end

fun check_ite simp t (e as Argo_Expr.E (Argo_Expr.Ite, [e1, e2, e3])) (eps, (prf, core)) =
      (case Argo_Core.identify (Argo_Term.Term t) core of
        (Argo_Term.Known _, core) => (eps, (prf, core))
      | (Argo_Term.New _, core) =>
          (eps, (prf, core))
          |> ite_clause simp Argo_Proof.Taut_Ite_Then [Argo_Expr.mk_not e1, Argo_Expr.mk_eq e e2]
          |> ite_clause simp Argo_Proof.Taut_Ite_Else [e1, Argo_Expr.mk_eq e e3])
  | check_ite _ _ _ cx = cx

fun lift_ites simp (t as Argo_Term.T (_, _, ts)) =
  check_ite simp t (Argo_Term.expr_of t) #>
  fold (lift_ites simp) ts


(* tagged expressions and terms *)

fun pos x = (true, x)
fun neg x = (false, x)

fun mk_lit true t = Argo_Lit.Pos t
  | mk_lit false t = Argo_Lit.Neg t

fun expr_of (true, t) = Argo_Term.expr_of t
  | expr_of (false, t) = Argo_Expr.mk_not (Argo_Term.expr_of t)


(* adding literals *)

fun lit_for (polarity, x) (new_atoms, core) =
  (case Argo_Core.add_atom x core of
    (Argo_Term.Known t, core) => (mk_lit polarity t, (new_atoms, core))
  | (Argo_Term.New t, core) => (mk_lit polarity t, (t :: new_atoms, core)))

fun lit_of (Argo_Expr.E (Argo_Expr.Not, [e])) = lit_for (neg (Argo_Term.Expr e))
  | lit_of e = lit_for (pos (Argo_Term.Expr e))

fun lit_of' (pol, Argo_Term.T (_, Argo_Expr.Not, [t])) = lit_for (not pol, Argo_Term.Term t)
  | lit_of' (pol, t) = lit_for (pol, Argo_Term.Term t)


(* adding clauses *)

fun add_clause f xs p (new_atoms, (prf, core)) =
  let val (lits, (new_atoms, core)) = fold_map f xs (new_atoms, core)
  in (new_atoms, (prf, Argo_Core.add_axiom (lits, p) core)) end

fun simp_lit (e as Argo_Expr.E (Argo_Expr.Not, [Argo_Expr.E (Argo_Expr.Not, [e'])])) =
      Argo_Rewr.rewr Argo_Proof.Rewr_Not_Not e' e
  | simp_lit e = Argo_Rewr.keep e

fun simp_clause (e as Argo_Expr.E (Argo_Expr.Or, _)) = Argo_Rewr.args simp_lit e
  | simp_clause e = Argo_Rewr.keep e

fun new_clause k ls (new_atoms, (prf, core)) =
  let
    val e = Argo_Expr.mk_or (map expr_of ls)
    val (p, prf) = Argo_Proof.mk_taut k e prf
    val ((_, p), prf) = Argo_Rewr.with_proof simp_clause (e, p) prf
  in add_clause lit_of' ls p (new_atoms, (prf, core)) end


(* clausifying propositions *)

fun clausify_and t ts cx =
  let
    val n = length ts
    val k1 = Argo_Proof.Taut_And_1 n and k2 = Argo_Proof.Taut_And_2 o rpair n
  in
    cx
    |> new_clause k1 (pos t :: map neg ts)
    |> fold_index (fn (i, t') => new_clause (k2 i) [neg t, pos t']) ts
  end

fun clausify_or t ts cx =
  let
    val n = length ts
    val k1 = Argo_Proof.Taut_Or_1 o rpair n and k2 = Argo_Proof.Taut_Or_2 n
  in
    cx
    |> fold_index (fn (i, t') => new_clause (k1 i) [pos t, neg t']) ts
    |> new_clause k2 (neg t :: map pos ts)
  end

fun clausify_iff t t1 t2 cx =
  cx
  |> new_clause Argo_Proof.Taut_Iff_1 [pos t, pos t1, pos t2]
  |> new_clause Argo_Proof.Taut_Iff_2 [pos t, neg t1, neg t2]
  |> new_clause Argo_Proof.Taut_Iff_3 [neg t, neg t1, pos t2]
  |> new_clause Argo_Proof.Taut_Iff_4 [neg t, pos t1, neg t2]

fun clausify_lit (t as Argo_Term.T (_, Argo_Expr.And, ts)) = clausify_and t ts
  | clausify_lit (t as Argo_Term.T (_, Argo_Expr.Or, ts)) = clausify_or t ts
  | clausify_lit (t as Argo_Term.T (_, Argo_Expr.Iff, [t1, t2])) = clausify_iff t t1 t2
  | clausify_lit _ = I

fun exhaust_new_atoms ([], cx) = cx
  | exhaust_new_atoms (t :: new_atoms, cx) = exhaust_new_atoms (clausify_lit t (new_atoms, cx))

fun clausify_expr _ (Argo_Expr.E (Argo_Expr.True, _), _) cx = cx
  | clausify_expr _ (Argo_Expr.E (Argo_Expr.False, _), p) _ = Argo_Proof.unsat p
  | clausify_expr f (Argo_Expr.E (Argo_Expr.And, es), p) cx =
      fold_index (clausify_conj f (length es) p) es cx
  | clausify_expr f (Argo_Expr.E (Argo_Expr.Or, es), p) cx = add_clausify f es p cx
  | clausify_expr f (e, p) cx = add_clausify f [e] p cx

and clausify_conj f n p (i, e) (prf, core) =
  let val (p, prf) = Argo_Proof.mk_conj i n p prf
  in clausify_expr f (e, p) (prf, core) end

and add_clausify f es p cx =
  let val ecx as (new_atoms, _) = add_clause lit_of es p ([], cx)
  in fold f new_atoms ([], exhaust_new_atoms ecx) |-> fold (clausify_expr (K I)) end

fun clausify simp ep cx = clausify_expr (lift_ites simp) ep cx

end