--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Mar 20 13:53:09 2012 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Mar 20 13:53:09 2012 +0100
@@ -14,6 +14,7 @@
val lam_transK = "lam_trans"
val uncurried_aliasesK = "uncurried_aliases"
val e_selection_heuristicK = "e_selection_heuristic"
+val term_orderK = "term_order"
val force_sosK = "force_sos"
val max_relevantK = "max_relevant"
val max_callsK = "max_calls"
@@ -376,9 +377,9 @@
SH_ERROR
fun run_sh prover_name prover type_enc strict max_relevant slice lam_trans
- uncurried_aliases e_selection_heuristic force_sos hard_timeout
- timeout preplay_timeout sh_minimizeLST max_new_mono_instancesLST
- max_mono_itersLST dir pos st =
+ uncurried_aliases e_selection_heuristic term_order force_sos
+ hard_timeout timeout preplay_timeout sh_minimizeLST
+ max_new_mono_instancesLST max_mono_itersLST dir pos st =
let
val {context = ctxt, facts = chained_ths, goal} = Proof.goal st
val i = 1
@@ -396,6 +397,8 @@
(set_file_name dir
#> (Option.map (Config.put ATP_Systems.e_selection_heuristic)
e_selection_heuristic |> the_default I)
+ #> (Option.map (Config.put ATP_Systems.term_order)
+ term_order |> the_default I)
#> (Option.map (Config.put ATP_Systems.force_sos)
force_sos |> the_default I))
val params as {relevance_thresholds, max_relevant, slice, ...} =
@@ -493,6 +496,7 @@
val lam_trans = AList.lookup (op =) args lam_transK
val uncurried_aliases = AList.lookup (op =) args uncurried_aliasesK
val e_selection_heuristic = AList.lookup (op =) args e_selection_heuristicK
+ val term_order = AList.lookup (op =) args term_orderK
val force_sos = AList.lookup (op =) args force_sosK
|> Option.map (curry (op <>) "false")
val dir = AList.lookup (op =) args keepK
@@ -508,9 +512,9 @@
val hard_timeout = SOME (2 * timeout)
val (msg, result) =
run_sh prover_name prover type_enc strict max_relevant slice lam_trans
- uncurried_aliases e_selection_heuristic force_sos hard_timeout
- timeout preplay_timeout sh_minimizeLST max_new_mono_instancesLST
- max_mono_itersLST dir pos st
+ uncurried_aliases e_selection_heuristic term_order force_sos
+ hard_timeout timeout preplay_timeout sh_minimizeLST
+ max_new_mono_instancesLST max_mono_itersLST dir pos st
in
case result of
SH_OK (time_isa, time_prover, names) =>
--- a/src/HOL/Tools/ATP/atp_systems.ML Tue Mar 20 13:53:09 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML Tue Mar 20 13:53:09 2012 +0100
@@ -174,7 +174,7 @@
val xsimpN = "_simp" (* SPASS-specific *)
(* Possible values for "atp_term_order":
- "smart", "(kbo(_weights)?|lpo)(_prec|_simp)?" *)
+ "smart", "(kbo|lpo)(_weights)?(_prec|_simp)?" *)
val term_order =
Attrib.setup_config_string @{binding atp_term_order} (K smartN)