src/HOL/Tools/sat_solver.ML
changeset 21858 05f57309170c
parent 21268 7a6299a17386
child 22220 6dc8d0dca678
     1.1 --- a/src/HOL/Tools/sat_solver.ML	Thu Dec 14 22:19:39 2006 +0100
     1.2 +++ b/src/HOL/Tools/sat_solver.ML	Fri Dec 15 00:08:06 2006 +0100
     1.3 @@ -564,14 +564,14 @@
     1.4  	fun minisat_with_proofs fm =
     1.5  	let
     1.6  		val _          = if (getenv "MINISAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
     1.7 -		val inpath     = File.tmp_path (Path.unpack "isabelle.cnf")
     1.8 -		val outpath    = File.tmp_path (Path.unpack "result")
     1.9 -		val proofpath  = File.tmp_path (Path.unpack "result.prf")
    1.10 -		val cmd        = (getenv "MINISAT_HOME") ^ "/minisat " ^ (Path.pack inpath) ^ " -r " ^ (Path.pack outpath) ^ " -t " ^ (Path.pack proofpath) ^ "> /dev/null"
    1.11 +		val inpath     = File.tmp_path (Path.explode "isabelle.cnf")
    1.12 +		val outpath    = File.tmp_path (Path.explode "result")
    1.13 +		val proofpath  = File.tmp_path (Path.explode "result.prf")
    1.14 +		val cmd        = (getenv "MINISAT_HOME") ^ "/minisat " ^ (Path.implode inpath) ^ " -r " ^ (Path.implode outpath) ^ " -t " ^ (Path.implode proofpath) ^ "> /dev/null"
    1.15  		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath fm
    1.16  		fun readfn ()  = SatSolver.read_std_result_file outpath ("SAT", "", "UNSAT")
    1.17 -		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.pack inpath)) else ()
    1.18 -		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.pack outpath)) else ()
    1.19 +		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else ()
    1.20 +		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else ()
    1.21  		val cnf        = PropLogic.defcnf fm
    1.22  		val result     = SatSolver.make_external_solver cmd writefn readfn cnf
    1.23  		val _          = try File.rm inpath
    1.24 @@ -749,13 +749,13 @@
    1.25  	fun minisat fm =
    1.26  	let
    1.27  		val _          = if (getenv "MINISAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
    1.28 -		val inpath     = File.tmp_path (Path.unpack "isabelle.cnf")
    1.29 -		val outpath    = File.tmp_path (Path.unpack "result")
    1.30 -		val cmd        = (getenv "MINISAT_HOME") ^ "/minisat " ^ (Path.pack inpath) ^ " -r " ^ (Path.pack outpath) ^ " > /dev/null"
    1.31 +		val inpath     = File.tmp_path (Path.explode "isabelle.cnf")
    1.32 +		val outpath    = File.tmp_path (Path.explode "result")
    1.33 +		val cmd        = (getenv "MINISAT_HOME") ^ "/minisat " ^ (Path.implode inpath) ^ " -r " ^ (Path.implode outpath) ^ " > /dev/null"
    1.34  		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
    1.35  		fun readfn ()  = SatSolver.read_std_result_file outpath ("SAT", "", "UNSAT")
    1.36 -		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.pack inpath)) else ()
    1.37 -		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.pack outpath)) else ()
    1.38 +		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else ()
    1.39 +		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else ()
    1.40  		val result     = SatSolver.make_external_solver cmd writefn readfn fm
    1.41  		val _          = try File.rm inpath
    1.42  		val _          = try File.rm outpath
    1.43 @@ -788,7 +788,7 @@
    1.44  	  SatSolver.UNSATISFIABLE NONE =>
    1.45  		(let
    1.46  			(* string list *)
    1.47 -			val proof_lines = ((split_lines o File.read) (Path.unpack "resolve_trace"))
    1.48 +			val proof_lines = ((split_lines o File.read) (Path.explode "resolve_trace"))
    1.49  				handle IO.Io _ => raise INVALID_PROOF "Could not read file \"resolve_trace\""
    1.50  			(* PropLogic.prop_formula -> int *)
    1.51  			fun cnf_number_of_clauses (PropLogic.And (fm1, fm2)) = cnf_number_of_clauses fm1 + cnf_number_of_clauses fm2
    1.52 @@ -911,13 +911,13 @@
    1.53  		                    (getenv "ZCHAFF_VERSION") <> "2004.11.15" then raise SatSolver.NOT_CONFIGURED else ()
    1.54  			(* both versions of zChaff appear to have the same interface, so we do *)
    1.55  			(* not actually need to distinguish between them in the following code *)
    1.56 -		val inpath     = File.tmp_path (Path.unpack "isabelle.cnf")
    1.57 -		val outpath    = File.tmp_path (Path.unpack "result")
    1.58 -		val cmd        = (getenv "ZCHAFF_HOME") ^ "/zchaff " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath)
    1.59 +		val inpath     = File.tmp_path (Path.explode "isabelle.cnf")
    1.60 +		val outpath    = File.tmp_path (Path.explode "result")
    1.61 +		val cmd        = (getenv "ZCHAFF_HOME") ^ "/zchaff " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath)
    1.62  		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
    1.63  		fun readfn ()  = SatSolver.read_std_result_file outpath ("Instance Satisfiable", "", "Instance Unsatisfiable")
    1.64 -		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.pack inpath)) else ()
    1.65 -		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.pack outpath)) else ()
    1.66 +		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else ()
    1.67 +		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else ()
    1.68  		val result     = SatSolver.make_external_solver cmd writefn readfn fm
    1.69  		val _          = try File.rm inpath
    1.70  		val _          = try File.rm outpath
    1.71 @@ -936,13 +936,13 @@
    1.72  	fun berkmin fm =
    1.73  	let
    1.74  		val _          = if (getenv "BERKMIN_HOME") = "" orelse (getenv "BERKMIN_EXE") = "" then raise SatSolver.NOT_CONFIGURED else ()
    1.75 -		val inpath     = File.tmp_path (Path.unpack "isabelle.cnf")
    1.76 -		val outpath    = File.tmp_path (Path.unpack "result")
    1.77 -		val cmd        = (getenv "BERKMIN_HOME") ^ "/" ^ (getenv "BERKMIN_EXE") ^ " " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath)
    1.78 +		val inpath     = File.tmp_path (Path.explode "isabelle.cnf")
    1.79 +		val outpath    = File.tmp_path (Path.explode "result")
    1.80 +		val cmd        = (getenv "BERKMIN_HOME") ^ "/" ^ (getenv "BERKMIN_EXE") ^ " " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath)
    1.81  		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
    1.82  		fun readfn ()  = SatSolver.read_std_result_file outpath ("Satisfiable          !!", "solution =", "UNSATISFIABLE          !!")
    1.83 -		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.pack inpath)) else ()
    1.84 -		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.pack outpath)) else ()
    1.85 +		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else ()
    1.86 +		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else ()
    1.87  		val result     = SatSolver.make_external_solver cmd writefn readfn fm
    1.88  		val _          = try File.rm inpath
    1.89  		val _          = try File.rm outpath
    1.90 @@ -961,13 +961,13 @@
    1.91  	fun jerusat fm =
    1.92  	let
    1.93  		val _          = if (getenv "JERUSAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
    1.94 -		val inpath     = File.tmp_path (Path.unpack "isabelle.cnf")
    1.95 -		val outpath    = File.tmp_path (Path.unpack "result")
    1.96 -		val cmd        = (getenv "JERUSAT_HOME") ^ "/Jerusat1.3 " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath)
    1.97 +		val inpath     = File.tmp_path (Path.explode "isabelle.cnf")
    1.98 +		val outpath    = File.tmp_path (Path.explode "result")
    1.99 +		val cmd        = (getenv "JERUSAT_HOME") ^ "/Jerusat1.3 " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath)
   1.100  		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
   1.101  		fun readfn ()  = SatSolver.read_std_result_file outpath ("s SATISFIABLE", "v ", "s UNSATISFIABLE")
   1.102 -		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.pack inpath)) else ()
   1.103 -		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.pack outpath)) else ()
   1.104 +		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else ()
   1.105 +		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else ()
   1.106  		val result     = SatSolver.make_external_solver cmd writefn readfn fm
   1.107  		val _          = try File.rm inpath
   1.108  		val _          = try File.rm outpath