src/HOL/Tools/ATP/atp_systems.ML
author blanchet
Tue, 23 Aug 2011 15:15:43 +0200
changeset 44420 3d0921b91a86
parent 44418 800baa1b1406
child 44422 1b0a31b7cfe8
permissions -rw-r--r--
avoid TFF format with older Vampire versions
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
38047
9033c03cc214 consequence of directory renaming
blanchet
parents: 38046
diff changeset
     1
(*  Title:      HOL/Tools/ATP/atp_systems.ML
28592
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
     2
    Author:     Fabian Immler, TU Muenchen
36371
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36370
diff changeset
     3
    Author:     Jasmin Blanchette, TU Muenchen
28592
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
     4
36376
e83d52a52449 renamed module "ATP_Wrapper" to "ATP_Systems"
blanchet
parents: 36371
diff changeset
     5
Setup for supported ATPs.
28592
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
     6
*)
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
     7
36376
e83d52a52449 renamed module "ATP_Wrapper" to "ATP_Systems"
blanchet
parents: 36371
diff changeset
     8
signature ATP_SYSTEMS =
28592
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
     9
sig
42577
78414ec6fa4e made the format (TFF or FOF) of the TPTP problem a global argument of the problem again and have the ATPs report which formats they support
blanchet
parents: 42571
diff changeset
    10
  type format = ATP_Problem.format
78414ec6fa4e made the format (TFF or FOF) of the TPTP problem a global argument of the problem again and have the ATPs report which formats they support
blanchet
parents: 42571
diff changeset
    11
  type formula_kind = ATP_Problem.formula_kind
39491
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39375
diff changeset
    12
  type failure = ATP_Proof.failure
38023
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
    13
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
    14
  type atp_config =
42578
1eaf4d437d4c define type system in ATP module so that ATPs can suggest a type system
blanchet
parents: 42577
diff changeset
    15
    {exec : string * string,
1eaf4d437d4c define type system in ATP module so that ATPs can suggest a type system
blanchet
parents: 42577
diff changeset
    16
     required_execs : (string * string) list,
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
    17
     arguments :
43473
fb2713b803e6 deal with ATP time slices in a more flexible/robust fashion
blanchet
parents: 43467
diff changeset
    18
       Proof.context -> bool -> string -> Time.time
43354
396aaa15dd8b pass --trim option to "eproof" script to speed up proof reconstruction
blanchet
parents: 43288
diff changeset
    19
       -> (unit -> (string * real) list) -> string,
42578
1eaf4d437d4c define type system in ATP module so that ATPs can suggest a type system
blanchet
parents: 42577
diff changeset
    20
     proof_delims : (string * string) list,
1eaf4d437d4c define type system in ATP module so that ATPs can suggest a type system
blanchet
parents: 42577
diff changeset
    21
     known_failures : (failure * string) list,
42709
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42708
diff changeset
    22
     conj_sym_kind : formula_kind,
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42708
diff changeset
    23
     prem_kind : formula_kind,
43473
fb2713b803e6 deal with ATP time slices in a more flexible/robust fashion
blanchet
parents: 43467
diff changeset
    24
     best_slices :
44416
cabd06b69c18 added formats to the slice and use TFF for remote Vampire
blanchet
parents: 44391
diff changeset
    25
       Proof.context -> (real * (bool * (int * format * string * string))) list}
38023
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
    26
44099
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
    27
  val force_sos : bool Config.T
43566
a818d5a34cca filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents: 43529
diff changeset
    28
  val e_smartN : string
a818d5a34cca filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents: 43529
diff changeset
    29
  val e_autoN : string
a818d5a34cca filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents: 43529
diff changeset
    30
  val e_fun_weightN : string
a818d5a34cca filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents: 43529
diff changeset
    31
  val e_sym_offset_weightN : string
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
    32
  val e_weight_method : string Config.T
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
    33
  val e_default_fun_weight : real Config.T
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
    34
  val e_fun_weight_base : real Config.T
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
    35
  val e_fun_weight_span : real Config.T
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
    36
  val e_default_sym_offs_weight : real Config.T
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
    37
  val e_sym_offs_weight_base : real Config.T
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
    38
  val e_sym_offs_weight_span : real Config.T
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
    39
  val eN : string
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
    40
  val spassN : string
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
    41
  val vampireN : string
42962
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42955
diff changeset
    42
  val leo2N : string
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42955
diff changeset
    43
  val satallaxN : string
44092
bf489e54d7f8 renamed E wrappers for consistency with CASC conventions
blanchet
parents: 43989
diff changeset
    44
  val e_sineN : string
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
    45
  val snarkN : string
44092
bf489e54d7f8 renamed E wrappers for consistency with CASC conventions
blanchet
parents: 43989
diff changeset
    46
  val e_tofofN : string
42938
c124032ac96f added Waldmeister
blanchet
parents: 42937
diff changeset
    47
  val waldmeisterN : string
41738
eb98c60a6cf0 added experimental "remote_z3_atp", Sutcliffe's TPTP-syntax-aware wrapper for Z3 -- allows to do head-to-head comparison of Sledgehammer's ATP translation and of Sascha's SMT translation
blanchet
parents: 41727
diff changeset
    48
  val z3_atpN : string
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
    49
  val remote_prefix : string
41738
eb98c60a6cf0 added experimental "remote_z3_atp", Sutcliffe's TPTP-syntax-aware wrapper for Z3 -- allows to do head-to-head comparison of Sledgehammer's ATP translation and of Sascha's SMT translation
blanchet
parents: 41727
diff changeset
    50
  val remote_atp :
eb98c60a6cf0 added experimental "remote_z3_atp", Sutcliffe's TPTP-syntax-aware wrapper for Z3 -- allows to do head-to-head comparison of Sledgehammer's ATP translation and of Sascha's SMT translation
blanchet
parents: 41727
diff changeset
    51
    string -> string -> string list -> (string * string) list
44416
cabd06b69c18 added formats to the slice and use TFF for remote Vampire
blanchet
parents: 44391
diff changeset
    52
    -> (failure * string) list -> formula_kind -> formula_kind
cabd06b69c18 added formats to the slice and use TFF for remote Vampire
blanchet
parents: 44391
diff changeset
    53
    -> (Proof.context -> int * format * string) -> string * atp_config
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
    54
  val add_atp : string * atp_config -> theory -> theory
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
    55
  val get_atp : theory -> string -> atp_config
41727
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41725
diff changeset
    56
  val supported_atps : theory -> string list
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
    57
  val is_atp_installed : theory -> string -> bool
35867
16279c4c7a33 move all ATP setup code into ATP_Wrapper
blanchet
parents: 35865
diff changeset
    58
  val refresh_systems_on_tptp : unit -> unit
16279c4c7a33 move all ATP setup code into ATP_Wrapper
blanchet
parents: 35865
diff changeset
    59
  val setup : theory -> theory
28592
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
    60
end;
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
    61
36376
e83d52a52449 renamed module "ATP_Wrapper" to "ATP_Systems"
blanchet
parents: 36371
diff changeset
    62
structure ATP_Systems : ATP_SYSTEMS =
28592
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
    63
struct
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
    64
42577
78414ec6fa4e made the format (TFF or FOF) of the TPTP problem a global argument of the problem again and have the ATPs report which formats they support
blanchet
parents: 42571
diff changeset
    65
open ATP_Problem
39491
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39375
diff changeset
    66
open ATP_Proof
32864
a226f29d4bdc re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents: 32740
diff changeset
    67
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
    68
(* ATP configuration *)
32864
a226f29d4bdc re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents: 32740
diff changeset
    69
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
    70
type atp_config =
42578
1eaf4d437d4c define type system in ATP module so that ATPs can suggest a type system
blanchet
parents: 42577
diff changeset
    71
  {exec : string * string,
1eaf4d437d4c define type system in ATP module so that ATPs can suggest a type system
blanchet
parents: 42577
diff changeset
    72
   required_execs : (string * string) list,
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
    73
   arguments :
43473
fb2713b803e6 deal with ATP time slices in a more flexible/robust fashion
blanchet
parents: 43467
diff changeset
    74
     Proof.context -> bool -> string -> Time.time
fb2713b803e6 deal with ATP time slices in a more flexible/robust fashion
blanchet
parents: 43467
diff changeset
    75
     -> (unit -> (string * real) list) -> string,
42578
1eaf4d437d4c define type system in ATP module so that ATPs can suggest a type system
blanchet
parents: 42577
diff changeset
    76
   proof_delims : (string * string) list,
1eaf4d437d4c define type system in ATP module so that ATPs can suggest a type system
blanchet
parents: 42577
diff changeset
    77
   known_failures : (failure * string) list,
42709
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42708
diff changeset
    78
   conj_sym_kind : formula_kind,
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42708
diff changeset
    79
   prem_kind : formula_kind,
43473
fb2713b803e6 deal with ATP time slices in a more flexible/robust fashion
blanchet
parents: 43467
diff changeset
    80
   best_slices :
44416
cabd06b69c18 added formats to the slice and use TFF for remote Vampire
blanchet
parents: 44391
diff changeset
    81
     Proof.context -> (real * (bool * (int * format * string * string))) list}
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
    82
42723
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42710
diff changeset
    83
(* "best_slices" must be found empirically, taking a wholistic approach since
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42710
diff changeset
    84
   the ATPs are run in parallel. The "real" components give the faction of the
43569
b342cd125533 removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
blanchet
parents: 43567
diff changeset
    85
   time available given to the slice and should add up to 1.0. The "bool"
42723
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42710
diff changeset
    86
   component indicates whether the slice's strategy is complete; the "int", the
43569
b342cd125533 removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
blanchet
parents: 43567
diff changeset
    87
   preferred number of facts to pass; the first "string", the preferred type
43575
cfb2077cb2db tweaked comment
blanchet
parents: 43569
diff changeset
    88
   system (which should be sound or quasi-sound); the second "string", extra
cfb2077cb2db tweaked comment
blanchet
parents: 43569
diff changeset
    89
   information to the prover (e.g., SOS or no SOS).
42723
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42710
diff changeset
    90
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42710
diff changeset
    91
   The last slice should be the most "normal" one, because it will get all the
43569
b342cd125533 removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
blanchet
parents: 43567
diff changeset
    92
   time available if the other slices fail early and also because it is used if
b342cd125533 removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
blanchet
parents: 43567
diff changeset
    93
   slicing is disabled (e.g., by the minimizer). *)
42710
84fcce345b5d further improved type system setup based on Judgment Days
blanchet
parents: 42709
diff changeset
    94
38061
685d1f0f75b3 handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents: 38049
diff changeset
    95
val known_perl_failures =
38094
d01b8119b2e0 better error and minimizer output
blanchet
parents: 38092
diff changeset
    96
  [(CantConnect, "HTTP error"),
d01b8119b2e0 better error and minimizer output
blanchet
parents: 38092
diff changeset
    97
   (NoPerl, "env: perl"),
38065
9069e1ad1527 improved ATP error handling some more
blanchet
parents: 38064
diff changeset
    98
   (NoLibwwwPerl, "Can't locate HTTP")]
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
    99
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   100
(* named ATPs *)
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   101
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   102
val eN = "e"
44099
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   103
val leo2N = "leo2"
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   104
val satallaxN = "satallax"
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   105
val spassN = "spass"
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   106
val vampireN = "vampire"
41740
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   107
val z3_atpN = "z3_atp"
44092
bf489e54d7f8 renamed E wrappers for consistency with CASC conventions
blanchet
parents: 43989
diff changeset
   108
val e_sineN = "e_sine"
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   109
val snarkN = "snark"
44092
bf489e54d7f8 renamed E wrappers for consistency with CASC conventions
blanchet
parents: 43989
diff changeset
   110
val e_tofofN = "e_tofof"
42938
c124032ac96f added Waldmeister
blanchet
parents: 42937
diff changeset
   111
val waldmeisterN = "waldmeister"
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   112
val remote_prefix = "remote_"
38001
a9b47b85ca24 reintroduced more preprocessing steps to Sledgehammer, adapted to the new FOF setting
blanchet
parents: 38000
diff changeset
   113
38023
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
   114
structure Data = Theory_Data
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
   115
(
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   116
  type T = (atp_config * stamp) Symtab.table
38023
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
   117
  val empty = Symtab.empty
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
   118
  val extend = I
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
   119
  fun merge data : T = Symtab.merge (eq_snd op =) data
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
   120
    handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
   121
)
38017
3ad3e3ca2451 move Sledgehammer-specific code out of "Sledgehammer_TPTP_Format"
blanchet
parents: 38015
diff changeset
   122
43981
404ae49ce29f give E at least two seconds -- anything else risks causing too early timeouts in the minimizer, because of too conservative time computations in E and eproof scripts
blanchet
parents: 43850
diff changeset
   123
fun to_secs min time = Int.max (min, (Time.toMilliseconds time + 999) div 1000)
36142
f5e15e9aae10 make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents: 36064
diff changeset
   124
43473
fb2713b803e6 deal with ATP time slices in a more flexible/robust fashion
blanchet
parents: 43467
diff changeset
   125
val sosN = "sos"
fb2713b803e6 deal with ATP time slices in a more flexible/robust fashion
blanchet
parents: 43467
diff changeset
   126
val no_sosN = "no_sos"
fb2713b803e6 deal with ATP time slices in a more flexible/robust fashion
blanchet
parents: 43467
diff changeset
   127
44099
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   128
val force_sos = Attrib.setup_config_bool @{binding atp_force_sos} (K false)
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   129
39491
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39375
diff changeset
   130
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   131
(* E *)
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   132
44420
3d0921b91a86 avoid TFF format with older Vampire versions
blanchet
parents: 44418
diff changeset
   133
fun is_old_e_version () = (string_ord (getenv "E_VERSION", "1.2w") = LESS)
3d0921b91a86 avoid TFF format with older Vampire versions
blanchet
parents: 44418
diff changeset
   134
36369
d2cd0d04b8e6 handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents: 36289
diff changeset
   135
val tstp_proof_delims =
42962
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42955
diff changeset
   136
  [("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation"),
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42955
diff changeset
   137
   ("% SZS output start CNFRefutation", "% SZS output end CNFRefutation")]
36369
d2cd0d04b8e6 handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents: 36289
diff changeset
   138
43473
fb2713b803e6 deal with ATP time slices in a more flexible/robust fashion
blanchet
parents: 43467
diff changeset
   139
