src/HOL/Tools/sat_solver.ML
changeset 29872 14e208d607af
parent 22567 1565d476a9e2
child 30237 e6f76bf0e067
     1.1 --- a/src/HOL/Tools/sat_solver.ML	Tue Feb 10 14:58:15 2009 +0100
     1.2 +++ b/src/HOL/Tools/sat_solver.ML	Tue Feb 10 18:57:02 2009 +0100
     1.3 @@ -569,9 +569,10 @@
     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.explode "isabelle.cnf")
     1.8 -    val outpath    = File.tmp_path (Path.explode "result")
     1.9 -    val proofpath  = File.tmp_path (Path.explode "result.prf")
    1.10 +    val serial_str = serial_string ()
    1.11 +    val inpath     = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
    1.12 +    val outpath    = File.tmp_path (Path.explode ("result" ^ serial_str))
    1.13 +    val proofpath  = File.tmp_path (Path.explode ("result" ^ serial_str ^ ".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 @@ -754,8 +755,9 @@
    1.18    fun minisat fm =
    1.19    let
    1.20      val _          = if (getenv "MINISAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
    1.21 -    val inpath     = File.tmp_path (Path.explode "isabelle.cnf")
    1.22 -    val outpath    = File.tmp_path (Path.explode "result")
    1.23 +    val serial_str = serial_string ()
    1.24 +    val inpath     = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
    1.25 +    val outpath    = File.tmp_path (Path.explode ("result" ^ serial_str))
    1.26      val cmd        = (getenv "MINISAT_HOME") ^ "/minisat " ^ (Path.implode inpath) ^ " -r " ^ (Path.implode outpath) ^ " > /dev/null"
    1.27      fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
    1.28      fun readfn ()  = SatSolver.read_std_result_file outpath ("SAT", "", "UNSAT")
    1.29 @@ -916,8 +918,9 @@
    1.30                          (getenv "ZCHAFF_VERSION") <> "2004.11.15" then raise SatSolver.NOT_CONFIGURED else ()
    1.31        (* both versions of zChaff appear to have the same interface, so we do *)
    1.32        (* not actually need to distinguish between them in the following code *)
    1.33 -    val inpath     = File.tmp_path (Path.explode "isabelle.cnf")
    1.34 -    val outpath    = File.tmp_path (Path.explode "result")
    1.35 +    val serial_str = serial_string ()
    1.36 +    val inpath     = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
    1.37 +    val outpath    = File.tmp_path (Path.explode ("result" ^ serial_str))
    1.38      val cmd        = (getenv "ZCHAFF_HOME") ^ "/zchaff " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath)
    1.39      fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
    1.40      fun readfn ()  = SatSolver.read_std_result_file outpath ("Instance Satisfiable", "", "Instance Unsatisfiable")
    1.41 @@ -941,8 +944,9 @@
    1.42    fun berkmin fm =
    1.43    let
    1.44      val _          = if (getenv "BERKMIN_HOME") = "" orelse (getenv "BERKMIN_EXE") = "" then raise SatSolver.NOT_CONFIGURED else ()
    1.45 -    val inpath     = File.tmp_path (Path.explode "isabelle.cnf")
    1.46 -    val outpath    = File.tmp_path (Path.explode "result")
    1.47 +    val serial_str = serial_string ()
    1.48 +    val inpath     = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
    1.49 +    val outpath    = File.tmp_path (Path.explode ("result" ^ serial_str))
    1.50      val cmd        = (getenv "BERKMIN_HOME") ^ "/" ^ (getenv "BERKMIN_EXE") ^ " " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath)
    1.51      fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
    1.52      fun readfn ()  = SatSolver.read_std_result_file outpath ("Satisfiable          !!", "solution =", "UNSATISFIABLE          !!")
    1.53 @@ -966,8 +970,9 @@
    1.54    fun jerusat fm =
    1.55    let
    1.56      val _          = if (getenv "JERUSAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
    1.57 -    val inpath     = File.tmp_path (Path.explode "isabelle.cnf")
    1.58 -    val outpath    = File.tmp_path (Path.explode "result")
    1.59 +    val serial_str = serial_string ()
    1.60 +    val inpath     = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
    1.61 +    val outpath    = File.tmp_path (Path.explode ("result" ^ serial_str))
    1.62      val cmd        = (getenv "JERUSAT_HOME") ^ "/Jerusat1.3 " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath)
    1.63      fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
    1.64      fun readfn ()  = SatSolver.read_std_result_file outpath ("s SATISFIABLE", "v ", "s UNSATISFIABLE")