automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
authorblanchet
Wed Feb 09 17:18:58 2011 +0100 (2011-02-09)
changeset 4174211e862c68b40
parent 41741 839d1488045f
child 41743 d52af5722f0f
automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/HOL/Tools/ATP/atp_systems.ML
src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
     1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Feb 09 17:18:58 2011 +0100
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Feb 09 17:18:58 2011 +0100
     1.3 @@ -475,14 +475,14 @@
     1.4        AList.lookup (op =) args minimize_timeoutK
     1.5        |> Option.map (fst o read_int o raw_explode)  (* FIXME Symbol.explode (?) *)
     1.6        |> the_default 5
     1.7 -    val params = Sledgehammer_Isar.default_params ctxt
     1.8 +    val params as {explicit_apply, ...} = Sledgehammer_Isar.default_params ctxt
     1.9        [("provers", prover_name),
    1.10         ("verbose", "true"),
    1.11         ("type_sys", type_sys),
    1.12         ("timeout", string_of_int timeout)]
    1.13      val minimize =
    1.14 -      Sledgehammer_Minimize.minimize_facts prover_name params true 1
    1.15 -                                           (Sledgehammer_Util.subgoal_count st)
    1.16 +      Sledgehammer_Minimize.minimize_facts prover_name params
    1.17 +          (SOME explicit_apply) true 1 (Sledgehammer_Util.subgoal_count st)
    1.18      val _ = log separator
    1.19    in
    1.20      case minimize st (these (!named_thms)) of
     2.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Wed Feb 09 17:18:58 2011 +0100
     2.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Wed Feb 09 17:18:58 2011 +0100
     2.3 @@ -241,7 +241,8 @@
     2.4     has_incomplete_mode = false,
     2.5     proof_delims = [],
     2.6     known_failures =
     2.7 -     [(IncompleteUnprovable, "\nsat"),
     2.8 +     [(Unprovable, "\nsat"),
     2.9 +      (IncompleteUnprovable, "\nunknown"),
    2.10        (ProofMissing, "\nunsat")],
    2.11     default_max_relevant = 250 (* FUDGE *),
    2.12     explicit_forall = true,
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Wed Feb 09 17:18:58 2011 +0100
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Wed Feb 09 17:18:58 2011 +0100
     3.3 @@ -28,6 +28,7 @@
     3.4    val split_used_facts :
     3.5      (string * locality) list
     3.6      -> (string * locality) list * (string * locality) list
     3.7 +  val metis_proof_text : metis_params -> text_result
     3.8    val isar_proof_text : isar_params -> metis_params -> text_result
     3.9    val proof_text : bool -> isar_params -> metis_params -> text_result
    3.10  end;
    3.11 @@ -165,9 +166,13 @@
    3.12      append (resolve_fact fact_names name)
    3.13    | add_fact _ _ = I
    3.14  
    3.15 -fun used_facts_in_tstplike_proof fact_names =
    3.16 -  atp_proof_from_tstplike_string false
    3.17 -  #> rpair [] #-> fold (add_fact fact_names)
    3.18 +fun used_facts_in_tstplike_proof fact_names tstplike_proof =
    3.19 +  if tstplike_proof = "" then
    3.20 +    Vector.foldl (op @) [] fact_names
    3.21 +  else
    3.22 +    tstplike_proof
    3.23 +    |> atp_proof_from_tstplike_string false
    3.24 +    |> rpair [] |-> fold (add_fact fact_names)
    3.25  
    3.26  val split_used_facts =
    3.27    List.partition (curry (op =) Chained o snd)
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Feb 09 17:18:58 2011 +0100
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Feb 09 17:18:58 2011 +0100
     4.3 @@ -13,7 +13,7 @@
     4.4    val binary_min_facts : int Unsynchronized.ref
     4.5    val filter_used_facts : ''a list -> (''a * 'b) list -> (''a * 'b) list
     4.6    val minimize_facts :
     4.7 -    string -> params -> bool -> int -> int -> Proof.state
     4.8 +    string -> params -> bool option -> bool -> int -> int -> Proof.state
     4.9      -> ((string * locality) * thm list) list
    4.10      -> ((string * locality) * thm list) list option * string
    4.11    val run_minimize :
    4.12 @@ -48,14 +48,24 @@
    4.13  fun print silent f = if silent then () else Output.urgent_message (f ())
    4.14  
    4.15  fun test_facts ({debug, verbose, overlord, provers, type_sys, isar_proof,
    4.16 -                 isar_shrink_factor, ...} : params) silent (prover : prover)
    4.17 -               explicit_apply timeout i n state facts =
    4.18 +                 isar_shrink_factor, ...} : params)
    4.19 +        explicit_apply_opt silent (prover : prover) timeout i n state facts =
    4.20    let
    4.21 +    val thy = Proof.theory_of state
    4.22      val _ =
    4.23        print silent (fn () =>
    4.24            "Testing " ^ n_facts (map fst facts) ^
    4.25            (if verbose then " (timeout: " ^ string_from_time timeout ^ ")"
    4.26            else "") ^ "...")
    4.27 +    val {goal, ...} = Proof.goal state
    4.28 +    val explicit_apply =
    4.29 +      case explicit_apply_opt of
    4.30 +        SOME explicit_apply => explicit_apply
    4.31 +      | NONE =>
    4.32 +        let val (_, hyp_ts, concl_t) = strip_subgoal goal i in
    4.33 +          not (forall (Meson.is_fol_term thy)
    4.34 +                      (concl_t :: hyp_ts @ maps (map prop_of o snd) facts))
    4.35 +        end
    4.36      val params =
    4.37        {debug = debug, verbose = false, overlord = overlord, blocking = true,
    4.38         provers = provers, type_sys = type_sys, explicit_apply = explicit_apply,
    4.39 @@ -64,7 +74,6 @@
    4.40         timeout = timeout, expect = ""}
    4.41      val facts =
    4.42        facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n))
    4.43 -    val {goal, ...} = Proof.goal state
    4.44      val problem =
    4.45        {state = state, goal = goal, subgoal = i, subgoal_count = n,
    4.46         facts = facts, smt_filter = NONE}
    4.47 @@ -129,8 +138,8 @@
    4.48     part of the timeout. *)
    4.49  val slack_msecs = 200
    4.50  
    4.51 -fun minimize_facts prover_name (params as {timeout, ...}) silent i n state
    4.52 -                   facts =
    4.53 +fun minimize_facts prover_name (params as {timeout, ...}) explicit_apply_opt
    4.54 +                   silent i n state facts =
    4.55    let
    4.56      val thy = Proof.theory_of state
    4.57      val ctxt = Proof.context_of state
    4.58 @@ -139,12 +148,8 @@
    4.59      val _ = print silent (fn () => "Sledgehammer minimize: " ^
    4.60                                     quote prover_name ^ ".")
    4.61      val {goal, ...} = Proof.goal state
    4.62 -    val (_, hyp_ts, concl_t) = strip_subgoal goal i
    4.63 -    val explicit_apply =
    4.64 -      not (forall (Meson.is_fol_term thy)
    4.65 -                  (concl_t :: hyp_ts @ maps (map prop_of o snd) facts))
    4.66      fun do_test timeout =
    4.67 -      test_facts params silent prover explicit_apply timeout i n state
    4.68 +      test_facts params explicit_apply_opt silent prover timeout i n state
    4.69      val timer = Timer.startRealTimer ()
    4.70    in
    4.71      (case do_test timeout facts of
    4.72 @@ -196,7 +201,7 @@
    4.73               [] => error "No prover is set."
    4.74             | prover :: _ =>
    4.75               (kill_provers ();
    4.76 -              minimize_facts prover params false i n state facts
    4.77 +              minimize_facts prover params NONE false i n state facts
    4.78                |> #2 |> Output.urgent_message)
    4.79    end
    4.80  
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Feb 09 17:18:58 2011 +0100
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Feb 09 17:18:58 2011 +0100
     5.3 @@ -445,26 +445,29 @@
     5.4          extract_important_message output
     5.5        else
     5.6          ""
     5.7 -    val (message, used_facts) =
     5.8 +    fun append_to_message message =
     5.9 +      message ^
    5.10 +      (if verbose then
    5.11 +         "\nATP real CPU time: " ^
    5.12 +         string_from_time (Time.fromMilliseconds (the msecs)) ^ "."
    5.13 +       else
    5.14 +         "") ^
    5.15 +      (if important_message <> "" then
    5.16 +         "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^ important_message
    5.17 +       else
    5.18 +         "")
    5.19 +    val isar_params = (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
    5.20 +    val metis_params =
    5.21 +      (proof_banner auto, type_sys, minimize_command, tstplike_proof,
    5.22 +       fact_names, goal, subgoal)
    5.23 +    val (outcome, (message, used_facts)) =
    5.24        case outcome of
    5.25          NONE =>
    5.26 -        proof_text isar_proof
    5.27 -            (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
    5.28 -            (proof_banner auto, type_sys, minimize_command, tstplike_proof,
    5.29 -             fact_names, goal, subgoal)
    5.30 -        |>> (fn message =>
    5.31 -                message ^
    5.32 -                (if verbose then
    5.33 -                   "\nATP real CPU time: " ^
    5.34 -                   string_from_time (Time.fromMilliseconds (the msecs)) ^ "."
    5.35 -                 else
    5.36 -                   "") ^
    5.37 -                (if important_message <> "" then
    5.38 -                   "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^
    5.39 -                   important_message
    5.40 -                 else
    5.41 -                   ""))
    5.42 -      | SOME failure => (string_for_failure "ATP" failure, [])
    5.43 +        (NONE, proof_text isar_proof isar_params metis_params
    5.44 +               |>> append_to_message)
    5.45 +      | SOME ProofMissing =>
    5.46 +        (NONE, metis_proof_text metis_params |>> append_to_message)
    5.47 +      | SOME failure => (outcome, (string_for_failure "ATP" failure, []))
    5.48    in
    5.49      {outcome = outcome, message = message, used_facts = used_facts,
    5.50       run_time_in_msecs = msecs}
     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Feb 09 17:18:58 2011 +0100
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Feb 09 17:18:58 2011 +0100
     6.3 @@ -44,8 +44,8 @@
     6.4  
     6.5  val auto_minimize_min_facts = Unsynchronized.ref (!binary_min_facts)
     6.6  
     6.7 -fun get_minimizing_prover ctxt auto name (params as {debug, verbose, ...})
     6.8 -        minimize_command
     6.9 +fun get_minimizing_prover ctxt auto name
    6.10 +        (params as {debug, verbose, explicit_apply, ...}) minimize_command
    6.11          (problem as {state, subgoal, subgoal_count, facts, ...}) =
    6.12    get_prover ctxt auto name params minimize_command problem
    6.13    |> (fn result as {outcome, used_facts, run_time_in_msecs, message} =>
    6.14 @@ -55,8 +55,8 @@
    6.15             let
    6.16               val (used_facts, message) =
    6.17                 if length used_facts >= !auto_minimize_min_facts then
    6.18 -                 minimize_facts name params (not verbose) subgoal subgoal_count
    6.19 -                     state
    6.20 +                 minimize_facts name params (SOME explicit_apply) (not verbose)
    6.21 +                     subgoal subgoal_count state
    6.22                       (filter_used_facts used_facts
    6.23                            (map (apsnd single o untranslated_fact) facts))
    6.24                   |>> Option.map (map fst)