# HG changeset patch
# User blanchet
# Date 1343895029 -7200
# Node ID 6ac7fd9b3a54e8cc63f372a2106dac102515125a
# Parent  15f0cf52deea57e6ffd01d61d8f726a8ed162f6c
support older versions of Vampire

diff -r 15f0cf52deea -r 6ac7fd9b3a54 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Thu Aug 02 10:10:29 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu Aug 02 10:10:29 2012 +0200
@@ -211,8 +211,8 @@
 
 (* E *)
 
-fun is_recent_e_version () = (string_ord (getenv "E_VERSION", "1.3") <> LESS)
-fun is_new_e_version () = (string_ord (getenv "E_VERSION", "1.6") <> LESS)
+fun is_e_at_least_1_3 () = (string_ord (getenv "E_VERSION", "1.3") <> LESS)
+fun is_e_at_least_1_6 () = (string_ord (getenv "E_VERSION", "1.6") <> LESS)
 
 val tstp_proof_delims =
   [("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation"),
@@ -289,16 +289,16 @@
     end
 
 fun e_shell_level_argument full_proof =
-  if is_new_e_version () then
+  if is_e_at_least_1_6 () then
     " --pcl-shell-level=" ^ (if full_proof then "0" else "2")
   else
     ""
 
 fun effective_e_selection_heuristic ctxt =
-  if is_recent_e_version () then Config.get ctxt e_selection_heuristic
+  if is_e_at_least_1_3 () then Config.get ctxt e_selection_heuristic
   else e_autoN
 
-fun e_kbo () = if is_recent_e_version () then "KBO6" else "KBO"
+fun e_kbo () = if is_e_at_least_1_3 () then "KBO6" else "KBO"
 
 val e_config : atp_config =
   {exec = (["E_HOME"], ["eproof_ram", "eproof"]),
@@ -445,7 +445,9 @@
 
 (* Vampire 1.8 has TFF support, but the support was buggy until revision
    1435 (or shortly before). *)
-fun is_new_vampire_version () =
+fun is_vampire_at_least_1_8 () =
+  string_ord (getenv "VAMPIRE_VERSION", "1.8") <> LESS
+fun is_vampire_beyond_1_8 () =
   string_ord (getenv "VAMPIRE_VERSION", "1.8") = GREATER
 
 val vampire_tff0 = TFF (Monomorphic, TPTP_Implicit)
@@ -454,9 +456,12 @@
   {exec = (["VAMPIRE_HOME"], ["vampire"]),
    arguments = fn _ => fn _ => fn sos => fn timeout => fn _ =>
        "--mode casc -t " ^ string_of_int (to_secs 1 timeout) ^
-       " --proof tptp --output_axiom_names on\
-       \ --forced_options propositional_to_bdd=off\
-       \ --thanks \"Andrei and Krystof\" --input_file"
+       " --proof tptp --output_axiom_names on" ^
+       (if is_vampire_at_least_1_8 () then
+          " --forced_options propositional_to_bdd=off"
+        else
+          "") ^
+       " --thanks \"Andrei and Krystof\" --input_file"
        |> sos = sosN ? prefix "--sos on ",
    proof_delims =
      [("=========== Refutation ==========",
@@ -473,7 +478,7 @@
    prem_role = Conjecture,
    best_slices = fn ctxt =>
      (* FUDGE *)
-     (if is_new_vampire_version () then
+     (if is_vampire_beyond_1_8 () then
         [(0.333, (false, ((500, vampire_tff0, "mono_native", combs_or_liftingN, false), sosN))),
          (0.333, (false, ((150, vampire_tff0, "poly_guards??", combs_or_liftingN, false), sosN))),
          (0.334, (true, ((50, vampire_tff0, "mono_native", combs_or_liftingN, false), no_sosN)))]