src/HOL/Tools/sat_solver.ML
changeset 15332 0dc05858a862
parent 15329 bd94b0a71dd2
child 15531 08c8dad8e399
     1.1 --- a/src/HOL/Tools/sat_solver.ML	Thu Nov 25 14:38:37 2004 +0100
     1.2 +++ b/src/HOL/Tools/sat_solver.ML	Thu Nov 25 14:44:52 2004 +0100
     1.3 @@ -515,13 +515,17 @@
     1.4  end;
     1.5  
     1.6  (* ------------------------------------------------------------------------- *)
     1.7 -(* ZChaff, Version 2004.05.13 (http://www.princeton.edu/~chaff/zchaff.html)  *)
     1.8 +(* zChaff (http://www.princeton.edu/~chaff/zchaff.html)                      *)
     1.9  (* ------------------------------------------------------------------------- *)
    1.10  
    1.11  let
    1.12  	fun zchaff fm =
    1.13  	let
    1.14  		val _          = if (getenv "ZCHAFF_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
    1.15 +		val _          = if (getenv "ZCHAFF_VERSION") <> "2004.5.13" andalso
    1.16 +		                    (getenv "ZCHAFF_VERSION") <> "2004.11.15" then raise SatSolver.NOT_CONFIGURED else ()
    1.17 +			(* both versions of zChaff appear to have the same interface, so we do *)
    1.18 +			(* not actually need to distinguish between them in the following code *)
    1.19  		val inpath     = File.tmp_path (Path.unpack "isabelle.cnf")
    1.20  		val outpath    = File.tmp_path (Path.unpack "result")
    1.21  		val cmd        = (getenv "ZCHAFF_HOME") ^ "/zchaff " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath)