src/HOL/Tools/sat_funcs.ML
author huffman
Fri Mar 30 12:32:35 2012 +0200 (2012-03-30)
changeset 47220 52426c62b5d0
parent 45740 132a3e1c0fe5
child 51550 cec08df2c030
permissions -rw-r--r--
replace lemmas eval_nat_numeral with a simpler reformulation
webertj@17618
     1
(*  Title:      HOL/Tools/sat_funcs.ML
webertj@17618
     2
    Author:     Stephan Merz and Alwen Tiu, QSL Team, LORIA (http://qsl.loria.fr)
wenzelm@29269
     3
    Author:     Tjark Weber, TU Muenchen
webertj@17618
     4
webertj@17618
     5
Proof reconstruction from SAT solvers.
webertj@17618
     6
webertj@17618
     7
  Description:
webertj@17618
     8
    This file defines several tactics to invoke a proof-producing
webertj@17618
     9
    SAT solver on a propositional goal in clausal form.
webertj@17618
    10
webertj@17618
    11
    We use a sequent presentation of clauses to speed up resolution
webertj@17695
    12
    proof reconstruction.
webertj@17695
    13
    We call such clauses "raw clauses", which are of the form
webertj@20440
    14
          [x1, ..., xn, P] |- False
webertj@19236
    15
    (note the use of |- instead of ==>, i.e. of Isabelle's (meta-)hyps here),
webertj@20440
    16
    where each xi is a literal (see also comments in cnf_funcs.ML).
webertj@17618
    17
webertj@19236
    18
    This does not work for goals containing schematic variables!
webertj@19236
    19
webertj@20039
    20
      The tactic produces a clause representation of the given goal
webertj@20039
    21
      in DIMACS format and invokes a SAT solver, which should return
webertj@20039
    22
      a proof consisting of a sequence of resolution steps, indicating
webertj@20039
    23
      the two input clauses, and resulting in new clauses, leading to
webertj@20039
    24
      the empty clause (i.e. "False").  The tactic replays this proof
webertj@20039
    25
      in Isabelle and thus solves the overall goal.
webertj@17618
    26
webertj@20440
    27
  There are three SAT tactics available.  They differ in the CNF transformation
webertj@20039
    28
  used. "sat_tac" uses naive CNF transformation to transform the theorem to be
webertj@20039
    29
  proved before giving it to the SAT solver.  The naive transformation in the
webertj@20440
    30
  worst case can lead to an exponential blow up in formula size.  Another
webertj@20039
    31
  tactic, "satx_tac", uses "definitional CNF transformation" which attempts to
webertj@20039
    32
  produce a formula of linear size increase compared to the input formula, at
webertj@20039
    33
  the cost of possibly introducing new variables.  See cnf_funcs.ML for more
webertj@20440
    34
  comments on the CNF transformation.  "rawsat_tac" should be used with
webertj@20440
    35
  caution: no CNF transformation is performed, and the tactic's behavior is
webertj@20440
    36
  undefined if the subgoal is not already given as [| C1; ...; Cn |] ==> False,
webertj@20440
    37
  where each Ci is a disjunction.
webertj@17618
    38
webertj@20039
    39
  The SAT solver to be used can be set via the "solver" reference.  See
webertj@20039
    40
  sat_solvers.ML for possible values, and etc/settings for required (solver-
webertj@20039
    41
  dependent) configuration settings.  To replay SAT proofs in Isabelle, you
webertj@20039
    42
  must of course use a proof-producing SAT solver in the first place.
webertj@20039
    43
webertj@20039
    44
  Proofs are replayed only if "!quick_and_dirty" is false.  If
webertj@20039
    45
  "!quick_and_dirty" is true, the theorem (in case the SAT solver claims its
webertj@20039
    46
  negation to be unsatisfiable) is proved via an oracle.
webertj@17618
    47
*)
webertj@17618
    48
webertj@17618
    49
signature SAT =
webertj@17618
    50
sig
wenzelm@41447
    51
  val trace_sat: bool Unsynchronized.ref    (* input: print trace messages *)
wenzelm@41447
    52
  val solver: string Unsynchronized.ref  (* input: name of SAT solver to be used *)
wenzelm@41447
    53
  val counter: int Unsynchronized.ref     (* output: number of resolution steps during last proof replay *)
wenzelm@41447
    54
  val rawsat_thm: Proof.context -> cterm list -> thm
wenzelm@41447
    55
  val rawsat_tac: Proof.context -> int -> tactic
wenzelm@41447
    56
  val sat_tac: Proof.context -> int -> tactic
wenzelm@41447
    57
  val satx_tac: Proof.context -> int -> tactic
webertj@17618
    58
end
webertj@17618
    59
wenzelm@32232
    60
functor SATFunc(cnf : CNF) : SAT =
webertj@17622
    61
struct
webertj@17618
    62
wenzelm@32740
    63
val trace_sat = Unsynchronized.ref false;
webertj@17622
    64
wenzelm@32740
    65
val solver = Unsynchronized.ref "zchaff_with_proofs";
wenzelm@32740
    66
  (*see HOL/Tools/sat_solver.ML for possible values*)
webertj@20039
    67
wenzelm@32740
    68
val counter = Unsynchronized.ref 0;
webertj@17622
    69
wenzelm@32010
    70
val resolution_thm =
wenzelm@32010
    71
  @{lemma "(P ==> False) ==> (~ P ==> False) ==> False" by (rule case_split)}
webertj@17622
    72
wenzelm@32010
    73
val cP = cterm_of @{theory} (Var (("P", 0), HOLogic.boolT));
webertj@20278
    74
webertj@20278
    75
(* ------------------------------------------------------------------------- *)
webertj@21768
    76
(* lit_ord: an order on integers that considers their absolute values only,  *)
webertj@21768
    77
(*      thereby treating integers that represent the same atom (positively   *)
webertj@21768
    78
(*      or negatively) as equal                                              *)
webertj@21768
    79
(* ------------------------------------------------------------------------- *)
webertj@21768
    80
wenzelm@41447
    81
fun lit_ord (i, j) = int_ord (abs i, abs j);
webertj@21768
    82
webertj@21768
    83
(* ------------------------------------------------------------------------- *)
webertj@20278
    84
(* CLAUSE: during proof reconstruction, three kinds of clauses are           *)
webertj@20278
    85
(*      distinguished:                                                       *)
webertj@20278
    86
(*      1. NO_CLAUSE: clause not proved (yet)                                *)
webertj@20278
    87
(*      2. ORIG_CLAUSE: a clause as it occurs in the original problem        *)
webertj@20278
    88
(*      3. RAW_CLAUSE: a raw clause, with additional precomputed information *)
webertj@20278
    89
(*         (a mapping from int's to its literals) for faster proof           *)
webertj@20278
    90
(*         reconstruction                                                    *)
webertj@20278
    91
(* ------------------------------------------------------------------------- *)
webertj@20278
    92
wenzelm@41447
    93
datatype CLAUSE =
wenzelm@41447
    94
    NO_CLAUSE
wenzelm@41447
    95
  | ORIG_CLAUSE of thm
wenzelm@41447
    96
  | RAW_CLAUSE of thm * (int * cterm) list;
webertj@20278
    97
webertj@17622
    98
(* ------------------------------------------------------------------------- *)
webertj@17809
    99
(* resolve_raw_clauses: given a non-empty list of raw clauses, we fold       *)
webertj@17809
   100
(*      resolution over the list (starting with its head), i.e. with two raw *)
webertj@17809
   101
(*      clauses                                                              *)
webertj@20440
   102
(*        [P, x1, ..., a, ..., xn] |- False                                  *)
webertj@17622
   103
(*      and                                                                  *)
webertj@20440
   104
(*        [Q, y1, ..., a', ..., ym] |- False                                 *)
webertj@19976
   105
(*      (where a and a' are dual to each other), we convert the first clause *)
webertj@19976
   106
(*      to                                                                   *)
webertj@20440
   107
(*        [P, x1, ..., xn] |- a ==> False ,                                  *)
webertj@19976
   108
(*      the second clause to                                                 *)
webertj@20440
   109
(*        [Q, y1, ..., ym] |- a' ==> False                                   *)
webertj@19976
   110
(*      and then perform resolution with                                     *)
webertj@19976
   111
(*        [| ?P ==> False; ~?P ==> False |] ==> False                        *)
webertj@19976
   112
(*      to produce                                                           *)
webertj@20440
   113
(*        [P, Q, x1, ..., xn, y1, ..., ym] |- False                          *)
webertj@21768
   114
(*      Each clause is accompanied with an association list mapping integers *)
webertj@21768
   115
(*      (positive for positive literals, negative for negative literals, and *)
webertj@21768
   116
(*      the same absolute value for dual literals) to the actual literals as *)
webertj@21768
   117
(*      cterms.                                                              *)
webertj@17622
   118
(* ------------------------------------------------------------------------- *)
webertj@17618
   119
webertj@17809
   120
fun resolve_raw_clauses [] =
wenzelm@32091
   121
      raise THM ("Proof reconstruction failed (empty list of resolvents)!", 0, [])
webertj@17809
   122
  | resolve_raw_clauses (c::cs) =
wenzelm@41447
   123
      let
wenzelm@41447
   124
        (* merges two sorted lists wrt. 'lit_ord', suppressing duplicates *)
wenzelm@41447
   125
        fun merge xs [] = xs
wenzelm@41447
   126
          | merge [] ys = ys
wenzelm@41447
   127
          | merge (x :: xs) (y :: ys) =
wenzelm@41447
   128
              (case (lit_ord o pairself fst) (x, y) of
wenzelm@41447
   129
                LESS => x :: merge xs (y :: ys)
wenzelm@41447
   130
              | EQUAL => x :: merge xs ys
wenzelm@41447
   131
              | GREATER => y :: merge (x :: xs) ys)
webertj@21768
   132
wenzelm@41447
   133
        (* find out which two hyps are used in the resolution *)
wenzelm@41447
   134
        fun find_res_hyps ([], _) _ =
wenzelm@41447
   135
              raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, [])
wenzelm@41447
   136
          | find_res_hyps (_, []) _ =
wenzelm@41447
   137
              raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, [])
wenzelm@41447
   138
          | find_res_hyps (h1 :: hyps1, h2 :: hyps2) acc =
wenzelm@41447
   139
              (case (lit_ord o pairself fst) (h1, h2) of
wenzelm@41447
   140
                LESS  => find_res_hyps (hyps1, h2 :: hyps2) (h1 :: acc)
wenzelm@41447
   141
              | EQUAL =>
wenzelm@41447
   142
                  let
wenzelm@41447
   143
                    val (i1, chyp1) = h1
wenzelm@41447
   144
                    val (i2, chyp2) = h2
wenzelm@41447
   145
                  in
wenzelm@41447
   146
                    if i1 = ~ i2 then
wenzelm@41447
   147
                      (i1 < 0, chyp1, chyp2, rev acc @ merge hyps1 hyps2)
wenzelm@41447
   148
                    else (* i1 = i2 *)
wenzelm@41447
   149
                      find_res_hyps (hyps1, hyps2) (h1 :: acc)
wenzelm@41447
   150
                  end
wenzelm@41447
   151
          | GREATER => find_res_hyps (h1 :: hyps1, hyps2) (h2 :: acc))
webertj@19976
   152
wenzelm@41447
   153
        fun resolution (c1, hyps1) (c2, hyps2) =
wenzelm@41447
   154
          let
wenzelm@41447
   155
            val _ =
wenzelm@44058
   156
              if ! trace_sat then  (* FIXME !? *)
wenzelm@41447
   157
                tracing ("Resolving clause: " ^ Display.string_of_thm_without_context c1 ^
wenzelm@44058
   158
                  " (hyps: " ^ ML_Syntax.print_list
wenzelm@44058
   159
                    (Syntax.string_of_term_global (theory_of_thm c1)) (Thm.hyps_of c1)
wenzelm@41447
   160
                  ^ ")\nwith clause: " ^ Display.string_of_thm_without_context c2 ^
wenzelm@44058
   161
                  " (hyps: " ^ ML_Syntax.print_list
wenzelm@44058
   162
                    (Syntax.string_of_term_global (theory_of_thm c2)) (Thm.hyps_of c2) ^ ")")
wenzelm@41447
   163
              else ()
webertj@17809
   164
wenzelm@41447
   165
            (* the two literals used for resolution *)
wenzelm@41447
   166
            val (hyp1_is_neg, hyp1, hyp2, new_hyps) = find_res_hyps (hyps1, hyps2) []
webertj@19236
   167
wenzelm@41447
   168
            val c1' = Thm.implies_intr hyp1 c1  (* Gamma1 |- hyp1 ==> False *)
wenzelm@41447
   169
            val c2' = Thm.implies_intr hyp2 c2  (* Gamma2 |- hyp2 ==> False *)
webertj@17618
   170
wenzelm@41447
   171
            val res_thm =  (* |- (lit ==> False) ==> (~lit ==> False) ==> False *)
wenzelm@41447
   172
              let
wenzelm@41447
   173
                val cLit =
wenzelm@41447
   174
                  snd (Thm.dest_comb (if hyp1_is_neg then hyp2 else hyp1))  (* strip Trueprop *)
wenzelm@41447
   175
              in
wenzelm@41447
   176
                Thm.instantiate ([], [(cP, cLit)]) resolution_thm
wenzelm@41447
   177
              end
webertj@19236
   178
wenzelm@41447
   179
            val _ =
wenzelm@41447
   180
              if !trace_sat then
wenzelm@41447
   181
                tracing ("Resolution theorem: " ^ Display.string_of_thm_without_context res_thm)
wenzelm@41447
   182
              else ()
webertj@19236
   183
wenzelm@41447
   184
            (* Gamma1, Gamma2 |- False *)
wenzelm@41447
   185
            val c_new =
wenzelm@41447
   186
              Thm.implies_elim
wenzelm@41447
   187
                (Thm.implies_elim res_thm (if hyp1_is_neg then c2' else c1'))
wenzelm@41447
   188
                (if hyp1_is_neg then c1' else c2')
webertj@20278
   189
wenzelm@41447
   190
            val _ =
wenzelm@41447
   191
              if !trace_sat then
wenzelm@41447
   192
                tracing ("Resulting clause: " ^ Display.string_of_thm_without_context c_new ^
wenzelm@41447
   193
                  " (hyps: " ^ ML_Syntax.print_list
wenzelm@44058
   194
                      (Syntax.string_of_term_global (theory_of_thm c_new)) (Thm.hyps_of c_new) ^ ")")
wenzelm@41447
   195
              else ()
wenzelm@41447
   196
            val _ = Unsynchronized.inc counter
wenzelm@41447
   197
          in
wenzelm@41447
   198
            (c_new, new_hyps)
wenzelm@41447
   199
          end
wenzelm@41447
   200
        in
wenzelm@41447
   201
          fold resolution cs c
wenzelm@41447
   202
        end;
webertj@17618
   203
webertj@17622
   204
(* ------------------------------------------------------------------------- *)
webertj@17809
   205
(* replay_proof: replays the resolution proof returned by the SAT solver;    *)
webertj@17809
   206
(*      cf. SatSolver.proof for details of the proof format.  Updates the    *)
webertj@17809
   207
(*      'clauses' array with derived clauses, and returns the derived clause *)
webertj@17809
   208
(*      at index 'empty_id' (which should just be "False" if proof           *)
webertj@17809
   209
(*      reconstruction was successful, with the used clauses as hyps).       *)
webertj@20278
   210
(*      'atom_table' must contain an injective mapping from all atoms that   *)
webertj@20278
   211
(*      occur (as part of a literal) in 'clauses' to positive integers.      *)
webertj@17622
   212
(* ------------------------------------------------------------------------- *)
webertj@17622
   213
webertj@20278
   214
fun replay_proof atom_table clauses (clause_table, empty_id) =
wenzelm@41447
   215
  let
wenzelm@41447
   216
    fun index_of_literal chyp =
wenzelm@41447
   217
      (case (HOLogic.dest_Trueprop o Thm.term_of) chyp of
wenzelm@41447
   218
        (Const (@{const_name Not}, _) $ atom) =>
wenzelm@41447
   219
          SOME (~ (the (Termtab.lookup atom_table atom)))
wenzelm@41447
   220
      | atom => SOME (the (Termtab.lookup atom_table atom)))
wenzelm@41447
   221
      handle TERM _ => NONE;  (* 'chyp' is not a literal *)
webertj@20278
   222
wenzelm@41447
   223
    fun prove_clause id =
wenzelm@41447
   224
      (case Array.sub (clauses, id) of
wenzelm@41447
   225
        RAW_CLAUSE clause => clause
wenzelm@41447
   226
      | ORIG_CLAUSE thm =>
wenzelm@41447
   227
          (* convert the original clause *)
wenzelm@41447
   228
          let
wenzelm@41447
   229
            val _ =
wenzelm@41447
   230
              if !trace_sat then tracing ("Using original clause #" ^ string_of_int id) else ()
wenzelm@41447
   231
            val raw = cnf.clause2raw_thm thm
wenzelm@41447
   232
            val hyps = sort (lit_ord o pairself fst) (map_filter (fn chyp =>
wenzelm@41447
   233
              Option.map (rpair chyp) (index_of_literal chyp)) (#hyps (Thm.crep_thm raw)))
wenzelm@41447
   234
            val clause = (raw, hyps)
wenzelm@41447
   235
            val _ = Array.update (clauses, id, RAW_CLAUSE clause)
wenzelm@41447
   236
          in
wenzelm@41447
   237
            clause
wenzelm@41447
   238
          end
wenzelm@41447
   239
      | NO_CLAUSE =>
wenzelm@41447
   240
          (* prove the clause, using information from 'clause_table' *)
wenzelm@41447
   241
          let
wenzelm@41447
   242
            val _ =
wenzelm@41447
   243
              if !trace_sat then tracing ("Proving clause #" ^ string_of_int id ^ " ...") else ()
wenzelm@41447
   244
            val ids = the (Inttab.lookup clause_table id)
wenzelm@41447
   245
            val clause = resolve_raw_clauses (map prove_clause ids)
wenzelm@41447
   246
            val _ = Array.update (clauses, id, RAW_CLAUSE clause)
wenzelm@41447
   247
            val _ =
wenzelm@41447
   248
              if !trace_sat then
wenzelm@41447
   249
                tracing ("Replay chain successful; clause stored at #" ^ string_of_int id)
wenzelm@41447
   250
              else ()
wenzelm@41447
   251
          in
wenzelm@41447
   252
            clause
wenzelm@41447
   253
          end)
webertj@17618
   254
wenzelm@41447
   255
    val _ = counter := 0
wenzelm@41447
   256
    val empty_clause = fst (prove_clause empty_id)
wenzelm@41447
   257
    val _ =
wenzelm@41447
   258
      if !trace_sat then
wenzelm@41447
   259
        tracing ("Proof reconstruction successful; " ^
wenzelm@41447
   260
          string_of_int (!counter) ^ " resolution step(s) total.")
wenzelm@41447
   261
      else ()
wenzelm@41447
   262
  in
wenzelm@41447
   263
    empty_clause
wenzelm@41447
   264
  end;
webertj@17622
   265
webertj@20278
   266
(* ------------------------------------------------------------------------- *)
webertj@20278
   267
(* string_of_prop_formula: return a human-readable string representation of  *)
webertj@20278
   268
(*      a 'prop_formula' (just for tracing)                                  *)
webertj@20278
   269
(* ------------------------------------------------------------------------- *)
webertj@20278
   270
wenzelm@41471
   271
fun string_of_prop_formula Prop_Logic.True = "True"
wenzelm@41471
   272
  | string_of_prop_formula Prop_Logic.False = "False"
wenzelm@41471
   273
  | string_of_prop_formula (Prop_Logic.BoolVar i) = "x" ^ string_of_int i
wenzelm@41471
   274
  | string_of_prop_formula (Prop_Logic.Not fm) = "~" ^ string_of_prop_formula fm
wenzelm@41471
   275
  | string_of_prop_formula (Prop_Logic.Or (fm1, fm2)) =
wenzelm@41447
   276
      "(" ^ string_of_prop_formula fm1 ^ " v " ^ string_of_prop_formula fm2 ^ ")"
wenzelm@41471
   277
  | string_of_prop_formula (Prop_Logic.And (fm1, fm2)) =
wenzelm@41447
   278
      "(" ^ string_of_prop_formula fm1 ^ " & " ^ string_of_prop_formula fm2 ^ ")";
webertj@17622
   279
webertj@17622
   280
(* ------------------------------------------------------------------------- *)
webertj@21267
   281
(* rawsat_thm: run external SAT solver with the given clauses.  Reconstructs *)
webertj@21267
   282
(*      a proof from the resulting proof trace of the SAT solver.  The       *)
webertj@21267
   283
(*      theorem returned is just "False" (with some of the given clauses as  *)
webertj@21267
   284
(*      hyps).                                                               *)
webertj@21267
   285
(* ------------------------------------------------------------------------- *)
webertj@21267
   286
wenzelm@32432
   287
fun rawsat_thm ctxt clauses =
wenzelm@41447
   288
  let
wenzelm@41447
   289
    (* remove premises that equal "True" *)
wenzelm@41447
   290
    val clauses' = filter (fn clause =>
wenzelm@45740
   291
      (not_equal @{term True} o HOLogic.dest_Trueprop o Thm.term_of) clause
wenzelm@41447
   292
        handle TERM ("dest_Trueprop", _) => true) clauses
wenzelm@41447
   293
    (* remove non-clausal premises -- of course this shouldn't actually   *)
wenzelm@41447
   294
    (* remove anything as long as 'rawsat_tac' is only called after the   *)
wenzelm@41447
   295
    (* premises have been converted to clauses                            *)
wenzelm@41447
   296
    val clauses'' = filter (fn clause =>
wenzelm@41447
   297
      ((cnf.is_clause o HOLogic.dest_Trueprop o Thm.term_of) clause
wenzelm@41447
   298
        handle TERM ("dest_Trueprop", _) => false)
wenzelm@41447
   299
      orelse (
wenzelm@41447
   300
        warning ("Ignoring non-clausal premise " ^ Syntax.string_of_term ctxt (Thm.term_of clause));
wenzelm@41447
   301
        false)) clauses'
wenzelm@41447
   302
    (* remove trivial clauses -- this is necessary because zChaff removes *)
wenzelm@41447
   303
    (* trivial clauses during preprocessing, and otherwise our clause     *)
wenzelm@41447
   304
    (* numbering would be off                                             *)
wenzelm@41447
   305
    val nontrivial_clauses =
wenzelm@41447
   306
      filter (not o cnf.clause_is_trivial o HOLogic.dest_Trueprop o Thm.term_of) clauses''
wenzelm@41447
   307
    (* sort clauses according to the term order -- an optimization,       *)
wenzelm@41447
   308
    (* useful because forming the union of hypotheses, as done by         *)
wenzelm@41447
   309
    (* Conjunction.intr_balanced and fold Thm.weaken below, is quadratic for *)
wenzelm@41447
   310
    (* terms sorted in descending order, while only linear for terms      *)
wenzelm@41447
   311
    (* sorted in ascending order                                          *)
wenzelm@41447
   312
    val sorted_clauses = sort (Term_Ord.fast_term_ord o pairself Thm.term_of) nontrivial_clauses
wenzelm@41447
   313
    val _ =
wenzelm@41447
   314
      if !trace_sat then
wenzelm@41447
   315
        tracing ("Sorted non-trivial clauses:\n" ^
wenzelm@41447
   316
          cat_lines (map (Syntax.string_of_term ctxt o Thm.term_of) sorted_clauses))
wenzelm@41447
   317
      else ()
wenzelm@41471
   318
    (* translate clauses from HOL terms to Prop_Logic.prop_formula *)
wenzelm@41447
   319
    val (fms, atom_table) =
wenzelm@41471
   320
      fold_map (Prop_Logic.prop_formula_of_term o HOLogic.dest_Trueprop o Thm.term_of)
wenzelm@41447
   321
        sorted_clauses Termtab.empty
wenzelm@41447
   322
    val _ =
wenzelm@41447
   323
      if !trace_sat then
wenzelm@41447
   324
        tracing ("Invoking SAT solver on clauses:\n" ^ cat_lines (map string_of_prop_formula fms))
wenzelm@41447
   325
      else ()
wenzelm@41471
   326
    val fm = Prop_Logic.all fms
wenzelm@41447
   327
    (* unit -> Thm.thm *)
wenzelm@41447
   328
    fun make_quick_and_dirty_thm () =
wenzelm@41447
   329
      let
wenzelm@41447
   330
        val _ =
wenzelm@41447
   331
          if !trace_sat then
wenzelm@41447
   332
            tracing "'quick_and_dirty' is set: proof reconstruction skipped, using oracle instead."
wenzelm@41447
   333
          else ()
wenzelm@45740
   334
        val False_thm = Skip_Proof.make_thm @{theory} (HOLogic.Trueprop $ @{term False})
wenzelm@41447
   335
      in
wenzelm@41447
   336
        (* 'fold Thm.weaken (rev sorted_clauses)' is linear, while 'fold    *)
wenzelm@41447
   337
        (* Thm.weaken sorted_clauses' would be quadratic, since we sorted   *)
wenzelm@41447
   338
        (* clauses in ascending order (which is linear for                  *)
wenzelm@41447
   339
        (* 'Conjunction.intr_balanced', used below)                         *)
wenzelm@41447
   340
        fold Thm.weaken (rev sorted_clauses) False_thm
wenzelm@41447
   341
      end
wenzelm@41447
   342
  in
wenzelm@41447
   343
    case
wenzelm@41447
   344
      let val the_solver = ! solver
wenzelm@41447
   345
      in (tracing ("Invoking solver " ^ the_solver); SatSolver.invoke_solver the_solver fm) end
wenzelm@41447
   346
    of
wenzelm@41447
   347
      SatSolver.UNSATISFIABLE (SOME (clause_table, empty_id)) =>
wenzelm@41447
   348
       (if !trace_sat then
wenzelm@41447
   349
          tracing ("Proof trace from SAT solver:\n" ^
wenzelm@41447
   350
            "clauses: " ^ ML_Syntax.print_list
wenzelm@41491
   351
              (ML_Syntax.print_pair ML_Syntax.print_int (ML_Syntax.print_list ML_Syntax.print_int))
wenzelm@41447
   352
              (Inttab.dest clause_table) ^ "\n" ^
wenzelm@41491
   353
            "empty clause: " ^ string_of_int empty_id)
wenzelm@41447
   354
        else ();
wenzelm@41447
   355
        if !quick_and_dirty then
wenzelm@41447
   356
          make_quick_and_dirty_thm ()
wenzelm@41447
   357
        else
wenzelm@41447
   358
          let
wenzelm@41447
   359
            (* optimization: convert the given clauses to "[c_1 && ... && c_n] |- c_i";  *)
wenzelm@41447
   360
            (*               this avoids accumulation of hypotheses during resolution    *)
wenzelm@41447
   361
            (* [c_1, ..., c_n] |- c_1 && ... && c_n *)
wenzelm@41447
   362
            val clauses_thm = Conjunction.intr_balanced (map Thm.assume sorted_clauses)
wenzelm@41447
   363
            (* [c_1 && ... && c_n] |- c_1 && ... && c_n *)
wenzelm@41447
   364
            val cnf_cterm = cprop_of clauses_thm
wenzelm@41447
   365
            val cnf_thm = Thm.assume cnf_cterm
wenzelm@41447
   366
            (* [[c_1 && ... && c_n] |- c_1, ..., [c_1 && ... && c_n] |- c_n] *)
wenzelm@41447
   367
            val cnf_clauses = Conjunction.elim_balanced (length sorted_clauses) cnf_thm
wenzelm@41447
   368
            (* initialize the clause array with the given clauses *)
wenzelm@41447
   369
            val max_idx = the (Inttab.max_key clause_table)
wenzelm@41447
   370
            val clause_arr = Array.array (max_idx + 1, NO_CLAUSE)
wenzelm@41447
   371
            val _ =
wenzelm@41447
   372
              fold (fn thm => fn idx => (Array.update (clause_arr, idx, ORIG_CLAUSE thm); idx+1))
wenzelm@41447
   373
                cnf_clauses 0
wenzelm@41447
   374
            (* replay the proof to derive the empty clause *)
wenzelm@41447
   375
            (* [c_1 && ... && c_n] |- False *)
wenzelm@41447
   376
            val raw_thm = replay_proof atom_table clause_arr (clause_table, empty_id)
wenzelm@41447
   377
          in
wenzelm@41447
   378
            (* [c_1, ..., c_n] |- False *)
wenzelm@41447
   379
            Thm.implies_elim (Thm.implies_intr cnf_cterm raw_thm) clauses_thm
wenzelm@41447
   380
          end)
wenzelm@41447
   381
    | SatSolver.UNSATISFIABLE NONE =>
wenzelm@41447
   382
        if !quick_and_dirty then
wenzelm@41447
   383
         (warning "SAT solver claims the formula to be unsatisfiable, but did not provide a proof";
wenzelm@41447
   384
          make_quick_and_dirty_thm ())
wenzelm@41447
   385
        else
wenzelm@41447
   386
          raise THM ("SAT solver claims the formula to be unsatisfiable, but did not provide a proof", 0, [])
wenzelm@41447
   387
    | SatSolver.SATISFIABLE assignment =>
wenzelm@41447
   388
        let
wenzelm@41447
   389
          val msg =
wenzelm@41447
   390
            "SAT solver found a countermodel:\n" ^
wenzelm@41447
   391
            (commas o map (fn (term, idx) =>
wenzelm@41447
   392
                Syntax.string_of_term_global @{theory} term ^ ": " ^
wenzelm@41447
   393
                  (case assignment idx of NONE => "arbitrary"
wenzelm@41447
   394
                  | SOME true => "true" | SOME false => "false")))
wenzelm@41447
   395
              (Termtab.dest atom_table)
wenzelm@41447
   396
        in
wenzelm@41447
   397
          raise THM (msg, 0, [])
wenzelm@41447
   398
        end
wenzelm@41447
   399
    | SatSolver.UNKNOWN =>
wenzelm@41447
   400
        raise THM ("SAT solver failed to decide the formula", 0, [])
wenzelm@41447
   401
  end;
webertj@17618
   402
webertj@17622
   403
(* ------------------------------------------------------------------------- *)
webertj@17622
   404
(* Tactics                                                                   *)
webertj@17622
   405
(* ------------------------------------------------------------------------- *)
webertj@17618
   406
webertj@17809
   407
(* ------------------------------------------------------------------------- *)
webertj@17809
   408
(* rawsat_tac: solves the i-th subgoal of the proof state; this subgoal      *)
webertj@17809
   409
(*      should be of the form                                                *)
webertj@17809
   410
(*        [| c1; c2; ...; ck |] ==> False                                    *)
webertj@17809
   411
(*      where each cj is a non-empty clause (i.e. a disjunction of literals) *)
webertj@17809
   412
(*      or "True"                                                            *)
webertj@17809
   413
(* ------------------------------------------------------------------------- *)
webertj@17809
   414
wenzelm@32232
   415
fun rawsat_tac ctxt i =
wenzelm@32432
   416
  Subgoal.FOCUS (fn {context = ctxt', prems, ...} =>
wenzelm@32432
   417
    rtac (rawsat_thm ctxt' (map cprop_of prems)) 1) ctxt i;
webertj@17618
   418
webertj@17809
   419
(* ------------------------------------------------------------------------- *)
webertj@17809
   420
(* pre_cnf_tac: converts the i-th subgoal                                    *)
webertj@17809
   421
(*        [| A1 ; ... ; An |] ==> B                                          *)
webertj@17809
   422
(*      to                                                                   *)
webertj@17809
   423
(*        [| A1; ... ; An ; ~B |] ==> False                                  *)
webertj@17809
   424
(*      (handling meta-logical connectives in B properly before negating),   *)
webertj@17809
   425
(*      then replaces meta-logical connectives in the premises (i.e. "==>",  *)
webertj@17809
   426
(*      "!!" and "==") by connectives of the HOL object-logic (i.e. by       *)
webertj@19553
   427
(*      "-->", "!", and "="), then performs beta-eta-normalization on the    *)
webertj@19553
   428
(*      subgoal                                                              *)
webertj@17809
   429
(* ------------------------------------------------------------------------- *)
webertj@17809
   430
wenzelm@23533
   431
val pre_cnf_tac =
wenzelm@41447
   432
  rtac ccontr THEN'
wenzelm@41447
   433
  Object_Logic.atomize_prems_tac THEN'
wenzelm@41447
   434
  CONVERSION Drule.beta_eta_conversion;
webertj@17809
   435
webertj@17809
   436
(* ------------------------------------------------------------------------- *)
webertj@17809
   437
(* cnfsat_tac: checks if the empty clause "False" occurs among the premises; *)
webertj@17809
   438
(*      if not, eliminates conjunctions (i.e. each clause of the CNF formula *)
webertj@17809
   439
(*      becomes a separate premise), then applies 'rawsat_tac' to solve the  *)
webertj@17809
   440
(*      subgoal                                                              *)
webertj@17809
   441
(* ------------------------------------------------------------------------- *)
webertj@17697
   442
wenzelm@32232
   443
fun cnfsat_tac ctxt i =
wenzelm@41447
   444
  (etac FalseE i) ORELSE (REPEAT_DETERM (etac conjE i) THEN rawsat_tac ctxt i);
webertj@17618
   445
webertj@17809
   446
(* ------------------------------------------------------------------------- *)
webertj@17809
   447
(* cnfxsat_tac: checks if the empty clause "False" occurs among the          *)
webertj@17809
   448
(*      premises; if not, eliminates conjunctions (i.e. each clause of the   *)
webertj@17809
   449
(*      CNF formula becomes a separate premise) and existential quantifiers, *)
webertj@17809
   450
(*      then applies 'rawsat_tac' to solve the subgoal                       *)
webertj@17809
   451
(* ------------------------------------------------------------------------- *)
webertj@17809
   452
wenzelm@32232
   453
fun cnfxsat_tac ctxt i =
wenzelm@41447
   454
  (etac FalseE i) ORELSE
wenzelm@41447
   455
    (REPEAT_DETERM (etac conjE i ORELSE etac exE i) THEN rawsat_tac ctxt i);
webertj@17618
   456
webertj@17809
   457
(* ------------------------------------------------------------------------- *)
webertj@17809
   458
(* sat_tac: tactic for calling an external SAT solver, taking as input an    *)
webertj@17809
   459
(*      arbitrary formula.  The input is translated to CNF, possibly causing *)
webertj@17809
   460
(*      an exponential blowup.                                               *)
webertj@17809
   461
(* ------------------------------------------------------------------------- *)
webertj@17809
   462
wenzelm@32232
   463
fun sat_tac ctxt i =
wenzelm@41447
   464
  pre_cnf_tac i THEN cnf.cnf_rewrite_tac ctxt i THEN cnfsat_tac ctxt i;
webertj@17809
   465
webertj@17809
   466
(* ------------------------------------------------------------------------- *)
webertj@17809
   467
(* satx_tac: tactic for calling an external SAT solver, taking as input an   *)
webertj@17809
   468
(*      arbitrary formula.  The input is translated to CNF, possibly         *)
webertj@17809
   469
(*      introducing new literals.                                            *)
webertj@17809
   470
(* ------------------------------------------------------------------------- *)
webertj@17809
   471
wenzelm@32232
   472
fun satx_tac ctxt i =
wenzelm@41447
   473
  pre_cnf_tac i THEN cnf.cnfx_rewrite_tac ctxt i THEN cnfxsat_tac ctxt i;
webertj@17618
   474
wenzelm@23533
   475
end;