disabled 'ite' in Zipperposition until we upgrade to a version of Zip that supports it and we generate the proper syntax draft
authorblanchet
Fri, 27 Aug 2021 13:02:52 +0200
changeset 74483 f218d52d3202
parent 74482 1e3d96cf52f2
child 74484 a175a39e0020
disabled 'ite' in Zipperposition until we upgrade to a version of Zip that supports it and we generate the proper syntax
src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Fri Aug 27 11:31:36 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Fri Aug 27 13:02:52 2021 +0200
@@ -550,7 +550,7 @@
 
 val zipperposition_config : atp_config =
   let
-    val format = THF (With_FOOL, Polymorphic, THF_Without_Choice)
+    val format = THF (Without_FOOL, Polymorphic, THF_Without_Choice)
   in
     {exec = (["ZIPPERPOSITION_HOME"], ["zipperposition"]),
      arguments = fn _ => fn _ => fn extra_options => fn timeout => fn problem => fn _ =>
@@ -561,9 +561,9 @@
      prem_role = Hypothesis,
      best_slices = fn _ =>
        (* FUDGE *)
-       [(0.333, (((128, "meshN"), format, "mono_native_higher_fool", keep_lamsN, false), zipperposition_blsimp)),
-        (0.333, (((32, "meshN"), format, "poly_native_higher_fool", keep_lamsN, false), zipperposition_s6)),
-        (0.334, (((512, "meshN"), format, "mono_native_higher_fool", keep_lamsN, false), zipperposition_cdots))],
+       [(0.333, (((128, "meshN"), format, "mono_native_higher", keep_lamsN, false), zipperposition_blsimp)),
+        (0.333, (((32, "meshN"), format, "poly_native_higher", keep_lamsN, false), zipperposition_s6)),
+        (0.334, (((512, "meshN"), format, "mono_native_higher", keep_lamsN, false), zipperposition_cdots))],
      best_max_mono_iters = default_max_mono_iters,
      best_max_new_mono_instances = default_max_new_mono_instances}
   end