merged
authorwenzelm
Tue, 14 Aug 2012 16:18:15 +0200
changeset 48806 559c1d80e129
parent 48803 ffa31bf5c662 (diff)
parent 48805 c3ea910b3581 (current diff)
child 48807 fde8c3d84ff5
child 48809 2db8aa3459d4
merged
--- a/doc-src/Sledgehammer/sledgehammer.tex	Tue Aug 14 15:42:58 2012 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Tue Aug 14 16:18:15 2012 +0200
@@ -927,12 +927,6 @@
 name, and set \texttt{Z3\_NON\_COMMERCIAL} to ``yes'' to confirm that you are a
 noncommercial user. Sledgehammer has been tested with versions 3.0, 3.1, 3.2,
 and 4.0.
-
-\item[\labelitemi] \textbf{\textit{z3\_tptp}:} This version of Z3 pretends to be
-an ATP, exploiting Z3's support for the TPTP untyped and typed first-order
-formats (FOF and TFF0). It is included for experimental purposes. Sledgehammer
-requires version 4.0 or above. To use it, set the environment variable
-\texttt{Z3\_HOME} to the directory that contains the \texttt{z3} executable.
 \end{enum}
 \end{sloppy}
 
@@ -986,9 +980,6 @@
 \item[\labelitemi] \textbf{\textit{remote\_z3}:} The remote version of Z3 runs on
 servers at the TU M\"unchen (or wherever \texttt{REMOTE\_SMT\_URL} is set to
 point).
-
-\item[\labelitemi] \textbf{\textit{remote\_z3\_tptp}:} The remote version of ``Z3
-with TPTP syntax'' runs on Geoff Sutcliffe's Miami servers.
 \end{enum}
 
 By default, Sledgehammer runs a selection of CVC3, E, E-SInE, SPASS, Vampire,
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Tue Aug 14 15:42:58 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Tue Aug 14 16:18:15 2012 +0200
@@ -52,7 +52,7 @@
     Proof.context -> (string * stature) list vector -> 'a proof
     -> string list option
   val unalias_type_enc : string -> string list
-  val one_line_proof_text : one_line_params -> string
+  val one_line_proof_text : int -> one_line_params -> string
   val make_tvar : string -> typ
   val make_tfree : Proof.context -> string -> typ
   val term_from_atp :
@@ -64,7 +64,7 @@
   val isar_proof_text :
     Proof.context -> bool -> isar_params -> one_line_params -> string
   val proof_text :
-    Proof.context -> bool -> isar_params -> one_line_params -> string
+    Proof.context -> bool -> isar_params -> int -> one_line_params -> string
 end;
 
 structure ATP_Proof_Reconstruct : ATP_PROOF_RECONSTRUCT =
@@ -250,21 +250,33 @@
 fun show_time NONE = ""
   | show_time (SOME ext_time) = " (" ^ string_from_ext_time ext_time ^ ")"
 
+fun unusing_chained_facts _ 0 = ""
+  | unusing_chained_facts used_chaineds num_chained =
+    if length used_chaineds = num_chained then ""
+    else if null used_chaineds then "(* using no facts *) "
+    else "(* using only " ^ space_implode " " used_chaineds ^ " *) "
+
 fun apply_on_subgoal _ 1 = "by "
   | apply_on_subgoal 1 _ = "apply "
   | apply_on_subgoal i n =
     "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n
+
 fun command_call name [] =
     name |> not (Lexicon.is_identifier name) ? enclose "(" ")"
   | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")"
+
 fun try_command_line banner time command =
   banner ^ ": " ^ Markup.markup Isabelle_Markup.sendback command ^ show_time time ^ "."
+
 fun using_labels [] = ""
   | using_labels ls =
     "using " ^ space_implode " " (map string_for_label ls) ^ " "
-fun reconstructor_command reconstr i n (ls, ss) =
+
+fun reconstructor_command reconstr i n used_chaineds num_chained (ls, ss) =
+  unusing_chained_facts used_chaineds num_chained ^
   using_labels ls ^ apply_on_subgoal i n ^
   command_call (string_for_reconstructor reconstr) ss
+
 fun minimize_line _ [] = ""
   | minimize_line minimize_command ss =
     case minimize_command ss of
@@ -276,8 +288,9 @@
   facts |> List.partition (fn (_, (sc, _)) => sc = Chained)
         |> pairself (sort_distinct (string_ord o pairself fst))
 
-fun one_line_proof_text (preplay, banner, used_facts, minimize_command,
-                         subgoal, subgoal_count) =
+fun one_line_proof_text num_chained
+        (preplay, banner, used_facts, minimize_command, subgoal,
+         subgoal_count) =
   let
     val (chained, extra) = split_used_facts used_facts
     val (failed, reconstr, ext_time) =
@@ -292,7 +305,8 @@
       | Failed_to_Play reconstr => (true, reconstr, NONE)
     val try_line =
       ([], map fst extra)
-      |> reconstructor_command reconstr subgoal subgoal_count
+      |> reconstructor_command reconstr subgoal subgoal_count (map fst chained)
+                               num_chained
       |> (if failed then
             enclose "One-line proof reconstruction failed: "
                      ".\n(Invoking \"sledgehammer\" with \"[strict]\" might \
@@ -845,7 +859,7 @@
     val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt)
     val reconstr = Metis (type_enc, lam_trans)
     fun do_facts (ls, ss) =
-      reconstructor_command reconstr 1 1
+      reconstructor_command reconstr 1 1 [] 0
           (ls |> sort_distinct (prod_ord string_ord int_ord),
            ss |> sort_distinct string_ord)
     and do_step ind (Fix xs) =
@@ -887,7 +901,7 @@
       (if isar_proof_requested then 1 else 2) * isar_shrink_factor
     val (params, hyp_ts, concl_t) = strip_subgoal ctxt goal subgoal
     val frees = fold Term.add_frees (concl_t :: hyp_ts) []
-    val one_line_proof = one_line_proof_text one_line_params
+    val one_line_proof = one_line_proof_text 0 one_line_params
     val type_enc =
       if is_typed_helper_used_in_atp_proof atp_proof then full_typesN
       else partial_typesN
@@ -982,11 +996,11 @@
                   ""
   in one_line_proof ^ isar_proof end
 
-fun proof_text ctxt isar_proof isar_params
+fun proof_text ctxt isar_proof isar_params num_chained
                (one_line_params as (preplay, _, _, _, _, _)) =
   (if case preplay of Failed_to_Play _ => true | _ => isar_proof then
      isar_proof_text ctxt isar_proof isar_params
    else
-     one_line_proof_text) one_line_params
+     one_line_proof_text num_chained) one_line_params
 
 end;
