src/HOL/Tools/sat_funcs.ML
author huffman
Fri Mar 30 12:32:35 2012 +0200 (2012-03-30)
changeset 47220 52426c62b5d0
parent 45740 132a3e1c0fe5
child 51550 cec08df2c030
permissions -rw-r--r--
replace lemmas eval_nat_numeral with a simpler reformulation
     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) = int_ord (abs i, abs j);
    82 
    83 (* ------------------------------------------------------------------------- *)
    84 (* CLAUSE: during proof reconstruction, three kinds of clauses are           *)
    85 (*      distinguished:                                                       *)
    86 (*      1. NO_CLAUSE: clause not proved (yet)                                *)
    87 (*      2. ORIG_CLAUSE: a clause as it occurs in the original problem        *)
    88 (*      3. RAW_CLAUSE: a raw clause, with additional precomputed information *)
    89 (*         (a mapping from int's to its literals) for faster proof           *)
    90 (*         reconstruction                                                    *)
    91 (* ------------------------------------------------------------------------- *)
    92 
    93 datatype CLAUSE =
    94     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 fun resolve_raw_clauses [] =
   121       raise THM ("Proof reconstruction failed (empty list of resolvents)!", 0, [])
   122   | resolve_raw_clauses (c::cs) =
   123       let
   124         (* merges two sorted lists wrt. 'lit_ord', suppressing duplicates *)
   125         fun merge xs [] = xs
   126           | merge [] ys = ys
   127           | merge (x :: xs) (y :: ys) =
   128               (case (lit_ord o pairself fst) (x, y) of
   129                 LESS => x :: merge xs (y :: ys)
   130               | EQUAL => x :: merge xs ys
   131               | GREATER => y :: merge (x :: xs) ys)
   132 
   133         (* find out which two hyps are used in the resolution *)
   134         fun find_res_hyps ([], _) _ =
   135               raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, [])
   136           | find_res_hyps (_, []) _ =
   137               raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, [])
   138           | find_res_hyps (h1 :: hyps1, h2 :: hyps2) acc =
   139               (case (lit_ord o pairself fst) (h1, h2) of
   140                 LESS  => find_res_hyps (hyps1, h2 :: hyps2) (h1 :: acc)
   141               | EQUAL =>
   142                   let
   143                     val (i1, chyp1) = h1
   144                     val (i2, chyp2) = h2
   145                   in
   146                     if i1 = ~ i2 then
   147                       (i1 < 0, chyp1, chyp2, rev acc @ merge hyps1 hyps2)
   148                     else (* i1 = i2 *)
   149                       find_res_hyps (hyps1, hyps2) (h1 :: acc)
   150                   end
   151           | GREATER => find_res_hyps (h1 :: hyps1, hyps2) (h2 :: acc))
   152 
   153         fun resolution (c1, hyps1) (c2, hyps2) =
   154           let
   155             val _ =
   156               if ! trace_sat then  (* FIXME !? *)
   157                 tracing ("Resolving clause: " ^ Display.string_of_thm_without_context c1 ^
   158                   " (hyps: " ^ ML_Syntax.print_list
   159                     (Syntax.string_of_term_global (theory_of_thm c1)) (Thm.hyps_of c1)
   160                   ^ ")\nwith clause: " ^ Display.string_of_thm_without_context c2 ^
   161                   " (hyps: " ^ ML_Syntax.print_list
   162                     (Syntax.string_of_term_global (theory_of_thm c2)) (Thm.hyps_of c2) ^ ")")
   163               else ()
   164 
   165             (* the two literals used for resolution *)
   166             val (hyp1_is_neg, hyp1, hyp2, new_hyps) = find_res_hyps (hyps1, hyps2) []
   167 
   168             val c1' = Thm.implies_intr hyp1 c1  (* Gamma1 |- hyp1 ==> False *)
   169             val c2' = Thm.implies_intr hyp2 c2  (* Gamma2 |- hyp2 ==> False *)
   170 
   171             val res_thm =  (* |- (lit ==> False) ==> (~lit ==> False) ==> False *)
   172               let
   173                 val cLit =
   174                   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 =
   186               Thm.implies_elim
   187                 (Thm.implies_elim res_thm (if hyp1_is_neg then c2' else c1'))
   188                 (if hyp1_is_neg then c1' else c2')
   189 
   190             val _ =
   191               if !trace_sat then
   192                 tracing ("Resulting clause: " ^ Display.string_of_thm_without_context c_new ^
   193                   " (hyps: " ^ ML_Syntax.print_list
   194                       (Syntax.string_of_term_global (theory_of_thm c_new)) (Thm.hyps_of c_new) ^ ")")
   195               else ()
   196             val _ = Unsynchronized.inc counter
   197           in
   198             (c_new, new_hyps)
   199           end
   200         in
   201           fold resolution cs c
   202         end;
   203 
   204 (* ------------------------------------------------------------------------- *)
   205 (* replay_proof: replays the resolution proof returned by the SAT solver;    *)
   206 (*      cf. SatSolver.proof for details of the proof format.  Updates the    *)
   207 (*      'clauses' array with derived clauses, and returns the derived clause *)
   208 (*      at index 'empty_id' (which should just be "False" if proof           *)
   209 (*      reconstruction was successful, with the used clauses as hyps).       *)
   210 (*      'atom_table' must contain an injective mapping from all atoms that   *)
   211 (*      occur (as part of a literal) in 'clauses' to positive integers.      *)
   212 (* ------------------------------------------------------------------------- *)
   213 
   214 fun replay_proof atom_table clauses (clause_table, empty_id) =
   215   let
   216     fun index_of_literal chyp =
   217       (case (HOLogic.dest_Trueprop o Thm.term_of) chyp of
   218         (Const (@{const_name Not}, _) $ atom) =>
   219           SOME (~ (the (Termtab.lookup atom_table atom)))
   220       | atom => SOME (the (Termtab.lookup atom_table atom)))
   221       handle TERM _ => NONE;  (* 'chyp' is not a literal *)
   222 
   223     fun prove_clause id =
   224       (case Array.sub (clauses, id) of
   225         RAW_CLAUSE clause => clause
   226       | ORIG_CLAUSE thm =>
   227           (* convert the original clause *)
   228           let
   229             val _ =
   230               if !trace_sat then tracing ("Using original clause #" ^ string_of_int id) else ()
   231             val raw = cnf.clause2raw_thm thm
   232             val hyps = sort (lit_ord o pairself fst) (map_filter (fn chyp =>
   233               Option.map (rpair chyp) (index_of_literal chyp)) (#hyps (Thm.crep_thm raw)))
   234             val clause = (raw, hyps)
   235             val _ = Array.update (clauses, id, RAW_CLAUSE clause)
   236           in
   237             clause
   238           end
   239       | NO_CLAUSE =>
   240           (* prove the clause, using information from 'clause_table' *)
   241           let
   242             val _ =
   243               if !trace_sat then tracing ("Proving clause #" ^ string_of_int id ^ " ...") else ()
   244             val ids = the (Inttab.lookup clause_table id)
   245             val clause = resolve_raw_clauses (map prove_clause ids)
   246             val _ = Array.update (clauses, id, RAW_CLAUSE clause)
   247             val _ =
   248               if !trace_sat then
   249                 tracing ("Replay chain successful; clause stored at #" ^ string_of_int id)
   250               else ()
   251           in
   252             clause
   253           end)
   254 
   255     val _ = counter := 0
   256     val empty_clause = fst (prove_clause empty_id)
   257     val _ =
   258       if !trace_sat then
   259         tracing ("Proof reconstruction successful; " ^
   260           string_of_int (!counter) ^ " resolution step(s) total.")
   261       else ()
   262   in
   263     empty_clause
   264   end;
   265 
   266 (* ------------------------------------------------------------------------- *)
   267 (* string_of_prop_formula: return a human-readable string representation of  *)
   268 (*      a 'prop_formula' (just for tracing)                                  *)
   269 (* ------------------------------------------------------------------------- *)
   270 
   271 fun string_of_prop_formula Prop_Logic.True = "True"
   272   | string_of_prop_formula Prop_Logic.False = "False"
   273   | string_of_prop_formula (Prop_Logic.BoolVar i) = "x" ^ string_of_int i
   274   | string_of_prop_formula (Prop_Logic.Not fm) = "~" ^ string_of_prop_formula fm
   275   | string_of_prop_formula (Prop_Logic.Or (fm1, fm2)) =
   276       "(" ^ string_of_prop_formula fm1 ^ " v " ^ string_of_prop_formula fm2 ^ ")"
   277   | string_of_prop_formula (Prop_Logic.And (fm1, fm2)) =
   278       "(" ^ string_of_prop_formula fm1 ^ " & " ^ string_of_prop_formula fm2 ^ ")";
   279 
   280 (* ------------------------------------------------------------------------- *)
   281 (* rawsat_thm: run external SAT solver with the given clauses.  Reconstructs *)
   282 (*      a proof from the resulting proof trace of the SAT solver.  The       *)
   283 (*      theorem returned is just "False" (with some of the given clauses as  *)
   284 (*      hyps).                                                               *)
   285 (* ------------------------------------------------------------------------- *)
   286 
   287 fun rawsat_thm ctxt clauses =
   288   let
   289     (* remove premises that equal "True" *)
   290     val clauses' = filter (fn clause =>
   291       (not_equal @{term True} o HOLogic.dest_Trueprop o Thm.term_of) clause
   292         handle TERM ("dest_Trueprop", _) => true) clauses
   293     (* remove non-clausal premises -- of course this shouldn't actually   *)
   294     (* remove anything as long as 'rawsat_tac' is only called after the   *)
   295     (* premises have been converted to clauses                            *)
   296     val clauses'' = filter (fn clause =>
   297       ((cnf.is_clause o HOLogic.dest_Trueprop o Thm.term_of) clause
   298         handle TERM ("dest_Trueprop", _) => false)
   299       orelse (
   300         warning ("Ignoring non-clausal premise " ^ Syntax.string_of_term ctxt (Thm.term_of clause));
   301         false)) clauses'
   302     (* remove trivial clauses -- this is necessary because zChaff removes *)
   303     (* trivial clauses during preprocessing, and otherwise our clause     *)
   304     (* numbering would be off                                             *)
   305     val nontrivial_clauses =
   306       filter (not o cnf.clause_is_trivial o HOLogic.dest_Trueprop o Thm.term_of) clauses''
   307     (* sort clauses according to the term order -- an optimization,       *)
   308     (* useful because forming the union of hypotheses, as done by         *)
   309     (* Conjunction.intr_balanced and fold Thm.weaken below, is quadratic for *)
   310     (* terms sorted in descending order, while only linear for terms      *)
   311     (* sorted in ascending order                                          *)
   312     val sorted_clauses = sort (Term_Ord.fast_term_ord o pairself Thm.term_of) nontrivial_clauses
   313     val _ =
   314       if !trace_sat then
   315         tracing ("Sorted non-trivial clauses:\n" ^
   316           cat_lines (map (Syntax.string_of_term ctxt o Thm.term_of) sorted_clauses))
   317       else ()
   318     (* translate clauses from HOL terms to Prop_Logic.prop_formula *)
   319     val (fms, atom_table) =
   320       fold_map (Prop_Logic.prop_formula_of_term o HOLogic.dest_Trueprop o Thm.term_of)
   321         sorted_clauses Termtab.empty
   322     val _ =
   323       if !trace_sat then
   324         tracing ("Invoking SAT solver on clauses:\n" ^ cat_lines (map string_of_prop_formula fms))
   325       else ()
   326     val fm = Prop_Logic.all fms
   327     (* unit -> Thm.thm *)
   328     fun make_quick_and_dirty_thm () =
   329       let
   330         val _ =
   331           if !trace_sat then
   332             tracing "'quick_and_dirty' is set: proof reconstruction skipped, using oracle instead."
   333           else ()
   334         val False_thm = Skip_Proof.make_thm @{theory} (HOLogic.Trueprop $ @{term False})
   335       in
   336         (* 'fold Thm.weaken (rev sorted_clauses)' is linear, while 'fold    *)
   337         (* Thm.weaken sorted_clauses' would be quadratic, since we sorted   *)
   338         (* clauses in ascending order (which is linear for                  *)
   339         (* 'Conjunction.intr_balanced', used below)                         *)
   340         fold Thm.weaken (rev sorted_clauses) False_thm
   341       end
   342   in
   343     case
   344       let val the_solver = ! solver
   345       in (tracing ("Invoking solver " ^ the_solver); SatSolver.invoke_solver the_solver fm) end
   346     of
   347       SatSolver.UNSATISFIABLE (SOME (clause_table, empty_id)) =>
   348        (if !trace_sat then
   349           tracing ("Proof trace from SAT solver:\n" ^
   350             "clauses: " ^ ML_Syntax.print_list
   351               (ML_Syntax.print_pair ML_Syntax.print_int (ML_Syntax.print_list ML_Syntax.print_int))
   352               (Inttab.dest clause_table) ^ "\n" ^
   353             "empty clause: " ^ string_of_int empty_id)
   354         else ();
   355         if !quick_and_dirty then
   356           make_quick_and_dirty_thm ()
   357         else
   358           let
   359             (* optimization: convert the given clauses to "[c_1 && ... && c_n] |- c_i";  *)
   360             (*               this avoids accumulation of hypotheses during resolution    *)
   361             (* [c_1, ..., c_n] |- c_1 && ... && c_n *)
   362             val clauses_thm = Conjunction.intr_balanced (map Thm.assume sorted_clauses)
   363             (* [c_1 && ... && c_n] |- c_1 && ... && c_n *)
   364             val cnf_cterm = cprop_of clauses_thm
   365             val cnf_thm = Thm.assume cnf_cterm
   366             (* [[c_1 && ... && c_n] |- c_1, ..., [c_1 && ... && c_n] |- c_n] *)
   367             val cnf_clauses = Conjunction.elim_balanced (length sorted_clauses) cnf_thm
   368             (* initialize the clause array with the given clauses *)
   369             val max_idx = the (Inttab.max_key clause_table)
   370             val clause_arr = Array.array (max_idx + 1, NO_CLAUSE)
   371             val _ =
   372               fold (fn thm => fn idx => (Array.update (clause_arr, idx, ORIG_CLAUSE thm); idx+1))
   373                 cnf_clauses 0
   374             (* replay the proof to derive the empty clause *)
   375             (* [c_1 && ... && c_n] |- False *)
   376             val raw_thm = replay_proof atom_table clause_arr (clause_table, empty_id)
   377           in
   378             (* [c_1, ..., c_n] |- False *)
   379             Thm.implies_elim (Thm.implies_intr cnf_cterm raw_thm) clauses_thm
   380           end)
   381     | SatSolver.UNSATISFIABLE NONE =>
   382         if !quick_and_dirty then
   383          (warning "SAT solver claims the formula to be unsatisfiable, but did not provide a proof";
   384           make_quick_and_dirty_thm ())
   385         else
   386           raise THM ("SAT solver claims the formula to be unsatisfiable, but did not provide a proof", 0, [])
   387     | SatSolver.SATISFIABLE assignment =>
   388         let
   389           val msg =
   390             "SAT solver found a countermodel:\n" ^
   391             (commas o map (fn (term, idx) =>
   392                 Syntax.string_of_term_global @{theory} term ^ ": " ^
   393                   (case assignment idx of NONE => "arbitrary"
   394                   | SOME true => "true" | SOME false => "false")))
   395               (Termtab.dest atom_table)
   396         in
   397           raise THM (msg, 0, [])
   398         end
   399     | SatSolver.UNKNOWN =>
   400         raise THM ("SAT solver failed to decide the formula", 0, [])
   401   end;
   402 
   403 (* ------------------------------------------------------------------------- *)
   404 (* Tactics                                                                   *)
   405 (* ------------------------------------------------------------------------- *)
   406 
   407 (* ------------------------------------------------------------------------- *)
   408 (* rawsat_tac: solves the i-th subgoal of the proof state; this subgoal      *)
   409 (*      should be of the form                                                *)
   410 (*        [| c1; c2; ...; ck |] ==> False                                    *)
   411 (*      where each cj is a non-empty clause (i.e. a disjunction of literals) *)
   412 (*      or "True"                                                            *)
   413 (* ------------------------------------------------------------------------- *)
   414 
   415 fun rawsat_tac ctxt i =
   416   Subgoal.FOCUS (fn {context = ctxt', prems, ...} =>
   417     rtac (rawsat_thm ctxt' (map cprop_of prems)) 1) ctxt i;
   418 
   419 (* ------------------------------------------------------------------------- *)
   420 (* pre_cnf_tac: converts the i-th subgoal                                    *)
   421 (*        [| A1 ; ... ; An |] ==> B                                          *)
   422 (*      to                                                                   *)
   423 (*        [| A1; ... ; An ; ~B |] ==> False                                  *)
   424 (*      (handling meta-logical connectives in B properly before negating),   *)
   425 (*      then replaces meta-logical connectives in the premises (i.e. "==>",  *)
   426 (*      "!!" and "==") by connectives of the HOL object-logic (i.e. by       *)
   427 (*      "-->", "!", and "="), then performs beta-eta-normalization on the    *)
   428 (*      subgoal                                                              *)
   429 (* ------------------------------------------------------------------------- *)
   430 
   431 val pre_cnf_tac =
   432   rtac ccontr THEN'
   433   Object_Logic.atomize_prems_tac THEN'
   434   CONVERSION Drule.beta_eta_conversion;
   435 
   436 (* ------------------------------------------------------------------------- *)
   437 (* cnfsat_tac: checks if the empty clause "False" occurs among the premises; *)
   438 (*      if not, eliminates conjunctions (i.e. each clause of the CNF formula *)
   439 (*      becomes a separate premise), then applies 'rawsat_tac' to solve the  *)
   440 (*      subgoal                                                              *)
   441 (* ------------------------------------------------------------------------- *)
   442 
   443 fun cnfsat_tac ctxt i =
   444   (etac FalseE i) ORELSE (REPEAT_DETERM (etac conjE i) THEN rawsat_tac ctxt i);
   445 
   446 (* ------------------------------------------------------------------------- *)
   447 (* cnfxsat_tac: checks if the empty clause "False" occurs among the          *)
   448 (*      premises; if not, eliminates conjunctions (i.e. each clause of the   *)
   449 (*      CNF formula becomes a separate premise) and existential quantifiers, *)
   450 (*      then applies 'rawsat_tac' to solve the subgoal                       *)
   451 (* ------------------------------------------------------------------------- *)
   452 
   453 fun cnfxsat_tac ctxt i =
   454   (etac FalseE i) ORELSE
   455     (REPEAT_DETERM (etac conjE i ORELSE etac exE i) THEN rawsat_tac ctxt i);
   456 
   457 (* ------------------------------------------------------------------------- *)
   458 (* sat_tac: tactic for calling an external SAT solver, taking as input an    *)
   459 (*      arbitrary formula.  The input is translated to CNF, possibly causing *)
   460 (*      an exponential blowup.                                               *)
   461 (* ------------------------------------------------------------------------- *)
   462 
   463 fun sat_tac ctxt i =
   464   pre_cnf_tac i THEN cnf.cnf_rewrite_tac ctxt i THEN cnfsat_tac ctxt i;
   465 
   466 (* ------------------------------------------------------------------------- *)
   467 (* satx_tac: tactic for calling an external SAT solver, taking as input an   *)
   468 (*      arbitrary formula.  The input is translated to CNF, possibly         *)
   469 (*      introducing new literals.                                            *)
   470 (* ------------------------------------------------------------------------- *)
   471 
   472 fun satx_tac ctxt i =
   473   pre_cnf_tac i THEN cnf.cnfx_rewrite_tac ctxt i THEN cnfxsat_tac ctxt i;
   474 
   475 end;