--- a/src/HOL/Tools/sat_solver.ML Tue Jul 26 12:13:35 2005 +0200
+++ b/src/HOL/Tools/sat_solver.ML Tue Jul 26 12:23:10 2005 +0200
@@ -1,7 +1,7 @@
(* Title: HOL/Tools/sat_solver.ML
ID: $Id$
Author: Tjark Weber
- Copyright 2004
+ Copyright 2004-2005
Interface to external SAT solvers, and (simple) built-in SAT solvers.
*)
@@ -414,7 +414,7 @@
in
fun dpll_solver fm =
let
- (* We could use 'PropLogic.defcnf fm' instead of 'PropLogic.nnf fm' *)
+ (* We could use 'PropLogic.auxcnf fm' instead of 'PropLogic.nnf fm' *)
(* but that sometimes introduces more boolean variables than we can *)
(* handle efficiently. *)
val fm' = PropLogic.nnf fm
@@ -534,11 +534,10 @@
(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_sat_file satpath fm; SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm))
+ fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.auxcnf 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 ()
@@ -563,7 +562,7 @@
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 writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.auxcnf fm)
fun readfn () = SatSolver.parse_std_result_file outpath ("Satisfiable !!", "solution =", "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 ()
@@ -588,7 +587,7 @@
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 writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.auxcnf fm)
fun readfn () = SatSolver.parse_std_result_file outpath ("s SATISFIABLE", "v ", "s 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 ()