replaced calls to PropLogic.auxcnf by PropLogic.defcnf again
authorwebertj
Tue Jul 26 14:31:42 2005 +0200 (2005-07-26)
changeset 16914e68528b4fc0b
parent 16913 1d8a8d010e69
child 16915 bca4c3b1afca
replaced calls to PropLogic.auxcnf by PropLogic.defcnf again
src/HOL/Tools/sat_solver.ML
     1.1 --- a/src/HOL/Tools/sat_solver.ML	Tue Jul 26 14:14:13 2005 +0200
     1.2 +++ b/src/HOL/Tools/sat_solver.ML	Tue Jul 26 14:31:42 2005 +0200
     1.3 @@ -414,7 +414,7 @@
     1.4  	in
     1.5  		fun dpll_solver fm =
     1.6  		let
     1.7 -			(* We could use 'PropLogic.auxcnf fm' instead of 'PropLogic.nnf fm' *)
     1.8 +			(* We could use 'PropLogic.defcnf fm' instead of 'PropLogic.nnf fm' *)
     1.9  			(* but that sometimes introduces more boolean variables than we can *)
    1.10  			(* handle efficiently.                                              *)
    1.11  			val fm' = PropLogic.nnf fm
    1.12 @@ -537,7 +537,7 @@
    1.13  		val inpath     = File.tmp_path (Path.unpack "isabelle.cnf")
    1.14  		val outpath    = File.tmp_path (Path.unpack "result")
    1.15  		val cmd        = (getenv "ZCHAFF_HOME") ^ "/zchaff " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath)
    1.16 -		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.auxcnf fm)
    1.17 +		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
    1.18  		fun readfn ()  = SatSolver.parse_std_result_file outpath ("Instance Satisfiable", "", "Instance Unsatisfiable")
    1.19  		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.pack inpath)) else ()
    1.20  		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.pack outpath)) else ()
    1.21 @@ -562,7 +562,7 @@
    1.22  		val inpath     = File.tmp_path (Path.unpack "isabelle.cnf")
    1.23  		val outpath    = File.tmp_path (Path.unpack "result")
    1.24  		val cmd        = (getenv "BERKMIN_HOME") ^ "/" ^ (getenv "BERKMIN_EXE") ^ " " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath)
    1.25 -		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.auxcnf fm)
    1.26 +		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
    1.27  		fun readfn ()  = SatSolver.parse_std_result_file outpath ("Satisfiable          !!", "solution =", "UNSATISFIABLE          !!")
    1.28  		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.pack inpath)) else ()
    1.29  		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.pack outpath)) else ()
    1.30 @@ -587,7 +587,7 @@
    1.31  		val inpath     = File.tmp_path (Path.unpack "isabelle.cnf")
    1.32  		val outpath    = File.tmp_path (Path.unpack "result")
    1.33  		val cmd        = (getenv "JERUSAT_HOME") ^ "/Jerusat1.3 " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath)
    1.34 -		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.auxcnf fm)
    1.35 +		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
    1.36  		fun readfn ()  = SatSolver.parse_std_result_file outpath ("s SATISFIABLE", "v ", "s UNSATISFIABLE")
    1.37  		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.pack inpath)) else ()
    1.38  		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.pack outpath)) else ()