--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 14 15:42:58 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 14 16:18:15 2012 +0200
@@ -513,8 +513,8 @@
    best_slices = fn ctxt =>
      (* FUDGE *)
      (if is_vampire_beyond_1_8 () then
-        [(0.333, ((500, vampire_tff0, "mono_native", combs_or_liftingN, false), sosN)),
-         (0.333, ((150, vampire_tff0, "poly_guards??", combs_or_liftingN, false), sosN)),
+        [(0.333, ((500, vampire_tff0, "mono_guards??", combs_or_liftingN, false), sosN)),
+         (0.333, ((150, vampire_tff0, "poly_tags??", combs_or_liftingN, false), sosN)),
          (0.334, ((50, vampire_tff0, "mono_native", combs_or_liftingN, false), no_sosN))]
       else
         [(0.333, ((150, FOF, "poly_guards??", combs_or_liftingN, false), sosN)),
@@ -528,7 +528,7 @@
 val vampire = (vampireN, fn () => vampire_config)
 
 
-(* Z3 with TPTP syntax *)
+(* Z3 with TPTP syntax (half experimental, half legacy) *)
 
 val z3_tff0 = TFF (Monomorphic, TPTP_Implicit)
 
@@ -665,9 +665,6 @@
 val remote_vampire =
   remotify_atp vampire "Vampire" ["2.6", "2.5", "1.8"]
       (K ((250, vampire_tff0, "mono_native", combs_or_liftingN, false), "") (* FUDGE *))
-val remote_z3_tptp =
-  remotify_atp z3_tptp "Z3" ["3.0"]
-      (K ((250, z3_tff0, "mono_native", combsN, false), "") (* FUDGE *))
 val remote_e_sine =
   remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Conjecture
       (K ((500, FOF, "mono_guards??", combsN, false), "") (* FUDGE *))
@@ -728,7 +725,7 @@
   [alt_ergo, e, e_males, iprover, iprover_eq, leo2, satallax, spass, spass_poly,
    vampire, z3_tptp, dummy_thf, remote_e, remote_e_sine, remote_e_tofof,
    remote_iprover, remote_iprover_eq, remote_leo2, remote_satallax,
-   remote_vampire, remote_z3_tptp, remote_snark, remote_waldmeister]
+   remote_vampire, remote_snark, remote_waldmeister]
 
 val setup = fold add_atp atps
 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Tue Aug 14 15:42:58 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Tue Aug 14 16:18:15 2012 +0200
@@ -128,8 +128,9 @@
         case test timeout (xs @ seen) of
           result as {outcome = NONE, used_facts, run_time, ...}
           : prover_result =>
-          min (new_timeout timeout run_time) (filter_used_facts used_facts xs)
-              (filter_used_facts used_facts seen, result)
+          min (new_timeout timeout run_time)
+              (filter_used_facts true used_facts xs)
+              (filter_used_facts false used_facts seen, result)
         | _ => min timeout xs (x :: seen, result)
   in min timeout xs ([], result) end
 
@@ -154,20 +155,21 @@
         in
           case test timeout (sup @ l0) of
             result as {outcome = NONE, used_facts, ...} =>
-            min depth result (filter_used_facts used_facts sup)
-                      (filter_used_facts used_facts l0)
+            min depth result (filter_used_facts true used_facts sup)
+                      (filter_used_facts true used_facts l0)
           | _ =>
             case test timeout (sup @ r0) of
               result as {outcome = NONE, used_facts, ...} =>
-              min depth result (filter_used_facts used_facts sup)
-                        (filter_used_facts used_facts r0)
+              min depth result (filter_used_facts true used_facts sup)
+                        (filter_used_facts true used_facts r0)
             | _ =>
               let
                 val (sup_r0, (l, result)) = min depth result (sup @ r0) l0
                 val (sup, r0) =
-                  (sup, r0) |> pairself (filter_used_facts (map fst sup_r0))
+                  (sup, r0)
+                  |> pairself (filter_used_facts true (map fst sup_r0))
                 val (sup_l, (r, result)) = min depth result (sup @ l) r0
-                val sup = sup |> filter_used_facts (map fst sup_l)
+                val sup = sup |> filter_used_facts true (map fst sup_l)
               in (sup, (l @ r, result)) end
         end
 (*
@@ -189,14 +191,18 @@
     val ctxt = Proof.context_of state
     val prover =
       get_prover ctxt (if silent then Auto_Minimize else Minimize) prover_name
-    val _ = print silent (fn () => "Sledgehammer minimizer: " ^
-                                   quote prover_name ^ ".")
     fun test timeout = test_facts params silent prover timeout i n state
+    val (chained, non_chained) = List.partition is_fact_chained facts
+    (* Push chained facts to the back, so that they are less likely to be
+       kicked out by the linear minimization algorithm. *)
+    val facts = non_chained @ chained
   in
-    (case test timeout facts of
+    (print silent (fn () => "Sledgehammer minimizer: " ^
+                            quote prover_name ^ ".");
+     case test timeout facts of
        result as {outcome = NONE, used_facts, run_time, ...} =>
        let
-         val facts = filter_used_facts used_facts facts
+         val facts = filter_used_facts true used_facts facts
          val min =
            if length facts >= Config.get ctxt binary_min_facts then
              binary_minimize
@@ -207,8 +213,7 @@
        in
          print silent (fn () => cat_lines
              ["Minimized to " ^ n_facts (map fst min_facts)] ^
-              (case min_facts |> filter (fn ((_, (sc, _)), _) => sc = Chained)
-                              |> length of
+              (case min_facts |> filter is_fact_chained |> length of
                  0 => ""
                | n => "\n(including " ^ string_of_int n ^ " chained)") ^ ".");
          (if learn then do_learn prover_name (maps snd min_facts) else ());
@@ -302,7 +307,7 @@
           minimize_facts do_learn minimize_name params
                          (mode <> Normal orelse not verbose) subgoal
                          subgoal_count state
-                         (filter_used_facts used_facts
+                         (filter_used_facts true used_facts
                               (map (apsnd single o untranslated_fact) facts))
           |>> Option.map (map fst)
         else
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Aug 14 15:42:58 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Aug 14 16:18:15 2012 +0200
@@ -131,7 +131,10 @@
   val kill_provers : unit -> unit
   val running_provers : unit -> unit
   val messages : int option -> unit
-  val filter_used_facts : ''a list -> (''a * 'b) list -> (''a * 'b) list
+  val is_fact_chained : (('a * stature) * 'b) -> bool
+  val filter_used_facts :
+    bool -> (''a * stature) list -> ((''a * stature) * 'b) list ->
+    ((''a * stature) * 'b) list
   val get_prover : Proof.context -> mode -> string -> prover
 end;
 
@@ -442,14 +445,18 @@
   | _ => "Try this"
 
 fun bunch_of_reconstructors needs_full_types lam_trans =
-  [(false, Metis (partial_type_enc, lam_trans false)),
-   (true, Metis (full_type_enc, lam_trans false)),
-   (false, Metis (no_typesN, lam_trans true)),
-   (true, Metis (really_full_type_enc, lam_trans true)),
-   (true, SMT)]
-  |> map_filter (fn (full_types, reconstr) =>
-                    if needs_full_types andalso not full_types then NONE
-                    else SOME reconstr)
+  if needs_full_types then
+    [Metis (full_type_enc, lam_trans false),
+     Metis (really_full_type_enc, lam_trans false),
+     Metis (full_type_enc, lam_trans true),
+     Metis (really_full_type_enc, lam_trans true),
+     SMT]
+  else
+    [Metis (partial_type_enc, lam_trans false),
+     Metis (full_type_enc, lam_trans false),
+     Metis (no_typesN, lam_trans true),
+     Metis (really_full_type_enc, lam_trans true),
+     SMT]
 
 fun extract_reconstructor ({type_enc, lam_trans, ...} : params)
                           (Metis (type_enc', lam_trans')) =
@@ -483,7 +490,11 @@
    #> (fn ctxt => tac_for_reconstructor reconstr ctxt ths))
   |> timed_apply timeout
 
-fun filter_used_facts used = filter (member (op =) used o fst)
+fun is_fact_chained ((_, (sc, _)), _) = sc = Chained
+
+fun filter_used_facts keep_chained used =
+  filter ((member (op =) used o fst) orf
+          (if keep_chained then is_fact_chained else K false))
 
 fun play_one_line_proof mode debug verbose timeout pairs state i preferred
                         reconstrs =
@@ -862,7 +873,8 @@
            fn () =>
               let
                 val used_pairs =
-                  facts |> map untranslated_fact |> filter_used_facts used_facts
+                  facts |> map untranslated_fact
+                        |> filter_used_facts false used_facts
               in
                 play_one_line_proof mode debug verbose preplay_timeout
                     used_pairs state subgoal (hd reconstrs) reconstrs
@@ -876,7 +888,11 @@
                   (preplay, proof_banner mode name, used_facts,
                    choose_minimize_command params minimize_command name preplay,
                    subgoal, subgoal_count)
-              in proof_text ctxt isar_proof isar_params one_line_params end,
+                val num_chained = length (#facts (Proof.goal state))
+              in
+                proof_text ctxt isar_proof isar_params num_chained
+                           one_line_params
+              end,
            (if verbose then
               "\nATP real CPU time: " ^ string_from_time run_time ^ "."
             else
@@ -906,7 +922,8 @@
    (103, MalformedInput),
    (110, MalformedInput)]
 val unix_failures =
-  [(139, Crashed)]
+  [(138, Crashed),
+   (139, Crashed)]
 val smt_failures = remote_smt_failures @ z3_failures @ unix_failures
 
 fun failure_from_smt_failure (SMT_Failure.Counterexample {is_real_cex, ...}) =
@@ -1045,15 +1062,17 @@
             play_one_line_proof mode debug verbose preplay_timeout used_pairs
                 state subgoal SMT
                 (bunch_of_reconstructors false
-                     (fn plain =>
-                         if plain then metis_default_lam_trans else liftingN)),
+                     (fn desperate =>
+                         if desperate then liftingN
+                         else metis_default_lam_trans)),
          fn preplay =>
             let
               val one_line_params =
                 (preplay, proof_banner mode name, used_facts,
                  choose_minimize_command params minimize_command name preplay,
                  subgoal, subgoal_count)
-            in one_line_proof_text one_line_params end,
+              val num_chained = length (#facts (Proof.goal state))
+            in one_line_proof_text num_chained one_line_params end,
          if verbose then
            "\nSMT solver real CPU time: " ^ string_from_time run_time ^ "."
          else
@@ -1095,7 +1114,8 @@
                 (play, proof_banner mode name, used_facts,
                  minimize_command override_params name, subgoal,
                  subgoal_count)
-            in one_line_proof_text one_line_params end,
+              val num_chained = length (#facts (Proof.goal state))
+            in one_line_proof_text num_chained one_line_params end,
        message_tail = ""}
     | play =>
       let
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Tue Aug 14 15:42:58 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Tue Aug 14 16:18:15 2012 +0200
@@ -87,7 +87,7 @@
     fun print_used_facts used_facts =
       tag_list 1 facts
       |> map (fn (j, fact) => fact |> untranslated_fact |> apsnd (K j))
-      |> filter_used_facts used_facts
+      |> filter_used_facts false used_facts
       |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j)
       |> commas
       |> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^