val e_smartN = "smart"
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   140
val e_autoN = "auto"
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   141
val e_fun_weightN = "fun_weight"
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   142
val e_sym_offset_weightN = "sym_offset_weight"
41725
7cca2de89296 added support for bleeding-edge E weighting function "SymOffsetsWeight"
blanchet
parents: 41335
diff changeset
   143
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   144
val e_weight_method =
43473
fb2713b803e6 deal with ATP time slices in a more flexible/robust fashion
blanchet
parents: 43467
diff changeset
   145
  Attrib.setup_config_string @{binding atp_e_weight_method} (K e_smartN)
41770
a710e96583d5 adjust fudge factors
blanchet
parents: 41769
diff changeset
   146
(* FUDGE *)
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   147
val e_default_fun_weight =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   148
  Attrib.setup_config_real @{binding atp_e_default_fun_weight} (K 20.0)
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   149
val e_fun_weight_base =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   150
  Attrib.setup_config_real @{binding atp_e_fun_weight_base} (K 0.0)
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   151
val e_fun_weight_span =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   152
  Attrib.setup_config_real @{binding atp_e_fun_weight_span} (K 40.0)
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   153
val e_default_sym_offs_weight =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   154
  Attrib.setup_config_real @{binding atp_e_default_sym_offs_weight} (K 1.0)
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   155
val e_sym_offs_weight_base =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   156
  Attrib.setup_config_real @{binding atp_e_sym_offs_weight_base} (K ~20.0)
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   157
val e_sym_offs_weight_span =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   158
  Attrib.setup_config_real @{binding atp_e_sym_offs_weight_span} (K 60.0)
41725
7cca2de89296 added support for bleeding-edge E weighting function "SymOffsetsWeight"
blanchet
parents: 41335
diff changeset
   159
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42332
diff changeset
   160
fun e_weight_method_case method fw sow =
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   161
  if method = e_fun_weightN then fw
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   162
  else if method = e_sym_offset_weightN then sow
43478
1cef683b588b slightly better setup for E
blanchet
parents: 43476
diff changeset
   163
  else raise Fail ("unexpected " ^ quote method)
41725
7cca2de89296 added support for bleeding-edge E weighting function "SymOffsetsWeight"
blanchet
parents: 41335
diff changeset
   164
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   165
fun scaled_e_weight ctxt method w =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   166
  w * Config.get ctxt
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   167
          (e_weight_method_case method e_fun_weight_span e_sym_offs_weight_span)
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   168
  + Config.get ctxt
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   169
        (e_weight_method_case method e_fun_weight_base e_sym_offs_weight_base)
41725
7cca2de89296 added support for bleeding-edge E weighting function "SymOffsetsWeight"
blanchet
parents: 41335
diff changeset
   170
  |> Real.ceil |> signed_string_of_int
41313
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41269
diff changeset
   171
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   172
fun e_weight_arguments ctxt method weights =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   173
  if method = e_autoN then
41725
7cca2de89296 added support for bleeding-edge E weighting function "SymOffsetsWeight"
blanchet
parents: 41335
diff changeset
   174
    "-xAutoDev"
7cca2de89296 added support for bleeding-edge E weighting function "SymOffsetsWeight"
blanchet
parents: 41335
diff changeset
   175
  else
43622
blanchet
parents: 43575
diff changeset
   176
    (* supplied by Stephan Schulz *)
41314
2dc1dfc1bc69 use the options provided by Stephan Schulz -- much better
blanchet
parents: 41313
diff changeset
   177
    "--split-clauses=4 --split-reuse-defs --simul-paramod --forward-context-sr \
2dc1dfc1bc69 use the options provided by Stephan Schulz -- much better
blanchet
parents: 41313
diff changeset
   178
    \--destructive-er-aggressive --destructive-er --presat-simplify \
2dc1dfc1bc69 use the options provided by Stephan Schulz -- much better
blanchet
parents: 41313
diff changeset
   179
    \--prefer-initial-clauses -tKBO6 -winvfreqrank -c1 -Ginvfreqconjmax -F1 \
2dc1dfc1bc69 use the options provided by Stephan Schulz -- much better
blanchet
parents: 41313
diff changeset
   180
    \--delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred \
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42332
diff changeset
   181
    \-H'(4*" ^ e_weight_method_case method "FunWeight" "SymOffsetWeight" ^
41725
7cca2de89296 added support for bleeding-edge E weighting function "SymOffsetsWeight"
blanchet
parents: 41335
diff changeset
   182
    "(SimulateSOS, " ^
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   183
    (e_weight_method_case method e_default_fun_weight e_default_sym_offs_weight
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   184
     |> Config.get ctxt |> Real.ceil |> signed_string_of_int) ^
41314
2dc1dfc1bc69 use the options provided by Stephan Schulz -- much better
blanchet
parents: 41313
diff changeset
   185
    ",20,1.5,1.5,1" ^
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   186
    (weights ()
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   187
     |> map (fn (s, w) => "," ^ s ^ ":" ^ scaled_e_weight ctxt method w)
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   188
     |> implode) ^
41314
2dc1dfc1bc69 use the options provided by Stephan Schulz -- much better
blanchet
parents: 41313
diff changeset
   189
    "),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,\
2dc1dfc1bc69 use the options provided by Stephan Schulz -- much better
blanchet
parents: 41313
diff changeset
   190
    \1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*\
2dc1dfc1bc69 use the options provided by Stephan Schulz -- much better
blanchet
parents: 41313
diff changeset
   191
    \FIFOWeight(PreferProcessed))'"
