src/HOL/Tools/ATP/atp_systems.ML
changeset 44754 265174356212
parent 44596 2621046c550a
child 44768 a7bc1bdb8bb4
     1.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Sep 06 18:07:44 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Sep 06 18:13:36 2011 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  
     1.5  signature ATP_SYSTEMS =
     1.6  sig
     1.7 -  type format = ATP_Problem.format
     1.8 +  type tptp_format = ATP_Problem.tptp_format
     1.9    type formula_kind = ATP_Problem.formula_kind
    1.10    type failure = ATP_Proof.failure
    1.11  
    1.12 @@ -22,7 +22,8 @@
    1.13       conj_sym_kind : formula_kind,
    1.14       prem_kind : formula_kind,
    1.15       best_slices :
    1.16 -       Proof.context -> (real * (bool * (int * format * string * string))) list}
    1.17 +       Proof.context
    1.18 +       -> (real * (bool * (int * tptp_format * string * string))) list}
    1.19  
    1.20    val force_sos : bool Config.T
    1.21    val e_smartN : string
    1.22 @@ -41,6 +42,7 @@
    1.23    val e_tofofN : string
    1.24    val leo2N : string
    1.25    val pffN : string
    1.26 +  val phfN : string
    1.27    val satallaxN : string
    1.28    val snarkN : string
    1.29    val spassN : string
    1.30 @@ -51,7 +53,7 @@
    1.31    val remote_atp :
    1.32      string -> string -> string list -> (string * string) list
    1.33      -> (failure * string) list -> formula_kind -> formula_kind
    1.34 -    -> (Proof.context -> int * format * string) -> string * atp_config
    1.35 +    -> (Proof.context -> int * tptp_format * string) -> string * atp_config
    1.36    val add_atp : string * atp_config -> theory -> theory
    1.37    val get_atp : theory -> string -> atp_config
    1.38    val supported_atps : theory -> string list
    1.39 @@ -79,7 +81,8 @@
    1.40     conj_sym_kind : formula_kind,
    1.41     prem_kind : formula_kind,
    1.42     best_slices :
    1.43 -     Proof.context -> (real * (bool * (int * format * string * string))) list}
    1.44 +     Proof.context
    1.45 +     -> (real * (bool * (int * tptp_format * string * string))) list}
    1.46  
    1.47  (* "best_slices" must be found empirically, taking a wholistic approach since
    1.48     the ATPs are run in parallel. The "real" components give the faction of the
    1.49 @@ -105,6 +108,7 @@
    1.50  val e_tofofN = "e_tofof"
    1.51  val leo2N = "leo2"
    1.52  val pffN = "pff"
    1.53 +val phfN = "phf"
    1.54  val satallaxN = "satallax"
    1.55  val snarkN = "snark"
    1.56  val spassN = "spass"
    1.57 @@ -230,6 +234,8 @@
    1.58  
    1.59  (* LEO-II *)
    1.60  
    1.61 +val leo2_thf0 = THF (TPTP_Monomorphic, TPTP_Explicit, THF_Without_Choice)
    1.62 +
    1.63  val leo2_config : atp_config =
    1.64    {exec = ("LEO2_HOME", "leo"),
    1.65     required_execs = [],
    1.66 @@ -243,10 +249,8 @@
    1.67     prem_kind = Hypothesis,
    1.68     best_slices = fn ctxt =>
    1.69       (* FUDGE *)
    1.70 -     [(0.667, (false, (150, THF0 THF_Without_Choice,
    1.71 -                       "mono_simple_higher", sosN))),
    1.72 -      (0.333, (true, (50, THF0 THF_Without_Choice,
    1.73 -                      "mono_simple_higher", no_sosN)))]
    1.74 +     [(0.667, (false, (150, leo2_thf0, "mono_simple_higher", sosN))),
    1.75 +      (0.333, (true, (50, leo2_thf0, "mono_simple_higher", no_sosN)))]
    1.76       |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
    1.77           else I)}
    1.78  
    1.79 @@ -255,6 +259,8 @@
    1.80  
    1.81  (* Satallax *)
    1.82  
    1.83 +val satallax_thf0 = THF (TPTP_Monomorphic, TPTP_Explicit, THF_With_Choice)
    1.84 +
    1.85  val satallax_config : atp_config =
    1.86    {exec = ("SATALLAX_HOME", "satallax"),
    1.87     required_execs = [],
    1.88 @@ -266,8 +272,8 @@
    1.89     conj_sym_kind = Axiom,
    1.90     prem_kind = Hypothesis,
    1.91     best_slices =
    1.92 -     K [(1.0, (true, (100, THF0 THF_With_Choice, "mono_simple_higher", "")))]
    1.93 -     (* FUDGE *)}
    1.94 +     (* FUDGE *)
    1.95 +     K [(1.0, (true, (100, satallax_thf0, "mono_simple_higher", "")))]}
    1.96  
    1.97  val satallax = (satallaxN, satallax_config)
    1.98  
    1.99 @@ -314,7 +320,7 @@
   1.100  fun is_old_vampire_version () =
   1.101    string_ord (getenv "VAMPIRE_VERSION", "1.8") <> GREATER
   1.102  
   1.103 -val vampire_tff = TFF (TFF_Monomorphic, TFF_Implicit)
   1.104 +val vampire_tff0 = TFF (TPTP_Monomorphic, TPTP_Implicit)
   1.105  
   1.106  val vampire_config : atp_config =
   1.107    {exec = ("VAMPIRE_HOME", "vampire"),
   1.108 @@ -347,9 +353,9 @@
   1.109           (0.333, (false, (500, FOF, "mono_tags?", sosN))),
   1.110           (0.334, (true, (50, FOF, "mono_guards?", no_sosN)))]
   1.111        else
   1.112 -        [(0.333, (false, (150, vampire_tff, "poly_guards", sosN))),
   1.113 -         (0.333, (false, (500, vampire_tff, "mono_simple", sosN))),
   1.114 -         (0.334, (true, (50, vampire_tff, "mono_simple", no_sosN)))])
   1.115 +        [(0.333, (false, (150, vampire_tff0, "poly_guards", sosN))),
   1.116 +         (0.333, (false, (500, vampire_tff0, "mono_simple", sosN))),
   1.117 +         (0.334, (true, (50, vampire_tff0, "mono_simple", no_sosN)))])
   1.118       |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
   1.119           else I)}
   1.120  
   1.121 @@ -358,7 +364,7 @@
   1.122  
   1.123  (* Z3 with TPTP syntax *)
   1.124  
   1.125 -val z3_tff = TFF (TFF_Monomorphic, TFF_Implicit)
   1.126 +val z3_tff0 = TFF (TPTP_Monomorphic, TPTP_Implicit)
   1.127  
   1.128  val z3_tptp_config : atp_config =
   1.129    {exec = ("Z3_HOME", "z3"),
   1.130 @@ -377,18 +383,17 @@
   1.131     prem_kind = Hypothesis,
   1.132     best_slices =
   1.133       (* FUDGE *)
   1.134 -     K [(0.5, (false, (250, z3_tff, "mono_simple", ""))),
   1.135 -        (0.25, (false, (125, z3_tff, "mono_simple", ""))),
   1.136 -        (0.125, (false, (62, z3_tff, "mono_simple", ""))),
   1.137 -        (0.125, (false, (31, z3_tff, "mono_simple", "")))]}
   1.138 +     K [(0.5, (false, (250, z3_tff0, "mono_simple", ""))),
   1.139 +        (0.25, (false, (125, z3_tff0, "mono_simple", ""))),
   1.140 +        (0.125, (false, (62, z3_tff0, "mono_simple", ""))),
   1.141 +        (0.125, (false, (31, z3_tff0, "mono_simple", "")))]}
   1.142  
   1.143  val z3_tptp = (z3_tptpN, z3_tptp_config)
   1.144  
   1.145 -(* Not really a prover: Experimental PFF (Polymorphic TFF) output *)
   1.146  
   1.147 -val poly_tff = TFF (TFF_Polymorphic, TFF_Implicit)
   1.148 +(* Not really a prover: Experimental Polymorphic TFF and THF output *)
   1.149  
   1.150 -val pff_config : atp_config =
   1.151 +fun dummy_config format type_enc : atp_config =
   1.152    {exec = ("ISABELLE_ATP", "scripts/dummy_atp"),
   1.153     required_execs = [],
   1.154     arguments = K (K (K (K (K "")))),
   1.155 @@ -396,10 +401,16 @@
   1.156     known_failures = [(GaveUp, "SZS status Unknown")],
   1.157     conj_sym_kind = Hypothesis,
   1.158     prem_kind = Hypothesis,
   1.159 -   best_slices = K [(1.0, (false, (200, poly_tff, "poly_simple", "")))]}
   1.160 +   best_slices = K [(1.0, (false, (200, format, type_enc, "")))]}
   1.161  
   1.162 +val pff_format = TFF (TPTP_Polymorphic, TPTP_Implicit)
   1.163 +val pff_config = dummy_config pff_format "poly_simple"
   1.164  val pff = (pffN, pff_config)
   1.165  
   1.166 +val phf_format = THF (TPTP_Polymorphic, TPTP_Implicit, THF_With_Choice)
   1.167 +val phf_config = dummy_config phf_format "poly_simple_higher"
   1.168 +val phf = (phfN, phf_config)
   1.169 +
   1.170  
   1.171  (* Remote ATP invocation via SystemOnTPTP *)
   1.172  
   1.173 @@ -475,34 +486,33 @@
   1.174    (remote_prefix ^ name,
   1.175     remotify_config system_name system_versions best_slice config)
   1.176  
   1.177 -val dumb_tff = TFF (TFF_Monomorphic, TFF_Explicit)
   1.178 +val explicit_tff0 = TFF (TPTP_Monomorphic, TPTP_Explicit)
   1.179  
   1.180  val remote_e =
   1.181    remotify_atp e "EP" ["1.0", "1.1", "1.2"]
   1.182                 (K (750, FOF, "mono_tags?") (* FUDGE *))
   1.183  val remote_leo2 =
   1.184    remotify_atp leo2 "LEO-II" ["1.2.8", "1.2.6"]
   1.185 -               (K (100, THF0 THF_Without_Choice,
   1.186 -                   "mono_simple_higher") (* FUDGE *))
   1.187 +               (K (100, leo2_thf0, "mono_simple_higher") (* FUDGE *))
   1.188  val remote_satallax =
   1.189    remotify_atp satallax "Satallax" ["2.1", "2.0", "2"]
   1.190 -               (K (100, THF0 THF_With_Choice,
   1.191 -                   "mono_simple_higher") (* FUDGE *))
   1.192 +               (K (100, satallax_thf0, "mono_simple_higher") (* FUDGE *))
   1.193  val remote_vampire =
   1.194    remotify_atp vampire "Vampire" ["1.8"]
   1.195                 (K (250, FOF, "mono_guards?") (* FUDGE *))
   1.196  val remote_z3_tptp =
   1.197 -  remotify_atp z3_tptp "Z3" ["3.0"] (K (250, z3_tff, "mono_simple") (* FUDGE *))
   1.198 +  remotify_atp z3_tptp "Z3" ["3.0"]
   1.199 +               (K (250, z3_tff0, "mono_simple") (* FUDGE *))
   1.200  val remote_e_sine =
   1.201    remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
   1.202               Conjecture (K (500, FOF, "mono_guards?") (* FUDGE *))
   1.203  val remote_snark =
   1.204    remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
   1.205               [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
   1.206 -             (K (100, dumb_tff, "mono_simple") (* FUDGE *))
   1.207 +             (K (100, explicit_tff0, "mono_simple") (* FUDGE *))
   1.208  val remote_e_tofof =
   1.209    remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config) Axiom
   1.210 -             Hypothesis (K (150, dumb_tff, "mono_simple") (* FUDGE *))
   1.211 +             Hypothesis (K (150, explicit_tff0, "mono_simple") (* FUDGE *))
   1.212  val remote_waldmeister =
   1.213    remote_atp waldmeisterN "Waldmeister" ["710"]
   1.214               [("#START OF PROOF", "Proved Goals:")]
   1.215 @@ -532,7 +542,7 @@
   1.216    Synchronized.change systems (fn _ => get_systems ())
   1.217  
   1.218  val atps =
   1.219 -  [e, leo2, pff, satallax, spass, vampire, z3_tptp, remote_e, remote_leo2,
   1.220 +  [e, leo2, pff, phf, satallax, spass, vampire, z3_tptp, remote_e, remote_leo2,
   1.221     remote_satallax, remote_vampire, remote_z3_tptp, remote_e_sine, remote_snark,
   1.222     remote_e_tofof, remote_waldmeister]
   1.223  val setup = fold add_atp atps