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