# HG changeset patch
# User webertj
# Date 1152231172 -7200
# Node ID 2b8dbb637792f26f692d12afa3dcbc220d70a8c4
# Parent  2087e56345983ca7691945bc31470566a2317295
added support for MiniSat 1.14

diff -r 2087e5634598 -r 2b8dbb637792 etc/settings
--- 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
diff -r 2087e5634598 -r 2b8dbb637792 src/HOL/Tools/sat_solver.ML
--- 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)                      *)
 (* ------------------------------------------------------------------------- *)