41313
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41269
diff changeset
   192
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   193
fun effective_e_weight_method ctxt =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   194
  if is_old_e_version () then e_autoN else Config.get ctxt e_weight_method
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42332
diff changeset
   195
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   196
val e_config : atp_config =
38092
81a003f7de0d speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents: 38090
diff changeset
   197
  {exec = ("E_HOME", "eproof"),
81a003f7de0d speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents: 38090
diff changeset
   198
   required_execs = [],
43354
396aaa15dd8b pass --trim option to "eproof" script to speed up proof reconstruction
blanchet
parents: 43288
diff changeset
   199
   arguments =
43567
dda3e38cc351 remove experimental trimming feature -- it slowed down things on Linux for some reason
blanchet
parents: 43566
diff changeset
   200
     fn ctxt => fn _ => fn method => fn timeout => fn weights =>
43473
fb2713b803e6 deal with ATP time slices in a more flexible/robust fashion
blanchet
parents: 43467
diff changeset
   201
        "--tstp-in --tstp-out -l5 " ^ e_weight_arguments ctxt method weights ^
43981
404ae49ce29f give E at least two seconds -- anything else risks causing too early timeouts in the minimizer, because of too conservative time computations in E and eproof scripts
blanchet
parents: 43850
diff changeset
   202
        " -tAutoDev --silent --cpu-limit=" ^ string_of_int (to_secs 2 timeout),
42962
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42955
diff changeset
   203
   proof_delims = tstp_proof_delims,
36265
41c9e755e552 distinguish between the different ATP errors in the user interface;
blanchet
parents: 36264
diff changeset
   204
   known_failures =
37995
06f02b15ef8a generate full first-order formulas (FOF) in Sledgehammer
blanchet
parents: 37994
diff changeset
   205
     [(Unprovable, "SZS status: CounterSatisfiable"),
06f02b15ef8a generate full first-order formulas (FOF) in Sledgehammer
blanchet
parents: 37994
diff changeset
   206
      (Unprovable, "SZS status CounterSatisfiable"),
42844
f133c030856a better error reporting: detect missing E proofs and remove Vampire native format error
blanchet
parents: 42779
diff changeset
   207
      (ProofMissing, "SZS status Theorem"),
36370
a4f601daa175 centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents: 36369
diff changeset
   208
      (TimedOut, "Failure: Resource limit exceeded (time)"),
a4f601daa175 centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents: 36369
diff changeset
   209
      (TimedOut, "time limit exceeded"),
43467
b62336f85ea7 recognize one more E failure message
blanchet
parents: 43466
diff changeset
   210
      (OutOfResources, "# Cannot determine problem status"),
36370
a4f601daa175 centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents: 36369
diff changeset
   211
      (OutOfResources, "SZS status: ResourceOut"),
a4f601daa175 centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents: 36369
diff changeset
   212
      (OutOfResources, "SZS status ResourceOut")],
43466
52f040bcfae7 tweaked TPTP formula kind for typing information used in the conjecture
blanchet
parents: 43354
diff changeset
   213
   conj_sym_kind = Hypothesis,
42709
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42708
diff changeset
   214
   prem_kind = Conjecture,
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   215
   best_slices = fn ctxt =>
43473
fb2713b803e6 deal with ATP time slices in a more flexible/robust fashion
blanchet
parents: 43467
diff changeset
   216
     let val method = effective_e_weight_method ctxt in
43474
423cd1ecf714 optimized E's time slicing, based on latest exhaustive Judgment Day results
blanchet
parents: 43473
diff changeset
   217
       (* FUDGE *)
43473
fb2713b803e6 deal with ATP time slices in a more flexible/robust fashion
blanchet
parents: 43467
diff changeset
   218
       if method = e_smartN then
44416
cabd06b69c18 added formats to the slice and use TFF for remote Vampire
blanchet
parents: 44391
diff changeset
   219
         [(0.333, (true, (500, FOF, "mangled_tags?", e_fun_weightN))),
cabd06b69c18 added formats to the slice and use TFF for remote Vampire
blanchet
parents: 44391
diff changeset
   220
          (0.334, (true, (50, FOF, "mangled_guards?", e_fun_weightN))),
cabd06b69c18 added formats to the slice and use TFF for remote Vampire
blanchet
parents: 44391
diff changeset
   221
          (0.333, (true, (1000, FOF, "mangled_tags?", e_sym_offset_weightN)))]
43473
fb2713b803e6 deal with ATP time slices in a more flexible/robust fashion
blanchet
parents: 43467
diff changeset
   222
       else
44416
cabd06b69c18 added formats to the slice and use TFF for remote Vampire
blanchet
parents: 44391
diff changeset
   223
         [(1.0, (true, (500, FOF, "mangled_tags?", method)))]
43473
fb2713b803e6 deal with ATP time slices in a more flexible/robust fashion
blanchet
parents: 43467
diff changeset
   224
     end}
38454
9043eefe8d71 detect old Vampire and give a nicer error message
blanchet
parents: 38433
diff changeset
   225
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   226
val e = (eN, e_config)
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   227
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   228
44099
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   229
(* LEO-II *)
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   230
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   231
val leo2_config : atp_config =
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   232
  {exec = ("LEO2_HOME", "leo"),
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   233
   required_execs = [],
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   234
   arguments =
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   235
     fn _ => fn _ => fn sos => fn timeout => fn _ =>
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   236
        "--proofoutput --timeout " ^ string_of_int (to_secs 1 timeout)
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   237
        |> sos = sosN ? prefix "--sos ",
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   238
   proof_delims = tstp_proof_delims,
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   239
   known_failures = [],
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   240
   conj_sym_kind = Axiom,
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   241
   prem_kind = Hypothesis,
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   242
   best_slices = fn ctxt =>
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   243
     (* FUDGE *)
44416
cabd06b69c18 added formats to the slice and use TFF for remote Vampire
blanchet
parents: 44391
diff changeset
   244
     [(0.667, (false, (150, THF Without_Choice, "simple_higher", sosN))),
cabd06b69c18 added formats to the slice and use TFF for remote Vampire
blanchet
parents: 44391
diff changeset
   245
      (0.333, (true, (50, THF Without_Choice, "simple_higher", no_sosN)))]
44099
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   246
     |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   247
         else I)}
39491
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39375
diff changeset
   248
44099
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   249
val leo2 = (leo2N, leo2_config)
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   250
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   251
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   252
(* Satallax *)
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   253
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   254
val satallax_config : atp_config =
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   255
  {exec = ("SATALLAX_HOME", "satallax"),
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   256
   required_execs = [],
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   257
   arguments =
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   258
     fn _ => fn _ => fn _ => fn timeout => fn _ =>
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   259
        "-t " ^ string_of_int (to_secs 1 timeout),
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   260
   proof_delims = tstp_proof_delims,
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   261
   known_failures = [(ProofMissing, "SZS status Theorem")],
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   262
   conj_sym_kind = Axiom,
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   263
   prem_kind = Hypothesis,
44416
cabd06b69c18 added formats to the slice and use TFF for remote Vampire
blanchet
parents: 44391
diff changeset
   264
   best_slices =
cabd06b69c18 added formats to the slice and use TFF for remote Vampire
blanchet
parents: 44391
diff changeset
   265
     K [(1.0, (true, (100, THF With_Choice, "simple_higher", "")))] (* FUDGE *)}
44099
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   266
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   267
val satallax = (satallaxN, satallax_config)
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   268
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   269
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   270
(* SPASS *)
42725
64dea91bbe0e added "force_sos" options to control SPASS's and Vampire's use of SOS in experiments + added corresponding Mirabelle options
blanchet
parents: 42723
diff changeset
   271
36219
16670b4f0baa set SPASS option on the command-line, so that it doesn't vanish when moving to TPTP format
blanchet
parents: 36190
diff changeset
   272
(* The "-VarWeight=3" option helps the higher-order problems, probably by
16670b4f0baa set SPASS option on the command-line, so that it doesn't vanish when moving to TPTP format
blanchet
parents: 36190
diff changeset
   273
   counteracting the presence of "hAPP". *)
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   274
val spass_config : atp_config =
38092
81a003f7de0d speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents: 38090
diff changeset
   275
  {exec = ("ISABELLE_ATP", "scripts/spass"),
39002
a2d7be688ea1 add dependency of "spass" script
blanchet
parents: 38999
diff changeset
   276
   required_execs = [("SPASS_HOME", "SPASS"), ("SPASS_HOME", "tptp2dfg")],
43569
b342cd125533 removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
blanchet
parents: 43567
diff changeset
   277
   arguments = fn _ => fn _ => fn sos => fn timeout => fn _ =>
37962
d7dbe01f48d7 keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems;
blanchet
parents: 37926
diff changeset
   278
     ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
43981
404ae49ce29f give E at least two seconds -- anything else risks causing too early timeouts in the minimizer, because of too conservative time computations in E and eproof scripts
blanchet
parents: 43850
diff changeset
   279
      \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_secs 1 timeout))
43473
fb2713b803e6 deal with ATP time slices in a more flexible/robust fashion
blanchet
parents: 43467
diff changeset
   280
     |> sos = sosN ? prefix "-SOS=1 ",
