src/HOL/Tools/sat_solver.ML

 Interface to external SAT solvers, and (simple) built-in SAT solvers.
 *)
 
 signature SAT_SOLVER =
 sig
-	type solver  (* PropLogic.prop_formula -> (int -> bool) option option *)
-
-	(* external SAT solvers *)
+	exception NOT_CONFIGURED
+
+	type assignment = int -> bool option
+	datatype result = SATISFIABLE of assignment
+	                | UNSATISFIABLE
+	                | UNKNOWN
+	type solver     = PropLogic.prop_formula -> result
+
+	(* auxiliary functions to create external SAT solvers *)
 	val write_dimacs_cnf_file : Path.T -> PropLogic.prop_formula -> unit
 	val write_dimacs_sat_file : Path.T -> PropLogic.prop_formula -> unit
-	val parse_std_result_file : Path.T -> string -> (int -> bool) option
-	val make_external_solver  : string -> (PropLogic.prop_formula -> unit) -> (unit -> (int -> bool) option)
-			-> PropLogic.prop_formula -> (int -> bool) option
+	val parse_std_result_file : Path.T -> string * string * string -> result
+	val make_external_solver  : string -> (PropLogic.prop_formula -> unit) -> (unit -> result) -> solver
 
 	(* generic interface *)
 	val solvers       : (string * solver) list ref
 	val add_solver    : string * solver -> unit
 	val invoke_solver : string -> solver  (* exception OPTION *)

 struct
 
 	open PropLogic;
 
 (* ------------------------------------------------------------------------- *)
-(* Type of SAT solvers: given a propositional formula, a satisfying          *)
+(* should be raised by an external SAT solver to indicate that the solver is *)
+(* not configured properly                                                   *)
+(* ------------------------------------------------------------------------- *)
+
+	exception NOT_CONFIGURED;
+
+(* ------------------------------------------------------------------------- *)
+(* type of partial (satisfying) assignments: 'a i = None' means that 'a' is  *)
+(*      a satisfying assigment regardless of the value of variable 'i'       *)
+(* ------------------------------------------------------------------------- *)
+
+	type assignment = int -> bool option;
+
+(* ------------------------------------------------------------------------- *)
+(* return type of SAT solvers: if the result is 'SATISFIABLE', a satisfying  *)
+(*      assignment must be returned as well                                  *)
+(* ------------------------------------------------------------------------- *)
+
+	datatype result = SATISFIABLE of assignment
+	                | UNSATISFIABLE
+	                | UNKNOWN;
+
+(* ------------------------------------------------------------------------- *)
+(* type of SAT solvers: given a propositional formula, a satisfying          *)
 (*      assignment may be returned                                           *)
