src/HOL/Tools/sat_solver.ML

 	val parse_std_result_file : Path.T -> string * string * string -> result
 	val make_external_solver  : string -> (PropLogic.prop_formula -> unit) -> (unit -> result) -> solver
 
 	val read_dimacs_cnf_file : Path.T -> PropLogic.prop_formula
 
-	(* generic interface *)
+	(* generic solver interface *)
 	val solvers       : (string * solver) list ref
 	val add_solver    : string * solver -> unit
 	val invoke_solver : string -> solver  (* exception Option *)
 end;
 

 			  | sat_string_acc False acc =
 				"+()" :: acc
 			  | sat_string_acc (BoolVar i) acc =
 				(assert (i>=1) "formula contains a variable index less than 1";
 				string_of_int i :: acc)
+			  | sat_string_acc (Not (BoolVar i)) acc =
+				"-" :: sat_string_acc (BoolVar i) acc
 			  | sat_string_acc (Not fm) acc =
 				"-(" :: sat_string_acc fm (")" :: acc)
 			  | sat_string_acc (Or (fm1,fm2)) acc =
-				"+(" :: sat_string_acc fm1 (" " :: sat_string_acc fm2 (")" :: acc))
+				"+(" :: sat_string_acc_or fm1 (" " :: sat_string_acc_or fm2 (")" :: acc))
 			  | sat_string_acc (And (fm1,fm2)) acc =
-				"*(" :: sat_string_acc fm1 (" " :: sat_string_acc fm2 (")" :: acc))
+				"*(" :: sat_string_acc_and fm1 (" " :: sat_string_acc_and fm2 (")" :: acc))
+			(* optimization to make use of n-ary disjunction/conjunction *)
+			(* prop_formula -> string list -> string list *)
+			and sat_string_acc_or (Or (fm1,fm2)) acc =
+				sat_string_acc_or fm1 (" " :: sat_string_acc_or fm2 acc)
+			  | sat_string_acc_or fm acc =
+				sat_string_acc fm acc
+			(* prop_formula -> string list -> string list *)
+			and sat_string_acc_and (And (fm1,fm2)) acc =
+				sat_string_acc_and fm1 (" " :: sat_string_acc_and fm2 acc)
+			  | sat_string_acc_and fm acc =
+				sat_string_acc fm acc
 		in
 			concat (sat_string_acc fm [])
 		end
 	in
 		File.write path

 				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"
+				(*"(" ^*) sat_string fm ^ "\n" (*")\n"*)
 			end)
 	end;
 
 (* ------------------------------------------------------------------------- *)
 (* parse_std_result_file: scans a SAT solver's output file for a satisfying  *)

 		val _          = if (getenv "ZCHAFF_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
 		val _          = if (getenv "ZCHAFF_VERSION") <> "2004.5.13" andalso
 		                    (getenv "ZCHAFF_VERSION") <> "2004.11.15" then raise SatSolver.NOT_CONFIGURED else ()
 			(* both versions of zChaff appear to have the same interface, so we do *)
 			(* not actually need to distinguish between them in the following code *)
+		val satpath    = File.tmp_path (Path.unpack "isabelle.sat")
 		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 (PropLogic.defcnf fm)
+		fun writefn fm = (SatSolver.write_dimacs_sat_file satpath fm; SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm))
 		fun readfn ()  = SatSolver.parse_std_result_file outpath ("Instance Satisfiable", "", "Instance Unsatisfiable")
 		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