src/Tools/Argo/argo_solver.ML
author boehmes
Thu Sep 29 20:54:44 2016 +0200 (2016-09-29)
changeset 63960 3daf02070be5
child 64927 a5a09855e424
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_solver.ML
boehmes@63960
     2
    Author:     Sascha Boehme
boehmes@63960
     3
boehmes@63960
     4
The main interface to the Argo solver.
boehmes@63960
     5
boehmes@63960
     6
The solver performs satisfiability checking for a given set of assertions. If these assertions
boehmes@63960
     7
are unsatisfiable, a proof trace is returned. If these assertions are satisfiable, the computed
boehmes@63960
     8
model can be queried or further assertions may be added.
boehmes@63960
     9
*)
boehmes@63960
    10
boehmes@63960
    11
signature ARGO_SOLVER =
boehmes@63960
    12
sig
boehmes@63960
    13
  type context
boehmes@63960
    14
  val context: context
boehmes@63960
    15
  val assert: Argo_Expr.expr list -> context -> context (* raises Argo_Expr.TYPE, Argo_Expr.EXPR
boehmes@63960
    16
    and Argo_Proof.UNSAT *)
boehmes@63960
    17
  val model_of: context -> string * Argo_Expr.typ -> bool option
boehmes@63960
    18
end
boehmes@63960
    19
boehmes@63960
    20
structure Argo_Solver: ARGO_SOLVER =
boehmes@63960
    21
struct
boehmes@63960
    22
boehmes@63960
    23
(* context *)
boehmes@63960
    24
boehmes@63960
    25
type context = {
boehmes@63960
    26
  next_axiom: int,
boehmes@63960
    27
  prf: Argo_Proof.context,
boehmes@63960
    28
  core: Argo_Core.context}
boehmes@63960
    29
boehmes@63960
    30
fun mk_context next_axiom prf core: context = {next_axiom=next_axiom, prf=prf, core=core}
boehmes@63960
    31
boehmes@63960
    32
val context = mk_context 0 Argo_Proof.solver_context Argo_Core.context
boehmes@63960
    33
boehmes@63960
    34
boehmes@63960
    35
(* negation normal form *)
boehmes@63960
    36
boehmes@63960
    37
fun nnf_nary r rhs env = SOME (r (length (Argo_Rewr.get_all env)), rhs)
boehmes@63960
    38
boehmes@63960
    39
val not_and_rhs = Argo_Rewr.scan "(or (# (not !)))"
boehmes@63960
    40
val not_or_rhs = Argo_Rewr.scan "(and (# (not !)))"
boehmes@63960
    41
boehmes@63960
    42
val nnf =
boehmes@63960
    43
  Argo_Rewr.rule Argo_Proof.Rewr_Not_True "(not true)" "false" #>
boehmes@63960
    44
  Argo_Rewr.rule Argo_Proof.Rewr_Not_False "(not false)" "true" #>
boehmes@63960
    45
  Argo_Rewr.rule Argo_Proof.Rewr_Not_Not "(not (not (? 1)))" "(? 1)" #>
boehmes@63960
    46
  Argo_Rewr.func "(not (and _))" (nnf_nary Argo_Proof.Rewr_Not_And not_and_rhs) #>
boehmes@63960
    47
  Argo_Rewr.func "(not (or _))" (nnf_nary Argo_Proof.Rewr_Not_Or not_or_rhs) #>
boehmes@63960
    48
  Argo_Rewr.rule Argo_Proof.Rewr_Not_Iff "(not (iff (not (? 1)) (? 2)))" "(iff (? 1) (? 2))" #>
boehmes@63960
    49
  Argo_Rewr.rule Argo_Proof.Rewr_Not_Iff "(not (iff (? 1) (not (? 2))))" "(iff (? 1) (? 2))" #>
boehmes@63960
    50
  Argo_Rewr.rule Argo_Proof.Rewr_Not_Iff "(not (iff (? 1) (? 2)))" "(iff (not (? 1)) (? 2))"
boehmes@63960
    51
boehmes@63960
    52
boehmes@63960
    53
(* propositional normalization *)
boehmes@63960
    54
boehmes@63960
    55
(*
boehmes@63960
    56
  Propositional expressions are transformed into literals in the clausifier. Having
boehmes@63960
    57
  fewer literals results in faster solver execution. Normalizing propositional expressions
boehmes@63960
    58
  turns similar expressions into equal expressions, for which the same literal can be used.
boehmes@63960
    59
  The clausifier expects that only negation, disjunction, conjunction and equivalence form
boehmes@63960
    60
  propositional expressions. Expressions may be simplified to truth or falsity, but both
boehmes@63960
    61
  truth and falsity eventually occur nowhere inside expressions.
boehmes@63960
    62
*)
boehmes@63960
    63
