tweaked Vampire's options + tuning
authorblanchet
Thu, 23 Apr 2020 15:45:42 +0200
changeset 72011 e771b8157fc7
parent 72010 936718dede80
child 72012 ac28714b7478
tweaked Vampire's options + tuning
src/HOL/ATP.thy
src/HOL/Sledgehammer.thy
src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/ATP.thy	Thu Apr 23 13:49:46 2020 +0200
+++ b/src/HOL/ATP.thy	Thu Apr 23 15:45:42 2020 +0200
@@ -137,6 +137,5 @@
 ML_file \<open>Tools/monomorph.ML\<close>
 ML_file \<open>Tools/ATP/atp_problem_generate.ML\<close>
 ML_file \<open>Tools/ATP/atp_proof_reconstruct.ML\<close>
-ML_file \<open>Tools/ATP/atp_systems.ML\<close>
 
 end
--- a/src/HOL/Sledgehammer.thy	Thu Apr 23 13:49:46 2020 +0200
+++ b/src/HOL/Sledgehammer.thy	Thu Apr 23 15:45:42 2020 +0200
@@ -16,6 +16,7 @@
 lemma size_ne_size_imp_ne: "size x \<noteq> size y \<Longrightarrow> x \<noteq> y"
   by (erule contrapos_nn) (rule arg_cong)
 
+ML_file \<open>Tools/ATP/atp_systems.ML\<close>
 ML_file \<open>Tools/Sledgehammer/async_manager_legacy.ML\<close>
 ML_file \<open>Tools/Sledgehammer/sledgehammer_util.ML\<close>
 ML_file \<open>Tools/Sledgehammer/sledgehammer_fact.ML\<close>
--- a/src/HOL/Tools/ATP/atp_systems.ML	Thu Apr 23 13:49:46 2020 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu Apr 23 15:45:42 2020 +0200
@@ -453,7 +453,7 @@
       (InternalError, "Please report this error")] @
       known_perl_failures,
    prem_role = Conjecture,
-   best_slices = fn ctxt =>
+   best_slices = fn _ =>
      (* FUDGE *)
      [(0.1667, (((150, meshN), DFG Monomorphic, "mono_native", combsN, true), "")),
       (0.1667, (((500, meshN), DFG Monomorphic, "mono_native", liftingN, true), spass_H2SOS)),
@@ -499,7 +499,7 @@
 val vampire_basic_options = "--proof tptp --output_axiom_names on $VAMPIRE_EXTRA_OPTIONS"
 
 val vampire_full_proof_options =
-  " --forced_options equality_proxy=off:general_splitting=off:inequality_splitting=0:naming=0"
+  " --proof_extra free --forced_options avatar=off:equality_proxy=off:general_splitting=off:inequality_splitting=0:naming=0"
 
 val remote_vampire_command =
   "vampire " ^ vampire_basic_options ^ " " ^ vampire_full_proof_options ^ " -t %d %s"