# HG changeset patch
# User blanchet
# Date 1314105343 -7200
# Node ID 3d0921b91a8643d57935ee2d6618a6dd6be343c8
# Parent  a460810d743ee8c755261be64d971175d70954ca
avoid TFF format with older Vampire versions

diff -r a460810d743e -r 3d0921b91a86 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 23 14:57:16 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 23 15:15:43 2011 +0200
@@ -130,6 +130,8 @@
 
 (* E *)
 
+fun is_old_e_version () = (string_ord (getenv "E_VERSION", "1.2w") = LESS)
+
 val tstp_proof_delims =
   [("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation"),
    ("% SZS output start CNFRefutation", "% SZS output end CNFRefutation")]
@@ -188,8 +190,6 @@
     \1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*\
     \FIFOWeight(PreferProcessed))'"
 
-fun is_old_e_version () = (string_ord (getenv "E_VERSION", "1.2w") = LESS)
-
 fun effective_e_weight_method ctxt =
   if is_old_e_version () then e_autoN else Config.get ctxt e_weight_method
 
@@ -304,6 +304,9 @@
 
 (* Vampire *)
 
+fun is_old_vampire_version () =
+  string_ord (getenv "VAMPIRE_VERSION", "1.8") = LESS
+
 val vampire_config : atp_config =
   {exec = ("VAMPIRE_HOME", "vampire"),
    required_execs = [],
@@ -331,9 +334,13 @@
    prem_kind = Conjecture,
    best_slices = fn ctxt =>
      (* FUDGE *)
-     [(0.333, (false, (150, TFF, "poly_guards", sosN))),
-      (0.334, (true, (50, TFF, "mangled_guards?", no_sosN))),
-      (0.333, (false, (500, TFF, "mangled_tags?", sosN)))]
+     (0.333, (false, (150, FOF, "poly_guards", sosN))) ::
+     (if is_old_vampire_version () then
+        [(0.334, (true, (50, FOF, "mangled_guards?", no_sosN))),
+         (0.333, (false, (500, FOF, "mangled_tags?", sosN)))]
+      else
+        [(0.334, (true, (50, TFF, "simple", no_sosN))),
+         (0.333, (false, (500, TFF, "simple", sosN)))])
      |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
          else I)}
 
@@ -346,7 +353,7 @@
   {exec = ("Z3_HOME", "z3"),
    required_execs = [],
    arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
-     "MBQI=true -p -t:" ^ string_of_int (to_secs 1 timeout),
+     "MBQI=true -tptp -t:" ^ string_of_int (to_secs 1 timeout),
    proof_delims = [],
    known_failures =
      [(Unprovable, "\nsat"),