Reintroduced previous changes: Made "Refute.norm_rhs" public and simplified the configuration of the BerkMin and zChaff SAT solvers.

--- a/etc/settings	Thu Mar 05 02:32:46 2009 +0100
+++ b/etc/settings	Thu Mar 05 10:19:51 2009 +0100
@@ -262,8 +262,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

--- a/src/HOL/Tools/refute.ML	Thu Mar 05 02:32:46 2009 +0100
+++ b/src/HOL/Tools/refute.ML	Thu Mar 05 10:19:51 2009 +0100
@@ -63,6 +63,7 @@
 
   val close_form : Term.term -> Term.term
   val get_classdef : theory -> string -> (string * Term.term) option
+  val norm_rhs : Term.term -> Term.term
   val get_def : theory -> string * Term.typ -> (string * Term.term) option
   val get_typedef : theory -> Term.typ -> (string * Term.term) option
   val is_IDT_constructor : theory -> string * Term.typ -> bool
@@ -548,6 +549,20 @@
   end;
 
 (* ------------------------------------------------------------------------- *)
+(* norm_rhs: maps  f ?t1 ... ?tn == rhs  to  %t1...tn. rhs                   *)
+(* ------------------------------------------------------------------------- *)
+
+  fun norm_rhs eqn =
+  let
+    fun lambda (v as Var ((x, _), T)) t = Abs (x, T, abstract_over (v, t))
+      | lambda v t                      = raise TERM ("lambda", [v, t])
+    val (lhs, rhs) = Logic.dest_equals eqn
+    val (_, args)  = Term.strip_comb lhs
+  in
+    fold lambda (rev args) rhs
+  end
+
+(* ------------------------------------------------------------------------- *)
 (* get_def: looks up the definition of a constant, as created by "constdefs" *)
 (* ------------------------------------------------------------------------- *)
 
@@ -555,16 +570,6 @@
 
   fun get_def thy (s, T) =
   let
-    (* maps  f ?t1 ... ?tn == rhs  to  %t1...tn. rhs *)
-    fun norm_rhs eqn =
-    let
-      fun lambda (v as Var ((x, _), T)) t = Abs (x, T, abstract_over (v, t))
-        | lambda v t                      = raise TERM ("lambda", [v, t])
-      val (lhs, rhs) = Logic.dest_equals eqn
-      val (_, args)  = Term.strip_comb lhs
-    in
-      fold lambda (rev args) rhs
-    end
     (* (string * Term.term) list -> (string * Term.term) option *)
     fun get_def_ax [] = NONE
       | get_def_ax ((axname, ax) :: axioms) =

--- a/src/HOL/Tools/sat_solver.ML	Thu Mar 05 02:32:46 2009 +0100
+++ b/src/HOL/Tools/sat_solver.ML	Thu Mar 05 10:19:51 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 ()