src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
changeset 42451 a75fcd103cbb
parent 42450 2765d4fb2b9c
child 42452 f7f796ce5d68
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Apr 21 22:32:00 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Apr 22 00:00:05 2011 +0200
     1.3 @@ -401,17 +401,20 @@
     1.4                  |> filter_out (curry (op =) ~1 o fst)
     1.5                  |> map (Untranslated_Fact o apfst (fst o nth facts))
     1.6                end
     1.7 -            fun run_slice type_sys
     1.8 +            fun run_slice blacklisted_facts
     1.9                            (slice, (time_frac, (complete, default_max_relevant)))
    1.10                            time_left =
    1.11                let
    1.12                  val num_facts =
    1.13                    length facts |> is_none max_relevant
    1.14                                    ? Integer.min default_max_relevant
    1.15 -                val facts = facts
    1.16 -                            |> take num_facts
    1.17 -                            |> monomorphize ? monomorphize_facts
    1.18 -                            |> map (atp_translated_fact ctxt)
    1.19 +                val facts =
    1.20 +                  facts |> take num_facts
    1.21 +                        |> not (null blacklisted_facts)
    1.22 +                           ? filter_out (member (op =) blacklisted_facts
    1.23 +                                         o fst o untranslated_fact)
    1.24 +                        |> monomorphize ? monomorphize_facts
    1.25 +                        |> map (atp_translated_fact ctxt)
    1.26                  val real_ms = Real.fromInt o Time.toMilliseconds
    1.27                  val slice_timeout =
    1.28                    ((real_ms time_left
    1.29 @@ -469,19 +472,25 @@
    1.30                    else
    1.31                      (conjecture_shape, fact_names) (* don't bother repairing *)
    1.32                  val outcome =
    1.33 -                  if is_none outcome andalso
    1.34 -                     not (is_type_system_sound type_sys) andalso
    1.35 -                     is_unsound_proof conjecture_shape fact_names atp_proof then
    1.36 -                    SOME UnsoundProof
    1.37 -                  else
    1.38 -                    outcome
    1.39 +                  case outcome of
    1.40 +                    NONE => if not (is_type_system_sound type_sys) andalso
    1.41 +                               is_unsound_proof conjecture_shape fact_names
    1.42 +                                                atp_proof then
    1.43 +                              SOME UnsoundProof
    1.44 +                            else
    1.45 +                              NONE
    1.46 +                  | SOME Unprovable =>
    1.47 +                    if null blacklisted_facts then outcome
    1.48 +                    else SOME IncompleteUnprovable
    1.49 +                  | _ => outcome
    1.50                in
    1.51                  ((pool, conjecture_shape, fact_names),
    1.52                   (output, msecs, atp_proof, outcome))
    1.53                end
    1.54              val timer = Timer.startRealTimer ()
    1.55 -            fun maybe_run_slice type_sys slice (_, (_, msecs0, _, SOME _)) =
    1.56 -                run_slice type_sys slice
    1.57 +            fun maybe_run_slice blacklisted_facts slice
    1.58 +                                (_, (_, msecs0, _, SOME _)) =
    1.59 +                run_slice blacklisted_facts slice
    1.60                            (Time.- (timeout, Timer.checkRealTimer timer))
    1.61                  |> (fn (stuff, (output, msecs, atp_proof, outcome)) =>
    1.62                         (stuff, (output, int_opt_add msecs0 msecs, atp_proof,
    1.63 @@ -490,11 +499,18 @@
    1.64            in
    1.65              ((Symtab.empty, [], Vector.fromList []),
    1.66               ("", SOME 0, [], SOME InternalError))
    1.67 -            |> fold (maybe_run_slice type_sys) actual_slices
    1.68 -               (* The ATP found an unsound proof? Automatically try again with
    1.69 -                  full types! *)
    1.70 -            |> (fn result as (_, (_, _, _, SOME UnsoundProof)) =>
    1.71 -                   result |> fold (maybe_run_slice (Tags true)) actual_slices
    1.72 +            |> fold (maybe_run_slice []) actual_slices
    1.73 +               (* The ATP found an unsound proof? Automatically try again
    1.74 +                  without the offending facts! *)
    1.75 +            |> (fn result as ((_, _, fact_names),
    1.76 +                              (_, _, atp_proof, SOME UnsoundProof)) =>
    1.77 +                   let
    1.78 +                     val blacklisted_facts =
    1.79 +                       used_facts_in_atp_proof fact_names atp_proof
    1.80 +                   in
    1.81 +                     result |> fold (maybe_run_slice blacklisted_facts)
    1.82 +                                    actual_slices
    1.83 +                   end
    1.84                   | result => result)
    1.85            end
    1.86          else
    1.87 @@ -565,7 +581,6 @@
    1.88  val smt_failures =
    1.89    remote_smt_failures @ z3_wrapper_failures @ z3_failures @ unix_failures
    1.90  
    1.91 -
    1.92  fun failure_from_smt_failure (SMT_Failure.Counterexample {is_real_cex, ...}) =
    1.93      if is_real_cex then Unprovable else IncompleteUnprovable
    1.94    | failure_from_smt_failure SMT_Failure.Time_Out = TimedOut