# HG changeset patch
# User blanchet
# Date 1572011965 -7200
# Node ID ce3a05ad07b7f2d3d6d958109829385a33fa8d37
# Parent  3218999b3715cf8381597c67a63ea3fa9495752f
added support for Zipperposition on SystemOnTPTP

diff -r 3218999b3715 -r ce3a05ad07b7 src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Fri Oct 25 15:32:41 2019 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex	Fri Oct 25 15:59:25 2019 +0200
@@ -148,9 +148,10 @@
 
 Among the ATPs, agsyHOL, Alt-Ergo, E, LEO-II, Leo-III, Satallax, SPASS,
 Vampire, and Zipperposition can be run locally; in addition, agsyHOL,
-Alt-Ergo, E, iProver, LEO-II, Leo-III, Satallax, SNARK, Vampire, and
-Waldmeister are available remotely via System\-On\-TPTP \cite{sutcliffe-2000}.
-The SMT solvers CVC3, CVC4, veriT, and Z3 can be run locally.
+Alt-Ergo, E, iProver, LEO-II, Leo-III, Satallax, SNARK, Vampire, Waldmeister,
+and Zipperposition are available remotely via System\-On\-TPTP
+\cite{sutcliffe-2000}. The SMT solvers CVC3, CVC4, veriT, and Z3 can be run
+locally.
 
 There are three main ways to install automatic provers on your machine:
 
@@ -881,12 +882,15 @@
 used to prove universally quantified equations using unconditional equations,
 corresponding to the TPTP CNF UEQ division. The remote version of Waldmeister
 runs on Geoff Sutcliffe's Miami servers.
+
+\item[\labelitemi] \textbf{\textit{remote\_zipperposition}:} The remote
+version of Zipperposition runs on Geoff Sutcliffe's Miami servers.
 \end{enum}
 
 By default, Sledgehammer runs a subset of CVC4, E, SPASS, Vampire, veriT, and
 Z3 in parallel, either locally or remotely---depending on the number of
 processor cores available and on which provers are actually installed. It is
-generally a good idea to run several provers in parallel.
+generally desirable to run several provers in parallel.
 
 \opnodefault{prover}{string}
 Alias for \textit{provers}.
diff -r 3218999b3715 -r ce3a05ad07b7 src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Fri Oct 25 15:32:41 2019 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Fri Oct 25 15:59:25 2019 +0200
@@ -505,13 +505,13 @@
 fun is_axiom_used_in_proof pred =
   exists (fn ((_, ss), _, _, _, []) => exists pred ss | _ => false)
 
-fun add_fact ctxt facts ((_, ss), _, _, rule, deps) =
+fun add_fact ctxt facts ((num, ss), _, _, rule, deps) =
   (if member (op =) [agsyhol_core_rule, leo2_extcnf_equal_neg_rule] rule orelse
       String.isPrefix satallax_tab_rule_prefix rule then
      insert (op =) (short_thm_name ctxt ext, (Global, General))
    else
      I)
-  #> (if null deps then union (op =) (resolve_facts facts ss) else I)
+  #> (if null deps then union (op =) (resolve_facts facts (num :: ss)) else I)
 
 fun used_facts_in_atp_proof ctxt facts atp_proof =
   if null atp_proof then facts else fold (add_fact ctxt facts) atp_proof []
@@ -776,7 +776,7 @@
             if j = length hyp_ts then ([], Conjecture, concl_t)
             else ([], Hypothesis, close_form (nth hyp_ts j))
           | _ =>
-            (case resolve_facts facts ss of
+            (case resolve_facts facts (num :: ss) of
               [] => (ss, if role = Lemma then Lemma else Plain, t)
             | facts => (map fst facts, Axiom, t)))
       in
diff -r 3218999b3715 -r ce3a05ad07b7 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Fri Oct 25 15:32:41 2019 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Fri Oct 25 15:59:25 2019 +0200
@@ -398,7 +398,7 @@
    prem_role = Hypothesis,
    best_slices =
      (* FUDGE *)
-     K [(1.0, (((150, ""), THF (Polymorphic, THF_Without_Choice), "poly_native_higher", keep_lamsN, false), ""))],
+     K [(1.0, (((150, ""), THF (Polymorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), ""))],
    best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
    best_max_new_mono_instances = default_max_new_mono_instances}
 
@@ -577,7 +577,7 @@
    prem_role = Hypothesis,
    best_slices = fn _ =>
      (* FUDGE *)
-     [(1.0, (((100, ""), THF (Polymorphic, THF_Predicate_Free), "poly_native_higher", keep_lamsN, false), ""))],
+     [(1.0, (((250, ""), THF (Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), ""))],
    best_max_mono_iters = default_max_mono_iters,
    best_max_new_mono_instances = default_max_new_mono_instances}
 
@@ -700,6 +700,9 @@
   remotify_atp vampire "Vampire" ["4.2", "4.1", "4.0"]
     (K (((400, ""), TFF Monomorphic, "mono_native", combs_or_liftingN, false), remote_vampire_full_proof_command) (* FUDGE *))
 val remote_waldmeister = gen_remote_waldmeister waldmeisterN "raw_mono_tags??"
+val remote_zipperposition =
+  remotify_atp zipperposition "Zipperpin" ["1.5"]
+    (K (((250, ""), THF (Monomorphic, THF_Without_Choice), "poly_native_higher", keep_lamsN, false), "") (* FUDGE *))
 
 
 (* Setup *)
@@ -737,7 +740,8 @@
 val atps =
   [agsyhol, alt_ergo, e, e_par, iprover, leo2, leo3, satallax, spass, vampire, z3_tptp,
    zipperposition, remote_agsyhol, remote_alt_ergo, remote_e, remote_iprover, remote_leo2,
-   remote_leo3, remote_vampire, remote_snark, remote_pirate, remote_waldmeister]
+   remote_leo3, remote_pirate, remote_snark, remote_vampire, remote_waldmeister,
+   remote_zipperposition]
 
 val _ = Theory.setup (fold add_atp atps)