boehmes@63960
    64
val e_true = Argo_Expr.true_expr
boehmes@63960
    65
val e_false = Argo_Expr.false_expr
boehmes@63960
    66
boehmes@63960
    67
fun first_index pred xs =
boehmes@63960
    68
  let val i = find_index pred xs
boehmes@63960
    69
  in if i >= 0 then SOME i else NONE end
boehmes@63960
    70
boehmes@63960
    71
fun find_zero r_zero zero es =
boehmes@63960
    72
  Option.map (fn i => (r_zero i, zero)) (first_index (curry Argo_Expr.eq_expr zero) es)
boehmes@63960
    73
boehmes@63960
    74
fun find_duals _ _ _ [] = NONE
boehmes@63960
    75
  | find_duals _ _ _ [_] = NONE
boehmes@63960
    76
  | find_duals r_dual zero i (e :: es) =
boehmes@63960
    77
      (case first_index (Argo_Expr.dual_expr e) es of
boehmes@63960
    78
        SOME i' => SOME (r_dual (i, i + i' + 1), zero)
boehmes@63960
    79
      | NONE => find_duals r_dual zero (i + 1) es)
boehmes@63960
    80
boehmes@63960
    81
fun sort_nary r_sort one mk l es =
boehmes@63960
    82
  let
boehmes@63960
    83
    val n = length es
boehmes@63960
    84
    fun add (i, e) = if Argo_Expr.eq_expr (e, one) then I else Argo_Exprtab.cons_list (e, i)
boehmes@63960
    85
    fun dest (e, i) (es, is) = (e :: es, i :: is)
boehmes@63960
    86
    val (es, iss) = Argo_Exprtab.fold_rev dest (fold_index add es Argo_Exprtab.empty) ([], [])
boehmes@63960
    87
    fun identity is = length is = n andalso forall (op =) (map_index I is)
boehmes@63960
    88
  in if l = 1 andalso identity (map hd iss) then NONE else (SOME (r_sort (n, iss), mk es)) end
boehmes@63960
    89
boehmes@63960
    90
fun apply_first fs es = get_first (fn f => f es) fs
boehmes@63960
    91
boehmes@63960
    92
fun norm_nary r_zero r_dual r_sort zero one mk l =
boehmes@63960
    93
  apply_first [find_zero r_zero zero, find_duals r_dual zero 0, sort_nary r_sort one mk l]
boehmes@63960
    94
boehmes@63960
    95
val norm_and = norm_nary Argo_Proof.Rewr_And_False Argo_Proof.Rewr_And_Dual Argo_Proof.Rewr_And_Sort
boehmes@63960
    96
  e_false e_true Argo_Expr.mk_and
boehmes@63960
    97
val norm_or = norm_nary Argo_Proof.Rewr_Or_True Argo_Proof.Rewr_Or_Dual Argo_Proof.Rewr_Or_Sort
boehmes@63960
    98
  e_true e_false Argo_Expr.mk_or
boehmes@63960
    99
boehmes@63960
   100
fun norm_iff env =
boehmes@63960
   101
  let val e1 = Argo_Rewr.get env 1 and e2 = Argo_Rewr.get env 2
boehmes@63960
   102
  in
boehmes@63960
   103
    if Argo_Expr.dual_expr e1 e2 then SOME (Argo_Proof.Rewr_Iff_Dual, Argo_Rewr.E e_false)
boehmes@63960
   104
    else
boehmes@63960
   105
      (case Argo_Expr.expr_ord (e1, e2) of
boehmes@63960
   106
        EQUAL => SOME (Argo_Proof.Rewr_Iff_Refl, Argo_Rewr.E e_true)
boehmes@63960
   107
      | LESS => NONE
boehmes@63960
   108
      | GREATER => SOME (Argo_Proof.Rewr_Iff_Symm, Argo_Rewr.E (Argo_Expr.mk_iff e2 e1)))
boehmes@63960
   109
  end
boehmes@63960
   110
boehmes@63960
   111
val norm_prop =
boehmes@63960
   112
  Argo_Rewr.flat "(and _)" norm_and #>
boehmes@63960
   113
  Argo_Rewr.flat "(or _)" norm_or #>
