src/HOL/Tools/sat.ML
author wenzelm
Fri Mar 06 15:58:56 2015 +0100 (2015-03-06)
changeset 59621 291934bac95e
parent 59582 0fbed69ff081
child 59642 929984c529d3
permissions -rw-r--r--
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm@55239
     1
(*  Title:      HOL/Tools/sat.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),
wenzelm@55239
    16
    where each xi is a literal (see also comments in cnf.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
wenzelm@55239
    33
  the cost of possibly introducing new variables.  See cnf.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
wenzelm@52059
    44
  Proofs are replayed only if "quick_and_dirty" is false.  If
wenzelm@52059
    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@55240
    51
  val trace: bool Config.T  (* print trace messages *)
wenzelm@55240
    52
  val solver: string Config.T  (* 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@55239
    60
structure SAT : SAT =
webertj@17622
    61
struct
webertj@17618
    62
wenzelm@55240
    63
val trace = Attrib.setup_config_bool @{binding sat_trace} (K false);
webertj@17622
    64
wenzelm@55240
    65
fun cond_tracing ctxt msg =
wenzelm@55240
    66
  if Config.get ctxt trace then tracing (msg ()) else ();
wenzelm@55240
    67
blanchet@56851
    68
val solver = Attrib.setup_config_string @{binding sat_solver} (K "cdclite");
wenzelm@32740
    69
  (*see HOL/Tools/sat_solver.ML for possible values*)
webertj@20039
    70
wenzelm@32740
    71
val counter = Unsynchronized.ref 0;
webertj@17622
    72
wenzelm@32010
    73
val resolution_thm =
wenzelm@32010
    74
  @{lemma "(P ==> False) ==> (~ P ==> False) ==> False" by (rule case_split)}
webertj@17622
    75
wenzelm@59621
    76
val cP = Thm.global_cterm_of @{theory} (Var (("P", 0), HOLogic.boolT));
webertj@20278
    77
webertj@20278
    78
(* ------------------------------------------------------------------------- *)
webertj@21768
    79
(* lit_ord: an order on integers that considers their absolute values only,  *)
webertj@21768
    80
(*      thereby treating integers that represent the same atom (positively   *)
webertj@21768
    81
(*      or negatively) as equal                                              *)
webertj@21768
    82
(* ------------------------------------------------------------------------- *)
webertj@21768
    83
wenzelm@41447
    84
fun lit_ord (i, j) = int_ord (abs i, abs j);
webertj@21768
    85
webertj@21768
    86
(* ------------------------------------------------------------------------- *)
webertj@20278
    87
(* CLAUSE: during proof reconstruction, three kinds of clauses are           *)
webertj@20278
    88
(*      distinguished:                                                       *)
webertj@20278
    89
(*      1. NO_CLAUSE: clause not proved (yet)                                *)
webertj@20278
    90
(*      2. ORIG_CLAUSE: a clause as it occurs in the original problem        *)
webertj@20278
    91
(*      3. RAW_CLAUSE: a raw clause, with additional precomputed information *)
webertj@20278
    92
(*         (a mapping from int's to its literals) for faster proof           *)
webertj@20278
    93
(*         reconstruction                                                    *)
webertj@20278
    94
(* ------------------------------------------------------------------------- *)
webertj@20278
    95
wenzelm@41447
    96
datatype CLAUSE =
wenzelm@41447
    97
    NO_CLAUSE
wenzelm@41447
    98
  | ORIG_CLAUSE of thm
wenzelm@41447
    99
  | RAW_CLAUSE of thm * (int * cterm) list;
webertj@20278
   100
webertj@17622
   101
(* ------------------------------------------------------------------------- *)
webertj@17809
   102
(* resolve_raw_clauses: given a non-empty list of raw clauses, we fold       *)
webertj@17809
   103
(*      resolution over the list (starting with its head), i.e. with two raw *)
webertj@17809
   104
(*      clauses                                                              *)
webertj@20440
   105
(*        [P, x1, ..., a, ..., xn] |- False                                  *)
webertj@17622
   106
(*      and                                                                  *)
webertj@20440
   107
(*        [Q, y1, ..., a', ..., ym] |- False                                 *)
webertj@19976
   108
(*      (where a and a' are dual to each other), we convert the first clause *)
webertj@19976
   109
(*      to                                                                   *)
webertj@20440
   110
(*        [P, x1, ..., xn] |- a ==> False ,                                  *)
webertj@19976
   111
(*      the second clause to                                                 *)
webertj@20440
   112
(*        [Q, y1, ..., ym] |- a' ==> False                                   *)
webertj@19976
   113
(*      and then perform resolution with                                     *)
webertj@19976
   114
(*        [| ?P ==> False; ~?P ==> False |] ==> False                        *)
webertj@19976
   115
(*      to produce                                                           *)
webertj@20440
   116
(*        [P, Q, x1, ..., xn, y1, ..., ym] |- False                          *)
webertj@21768
   117
(*      Each clause is accompanied with an association list mapping integers *)
webertj@21768
   118
(*      (positive for positive literals, negative for negative literals, and *)
webertj@21768
   119
(*      the same absolute value for dual literals) to the actual literals as *)
webertj@21768
   120
(*      cterms.                                                              *)
webertj@17622
   121
(* ------------------------------------------------------------------------- *)
webertj@17618
   122
wenzelm@55236
   123
fun resolve_raw_clauses _ [] =
wenzelm@32091
   124
      raise THM ("Proof reconstruction failed (empty list of resolvents)!", 0, [])
wenzelm@55236
   125
  | resolve_raw_clauses ctxt (c::cs) =
wenzelm@41447
   126
      let
wenzelm@41447
   127
        (* merges two sorted lists wrt. 'lit_ord', suppressing duplicates *)
wenzelm@41447
   128
        fun merge xs [] = xs
wenzelm@41447
   129
          | merge [] ys = ys
wenzelm@41447
   130
          | merge (x :: xs) (y :: ys) =
wenzelm@59058
   131
              (case lit_ord (apply2 fst (x, y)) of
wenzelm@41447
   132
                LESS => x :: merge xs (y :: ys)
wenzelm@41447
   133
              | EQUAL => x :: merge xs ys
wenzelm@41447
   134
              | GREATER => y :: merge (x :: xs) ys)
webertj@21768
   135
wenzelm@41447
   136
        (* find out which two hyps are used in the resolution *)
wenzelm@41447
   137
        fun find_res_hyps ([], _) _ =
wenzelm@41447
   138
              raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, [])
wenzelm@41447
   139
          | find_res_hyps (_, []) _ =
wenzelm@41447
   140
              raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, [])
wenzelm@41447
   141
          | find_res_hyps (h1 :: hyps1, h2 :: hyps2) acc =
wenzelm@59058
   142
              (case lit_ord  (apply2 fst (h1, h2)) of
wenzelm@41447
   143
                LESS  => find_res_hyps (hyps1, h2 :: hyps2) (h1 :: acc)
wenzelm@41447
   144
              | EQUAL =>
wenzelm@41447
   145
                  let
wenzelm@41447
   146
                    val (i1, chyp1) = h1
wenzelm@41447
   147
                    val (i2, chyp2) = h2
wenzelm@41447
   148
                  in
wenzelm@41447
   149
                    if i1 = ~ i2 then
wenzelm@41447
   150
                      (i1 < 0, chyp1, chyp2, rev acc @ merge hyps1 hyps2)
wenzelm@41447
   151
                    else (* i1 = i2 *)
wenzelm@41447
   152
                      find_res_hyps (hyps1, hyps2) (h1 :: acc)
wenzelm@41447
   153
                  end
wenzelm@41447
   154
          | GREATER => find_res_hyps (h1 :: hyps1, hyps2) (h2 :: acc))
webertj@19976
   155
wenzelm@41447
   156
        fun resolution (c1, hyps1) (c2, hyps2) =
wenzelm@41447
   157
          let
wenzelm@41447
   158
            val _ =
wenzelm@55240
   159
              cond_tracing ctxt (fn () =>
wenzelm@55240
   160
                "Resolving clause: " ^ Display.string_of_thm ctxt c1 ^
wenzelm@55240
   161
                " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term ctxt) (Thm.hyps_of c1) ^
wenzelm@55240
   162
                ")\nwith clause: " ^ Display.string_of_thm ctxt c2 ^
wenzelm@55240
   163
                " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term ctxt) (Thm.hyps_of c2) ^ ")")
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@55240
   180
              cond_tracing ctxt
wenzelm@55240
   181
                (fn () => "Resolution theorem: " ^ Display.string_of_thm ctxt res_thm)
webertj@19236
   182
wenzelm@41447
   183
            (* Gamma1, Gamma2 |- False *)
wenzelm@41447
   184
            val c_new =
wenzelm@41447
   185
              Thm.implies_elim
wenzelm@41447
   186
                (Thm.implies_elim res_thm (if hyp1_is_neg then c2' else c1'))
wenzelm@41447
   187
                (if hyp1_is_neg then c1' else c2')
webertj@20278
   188
wenzelm@41447
   189
            val _ =
wenzelm@55240
   190
              cond_tracing ctxt (fn () =>
wenzelm@55240
   191
                "Resulting clause: " ^ Display.string_of_thm ctxt c_new ^
wenzelm@55240
   192
                " (hyps: " ^
wenzelm@55240
   193
                ML_Syntax.print_list (Syntax.string_of_term ctxt) (Thm.hyps_of c_new) ^ ")")
wenzelm@55240
   194
wenzelm@41447
   195
            val _ = Unsynchronized.inc counter
wenzelm@41447
   196
          in
wenzelm@41447
   197
            (c_new, new_hyps)
wenzelm@41447
   198
          end
wenzelm@41447
   199
        in
wenzelm@41447
   200
          fold resolution cs c
wenzelm@41447
   201
        end;
webertj@17618
   202
webertj@17622
   203
(* ------------------------------------------------------------------------- *)
webertj@17809
   204
(* replay_proof: replays the resolution proof returned by the SAT solver;    *)
blanchet@56853
   205
(*      cf. SAT_Solver.proof for details of the proof format.  Updates the   *)
webertj@17809
   206
(*      'clauses' array with derived clauses, and returns the derived clause *)
webertj@17809
   207
(*      at index 'empty_id' (which should just be "False" if proof           *)
webertj@17809
   208
(*      reconstruction was successful, with the used clauses as hyps).       *)
webertj@20278
   209
(*      'atom_table' must contain an injective mapping from all atoms that   *)
webertj@20278
   210
(*      occur (as part of a literal) in 'clauses' to positive integers.      *)
webertj@17622
   211
(* ------------------------------------------------------------------------- *)
webertj@17622
   212
wenzelm@55236
   213
fun replay_proof ctxt atom_table clauses (clause_table, empty_id) =
wenzelm@41447
   214
  let
wenzelm@41447
   215
    fun index_of_literal chyp =
wenzelm@41447
   216
      (case (HOLogic.dest_Trueprop o Thm.term_of) chyp of
wenzelm@41447
   217
        (Const (@{const_name Not}, _) $ atom) =>
wenzelm@41447
   218
          SOME (~ (the (Termtab.lookup atom_table atom)))
wenzelm@41447
   219
      | atom => SOME (the (Termtab.lookup atom_table atom)))
wenzelm@41447
   220
      handle TERM _ => NONE;  (* 'chyp' is not a literal *)
webertj@20278
   221
wenzelm@41447
   222
    fun prove_clause id =
wenzelm@41447
   223
      (case Array.sub (clauses, id) of
wenzelm@41447
   224
        RAW_CLAUSE clause => clause
wenzelm@41447
   225
      | ORIG_CLAUSE thm =>
wenzelm@41447
   226
          (* convert the original clause *)
wenzelm@41447
   227
          let
wenzelm@55240
   228
            val _ = cond_tracing ctxt (fn () => "Using original clause #" ^ string_of_int id)
wenzelm@59498
   229
            val raw = CNF.clause2raw_thm ctxt thm
wenzelm@59058
   230
            val hyps = sort (lit_ord o apply2 fst) (map_filter (fn chyp =>
wenzelm@41447
   231
              Option.map (rpair chyp) (index_of_literal chyp)) (#hyps (Thm.crep_thm raw)))
wenzelm@41447
   232
            val clause = (raw, hyps)
wenzelm@41447
   233
            val _ = Array.update (clauses, id, RAW_CLAUSE clause)
wenzelm@41447
   234
          in
wenzelm@41447
   235
            clause
wenzelm@41447
   236
          end
wenzelm@41447
   237
      | NO_CLAUSE =>
wenzelm@41447
   238
          (* prove the clause, using information from 'clause_table' *)
wenzelm@41447
   239
          let
wenzelm@55240
   240
            val _ = cond_tracing ctxt (fn () => "Proving clause #" ^ string_of_int id ^ " ...")
wenzelm@41447
   241
            val ids = the (Inttab.lookup clause_table id)
wenzelm@55236
   242
            val clause = resolve_raw_clauses ctxt (map prove_clause ids)
wenzelm@41447
   243
            val _ = Array.update (clauses, id, RAW_CLAUSE clause)
wenzelm@41447
   244
            val _ =
wenzelm@55240
   245
              cond_tracing ctxt
wenzelm@55240
   246
                (fn () => "Replay chain successful; clause stored at #" ^ string_of_int id)
wenzelm@41447
   247
          in
wenzelm@41447
   248
            clause
wenzelm@41447
   249
          end)
webertj@17618
   250
wenzelm@41447
   251
    val _ = counter := 0
wenzelm@41447
   252
    val empty_clause = fst (prove_clause empty_id)
wenzelm@41447
   253
    val _ =
wenzelm@55240
   254
      cond_tracing ctxt (fn () =>
wenzelm@55240
   255
        "Proof reconstruction successful; " ^
wenzelm@55240
   256
        string_of_int (!counter) ^ " resolution step(s) total.")
wenzelm@41447
   257
  in
wenzelm@41447
   258
    empty_clause
wenzelm@41447
   259
  end;
webertj@17622
   260
webertj@20278
   261
(* ------------------------------------------------------------------------- *)
webertj@20278
   262
(* string_of_prop_formula: return a human-readable string representation of  *)
webertj@20278
   263
(*      a 'prop_formula' (just for tracing)                                  *)
webertj@20278
   264
(* ------------------------------------------------------------------------- *)
webertj@20278
   265
wenzelm@41471
   266
fun string_of_prop_formula Prop_Logic.True = "True"
wenzelm@41471
   267
  | string_of_prop_formula Prop_Logic.False = "False"
wenzelm@41471
   268
  | string_of_prop_formula (Prop_Logic.BoolVar i) = "x" ^ string_of_int i
wenzelm@41471
   269
  | string_of_prop_formula (Prop_Logic.Not fm) = "~" ^ string_of_prop_formula fm
wenzelm@41471
   270
  | string_of_prop_formula (Prop_Logic.Or (fm1, fm2)) =
wenzelm@41447
   271
      "(" ^ string_of_prop_formula fm1 ^ " v " ^ string_of_prop_formula fm2 ^ ")"
wenzelm@41471
   272
  | string_of_prop_formula (Prop_Logic.And (fm1, fm2)) =
wenzelm@41447
   273
      "(" ^ string_of_prop_formula fm1 ^ " & " ^ string_of_prop_formula fm2 ^ ")";
webertj@17622
   274
webertj@17622
   275
(* ------------------------------------------------------------------------- *)
webertj@21267
   276
(* rawsat_thm: run external SAT solver with the given clauses.  Reconstructs *)
webertj@21267
   277
(*      a proof from the resulting proof trace of the SAT solver.  The       *)
webertj@21267
   278
(*      theorem returned is just "False" (with some of the given clauses as  *)
webertj@21267
   279
(*      hyps).                                                               *)
webertj@21267
   280
(* ------------------------------------------------------------------------- *)
webertj@21267
   281
wenzelm@32432
   282
fun rawsat_thm ctxt clauses =
wenzelm@41447
   283
  let
wenzelm@41447
   284
    (* remove premises that equal "True" *)
wenzelm@41447
   285
    val clauses' = filter (fn clause =>
wenzelm@45740
   286
      (not_equal @{term True} o HOLogic.dest_Trueprop o Thm.term_of) clause
wenzelm@41447
   287
        handle TERM ("dest_Trueprop", _) => true) clauses
wenzelm@41447
   288
    (* remove non-clausal premises -- of course this shouldn't actually   *)
wenzelm@41447
   289
    (* remove anything as long as 'rawsat_tac' is only called after the   *)
wenzelm@41447
   290
    (* premises have been converted to clauses                            *)
wenzelm@41447
   291
    val clauses'' = filter (fn clause =>
wenzelm@55239
   292
      ((CNF.is_clause o HOLogic.dest_Trueprop o Thm.term_of) clause
wenzelm@41447
   293
        handle TERM ("dest_Trueprop", _) => false)
wenzelm@59352
   294
      orelse
wenzelm@59352
   295
       (if Context_Position.is_visible ctxt then
wenzelm@59352
   296
          warning ("Ignoring non-clausal premise " ^ Syntax.string_of_term ctxt (Thm.term_of clause))
wenzelm@59352
   297
        else (); false)) clauses'
wenzelm@41447
   298
    (* remove trivial clauses -- this is necessary because zChaff removes *)
wenzelm@41447
   299
    (* trivial clauses during preprocessing, and otherwise our clause     *)
wenzelm@41447
   300
    (* numbering would be off                                             *)
wenzelm@41447
   301
    val nontrivial_clauses =
wenzelm@55239
   302
      filter (not o CNF.clause_is_trivial o HOLogic.dest_Trueprop o Thm.term_of) clauses''
wenzelm@41447
   303
    (* sort clauses according to the term order -- an optimization,       *)
wenzelm@41447
   304
    (* useful because forming the union of hypotheses, as done by         *)
wenzelm@41447
   305
    (* Conjunction.intr_balanced and fold Thm.weaken below, is quadratic for *)
wenzelm@41447
   306
    (* terms sorted in descending order, while only linear for terms      *)
wenzelm@41447
   307
    (* sorted in ascending order                                          *)
wenzelm@59058
   308
    val sorted_clauses = sort (Term_Ord.fast_term_ord o apply2 Thm.term_of) nontrivial_clauses
wenzelm@41447
   309
    val _ =
wenzelm@55240
   310
      cond_tracing ctxt (fn () =>
wenzelm@55240
   311
        "Sorted non-trivial clauses:\n" ^
wenzelm@55240
   312
        cat_lines (map (Syntax.string_of_term ctxt o Thm.term_of) sorted_clauses))
wenzelm@41471
   313
    (* translate clauses from HOL terms to Prop_Logic.prop_formula *)
wenzelm@41447
   314
    val (fms, atom_table) =
wenzelm@41471
   315
      fold_map (Prop_Logic.prop_formula_of_term o HOLogic.dest_Trueprop o Thm.term_of)
wenzelm@41447
   316
        sorted_clauses Termtab.empty
wenzelm@41447
   317
    val _ =
wenzelm@55240
   318
      cond_tracing ctxt
wenzelm@55240
   319
        (fn () => "Invoking SAT solver on clauses:\n" ^ cat_lines (map string_of_prop_formula fms))
wenzelm@41471
   320
    val fm = Prop_Logic.all fms
wenzelm@41447
   321
    fun make_quick_and_dirty_thm () =
wenzelm@41447
   322
      let
wenzelm@41447
   323
        val _ =
wenzelm@55240
   324
          cond_tracing ctxt
wenzelm@55240
   325
            (fn () => "quick_and_dirty is set: proof reconstruction skipped, using oracle instead")
wenzelm@51550
   326
        val False_thm = Skip_Proof.make_thm_cterm @{cprop False}
wenzelm@41447
   327
      in
wenzelm@41447
   328
        (* 'fold Thm.weaken (rev sorted_clauses)' is linear, while 'fold    *)
wenzelm@41447
   329
        (* Thm.weaken sorted_clauses' would be quadratic, since we sorted   *)
wenzelm@41447
   330
        (* clauses in ascending order (which is linear for                  *)
wenzelm@41447
   331
        (* 'Conjunction.intr_balanced', used below)                         *)
wenzelm@41447
   332
        fold Thm.weaken (rev sorted_clauses) False_thm
wenzelm@41447
   333
      end
wenzelm@41447
   334
  in
wenzelm@41447
   335
    case
boehmes@56817
   336
      let
boehmes@56817
   337
        val the_solver = Config.get ctxt solver
boehmes@56817
   338
        val _ = cond_tracing ctxt (fn () => "Invoking solver " ^ the_solver)
blanchet@56853
   339
      in SAT_Solver.invoke_solver the_solver fm end
wenzelm@41447
   340
    of
blanchet@56853
   341
      SAT_Solver.UNSATISFIABLE (SOME (clause_table, empty_id)) =>
wenzelm@55240
   342
       (cond_tracing ctxt (fn () =>
wenzelm@55240
   343
          "Proof trace from SAT solver:\n" ^
wenzelm@55240
   344
          "clauses: " ^ ML_Syntax.print_list
wenzelm@55240
   345
            (ML_Syntax.print_pair ML_Syntax.print_int (ML_Syntax.print_list ML_Syntax.print_int))
wenzelm@55240
   346
            (Inttab.dest clause_table) ^ "\n" ^
wenzelm@55240
   347
          "empty clause: " ^ string_of_int empty_id);
wenzelm@52059
   348
        if Config.get ctxt quick_and_dirty then
wenzelm@41447
   349
          make_quick_and_dirty_thm ()
wenzelm@41447
   350
        else
wenzelm@41447
   351
          let
wenzelm@41447
   352
            (* optimization: convert the given clauses to "[c_1 && ... && c_n] |- c_i";  *)
wenzelm@41447
   353
            (*               this avoids accumulation of hypotheses during resolution    *)
wenzelm@41447
   354
            (* [c_1, ..., c_n] |- c_1 && ... && c_n *)
wenzelm@41447
   355
            val clauses_thm = Conjunction.intr_balanced (map Thm.assume sorted_clauses)
wenzelm@41447
   356
            (* [c_1 && ... && c_n] |- c_1 && ... && c_n *)
wenzelm@59582
   357
            val cnf_cterm = Thm.cprop_of clauses_thm
wenzelm@41447
   358
            val cnf_thm = Thm.assume cnf_cterm
wenzelm@41447
   359
            (* [[c_1 && ... && c_n] |- c_1, ..., [c_1 && ... && c_n] |- c_n] *)
wenzelm@41447
   360
            val cnf_clauses = Conjunction.elim_balanced (length sorted_clauses) cnf_thm
wenzelm@41447
   361
            (* initialize the clause array with the given clauses *)
wenzelm@52049
   362
            val max_idx = fst (the (Inttab.max clause_table))
wenzelm@41447
   363
            val clause_arr = Array.array (max_idx + 1, NO_CLAUSE)
wenzelm@41447
   364
            val _ =
wenzelm@41447
   365
              fold (fn thm => fn idx => (Array.update (clause_arr, idx, ORIG_CLAUSE thm); idx+1))
wenzelm@41447
   366
                cnf_clauses 0
wenzelm@41447
   367
            (* replay the proof to derive the empty clause *)
wenzelm@41447
   368
            (* [c_1 && ... && c_n] |- False *)
wenzelm@55236
   369
            val raw_thm = replay_proof ctxt atom_table clause_arr (clause_table, empty_id)
wenzelm@41447
   370
          in
wenzelm@41447
   371
            (* [c_1, ..., c_n] |- False *)
wenzelm@41447
   372
            Thm.implies_elim (Thm.implies_intr cnf_cterm raw_thm) clauses_thm
wenzelm@41447
   373
          end)
blanchet@56853
   374
    | SAT_Solver.UNSATISFIABLE NONE =>
wenzelm@52059
   375
        if Config.get ctxt quick_and_dirty then
wenzelm@59352
   376
         (if Context_Position.is_visible ctxt then
wenzelm@59352
   377
            warning "SAT solver claims the formula to be unsatisfiable, but did not provide a proof"
wenzelm@59352
   378
          else ();
wenzelm@41447
   379
          make_quick_and_dirty_thm ())
wenzelm@41447
   380
        else
wenzelm@41447
   381
          raise THM ("SAT solver claims the formula to be unsatisfiable, but did not provide a proof", 0, [])
blanchet@56853
   382
    | SAT_Solver.SATISFIABLE assignment =>
wenzelm@41447
   383
        let
wenzelm@41447
   384
          val msg =
wenzelm@41447
   385
            "SAT solver found a countermodel:\n" ^
wenzelm@41447
   386
            (commas o map (fn (term, idx) =>
wenzelm@41447
   387
                Syntax.string_of_term_global @{theory} term ^ ": " ^
wenzelm@41447
   388
                  (case assignment idx of NONE => "arbitrary"
wenzelm@41447
   389
                  | SOME true => "true" | SOME false => "false")))
wenzelm@41447
   390
              (Termtab.dest atom_table)
wenzelm@41447
   391
        in
wenzelm@41447
   392
          raise THM (msg, 0, [])
wenzelm@41447
   393
        end
blanchet@56853
   394
    | SAT_Solver.UNKNOWN =>
wenzelm@41447
   395
        raise THM ("SAT solver failed to decide the formula", 0, [])
wenzelm@41447
   396
  end;
webertj@17618
   397
webertj@17622
   398
(* ------------------------------------------------------------------------- *)
webertj@17622
   399
(* Tactics                                                                   *)
webertj@17622
   400
(* ------------------------------------------------------------------------- *)
webertj@17618
   401
webertj@17809
   402
(* ------------------------------------------------------------------------- *)
webertj@17809
   403
(* rawsat_tac: solves the i-th subgoal of the proof state; this subgoal      *)
webertj@17809
   404
(*      should be of the form                                                *)
webertj@17809
   405
(*        [| c1; c2; ...; ck |] ==> False                                    *)
webertj@17809
   406
(*      where each cj is a non-empty clause (i.e. a disjunction of literals) *)
webertj@17809
   407
(*      or "True"                                                            *)
webertj@17809
   408
(* ------------------------------------------------------------------------- *)
webertj@17809
   409
wenzelm@32232
   410
fun rawsat_tac ctxt i =
wenzelm@32432
   411
  Subgoal.FOCUS (fn {context = ctxt', prems, ...} =>
wenzelm@59582
   412
    resolve_tac ctxt' [rawsat_thm ctxt' (map Thm.cprop_of prems)] 1) ctxt i;
webertj@17618
   413
webertj@17809
   414
(* ------------------------------------------------------------------------- *)
webertj@17809
   415
(* pre_cnf_tac: converts the i-th subgoal                                    *)
webertj@17809
   416
(*        [| A1 ; ... ; An |] ==> B                                          *)
webertj@17809
   417
(*      to                                                                   *)
webertj@17809
   418
(*        [| A1; ... ; An ; ~B |] ==> False                                  *)
webertj@17809
   419
(*      (handling meta-logical connectives in B properly before negating),   *)
webertj@17809
   420
(*      then replaces meta-logical connectives in the premises (i.e. "==>",  *)
webertj@17809
   421
(*      "!!" and "==") by connectives of the HOL object-logic (i.e. by       *)
webertj@19553
   422
(*      "-->", "!", and "="), then performs beta-eta-normalization on the    *)
webertj@19553
   423
(*      subgoal                                                              *)
webertj@17809
   424
(* ------------------------------------------------------------------------- *)
webertj@17809
   425
wenzelm@54742
   426
fun pre_cnf_tac ctxt =
wenzelm@59498
   427
  resolve_tac ctxt @{thms ccontr} THEN'
wenzelm@54742
   428
  Object_Logic.atomize_prems_tac ctxt THEN'
wenzelm@41447
   429
  CONVERSION Drule.beta_eta_conversion;
webertj@17809
   430
webertj@17809
   431
(* ------------------------------------------------------------------------- *)
webertj@17809
   432
(* cnfsat_tac: checks if the empty clause "False" occurs among the premises; *)
webertj@17809
   433
(*      if not, eliminates conjunctions (i.e. each clause of the CNF formula *)
webertj@17809
   434
(*      becomes a separate premise), then applies 'rawsat_tac' to solve the  *)
webertj@17809
   435
(*      subgoal                                                              *)
webertj@17809
   436
(* ------------------------------------------------------------------------- *)
webertj@17697
   437
wenzelm@32232
   438
fun cnfsat_tac ctxt i =
wenzelm@59498
   439
  (eresolve_tac  ctxt [FalseE] i) ORELSE
wenzelm@59498
   440
  (REPEAT_DETERM (eresolve_tac ctxt [conjE] i) THEN rawsat_tac ctxt i);
webertj@17618
   441
webertj@17809
   442
(* ------------------------------------------------------------------------- *)
webertj@17809
   443
(* cnfxsat_tac: checks if the empty clause "False" occurs among the          *)
webertj@17809
   444
(*      premises; if not, eliminates conjunctions (i.e. each clause of the   *)
webertj@17809
   445
(*      CNF formula becomes a separate premise) and existential quantifiers, *)
webertj@17809
   446
(*      then applies 'rawsat_tac' to solve the subgoal                       *)
webertj@17809
   447
(* ------------------------------------------------------------------------- *)
webertj@17809
   448
wenzelm@32232
   449
fun cnfxsat_tac ctxt i =
wenzelm@59498
   450
  (eresolve_tac ctxt [FalseE] i) ORELSE
wenzelm@59498
   451
    (REPEAT_DETERM (eresolve_tac ctxt [conjE] i ORELSE eresolve_tac ctxt [exE] i) THEN
wenzelm@59498
   452
      rawsat_tac ctxt i);
webertj@17618
   453
webertj@17809
   454
(* ------------------------------------------------------------------------- *)
webertj@17809
   455
(* sat_tac: tactic for calling an external SAT solver, taking as input an    *)
webertj@17809
   456
(*      arbitrary formula.  The input is translated to CNF, possibly causing *)
webertj@17809
   457
(*      an exponential blowup.                                               *)
webertj@17809
   458
(* ------------------------------------------------------------------------- *)
webertj@17809
   459
wenzelm@32232
   460
fun sat_tac ctxt i =
wenzelm@55239
   461
  pre_cnf_tac ctxt i THEN CNF.cnf_rewrite_tac ctxt i THEN cnfsat_tac ctxt i;
webertj@17809
   462
webertj@17809
   463
(* ------------------------------------------------------------------------- *)
webertj@17809
   464
(* satx_tac: tactic for calling an external SAT solver, taking as input an   *)
webertj@17809
   465
(*      arbitrary formula.  The input is translated to CNF, possibly         *)
webertj@17809
   466
(*      introducing new literals.                                            *)
webertj@17809
   467
(* ------------------------------------------------------------------------- *)
webertj@17809
   468
wenzelm@32232
   469
fun satx_tac ctxt i =
wenzelm@55239
   470
  pre_cnf_tac ctxt i THEN CNF.cnfx_rewrite_tac ctxt i THEN cnfxsat_tac ctxt i;
webertj@17618
   471
wenzelm@23533
   472
end;