# 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 ()