rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does
authorblanchet
Mon, 19 Apr 2010 10:45:08 +0200
changeset 36220 f3655a3ae1ab
parent 36219 16670b4f0baa
child 36221 3abbae8a10cd
rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does
src/HOL/Tools/ATP_Manager/atp_manager.ML
src/HOL/Tools/ATP_Manager/atp_wrapper.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Mon Apr 19 10:15:02 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Mon Apr 19 10:45:08 2010 +0200
@@ -18,7 +18,7 @@
      respect_no_atp: bool,
      relevance_threshold: real,
      convergence: real,
-     theory_const: bool option,
+     theory_relevant: bool option,
      higher_order: bool option,
      follow_defs: bool,
      isar_proof: bool,
@@ -71,7 +71,7 @@
    respect_no_atp: bool,
    relevance_threshold: real,
    convergence: real,
-   theory_const: bool option,
+   theory_relevant: bool option,
    higher_order: bool option,
    follow_defs: bool,
    isar_proof: bool,
--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Mon Apr 19 10:15:02 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Mon Apr 19 10:45:08 2010 +0200
@@ -48,7 +48,7 @@
   arguments: Time.time -> string,
   failure_strs: string list,
   max_new_clauses: int,
-  prefers_theory_const: bool,
+  prefers_theory_relevant: bool,
   supports_isar_proofs: bool};
 
 
@@ -167,15 +167,15 @@
 
 fun generic_tptp_prover
         (name, {command, arguments, failure_strs, max_new_clauses,
-                prefers_theory_const, supports_isar_proofs})
+                prefers_theory_relevant, supports_isar_proofs})
         (params as {overlord, respect_no_atp, relevance_threshold, convergence,
-                    theory_const, higher_order, follow_defs, isar_proof,
+                    theory_relevant, higher_order, follow_defs, isar_proof,
                     modulus, sorts, ...})
         timeout =
   generic_prover overlord
       (get_relevant_facts respect_no_atp relevance_threshold convergence
                           higher_order follow_defs max_new_clauses
-                          (the_default prefers_theory_const theory_const))
+                          (the_default prefers_theory_relevant theory_relevant))
       (prepare_clauses higher_order false) write_tptp_file command
       (arguments timeout) failure_strs
       (if supports_isar_proofs andalso isar_proof then
@@ -201,7 +201,7 @@
    failure_strs =
      ["Satisfiability detected", "Refutation not found", "CANNOT PROVE"],
    max_new_clauses = 60,
-   prefers_theory_const = false,
+   prefers_theory_relevant = false,
    supports_isar_proofs = true}
 val vampire = tptp_prover "vampire" vampire_config
 
@@ -218,7 +218,7 @@
         "SZS status: ResourceOut", "SZS status ResourceOut",
         "# Cannot determine problem status"],
    max_new_clauses = 100,
-   prefers_theory_const = false,
+   prefers_theory_relevant = false,
    supports_isar_proofs = true}
 val e = tptp_prover "e" e_config
 
@@ -227,14 +227,14 @@
 
 fun generic_dfg_prover
         (name, ({command, arguments, failure_strs, max_new_clauses,
-                 prefers_theory_const, ...} : prover_config))
+                 prefers_theory_relevant, ...} : prover_config))
         (params as {overlord, respect_no_atp, relevance_threshold, convergence,
-                    theory_const, higher_order, follow_defs, ...})
+                    theory_relevant, higher_order, follow_defs, ...})
         timeout =
   generic_prover overlord
       (get_relevant_facts respect_no_atp relevance_threshold convergence
                           higher_order follow_defs max_new_clauses
-                          (the_default prefers_theory_const theory_const))
+                          (the_default prefers_theory_relevant theory_relevant))
       (prepare_clauses higher_order true) write_dfg_file command
       (arguments timeout) failure_strs (metis_lemma_list true) name params;
 
@@ -251,7 +251,7 @@
     ["SPASS beiseite: Completion found.", "SPASS beiseite: Ran out of time.",
      "SPASS beiseite: Maximal number of loops exceeded."],
   max_new_clauses = 40,
-  prefers_theory_const = true,
+  prefers_theory_relevant = true,
   supports_isar_proofs = false}
 val spass = dfg_prover ("spass", spass_config)
 
@@ -285,7 +285,7 @@
 val remote_failure_strs = ["Remote-script could not extract proof"];
 
 fun remote_prover_config prover_prefix args
