# HG changeset patch
# User blanchet
# Date 1643716154 -3600
# Node ID 95e3aade547d95abd6a8c59573dd0693e878ff1e
# Parent  9e1d486e2d9f608d4350fb719815425fa8da218f
don't pass --auto-schedule to E indiscriminately -- use it instead of 'auto' in one slice

diff -r 9e1d486e2d9f -r 95e3aade547d src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Tue Feb 01 12:48:33 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Tue Feb 01 12:49:14 2022 +0100
@@ -28,8 +28,7 @@
   val default_max_mono_iters : int
   val default_max_new_mono_instances : int
   val term_order : string Config.T
-  val e_smartN : string
-  val e_autoN : string
+  val e_autoscheduleN : string
   val e_fun_weightN : string
   val e_sym_offset_weightN : string
   val e_default_fun_weight : real Config.T
@@ -204,8 +203,7 @@
 
 (* E *)
 
-val e_smartN = "smart"
-val e_autoN = "auto"
+val e_autoscheduleN = "auto"
 val e_fun_weightN = "fun_weight"
 val e_sym_offset_weightN = "sym_offset_weight"
 
@@ -256,7 +254,7 @@
     \1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*\
     \FIFOWeight(PreferProcessed))' "
   else
-    "-xAuto "
+    "--auto-schedule "
 
 val e_ord_weights = map (fn (s, w) => s ^ ":" ^ string_of_int w) #> space_implode ","
 fun e_ord_precedence [_] = ""
@@ -273,7 +271,7 @@
   {exec = (["E_HOME"], ["eprover-ho", "eprover"]),
    arguments = fn ctxt => fn _ => fn heuristic => fn timeout => fn problem =>
      fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) =>
-       ["--auto-schedule --tstp-in --tstp-out --silent " ^
+       ["--tstp-in --tstp-out --silent " ^
         e_selection_weight_arguments ctxt heuristic sel_weights ^
         e_term_order_info_arguments gen_weights gen_prec ord_info ^
         "--term-ordering=" ^ (if is_lpo then "LPO4" else "KBO6") ^ " " ^
@@ -301,7 +299,7 @@
        (* FUDGE *)
        K [((512, meshN), (format, type_enc, lam_trans, false, e_fun_weightN)),
         ((1024, meshN), (format, type_enc, lam_trans, false, e_sym_offset_weightN)),
-        ((128, mepoN), (format, type_enc, lam_trans, false, e_autoN)),
+        ((128, mepoN), (format, type_enc, lam_trans, false, e_autoscheduleN)),
         ((724, meshN), (format, "poly_guards??", lam_trans, false, e_sym_offset_weightN)),
         ((256, mepoN), (format, type_enc, liftingN, false, e_fun_weightN)),
         ((64, mashN), (format, type_enc, combsN, false, e_fun_weightN))]