src/HOL/Tools/sat_funcs.ML
author wenzelm
Sun Mar 07 12:19:47 2010 +0100 (2010-03-07)
changeset 35625 9c818cab0dd0
parent 35408 b48ab741683b
child 38549 d0385f2764d8
permissions -rw-r--r--
modernized structure Object_Logic;
     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;