src/HOL/Tools/sat_solver.ML
changeset 15313 24aee76539df
parent 15299 576fd0b65ed8
child 15329 bd94b0a71dd2
equal deleted inserted replaced
15312:7d6e12ead964 15313:24aee76539df
   524 		val inpath     = File.tmp_path (Path.unpack "isabelle.cnf")
   524 		val inpath     = File.tmp_path (Path.unpack "isabelle.cnf")
   525 		val outpath    = File.tmp_path (Path.unpack "result")
   525 		val outpath    = File.tmp_path (Path.unpack "result")
   526 		val cmd        = (getenv "ZCHAFF_HOME") ^ "/zchaff " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath)
   526 		val cmd        = (getenv "ZCHAFF_HOME") ^ "/zchaff " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath)
   527 		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
   527 		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
   528 		fun readfn ()  = SatSolver.parse_std_result_file outpath ("Instance Satisfiable", "", "Instance Unsatisfiable")
   528 		fun readfn ()  = SatSolver.parse_std_result_file outpath ("Instance Satisfiable", "", "Instance Unsatisfiable")
   529 		val _          = assert (not (File.exists inpath)) ("file " ^ quote (Path.pack inpath) ^ " exists, please delete (will not overwrite)")
   529 		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (File.sysify_path inpath)) else ()
   530 		val _          = assert (not (File.exists outpath)) ("file " ^ quote (Path.pack outpath) ^ " exists, please delete (will not overwrite)")
   530 		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (File.sysify_path outpath)) else ()
   531 		val result     = SatSolver.make_external_solver cmd writefn readfn fm
   531 		val result     = SatSolver.make_external_solver cmd writefn readfn fm
   532 		val _          = (File.rm inpath handle _ => ())
   532 		val _          = (File.rm inpath handle _ => ())
   533 		val _          = (File.rm outpath handle _ => ())
   533 		val _          = (File.rm outpath handle _ => ())
   534 	in
   534 	in
   535 		result
   535 		result
   549 		val inpath     = File.tmp_path (Path.unpack "isabelle.cnf")
   549 		val inpath     = File.tmp_path (Path.unpack "isabelle.cnf")
   550 		val outpath    = File.tmp_path (Path.unpack "result")
   550 		val outpath    = File.tmp_path (Path.unpack "result")
   551 		val cmd        = (getenv "BERKMIN_HOME") ^ "/" ^ (getenv "BERKMIN_EXE") ^ " " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath)
   551 		val cmd        = (getenv "BERKMIN_HOME") ^ "/" ^ (getenv "BERKMIN_EXE") ^ " " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath)
   552 		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
   552 		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
   553 		fun readfn ()  = SatSolver.parse_std_result_file outpath ("Satisfiable          !!", "solution =", "UNSATISFIABLE          !!")
   553 		fun readfn ()  = SatSolver.parse_std_result_file outpath ("Satisfiable          !!", "solution =", "UNSATISFIABLE          !!")
   554 		val _          = assert (not (File.exists inpath)) ("file " ^ quote (Path.pack inpath) ^ " exists, please delete (will not overwrite)")
   554 		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (File.sysify_path inpath)) else ()
   555 		val _          = assert (not (File.exists outpath)) ("file " ^ quote (Path.pack outpath) ^ " exists, please delete (will not overwrite)")
   555 		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (File.sysify_path outpath)) else ()
   556 		val result     = SatSolver.make_external_solver cmd writefn readfn fm
   556 		val result     = SatSolver.make_external_solver cmd writefn readfn fm
   557 		val _          = (File.rm inpath handle _ => ())
   557 		val _          = (File.rm inpath handle _ => ())
   558 		val _          = (File.rm outpath handle _ => ())
   558 		val _          = (File.rm outpath handle _ => ())
   559 	in
   559 	in
   560 		result
   560 		result
   574 		val inpath     = File.tmp_path (Path.unpack "isabelle.cnf")
   574 		val inpath     = File.tmp_path (Path.unpack "isabelle.cnf")
   575 		val outpath    = File.tmp_path (Path.unpack "result")
   575 		val outpath    = File.tmp_path (Path.unpack "result")
   576 		val cmd        = (getenv "JERUSAT_HOME") ^ "/Jerusat1.3 " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath)
   576 		val cmd        = (getenv "JERUSAT_HOME") ^ "/Jerusat1.3 " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath)
   577 		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
   577 		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
   578 		fun readfn ()  = SatSolver.parse_std_result_file outpath ("s SATISFIABLE", "v ", "s UNSATISFIABLE")
   578 		fun readfn ()  = SatSolver.parse_std_result_file outpath ("s SATISFIABLE", "v ", "s UNSATISFIABLE")
   579 		val _          = assert (not (File.exists inpath)) ("file " ^ quote (Path.pack inpath) ^ " exists, please delete (will not overwrite)")
   579 		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (File.sysify_path inpath)) else ()
   580 		val _          = assert (not (File.exists outpath)) ("file " ^ quote (Path.pack outpath) ^ " exists, please delete (will not overwrite)")
   580 		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (File.sysify_path outpath)) else ()
   581 		val result     = SatSolver.make_external_solver cmd writefn readfn fm
   581 		val result     = SatSolver.make_external_solver cmd writefn readfn fm
   582 		val _          = (File.rm inpath handle _ => ())
   582 		val _          = (File.rm inpath handle _ => ())
   583 		val _          = (File.rm outpath handle _ => ())
   583 		val _          = (File.rm outpath handle _ => ())
   584 	in
   584 	in
   585 		result
   585 		result