# HG changeset patch
# User blanchet
# Date 1572010361 -7200
# Node ID 3218999b3715cf8381597c67a63ea3fa9495752f
# Parent  6d84c3c333d5e2f9efc2710d1bae0a4f646d71a9
folded experimental Ehoh into E now that E 2.3 has been released

diff -r 6d84c3c333d5 -r 3218999b3715 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Fri Oct 25 15:23:14 2019 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Fri Oct 25 15:32:41 2019 +0200
@@ -49,7 +49,6 @@
   val alt_ergoN : string
   val eN : string
   val e_parN : string
-  val ehohN : string
   val iproverN : string
   val leo2N : string
   val leo3N : string
@@ -113,7 +112,6 @@
 val alt_ergoN = "alt_ergo"
 val eN = "e"
 val e_parN = "e_par"
-val ehohN = "ehoh"
 val iproverN = "iprover"
 val leo2N = "leo2"
 val leo3N = "leo3"
diff -r 6d84c3c333d5 -r 3218999b3715 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Fri Oct 25 15:23:14 2019 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Fri Oct 25 15:32:41 2019 +0200
@@ -261,8 +261,7 @@
   else
     "-xAuto "
 
-val e_ord_weights =
-  map (fn (s, w) => s ^ ":" ^ string_of_int w) #> space_implode ","
+val e_ord_weights = map (fn (s, w) => s ^ ":" ^ string_of_int w) #> space_implode ","
 fun e_ord_precedence [_] = ""
   | e_ord_precedence info = info |> map fst |> space_implode "<"
 
@@ -293,17 +292,23 @@
      known_szs_status_failures,
    prem_role = Conjecture,
    best_slices = fn ctxt =>
-     let val heuristic = Config.get ctxt e_selection_heuristic in
+     let
+       val heuristic = Config.get ctxt e_selection_heuristic
+       val ehoh = string_ord (getenv "E_VERSION", "2.3") <> LESS
+       val (format, enc) =
+         if ehoh then (THF (Monomorphic, THF_Predicate_Free), "mono_native_higher")
+         else (TFF Monomorphic, "mono_native")
+     in
        (* FUDGE *)
        if heuristic = e_smartN then
-         [(0.15, (((128, meshN), TFF Monomorphic, "mono_native", combsN, false), e_fun_weightN)),
-          (0.15, (((128, mashN), TFF Monomorphic, "mono_native", combsN, false), e_sym_offset_weightN)),
-          (0.15, (((91, mepoN), TFF Monomorphic, "mono_native", combsN, false), e_autoN)),
-          (0.15, (((1000, meshN), TFF Monomorphic, "poly_guards??", combsN, false), e_sym_offset_weightN)),
-          (0.15, (((256, mepoN), TFF Monomorphic, "mono_native", liftingN, false), e_fun_weightN)),
-          (0.25, (((64, mashN), TFF Monomorphic, "mono_native", combsN, false), e_fun_weightN))]
+         [(0.15, (((128, meshN), format, enc, combsN, false), e_fun_weightN)),
+          (0.15, (((128, mashN), format, enc, combsN, false), e_sym_offset_weightN)),
+          (0.15, (((91, mepoN), format, enc, combsN, false), e_autoN)),
+          (0.15, (((1000, meshN), format, "poly_guards??", combsN, false), e_sym_offset_weightN)),
+          (0.15, (((256, mepoN), format, enc, liftingN, false), e_fun_weightN)),
+          (0.25, (((64, mashN), format, enc, combsN, false), e_fun_weightN))]
        else
-         [(1.0, (((500, ""), TFF Monomorphic, "mono_native", combsN, false), heuristic))]
+         [(1.0, (((500, ""), format, enc, combsN, false), heuristic))]
      end,
    best_max_mono_iters = default_max_mono_iters,
    best_max_new_mono_instances = default_max_new_mono_instances}
@@ -332,30 +337,6 @@
 val e_par = (e_parN, fn () => e_par_config)
 
 
-(* Ehoh *)
-
-val ehoh_config : atp_config =
-  {exec = fn _ => (["E_HOME"], ["eprover"]),
-   arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
-     "--auto-schedule --tstp-in --tstp-out --silent --cpu-limit=" ^
-     string_of_int (to_secs 2 timeout) ^ " --proof-object=1 " ^ file_name,
-   proof_delims =
-     [("# SZS output start CNFRefutation", "# SZS output end CNFRefutation")] @
-     tstp_proof_delims,
-   known_failures =
-     [(TimedOut, "Failure: Resource limit exceeded (time)"),
-      (TimedOut, "time limit exceeded")] @
-     known_szs_status_failures,
-   prem_role = Hypothesis,
-   best_slices =
-     (* FUDGE *)
-     K [(1.0, (((500, ""), THF (Monomorphic, THF_Predicate_Free), "mono_native_higher", liftingN, false), ""))],
-   best_max_mono_iters = default_max_mono_iters,
-   best_max_new_mono_instances = default_max_new_mono_instances}
-
-val ehoh = (ehohN, fn () => ehoh_config)
-
-
 (* iProver *)
 
 val iprover_config : atp_config =
@@ -754,7 +735,7 @@
   end
 
 val atps =
-  [agsyhol, alt_ergo, e, e_par, ehoh, iprover, leo2, leo3, satallax, spass, vampire, z3_tptp,
+  [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]