prevent double inclusion of the fact "True_or_False" in TPTP problems
authorblanchet
Mon Aug 23 16:12:41 2010 +0200 (2010-08-23)
changeset 386781bf1e21d3136
parent 38654 0b1a63d06805
child 38679 2cfd0777580f
prevent double inclusion of the fact "True_or_False" in TPTP problems
src/HOL/Tools/ATP/atp_systems.ML
src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Mon Aug 23 15:30:42 2010 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Mon Aug 23 16:12:41 2010 +0200
     1.3 @@ -208,7 +208,7 @@
     1.4     default_max_relevant_per_iter = 45 (* FUDGE *),
     1.5     default_theory_relevant = false,
     1.6     explicit_forall = false,
     1.7 -   use_conjecture_for_hypotheses = true}
     1.8 +   use_conjecture_for_hypotheses = false} (*###*)
     1.9  
    1.10  val vampire = ("vampire", vampire_config)
    1.11  
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Mon Aug 23 15:30:42 2010 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Mon Aug 23 16:12:41 2010 +0200
     2.3 @@ -223,13 +223,13 @@
     2.4     (["c_COMBB", "c_COMBC"], @{thms COMBB_def COMBC_def}),
     2.5     (["c_COMBS"], @{thms COMBS_def})]
     2.6  val optional_typed_helpers =
     2.7 -  [(["c_True", "c_False"], @{thms True_or_False}),
     2.8 -   (["c_If"], @{thms if_True if_False True_or_False})]
     2.9 +  [(["c_True", "c_False", "c_If"], @{thms True_or_False}),
    2.10 +   (["c_If"], @{thms if_True if_False})]
    2.11  val mandatory_helpers = @{thms fequal_def}
    2.12  
    2.13  val init_counters =
    2.14 -  Symtab.make (maps (maps (map (rpair 0) o fst))
    2.15 -                    [optional_helpers, optional_typed_helpers])
    2.16 +  [optional_helpers, optional_typed_helpers] |> maps (maps fst) 
    2.17 +  |> sort_distinct string_ord |> map (rpair 0) |> Symtab.make
    2.18  
    2.19  fun get_helper_facts ctxt is_FO full_types conjectures axioms =
    2.20    let
    2.21 @@ -472,7 +472,7 @@
    2.22          (is_tptp_variable s andalso not (member (op =) bounds name))
    2.23            ? insert (op =) name
    2.24          #> fold (term_vars bounds) tms
    2.25 -    fun formula_vars bounds (AQuant (q, xs, phi)) =
    2.26 +    fun formula_vars bounds (AQuant (_, xs, phi)) =
    2.27          formula_vars (xs @ bounds) phi
    2.28        | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis
    2.29        | formula_vars bounds (AAtom tm) = term_vars bounds tm