--- a/src/HOL/Tools/sat_solver.ML Wed Jul 20 17:01:20 2005 +0200
+++ b/src/HOL/Tools/sat_solver.ML Thu Jul 21 18:52:17 2005 +0200
@@ -24,7 +24,7 @@
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 *)
@@ -147,12 +147,25 @@
| 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
@@ -164,7 +177,7 @@
"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;
@@ -521,10 +534,11 @@
(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 ()