# HG changeset patch
# User blanchet
# Date 1292890337 -3600
# Node ID 3cb52cbf0eed18287a93611eb72a07a61c1ece18
# Parent  2a12d91a6ab7a982d5f878a0e0fba56439597f87
enable E weight generation with unofficial latest version of E (tentatively called E 1.2B) -- backed by Judgment Day

diff -r 2a12d91a6ab7 -r 3cb52cbf0eed src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Mon Dec 20 23:36:58 2010 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Tue Dec 21 01:12:17 2010 +0100
@@ -125,7 +125,8 @@
   | string_for_failure prover (UnknownError string) =
     (* "An" is correct for "ATP" and "SMT". *)
     "An " ^ prover ^ " error occurred" ^
-    (if string = "" then "." else ":\n" ^ string)
+    (if string = "" then ". (Pass the \"verbose\" option for details.)"
+     else ":\n" ^ string)
 
 fun extract_delimited (begin_delim, end_delim) output =
   output |> first_field begin_delim |> the |> snd
diff -r 2a12d91a6ab7 -r 3cb52cbf0eed src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Mon Dec 20 23:36:58 2010 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Dec 21 01:12:17 2010 +0100
@@ -90,21 +90,18 @@
    account for the overhead of the script itself, which is in fact much
    lower. *)
 fun e_bonus () =
-  case getenv "E_VERSION" of
-    "" => 2000
-  | version =>
-    if exists (fn s => String.isPrefix s version) ["0.9", "1.0"] then 2000
-    else 1000
+  if string_ord (getenv "E_VERSION", "1.1") = LESS then 2000 else 1000
 
 val tstp_proof_delims =
   ("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation")
 
-val e_generate_weights = Unsynchronized.ref false
-val e_weight_factor = Unsynchronized.ref 60.0
+val e_generate_weights = Unsynchronized.ref true
+val e_weight_factor = Unsynchronized.ref 40.0
 val e_default_weight = Unsynchronized.ref 0.5
 
 fun e_weights weights =
-  if !e_generate_weights then
+  if !e_generate_weights andalso
+     string_ord (getenv "E_VERSION", "1.2B") <> LESS then
     "--split-clauses=4 --split-reuse-defs --simul-paramod --forward-context-sr \
     \--destructive-er-aggressive --destructive-er --presat-simplify \
     \--prefer-initial-clauses -tKBO6 -winvfreqrank -c1 -Ginvfreqconjmax -F1 \