make sure that all facts are passed to ATP from minimizer
authorblanchet
Wed Aug 24 15:25:39 2011 +0200 (2011-08-24)
changeset 44463c471a2b48fa1
parent 44462 d9a657c44380
child 44464 85103fbc9004
make sure that all facts are passed to ATP from minimizer
src/HOL/Tools/ATP/atp_translate.ML
src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Aug 24 11:17:33 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Aug 24 15:25:39 2011 +0200
     1.3 @@ -1062,11 +1062,10 @@
     1.4  fun s_not_trueprop (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t
     1.5    | s_not_trueprop t = s_not t
     1.6  
     1.7 -fun make_conjecture thy format type_enc ps =
     1.8 -  map2 (fn j => fn ((name, loc), (kind, t)) =>
     1.9 -           t |> kind = Conjecture ? s_not_trueprop
    1.10 -             |> make_formula thy type_enc (format <> CNF) name loc kind)
    1.11 -       (0 upto length ps - 1) ps
    1.12 +fun make_conjecture thy format type_enc =
    1.13 +  map (fn ((name, loc), (kind, t)) =>
    1.14 +          t |> kind = Conjecture ? s_not_trueprop
    1.15 +            |> make_formula thy type_enc (format <> CNF) name loc kind)
    1.16  
    1.17  (** Finite and infinite type inference **)
    1.18  
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Aug 24 11:17:33 2011 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Aug 24 15:25:39 2011 +0200
     2.3 @@ -57,16 +57,16 @@
     2.4            (if verbose then " (timeout: " ^ string_from_time timeout ^ ")"
     2.5             else "") ^ "...")
     2.6      val {goal, ...} = Proof.goal state
     2.7 +    val facts =
     2.8 +      facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n))
     2.9      val params =
    2.10        {debug = debug, verbose = verbose, overlord = overlord, blocking = true,
    2.11         provers = provers, type_enc = type_enc, sound = true,
    2.12 -       relevance_thresholds = (1.01, 1.01), max_relevant = NONE,
    2.13 +       relevance_thresholds = (1.01, 1.01), max_relevant = SOME (length facts),
    2.14         max_mono_iters = max_mono_iters,
    2.15         max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
    2.16         isar_shrink_factor = isar_shrink_factor, slicing = false,
    2.17         timeout = timeout, preplay_timeout = preplay_timeout, expect = ""}
    2.18 -    val facts =
    2.19 -      facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n))
    2.20      val problem =
    2.21        {state = state, goal = goal, subgoal = i, subgoal_count = n,
    2.22         facts = facts, smt_filter = NONE}