external solvers may now overwrite existing temporary files
authorwebertj
Tue Nov 23 15:36:39 2004 +0100 (2004-11-23)
changeset 1531324aee76539df
parent 15312 7d6e12ead964
child 15314 55eec5c6d401
external solvers may now overwrite existing temporary files
src/HOL/Tools/sat_solver.ML
     1.1 --- a/src/HOL/Tools/sat_solver.ML	Tue Nov 23 15:32:11 2004 +0100
     1.2 +++ b/src/HOL/Tools/sat_solver.ML	Tue Nov 23 15:36:39 2004 +0100
     1.3 @@ -526,8 +526,8 @@
     1.4  		val cmd        = (getenv "ZCHAFF_HOME") ^ "/zchaff " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath)
     1.5  		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
     1.6  		fun readfn ()  = SatSolver.parse_std_result_file outpath ("Instance Satisfiable", "", "Instance Unsatisfiable")
     1.7 -		val _          = assert (not (File.exists inpath)) ("file " ^ quote (Path.pack inpath) ^ " exists, please delete (will not overwrite)")
     1.8 -		val _          = assert (not (File.exists outpath)) ("file " ^ quote (Path.pack outpath) ^ " exists, please delete (will not overwrite)")
     1.9 +		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (File.sysify_path inpath)) else ()
    1.10 +		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (File.sysify_path outpath)) else ()
    1.11  		val result     = SatSolver.make_external_solver cmd writefn readfn fm
    1.12  		val _          = (File.rm inpath handle _ => ())
    1.13  		val _          = (File.rm outpath handle _ => ())
    1.14 @@ -551,8 +551,8 @@
    1.15  		val cmd        = (getenv "BERKMIN_HOME") ^ "/" ^ (getenv "BERKMIN_EXE") ^ " " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath)
    1.16  		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
    1.17  		fun readfn ()  = SatSolver.parse_std_result_file outpath ("Satisfiable          !!", "solution =", "UNSATISFIABLE          !!")
    1.18 -		val _          = assert (not (File.exists inpath)) ("file " ^ quote (Path.pack inpath) ^ " exists, please delete (will not overwrite)")
    1.19 -		val _          = assert (not (File.exists outpath)) ("file " ^ quote (Path.pack outpath) ^ " exists, please delete (will not overwrite)")
    1.20 +		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (File.sysify_path inpath)) else ()
    1.21 +		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (File.sysify_path outpath)) else ()
    1.22  		val result     = SatSolver.make_external_solver cmd writefn readfn fm
    1.23  		val _          = (File.rm inpath handle _ => ())
    1.24  		val _          = (File.rm outpath handle _ => ())
    1.25 @@ -576,8 +576,8 @@
    1.26  		val cmd        = (getenv "JERUSAT_HOME") ^ "/Jerusat1.3 " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath)
    1.27  		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
    1.28  		fun readfn ()  = SatSolver.parse_std_result_file outpath ("s SATISFIABLE", "v ", "s UNSATISFIABLE")
    1.29 -		val _          = assert (not (File.exists inpath)) ("file " ^ quote (Path.pack inpath) ^ " exists, please delete (will not overwrite)")
    1.30 -		val _          = assert (not (File.exists outpath)) ("file " ^ quote (Path.pack outpath) ^ " exists, please delete (will not overwrite)")
    1.31 +		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (File.sysify_path inpath)) else ()
    1.32 +		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (File.sysify_path outpath)) else ()
    1.33  		val result     = SatSolver.make_external_solver cmd writefn readfn fm
    1.34  		val _          = (File.rm inpath handle _ => ())
    1.35  		val _          = (File.rm outpath handle _ => ())