# HG changeset patch
# User blanchet
# Date 1235488347 -3600
# Node ID e6f76bf0e0673926a713a4bc4314d339c85d8f2f
# Parent  ef79dc615f47f90da74d59ee166d8749cfabb255
Eliminated ZCHAFF_VERSION configuration variable, since zChaff's output format is identical in all versions since March 2003 (at least), and also because it forces users who want to use the latest versions to lie about the version number.
I also made the BERKMIN_EXE variable optional, defaulting to BerkMin561 (a reasonable name with no platform encoded in it).
These changes have no inpacts on already working Isabelle installations.

diff -r ef79dc615f47 -r e6f76bf0e067 etc/settings
--- a/etc/settings	Wed Feb 18 10:26:48 2009 +0100
+++ b/etc/settings	Tue Feb 24 16:12:27 2009 +0100
@@ -268,8 +268,6 @@
 
 # zChaff (SAT Solver, cf. Isabelle/src/HOL/Tools/sat_solver.ML)
 #ZCHAFF_HOME=/usr/local/bin
-#ZCHAFF_VERSION=2004.5.13
-#ZCHAFF_VERSION=2004.11.15
 
 # BerkMin561 (SAT Solver, cf. Isabelle/src/HOL/Tools/sat_solver.ML)
 #BERKMIN_HOME=/usr/local/bin
diff -r ef79dc615f47 -r e6f76bf0e067 src/HOL/Tools/sat_solver.ML
--- a/src/HOL/Tools/sat_solver.ML	Wed Feb 18 10:26:48 2009 +0100
+++ b/src/HOL/Tools/sat_solver.ML	Tue Feb 24 16:12:27 2009 +0100
@@ -914,10 +914,6 @@
   fun zchaff fm =
   let
     val _          = if (getenv "ZCHAFF_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
-    val _          = if (getenv "ZCHAFF_VERSION") <> "2004.5.13" andalso
-                        (getenv "ZCHAFF_VERSION") <> "2004.11.15" then raise SatSolver.NOT_CONFIGURED else ()
-      (* both versions of zChaff appear to have the same interface, so we do *)
-      (* not actually need to distinguish between them in the following code *)
     val serial_str = serial_string ()
     val inpath     = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
     val outpath    = File.tmp_path (Path.explode ("result" ^ serial_str))
@@ -943,11 +939,12 @@
 let
   fun berkmin fm =
   let
-    val _          = if (getenv "BERKMIN_HOME") = "" orelse (getenv "BERKMIN_EXE") = "" then raise SatSolver.NOT_CONFIGURED else ()
+    val _          = if (getenv "BERKMIN_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
     val serial_str = serial_string ()
     val inpath     = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
     val outpath    = File.tmp_path (Path.explode ("result" ^ serial_str))
-    val cmd        = (getenv "BERKMIN_HOME") ^ "/" ^ (getenv "BERKMIN_EXE") ^ " " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath)
+    val exec       = getenv "BERKMIN_EXE"
+    val cmd        = (getenv "BERKMIN_HOME") ^ "/" ^ (if exec = "" then "BerkMin561" else exec) ^ " " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath)
     fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
     fun readfn ()  = SatSolver.read_std_result_file outpath ("Satisfiable          !!", "solution =", "UNSATISFIABLE          !!")
     val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else ()