-        ({failure_strs, max_new_clauses, prefers_theory_const, ...}
+        ({failure_strs, max_new_clauses, prefers_theory_relevant, ...}
          : prover_config) : prover_config =
   {command = Path.explode "$ISABELLE_ATP_MANAGER/SystemOnTPTP",
    arguments = (fn timeout =>
@@ -293,7 +293,7 @@
      the_system prover_prefix),
    failure_strs = remote_failure_strs @ failure_strs,
    max_new_clauses = max_new_clauses,
-   prefers_theory_const = prefers_theory_const,
+   prefers_theory_relevant = prefers_theory_relevant,
    supports_isar_proofs = false}
 
 val remote_vampire =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Mon Apr 19 10:15:02 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Mon Apr 19 10:45:08 2010 +0200
@@ -127,8 +127,8 @@
 
 (*Inserts a dummy "constant" referring to the theory name, so that relevance
   takes the given theory into account.*)
-fun const_prop_of theory_const th =
- if theory_const then
+fun const_prop_of theory_relevant th =
+ if theory_relevant then
   let val name = Context.theory_name (theory_of_thm th)
       val t = Const (name ^ ". 1", HOLogic.boolT)
   in  t $ prop_of th  end
@@ -157,7 +157,7 @@
 
 structure CTtab = Table(type key = const_typ list val ord = dict_ord const_typ_ord);
 
-fun count_axiom_consts theory_const thy ((thm,_), tab) = 
+fun count_axiom_consts theory_relevant thy ((thm,_), tab) = 
   let fun count_const (a, T, tab) =
         let val (c, cts) = const_with_typ thy (a,T)
         in  (*Two-dimensional table update. Constant maps to types maps to count.*)
@@ -170,7 +170,7 @@
             count_term_consts (t, count_term_consts (u, tab))
         | count_term_consts (Abs(_,_,t), tab) = count_term_consts (t, tab)
         | count_term_consts (_, tab) = tab
-  in  count_term_consts (const_prop_of theory_const thm, tab)  end;
+  in  count_term_consts (const_prop_of theory_relevant thm, tab)  end;
 
 
 (**** Actual Filtering Code ****)
@@ -201,8 +201,8 @@
   let val tab = add_term_consts_typs_rm thy (t, null_const_tab)
   in  Symtab.fold add_expand_pairs tab []  end;
 
-fun pair_consts_typs_axiom theory_const thy (p as (thm, _)) =
-  (p, (consts_typs_of_term thy (const_prop_of theory_const thm)));
+fun pair_consts_typs_axiom theory_relevant thy (p as (thm, _)) =
+  (p, (consts_typs_of_term thy (const_prop_of theory_relevant thm)));
 
 exception ConstFree;
 fun dest_ConstFree (Const aT) = aT
@@ -294,10 +294,10 @@
   in iter end
         
 fun relevance_filter ctxt relevance_threshold convergence follow_defs max_new
-                     theory_const relevance_override thy axioms goals = 
+                     theory_relevant relevance_override thy axioms goals = 
   if relevance_threshold > 0.0 then
     let
-      val const_tab = List.foldl (count_axiom_consts theory_const thy)
+      val const_tab = List.foldl (count_axiom_consts theory_relevant thy)
                                  Symtab.empty axioms
       val goal_const_tab = get_goal_consts_typs thy goals
       val _ =
@@ -306,7 +306,8 @@
       val relevant =
         relevant_clauses ctxt convergence follow_defs max_new relevance_override
                          thy const_tab relevance_threshold goal_const_tab
-                         (map (pair_consts_typs_axiom theory_const thy) axioms)
+                         (map (pair_consts_typs_axiom theory_relevant thy)
+                              axioms)
     in
       trace_msg (fn () => "Total relevant: " ^ Int.toString (length relevant));
       relevant
@@ -502,7 +503,7 @@
   | SOME b => not b
 
 fun get_relevant_facts respect_no_atp relevance_threshold convergence
-                       higher_order follow_defs max_new theory_const
+                       higher_order follow_defs max_new theory_relevant
                        (relevance_override as {add, only, ...})
                        (ctxt, (chain_ths, th)) goal_cls =
   if (only andalso null add) orelse relevance_threshold > 1.0 then
@@ -517,7 +518,7 @@
         |> remove_unwanted_clauses
     in
       relevance_filter ctxt relevance_threshold convergence follow_defs max_new
-                       theory_const relevance_override thy included_cls
+                       theory_relevant relevance_override thy included_cls
                        (map prop_of goal_cls)
     end
 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Apr 19 10:15:02 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Apr 19 10:45:08 2010 +0200
@@ -44,7 +44,7 @@
    ("respect_no_atp", "true"),
    ("relevance_threshold", "50"),
    ("convergence", "320"),
-   ("theory_const", "smart"),
+   ("theory_relevant", "smart"),
    ("higher_order", "smart"),
    ("follow_defs", "false"),
    ("isar_proof", "false"),
@@ -60,7 +60,7 @@
    ("no_overlord", "overlord"),
    ("ignore_no_atp", "respect_no_atp"),
    ("partial_types", "full_types"),
-   ("no_theory_const", "theory_const"),
+   ("theory_irrelevant", "theory_relevant"),
    ("first_order", "higher_order"),
    ("dont_follow_defs", "follow_defs"),
    ("metis_proof", "isar_proof"),
@@ -150,7 +150,7 @@
     val relevance_threshold =
       0.01 * Real.fromInt (lookup_int "relevance_threshold")
     val convergence = 0.01 * Real.fromInt (lookup_int "convergence")
-    val theory_const = lookup_bool_option "theory_const"
+    val theory_relevant = lookup_bool_option "theory_relevant"
     val higher_order = lookup_bool_option "higher_order"
     val follow_defs = lookup_bool "follow_defs"
     val isar_proof = lookup_bool "isar_proof"
@@ -162,7 +162,7 @@
     {debug = debug, verbose = verbose, overlord = overlord, atps = atps,
      full_types = full_types, respect_no_atp = respect_no_atp,
      relevance_threshold = relevance_threshold, convergence = convergence,
-     theory_const = theory_const, higher_order = higher_order,
+     theory_relevant = theory_relevant, higher_order = higher_order,
      follow_defs = follow_defs, isar_proof = isar_proof, modulus = modulus,
      sorts = sorts, timeout = timeout, minimize_timeout = minimize_timeout}
   end