--- a/etc/settings Thu Jul 06 23:36:40 2006 +0200
+++ b/etc/settings Fri Jul 07 02:12:52 2006 +0200
@@ -197,6 +197,9 @@
# Einhoven model checker
#EINDHOVEN_HOME=/usr/local/bin
+# MiniSat 1.14 (SAT Solver, cf. Isabelle/src/HOL/Tools/sat_solver.ML)
+#MINISAT_HOME=/usr/local/bin
+
# zChaff (SAT Solver, cf. Isabelle/src/HOL/Tools/sat_solver.ML)
#ZCHAFF_HOME=/usr/local/bin
#ZCHAFF_VERSION=2004.5.13
--- a/src/HOL/Tools/sat_solver.ML Thu Jul 06 23:36:40 2006 +0200
+++ b/src/HOL/Tools/sat_solver.ML Fri Jul 07 02:12:52 2006 +0200
@@ -251,10 +251,10 @@
fun parse_lines [] =
UNKNOWN
| parse_lines (line::lines) =
- if is_substring satisfiable line then
+ if is_substring unsatisfiable line then
+ UNSATISFIABLE NONE
+ else if is_substring satisfiable line then
SATISFIABLE (parse_assignment [] lines)
- else if is_substring unsatisfiable line then
- UNSATISFIABLE NONE
else
parse_lines lines
in
@@ -541,6 +541,32 @@
end;
(* ------------------------------------------------------------------------- *)
+(* MiniSat 1.14 *)
+(* (http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/) *)
+(* ------------------------------------------------------------------------- *)
+
+let
+ fun minisat fm =
+ let
+ val _ = if (getenv "MINISAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
+ val inpath = File.tmp_path (Path.unpack "isabelle.cnf")
+ val outpath = File.tmp_path (Path.unpack "result")
+ val cmd = (getenv "MINISAT_HOME") ^ "/minisat " ^ (Path.pack inpath) ^ " -r " ^ (Path.pack outpath) ^ " > /dev/null"
+ fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
+ fun readfn () = SatSolver.read_std_result_file outpath ("SAT", "", "UNSAT")
+ val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.pack inpath)) else ()
+ val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.pack outpath)) else ()
+ val result = SatSolver.make_external_solver cmd writefn readfn fm
+ val _ = try File.rm inpath
+ val _ = try File.rm outpath
+ in
+ result
+ end
+in
+ SatSolver.add_solver ("minisat", minisat)
+end;
+
+(* ------------------------------------------------------------------------- *)
(* zChaff (http://www.princeton.edu/~chaff/zchaff.html) *)
(* ------------------------------------------------------------------------- *)