-(*      - 'Some None' means that no satisfying assignment was found          *)
-(*      - 'None' means that the solver was not configured/installed properly *)
-(* ------------------------------------------------------------------------- *)
-
-	type solver = prop_formula -> (int -> bool) option option;
+(* ------------------------------------------------------------------------- *)
+
+	type solver = prop_formula -> result;
 
 (* ------------------------------------------------------------------------- *)
 (* write_dimacs_cnf_file: serializes a formula 'fm' of propositional logic   *)
 (*      to a file in DIMACS CNF format (see "Satisfiability Suggested        *)
 (*      Format", May 8 1993, Section 2.1)                                    *)
 (* Note: 'fm' must not contain a variable index less than 1.                 *)
-(* Note: 'fm' is converted into (definitional) CNF.                          *)
+(* Note: 'fm' must be given in CNF.                                          *)
 (* ------------------------------------------------------------------------- *)
 
 	(* Path.T -> prop_formula -> unit *)
 
 	fun write_dimacs_cnf_file path fm =

 			error "formula is not in CNF"
 		  | cnf_string (BoolVar i) =
 			(assert (i>=1) "formula contains a variable index less than 1";
 			string_of_int i)
 		  | cnf_string (Not fm) =
-			"-" ^ (cnf_string fm)
+			"-" ^ cnf_string fm
 		  | cnf_string (Or (fm1,fm2)) =
-			(cnf_string fm1) ^ " " ^ (cnf_string fm2)
+			cnf_string fm1 ^ " " ^ cnf_string fm2
 		  | cnf_string (And (fm1,fm2)) =
-			(cnf_string fm1) ^ " 0\n" ^ (cnf_string fm2)
+			cnf_string fm1 ^ " 0\n" ^ cnf_string fm2
 	in
 		File.write path
 			(let
-				val cnf               = (cnf_True_False_elim o defcnf) fm  (* conversion into def. CNF *)
-				val number_of_vars    = maxidx cnf
-				val number_of_clauses = cnf_number_of_clauses cnf
+				val fm'               = cnf_True_False_elim fm
+				val number_of_vars    = maxidx fm'
+				val number_of_clauses = cnf_number_of_clauses fm'
+				val cnfstring         = cnf_string fm'
 			in
 				"c This file was generated by SatSolver.write_dimacs_cnf_file\n" ^
 				"c (c) Tjark Weber\n" ^
-				"p cnf " ^ (string_of_int number_of_vars) ^ " " ^ (string_of_int number_of_clauses) ^ "\n" ^
-				(cnf_string cnf) ^ "\n"
+				"p cnf " ^ string_of_int number_of_vars ^ " " ^ string_of_int number_of_clauses ^ "\n" ^
+				cnfstring ^ " 0\n"
 			end)
 	end;
 
 (* ------------------------------------------------------------------------- *)
 (* write_dimacs_sat_file: serializes a formula 'fm' of propositional logic   *)

 			"+()"
 		  | sat_string (BoolVar i) =
 			(assert (i>=1) "formula contains a variable index less than 1";
 			string_of_int i)
 		  | sat_string (Not fm) =
-			"-(" ^ (sat_string fm) ^ ")"
+			"-(" ^ sat_string fm ^ ")"
 		  | sat_string (Or (fm1,fm2)) =
-			"+(" ^ (sat_string fm1) ^ " " ^ (sat_string fm2) ^ ")"
+			"+(" ^ sat_string fm1 ^ " " ^ sat_string fm2 ^ ")"
 		  | sat_string (And (fm1,fm2)) =
-			"*(" ^ (sat_string fm1) ^ " " ^ (sat_string fm2) ^ ")"
+			"*(" ^ sat_string fm1 ^ " " ^ sat_string fm2 ^ ")"
 	in
 		File.write path
 			(let
 				val number_of_vars = Int.max (maxidx fm, 1)
 			in
 				"c This file was generated by SatSolver.write_dimacs_sat_file\n" ^
 				"c (c) Tjark Weber\n" ^
-				"p sat " ^ (string_of_int number_of_vars) ^ "\n" ^
-				"(" ^ (sat_string fm) ^ ")\n"
+				"p sat " ^ string_of_int number_of_vars ^ "\n" ^
+				"(" ^ sat_string fm ^ ")\n"
 			end)
 	end;
 
 (* ------------------------------------------------------------------------- *)
 (* parse_std_result_file: scans a SAT solver's output file for a satisfying  *)
-(*      variable assignment.  Returns the assignment, or 'None' if the SAT   *)
-(*      solver did not find one.  The file format must be as follows:        *)
-(*      ,-----                                                               *)
-(*      | 0 or more lines not containing 'success'                           *)
-(*      | A line containing 'success' as a substring                         *)
-(*      | A line ASSIGNMENT containing integers, separated by " "            *)
-(*      | 0 or more lines                                                    *)
-(*      `-----                                                               *)
-(*      If variable i is contained in ASSIGNMENT, then i is interpreted as   *)
-(*      'true'.  If ~i is contained in ASSIGNMENT, then i is interpreted as  *)
-(*      'false'.                                                             *)
-(* ------------------------------------------------------------------------- *)
-
-	(* Path.T -> string -> (int -> bool) option *)
-
-	fun parse_std_result_file path success =
+(*      variable assignment.  Returns the assignment, or 'UNSATISFIABLE' if  *)
+(*      the file contains 'unsatisfiable', or 'UNKNOWN' if the file contains *)
+(*      neither 'satisfiable' nor 'unsatisfiable'.  Empty lines are ignored. *)
+(*      The assignment must be given in one or more lines immediately after  *)
+(*      the line that contains 'satisfiable'.  These lines must begin with   *)
+(*      'assignment_prefix'.  Variables must be separated by " ".  Non-      *)
+(*      integer strings are ignored.  If variable i is contained in the      *)
+(*      assignment, then i is interpreted as 'true'.  If ~i is contained in  *)
+(*      the assignment, then i is interpreted as 'false'.  Otherwise the     *)
+(*      value of i is taken to be unspecified.                               *)
+(* ------------------------------------------------------------------------- *)
+
+	(* Path.T -> string * string * string -> result *)
+
+	fun parse_std_result_file path (satisfiable, assignment_prefix, unsatisfiable) =
 	let
 		(* 'a option -> 'a Library.option *)
 		fun option (SOME a) =
 			Some a
 		  | option NONE =
 			None
 		(* string -> int list *)
 		fun int_list_from_string s =
 			mapfilter (option o Int.fromString) (space_explode " " s)
-		(* int list -> int -> bool *)
+		(* int list -> assignment *)
 		fun assignment_from_list [] i =
-			false  (* could be 'true' just as well; the SAT solver didn't provide a value for this variable *)
+			None  (* the SAT solver didn't provide a value for this variable *)
 		  | assignment_from_list (x::xs) i =
-			if x=i then true
-			else if x=(~i) then false
+			if x=i then (Some true)
+			else if x=(~i) then (Some false)
 			else assignment_from_list xs i
+		(* int list -> string list -> assignment *)
+		fun parse_assignment xs [] =
+			assignment_from_list xs
+		  | parse_assignment xs (line::lines) =
+			if String.isPrefix assignment_prefix line then
+				parse_assignment (xs @ int_list_from_string line) lines
+			else
+				assignment_from_list xs
 		(* string -> string -> bool *)
 		fun is_substring needle haystack =
 		let
 			val length1 = String.size needle
 			val length2 = String.size haystack

 				false
 			else if needle = String.substring (haystack, 0, length1) then
 				true
 			else is_substring needle (String.substring (haystack, 1, length2-1))
 		end
-		(* string list -> int list option *)
+		(* string list -> result *)
 		fun parse_lines [] =
-			None
+			UNKNOWN
 		  | parse_lines (line::lines) =
-			if is_substring success line then
-				(* the next line must be a list of integers *)
-				(Some o assignment_from_list o int_list_from_string o hd) lines
+			if is_substring satisfiable line then
+				SATISFIABLE (parse_assignment [] lines)
+			else if is_substring unsatisfiable line then
+				UNSATISFIABLE
 			else
 				parse_lines lines
 	in
-		(parse_lines o split_lines o File.read) path
+		(parse_lines o (filter (fn l => l <> "")) o split_lines o File.read) path
 	end;
 
 (* ------------------------------------------------------------------------- *)
 (* make_external_solver: call 'writefn', execute 'cmd', call 'readfn'        *)
 (* ------------------------------------------------------------------------- *)
 
-	(* string -> (prop_formula -> unit) -> (unit -> (int -> bool) option) -> prop_formula -> (int -> bool) option *)
+	(* string -> (PropLogic.prop_formula -> unit) -> (unit -> result) -> solver *)
 
 	fun make_external_solver cmd writefn readfn fm =
-		(writefn fm;
-		assert ((system cmd)=0) ("system command " ^ quote cmd ^ " failed (make sure the SAT solver is installed)");
-		readfn ());
+		(writefn fm; system cmd; readfn ());
 
 (* ------------------------------------------------------------------------- *)
 (* solvers: a (reference to a) table of all registered SAT solvers           *)
 (* ------------------------------------------------------------------------- *)
 

 				(* set the lowest bit that wasn't set before, keep the higher bits *)
 				Some (y::x::xs)
 		(* int list -> int -> bool *)
 		fun assignment_from_list xs i =
 			i mem xs
-		(* int list -> (int -> bool) option *)
+		(* int list -> SatSolver.result *)
 		fun solver_loop xs =
 			if PropLogic.eval (assignment_from_list xs) fm then
-				Some (assignment_from_list xs)
+				SatSolver.SATISFIABLE (Some o (assignment_from_list xs))
 			else
 				(case next_list xs indices of
 				  Some xs' => solver_loop xs'
-				| None     => None)
-	in
-		(* start with the "first" assignment (all variables are interpreted as 'False') *)
+				| None     => SatSolver.UNSATISFIABLE)
+	in
+		(* start with the "first" assignment (all variables are interpreted as 'false') *)
 		solver_loop []
 	end
 in
-	SatSolver.add_solver ("enumerate", Some o enum_solver)
+	SatSolver.add_solver ("enumerate", enum_solver)
 end;
 
 (* ------------------------------------------------------------------------- *)
 (* Internal SAT solver, available as 'SatSolver.invoke_solver "dpll"' -- a   *)
 (* simple implementation of the DPLL algorithm (cf. L. Zhang, S. Malik: "The *)

 	local
 		open PropLogic
 	in
 		fun dpll_solver fm =
 		let
-			(* We could use 'PropLogic.defcnf fm' instead of 'nnf fm', but that *)
-			(* sometimes introduces more boolean variables than we can handle   *)
-			(* efficiently.                                                     *)
+			(* We could use 'PropLogic.defcnf fm' instead of 'PropLogic.nnf fm' *)
+			(* but that sometimes introduces more boolean variables than we can *)
+			(* handle efficiently.                                              *)
 			val fm' = PropLogic.nnf fm
 			(* int list *)
 			val indices = PropLogic.indices fm'
 			(* int list -> int -> prop_formula *)
 			fun partial_var_eval []      i = BoolVar i

 						case dpll (x::xs') fm' of  (* passing fm' rather than fm should save some simplification work *)
 						  Some xs'' => Some xs''
 						| None      => dpll ((~x)::xs') fm'  (* now try interpreting 'x' as 'False' *)
 					end
 			end
-			(* int list -> int -> bool *)
+			(* int list -> assignment *)
 			fun assignment_from_list [] i =
-				false  (* could be 'true' just as well; the DPLL procedure didn't provide a value for this variable *)
+				None  (* the DPLL procedure didn't provide a value for this variable *)
 			  | assignment_from_list (x::xs) i =
-				if x=i then true
-				else if x=(~i) then false
+				if x=i then (Some true)
+				else if x=(~i) then (Some false)
 				else assignment_from_list xs i
 		in
 			(* initially, no variable is interpreted yet *)
-			apsome assignment_from_list (dpll [] fm')
+			case dpll [] fm' of
+			  Some assignment => SatSolver.SATISFIABLE (assignment_from_list assignment)
+			| None            => SatSolver.UNSATISFIABLE
 		end
 	end  (* local *)
 in
-	SatSolver.add_solver ("dpll", Some o dpll_solver)
+	SatSolver.add_solver ("dpll", dpll_solver)
 end;
 
 (* ------------------------------------------------------------------------- *)
 (* Internal SAT solver, available as 'SatSolver.invoke_solver "auto"': uses  *)
-(* the first installed solver (other than "auto" itself)                     *)
+(* all installed solvers (other than "auto" itself) until one returns either *)
+(* SATISFIABLE or UNSATISFIABLE                                              *)
 (* ------------------------------------------------------------------------- *)
 
 let
 	fun auto_solver fm =
-		get_first (fn (name,solver) =>
+	let
+		fun loop [] =
+			SatSolver.UNKNOWN
+		  | loop ((name, solver)::solvers) =
 			if name="auto" then
-				None
+				(* do not call solver "auto" from within "auto" *)
+				loop solvers
 			else
-				((if name="dpll" orelse name="enumerate" then
+			(
+				(if name="dpll" orelse name="enumerate" then
 					warning ("Using SAT solver " ^ quote name ^ "; for better performance, consider using an external solver.")
 				else
 					());
-				solver fm)) (rev (!SatSolver.solvers))
+				(* apply 'solver' to 'fm' *)
+				(case solver fm of
+				  SatSolver.SATISFIABLE a => SatSolver.SATISFIABLE a
+				| SatSolver.UNSATISFIABLE => SatSolver.UNSATISFIABLE
+				| SatSolver.UNKNOWN       => loop solvers)
+				handle SatSolver.NOT_CONFIGURED => loop solvers
+			)
+	in
+		loop (rev (!SatSolver.solvers))
+	end
 in
 	SatSolver.add_solver ("auto", auto_solver)
 end;
 
 (* ------------------------------------------------------------------------- *)
-(* ZChaff, Version 2003.12.04                                                *)
+(* ZChaff, Version 2003.12.04 (http://www.princeton.edu/~chaff/zchaff.html)  *)
 (* ------------------------------------------------------------------------- *)
 
 let
 	fun zchaff fm =
 	let
-		val inname     = "isabelle.cnf"
-		val outname    = "result"
-		val inpath     = File.tmp_path (Path.unpack inname)
-		val outpath    = File.tmp_path (Path.unpack outname)
+		val _          = if (getenv "ZCHAFF_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 "ZCHAFF_HOME") ^ "/zchaff " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath)
-		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath fm
-		fun readfn ()  = SatSolver.parse_std_result_file outpath "Verify Solution successful. Instance satisfiable"
+		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
+		fun readfn ()  = SatSolver.parse_std_result_file outpath ("Verify Solution successful. Instance satisfiable", "", "Instance unsatisfiable")
 		val _          = assert (not (File.exists inpath)) ("file " ^ quote (Path.pack inpath) ^ " exists, please delete (will not overwrite)")
 		val _          = assert (not (File.exists outpath)) ("file " ^ quote (Path.pack outpath) ^ " exists, please delete (will not overwrite)")
-		val assignment = SatSolver.make_external_solver cmd writefn readfn fm
+		val result     = SatSolver.make_external_solver cmd writefn readfn fm
 		val _          = (File.rm inpath handle _ => ())
 		val _          = (File.rm outpath handle _ => ())
 	in
-		assignment
+		result
 	end
 in
-		SatSolver.add_solver ("zchaff", (fn fm => if getenv "ZCHAFF_HOME" <> "" then Some (zchaff fm) else None))
+	SatSolver.add_solver ("zchaff", zchaff)
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* BerkMin 561 (http://eigold.tripod.com/BerkMin.html)                       *)
+(* ------------------------------------------------------------------------- *)
+
+let
+	fun berkmin fm =
+	let
+		val _          = if (getenv "BERKMIN_HOME") = "" orelse (getenv "BERKMIN_EXE") = "" 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 "BERKMIN_HOME") ^ "/" ^ (getenv "BERKMIN_EXE") ^ " " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath)
+		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
+		fun readfn ()  = SatSolver.parse_std_result_file outpath ("Satisfiable          !!", "solution =", "UNSATISFIABLE          !!")
+		val _          = assert (not (File.exists inpath)) ("file " ^ quote (Path.pack inpath) ^ " exists, please delete (will not overwrite)")
+		val _          = assert (not (File.exists outpath)) ("file " ^ quote (Path.pack outpath) ^ " exists, please delete (will not overwrite)")
+		val result     = SatSolver.make_external_solver cmd writefn readfn fm
+		val _          = (File.rm inpath handle _ => ())
+		val _          = (File.rm outpath handle _ => ())
+	in
+		result
+	end
+in
+	SatSolver.add_solver ("berkmin", berkmin)
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* Jerusat 1.3 (http://www.cs.tau.ac.il/~ale1/)                              *)
+(* ------------------------------------------------------------------------- *)
+
+let
+	fun jerusat fm =
+	let
+		val _          = if (getenv "JERUSAT_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 "JERUSAT_HOME") ^ "/Jerusat1.3 " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath)
+		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
+		fun readfn ()  = SatSolver.parse_std_result_file outpath ("s SATISFIABLE", "v ", "s UNSATISFIABLE")
+		val _          = assert (not (File.exists inpath)) ("file " ^ quote (Path.pack inpath) ^ " exists, please delete (will not overwrite)")
+		val _          = assert (not (File.exists outpath)) ("file " ^ quote (Path.pack outpath) ^ " exists, please delete (will not overwrite)")
+		val result     = SatSolver.make_external_solver cmd writefn readfn fm
+		val _          = (File.rm inpath handle _ => ())
+		val _          = (File.rm outpath handle _ => ())
+	in
+		result
+	end
+in
+	SatSolver.add_solver ("jerusat", jerusat)
 end;
 
 (* ------------------------------------------------------------------------- *)
 (* Add code for other SAT solvers below.                                     *)
 (* ------------------------------------------------------------------------- *)
 
 (*
 let
 	fun mysolver fm = ...
 in
-	SatSolver.add_solver ("myname", (fn fm => if mysolver_is_installed then Some (mysolver fm) else None));  -- register the solver
+	SatSolver.add_solver ("myname", (fn fm => if mysolver_is_configured then mysolver fm else raise SatSolver.NOT_CONFIGURED));  -- register the solver
 end;
 
 -- the solver is now available as SatSolver.invoke_solver "myname"
 *)