# HG changeset patch
# User webertj
# Date 1122373390 -7200
# Node ID 20a139ca2f62edea322b5a8f45fccae6446283d6
# Parent  19b4bf469fb26264ad1adb23ac7a70010bf20748
replaced calls to PropLogic.defcnf by PropLogic.auxcnf

diff -r 19b4bf469fb2 -r 20a139ca2f62 src/HOL/Tools/sat_solver.ML
--- 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 ()