36369
d2cd0d04b8e6 handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents: 36289
diff changeset
   281
   proof_delims = [("Here is a proof", "Formulae used in the proof")],
36289
f75b6a3e1450 set "atps" reference's default value to "(remote_)e (remote_)spass (remote_)vampire", based on what is installed
blanchet
parents: 36287
diff changeset
   282
   known_failures =
38061
685d1f0f75b3 handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents: 38049
diff changeset
   283
     known_perl_failures @
43050
59284a13abc4 support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents: 42999
diff changeset
   284
     [(GaveUp, "SPASS beiseite: Completion found"),
36370
a4f601daa175 centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents: 36369
diff changeset
   285
      (TimedOut, "SPASS beiseite: Ran out of time"),
36965
67ae217c6b5c identify common SPASS error more clearly
blanchet
parents: 36924
diff changeset
   286
      (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
37413
e856582fe9c4 improve ATP-specific error messages
blanchet
parents: 37347
diff changeset
   287
      (MalformedInput, "Undefined symbol"),
37414
d0cea0796295 expect SPASS 3.7, and give a friendly warning if an older version is used
blanchet
parents: 37413
diff changeset
   288
      (MalformedInput, "Free Variable"),
44391
7b4104df2be6 gracefully handle empty SPASS problems
blanchet
parents: 44235
diff changeset
   289
      (Unprovable, "No formulae and clauses found in input file"),
39263
e2a3c435334b more precise error messages when Vampire is interrupted or SPASS runs into an internal bug
blanchet
parents: 39262
diff changeset
   290
      (SpassTooOld, "tptp2dfg"),
e2a3c435334b more precise error messages when Vampire is interrupted or SPASS runs into an internal bug
blanchet
parents: 39262
diff changeset
   291
      (InternalError, "Please report this error")],
43466
52f040bcfae7 tweaked TPTP formula kind for typing information used in the conjecture
blanchet
parents: 43354
diff changeset
   292
   conj_sym_kind = Hypothesis,
42709
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42708
diff changeset
   293
   prem_kind = Conjecture,
42725
64dea91bbe0e added "force_sos" options to control SPASS's and Vampire's use of SOS in experiments + added corresponding Mirabelle options
blanchet
parents: 42723
diff changeset
   294
   best_slices = fn ctxt =>
42723
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42710
diff changeset
   295
     (* FUDGE *)
44416
cabd06b69c18 added formats to the slice and use TFF for remote Vampire
blanchet
parents: 44391
diff changeset
   296
     [(0.333, (false, (150, FOF, "mangled_tags", sosN))),
cabd06b69c18 added formats to the slice and use TFF for remote Vampire
blanchet
parents: 44391
diff changeset
   297
      (0.333, (false, (300, FOF, "poly_tags?", sosN))),
cabd06b69c18 added formats to the slice and use TFF for remote Vampire
blanchet
parents: 44391
diff changeset
   298
      (0.334, (true, (50, FOF, "mangled_tags?", no_sosN)))]
44099
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   299
     |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
42725
64dea91bbe0e added "force_sos" options to control SPASS's and Vampire's use of SOS in experiments + added corresponding Mirabelle options
blanchet
parents: 42723
diff changeset
   300
         else I)}
38454
9043eefe8d71 detect old Vampire and give a nicer error message
blanchet
parents: 38433
diff changeset
   301
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   302
val spass = (spassN, spass_config)
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   303
38454
9043eefe8d71 detect old Vampire and give a nicer error message
blanchet
parents: 38433
diff changeset
   304
37509
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents: 37506
diff changeset
   305
(* Vampire *)
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents: 37506
diff changeset
   306
44420
3d0921b91a86 avoid TFF format with older Vampire versions
blanchet
parents: 44418
diff changeset
   307
fun is_old_vampire_version () =
3d0921b91a86 avoid TFF format with older Vampire versions
blanchet
parents: 44418
diff changeset
   308
  string_ord (getenv "VAMPIRE_VERSION", "1.8") = LESS
3d0921b91a86 avoid TFF format with older Vampire versions
blanchet
parents: 44418
diff changeset
   309
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   310
val vampire_config : atp_config =
38092
81a003f7de0d speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents: 38090
diff changeset
   311
  {exec = ("VAMPIRE_HOME", "vampire"),
81a003f7de0d speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents: 38090
diff changeset
   312
   required_execs = [],
43569
b342cd125533 removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
blanchet
parents: 43567
diff changeset
   313
   arguments = fn _ => fn _ => fn sos => fn timeout => fn _ =>
44417
c76c04d876ef kindly ask Vampire to output axiom names
blanchet
parents: 44416
diff changeset
   314
     "--mode casc -t " ^ string_of_int (to_secs 1 timeout) ^
c76c04d876ef kindly ask Vampire to output axiom names
blanchet
parents: 44416
diff changeset
   315
     " --proof tptp --output_axiom_names on \
c76c04d876ef kindly ask Vampire to output axiom names
blanchet
parents: 44416
diff changeset
   316
     \ --thanks \"Andrei and Krystof\" --input_file"
43473
fb2713b803e6 deal with ATP time slices in a more flexible/robust fashion
blanchet
parents: 43467
diff changeset
   317
     |> sos = sosN ? prefix "--sos on ",
37509
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents: 37506
diff changeset
   318
   proof_delims =
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents: 37506
diff changeset
   319
     [("=========== Refutation ==========",
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents: 37506
diff changeset
   320
       "======= End of refutation ======="),
38033
df99f022751d support latest version of Vampire (1.0) locally
blanchet
parents: 38032
diff changeset
   321
      ("% SZS output start Refutation", "% SZS output end Refutation"),
df99f022751d support latest version of Vampire (1.0) locally
blanchet
parents: 38032
diff changeset
   322
      ("% SZS output start Proof", "% SZS output end Proof")],
37509
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents: 37506
diff changeset
   323
   known_failures =
43050
59284a13abc4 support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents: 42999
diff changeset
   324
     [(GaveUp, "UNPROVABLE"),
59284a13abc4 support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents: 42999
diff changeset
   325
      (GaveUp, "CANNOT PROVE"),
59284a13abc4 support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents: 42999
diff changeset
   326
      (GaveUp, "SZS status GaveUp"),
42882
391e41ac038b make sure the Vampire incomplete proof detection code kicks in
blanchet
parents: 42855
diff changeset
   327
      (ProofIncomplete, "predicate_definition_introduction,[]"),
38092
81a003f7de0d speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents: 38090
diff changeset
   328
      (TimedOut, "SZS status Timeout"),
37509
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents: 37506
diff changeset
   329
      (Unprovable, "Satisfiability detected"),
38647
5500241da479 play with fudge factor + parse one more Vampire error
blanchet
parents: 38646
diff changeset
   330
      (Unprovable, "Termination reason: Satisfiable"),
39263
e2a3c435334b more precise error messages when Vampire is interrupted or SPASS runs into an internal bug
blanchet
parents: 39262
diff changeset
   331
      (VampireTooOld, "not a valid option"),
e2a3c435334b more precise error messages when Vampire is interrupted or SPASS runs into an internal bug
blanchet
parents: 39262
diff changeset
   332
      (Interrupted, "Aborted by signal SIGINT")],
43466
52f040bcfae7 tweaked TPTP formula kind for typing information used in the conjecture
blanchet
parents: 43354
diff changeset
   333
   conj_sym_kind = Conjecture,
42709
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42708
diff changeset
   334
   prem_kind = Conjecture,
42725
64dea91bbe0e added "force_sos" options to control SPASS's and Vampire's use of SOS in experiments + added corresponding Mirabelle options
blanchet
parents: 42723
diff changeset
   335
   best_slices = fn ctxt =>
42723
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42710
diff changeset
   336
     (* FUDGE *)
44420
3d0921b91a86 avoid TFF format with older Vampire versions
blanchet
parents: 44418
diff changeset
   337
     (0.333, (false, (150, FOF, "poly_guards", sosN))) ::
3d0921b91a86 avoid TFF format with older Vampire versions
blanchet
parents: 44418
diff changeset
   338
     (if is_old_vampire_version () then
3d0921b91a86 avoid TFF format with older Vampire versions
blanchet
parents: 44418
diff changeset
   339
        [(0.334, (true, (50, FOF, "mangled_guards?", no_sosN))),
3d0921b91a86 avoid TFF format with older Vampire versions
blanchet
parents: 44418
diff changeset
   340
         (0.333, (false, (500, FOF, "mangled_tags?", sosN)))]
3d0921b91a86 avoid TFF format with older Vampire versions
blanchet
parents: 44418
diff changeset
   341
      else
3d0921b91a86 avoid TFF format with older Vampire versions
blanchet
parents: 44418
diff changeset
   342
        [(0.334, (true, (50, TFF, "simple", no_sosN))),
3d0921b91a86 avoid TFF format with older Vampire versions
blanchet
parents: 44418
diff changeset
   343
         (0.333, (false, (500, TFF, "simple", sosN)))])
44099
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   344
     |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
42725
64dea91bbe0e added "force_sos" options to control SPASS's and Vampire's use of SOS in experiments + added corresponding Mirabelle options
blanchet
parents: 42723
diff changeset
   345
         else I)}
