# HG changeset patch
# User webertj
# Date 1122381102 -7200
# Node ID e68528b4fc0bce387af31c0063de433500ab1b37
# Parent  1d8a8d010e699035cc63c99830555a8e8e93c6b9
replaced calls to PropLogic.auxcnf by PropLogic.defcnf again

diff -r 1d8a8d010e69 -r e68528b4fc0b src/HOL/Tools/sat_solver.ML
--- a/src/HOL/Tools/sat_solver.ML	Tue Jul 26 14:14:13 2005 +0200
+++ b/src/HOL/Tools/sat_solver.ML	Tue Jul 26 14:31:42 2005 +0200
@@ -414,7 +414,7 @@
 	in
 		fun dpll_solver fm =
 		let
-			(* We could use 'PropLogic.auxcnf fm' instead of 'PropLogic.nnf fm' *)
+			(* 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
@@ -537,7 +537,7 @@
 		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.auxcnf fm)
+		fun writefn 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 ()
@@ -562,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.auxcnf fm)
+		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf 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 ()
@@ -587,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.auxcnf fm)
+		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 _          = 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 ()