# HG changeset patch
# User blanchet
# Date 1314108421 -7200
# Node ID f74707e12d30348eda0e014a1ba64c7ccc02cb66
# Parent  1b0a31b7cfe877dc0a41d9a43e0df8653c0e17ea
exploit TFF format in Z3 used as ATP, and renamed it "z3_tptp"

diff -r 1b0a31b7cfe8 -r f74707e12d30 doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Tue Aug 23 15:50:27 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Tue Aug 23 16:07:01 2011 +0200
@@ -765,8 +765,8 @@
 name, and set \texttt{Z3\_NON\_COMMERCIAL} to ``yes'' to confirm that you are a
 noncommercial user. Sledgehammer has been tested with versions 2.7 to 2.18.
 
-\item[$\bullet$] \textbf{\textit{z3\_atp}:} This version of Z3 pretends to be an
-ATP, exploiting Z3's support for the TPTP untyped and many-typed first-order
+\item[$\bullet$] \textbf{\textit{z3\_tptp}:} This version of Z3 pretends to be
+an ATP, exploiting Z3's support for the TPTP untyped and many-typed first-order
 formats (FOF and TFF). It is included for experimental purposes. It requires
 version 3.0 or above.
 \end{enum}
@@ -814,8 +814,8 @@
 servers at the TU M\"unchen (or wherever \texttt{REMOTE\_SMT\_URL} is set to
 point).
 
-\item[$\bullet$] \textbf{\textit{remote\_z3\_atp}:} The remote version of ``Z3
-as an ATP'' runs on Geoff Sutcliffe's Miami servers.
+\item[$\bullet$] \textbf{\textit{remote\_z3\_tptp}:} The remote version of ``Z3
+with TPTP syntax'' runs on Geoff Sutcliffe's Miami servers.
 \end{enum}
 
 By default, Sledgehammer will run E, E-SInE, SPASS, Vampire, Z3 (or whatever
diff -r 1b0a31b7cfe8 -r f74707e12d30 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 23 15:50:27 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 23 16:07:01 2011 +0200
@@ -45,7 +45,7 @@
   val snarkN : string
   val e_tofofN : string
   val waldmeisterN : string
-  val z3_atpN : string
+  val z3_tptpN : string
   val remote_prefix : string
   val remote_atp :
     string -> string -> string list -> (string * string) list
@@ -104,7 +104,7 @@
 val satallaxN = "satallax"
 val spassN = "spass"
 val vampireN = "vampire"
-val z3_atpN = "z3_atp"
+val z3_tptpN = "z3_tptp"
 val e_sineN = "e_sine"
 val snarkN = "snark"
 val e_tofofN = "e_tofof"
@@ -349,7 +349,7 @@
 
 (* Z3 with TPTP syntax *)
 
-val z3_atp_config : atp_config =
+val z3_tptp_config : atp_config =
   {exec = ("Z3_HOME", "z3"),
    required_execs = [],
    arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
@@ -364,13 +364,13 @@
    conj_sym_kind = Hypothesis,
    prem_kind = Hypothesis,
    best_slices =
-     (* FUDGE (FIXME) *)
-     K [(0.5, (false, (250, FOF, "mangled_guards?", ""))),
-        (0.25, (false, (125, FOF, "mangled_guards?", ""))),
-        (0.125, (false, (62, FOF, "mangled_guards?", ""))),
-        (0.125, (false, (31, FOF, "mangled_guards?", "")))]}
+     (* FUDGE *)
+     K [(0.5, (false, (250, TFF, "simple", ""))),
+        (0.25, (false, (125, TFF, "simple", ""))),
+        (0.125, (false, (62, TFF, "simple", ""))),
+        (0.125, (false, (31, TFF, "simple", "")))]}
 
-val z3_atp = (z3_atpN, z3_atp_config)
+val z3_tptp = (z3_tptpN, z3_tptp_config)
 
 
 (* Remote ATP invocation via SystemOnTPTP *)
@@ -457,9 +457,8 @@
                (K (100, THF With_Choice, "simple_higher") (* FUDGE *))
 val remote_vampire =
   remotify_atp vampire "Vampire" ["1.8"] (K (250, TFF, "simple") (* FUDGE *))
-val remote_z3_atp =
-  remotify_atp z3_atp "Z3" ["2.18"]
-               (K (250, FOF, "mangled_guards?") (* FUDGE *))
+val remote_z3_tptp =
+  remotify_atp z3_tptp "Z3" ["3.0"] (K (250, TFF, "simple") (* FUDGE *))
 val remote_e_sine =
   remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
              Conjecture (K (500, FOF, "mangled_guards?") (* FUDGE *))
@@ -499,8 +498,8 @@
   Synchronized.change systems (fn _ => get_systems ())
 
 val atps =
-  [e, leo2, satallax, spass, vampire, z3_atp, remote_e, remote_leo2,
-   remote_satallax, remote_vampire, remote_z3_atp, remote_e_sine, remote_snark,
+  [e, leo2, satallax, spass, vampire, z3_tptp, remote_e, remote_leo2,
+   remote_satallax, remote_vampire, remote_z3_tptp, remote_e_sine, remote_snark,
    remote_e_tofof, remote_waldmeister]
 val setup = fold add_atp atps
 
diff -r 1b0a31b7cfe8 -r f74707e12d30 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Aug 23 15:50:27 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Aug 23 16:07:01 2011 +0200
@@ -536,7 +536,7 @@
   #> Config.put Monomorph.max_new_instances max_new_instances
   #> Config.put Monomorph.keep_partial_instances false
 
-(* Give the ATPs some slack before interrupting them the hard way. "z3_atp" on
+(* Give the ATPs some slack before interrupting them the hard way. "z3_tptp" on
    Linux appears to be the only ATP that does not honor its time limit. *)
 val atp_timeout_slack = seconds 1.0