38454
9043eefe8d71 detect old Vampire and give a nicer error message
blanchet
parents: 38433
diff changeset
   346
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   347
val vampire = (vampireN, vampire_config)
37509
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents: 37506
diff changeset
   348
38454
9043eefe8d71 detect old Vampire and give a nicer error message
blanchet
parents: 38433
diff changeset
   349
41740
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   350
(* Z3 with TPTP syntax *)
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   351
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   352
val z3_atp_config : atp_config =
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   353
  {exec = ("Z3_HOME", "z3"),
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   354
   required_execs = [],
43354
396aaa15dd8b pass --trim option to "eproof" script to speed up proof reconstruction
blanchet
parents: 43288
diff changeset
   355
   arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
44420
3d0921b91a86 avoid TFF format with older Vampire versions
blanchet
parents: 44418
diff changeset
   356
     "MBQI=true -tptp -t:" ^ string_of_int (to_secs 1 timeout),
41740
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   357
   proof_delims = [],
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   358
   known_failures =
41742
11e862c68b40 automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents: 41741
diff changeset
   359
     [(Unprovable, "\nsat"),
43050
59284a13abc4 support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents: 42999
diff changeset
   360
      (GaveUp, "\nunknown"),
59284a13abc4 support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents: 42999
diff changeset
   361
      (GaveUp, "SZS status Satisfiable"),
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42332
diff changeset
   362
      (ProofMissing, "\nunsat"),
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42332
diff changeset
   363
      (ProofMissing, "SZS status Unsatisfiable")],
42709
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42708
diff changeset
   364
   conj_sym_kind = Hypothesis,
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42708
diff changeset
   365
   prem_kind = Hypothesis,
42723
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42710
diff changeset
   366
   best_slices =
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42710
diff changeset
   367
     (* FUDGE (FIXME) *)
44416
cabd06b69c18 added formats to the slice and use TFF for remote Vampire
blanchet
parents: 44391
diff changeset
   368
     K [(0.5, (false, (250, FOF, "mangled_guards?", ""))),
cabd06b69c18 added formats to the slice and use TFF for remote Vampire
blanchet
parents: 44391
diff changeset
   369
        (0.25, (false, (125, FOF, "mangled_guards?", ""))),
cabd06b69c18 added formats to the slice and use TFF for remote Vampire
blanchet
parents: 44391
diff changeset
   370
        (0.125, (false, (62, FOF, "mangled_guards?", ""))),
cabd06b69c18 added formats to the slice and use TFF for remote Vampire
blanchet
parents: 44391
diff changeset
   371
        (0.125, (false, (31, FOF, "mangled_guards?", "")))]}
41740
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   372
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   373
val z3_atp = (z3_atpN, z3_atp_config)
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   374
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   375
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   376
(* Remote ATP invocation via SystemOnTPTP *)
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   377
38061
685d1f0f75b3 handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents: 38049
diff changeset
   378
val systems = Synchronized.var "atp_systems" ([] : string list)
31835
b686d4df54c2 check for current versions on server
immler@in.tum.de
parents: 31832
diff changeset
   379
b686d4df54c2 check for current versions on server
immler@in.tum.de
parents: 31832
diff changeset
   380
fun get_systems () =
43850
7f2cbc713344 moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents: 43690
diff changeset
   381
  case Isabelle_System.bash_output "\"$ISABELLE_ATP/scripts/remote_atp\" -w 2>&1" of
39491
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39375
diff changeset
   382
    (output, 0) => split_lines output
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39375
diff changeset
   383
  | (output, _) =>
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39375
diff changeset
   384
    error (case extract_known_failure known_perl_failures output of
41744
a18e7bbca258 make minimizer verbose
blanchet
parents: 41742
diff changeset
   385
             SOME failure => string_for_failure failure
39491
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39375
diff changeset
   386
           | NONE => perhaps (try (unsuffix "\n")) output ^ ".")
31835
b686d4df54c2 check for current versions on server
immler@in.tum.de
parents: 31832
diff changeset
   387
42537
25ceb855a18b improve version handling -- prefer versions of ToFoF, SInE, and SNARK that are known to work
blanchet
parents: 42535
diff changeset
   388
fun find_system name [] systems =
25ceb855a18b improve version handling -- prefer versions of ToFoF, SInE, and SNARK that are known to work
blanchet
parents: 42535
diff changeset
   389
    find_first (String.isPrefix (name ^ "---")) systems
38690
38a926e033ad make remote ATP versions more robust, by starting with "preferred" version numbers and falling back on any version
blanchet
parents: 38685
diff changeset
   390
  | find_system name (version :: versions) systems =
38a926e033ad make remote ATP versions more robust, by starting with "preferred" version numbers and falling back on any version
blanchet
parents: 38685
diff changeset
   391
    case find_first (String.isPrefix (name ^ "---" ^ version)) systems of
38a926e033ad make remote ATP versions more robust, by starting with "preferred" version numbers and falling back on any version
blanchet
parents: 38685
diff changeset
   392
      NONE => find_system name versions systems
38a926e033ad make remote ATP versions more robust, by starting with "preferred" version numbers and falling back on any version
blanchet
parents: 38685
diff changeset
   393
    | res => res
38a926e033ad make remote ATP versions more robust, by starting with "preferred" version numbers and falling back on any version
blanchet
parents: 38685
diff changeset
   394
38a926e033ad make remote ATP versions more robust, by starting with "preferred" version numbers and falling back on any version
blanchet
parents: 38685
diff changeset
   395
