# HG changeset patch
# User blanchet
# Date 1332247989 -3600
# Node ID 72bd3311ecba15d52e45c09da5ff02e7c8d31830
# Parent  3347c853d8e2bd7554af32932bb22f22f5b00347
added term_order option to Mirabelle

diff -r 3347c853d8e2 -r 72bd3311ecba src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- 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) =>
diff -r 3347c853d8e2 -r 72bd3311ecba src/HOL/Tools/ATP/atp_systems.ML
--- 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)