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