added formats to the slice and use TFF for remote Vampire
authorblanchet
Tue Aug 23 14:44:19 2011 +0200 (2011-08-23)
changeset 44416cabd06b69c18
parent 44415 ce6cd1b2344b
child 44417 c76c04d876ef
added formats to the slice and use TFF for remote Vampire
src/HOL/Tools/ATP/atp_systems.ML
src/HOL/Tools/ATP/atp_translate.ML
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 23 07:14:09 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 23 14:44:19 2011 +0200
     1.3 @@ -21,9 +21,8 @@
     1.4       known_failures : (failure * string) list,
     1.5       conj_sym_kind : formula_kind,
     1.6       prem_kind : formula_kind,
     1.7 -     formats : format list,
     1.8       best_slices :
     1.9 -       Proof.context -> (real * (bool * (int * string * string))) list}
    1.10 +       Proof.context -> (real * (bool * (int * format * string * string))) list}
    1.11  
    1.12    val force_sos : bool Config.T
    1.13    val e_smartN : string
    1.14 @@ -50,8 +49,8 @@
    1.15    val remote_prefix : string
    1.16    val remote_atp :
    1.17      string -> string -> string list -> (string * string) list
    1.18 -    -> (failure * string) list -> formula_kind -> formula_kind -> format list
    1.19 -    -> (Proof.context -> int * string) -> string * atp_config
    1.20 +    -> (failure * string) list -> formula_kind -> formula_kind
    1.21 +    -> (Proof.context -> int * format * string) -> string * atp_config
    1.22    val add_atp : string * atp_config -> theory -> theory
    1.23    val get_atp : theory -> string -> atp_config
    1.24    val supported_atps : theory -> string list
    1.25 @@ -78,9 +77,8 @@
    1.26     known_failures : (failure * string) list,
    1.27     conj_sym_kind : formula_kind,
    1.28     prem_kind : formula_kind,
    1.29 -   formats : format list,
    1.30     best_slices :
    1.31 -     Proof.context -> (real * (bool * (int * string * string))) list}
    1.32 +     Proof.context -> (real * (bool * (int * format * string * string))) list}
    1.33  
    1.34  (* "best_slices" must be found empirically, taking a wholistic approach since
    1.35     the ATPs are run in parallel. The "real" components give the faction of the
    1.36 @@ -214,16 +212,15 @@
    1.37        (OutOfResources, "SZS status ResourceOut")],
    1.38     conj_sym_kind = Hypothesis,
    1.39     prem_kind = Conjecture,
    1.40 -   formats = [FOF],
    1.41     best_slices = fn ctxt =>
    1.42       let val method = effective_e_weight_method ctxt in
    1.43         (* FUDGE *)
    1.44         if method = e_smartN then
    1.45 -         [(0.333, (true, (500, "mangled_tags?", e_fun_weightN))),
    1.46 -          (0.334, (true, (50, "mangled_guards?", e_fun_weightN))),
    1.47 -          (0.333, (true, (1000, "mangled_tags?", e_sym_offset_weightN)))]
    1.48 +         [(0.333, (true, (500, FOF, "mangled_tags?", e_fun_weightN))),
    1.49 +          (0.334, (true, (50, FOF, "mangled_guards?", e_fun_weightN))),
    1.50 +          (0.333, (true, (1000, FOF, "mangled_tags?", e_sym_offset_weightN)))]
    1.51         else
    1.52 -         [(1.0, (true, (500, "mangled_tags?", method)))]
    1.53 +         [(1.0, (true, (500, FOF, "mangled_tags?", method)))]
    1.54       end}
    1.55  
    1.56  val e = (eN, e_config)
    1.57 @@ -242,11 +239,10 @@
    1.58     known_failures = [],
    1.59     conj_sym_kind = Axiom,
    1.60     prem_kind = Hypothesis,
    1.61 -   formats = [THF Without_Choice, FOF],
    1.62     best_slices = fn ctxt =>
    1.63       (* FUDGE *)
    1.64 -     [(0.667, (false, (150, "simple_higher", sosN))),
    1.65 -      (0.333, (true, (50, "simple_higher", no_sosN)))]
    1.66 +     [(0.667, (false, (150, THF Without_Choice, "simple_higher", sosN))),
    1.67 +      (0.333, (true, (50, THF Without_Choice, "simple_higher", no_sosN)))]
    1.68       |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
    1.69           else I)}
    1.70  
    1.71 @@ -265,8 +261,8 @@
    1.72     known_failures = [(ProofMissing, "SZS status Theorem")],
    1.73     conj_sym_kind = Axiom,
    1.74     prem_kind = Hypothesis,
    1.75 -   formats = [THF With_Choice],
    1.76 -   best_slices = K [(1.0, (true, (100, "simple_higher", "")))] (* FUDGE *)}
    1.77 +   best_slices =
    1.78 +     K [(1.0, (true, (100, THF With_Choice, "simple_higher", "")))] (* FUDGE *)}
    1.79  
    1.80  val satallax = (satallaxN, satallax_config)
    1.81  
    1.82 @@ -295,12 +291,11 @@
    1.83        (InternalError, "Please report this error")],
    1.84     conj_sym_kind = Hypothesis,
    1.85     prem_kind = Conjecture,
    1.86 -   formats = [FOF],
    1.87     best_slices = fn ctxt =>
    1.88       (* FUDGE *)
    1.89 -     [(0.333, (false, (150, "mangled_tags", sosN))),
    1.90 -      (0.333, (false, (300, "poly_tags?", sosN))),
    1.91 -      (0.334, (true, (50, "mangled_tags?", no_sosN)))]
    1.92 +     [(0.333, (false, (150, FOF, "mangled_tags", sosN))),
    1.93 +      (0.333, (false, (300, FOF, "poly_tags?", sosN))),
    1.94 +      (0.334, (true, (50, FOF, "mangled_tags?", no_sosN)))]
    1.95       |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
    1.96           else I)}
    1.97  
    1.98 @@ -333,12 +328,11 @@
    1.99        (Interrupted, "Aborted by signal SIGINT")],
   1.100     conj_sym_kind = Conjecture,
   1.101     prem_kind = Conjecture,
   1.102 -   formats = [FOF],
   1.103     best_slices = fn ctxt =>
   1.104       (* FUDGE *)
   1.105 -     [(0.333, (false, (150, "poly_guards", sosN))),
   1.106 -      (0.334, (true, (50, "mangled_guards?", no_sosN))),
   1.107 -      (0.333, (false, (500, "mangled_tags?", sosN)))]
   1.108 +     [(0.333, (false, (150, TFF, "poly_guards", sosN))),
   1.109 +      (0.334, (true, (50, TFF, "mangled_guards?", no_sosN))),
   1.110 +      (0.333, (false, (500, TFF, "mangled_tags?", sosN)))]
   1.111       |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
   1.112           else I)}
   1.113  
   1.114 @@ -361,13 +355,12 @@
   1.115        (ProofMissing, "SZS status Unsatisfiable")],
   1.116     conj_sym_kind = Hypothesis,
   1.117     prem_kind = Hypothesis,
   1.118 -   formats = [FOF],
   1.119     best_slices =
   1.120       (* FUDGE (FIXME) *)
   1.121 -     K [(0.5, (false, (250, "mangled_guards?", ""))),
   1.122 -        (0.25, (false, (125, "mangled_guards?", ""))),
   1.123 -        (0.125, (false, (62, "mangled_guards?", ""))),
   1.124 -        (0.125, (false, (31, "mangled_guards?", "")))]}
   1.125 +     K [(0.5, (false, (250, FOF, "mangled_guards?", ""))),
   1.126 +        (0.25, (false, (125, FOF, "mangled_guards?", ""))),
   1.127 +        (0.125, (false, (62, FOF, "mangled_guards?", ""))),
   1.128 +        (0.125, (false, (31, FOF, "mangled_guards?", "")))]}
   1.129  
   1.130  val z3_atp = (z3_atpN, z3_atp_config)
   1.131  
   1.132 @@ -407,7 +400,7 @@
   1.133  val max_remote_secs = 240 (* give Geoff Sutcliffe's servers a break *)
   1.134  
   1.135  fun remote_config system_name system_versions proof_delims known_failures
   1.136 -                  conj_sym_kind prem_kind formats best_slice : atp_config =
   1.137 +                  conj_sym_kind prem_kind best_slice : atp_config =
   1.138    {exec = ("ISABELLE_ATP", "scripts/remote_atp"),
   1.139     required_execs = [],
   1.140     arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
   1.141 @@ -425,58 +418,58 @@
   1.142        (Inappropriate, "says Inappropriate")],
   1.143     conj_sym_kind = conj_sym_kind,
   1.144     prem_kind = prem_kind,
   1.145 -   formats = formats,
   1.146     best_slices = fn ctxt =>
   1.147 -     let val (max_relevant, type_enc) = best_slice ctxt in
   1.148 -       [(1.0, (false, (max_relevant, type_enc, "")))]
   1.149 +     let val (max_relevant, format, type_enc) = best_slice ctxt in
   1.150 +       [(1.0, (false, (max_relevant, format, type_enc, "")))]
   1.151       end}
   1.152  
   1.153  fun remotify_config system_name system_versions best_slice
   1.154 -        ({proof_delims, known_failures, conj_sym_kind, prem_kind, formats, ...}
   1.155 +        ({proof_delims, known_failures, conj_sym_kind, prem_kind, ...}
   1.156           : atp_config) : atp_config =
   1.157    remote_config system_name system_versions proof_delims known_failures
   1.158 -                conj_sym_kind prem_kind formats best_slice
   1.159 +                conj_sym_kind prem_kind best_slice
   1.160  
   1.161  fun remote_atp name system_name system_versions proof_delims known_failures
   1.162 -        conj_sym_kind prem_kind formats best_slice =
   1.163 +               conj_sym_kind prem_kind best_slice =
   1.164    (remote_prefix ^ name,
   1.165     remote_config system_name system_versions proof_delims known_failures
   1.166 -                 conj_sym_kind prem_kind formats best_slice)
   1.167 +                 conj_sym_kind prem_kind best_slice)
   1.168  fun remotify_atp (name, config) system_name system_versions best_slice =
   1.169    (remote_prefix ^ name,
   1.170     remotify_config system_name system_versions best_slice config)
   1.171  
   1.172  val remote_e =
   1.173    remotify_atp e "EP" ["1.0", "1.1", "1.2"]
   1.174 -               (K (750, "mangled_tags?") (* FUDGE *))
   1.175 +               (K (750, FOF, "mangled_tags?") (* FUDGE *))
   1.176  val remote_leo2 =
   1.177    remotify_atp leo2 "LEO-II" ["1.2.8", "1.2.6"]
   1.178 -               (K (100, "simple_higher") (* FUDGE *))
   1.179 +               (K (100, THF Without_Choice, "simple_higher") (* FUDGE *))
   1.180  val remote_satallax =
   1.181    remotify_atp satallax "Satallax" ["2.1", "2.0", "2"]
   1.182 -               (K (100, "simple_higher") (* FUDGE *))
   1.183 +               (K (100, THF With_Choice, "simple_higher") (* FUDGE *))
   1.184  val remote_vampire =
   1.185 -  remotify_atp vampire "Vampire" ["0.6", "9.0", "1.0"]
   1.186 -               (K (200, "mangled_guards?") (* FUDGE *))
   1.187 +  remotify_atp vampire "Vampire" ["1.8"]
   1.188 +               (K (200, TFF, "mangled_guards?") (* FUDGE *))
   1.189  val remote_z3_atp =
   1.190 -  remotify_atp z3_atp "Z3" ["2.18"] (K (250, "mangled_guards?") (* FUDGE *))
   1.191 +  remotify_atp z3_atp "Z3" ["2.18"]
   1.192 +               (K (250, FOF, "mangled_guards?") (* FUDGE *))
   1.193  val remote_e_sine =
   1.194    remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
   1.195 -             Conjecture [FOF] (K (500, "mangled_guards?") (* FUDGE *))
   1.196 +             Conjecture (K (500, FOF, "mangled_guards?") (* FUDGE *))
   1.197  val remote_snark =
   1.198    remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
   1.199               [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
   1.200 -             [TFF, FOF] (K (100, "simple") (* FUDGE *))
   1.201 +             (K (100, TFF, "simple") (* FUDGE *))
   1.202  val remote_e_tofof =
   1.203    remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config)
   1.204 -             Axiom Hypothesis [TFF] (K (150, "simple") (* FUDGE *))
   1.205 +             Axiom Hypothesis (K (150, TFF, "simple") (* FUDGE *))
   1.206  val remote_waldmeister =
   1.207    remote_atp waldmeisterN "Waldmeister" ["710"]
   1.208               [("#START OF PROOF", "Proved Goals:")]
   1.209               [(OutOfResources, "Too many function symbols"),
   1.210                (Crashed, "Unrecoverable Segmentation Fault")]
   1.211 -             Hypothesis Hypothesis [CNF_UEQ]
   1.212 -             (K (50, "mangled_tags?") (* FUDGE *))
   1.213 +             Hypothesis Hypothesis
   1.214 +             (K (50, CNF_UEQ, "mangled_tags?") (* FUDGE *))
   1.215  
   1.216  (* Setup *)
   1.217  
     2.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Tue Aug 23 07:14:09 2011 +0200
     2.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Aug 23 14:44:19 2011 +0200
     2.3 @@ -90,7 +90,7 @@
     2.4    val level_of_type_enc : type_enc -> type_level
     2.5    val is_type_enc_quasi_sound : type_enc -> bool
     2.6    val is_type_enc_fairly_sound : type_enc -> bool
     2.7 -  val choose_format : format list -> type_enc -> format * type_enc
     2.8 +  val adjust_type_enc : format -> type_enc -> type_enc
     2.9    val mk_aconns :
    2.10      connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
    2.11    val unmangled_const : string -> string * (string, 'b) ho_term list
    2.12 @@ -611,23 +611,14 @@
    2.13    | is_type_level_monotonicity_based Fin_Nonmono_Types = true
    2.14    | is_type_level_monotonicity_based _ = false
    2.15  
    2.16 -fun choose_format formats (Simple_Types (order, level)) =
    2.17 -    (case find_first is_format_thf formats of
    2.18 -       SOME format => (format, Simple_Types (order, level))
    2.19 -     | NONE =>
    2.20 -       if member (op =) formats TFF then
    2.21 -         (TFF, Simple_Types (First_Order, level))
    2.22 -       else
    2.23 -         choose_format formats (Guards (Mangled_Monomorphic, level, Uniform)))
    2.24 -  | choose_format formats type_enc =
    2.25 -    (case hd formats of
    2.26 -       CNF_UEQ =>
    2.27 -       (CNF_UEQ, case type_enc of
    2.28 -                   Guards stuff =>
    2.29 -                   (if is_type_enc_fairly_sound type_enc then Tags else Guards)
    2.30 -                       stuff
    2.31 -                 | _ => type_enc)
    2.32 -     | format => (format, type_enc))
    2.33 +fun adjust_type_enc (THF _) type_enc = type_enc
    2.34 +  | adjust_type_enc TFF (Simple_Types (Higher_Order, level)) =
    2.35 +    Simple_Types (First_Order, level)
    2.36 +  | adjust_type_enc format (Simple_Types (_, level)) =
    2.37 +    adjust_type_enc format (Guards (Mangled_Monomorphic, level, Uniform))
    2.38 +  | adjust_type_enc CNF_UEQ (type_enc as Guards stuff) =
    2.39 +    (if is_type_enc_fairly_sound type_enc then Tags else Guards) stuff
    2.40 +  | adjust_type_enc _ type_enc = type_enc
    2.41  
    2.42  fun lift_lambdas ctxt type_enc =
    2.43    map (close_form o Envir.eta_contract) #> rpair ctxt
    2.44 @@ -2087,7 +2078,7 @@
    2.45  fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc exporter
    2.46          lambda_trans readable_names preproc hyp_ts concl_t facts =
    2.47    let
    2.48 -    val (format, type_enc) = choose_format [format] type_enc
    2.49 +    val type_enc = type_enc |> adjust_type_enc format
    2.50      val lambda_trans =
    2.51        if lambda_trans = smartN then
    2.52          if is_type_enc_higher_order type_enc then lambdasN else combinatorsN
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Aug 23 07:14:09 2011 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Aug 23 14:44:19 2011 +0200
     3.3 @@ -154,7 +154,9 @@
     3.4  fun is_unit_equational_atp ctxt name =
     3.5    let val thy = Proof_Context.theory_of ctxt in
     3.6      case try (get_atp thy) name of
     3.7 -      SOME {formats, ...} => member (op =) formats CNF_UEQ
     3.8 +      SOME {best_slices, ...} =>
     3.9 +      exists (fn (_, (_, (_, format, _, _))) => format = CNF_UEQ)
    3.10 +             (best_slices ctxt)
    3.11      | NONE => false
    3.12    end
    3.13  
    3.14 @@ -512,10 +514,10 @@
    3.15     them each time. *)
    3.16  val atp_important_message_keep_quotient = 10
    3.17  
    3.18 -fun choose_format_and_type_enc soundness best_type_enc formats =
    3.19 +fun choose_type_enc soundness best_type_enc format =
    3.20    the_default best_type_enc
    3.21    #> type_enc_from_string soundness
    3.22 -  #> choose_format formats
    3.23 +  #> adjust_type_enc format
    3.24  
    3.25  val metis_minimize_max_time = seconds 2.0
    3.26  
    3.27 @@ -540,7 +542,7 @@
    3.28  
    3.29  fun run_atp mode name
    3.30          ({exec, required_execs, arguments, proof_delims, known_failures,
    3.31 -          conj_sym_kind, prem_kind, formats, best_slices, ...} : atp_config)
    3.32 +          conj_sym_kind, prem_kind, best_slices, ...} : atp_config)
    3.33          ({debug, verbose, overlord, type_enc, sound, max_relevant,
    3.34            max_mono_iters, max_new_mono_instances, isar_proof,
    3.35            isar_shrink_factor, slicing, timeout, preplay_timeout, ...} : params)
    3.36 @@ -609,7 +611,8 @@
    3.37                  |> maps (fn (name, rths) => map (pair name o snd) rths)
    3.38                end
    3.39              fun run_slice (slice, (time_frac, (complete,
    3.40 -                                    (best_max_relevant, best_type_enc, extra))))
    3.41 +                                    (best_max_relevant, format, best_type_enc,
    3.42 +                                     extra))))
    3.43                            time_left =
    3.44                let
    3.45                  val num_facts =
    3.46 @@ -623,9 +626,8 @@
    3.47                        Sound
    3.48                    else
    3.49                      Unsound
    3.50 -                val (format, type_enc) =
    3.51 -                  choose_format_and_type_enc soundness best_type_enc formats
    3.52 -                                             type_enc
    3.53 +                val type_enc =
    3.54 +                  type_enc |> choose_type_enc soundness best_type_enc format
    3.55                  val fairly_sound = is_type_enc_fairly_sound type_enc
    3.56                  val facts =
    3.57                    facts |> map untranslated_fact