src/HOL/Tools/sat_solver.ML
changeset 20033 2b8dbb637792
parent 19190 7c311c513bae
child 20135 5a6b33268bb6
     1.1 --- a/src/HOL/Tools/sat_solver.ML	Thu Jul 06 23:36:40 2006 +0200
     1.2 +++ b/src/HOL/Tools/sat_solver.ML	Fri Jul 07 02:12:52 2006 +0200
     1.3 @@ -251,10 +251,10 @@
     1.4  		fun parse_lines [] =
     1.5  			UNKNOWN
     1.6  		  | parse_lines (line::lines) =
     1.7 -			if is_substring satisfiable line then
     1.8 +			if is_substring unsatisfiable line then
     1.9 +				UNSATISFIABLE NONE
    1.10 +			else if is_substring satisfiable line then
    1.11  				SATISFIABLE (parse_assignment [] lines)
    1.12 -			else if is_substring unsatisfiable line then
    1.13 -				UNSATISFIABLE NONE
    1.14  			else
    1.15  				parse_lines lines
    1.16  	in
    1.17 @@ -541,6 +541,32 @@
    1.18  end;
    1.19  
    1.20  (* ------------------------------------------------------------------------- *)
    1.21 +(* MiniSat 1.14                                                              *)
    1.22 +(* (http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/)            *)
    1.23 +(* ------------------------------------------------------------------------- *)
    1.24 +
    1.25 +let
    1.26 +	fun minisat fm =
    1.27 +	let
    1.28 +		val _          = if (getenv "MINISAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
    1.29 +		val inpath     = File.tmp_path (Path.unpack "isabelle.cnf")
    1.30 +		val outpath    = File.tmp_path (Path.unpack "result")
    1.31 +		val cmd        = (getenv "MINISAT_HOME") ^ "/minisat " ^ (Path.pack inpath) ^ " -r " ^ (Path.pack outpath) ^ " > /dev/null"
    1.32 +		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
    1.33 +		fun readfn ()  = SatSolver.read_std_result_file outpath ("SAT", "", "UNSAT")
    1.34 +		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.pack inpath)) else ()
    1.35 +		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.pack outpath)) else ()
    1.36 +		val result     = SatSolver.make_external_solver cmd writefn readfn fm
    1.37 +		val _          = try File.rm inpath
    1.38 +		val _          = try File.rm outpath
    1.39 +	in
    1.40 +		result
    1.41 +	end
    1.42 +in
    1.43 +	SatSolver.add_solver ("minisat", minisat)
    1.44 +end;
    1.45 +
    1.46 +(* ------------------------------------------------------------------------- *)
    1.47  (* zChaff (http://www.princeton.edu/~chaff/zchaff.html)                      *)
    1.48  (* ------------------------------------------------------------------------- *)
    1.49