disabled 'ite' in Zipperposition until we upgrade to a version of Zip that supports it and we generate the proper syntax
authorblanchet
Fri, 27 Aug 2021 14:28:56 +0200
changeset 74485 9c6159cbf9ee
parent 74481 5f0f0553762f
child 74486 adf767b94f77
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	Thu Aug 26 23:23:16 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Fri Aug 27 14:28:56 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