fun get_system name versions =
38589
b03f8fe043ec added "max_relevant_per_iter" option to Sledgehammer
blanchet
parents: 38588
diff changeset
   396
  Synchronized.change_result systems
b03f8fe043ec added "max_relevant_per_iter" option to Sledgehammer
blanchet
parents: 38588
diff changeset
   397
      (fn systems => (if null systems then get_systems () else systems)
42955
576bd30cc4ea clearer SystemOnTPTP errors
blanchet
parents: 42954
diff changeset
   398
                     |> `(`(find_system name versions)))
32864
a226f29d4bdc re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents: 32740
diff changeset
   399
38690
38a926e033ad make remote ATP versions more robust, by starting with "preferred" version numbers and falling back on any version
blanchet
parents: 38685
diff changeset
   400
fun the_system name versions =
38a926e033ad make remote ATP versions more robust, by starting with "preferred" version numbers and falling back on any version
blanchet
parents: 38685
diff changeset
   401
  case get_system name versions of
42955
576bd30cc4ea clearer SystemOnTPTP errors
blanchet
parents: 42954
diff changeset
   402
    (SOME sys, _) => sys
576bd30cc4ea clearer SystemOnTPTP errors
blanchet
parents: 42954
diff changeset
   403
  | (NONE, []) => error ("SystemOnTPTP is currently not available.")
576bd30cc4ea clearer SystemOnTPTP errors
blanchet
parents: 42954
diff changeset
   404
  | (NONE, syss) =>
576bd30cc4ea clearer SystemOnTPTP errors
blanchet
parents: 42954
diff changeset
   405
    error ("System " ^ quote name ^ " is not available at SystemOnTPTP.\n" ^
576bd30cc4ea clearer SystemOnTPTP errors
blanchet
parents: 42954
diff changeset
   406
           "(Available systems: " ^ commas_quote syss ^ ".)")
31835
b686d4df54c2 check for current versions on server
immler@in.tum.de
parents: 31832
diff changeset
   407
41148
f5229ab54284 added timeout max for remote server invocation
blanchet
parents: 40669
diff changeset
   408