boehmes@63960
   114
  Argo_Rewr.rule Argo_Proof.Rewr_Imp "(imp (? 1) (? 2))" "(or (not (? 1)) (? 2))" #>
boehmes@63960
   115
  Argo_Rewr.rule Argo_Proof.Rewr_Iff_True "(iff true (? 1))" "(? 1)" #>
boehmes@63960
   116
  Argo_Rewr.rule Argo_Proof.Rewr_Iff_False "(iff false (? 1))" "(not (? 1))" #>
boehmes@63960
   117
  Argo_Rewr.rule Argo_Proof.Rewr_Iff_True "(iff (? 1) true)" "(? 1)" #>
boehmes@63960
   118
  Argo_Rewr.rule Argo_Proof.Rewr_Iff_False "(iff (? 1) false)" "(not (? 1))" #>
boehmes@63960
   119
  Argo_Rewr.rule Argo_Proof.Rewr_Iff_Not_Not "(iff (not (? 1)) (not (? 2)))" "(iff (? 1) (? 2))" #>
boehmes@63960
   120
  Argo_Rewr.func "(iff (? 1) (? 2))" norm_iff
boehmes@63960
   121
boehmes@63960
   122
boehmes@63960
   123
(* normalization of if-then-else expressions *)
boehmes@63960
   124
boehmes@63960
   125
val simp_prop_ite_result =
boehmes@63960
   126
  Argo_Rewr.scan "(and (or (not (? 1)) (? 2)) (or (? 1) (? 3)) (or (? 2) (? 3)))"
boehmes@63960
   127
boehmes@63960
   128
val simp_ite_eq_result = Argo_Rewr.scan "(? 2)"
boehmes@63960
   129
boehmes@63960
   130
fun simp_ite env =
boehmes@63960
   131
  if Argo_Expr.type_of (Argo_Rewr.get env 2) = Argo_Expr.Bool then
boehmes@63960
   132
    SOME (Argo_Proof.Rewr_Ite_Prop, simp_prop_ite_result)
boehmes@63960
   133
  else if Argo_Expr.eq_expr (Argo_Rewr.get env 2, Argo_Rewr.get env 3) then
boehmes@63960
   134
    SOME (Argo_Proof.Rewr_Ite_Eq, simp_ite_eq_result)
boehmes@63960
   135
  else NONE
boehmes@63960
   136
boehmes@63960
   137
val norm_ite =
boehmes@63960
   138
  Argo_Rewr.rule Argo_Proof.Rewr_Ite_True "(ite true (? 1) (? 2))" "(? 1)" #>
boehmes@63960
   139
  Argo_Rewr.rule Argo_Proof.Rewr_Ite_False "(ite false (? 1) (? 2))" "(? 2)" #>
boehmes@63960
   140
  Argo_Rewr.func "(ite (? 1) (? 2) (? 3))" simp_ite
boehmes@63960
   141
boehmes@63960
   142
boehmes@63960
   143
(* rewriting and normalizing axioms *)
boehmes@63960
   144
boehmes@63960
   145
val simp_context = Argo_Rewr.context |> nnf |> norm_prop |> norm_ite |> Argo_Thy.simplify
boehmes@63960
   146
val simp_axiom = Argo_Rewr.with_proof (Argo_Rewr.rewrite simp_context)
boehmes@63960
   147
boehmes@63960
   148
boehmes@63960
   149
(* asserting axioms *)
boehmes@63960
   150
boehmes@63960
   151
fun add_axiom e ({next_axiom, prf, core}: context) =
boehmes@63960
   152
  let
boehmes@63960
   153
    val _ = Argo_Expr.check e
boehmes@63960
   154
    val (p, prf) = Argo_Proof.mk_axiom next_axiom prf
boehmes@63960
   155
    val (ep, prf) = simp_axiom (e, p) prf 
boehmes@63960
   156
    val (prf, core) = Argo_Clausify.clausify simp_context ep (prf, core)
boehmes@63960
   157
  in mk_context (next_axiom + 1) prf core end
boehmes@63960
   158
boehmes@63960
   159
fun assert es cx =
boehmes@63960
   160
  let val {next_axiom, prf, core}: context = fold add_axiom es cx
boehmes@63960
   161
  in mk_context next_axiom prf (Argo_Core.run core) end
boehmes@63960
   162
boehmes@63960
   163
boehmes@63960
   164
(* models *)
boehmes@63960
   165
boehmes@63960
   166
fun model_of ({core, ...}: context) = Argo_Core.model_of core
boehmes@63960
   167
boehmes@63960
   168
end