1.1 --- a/etc/settings	Thu Mar 05 02:32:46 2009 +0100
     1.2 +++ b/etc/settings	Thu Mar 05 10:19:51 2009 +0100
     1.3 @@ -262,8 +262,6 @@
     1.4  
     1.5  # zChaff (SAT Solver, cf. Isabelle/src/HOL/Tools/sat_solver.ML)
     1.6  #ZCHAFF_HOME=/usr/local/bin
     1.7 -#ZCHAFF_VERSION=2004.5.13
     1.8 -#ZCHAFF_VERSION=2004.11.15
     1.9  
    1.10  # BerkMin561 (SAT Solver, cf. Isabelle/src/HOL/Tools/sat_solver.ML)
    1.11  #BERKMIN_HOME=/usr/local/bin

     2.1 --- a/src/HOL/Tools/refute.ML	Thu Mar 05 02:32:46 2009 +0100
     2.2 +++ b/src/HOL/Tools/refute.ML	Thu Mar 05 10:19:51 2009 +0100
     2.3 @@ -63,6 +63,7 @@
     2.4  
     2.5    val close_form : Term.term -> Term.term
     2.6    val get_classdef : theory -> string -> (string * Term.term) option
     2.7 +  val norm_rhs : Term.term -> Term.term
     2.8    val get_def : theory -> string * Term.typ -> (string * Term.term) option
     2.9    val get_typedef : theory -> Term.typ -> (string * Term.term) option
    2.10    val is_IDT_constructor : theory -> string * Term.typ -> bool
    2.11 @@ -548,6 +549,20 @@
    2.12    end;
    2.13  
    2.14  (* ------------------------------------------------------------------------- *)
    2.15 +(* norm_rhs: maps  f ?t1 ... ?tn == rhs  to  %t1...tn. rhs                   *)
    2.16 +(* ------------------------------------------------------------------------- *)
    2.17 +
    2.18 +  fun norm_rhs eqn =
    2.19 +  let
    2.20 +    fun lambda (v as Var ((x, _), T)) t = Abs (x, T, abstract_over (v, t))
    2.21 +      | lambda v t                      = raise TERM ("lambda", [v, t])
    2.22 +    val (lhs, rhs) = Logic.dest_equals eqn
    2.23 +    val (_, args)  = Term.strip_comb lhs
    2.24 +  in
    2.25 +    fold lambda (rev args) rhs
    2.26 +  end
    2.27 +
    2.28 +(* ------------------------------------------------------------------------- *)
    2.29  (* get_def: looks up the definition of a constant, as created by "constdefs" *)
    2.30  (* ------------------------------------------------------------------------- *)
    2.31  
    2.32 @@ -555,16 +570,6 @@
    2.33  
    2.34    fun get_def thy (s, T) =
    2.35    let
    2.36 -    (* maps  f ?t1 ... ?tn == rhs  to  %t1...tn. rhs *)
    2.37 -    fun norm_rhs eqn =
    2.38 -    let
    2.39 -      fun lambda (v as Var ((x, _), T)) t = Abs (x, T, abstract_over (v, t))
    2.40 -        | lambda v t                      = raise TERM ("lambda", [v, t])
    2.41 -      val (lhs, rhs) = Logic.dest_equals eqn
    2.42 -      val (_, args)  = Term.strip_comb lhs
    2.43 -    in
    2.44 -      fold lambda (rev args) rhs
    2.45 -    end
    2.46      (* (string * Term.term) list -> (string * Term.term) option *)
    2.47      fun get_def_ax [] = NONE
    2.48        | get_def_ax ((axname, ax) :: axioms) =

     3.1 --- a/src/HOL/Tools/sat_solver.ML	Thu Mar 05 02:32:46 2009 +0100
     3.2 +++ b/src/HOL/Tools/sat_solver.ML	Thu Mar 05 10:19:51 2009 +0100
     3.3 @@ -914,10 +914,6 @@
     3.4    fun zchaff fm =
     3.5    let
     3.6      val _          = if (getenv "ZCHAFF_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
     3.7 -    val _          = if (getenv "ZCHAFF_VERSION") <> "2004.5.13" andalso
     3.8 -                        (getenv "ZCHAFF_VERSION") <> "2004.11.15" then raise SatSolver.NOT_CONFIGURED else ()
     3.9 -      (* both versions of zChaff appear to have the same interface, so we do *)
    3.10 -      (* not actually need to distinguish between them in the following code *)
    3.11      val serial_str = serial_string ()
    3.12      val inpath     = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
    3.13      val outpath    = File.tmp_path (Path.explode ("result" ^ serial_str))
    3.14 @@ -943,11 +939,12 @@
    3.15  let
    3.16    fun berkmin fm =
    3.17    let
    3.18 -    val _          = if (getenv "BERKMIN_HOME") = "" orelse (getenv "BERKMIN_EXE") = "" then raise SatSolver.NOT_CONFIGURED else ()
    3.19 +    val _          = if (getenv "BERKMIN_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
    3.20      val serial_str = serial_string ()
    3.21      val inpath     = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
    3.22      val outpath    = File.tmp_path (Path.explode ("result" ^ serial_str))
    3.23 -    val cmd        = (getenv "BERKMIN_HOME") ^ "/" ^ (getenv "BERKMIN_EXE") ^ " " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath)
    3.24 +    val exec       = getenv "BERKMIN_EXE"
    3.25 +    val cmd        = (getenv "BERKMIN_HOME") ^ "/" ^ (if exec = "" then "BerkMin561" else exec) ^ " " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath)
    3.26      fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
    3.27      fun readfn ()  = SatSolver.read_std_result_file outpath ("Satisfiable          !!", "solution =", "UNSATISFIABLE          !!")
    3.28      val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else ()