# HG changeset patch
# User webertj
# Date 1152288838 -7200
# Node ID 4293f932fe83f3aa318875b5615dccbe44c1755f
# Parent  73231d03a2ac1629d33ea50f15db1e5249bfede8
"solver" reference added to make the SAT solver configurable

diff -r 73231d03a2ac -r 4293f932fe83 src/HOL/Tools/sat_funcs.ML
--- a/src/HOL/Tools/sat_funcs.ML	Fri Jul 07 15:13:15 2006 +0200
+++ b/src/HOL/Tools/sat_funcs.ML	Fri Jul 07 18:13:58 2006 +0200
@@ -22,39 +22,49 @@
 
     This does not work for goals containing schematic variables!
 
-       The tactic produces a clause representation of the given goal
-       in DIMACS format and invokes a SAT solver, which should return
-       a proof consisting of a sequence of resolution steps, indicating
-       the two input clauses, and resulting in new clauses, leading to
-       the empty clause (i.e., False).  The tactic replays this proof
-       in Isabelle and thus solves the overall goal.
+      The tactic produces a clause representation of the given goal
+      in DIMACS format and invokes a SAT solver, which should return
+      a proof consisting of a sequence of resolution steps, indicating
+      the two input clauses, and resulting in new clauses, leading to
+      the empty clause (i.e. "False").  The tactic replays this proof
+      in Isabelle and thus solves the overall goal.
 
-   There are two SAT tactics available. They differ in the CNF transformation
-   used. The "sat_tac" uses naive CNF transformation to transform the theorem
-   to be proved before giving it to SAT solver. The naive transformation in
-   some worst case can lead to explonential blow up in formula size.
-   The other tactic, the "satx_tac" uses the "definitional CNF transformation"
-   which produces formula of linear size increase compared to the input formula.
-   This transformation introduces new variables. See also cnf_funcs.ML for
-   more comments.
+  There are two SAT tactics available.  They differ in the CNF transformation
+  used. "sat_tac" uses naive CNF transformation to transform the theorem to be
+  proved before giving it to the SAT solver.  The naive transformation in the
+  worst case can lead to an exponential blow up in formula size.  The other
+  tactic, "satx_tac", uses "definitional CNF transformation" which attempts to
+  produce a formula of linear size increase compared to the input formula, at
+  the cost of possibly introducing new variables.  See cnf_funcs.ML for more
+  comments on the CNF transformation.
 
- Notes for the current revision:
-   - The current version supports only zChaff prover.
-   - The environment variable ZCHAFF_HOME must be set to point to
-     the directory where zChaff executable resides
-   - The environment variable ZCHAFF_VERSION must be set according to
-     the version of zChaff used. Current supported version of zChaff:
+  The SAT solver to be used can be set via the "solver" reference.  See
+  sat_solvers.ML for possible values, and etc/settings for required (solver-
+  dependent) configuration settings.  To replay SAT proofs in Isabelle, you
+  must of course use a proof-producing SAT solver in the first place.
+
+  Notes for the current revision:
+   - Currently zChaff is the only proof-producing SAT solver that is supported.
+   - The environment variable ZCHAFF_HOME must be set to point to the directory
+     where the zChaff executable resides.
+   - The environment variable ZCHAFF_VERSION must be set according to the
+     version of zChaff used.  Current supported version of zChaff:
      zChaff version 2004.11.15
    - zChaff must have been compiled with proof generation enabled
      (#define VERIFY_ON).
+
+  Proofs are replayed only if "!quick_and_dirty" is false.  If
+  "!quick_and_dirty" is true, the theorem (in case the SAT solver claims its
+  negation to be unsatisfiable) is proved via an oracle.
 *)
 
 signature SAT =
 sig
-	val trace_sat : bool ref  (* print trace messages *)
+	val trace_sat : bool ref    (* print trace messages *)
+	val solver    : string ref  (* name of SAT solver to be used *)
+	val counter   : int ref     (* number of resolution steps during last proof replay *)
 	val sat_tac   : int -> Tactical.tactic
 	val satx_tac  : int -> Tactical.tactic
-	val counter   : int ref  (* number of resolution steps during last proof replay *)
 end
 
 functor SATFunc (structure cnf : CNF) : SAT =
@@ -62,6 +72,8 @@
 
 val trace_sat = ref false;
 
+val solver = ref "zchaff_with_proofs";
+
 val counter = ref 0;
 
 (* Thm.thm *)
@@ -273,7 +285,7 @@
 		SkipProof.make_thm (the_context ()) (HOLogic.Trueprop $ HOLogic.false_const)
 	)
 in
-	case SatSolver.invoke_solver "zchaff_with_proofs" fm of
+	case SatSolver.invoke_solver (!solver) fm of
 	  SatSolver.UNSATISFIABLE (SOME (clause_table, empty_id)) => (
 		if !trace_sat then
 			tracing ("Proof trace from SAT solver:\n" ^
@@ -397,4 +409,4 @@
 
 fun satx_tac i = pre_cnf_tac i THEN cnf.cnfx_rewrite_tac i THEN cnfxsat_tac i;
 
-end;  (* of structure *)
+end;  (* of structure SATFunc *)
diff -r 73231d03a2ac -r 4293f932fe83 src/HOL/ex/SAT_Examples.thy
--- a/src/HOL/ex/SAT_Examples.thy	Fri Jul 07 15:13:15 2006 +0200
+++ b/src/HOL/ex/SAT_Examples.thy	Fri Jul 07 18:13:58 2006 +0200
@@ -10,6 +10,7 @@
 
 begin
 
+(* ML {* sat.solver := "zchaff_with_proofs"; *} *)
 ML {* set sat.trace_sat; *}
 ML {* set quick_and_dirty; *}