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