src/HOL/Tools/sat_solver.ML
changeset 16911 20a139ca2f62
parent 16899 ee4d620bcc1c
child 16912 35b01ba73625
equal deleted inserted replaced
16910:19b4bf469fb2 16911:20a139ca2f62
     1 (*  Title:      HOL/Tools/sat_solver.ML
     1 (*  Title:      HOL/Tools/sat_solver.ML
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Tjark Weber
     3     Author:     Tjark Weber
     4     Copyright   2004
     4     Copyright   2004-2005
     5 
     5 
     6 Interface to external SAT solvers, and (simple) built-in SAT solvers.
     6 Interface to external SAT solvers, and (simple) built-in SAT solvers.
     7 *)
     7 *)
     8 
     8 
     9 signature SAT_SOLVER =
     9 signature SAT_SOLVER =
   412 	local
   412 	local
   413 		open PropLogic
   413 		open PropLogic
   414 	in
   414 	in
   415 		fun dpll_solver fm =
   415 		fun dpll_solver fm =
   416 		let
   416 		let
   417 			(* We could use 'PropLogic.defcnf fm' instead of 'PropLogic.nnf fm' *)
   417 			(* We could use 'PropLogic.auxcnf fm' instead of 'PropLogic.nnf fm' *)
   418 			(* but that sometimes introduces more boolean variables than we can *)
   418 			(* but that sometimes introduces more boolean variables than we can *)
   419 			(* handle efficiently.                                              *)
   419 			(* handle efficiently.                                              *)
   420 			val fm' = PropLogic.nnf fm
   420 			val fm' = PropLogic.nnf fm
   421 			(* int list *)
   421 			(* int list *)
   422 			val indices = PropLogic.indices fm'
   422 			val indices = PropLogic.indices fm'
   532 		val _          = if (getenv "ZCHAFF_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
   532 		val _          = if (getenv "ZCHAFF_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
   533 		val _          = if (getenv "ZCHAFF_VERSION") <> "2004.5.13" andalso
   533 		val _          = if (getenv "ZCHAFF_VERSION") <> "2004.5.13" andalso
   534 		                    (getenv "ZCHAFF_VERSION") <> "2004.11.15" then raise SatSolver.NOT_CONFIGURED else ()
   534 		                    (getenv "ZCHAFF_VERSION") <> "2004.11.15" then raise SatSolver.NOT_CONFIGURED else ()
   535 			(* both versions of zChaff appear to have the same interface, so we do *)
   535 			(* both versions of zChaff appear to have the same interface, so we do *)
   536 			(* not actually need to distinguish between them in the following code *)
   536 			(* not actually need to distinguish between them in the following code *)
   537 		val satpath    = File.tmp_path (Path.unpack "isabelle.sat")
       
   538 		val inpath     = File.tmp_path (Path.unpack "isabelle.cnf")
   537 		val inpath     = File.tmp_path (Path.unpack "isabelle.cnf")
   539 		val outpath    = File.tmp_path (Path.unpack "result")
   538 		val outpath    = File.tmp_path (Path.unpack "result")
   540 		val cmd        = (getenv "ZCHAFF_HOME") ^ "/zchaff " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath)
   539 		val cmd        = (getenv "ZCHAFF_HOME") ^ "/zchaff " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath)
   541 		fun writefn fm = (SatSolver.write_dimacs_sat_file satpath fm; SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm))
   540 		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.auxcnf fm)
   542 		fun readfn ()  = SatSolver.parse_std_result_file outpath ("Instance Satisfiable", "", "Instance Unsatisfiable")
   541 		fun readfn ()  = SatSolver.parse_std_result_file outpath ("Instance Satisfiable", "", "Instance Unsatisfiable")
   543 		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.pack inpath)) else ()
   542 		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.pack inpath)) else ()
   544 		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.pack outpath)) else ()
   543 		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.pack outpath)) else ()
   545 		val result     = SatSolver.make_external_solver cmd writefn readfn fm
   544 		val result     = SatSolver.make_external_solver cmd writefn readfn fm
   546 		val _          = try File.rm inpath
   545 		val _          = try File.rm inpath
   561 	let
   560 	let
   562 		val _          = if (getenv "BERKMIN_HOME") = "" orelse (getenv "BERKMIN_EXE") = "" then raise SatSolver.NOT_CONFIGURED else ()
   561 		val _          = if (getenv "BERKMIN_HOME") = "" orelse (getenv "BERKMIN_EXE") = "" then raise SatSolver.NOT_CONFIGURED else ()
   563 		val inpath     = File.tmp_path (Path.unpack "isabelle.cnf")
   562 		val inpath     = File.tmp_path (Path.unpack "isabelle.cnf")
   564 		val outpath    = File.tmp_path (Path.unpack "result")
   563 		val outpath    = File.tmp_path (Path.unpack "result")
   565 		val cmd        = (getenv "BERKMIN_HOME") ^ "/" ^ (getenv "BERKMIN_EXE") ^ " " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath)
   564 		val cmd        = (getenv "BERKMIN_HOME") ^ "/" ^ (getenv "BERKMIN_EXE") ^ " " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath)
   566 		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
   565 		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.auxcnf fm)
   567 		fun readfn ()  = SatSolver.parse_std_result_file outpath ("Satisfiable          !!", "solution =", "UNSATISFIABLE          !!")
   566 		fun readfn ()  = SatSolver.parse_std_result_file outpath ("Satisfiable          !!", "solution =", "UNSATISFIABLE          !!")
   568 		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.pack inpath)) else ()
   567 		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.pack inpath)) else ()
   569 		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.pack outpath)) else ()
   568 		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.pack outpath)) else ()
   570 		val result     = SatSolver.make_external_solver cmd writefn readfn fm
   569 		val result     = SatSolver.make_external_solver cmd writefn readfn fm
   571 		val _          = try File.rm inpath
   570 		val _          = try File.rm inpath
   586 	let
   585 	let
   587 		val _          = if (getenv "JERUSAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
   586 		val _          = if (getenv "JERUSAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
   588 		val inpath     = File.tmp_path (Path.unpack "isabelle.cnf")
   587 		val inpath     = File.tmp_path (Path.unpack "isabelle.cnf")
   589 		val outpath    = File.tmp_path (Path.unpack "result")
   588 		val outpath    = File.tmp_path (Path.unpack "result")
   590 		val cmd        = (getenv "JERUSAT_HOME") ^ "/Jerusat1.3 " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath)
   589 		val cmd        = (getenv "JERUSAT_HOME") ^ "/Jerusat1.3 " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath)
   591 		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
   590 		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.auxcnf fm)
   592 		fun readfn ()  = SatSolver.parse_std_result_file outpath ("s SATISFIABLE", "v ", "s UNSATISFIABLE")
   591 		fun readfn ()  = SatSolver.parse_std_result_file outpath ("s SATISFIABLE", "v ", "s UNSATISFIABLE")
   593 		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.pack inpath)) else ()
   592 		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.pack inpath)) else ()
   594 		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.pack outpath)) else ()
   593 		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.pack outpath)) else ()
   595 		val result     = SatSolver.make_external_solver cmd writefn readfn fm
   594 		val result     = SatSolver.make_external_solver cmd writefn readfn fm
   596 		val _          = try File.rm inpath
   595 		val _          = try File.rm inpath