automatically remove offending facts when faced with an unsound proof -- instead of using the highly inefficient "full_types" option
authorblanchet
Fri Apr 22 00:00:05 2011 +0200 (2011-04-22)
changeset 42451a75fcd103cbb
parent 42450 2765d4fb2b9c
child 42452 f7f796ce5d68
automatically remove offending facts when faced with an unsound proof -- instead of using the highly inefficient "full_types" option
src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Thu Apr 21 22:32:00 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Fri Apr 22 00:00:05 2011 +0200
     1.3 @@ -22,6 +22,8 @@
     1.4    val repair_conjecture_shape_and_fact_names :
     1.5      string -> int list list -> (string * locality) list vector
     1.6      -> int list list * (string * locality) list vector
     1.7 +  val used_facts_in_atp_proof :
     1.8 +    (string * locality) list vector -> string proof -> (string * locality) list
     1.9    val is_unsound_proof :
    1.10      int list list -> (string * locality) list vector -> string proof -> bool
    1.11    val apply_on_subgoal : string -> int -> int -> string
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Apr 21 22:32:00 2011 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Apr 22 00:00:05 2011 +0200
     2.3 @@ -401,17 +401,20 @@
     2.4                  |> filter_out (curry (op =) ~1 o fst)
     2.5                  |> map (Untranslated_Fact o apfst (fst o nth facts))
     2.6                end
     2.7 -            fun run_slice type_sys
     2.8 +            fun run_slice blacklisted_facts
     2.9                            (slice, (time_frac, (complete, default_max_relevant)))
    2.10                            time_left =
    2.11                let
    2.12                  val num_facts =
    2.13                    length facts |> is_none max_relevant
    2.14                                    ? Integer.min default_max_relevant
    2.15 -                val facts = facts
    2.16 -                            |> take num_facts
    2.17 -                            |> monomorphize ? monomorphize_facts
    2.18 -                            |> map (atp_translated_fact ctxt)
    2.19 +                val facts =
    2.20 +                  facts |> take num_facts
    2.21 +                        |> not (null blacklisted_facts)
    2.22 +                           ? filter_out (member (op =) blacklisted_facts
    2.23 +                                         o fst o untranslated_fact)
    2.24 +                        |> monomorphize ? monomorphize_facts
    2.25 +                        |> map (atp_translated_fact ctxt)
    2.26                  val real_ms = Real.fromInt o Time.toMilliseconds
    2.27                  val slice_timeout =
    2.28                    ((real_ms time_left
    2.29 @@ -469,19 +472,25 @@
    2.30                    else
    2.31                      (conjecture_shape, fact_names) (* don't bother repairing *)
    2.32                  val outcome =
    2.33 -                  if is_none outcome andalso
    2.34 -                     not (is_type_system_sound type_sys) andalso
    2.35 -                     is_unsound_proof conjecture_shape fact_names atp_proof then
    2.36 -                    SOME UnsoundProof
    2.37 -                  else
    2.38 -                    outcome
    2.39 +                  case outcome of
    2.40 +                    NONE => if not (is_type_system_sound type_sys) andalso
    2.41 +                               is_unsound_proof conjecture_shape fact_names
    2.42 +                                                atp_proof then
    2.43 +                              SOME UnsoundProof
    2.44 +                            else
    2.45 +                              NONE
    2.46 +                  | SOME Unprovable =>
    2.47 +                    if null blacklisted_facts then outcome
    2.48 +                    else SOME IncompleteUnprovable
    2.49 +                  | _ => outcome
    2.50                in
    2.51                  ((pool, conjecture_shape, fact_names),
    2.52                   (output, msecs, atp_proof, outcome))
    2.53                end
    2.54              val timer = Timer.startRealTimer ()
    2.55 -            fun maybe_run_slice type_sys slice (_, (_, msecs0, _, SOME _)) =
    2.56 -                run_slice type_sys slice
    2.57 +            fun maybe_run_slice blacklisted_facts slice
    2.58 +                                (_, (_, msecs0, _, SOME _)) =
    2.59 +                run_slice blacklisted_facts slice
    2.60                            (Time.- (timeout, Timer.checkRealTimer timer))
    2.61                  |> (fn (stuff, (output, msecs, atp_proof, outcome)) =>
    2.62                         (stuff, (output, int_opt_add msecs0 msecs, atp_proof,
    2.63 @@ -490,11 +499,18 @@
    2.64            in
    2.65              ((Symtab.empty, [], Vector.fromList []),
    2.66               ("", SOME 0, [], SOME InternalError))
    2.67 -            |> fold (maybe_run_slice type_sys) actual_slices
    2.68 -               (* The ATP found an unsound proof? Automatically try again with
    2.69 -                  full types! *)
    2.70 -            |> (fn result as (_, (_, _, _, SOME UnsoundProof)) =>
    2.71 -                   result |> fold (maybe_run_slice (Tags true)) actual_slices
    2.72 +            |> fold (maybe_run_slice []) actual_slices
    2.73 +               (* The ATP found an unsound proof? Automatically try again
    2.74 +                  without the offending facts! *)
    2.75 +            |> (fn result as ((_, _, fact_names),
    2.76 +                              (_, _, atp_proof, SOME UnsoundProof)) =>
    2.77 +                   let
    2.78 +                     val blacklisted_facts =
    2.79 +                       used_facts_in_atp_proof fact_names atp_proof
    2.80 +                   in
    2.81 +                     result |> fold (maybe_run_slice blacklisted_facts)
    2.82 +                                    actual_slices
    2.83 +                   end
    2.84                   | result => result)
    2.85            end
    2.86          else
    2.87 @@ -565,7 +581,6 @@
    2.88  val smt_failures =
    2.89    remote_smt_failures @ z3_wrapper_failures @ z3_failures @ unix_failures
    2.90  
    2.91 -
    2.92  fun failure_from_smt_failure (SMT_Failure.Counterexample {is_real_cex, ...}) =
    2.93      if is_real_cex then Unprovable else IncompleteUnprovable
    2.94    | failure_from_smt_failure SMT_Failure.Time_Out = TimedOut