val max_remote_secs = 240 (* give Geoff Sutcliffe's servers a break *)
f5229ab54284 added timeout max for remote server invocation
blanchet
parents: 40669
diff changeset
   409
38690
38a926e033ad make remote ATP versions more robust, by starting with "preferred" version numbers and falling back on any version
blanchet
parents: 38685
diff changeset
   410
fun remote_config system_name system_versions proof_delims known_failures
44416
cabd06b69c18 added formats to the slice and use TFF for remote Vampire
blanchet
parents: 44391
diff changeset
   411
                  conj_sym_kind prem_kind best_slice : atp_config =
38092
81a003f7de0d speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents: 38090
diff changeset
   412
  {exec = ("ISABELLE_ATP", "scripts/remote_atp"),
81a003f7de0d speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents: 38090
diff changeset
   413
   required_execs = [],
43354
396aaa15dd8b pass --trim option to "eproof" script to speed up proof reconstruction
blanchet
parents: 43288
diff changeset
   414
   arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
43981
404ae49ce29f give E at least two seconds -- anything else risks causing too early timeouts in the minimizer, because of too conservative time computations in E and eproof scripts
blanchet
parents: 43850
diff changeset
   415
     "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout))
41148
f5229ab54284 added timeout max for remote server invocation
blanchet
parents: 40669
diff changeset
   416
     ^ " -s " ^ the_system system_name system_versions,
42962
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42955
diff changeset
   417
   proof_delims = union (op =) tstp_proof_delims proof_delims,
42965
1403595ec38c slightly gracefuller handling of LEO-II and Satallax output
blanchet
parents: 42963
diff changeset
   418
   known_failures = known_failures @ known_perl_failures @
42941
47f366f1fe32 recognize one more SystemOnTPTP error
blanchet
parents: 42939
diff changeset
   419
     [(Unprovable, "says Satisfiable"),
42999
0db96016bdbf recognize more ATP failures
blanchet
parents: 42974
diff changeset
   420
      (Unprovable, "says CounterSatisfiable"),
43050
59284a13abc4 support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents: 42999
diff changeset
   421
      (GaveUp, "says Unknown"),
59284a13abc4 support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents: 42999
diff changeset
   422
      (GaveUp, "says GaveUp"),
42965
1403595ec38c slightly gracefuller handling of LEO-II and Satallax output
blanchet
parents: 42963
diff changeset
   423
      (ProofMissing, "says Theorem"),
42999
0db96016bdbf recognize more ATP failures
blanchet
parents: 42974
diff changeset
   424
      (ProofMissing, "says Unsatisfiable"),
42953
26111aafab12 detect inappropriate problems and crashes better in Waldmeister
blanchet
parents: 42944
diff changeset
   425
      (TimedOut, "says Timeout"),
26111aafab12 detect inappropriate problems and crashes better in Waldmeister
blanchet
parents: 42944
diff changeset
   426
      (Inappropriate, "says Inappropriate")],
42709
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42708
diff changeset
   427
   conj_sym_kind = conj_sym_kind,
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42708
diff changeset
   428
   prem_kind = prem_kind,
43473
fb2713b803e6 deal with ATP time slices in a more flexible/robust fashion
blanchet
parents: 43467
diff changeset
   429
   best_slices = fn ctxt =>
44416
cabd06b69c18 added formats to the slice and use TFF for remote Vampire
blanchet
parents: 44391
diff changeset
   430
     let val (max_relevant, format, type_enc) = best_slice ctxt in
cabd06b69c18 added formats to the slice and use TFF for remote Vampire
blanchet
parents: 44391
diff changeset
   431
       [(1.0, (false, (max_relevant, format, type_enc, "")))]
43473
fb2713b803e6 deal with ATP time slices in a more flexible/robust fashion
blanchet
parents: 43467
diff changeset
   432
     end}
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42332
diff changeset
   433
43500
4c357b7aa710 provide appropriate type system and number of fact defaults for remote ATPs
blanchet
parents: 43497
diff changeset
   434
fun remotify_config system_name system_versions best_slice
44416
cabd06b69c18 added formats to the slice and use TFF for remote Vampire
blanchet
parents: 44391
diff changeset
   435
        ({proof_delims, known_failures, conj_sym_kind, prem_kind, ...}
43500
4c357b7aa710 provide appropriate type system and number of fact defaults for remote ATPs
blanchet
parents: 43497
diff changeset
   436
         : atp_config) : atp_config =
38690
38a926e033ad make remote ATP versions more robust, by starting with "preferred" version numbers and falling back on any version
blanchet
parents: 38685
diff changeset
   437
  remote_config system_name system_versions proof_delims known_failures
44416
cabd06b69c18 added formats to the slice and use TFF for remote Vampire
blanchet
parents: 44391
diff changeset
   438
                conj_sym_kind prem_kind best_slice
38023
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
   439
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   440
fun remote_atp name system_name system_versions proof_delims known_failures
44416
cabd06b69c18 added formats to the slice and use TFF for remote Vampire
blanchet
parents: 44391
diff changeset
   441
               conj_sym_kind prem_kind best_slice =
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   442
  (remote_prefix ^ name,
38690
38a926e033ad make remote ATP versions more robust, by starting with "preferred" version numbers and falling back on any version
blanchet
parents: 38685
diff changeset
   443
   remote_config system_name system_versions proof_delims known_failures
44416
cabd06b69c18 added formats to the slice and use TFF for remote Vampire
blanchet
parents: 44391
diff changeset
   444
                 conj_sym_kind prem_kind best_slice)
43500
4c357b7aa710 provide appropriate type system and number of fact defaults for remote ATPs
blanchet
parents: 43497
diff changeset
   445
fun remotify_atp (name, config) system_name system_versions best_slice =
4c357b7aa710 provide appropriate type system and number of fact defaults for remote ATPs
blanchet
parents: 43497
diff changeset
   446
  (remote_prefix ^ name,
4c357b7aa710 provide appropriate type system and number of fact defaults for remote ATPs
blanchet
parents: 43497
diff changeset
   447
   remotify_config system_name system_versions best_slice config)
28592
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
   448
43500
4c357b7aa710 provide appropriate type system and number of fact defaults for remote ATPs
blanchet
parents: 43497
diff changeset
   449
val remote_e =
4c357b7aa710 provide appropriate type system and number of fact defaults for remote ATPs
blanchet
parents: 43497
diff changeset
   450
  remotify_atp e "EP" ["1.0", "1.1", "1.2"]
44416
cabd06b69c18 added formats to the slice and use TFF for remote Vampire
blanchet
parents: 44391
diff changeset
   451
               (K (750, FOF, "mangled_tags?") (* FUDGE *))
44099
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   452
val remote_leo2 =
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   453
  remotify_atp leo2 "LEO-II" ["1.2.8", "1.2.6"]
44416
cabd06b69c18 added formats to the slice and use TFF for remote Vampire
blanchet
parents: 44391
diff changeset
   454
               (K (100, THF Without_Choice, "simple_higher") (* FUDGE *))
44099
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   455
val remote_satallax =
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   456
  remotify_atp satallax "Satallax" ["2.1", "2.0", "2"]
44416
cabd06b69c18 added formats to the slice and use TFF for remote Vampire
blanchet
parents: 44391
diff changeset
   457
               (K (100, THF With_Choice, "simple_higher") (* FUDGE *))
43500
4c357b7aa710 provide appropriate type system and number of fact defaults for remote ATPs
blanchet
parents: 43497
diff changeset
   458
val remote_vampire =
44418
800baa1b1406 fixed TFF slicing
blanchet
parents: 44417
diff changeset
   459
  remotify_atp vampire "Vampire" ["1.8"] (K (250, TFF, "simple") (* FUDGE *))
43500
4c357b7aa710 provide appropriate type system and number of fact defaults for remote ATPs
blanchet
parents: 43497
diff changeset
   460
val remote_z3_atp =
44416
cabd06b69c18 added formats to the slice and use TFF for remote Vampire
blanchet
parents: 44391
diff changeset
   461
  remotify_atp z3_atp "Z3" ["2.18"]
cabd06b69c18 added formats to the slice and use TFF for remote Vampire
blanchet
parents: 44391
diff changeset
   462
               (K (250, FOF, "mangled_guards?") (* FUDGE *))
44092
bf489e54d7f8 renamed E wrappers for consistency with CASC conventions
blanchet
parents: 43989
diff changeset
   463
val remote_e_sine =
bf489e54d7f8 renamed E wrappers for consistency with CASC conventions
blanchet
parents: 43989
diff changeset
   464
  remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
44416
cabd06b69c18 added formats to the slice and use TFF for remote Vampire
blanchet
parents: 44391
diff changeset
   465
             Conjecture (K (500, FOF, "mangled_guards?") (* FUDGE *))
41740
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   466
val remote_snark =
42939
0134d6650092 added support for remote Waldmeister
blanchet
parents: 42938
diff changeset
   467
  remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
42962
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42955
diff changeset
   468
             [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
44416
cabd06b69c18 added formats to the slice and use TFF for remote Vampire
blanchet
parents: 44391
diff changeset
   469
             (K (100, TFF, "simple") (* FUDGE *))
44092
bf489e54d7f8 renamed E wrappers for consistency with CASC conventions
blanchet
parents: 43989
diff changeset
   470
val remote_e_tofof =
bf489e54d7f8 renamed E wrappers for consistency with CASC conventions
blanchet
parents: 43989
diff changeset
   471
  remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config)
44416
cabd06b69c18 added formats to the slice and use TFF for remote Vampire
blanchet
parents: 44391
diff changeset
   472
             Axiom Hypothesis (K (150, TFF, "simple") (* FUDGE *))
42938
c124032ac96f added Waldmeister
blanchet
parents: 42937
diff changeset
   473
val remote_waldmeister =
c124032ac96f added Waldmeister
blanchet
parents: 42937
diff changeset
   474
  remote_atp waldmeisterN "Waldmeister" ["710"]
42944
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42943
diff changeset
   475
             [("#START OF PROOF", "Proved Goals:")]
42953
26111aafab12 detect inappropriate problems and crashes better in Waldmeister
blanchet
parents: 42944
diff changeset
   476
             [(OutOfResources, "Too many function symbols"),
26111aafab12 detect inappropriate problems and crashes better in Waldmeister
blanchet
parents: 42944
diff changeset
   477
              (Crashed, "Unrecoverable Segmentation Fault")]
44416
cabd06b69c18 added formats to the slice and use TFF for remote Vampire
blanchet
parents: 44391
diff changeset
   478
             Hypothesis Hypothesis
cabd06b69c18 added formats to the slice and use TFF for remote Vampire
blanchet
parents: 44391
diff changeset
   479
             (K (50, CNF_UEQ, "mangled_tags?") (* FUDGE *))
38454
9043eefe8d71 detect old Vampire and give a nicer error message
blanchet
parents: 38433
diff changeset
   480
9043eefe8d71 detect old Vampire and give a nicer error message
blanchet
parents: 38433
diff changeset
   481
(* Setup *)
9043eefe8d71 detect old Vampire and give a nicer error message
blanchet
parents: 38433
diff changeset
   482
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   483
fun add_atp (name, config) thy =
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   484
  Data.map (Symtab.update_new (name, (config, stamp ()))) thy
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   485
  handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   486
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   487
fun get_atp thy name =
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   488
  the (Symtab.lookup (Data.get thy) name) |> fst
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   489
  handle Option.Option => error ("Unknown ATP: " ^ name ^ ".")
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   490
41727
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41725
diff changeset
   491
val supported_atps = Symtab.keys o Data.get
36371
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36370
diff changeset
   492
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   493
fun is_atp_installed thy name =
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   494
  let val {exec, required_execs, ...} = get_atp thy name in
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   495
    forall (curry (op <>) "" o getenv o fst) (exec :: required_execs)
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   496
  end
36371
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36370
diff changeset
   497
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   498
fun refresh_systems_on_tptp () =
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   499
  Synchronized.change systems (fn _ => get_systems ())
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   500
42962
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42955
diff changeset
   501
val atps =
44099
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   502
  [e, leo2, satallax, spass, vampire, z3_atp, remote_e, remote_leo2,
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   503
   remote_satallax, remote_vampire, remote_z3_atp, remote_e_sine, remote_snark,
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   504
   remote_e_tofof, remote_waldmeister]
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   505
val setup = fold add_atp atps
35867
16279c4c7a33 move all ATP setup code into ATP_Wrapper
blanchet
parents: 35865
diff changeset
   506
28592
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
   507
end;