src/HOL/Tools/ATP/atp_systems.ML
author blanchet
Thu, 28 Aug 2014 16:58:27 +0200
changeset 58084 9f77084444df
parent 57759 d7454ee84f34
child 58478 999adf103930
permissions -rw-r--r--
pass options to remote Vampire
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
47038
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47034
diff changeset
    10
  type term_order = ATP_Problem.term_order
45301
866b075aa99b added sorted DFG output for coming version of SPASS
blanchet
parents: 45300
diff changeset
    11
  type atp_format = ATP_Problem.atp_format
53586
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 53515
diff changeset
    12
  type atp_formula_role = ATP_Problem.atp_formula_role
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 53515
diff changeset
    13
  type atp_failure = ATP_Proof.atp_failure
38023
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
    14
51011
62b992e53eb8 store fact filter along with ATP slice
blanchet
parents: 50950
diff changeset
    15
  type slice_spec = (int * string) * atp_format * string * string * bool
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
    16
  type atp_config =
57671
dc5e1b1db9ba avoid 'eproof' and 'eproof_ram' scripts if possible (i.e. if 'eprover' can produce reasonable enough proofs for one-liner reconstruction)
blanchet
parents: 57636
diff changeset
    17
    {exec : bool -> string list * string list,
dc5e1b1db9ba avoid 'eproof' and 'eproof_ram' scripts if possible (i.e. if 'eprover' can produce reasonable enough proofs for one-liner reconstruction)
blanchet
parents: 57636
diff changeset
    18
     arguments : Proof.context -> bool -> string -> Time.time -> string ->
dc5e1b1db9ba avoid 'eproof' and 'eproof_ram' scripts if possible (i.e. if 'eprover' can produce reasonable enough proofs for one-liner reconstruction)
blanchet
parents: 57636
diff changeset
    19
       term_order * (unit -> (string * int) list) * (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,
53586
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 53515
diff changeset
    21
     known_failures : (atp_failure * string) list,
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 53515
diff changeset
    22
     prem_role : atp_formula_role,
48716
1d2a12bb0640 stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
blanchet
parents: 48715
diff changeset
    23
     best_slices : Proof.context -> (real * (slice_spec * string)) list,
47962
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47955
diff changeset
    24
     best_max_mono_iters : int,
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47955
diff changeset
    25
     best_max_new_mono_instances : int}
38023
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
    26
47962
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47955
diff changeset
    27
  val default_max_mono_iters : int
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47955
diff changeset
    28
  val default_max_new_mono_instances : int
44099
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
    29
  val force_sos : bool Config.T
47032
73cdeed236c0 more weight attribute tuning
blanchet
parents: 47031
diff changeset
    30
  val term_order : string 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
    31
  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
    32
  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
    33
  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
    34
  val e_sym_offset_weightN : string
47032
73cdeed236c0 more weight attribute tuning
blanchet
parents: 47031
diff changeset
    35
  val e_selection_heuristic : string Config.T
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
    36
  val e_default_fun_weight : real Config.T
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
    37
  val e_fun_weight_base : real Config.T
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
    38
  val e_fun_weight_span : real Config.T
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
    39
  val e_default_sym_offs_weight : real Config.T
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
    40
  val e_sym_offs_weight_base : real Config.T
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
    41
  val e_sym_offs_weight_span : real Config.T
50950
a145ee10371b make SPASS more configurable, for experiments
blanchet
parents: 50927
diff changeset
    42
  val spass_H1SOS : string
a145ee10371b make SPASS more configurable, for experiments
blanchet
parents: 50927
diff changeset
    43
  val spass_H2 : string
a145ee10371b make SPASS more configurable, for experiments
blanchet
parents: 50927
diff changeset
    44
  val spass_H2LR0LT0 : string
a145ee10371b make SPASS more configurable, for experiments
blanchet
parents: 50927
diff changeset
    45
  val spass_H2NuVS0 : string
a145ee10371b make SPASS more configurable, for experiments
blanchet
parents: 50927
diff changeset
    46
  val spass_H2NuVS0Red2 : string
a145ee10371b make SPASS more configurable, for experiments
blanchet
parents: 50927
diff changeset
    47
  val spass_H2SOS : string
a145ee10371b make SPASS more configurable, for experiments
blanchet
parents: 50927
diff changeset
    48
  val spass_extra_options : string Config.T
57671
dc5e1b1db9ba avoid 'eproof' and 'eproof_ram' scripts if possible (i.e. if 'eprover' can produce reasonable enough proofs for one-liner reconstruction)
blanchet
parents: 57636
diff changeset
    49
  val remote_atp : string -> string -> string list -> (string * string) list ->
dc5e1b1db9ba avoid 'eproof' and 'eproof_ram' scripts if possible (i.e. if 'eprover' can produce reasonable enough proofs for one-liner reconstruction)
blanchet
parents: 57636
diff changeset
    50
    (atp_failure * string) list -> atp_formula_role -> (Proof.context -> slice_spec * string) ->
dc5e1b1db9ba avoid 'eproof' and 'eproof_ram' scripts if possible (i.e. if 'eprover' can produce reasonable enough proofs for one-liner reconstruction)
blanchet
parents: 57636
diff changeset
    51
    string * (unit -> atp_config)
47606
06dde48a1503 true delayed evaluation of "SPASS_VERSION" environment variable
blanchet
parents: 47506
diff changeset
    52
  val add_atp : string * (unit -> atp_config) -> theory -> theory
06dde48a1503 true delayed evaluation of "SPASS_VERSION" environment variable
blanchet
parents: 47506
diff changeset
    53
  val get_atp : theory -> string -> (unit -> atp_config)
41727
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41725
diff changeset
    54
  val supported_atps : theory -> string list
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
    55
  val is_atp_installed : theory -> string -> bool
35867
16279c4c7a33 move all ATP setup code into ATP_Wrapper
blanchet
parents: 35865
diff changeset
    56
  val refresh_systems_on_tptp : unit -> unit
47055
16e2633f3b4b made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
blanchet
parents: 47053
diff changeset
    57
  val effective_term_order : Proof.context -> string -> term_order
28592
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
    58
end;
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
    59
36376
e83d52a52449 renamed module "ATP_Wrapper" to "ATP_Systems"
blanchet
parents: 36371
diff changeset
    60
structure ATP_Systems : ATP_SYSTEMS =
28592
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
    61
struct
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
    62
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
    63
open ATP_Problem
39491
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39375
diff changeset
    64
open ATP_Proof
46320
0b8b73b49848 renamed two files to make room for a new file
blanchet
parents: 45876
diff changeset
    65
open ATP_Problem_Generate
32864
a226f29d4bdc re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents: 32740
diff changeset
    66
52073
ccb292952774 started adding agsyHOL as an experimental prover
blanchet
parents: 51998
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
47962
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47955
diff changeset
    70
val default_max_mono_iters = 3 (* FUDGE *)
53515
f5b678b155f6 adjusted number of generated monomorphic instances for new monomorphizer based on new evaluation (E, SPASS, Vampire)
blanchet
parents: 53225
diff changeset
    71
val default_max_new_mono_instances = 100 (* FUDGE *)
47962
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47955
diff changeset
    72
51011
62b992e53eb8 store fact filter along with ATP slice
blanchet
parents: 50950
diff changeset
    73
type slice_spec = (int * string) * atp_format * string * string * bool
46409
d4754183ccce made option available to users (mostly for experiments)
blanchet
parents: 46407
diff changeset
    74
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
    75
type atp_config =
57671
dc5e1b1db9ba avoid 'eproof' and 'eproof_ram' scripts if possible (i.e. if 'eprover' can produce reasonable enough proofs for one-liner reconstruction)
blanchet
parents: 57636
diff changeset
    76
  {exec : bool -> string list * string list,
dc5e1b1db9ba avoid 'eproof' and 'eproof_ram' scripts if possible (i.e. if 'eprover' can produce reasonable enough proofs for one-liner reconstruction)
blanchet
parents: 57636
diff changeset
    77
   arguments : Proof.context -> bool -> string -> Time.time -> string ->
dc5e1b1db9ba avoid 'eproof' and 'eproof_ram' scripts if possible (i.e. if 'eprover' can produce reasonable enough proofs for one-liner reconstruction)
blanchet
parents: 57636
diff changeset
    78
     term_order * (unit -> (string * int) list) * (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
    79
   proof_delims : (string * string) list,
53586
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 53515
diff changeset
    80
   known_failures : (atp_failure * string) list,
bd5fa6425993 prefixed types and some functions with "atp_" for disambiguation
blanchet
parents: 53515
diff changeset
    81
   prem_role : atp_formula_role,
48716
1d2a12bb0640 stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
blanchet
parents: 48715
diff changeset
    82
   best_slices : Proof.context -> (real * (slice_spec * string)) list,
47962
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47955
diff changeset
    83
   best_max_mono_iters : int,
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47955
diff changeset
    84
   best_max_new_mono_instances : int}
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
    85
42723
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42710
diff changeset
    86
(* "best_slices" must be found empirically, taking a wholistic approach since
51011
62b992e53eb8 store fact filter along with ATP slice
blanchet
parents: 50950
diff changeset
    87
   the ATPs are run in parallel. Each slice has the format
62b992e53eb8 store fact filter along with ATP slice
blanchet
parents: 50950
diff changeset
    88
62b992e53eb8 store fact filter along with ATP slice
blanchet
parents: 50950
diff changeset
    89
     (time_frac, ((max_facts, fact_filter), format, type_enc,
62b992e53eb8 store fact filter along with ATP slice
blanchet
parents: 50950
diff changeset
    90
                  lam_trans, uncurried_aliases), extra)
62b992e53eb8 store fact filter along with ATP slice
blanchet
parents: 50950
diff changeset
    91
62b992e53eb8 store fact filter along with ATP slice
blanchet
parents: 50950
diff changeset
    92
   where
62b992e53eb8 store fact filter along with ATP slice
blanchet
parents: 50950
diff changeset
    93
62b992e53eb8 store fact filter along with ATP slice
blanchet
parents: 50950
diff changeset
    94
     time_frac = faction of the time available given to the slice (which should
62b992e53eb8 store fact filter along with ATP slice
blanchet
parents: 50950
diff changeset
    95
       add up to 1.0)
62b992e53eb8 store fact filter along with ATP slice
blanchet
parents: 50950
diff changeset
    96
62b992e53eb8 store fact filter along with ATP slice
blanchet
parents: 50950
diff changeset
    97
     extra = extra 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
    98
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42710
diff changeset
    99
   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
   100
   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
   101
   slicing is disabled (e.g., by the minimizer). *)
42710
84fcce345b5d further improved type system setup based on Judgment Days
blanchet
parents: 42709
diff changeset
   102
51011
62b992e53eb8 store fact filter along with ATP slice
blanchet
parents: 50950
diff changeset
   103
val mepoN = "mepo"
62b992e53eb8 store fact filter along with ATP slice
blanchet
parents: 50950
diff changeset
   104
val mashN = "mash"
62b992e53eb8 store fact filter along with ATP slice
blanchet
parents: 50950
diff changeset
   105
val meshN = "mesh"
62b992e53eb8 store fact filter along with ATP slice
blanchet
parents: 50950
diff changeset
   106
52073
ccb292952774 started adding agsyHOL as an experimental prover
blanchet
parents: 51998
diff changeset
   107
val tstp_proof_delims =
ccb292952774 started adding agsyHOL as an experimental prover
blanchet
parents: 51998
diff changeset
   108
  [("% SZS output start CNFRefutation", "% SZS output end CNFRefutation"),
ccb292952774 started adding agsyHOL as an experimental prover
blanchet
parents: 51998
diff changeset
   109
   ("% SZS output start Refutation", "% SZS output end Refutation"),
ccb292952774 started adding agsyHOL as an experimental prover
blanchet
parents: 51998
diff changeset
   110
   ("% SZS output start Proof", "% SZS output end Proof")]
ccb292952774 started adding agsyHOL as an experimental prover
blanchet
parents: 51998
diff changeset
   111
38061
685d1f0f75b3 handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents: 38049
diff changeset
   112
val known_perl_failures =
38094
d01b8119b2e0 better error and minimizer output
blanchet
parents: 38092
diff changeset
   113
  [(CantConnect, "HTTP error"),
d01b8119b2e0 better error and minimizer output
blanchet
parents: 38092
diff changeset
   114
   (NoPerl, "env: perl"),
38065
9069e1ad1527 improved ATP error handling some more
blanchet
parents: 38064
diff changeset
   115
   (NoLibwwwPerl, "Can't locate HTTP")]
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   116
45203
e3c13fa443ef more uniform SZS status handling
blanchet
parents: 45162
diff changeset
   117
fun known_szs_failures wrap =
e3c13fa443ef more uniform SZS status handling
blanchet
parents: 45162
diff changeset
   118
  [(Unprovable, wrap "CounterSatisfiable"),
e3c13fa443ef more uniform SZS status handling
blanchet
parents: 45162
diff changeset
   119
   (Unprovable, wrap "Satisfiable"),
e3c13fa443ef more uniform SZS status handling
blanchet
parents: 45162
diff changeset
   120
   (GaveUp, wrap "GaveUp"),
e3c13fa443ef more uniform SZS status handling
blanchet
parents: 45162
diff changeset
   121
   (GaveUp, wrap "Unknown"),
e3c13fa443ef more uniform SZS status handling
blanchet
parents: 45162
diff changeset
   122
   (GaveUp, wrap "Incomplete"),
e3c13fa443ef more uniform SZS status handling
blanchet
parents: 45162
diff changeset
   123
   (ProofMissing, wrap "Theorem"),
e3c13fa443ef more uniform SZS status handling
blanchet
parents: 45162
diff changeset
   124
   (ProofMissing, wrap "Unsatisfiable"),
e3c13fa443ef more uniform SZS status handling
blanchet
parents: 45162
diff changeset
   125
   (TimedOut, wrap "Timeout"),
e3c13fa443ef more uniform SZS status handling
blanchet
parents: 45162
diff changeset
   126
   (Inappropriate, wrap "Inappropriate"),
e3c13fa443ef more uniform SZS status handling
blanchet
parents: 45162
diff changeset
   127
   (OutOfResources, wrap "ResourceOut"),
e3c13fa443ef more uniform SZS status handling
blanchet
parents: 45162
diff changeset
   128
   (OutOfResources, wrap "MemoryOut"),
e3c13fa443ef more uniform SZS status handling
blanchet
parents: 45162
diff changeset
   129
   (Interrupted, wrap "Forced"),
e3c13fa443ef more uniform SZS status handling
blanchet
parents: 45162
diff changeset
   130
   (Interrupted, wrap "User")]
e3c13fa443ef more uniform SZS status handling
blanchet
parents: 45162
diff changeset
   131
e3c13fa443ef more uniform SZS status handling
blanchet
parents: 45162
diff changeset
   132
val known_szs_status_failures = known_szs_failures (prefix "SZS status ")
e3c13fa443ef more uniform SZS status handling
blanchet
parents: 45162
diff changeset
   133
val known_says_failures = known_szs_failures (prefix " says ")
e3c13fa443ef more uniform SZS status handling
blanchet
parents: 45162
diff changeset
   134
38023
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
   135
structure Data = Theory_Data
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
   136
(
47606
06dde48a1503 true delayed evaluation of "SPASS_VERSION" environment variable
blanchet
parents: 47506
diff changeset
   137
  type T = ((unit -> atp_config) * stamp) Symtab.table
38023
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
   138
  val empty = Symtab.empty
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
   139
  val extend = I
46407
30e9720cc0b9 optimization: slice caching in case two consecutive slices are nearly identical
blanchet
parents: 46402
diff changeset
   140
  fun merge data : T =
30e9720cc0b9 optimization: slice caching in case two consecutive slices are nearly identical
blanchet
parents: 46402
diff changeset
   141
    Symtab.merge (eq_snd (op =)) data
38023
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
   142
    handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
   143
)
38017
3ad3e3ca2451 move Sledgehammer-specific code out of "Sledgehammer_TPTP_Format"
blanchet
parents: 38015
diff changeset
   144
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
   145
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
   146
43473
fb2713b803e6 deal with ATP time slices in a more flexible/robust fashion
blanchet
parents: 43467
diff changeset
   147
val sosN = "sos"
fb2713b803e6 deal with ATP time slices in a more flexible/robust fashion
blanchet
parents: 43467
diff changeset
   148
val no_sosN = "no_sos"
fb2713b803e6 deal with ATP time slices in a more flexible/robust fashion
blanchet
parents: 43467
diff changeset
   149
44099
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   150
val force_sos = Attrib.setup_config_bool @{binding atp_force_sos} (K false)
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   151
47032
73cdeed236c0 more weight attribute tuning
blanchet
parents: 47031
diff changeset
   152
val smartN = "smart"
47073
c73f7b0c7ebc generate weights and precedences for predicates as well
blanchet
parents: 47055
diff changeset
   153
(* val kboN = "kbo" *)
47032
73cdeed236c0 more weight attribute tuning
blanchet
parents: 47031
diff changeset
   154
val lpoN = "lpo"
47034
77da780ddd6b implement term order attribute (for experiments)
blanchet
parents: 47033
diff changeset
   155
val xweightsN = "_weights"
77da780ddd6b implement term order attribute (for experiments)
blanchet
parents: 47033
diff changeset
   156
val xprecN = "_prec"
77da780ddd6b implement term order attribute (for experiments)
blanchet
parents: 47033
diff changeset
   157
val xsimpN = "_simp" (* SPASS-specific *)
47032
73cdeed236c0 more weight attribute tuning
blanchet
parents: 47031
diff changeset
   158
47038
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47034
diff changeset
   159
(* Possible values for "atp_term_order":
47049
72bd3311ecba added term_order option to Mirabelle
blanchet
parents: 47039
diff changeset
   160
   "smart", "(kbo|lpo)(_weights)?(_prec|_simp)?" *)
47032
73cdeed236c0 more weight attribute tuning
blanchet
parents: 47031
diff changeset
   161
val term_order =
73cdeed236c0 more weight attribute tuning
blanchet
parents: 47031
diff changeset
   162
  Attrib.setup_config_string @{binding atp_term_order} (K smartN)
73cdeed236c0 more weight attribute tuning
blanchet
parents: 47031
diff changeset
   163
52073
ccb292952774 started adding agsyHOL as an experimental prover
blanchet
parents: 51998
diff changeset
   164
ccb292952774 started adding agsyHOL as an experimental prover
blanchet
parents: 51998
diff changeset
   165
(* agsyHOL *)
ccb292952774 started adding agsyHOL as an experimental prover
blanchet
parents: 51998
diff changeset
   166
54197
994ebb795b75 use definitions for LEO-II as well -- this simplifies the code and matches some users' expectations
blanchet
parents: 53586
diff changeset
   167
val agsyhol_thf0 = THF (Monomorphic, THF_Without_Choice)
52073
ccb292952774 started adding agsyHOL as an experimental prover
blanchet
parents: 51998
diff changeset
   168
ccb292952774 started adding agsyHOL as an experimental prover
blanchet
parents: 51998
diff changeset
   169
val agsyhol_config : atp_config =
52754
d9d90d29860e added support for E 1.8's internal proof objects (eliminating the need for "eproof_ram")
blanchet
parents: 52151
diff changeset
   170
  {exec = K (["AGSYHOL_HOME"], ["agsyHOL"]),
52073
ccb292952774 started adding agsyHOL as an experimental prover
blanchet
parents: 51998
diff changeset
   171
   arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
ccb292952774 started adding agsyHOL as an experimental prover
blanchet
parents: 51998
diff changeset
   172
       "--proof --time-out " ^ string_of_int (to_secs 1 timeout) ^ " " ^
ccb292952774 started adding agsyHOL as an experimental prover
blanchet
parents: 51998
diff changeset
   173
       file_name,
ccb292952774 started adding agsyHOL as an experimental prover
blanchet
parents: 51998
diff changeset
   174
   proof_delims = tstp_proof_delims,
ccb292952774 started adding agsyHOL as an experimental prover
blanchet
parents: 51998
diff changeset
   175
   known_failures = known_szs_status_failures,
ccb292952774 started adding agsyHOL as an experimental prover
blanchet
parents: 51998
diff changeset
   176
   prem_role = Hypothesis,
ccb292952774 started adding agsyHOL as an experimental prover
blanchet
parents: 51998
diff changeset
   177
   best_slices =
ccb292952774 started adding agsyHOL as an experimental prover
blanchet
parents: 51998
diff changeset
   178
     (* FUDGE *)
ccb292952774 started adding agsyHOL as an experimental prover
blanchet
parents: 51998
diff changeset
   179
     K [(1.0, (((60, ""), agsyhol_thf0, "mono_native_higher", keep_lamsN, false), ""))],
ccb292952774 started adding agsyHOL as an experimental prover
blanchet
parents: 51998
diff changeset
   180
   best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
53515
f5b678b155f6 adjusted number of generated monomorphic instances for new monomorphizer based on new evaluation (E, SPASS, Vampire)
blanchet
parents: 53225
diff changeset
   181
   best_max_new_mono_instances = default_max_new_mono_instances}
52073
ccb292952774 started adding agsyHOL as an experimental prover
blanchet
parents: 51998
diff changeset
   182
ccb292952774 started adding agsyHOL as an experimental prover
blanchet
parents: 51998
diff changeset
   183
val agsyhol = (agsyholN, fn () => agsyhol_config)
ccb292952774 started adding agsyHOL as an experimental prover
blanchet
parents: 51998
diff changeset
   184
ccb292952774 started adding agsyHOL as an experimental prover
blanchet
parents: 51998
diff changeset
   185
46643
a88bccd2b567 added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents: 46481
diff changeset
   186
(* Alt-Ergo *)
a88bccd2b567 added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents: 46481
diff changeset
   187
a88bccd2b567 added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents: 46481
diff changeset
   188
val alt_ergo_config : atp_config =
52754
d9d90d29860e added support for E 1.8's internal proof objects (eliminating the need for "eproof_ram")
blanchet
parents: 52151
diff changeset
   189
  {exec = K (["WHY3_HOME"], ["why3"]),
50927
31d864d5057a added E-Par support
blanchet
parents: 50333
diff changeset
   190
   arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
56379
d8ecce5d51cd use Alt-Ergo 0.95.2, the latest and greatest version
blanchet
parents: 56378
diff changeset
   191
       "--format tptp --prover 'Alt-Ergo,0.95.2,' --timelimit " ^
50927
31d864d5057a added E-Par support
blanchet
parents: 50333
diff changeset
   192
       string_of_int (to_secs 1 timeout) ^ " " ^ file_name,
46643
a88bccd2b567 added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents: 46481
diff changeset
   193
   proof_delims = [],
a88bccd2b567 added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents: 46481
diff changeset
   194
   known_failures =
a88bccd2b567 added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents: 46481
diff changeset
   195
     [(ProofMissing, ": Valid"),
a88bccd2b567 added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents: 46481
diff changeset
   196
      (TimedOut, ": Timeout"),
a88bccd2b567 added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents: 46481
diff changeset
   197
      (GaveUp, ": Unknown")],
47976
6b13451135a9 tuned names
blanchet
parents: 47974
diff changeset
   198
   prem_role = Hypothesis,
46643
a88bccd2b567 added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents: 46481
diff changeset
   199
   best_slices = fn _ =>
a88bccd2b567 added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents: 46481
diff changeset
   200
     (* FUDGE *)
57547
677b07d777c3 don't generate TPTP THF 'Definition's, because they complicate reconstruction for AgsyHOL and Satallax
blanchet
parents: 57293
diff changeset
   201
     [(1.0, (((100, ""), TFF Polymorphic, "poly_native", liftingN, false), ""))],
47962
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47955
diff changeset
   202
   best_max_mono_iters = default_max_mono_iters,
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47955
diff changeset
   203
   best_max_new_mono_instances = default_max_new_mono_instances}
46643
a88bccd2b567 added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents: 46481
diff changeset
   204
47646
9460f3f22365 tried to make SML/NJ happy
blanchet
parents: 47606
diff changeset
   205
val alt_ergo = (alt_ergoN, fn () => alt_ergo_config)
46643
a88bccd2b567 added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents: 46481
diff changeset
   206
a88bccd2b567 added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents: 46481
diff changeset
   207
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   208
(* E *)
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   209
52754
d9d90d29860e added support for E 1.8's internal proof objects (eliminating the need for "eproof_ram")
blanchet
parents: 52151
diff changeset
   210
fun is_e_at_least_1_8 () = string_ord (getenv "E_VERSION", "1.8") <> LESS
44420
3d0921b91a86 avoid TFF format with older Vampire versions
blanchet
parents: 44418
diff changeset
   211
43473
fb2713b803e6 deal with ATP time slices in a more flexible/robust fashion
blanchet
parents: 43467
diff changeset
   212
val e_smartN = "smart"
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   213
val e_autoN = "auto"
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   214
val e_fun_weightN = "fun_weight"
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   215
val e_sym_offset_weightN = "sym_offset_weight"
41725
7cca2de89296 added support for bleeding-edge E weighting function "SymOffsetsWeight"
blanchet
parents: 41335
diff changeset
   216
47032
73cdeed236c0 more weight attribute tuning
blanchet
parents: 47031
diff changeset
   217
val e_selection_heuristic =
73cdeed236c0 more weight attribute tuning
blanchet
parents: 47031
diff changeset
   218
  Attrib.setup_config_string @{binding atp_e_selection_heuristic} (K e_smartN)
41770
a710e96583d5 adjust fudge factors
blanchet
parents: 41769
diff changeset
   219
(* FUDGE *)
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   220
val e_default_fun_weight =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   221
  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
   222
val e_fun_weight_base =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   223
  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
   224
val e_fun_weight_span =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   225
  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
   226
val e_default_sym_offs_weight =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   227
  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
   228
val e_sym_offs_weight_base =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   229
  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
   230
val e_sym_offs_weight_span =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   231
  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
   232
47038
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47034
diff changeset
   233
fun e_selection_heuristic_case heuristic fw sow =
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47034
diff changeset
   234
  if heuristic = e_fun_weightN then fw
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47034
diff changeset
   235
  else if heuristic = e_sym_offset_weightN then sow
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47034
diff changeset
   236
  else raise Fail ("unexpected " ^ quote heuristic)
41725
7cca2de89296 added support for bleeding-edge E weighting function "SymOffsetsWeight"
blanchet
parents: 41335
diff changeset
   237
47038
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47034
diff changeset
   238
fun scaled_e_selection_weight ctxt heuristic w =
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47034
diff changeset
   239
  w * Config.get ctxt (e_selection_heuristic_case heuristic
47029
72802e2edda4 renamed E weight attribute
blanchet
parents: 46643
diff changeset
   240
                           e_fun_weight_span e_sym_offs_weight_span)
47038
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47034
diff changeset
   241
  + Config.get ctxt (e_selection_heuristic_case heuristic
47029
72802e2edda4 renamed E weight attribute
blanchet
parents: 46643
diff changeset
   242
                         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
   243
  |> 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
   244
47038
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47034
diff changeset
   245
fun e_selection_weight_arguments ctxt heuristic sel_weights =
51631
8d60dfb41d19 robustness w.r.t. unknown arguments
blanchet
parents: 51467
diff changeset
   246
  if heuristic = e_fun_weightN orelse heuristic = e_sym_offset_weightN then
43622
blanchet
parents: 43575
diff changeset
   247
    (* supplied by Stephan Schulz *)
41314
2dc1dfc1bc69 use the options provided by Stephan Schulz -- much better
blanchet
parents: 41313
diff changeset
   248
    "--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
   249
    \--destructive-er-aggressive --destructive-er --presat-simplify \
47505
e33d957ae2bf avoid option introduced in E 1.2 when invoking older versions of E
blanchet
parents: 47499
diff changeset
   250
    \--prefer-initial-clauses -winvfreqrank -c1 -Ginvfreqconjmax -F1 \
e33d957ae2bf avoid option introduced in E 1.2 when invoking older versions of E
blanchet
parents: 47499
diff changeset
   251
    \--delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*" ^
47038
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47034
diff changeset
   252
    e_selection_heuristic_case heuristic "FunWeight" "SymOffsetWeight" ^
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48232
diff changeset
   253
    "(SimulateSOS," ^
47038
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47034
diff changeset
   254
    (e_selection_heuristic_case heuristic
47029
72802e2edda4 renamed E weight attribute
blanchet
parents: 46643
diff changeset
   255
         e_default_fun_weight e_default_sym_offs_weight
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   256
     |> 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
   257
    ",20,1.5,1.5,1" ^
47030
7e80e14247fc internal renamings
blanchet
parents: 47029
diff changeset
   258
    (sel_weights ()
47029
72802e2edda4 renamed E weight attribute
blanchet
parents: 46643
diff changeset
   259
     |> map (fn (s, w) => "," ^ s ^ ":" ^
47038
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47034
diff changeset
   260
                          scaled_e_selection_weight ctxt heuristic w)
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   261
     |> implode) ^
41314
2dc1dfc1bc69 use the options provided by Stephan Schulz -- much better
blanchet
parents: 41313
diff changeset
   262
    "),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
   263
    \1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*\
57672
blanchet
parents: 57671
diff changeset
   264
    \FIFOWeight(PreferProcessed))' "
51631
8d60dfb41d19 robustness w.r.t. unknown arguments
blanchet
parents: 51467
diff changeset
   265
  else
57672
blanchet
parents: 57671
diff changeset
   266
    "-xAuto "
41313
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41269
diff changeset
   267
47038
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47034
diff changeset
   268
val e_ord_weights =
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47034
diff changeset
   269
  map (fn (s, w) => s ^ ":" ^ string_of_int w) #> space_implode ","
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47034
diff changeset
   270
fun e_ord_precedence [_] = ""
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47034
diff changeset
   271
  | e_ord_precedence info = info |> map fst |> space_implode "<"
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47034
diff changeset
   272
47039
1b36a05a070d added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
blanchet
parents: 47038
diff changeset
   273
fun e_term_order_info_arguments false false _ = ""
1b36a05a070d added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
blanchet
parents: 47038
diff changeset
   274
  | e_term_order_info_arguments gen_weights gen_prec ord_info =
47038
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47034
diff changeset
   275
    let val ord_info = ord_info () in
57672
blanchet
parents: 57671
diff changeset
   276
      (if gen_weights then "--order-weights='" ^ e_ord_weights ord_info ^ "' " else "") ^
blanchet
parents: 57671
diff changeset
   277
      (if gen_prec then "--precedence='" ^ e_ord_precedence ord_info ^ "' " else "")
47038
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47034
diff changeset
   278
    end
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47034
diff changeset
   279
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   280
val e_config : atp_config =
57671
dc5e1b1db9ba avoid 'eproof' and 'eproof_ram' scripts if possible (i.e. if 'eprover' can produce reasonable enough proofs for one-liner reconstruction)
blanchet
parents: 57636
diff changeset
   281
  {exec = fn full_proofs => (["E_HOME"],
dc5e1b1db9ba avoid 'eproof' and 'eproof_ram' scripts if possible (i.e. if 'eprover' can produce reasonable enough proofs for one-liner reconstruction)
blanchet
parents: 57636
diff changeset
   282
     if full_proofs orelse not (is_e_at_least_1_8 ()) then ["eproof_ram", "eproof"]
dc5e1b1db9ba avoid 'eproof' and 'eproof_ram' scripts if possible (i.e. if 'eprover' can produce reasonable enough proofs for one-liner reconstruction)
blanchet
parents: 57636
diff changeset
   283
     else ["eprover"]),
dc5e1b1db9ba avoid 'eproof' and 'eproof_ram' scripts if possible (i.e. if 'eprover' can produce reasonable enough proofs for one-liner reconstruction)
blanchet
parents: 57636
diff changeset
   284
   arguments = fn ctxt => fn full_proofs => fn heuristic => fn timeout => fn file_name =>
57008
10f68b83b474 use E 1.8's auto scheduler option
blanchet
parents: 56848
diff changeset
   285
     fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) =>
10f68b83b474 use E 1.8's auto scheduler option
blanchet
parents: 56848
diff changeset
   286
       (if is_e_at_least_1_8 () then "--auto-schedule " else "") ^
52754
d9d90d29860e added support for E 1.8's internal proof objects (eliminating the need for "eproof_ram")
blanchet
parents: 52151
diff changeset
   287
       "--tstp-in --tstp-out --silent " ^
57672
blanchet
parents: 57671
diff changeset
   288
       e_selection_weight_arguments ctxt heuristic sel_weights ^
blanchet
parents: 57671
diff changeset
   289
       e_term_order_info_arguments gen_weights gen_prec ord_info ^
57636
3ab503b04bdb stick to external proofs when invoking E, because they are more detailed and do not merge steps
blanchet
parents: 57547
diff changeset
   290
       "--term-ordering=" ^ (if is_lpo then "LPO4" else "KBO6") ^ " " ^
48651
fb461f81e76e added E-MaLeS to list of provers for testing
blanchet
parents: 48558
diff changeset
   291
       "--cpu-limit=" ^ string_of_int (to_secs 2 timeout) ^
57671
dc5e1b1db9ba avoid 'eproof' and 'eproof_ram' scripts if possible (i.e. if 'eprover' can produce reasonable enough proofs for one-liner reconstruction)
blanchet
parents: 57636
diff changeset
   292
       (if full_proofs orelse not (is_e_at_least_1_8 ()) then
dc5e1b1db9ba avoid 'eproof' and 'eproof_ram' scripts if possible (i.e. if 'eprover' can produce reasonable enough proofs for one-liner reconstruction)
blanchet
parents: 57636
diff changeset
   293
          " --output-level=5 --pcl-shell-level=" ^ (if full_proofs then "0" else "2")
dc5e1b1db9ba avoid 'eproof' and 'eproof_ram' scripts if possible (i.e. if 'eprover' can produce reasonable enough proofs for one-liner reconstruction)
blanchet
parents: 57636
diff changeset
   294
        else
dc5e1b1db9ba avoid 'eproof' and 'eproof_ram' scripts if possible (i.e. if 'eprover' can produce reasonable enough proofs for one-liner reconstruction)
blanchet
parents: 57636
diff changeset
   295
          " --proof-object=1") ^
52754
d9d90d29860e added support for E 1.8's internal proof objects (eliminating the need for "eproof_ram")
blanchet
parents: 52151
diff changeset
   296
       " " ^ file_name,
52073
ccb292952774 started adding agsyHOL as an experimental prover
blanchet
parents: 51998
diff changeset
   297
   proof_delims =
ccb292952774 started adding agsyHOL as an experimental prover
blanchet
parents: 51998
diff changeset
   298
     [("# SZS output start CNFRefutation", "# SZS output end CNFRefutation")] @
ccb292952774 started adding agsyHOL as an experimental prover
blanchet
parents: 51998
diff changeset
   299
     tstp_proof_delims,
36265
41c9e755e552 distinguish between the different ATP errors in the user interface;
blanchet
parents: 36264
diff changeset
   300
   known_failures =
45203
e3c13fa443ef more uniform SZS status handling
blanchet
parents: 45162
diff changeset
   301
     [(TimedOut, "Failure: Resource limit exceeded (time)"),
47972
96c9b8381909 better handling of incomplete TSTP proofs
blanchet
parents: 47962
diff changeset
   302
      (TimedOut, "time limit exceeded")] @
96c9b8381909 better handling of incomplete TSTP proofs
blanchet
parents: 47962
diff changeset
   303
     known_szs_status_failures,
47976
6b13451135a9 tuned names
blanchet
parents: 47974
diff changeset
   304
   prem_role = Conjecture,
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   305
   best_slices = fn ctxt =>
57636
3ab503b04bdb stick to external proofs when invoking E, because they are more detailed and do not merge steps
blanchet
parents: 57547
diff changeset
   306
     let val heuristic = Config.get ctxt e_selection_heuristic in
43474
423cd1ecf714 optimized E's time slicing, based on latest exhaustive Judgment Day results
blanchet
parents: 43473
diff changeset
   307
       (* FUDGE *)
47038
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47034
diff changeset
   308
       if heuristic = e_smartN then
51017
6a760e7f6933 tune slices further
blanchet
parents: 51016
diff changeset
   309
         [(0.15, (((128, meshN), FOF, "mono_tags??", combsN, false), e_fun_weightN)),
6a760e7f6933 tune slices further
blanchet
parents: 51016
diff changeset
   310
          (0.15, (((128, mashN), FOF, "mono_guards??", combsN, false), e_sym_offset_weightN)),
6a760e7f6933 tune slices further
blanchet
parents: 51016
diff changeset
   311
          (0.15, (((91, mepoN), FOF, "mono_tags??", combsN, false), e_autoN)),
6a760e7f6933 tune slices further
blanchet
parents: 51016
diff changeset
   312
          (0.15, (((1000, meshN), FOF, "poly_guards??", combsN, false), e_sym_offset_weightN)),
51214
4fb12e2598dc swap slices so that the last slice is more complete (for minimization)
blanchet
parents: 51205
diff changeset
   313
          (0.15, (((256, mepoN), FOF, "mono_tags??", liftingN, false), e_fun_weightN)),
4fb12e2598dc swap slices so that the last slice is more complete (for minimization)
blanchet
parents: 51205
diff changeset
   314
          (0.25, (((64, mashN), FOF, "mono_guards??", combsN, false), e_fun_weightN))]
43473
fb2713b803e6 deal with ATP time slices in a more flexible/robust fashion
blanchet
parents: 43467
diff changeset
   315
       else
51011
62b992e53eb8 store fact filter along with ATP slice
blanchet
parents: 50950
diff changeset
   316
         [(1.0, (((500, ""), FOF, "mono_tags??", combsN, false), heuristic))]
47962
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47955
diff changeset
   317
     end,
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47955
diff changeset
   318
   best_max_mono_iters = default_max_mono_iters,
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47955
diff changeset
   319
   best_max_new_mono_instances = default_max_new_mono_instances}
38454
9043eefe8d71 detect old Vampire and give a nicer error message
blanchet
parents: 38433
diff changeset
   320
47646
9460f3f22365 tried to make SML/NJ happy
blanchet
parents: 47606
diff changeset
   321
val e = (eN, fn () => e_config)
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   322
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   323
48651
fb461f81e76e added E-MaLeS to list of provers for testing
blanchet
parents: 48558
diff changeset
   324
(* E-MaLeS *)
fb461f81e76e added E-MaLeS to list of provers for testing
blanchet
parents: 48558
diff changeset
   325
fb461f81e76e added E-MaLeS to list of provers for testing
blanchet
parents: 48558
diff changeset
   326
val e_males_config : atp_config =
52754
d9d90d29860e added support for E 1.8's internal proof objects (eliminating the need for "eproof_ram")
blanchet
parents: 52151
diff changeset
   327
  {exec = K (["E_MALES_HOME"], ["emales.py"]),
50927
31d864d5057a added E-Par support
blanchet
parents: 50333
diff changeset
   328
   arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
31d864d5057a added E-Par support
blanchet
parents: 50333
diff changeset
   329
       "-t " ^ string_of_int (to_secs 1 timeout) ^ " -p " ^ file_name,
48651
fb461f81e76e added E-MaLeS to list of provers for testing
blanchet
parents: 48558
diff changeset
   330
   proof_delims = tstp_proof_delims,
fb461f81e76e added E-MaLeS to list of provers for testing
blanchet
parents: 48558
diff changeset
   331
   known_failures = #known_failures e_config,
fb461f81e76e added E-MaLeS to list of provers for testing
blanchet
parents: 48558
diff changeset
   332
   prem_role = Conjecture,
fb461f81e76e added E-MaLeS to list of provers for testing
blanchet
parents: 48558
diff changeset
   333
   best_slices =
fb461f81e76e added E-MaLeS to list of provers for testing
blanchet
parents: 48558
diff changeset
   334
     (* FUDGE *)
51018
a4a32c1d2866 tuned slicing (E-MaLeS and E-Par)
blanchet
parents: 51017
diff changeset
   335
     K [(0.25, (((500, meshN), FOF, "mono_guards??", combs_or_liftingN, false), "")),
a4a32c1d2866 tuned slicing (E-MaLeS and E-Par)
blanchet
parents: 51017
diff changeset
   336
        (0.25, (((150, meshN), FOF, "poly_tags??", combs_or_liftingN, false), "")),
a4a32c1d2866 tuned slicing (E-MaLeS and E-Par)
blanchet
parents: 51017
diff changeset
   337
        (0.25, (((50, meshN), FOF, "mono_tags??", combs_or_liftingN, false), "")),
a4a32c1d2866 tuned slicing (E-MaLeS and E-Par)
blanchet
parents: 51017
diff changeset
   338
        (0.25, (((1000, meshN), FOF, "poly_guards??", combsN, false), ""))],
48651
fb461f81e76e added E-MaLeS to list of provers for testing
blanchet
parents: 48558
diff changeset
   339
   best_max_mono_iters = default_max_mono_iters,
fb461f81e76e added E-MaLeS to list of provers for testing
blanchet
parents: 48558
diff changeset
   340
   best_max_new_mono_instances = default_max_new_mono_instances}
fb461f81e76e added E-MaLeS to list of provers for testing
blanchet
parents: 48558
diff changeset
   341
fb461f81e76e added E-MaLeS to list of provers for testing
blanchet
parents: 48558
diff changeset
   342
val e_males = (e_malesN, fn () => e_males_config)
fb461f81e76e added E-MaLeS to list of provers for testing
blanchet
parents: 48558
diff changeset
   343
fb461f81e76e added E-MaLeS to list of provers for testing
blanchet
parents: 48558
diff changeset
   344
50927
31d864d5057a added E-Par support
blanchet
parents: 50333
diff changeset
   345
(* E-Par *)
31d864d5057a added E-Par support
blanchet
parents: 50333
diff changeset
   346
31d864d5057a added E-Par support
blanchet
parents: 50333
diff changeset
   347
val e_par_config : atp_config =
52754
d9d90d29860e added support for E 1.8's internal proof objects (eliminating the need for "eproof_ram")
blanchet
parents: 52151
diff changeset
   348
  {exec = K (["E_HOME"], ["runepar.pl"]),
50927
31d864d5057a added E-Par support
blanchet
parents: 50333
diff changeset
   349
   arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
31d864d5057a added E-Par support
blanchet
parents: 50333
diff changeset
   350
       string_of_int (to_secs 1 timeout) ^ " 1 " (* SInE *) ^ file_name ^
31d864d5057a added E-Par support
blanchet
parents: 50333
diff changeset
   351
       " 2" (* proofs *),
31d864d5057a added E-Par support
blanchet
parents: 50333
diff changeset
   352
   proof_delims = tstp_proof_delims,
31d864d5057a added E-Par support
blanchet
parents: 50333
diff changeset
   353
   known_failures = #known_failures e_config,
31d864d5057a added E-Par support
blanchet
parents: 50333
diff changeset
   354
   prem_role = Conjecture,
31d864d5057a added E-Par support
blanchet
parents: 50333
diff changeset
   355
   best_slices = #best_slices e_males_config,
31d864d5057a added E-Par support
blanchet
parents: 50333
diff changeset
   356
   best_max_mono_iters = default_max_mono_iters,
31d864d5057a added E-Par support
blanchet
parents: 50333
diff changeset
   357
   best_max_new_mono_instances = default_max_new_mono_instances}
31d864d5057a added E-Par support
blanchet
parents: 50333
diff changeset
   358
31d864d5057a added E-Par support
blanchet
parents: 50333
diff changeset
   359
val e_par = (e_parN, fn () => e_par_config)
31d864d5057a added E-Par support
blanchet
parents: 50333
diff changeset
   360
31d864d5057a added E-Par support
blanchet
parents: 50333
diff changeset
   361
48700
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   362
(* iProver *)
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   363
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   364
val iprover_config : atp_config =
52754
d9d90d29860e added support for E 1.8's internal proof objects (eliminating the need for "eproof_ram")
blanchet
parents: 52151
diff changeset
   365
  {exec = K (["IPROVER_HOME"], ["iprover"]),
50927
31d864d5057a added E-Par support
blanchet
parents: 50333
diff changeset
   366
   arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
48720
95669b431edd proper quoting
blanchet
parents: 48716
diff changeset
   367
       "--clausifier \"$IPROVER_HOME\"/vclausify_rel --time_out_real " ^
50927
31d864d5057a added E-Par support
blanchet
parents: 50333
diff changeset
   368
       string_of_real (Time.toReal timeout) ^ " " ^ file_name,
48700
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   369
   proof_delims = tstp_proof_delims,
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   370
   known_failures =
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   371
     [(ProofIncomplete, "% SZS output start CNFRefutation")] @
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   372
     known_szs_status_failures,
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   373
   prem_role = Hypothesis,
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   374
   best_slices =
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   375
     (* FUDGE *)
51011
62b992e53eb8 store fact filter along with ATP slice
blanchet
parents: 50950
diff changeset
   376
     K [(1.0, (((150, ""), FOF, "mono_guards??", liftingN, false), ""))],
48700
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   377
   best_max_mono_iters = default_max_mono_iters,
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   378
   best_max_new_mono_instances = default_max_new_mono_instances}
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   379
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   380
val iprover = (iproverN, fn () => iprover_config)
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   381
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   382
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   383
(* iProver-Eq *)
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   384
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   385
val iprover_eq_config : atp_config =
52754
d9d90d29860e added support for E 1.8's internal proof objects (eliminating the need for "eproof_ram")
blanchet
parents: 52151
diff changeset
   386
  {exec = K (["IPROVER_EQ_HOME"], ["iprover-eq"]),
48700
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   387
   arguments = #arguments iprover_config,
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   388
   proof_delims = #proof_delims iprover_config,
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   389
   known_failures = #known_failures iprover_config,
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   390
   prem_role = #prem_role iprover_config,
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   391
   best_slices = #best_slices iprover_config,
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   392
   best_max_mono_iters = #best_max_mono_iters iprover_config,
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   393
   best_max_new_mono_instances = #best_max_new_mono_instances iprover_config}
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   394
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   395
val iprover_eq = (iprover_eqN, fn () => iprover_eq_config)
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   396
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   397
44099
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   398
(* LEO-II *)
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   399
54197
994ebb795b75 use definitions for LEO-II as well -- this simplifies the code and matches some users' expectations
blanchet
parents: 53586
diff changeset
   400
val leo2_thf0 = THF (Monomorphic, THF_Without_Choice)
44754
265174356212 added dummy polymorphic THF system
blanchet
parents: 44596
diff changeset
   401
44099
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   402
val leo2_config : atp_config =
52754
d9d90d29860e added support for E 1.8's internal proof objects (eliminating the need for "eproof_ram")
blanchet
parents: 52151
diff changeset
   403
  {exec = K (["LEO2_HOME"], ["leo.opt", "leo"]),
57759
d7454ee84f34 more precise handling of LEO-II skolemization
blanchet
parents: 57707
diff changeset
   404
   arguments = fn _ => fn full_proofs => fn _ => fn timeout => fn file_name => fn _ =>
d7454ee84f34 more precise handling of LEO-II skolemization
blanchet
parents: 57707
diff changeset
   405
     "--foatp e --atp e=\"$E_HOME\"/eprover \
d7454ee84f34 more precise handling of LEO-II skolemization
blanchet
parents: 57707
diff changeset
   406
     \--atp epclextract=\"$E_HOME\"/epclextract \
d7454ee84f34 more precise handling of LEO-II skolemization
blanchet
parents: 57707
diff changeset
   407
     \--proofoutput 1 --timeout " ^ string_of_int (to_secs 1 timeout) ^ " " ^
d7454ee84f34 more precise handling of LEO-II skolemization
blanchet
parents: 57707
diff changeset
   408
     (if full_proofs then "--notReplLeibnizEQ --notReplAndrewsEQ --notUseExtCnfCmbd " else "") ^
d7454ee84f34 more precise handling of LEO-II skolemization
blanchet
parents: 57707
diff changeset
   409
     file_name,
44099
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   410
   proof_delims = tstp_proof_delims,
45207
1d13334628a9 one more LEO-II failure
blanchet
parents: 45203
diff changeset
   411
   known_failures =
47974
08d2dcc2dab9 improved LEO-II definition handling -- still hoping for a fix directly in LEO-II
blanchet
parents: 47972
diff changeset
   412
     [(TimedOut, "CPU time limit exceeded, terminating"),
47972
96c9b8381909 better handling of incomplete TSTP proofs
blanchet
parents: 47962
diff changeset
   413
      (GaveUp, "No.of.Axioms")] @
96c9b8381909 better handling of incomplete TSTP proofs
blanchet
parents: 47962
diff changeset
   414
     known_szs_status_failures,
47976
6b13451135a9 tuned names
blanchet
parents: 47974
diff changeset
   415
   prem_role = Hypothesis,
47914
94f37848b7c9 LEO-II's "--sos" option confusingly disables rather than enables SOS, and SOS seems to be ignored anyway; also, pass a number of facts that's more appropriate for each prover
blanchet
parents: 47912
diff changeset
   416
   best_slices =
44099
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   417
     (* FUDGE *)
51011
62b992e53eb8 store fact filter along with ATP slice
blanchet
parents: 50950
diff changeset
   418
     K [(1.0, (((40, ""), leo2_thf0, "mono_native_higher", keep_lamsN, false), ""))],
47962
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47955
diff changeset
   419
   best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
53515
f5b678b155f6 adjusted number of generated monomorphic instances for new monomorphizer based on new evaluation (E, SPASS, Vampire)
blanchet
parents: 53225
diff changeset
   420
   best_max_new_mono_instances = default_max_new_mono_instances}
39491
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39375
diff changeset
   421
47646
9460f3f22365 tried to make SML/NJ happy
blanchet
parents: 47606
diff changeset
   422
val leo2 = (leo2N, fn () => leo2_config)
44099
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   423
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   424
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   425
(* Satallax *)
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   426
52097
f353fe3c2b92 disabled choice in Satallax
blanchet
parents: 52095
diff changeset
   427
(* Choice is disabled until there is proper reconstruction for it. *)
54197
994ebb795b75 use definitions for LEO-II as well -- this simplifies the code and matches some users' expectations
blanchet
parents: 53586
diff changeset
   428
val satallax_thf0 = THF (Monomorphic, THF_Without_Choice)
44754
265174356212 added dummy polymorphic THF system
blanchet
parents: 44596
diff changeset
   429
44099
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   430
val satallax_config : atp_config =
52754
d9d90d29860e added support for E 1.8's internal proof objects (eliminating the need for "eproof_ram")
blanchet
parents: 52151
diff changeset
   431
  {exec = K (["SATALLAX_HOME"], ["satallax.opt", "satallax"]),
50927
31d864d5057a added E-Par support
blanchet
parents: 50333
diff changeset
   432
   arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
57707
0242e9578828 imported patch satallax_proof_support_Sledgehammer
fleury
parents: 57672
diff changeset
   433
       "-p tstp -t " ^ string_of_int (to_secs 1 timeout) ^ " " ^ file_name,
45162
170dffc6df75 parse Satallax unsat cores
blanchet
parents: 44786
diff changeset
   434
   proof_delims =
57707
0242e9578828 imported patch satallax_proof_support_Sledgehammer
fleury
parents: 57672
diff changeset
   435
     [("% SZS output start Proof", "% SZS output end Proof")],
45203
e3c13fa443ef more uniform SZS status handling
blanchet
parents: 45162
diff changeset
   436
   known_failures = known_szs_status_failures,
47981
df35a8dd6368 gracefully handle definition-looking premises
blanchet
parents: 47976
diff changeset
   437
   prem_role = Hypothesis,
44416
cabd06b69c18 added formats to the slice and use TFF for remote Vampire
blanchet
parents: 44391
diff changeset
   438
   best_slices =
44754
265174356212 added dummy polymorphic THF system
blanchet
parents: 44596
diff changeset
   439
     (* FUDGE *)
51011
62b992e53eb8 store fact filter along with ATP slice
blanchet
parents: 50950
diff changeset
   440
     K [(1.0, (((60, ""), satallax_thf0, "mono_native_higher", keep_lamsN, false), ""))],
47962
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47955
diff changeset
   441
   best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
53515
f5b678b155f6 adjusted number of generated monomorphic instances for new monomorphizer based on new evaluation (E, SPASS, Vampire)
blanchet
parents: 53225
diff changeset
   442
   best_max_new_mono_instances = default_max_new_mono_instances}
44099
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   443
47646
9460f3f22365 tried to make SML/NJ happy
blanchet
parents: 47606
diff changeset
   444
val satallax = (satallaxN, fn () => satallax_config)
44099
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   445
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   446
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   447
(* 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
   448
48005
eeede26f2721 killed SPASS 3.5/3.7 FLOTTER hack -- requires users to upgrade to SPASS 3.8
blanchet
parents: 48004
diff changeset
   449
val spass_H1SOS = "-Heuristic=1 -SOS"
50333
20c69b00e73c tweak SPASS default a tiny bit, so that a more interesting heuristic is chosen when "slicing=false" (for experiments)
blanchet
parents: 49991
diff changeset
   450
val spass_H2 = "-Heuristic=2"
48005
eeede26f2721 killed SPASS 3.5/3.7 FLOTTER hack -- requires users to upgrade to SPASS 3.8
blanchet
parents: 48004
diff changeset
   451
val spass_H2LR0LT0 = "-Heuristic=2 -LR=0 -LT=0"
eeede26f2721 killed SPASS 3.5/3.7 FLOTTER hack -- requires users to upgrade to SPASS 3.8
blanchet
parents: 48004
diff changeset
   452
val spass_H2NuVS0 = "-Heuristic=2 -RNuV=1 -Sorts=0"
eeede26f2721 killed SPASS 3.5/3.7 FLOTTER hack -- requires users to upgrade to SPASS 3.8
blanchet
parents: 48004
diff changeset
   453
val spass_H2NuVS0Red2 = "-Heuristic=2 -RNuV=1 -Sorts=0 -RFRew=2 -RBRew=2 -RTaut=2"
50333
20c69b00e73c tweak SPASS default a tiny bit, so that a more interesting heuristic is chosen when "slicing=false" (for experiments)
blanchet
parents: 49991
diff changeset
   454
val spass_H2SOS = "-Heuristic=2 -SOS"
47055
16e2633f3b4b made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
blanchet
parents: 47053
diff changeset
   455
50950
a145ee10371b make SPASS more configurable, for experiments
blanchet
parents: 50927
diff changeset
   456
val spass_extra_options =
a145ee10371b make SPASS more configurable, for experiments
blanchet
parents: 50927
diff changeset
   457
  Attrib.setup_config_string @{binding atp_spass_extra_options} (K "")
a145ee10371b make SPASS more configurable, for experiments
blanchet
parents: 50927
diff changeset
   458
48005
eeede26f2721 killed SPASS 3.5/3.7 FLOTTER hack -- requires users to upgrade to SPASS 3.8
blanchet
parents: 48004
diff changeset
   459
(* FIXME: Make "SPASS_NEW_HOME" legacy. *)
eeede26f2721 killed SPASS 3.5/3.7 FLOTTER hack -- requires users to upgrade to SPASS 3.8
blanchet
parents: 48004
diff changeset
   460
val spass_config : atp_config =
52754
d9d90d29860e added support for E 1.8's internal proof objects (eliminating the need for "eproof_ram")
blanchet
parents: 52151
diff changeset
   461
  {exec = K (["SPASS_NEW_HOME", "SPASS_HOME"], ["SPASS"]),
52151
de43876e77bf disable SPASS's splitting if Isar proofs are desired, because these are not handled by the proof reconstruction code (and it's not clear how to handle them considering the lack of documentation)
blanchet
parents: 52097
diff changeset
   462
   arguments = fn _ => fn full_proofs => fn extra_options => fn timeout =>
de43876e77bf disable SPASS's splitting if Isar proofs are desired, because these are not handled by the proof reconstruction code (and it's not clear how to handle them considering the lack of documentation)
blanchet
parents: 52097
diff changeset
   463
       fn file_name => fn _ =>
de43876e77bf disable SPASS's splitting if Isar proofs are desired, because these are not handled by the proof reconstruction code (and it's not clear how to handle them considering the lack of documentation)
blanchet
parents: 52097
diff changeset
   464
       "-Isabelle=1 " ^ (if full_proofs then "-Splits=0 " else "") ^
de43876e77bf disable SPASS's splitting if Isar proofs are desired, because these are not handled by the proof reconstruction code (and it's not clear how to handle them considering the lack of documentation)
blanchet
parents: 52097
diff changeset
   465
       "-TimeLimit=" ^ string_of_int (to_secs 1 timeout) ^ " " ^ file_name
de43876e77bf disable SPASS's splitting if Isar proofs are desired, because these are not handled by the proof reconstruction code (and it's not clear how to handle them considering the lack of documentation)
blanchet
parents: 52097
diff changeset
   466
       |> extra_options <> "" ? prefix (extra_options ^ " "),
36369
d2cd0d04b8e6 handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents: 36289
diff changeset
   467
   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
   468
   known_failures =
53225
16235bb41881 got rid of old error -- users who install SPASS manually are responsible for any version mismatches
blanchet
parents: 52995
diff changeset
   469
     [(GaveUp, "SPASS beiseite: Completion found"),
36370
a4f601daa175 centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents: 36369
diff changeset
   470
      (TimedOut, "SPASS beiseite: Ran out of time"),
36965
67ae217c6b5c identify common SPASS error more clearly
blanchet
parents: 36924
diff changeset
   471
      (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
37413
e856582fe9c4 improve ATP-specific error messages
blanchet
parents: 37347
diff changeset
   472
      (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
   473
      (MalformedInput, "Free Variable"),
44391
7b4104df2be6 gracefully handle empty SPASS problems
blanchet
parents: 44235
diff changeset
   474
      (Unprovable, "No formulae and clauses found in input file"),
47972
96c9b8381909 better handling of incomplete TSTP proofs
blanchet
parents: 47962
diff changeset
   475
      (InternalError, "Please report this error")] @
96c9b8381909 better handling of incomplete TSTP proofs
blanchet
parents: 47962
diff changeset
   476
      known_perl_failures,
47976
6b13451135a9 tuned names
blanchet
parents: 47974
diff changeset
   477
   prem_role = Conjecture,
50950
a145ee10371b make SPASS more configurable, for experiments
blanchet
parents: 50927
diff changeset
   478
   best_slices = fn ctxt =>
42723
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42710
diff changeset
   479
     (* FUDGE *)
51016
02cb70db9ede tweak ATP slices further
blanchet
parents: 51012
diff changeset
   480
     [(0.1667, (((150, meshN), DFG Monomorphic, "mono_native", combsN, true), "")),
02cb70db9ede tweak ATP slices further
blanchet
parents: 51012
diff changeset
   481
      (0.1667, (((500, meshN), DFG Monomorphic, "mono_native", liftingN, true), spass_H2SOS)),
02cb70db9ede tweak ATP slices further
blanchet
parents: 51012
diff changeset
   482
      (0.1666, (((50, meshN), DFG Monomorphic,  "mono_native", liftingN, true), spass_H2LR0LT0)),
02cb70db9ede tweak ATP slices further
blanchet
parents: 51012
diff changeset
   483
      (0.1000, (((250, meshN), DFG Monomorphic, "mono_native", combsN, true), spass_H2NuVS0)),
02cb70db9ede tweak ATP slices further
blanchet
parents: 51012
diff changeset
   484
      (0.1000, (((1000, mepoN), DFG Monomorphic, "mono_native", liftingN, true), spass_H1SOS)),
02cb70db9ede tweak ATP slices further
blanchet
parents: 51012
diff changeset
   485
      (0.1000, (((150, meshN), DFG Monomorphic, "poly_guards??", liftingN, false), spass_H2NuVS0Red2)),
02cb70db9ede tweak ATP slices further
blanchet
parents: 51012
diff changeset
   486
      (0.1000, (((300, meshN), DFG Monomorphic, "mono_native", combsN, true), spass_H2SOS)),
02cb70db9ede tweak ATP slices further
blanchet
parents: 51012
diff changeset
   487
      (0.1000, (((100, meshN), DFG Monomorphic, "mono_native", combs_and_liftingN, true), spass_H2))]
50950
a145ee10371b make SPASS more configurable, for experiments
blanchet
parents: 50927
diff changeset
   488
     |> (case Config.get ctxt spass_extra_options of
a145ee10371b make SPASS more configurable, for experiments
blanchet
parents: 50927
diff changeset
   489
           "" => I
a145ee10371b make SPASS more configurable, for experiments
blanchet
parents: 50927
diff changeset
   490
         | opts => map (apsnd (apsnd (K opts)))),
47962
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47955
diff changeset
   491
   best_max_mono_iters = default_max_mono_iters,
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47955
diff changeset
   492
   best_max_new_mono_instances = default_max_new_mono_instances}
38454
9043eefe8d71 detect old Vampire and give a nicer error message
blanchet
parents: 38433
diff changeset
   493
48005
eeede26f2721 killed SPASS 3.5/3.7 FLOTTER hack -- requires users to upgrade to SPASS 3.8
blanchet
parents: 48004
diff changeset
   494
val spass = (spassN, fn () => spass_config)
38454
9043eefe8d71 detect old Vampire and give a nicer error message
blanchet
parents: 38433
diff changeset
   495
52073
ccb292952774 started adding agsyHOL as an experimental prover
blanchet
parents: 51998
diff changeset
   496
37509
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents: 37506
diff changeset
   497
(* Vampire *)
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents: 37506
diff changeset
   498
56380
9bb2856cc845 don't pass Vampire option that doesn't exist anymore (and that wasn't strictly necessary with older Vampires)
blanchet
parents: 56379
diff changeset
   499
(* Vampire 1.8 has TFF0 support, but the support was buggy until revision
48007
955ea323ddcc tweaked remote Vampire setup
blanchet
parents: 48005
diff changeset
   500
   1435 (or shortly before). *)
51873
blanchet
parents: 51872
diff changeset
   501
fun is_vampire_at_least_1_8 () = string_ord (getenv "VAMPIRE_VERSION", "1.8") <> LESS
blanchet
parents: 51872
diff changeset
   502
fun is_vampire_beyond_1_8 () = string_ord (getenv "VAMPIRE_VERSION", "1.8") = GREATER
44420
3d0921b91a86 avoid TFF format with older Vampire versions
blanchet
parents: 44418
diff changeset
   503
52995
ab98feb66684 Vampire 3.0 requires types to be declared -- make it happy (and get rid of "implicit" types since only Satallax seems to support them anymore)
blanchet
parents: 52754
diff changeset
   504
val vampire_tff0 = TFF Monomorphic
44589
0a1dfc6365e9 first step towards polymorphic TFF + changed defaults for Vampire
blanchet
parents: 44586
diff changeset
   505
58084
9f77084444df pass options to remote Vampire
blanchet
parents: 57759
diff changeset
   506
val vampire_basic_options = "--proof tptp --output_axiom_names on --mode casc"
9f77084444df pass options to remote Vampire
blanchet
parents: 57759
diff changeset
   507
9f77084444df pass options to remote Vampire
blanchet
parents: 57759
diff changeset
   508
(* cf. p. 20 of http://www.complang.tuwien.ac.at/lkovacs/Cade23_Tutorial_Slides/Session2_Slides.pdf *)
9f77084444df pass options to remote Vampire
blanchet
parents: 57759
diff changeset
   509
val vampire_full_proof_options =
9f77084444df pass options to remote Vampire
blanchet
parents: 57759
diff changeset
   510
  " --forced_options splitting=off:equality_proxy=off:general_splitting=off:inequality_splitting=0:\
9f77084444df pass options to remote Vampire
blanchet
parents: 57759
diff changeset
   511
  \naming=0"
9f77084444df pass options to remote Vampire
blanchet
parents: 57759
diff changeset
   512
9f77084444df pass options to remote Vampire
blanchet
parents: 57759
diff changeset
   513
val remote_vampire_full_proof_command =
9f77084444df pass options to remote Vampire
blanchet
parents: 57759
diff changeset
   514
  "vampire " ^ vampire_basic_options ^ " " ^ vampire_full_proof_options ^ " -t %d %s"
9f77084444df pass options to remote Vampire
blanchet
parents: 57759
diff changeset
   515
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   516
val vampire_config : atp_config =
52754
d9d90d29860e added support for E 1.8's internal proof objects (eliminating the need for "eproof_ram")
blanchet
parents: 52151
diff changeset
   517
  {exec = K (["VAMPIRE_HOME"], ["vampire"]),
58084
9f77084444df pass options to remote Vampire
blanchet
parents: 57759
diff changeset
   518
   arguments = fn _ => fn full_proofs => fn sos => fn timeout => fn file_name => fn _ =>
9f77084444df pass options to remote Vampire
blanchet
parents: 57759
diff changeset
   519
     vampire_basic_options ^
9f77084444df pass options to remote Vampire
blanchet
parents: 57759
diff changeset
   520
     (if is_vampire_at_least_1_8 () andalso full_proofs then " " ^ vampire_full_proof_options
9f77084444df pass options to remote Vampire
blanchet
parents: 57759
diff changeset
   521
      else "") ^
9f77084444df pass options to remote Vampire
blanchet
parents: 57759
diff changeset
   522
     " -t " ^ string_of_int (to_secs 1 timeout) ^ " --input_file " ^ file_name
9f77084444df pass options to remote Vampire
blanchet
parents: 57759
diff changeset
   523
     |> 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
   524
   proof_delims =
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents: 37506
diff changeset
   525
     [("=========== Refutation ==========",
52073
ccb292952774 started adding agsyHOL as an experimental prover
blanchet
parents: 51998
diff changeset
   526
       "======= End of refutation =======")] @
ccb292952774 started adding agsyHOL as an experimental prover
blanchet
parents: 51998
diff changeset
   527
     tstp_proof_delims,
37509
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents: 37506
diff changeset
   528
   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
   529
     [(GaveUp, "UNPROVABLE"),
59284a13abc4 support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents: 42999
diff changeset
   530
      (GaveUp, "CANNOT PROVE"),
37509
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents: 37506
diff changeset
   531
      (Unprovable, "Satisfiability detected"),
38647
5500241da479 play with fudge factor + parse one more Vampire error
blanchet
parents: 38646
diff changeset
   532
      (Unprovable, "Termination reason: Satisfiable"),
47972
96c9b8381909 better handling of incomplete TSTP proofs
blanchet
parents: 47962
diff changeset
   533
      (Interrupted, "Aborted by signal SIGINT")] @
96c9b8381909 better handling of incomplete TSTP proofs
blanchet
parents: 47962
diff changeset
   534
     known_szs_status_failures,
47976
6b13451135a9 tuned names
blanchet
parents: 47974
diff changeset
   535
   prem_role = 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
   536
   best_slices = fn ctxt =>
42723
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42710
diff changeset
   537
     (* FUDGE *)
48653
6ac7fd9b3a54 support older versions of Vampire
blanchet
parents: 48651
diff changeset
   538
     (if is_vampire_beyond_1_8 () then
51016
02cb70db9ede tweak ATP slices further
blanchet
parents: 51012
diff changeset
   539
        [(0.333, (((500, meshN), vampire_tff0, "mono_guards??", combs_or_liftingN, false), sosN)),
02cb70db9ede tweak ATP slices further
blanchet
parents: 51012
diff changeset
   540
         (0.333, (((150, meshN), vampire_tff0, "poly_tags??", combs_or_liftingN, false), sosN)),
51017
6a760e7f6933 tune slices further
blanchet
parents: 51016
diff changeset
   541
         (0.334, (((50, meshN), vampire_tff0, "mono_native", combs_or_liftingN, false), no_sosN))]
47055
16e2633f3b4b made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
blanchet
parents: 47053
diff changeset
   542
      else
51016
02cb70db9ede tweak ATP slices further
blanchet
parents: 51012
diff changeset
   543
        [(0.333, (((150, meshN), FOF, "poly_guards??", combs_or_liftingN, false), sosN)),
51011
62b992e53eb8 store fact filter along with ATP slice
blanchet
parents: 50950
diff changeset
   544
         (0.333, (((500, meshN), FOF, "mono_tags??", combs_or_liftingN, false), sosN)),
51016
02cb70db9ede tweak ATP slices further
blanchet
parents: 51012
diff changeset
   545
         (0.334, (((50, meshN), FOF, "mono_guards??", combs_or_liftingN, false), no_sosN))])
58084
9f77084444df pass options to remote Vampire
blanchet
parents: 57759
diff changeset
   546
     |> Config.get ctxt force_sos ? (hd #> apfst (K 1.0) #> single),
47962
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47955
diff changeset
   547
   best_max_mono_iters = default_max_mono_iters,
53515
f5b678b155f6 adjusted number of generated monomorphic instances for new monomorphizer based on new evaluation (E, SPASS, Vampire)
blanchet
parents: 53225
diff changeset
   548
   best_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)}
38454
9043eefe8d71 detect old Vampire and give a nicer error message
blanchet
parents: 38433
diff changeset
   549
47646
9460f3f22365 tried to make SML/NJ happy
blanchet
parents: 47606
diff changeset
   550
val vampire = (vampireN, fn () => vampire_config)
37509
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents: 37506
diff changeset
   551
48803
ffa31bf5c662 tone down "z3_tptp", now that Z3 (starting with 4.1) no longer supports TPTP TFF0
blanchet
parents: 48801
diff changeset
   552
(* Z3 with TPTP syntax (half experimental, half legacy) *)
41740
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   553
52995
ab98feb66684 Vampire 3.0 requires types to be declared -- make it happy (and get rid of "implicit" types since only Satallax seems to support them anymore)
blanchet
parents: 52754
diff changeset
   554
val z3_tff0 = TFF Monomorphic
44589
0a1dfc6365e9 first step towards polymorphic TFF + changed defaults for Vampire
blanchet
parents: 44586
diff changeset
   555
44423
f74707e12d30 exploit TFF format in Z3 used as ATP, and renamed it "z3_tptp"
blanchet
parents: 44422
diff changeset
   556
val z3_tptp_config : atp_config =
56378
8fb4515818f7 updated Z3 TPTP to 4.3.1+
blanchet
parents: 54802
diff changeset
   557
  {exec = K (["Z3_TPTP_HOME"], ["z3_tptp"]),
50927
31d864d5057a added E-Par support
blanchet
parents: 50333
diff changeset
   558
   arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
57261
49c1db0313e6 give Z3 TPTP proofs a chance
blanchet
parents: 57255
diff changeset
   559
     "-proof -t:" ^ string_of_int (to_secs 1 timeout) ^ " -file:" ^ file_name,
56397
6e08b45432f6 improved parsing of "z3_tptp" proofs
blanchet
parents: 56380
diff changeset
   560
   proof_delims = [("SZS status Theorem", "")],
45203
e3c13fa443ef more uniform SZS status handling
blanchet
parents: 45162
diff changeset
   561
   known_failures = known_szs_status_failures,
47976
6b13451135a9 tuned names
blanchet
parents: 47974
diff changeset
   562
   prem_role = Hypothesis,
42723
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42710
diff changeset
   563
   best_slices =
44423
f74707e12d30 exploit TFF format in Z3 used as ATP, and renamed it "z3_tptp"
blanchet
parents: 44422
diff changeset
   564
     (* FUDGE *)
51011
62b992e53eb8 store fact filter along with ATP slice
blanchet
parents: 50950
diff changeset
   565
     K [(0.5, (((250, meshN), z3_tff0, "mono_native", combsN, false), "")),
62b992e53eb8 store fact filter along with ATP slice
blanchet
parents: 50950
diff changeset
   566
        (0.25, (((125, mepoN), z3_tff0, "mono_native", combsN, false), "")),
62b992e53eb8 store fact filter along with ATP slice
blanchet
parents: 50950
diff changeset
   567
        (0.125, (((62, mashN), z3_tff0, "mono_native", combsN, false), "")),
62b992e53eb8 store fact filter along with ATP slice
blanchet
parents: 50950
diff changeset
   568
        (0.125, (((31, meshN), z3_tff0, "mono_native", combsN, false), ""))],
47962
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47955
diff changeset
   569
   best_max_mono_iters = default_max_mono_iters,
53515
f5b678b155f6 adjusted number of generated monomorphic instances for new monomorphizer based on new evaluation (E, SPASS, Vampire)
blanchet
parents: 53225
diff changeset
   570
   best_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)}
41740
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   571
47646
9460f3f22365 tried to make SML/NJ happy
blanchet
parents: 47606
diff changeset
   572
val z3_tptp = (z3_tptpN, fn () => z3_tptp_config)
41740
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   573
44590
3a8a31be92d2 added dummy PFF prover, for debugging purposes
blanchet
parents: 44589
diff changeset
   574
57154
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 57008
diff changeset
   575
(* Zipperposition*)
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 57008
diff changeset
   576
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 57008
diff changeset
   577
val zipperposition_config : atp_config =
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 57008
diff changeset
   578
  {exec = K (["ZIPPERPOSITION_HOME"], ["zipperposition"]),
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 57008
diff changeset
   579
   arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 57008
diff changeset
   580
       "-print none -proof tstp -print-types -timeout " ^
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 57008
diff changeset
   581
       string_of_int (to_secs 1 timeout) ^ " " ^ file_name,
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 57008
diff changeset
   582
   proof_delims = tstp_proof_delims,
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 57008
diff changeset
   583
   known_failures = known_szs_status_failures,
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 57008
diff changeset
   584
   prem_role = Hypothesis,
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 57008
diff changeset
   585
   best_slices = fn _ =>
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 57008
diff changeset
   586
     (* FUDGE *)
57547
677b07d777c3 don't generate TPTP THF 'Definition's, because they complicate reconstruction for AgsyHOL and Satallax
blanchet
parents: 57293
diff changeset
   587
     [(1.0, (((100, ""), TFF Polymorphic, "poly_native", liftingN, false), ""))],
57154
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 57008
diff changeset
   588
   best_max_mono_iters = default_max_mono_iters,
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 57008
diff changeset
   589
   best_max_new_mono_instances = default_max_new_mono_instances}
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 57008
diff changeset
   590
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 57008
diff changeset
   591
val zipperposition = (zipperpositionN, fn () => zipperposition_config)
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 57008
diff changeset
   592
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 57008
diff changeset
   593
48131
1016664b8feb started adding polymophic SPASS output
blanchet
parents: 48130
diff changeset
   594
(* Not really a prover: Experimental Polymorphic THF and DFG output *)
44590
3a8a31be92d2 added dummy PFF prover, for debugging purposes
blanchet
parents: 44589
diff changeset
   595
51919
097b191d1f0d use right default for "uncurried_aliases" with polymorphic SPASS
blanchet
parents: 51873
diff changeset
   596
fun dummy_config prem_role format type_enc uncurried_aliases : atp_config =
52754
d9d90d29860e added support for E 1.8's internal proof objects (eliminating the need for "eproof_ram")
blanchet
parents: 52151
diff changeset
   597
  {exec = K (["ISABELLE_ATP"], ["scripts/dummy_atp"]),
50927
31d864d5057a added E-Par support
blanchet
parents: 50333
diff changeset
   598
   arguments = K (K (K (K (K (K ""))))),
44590
3a8a31be92d2 added dummy PFF prover, for debugging purposes
blanchet
parents: 44589
diff changeset
   599
   proof_delims = [],
45203
e3c13fa443ef more uniform SZS status handling
blanchet
parents: 45162
diff changeset
   600
   known_failures = known_szs_status_failures,
51467
60472a1b4536 use the right role for SPASS hypotheses
blanchet
parents: 51336
diff changeset
   601
   prem_role = prem_role,
45521
0cd6e59bd0b5 give each time slice its own lambda translation
blanchet
parents: 45365
diff changeset
   602
   best_slices =
51011
62b992e53eb8 store fact filter along with ATP slice
blanchet
parents: 50950
diff changeset
   603
     K [(1.0, (((200, ""), format, type_enc,
48716
1d2a12bb0640 stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
blanchet
parents: 48715
diff changeset
   604
                if is_format_higher_order format then keep_lamsN
51919
097b191d1f0d use right default for "uncurried_aliases" with polymorphic SPASS
blanchet
parents: 51873
diff changeset
   605
                else combsN, uncurried_aliases), ""))],
47962
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47955
diff changeset
   606
   best_max_mono_iters = default_max_mono_iters,
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47955
diff changeset
   607
   best_max_new_mono_instances = default_max_new_mono_instances}
44590
3a8a31be92d2 added dummy PFF prover, for debugging purposes
blanchet
parents: 44589
diff changeset
   608
54197
994ebb795b75 use definitions for LEO-II as well -- this simplifies the code and matches some users' expectations
blanchet
parents: 53586
diff changeset
   609
val dummy_thf_format = THF (Polymorphic, THF_With_Choice)
57293
4e619ee65a61 added 'dummy_thf_ml' prover for experiments with HOLyHammer
blanchet
parents: 57269
diff changeset
   610
54788
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54197
diff changeset
   611
val dummy_thf_config = dummy_config Hypothesis dummy_thf_format "poly_native_higher" false
47646
9460f3f22365 tried to make SML/NJ happy
blanchet
parents: 47606
diff changeset
   612
val dummy_thf = (dummy_thfN, fn () => dummy_thf_config)
44754
265174356212 added dummy polymorphic THF system
blanchet
parents: 44596
diff changeset
   613
57293
4e619ee65a61 added 'dummy_thf_ml' prover for experiments with HOLyHammer
blanchet
parents: 57269
diff changeset
   614
val dummy_thf_ml_config = dummy_config Hypothesis dummy_thf_format "ml_poly_native_higher" false
4e619ee65a61 added 'dummy_thf_ml' prover for experiments with HOLyHammer
blanchet
parents: 57269
diff changeset
   615
val dummy_thf_ml = (dummy_thf_mlN, fn () => dummy_thf_ml_config)
4e619ee65a61 added 'dummy_thf_ml' prover for experiments with HOLyHammer
blanchet
parents: 57269
diff changeset
   616
54788
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54197
diff changeset
   617
val spass_pirate_format = DFG Polymorphic
54802
9ce867291c76 made SML/NJ happier
blanchet
parents: 54788
diff changeset
   618
val remote_spass_pirate_config : atp_config =
54788
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54197
diff changeset
   619
  {exec = K (["ISABELLE_ATP"], ["scripts/remote_spass_pirate"]),
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54197
diff changeset
   620
   arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54197
diff changeset
   621
     string_of_int (to_secs 1 timeout) ^ " " ^ file_name,
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54197
diff changeset
   622
   proof_delims = [("Involved clauses:", "Involved clauses:")],
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54197
diff changeset
   623
   known_failures = known_szs_status_failures,
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54197
diff changeset
   624
   prem_role = #prem_role spass_config,
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54197
diff changeset
   625
   best_slices = K [(1.0, (((200, ""), spass_pirate_format, "tc_native", combsN, true), ""))],
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54197
diff changeset
   626
   best_max_mono_iters = default_max_mono_iters,
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54197
diff changeset
   627
   best_max_new_mono_instances = default_max_new_mono_instances}
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54197
diff changeset
   628
val remote_spass_pirate = (remote_prefix ^ spass_pirateN, fn () => remote_spass_pirate_config)
41740
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   629
52073
ccb292952774 started adding agsyHOL as an experimental prover
blanchet
parents: 51998
diff changeset
   630
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   631
(* Remote ATP invocation via SystemOnTPTP *)
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   632
49984
blanchet
parents: 48803
diff changeset
   633
val remote_systems = Synchronized.var "atp_remote_systems" ([] : string list)
31835
b686d4df54c2 check for current versions on server
immler@in.tum.de
parents: 31832
diff changeset
   634
49984
blanchet
parents: 48803
diff changeset
   635
fun get_remote_systems () =
58084
9f77084444df pass options to remote Vampire
blanchet
parents: 57759
diff changeset
   636
  TimeLimit.timeLimit (seconds 10.0) (fn () =>
9f77084444df pass options to remote Vampire
blanchet
parents: 57759
diff changeset
   637
    (case Isabelle_System.bash_output "\"$ISABELLE_ATP/scripts/remote_atp\" -w 2>&1" of
9f77084444df pass options to remote Vampire
blanchet
parents: 57759
diff changeset
   638
      (output, 0) => split_lines output
9f77084444df pass options to remote Vampire
blanchet
parents: 57759
diff changeset
   639
    | (output, _) =>
9f77084444df pass options to remote Vampire
blanchet
parents: 57759
diff changeset
   640
      (warning
9f77084444df pass options to remote Vampire
blanchet
parents: 57759
diff changeset
   641
         (case extract_known_atp_failure known_perl_failures output of
9f77084444df pass options to remote Vampire
blanchet
parents: 57759
diff changeset
   642
           SOME failure => string_of_atp_failure failure
9f77084444df pass options to remote Vampire
blanchet
parents: 57759
diff changeset
   643
         | NONE => trim_line output ^ "."); []))) ()
49991
e0761153fbd1 less verbose -- the warning will reach the users anyway by other means
blanchet
parents: 49990
diff changeset
   644
  handle TimeLimit.TimeOut => []
31835
b686d4df54c2 check for current versions on server
immler@in.tum.de
parents: 31832
diff changeset
   645
49984
blanchet
parents: 48803
diff changeset
   646
fun find_remote_system name [] systems =
42537
25ceb855a18b improve version handling -- prefer versions of ToFoF, SInE, and SNARK that are known to work
blanchet
parents: 42535
diff changeset
   647
    find_first (String.isPrefix (name ^ "---")) systems
49984
blanchet
parents: 48803
diff changeset
   648
  | find_remote_system name (version :: versions) 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
   649
    case find_first (String.isPrefix (name ^ "---" ^ version)) systems of
49984
blanchet
parents: 48803
diff changeset
   650
      NONE => find_remote_system name versions 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
   651
    | 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
   652
49984
blanchet
parents: 48803
diff changeset
   653
fun get_remote_system name versions =
blanchet
parents: 48803
diff changeset
   654
  Synchronized.change_result remote_systems
blanchet
parents: 48803
diff changeset
   655
      (fn systems => (if null systems then get_remote_systems () else systems)
blanchet
parents: 48803
diff changeset
   656
                     |> `(`(find_remote_system name versions)))
32864
a226f29d4bdc re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents: 32740
diff changeset
   657
49984
blanchet
parents: 48803
diff changeset
   658
fun the_remote_system name versions =
54788
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54197
diff changeset
   659
  (case get_remote_system name versions of
42955
576bd30cc4ea clearer SystemOnTPTP errors
blanchet
parents: 42954
diff changeset
   660
    (SOME sys, _) => sys
54788
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54197
diff changeset
   661
  | (NONE, []) => error "SystemOnTPTP is not available."
42955
576bd30cc4ea clearer SystemOnTPTP errors
blanchet
parents: 42954
diff changeset
   662
  | (NONE, syss) =>
54788
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54197
diff changeset
   663
    (case syss |> filter_out (String.isPrefix "%") |> filter_out (curry (op =) "") of
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54197
diff changeset
   664
      [] => error "SystemOnTPTP is currently not available."
49990
42209bfa1548 tuned messages
blanchet
parents: 49987
diff changeset
   665
    | [msg] => error ("SystemOnTPTP is currently not available: " ^ msg ^ ".")
46480
24990fae5f92 better error message
blanchet
parents: 46455
diff changeset
   666
    | syss =>
54788
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54197
diff changeset
   667
      error ("System " ^ quote name ^ " is not available at SystemOnTPTP.\n(Available systems: " ^
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54197
diff changeset
   668
        commas_quote syss ^ ".)")))
31835
b686d4df54c2 check for current versions on server
immler@in.tum.de
parents: 31832
diff changeset
   669
41148
f5229ab54284 added timeout max for remote server invocation
blanchet
parents: 40669
diff changeset
   670
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
   671
58084
9f77084444df pass options to remote Vampire
blanchet
parents: 57759
diff changeset
   672
fun remote_config system_name system_versions proof_delims known_failures prem_role best_slice =
52754
d9d90d29860e added support for E 1.8's internal proof objects (eliminating the need for "eproof_ram")
blanchet
parents: 52151
diff changeset
   673
  {exec = K (["ISABELLE_ATP"], ["scripts/remote_atp"]),
58084
9f77084444df pass options to remote Vampire
blanchet
parents: 57759
diff changeset
   674
   arguments = fn _ => fn full_proofs => fn full_proof_command => fn timeout => fn file_name => fn _ =>
9f77084444df pass options to remote Vampire
blanchet
parents: 57759
diff changeset
   675
     (if full_proofs andalso full_proof_command <> "" then "-c " ^ quote full_proof_command ^ " "
9f77084444df pass options to remote Vampire
blanchet
parents: 57759
diff changeset
   676
      else "") ^
54788
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54197
diff changeset
   677
     "-s " ^ the_remote_system system_name system_versions ^ " " ^
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54197
diff changeset
   678
     "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout)) ^
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54197
diff changeset
   679
     " " ^ file_name,
42962
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42955
diff changeset
   680
   proof_delims = union (op =) tstp_proof_delims proof_delims,
45203
e3c13fa443ef more uniform SZS status handling
blanchet
parents: 45162
diff changeset
   681
   known_failures = known_failures @ known_perl_failures @ known_says_failures,
47976
6b13451135a9 tuned names
blanchet
parents: 47974
diff changeset
   682
   prem_role = prem_role,
48716
1d2a12bb0640 stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
blanchet
parents: 48715
diff changeset
   683
   best_slices = fn ctxt => [(1.0, best_slice ctxt)],
47962
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47955
diff changeset
   684
   best_max_mono_iters = default_max_mono_iters,
58084
9f77084444df pass options to remote Vampire
blanchet
parents: 57759
diff changeset
   685
   best_max_new_mono_instances = default_max_new_mono_instances} : atp_config
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42332
diff changeset
   686
43500
4c357b7aa710 provide appropriate type system and number of fact defaults for remote ATPs
blanchet
parents: 43497
diff changeset
   687
fun remotify_config system_name system_versions best_slice
58084
9f77084444df pass options to remote Vampire
blanchet
parents: 57759
diff changeset
   688
    ({proof_delims, known_failures, prem_role, ...} : atp_config) =
9f77084444df pass options to remote Vampire
blanchet
parents: 57759
diff changeset
   689
  remote_config system_name system_versions proof_delims known_failures prem_role best_slice
38023
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
   690
58084
9f77084444df pass options to remote Vampire
blanchet
parents: 57759
diff changeset
   691
fun remote_atp name system_name system_versions proof_delims known_failures prem_role best_slice =
9f77084444df pass options to remote Vampire
blanchet
parents: 57759
diff changeset
   692
  (remote_prefix ^ name, fn () =>
9f77084444df pass options to remote Vampire
blanchet
parents: 57759
diff changeset
   693
     remote_config system_name system_versions proof_delims known_failures prem_role best_slice)
43500
4c357b7aa710 provide appropriate type system and number of fact defaults for remote ATPs
blanchet
parents: 43497
diff changeset
   694
fun remotify_atp (name, config) system_name system_versions best_slice =
58084
9f77084444df pass options to remote Vampire
blanchet
parents: 57759
diff changeset
   695
  (remote_prefix ^ name, remotify_config system_name system_versions best_slice o config)
28592
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
   696
57269
1df6f747f164 changed type encoding for new Waldmeister, to trigger filtering of 'dangerous' lemmas
blanchet
parents: 57265
diff changeset
   697
fun gen_remote_waldmeister name type_enc =
57265
cab38f7a3adb use right delimiters for Waldmeister proofs
blanchet
parents: 57264
diff changeset
   698
  remote_atp name "Waldmeister" ["710"] tstp_proof_delims
cab38f7a3adb use right delimiters for Waldmeister proofs
blanchet
parents: 57264
diff changeset
   699
    ([(OutOfResources, "Too many function symbols"),
cab38f7a3adb use right delimiters for Waldmeister proofs
blanchet
parents: 57264
diff changeset
   700
      (Inappropriate, "****  Unexpected end of file."),
cab38f7a3adb use right delimiters for Waldmeister proofs
blanchet
parents: 57264
diff changeset
   701
      (Crashed, "Unrecoverable Segmentation Fault")]
cab38f7a3adb use right delimiters for Waldmeister proofs
blanchet
parents: 57264
diff changeset
   702
     @ known_szs_status_failures)
57264
13db1d078743 added 'waldmeister_new' as ATP
blanchet
parents: 57262
diff changeset
   703
    Hypothesis
57269
1df6f747f164 changed type encoding for new Waldmeister, to trigger filtering of 'dangerous' lemmas
blanchet
parents: 57265
diff changeset
   704
    (K (((50, ""), CNF_UEQ, type_enc, combsN, false), "") (* FUDGE *))
57264
13db1d078743 added 'waldmeister_new' as ATP
blanchet
parents: 57262
diff changeset
   705
52995
ab98feb66684 Vampire 3.0 requires types to be declared -- make it happy (and get rid of "implicit" types since only Satallax seems to support them anymore)
blanchet
parents: 52754
diff changeset
   706
val explicit_tff0 = TFF Monomorphic
44589
0a1dfc6365e9 first step towards polymorphic TFF + changed defaults for Vampire
blanchet
parents: 44586
diff changeset
   707
52094
018cc7c7e640 updated remote provers
blanchet
parents: 52073
diff changeset
   708
val remote_agsyhol =
018cc7c7e640 updated remote provers
blanchet
parents: 52073
diff changeset
   709
  remotify_atp agsyhol "agsyHOL" ["1.0", "1"]
58084
9f77084444df pass options to remote Vampire
blanchet
parents: 57759
diff changeset
   710
    (K (((60, ""), agsyhol_thf0, "mono_native_higher", keep_lamsN, false), "") (* FUDGE *))
43500
4c357b7aa710 provide appropriate type system and number of fact defaults for remote ATPs
blanchet
parents: 43497
diff changeset
   711
val remote_e =
52094
018cc7c7e640 updated remote provers
blanchet
parents: 52073
diff changeset
   712
  remotify_atp e "EP" ["1.7", "1.6", "1.5", "1"]
58084
9f77084444df pass options to remote Vampire
blanchet
parents: 57759
diff changeset
   713
    (K (((750, ""), FOF, "mono_tags??", combsN, false), "") (* FUDGE *))
48700
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   714
val remote_iprover =
52094
018cc7c7e640 updated remote provers
blanchet
parents: 52073
diff changeset
   715
  remotify_atp iprover "iProver" ["0.99"]
58084
9f77084444df pass options to remote Vampire
blanchet
parents: 57759
diff changeset
   716
    (K (((150, ""), FOF, "mono_guards??", liftingN, false), "") (* FUDGE *))
48700
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   717
val remote_iprover_eq =
52094
018cc7c7e640 updated remote provers
blanchet
parents: 52073
diff changeset
   718
  remotify_atp iprover_eq "iProver-Eq" ["0.8"]
58084
9f77084444df pass options to remote Vampire
blanchet
parents: 57759
diff changeset
   719
    (K (((150, ""), FOF, "mono_guards??", liftingN, false), "") (* FUDGE *))
44099
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   720
val remote_leo2 =
52094
018cc7c7e640 updated remote provers
blanchet
parents: 52073
diff changeset
   721
  remotify_atp leo2 "LEO-II" ["1.5.0", "1.4", "1.3", "1.2", "1"]
58084
9f77084444df pass options to remote Vampire
blanchet
parents: 57759
diff changeset
   722
    (K (((40, ""), leo2_thf0, "mono_native_higher", liftingN, false), "") (* FUDGE *))
44099
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   723
val remote_satallax =
52094
018cc7c7e640 updated remote provers
blanchet
parents: 52073
diff changeset
   724
  remotify_atp satallax "Satallax" ["2.7", "2.3", "2"]
58084
9f77084444df pass options to remote Vampire
blanchet
parents: 57759
diff changeset
   725
    (K (((60, ""), satallax_thf0, "mono_native_higher", keep_lamsN, false), "") (* FUDGE *))
43500
4c357b7aa710 provide appropriate type system and number of fact defaults for remote ATPs
blanchet
parents: 43497
diff changeset
   726
val remote_vampire =
58084
9f77084444df pass options to remote Vampire
blanchet
parents: 57759
diff changeset
   727
  remotify_atp vampire "Vampire" ["3.0", "2.6", "2.5"]
9f77084444df pass options to remote Vampire
blanchet
parents: 57759
diff changeset
   728
    (K (((400, ""), vampire_tff0, "mono_native", combs_or_liftingN, false), remote_vampire_full_proof_command) (* FUDGE *))
44092
bf489e54d7f8 renamed E wrappers for consistency with CASC conventions
blanchet
parents: 43989
diff changeset
   729
val remote_e_sine =
47912
12de57c5eee5 get rid of "conj_sym_kind" -- most interesting provers now have built-in sorts, and for the others (e.g. E) "Hypothesis" isn't too bad a default
blanchet
parents: 47900
diff changeset
   730
  remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Conjecture
58084
9f77084444df pass options to remote Vampire
blanchet
parents: 57759
diff changeset
   731
    (K (((500, ""), FOF, "mono_guards??", combsN, false), "") (* FUDGE *))
41740
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   732
val remote_snark =
52094
018cc7c7e640 updated remote provers
blanchet
parents: 52073
diff changeset
   733
  remote_atp snarkN "SNARK" ["20120808r022", "20080805r029", "20080805r024"]
58084
9f77084444df pass options to remote Vampire
blanchet
parents: 57759
diff changeset
   734
    [("refutation.", "end_refutation.")] [] Hypothesis
9f77084444df pass options to remote Vampire
blanchet
parents: 57759
diff changeset
   735
    (K (((100, ""), explicit_tff0, "mono_native", liftingN, false), "") (* FUDGE *))
44092
bf489e54d7f8 renamed E wrappers for consistency with CASC conventions
blanchet
parents: 43989
diff changeset
   736
val remote_e_tofof =
47912
12de57c5eee5 get rid of "conj_sym_kind" -- most interesting provers now have built-in sorts, and for the others (e.g. E) "Hypothesis" isn't too bad a default
blanchet
parents: 47900
diff changeset
   737
  remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config) Hypothesis
58084
9f77084444df pass options to remote Vampire
blanchet
parents: 57759
diff changeset
   738
    (K (((150, ""), explicit_tff0, "mono_native", liftingN, false), "") (* FUDGE *))
57269
1df6f747f164 changed type encoding for new Waldmeister, to trigger filtering of 'dangerous' lemmas
blanchet
parents: 57265
diff changeset
   739
val remote_waldmeister = gen_remote_waldmeister waldmeisterN "raw_mono_tags??"
1df6f747f164 changed type encoding for new Waldmeister, to trigger filtering of 'dangerous' lemmas
blanchet
parents: 57265
diff changeset
   740
val remote_waldmeister_new = gen_remote_waldmeister waldmeister_newN "mono_args"
38454
9043eefe8d71 detect old Vampire and give a nicer error message
blanchet
parents: 38433
diff changeset
   741
52073
ccb292952774 started adding agsyHOL as an experimental prover
blanchet
parents: 51998
diff changeset
   742
38454
9043eefe8d71 detect old Vampire and give a nicer error message
blanchet
parents: 38433
diff changeset
   743
(* Setup *)
9043eefe8d71 detect old Vampire and give a nicer error message
blanchet
parents: 38433
diff changeset
   744
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   745
fun add_atp (name, config) thy =
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   746
  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
   747
  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
   748
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   749
fun get_atp thy name =
54788
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54197
diff changeset
   750
  fst (the (Symtab.lookup (Data.get thy) name))
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   751
  handle Option.Option => error ("Unknown ATP: " ^ name ^ ".")
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   752
41727
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41725
diff changeset
   753
val supported_atps = Symtab.keys o Data.get
36371
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36370
diff changeset
   754
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   755
fun is_atp_installed thy name =
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48232
diff changeset
   756
  let val {exec, ...} = get_atp thy name () in
57671
dc5e1b1db9ba avoid 'eproof' and 'eproof_ram' scripts if possible (i.e. if 'eprover' can produce reasonable enough proofs for one-liner reconstruction)
blanchet
parents: 57636
diff changeset
   757
    exists (fn var => getenv var <> "") (fst (exec false))
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   758
  end
36371
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36370
diff changeset
   759
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   760
fun refresh_systems_on_tptp () =
49984
blanchet
parents: 48803
diff changeset
   761
  Synchronized.change remote_systems (fn _ => get_remote_systems ())
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   762
47055
16e2633f3b4b made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
blanchet
parents: 47053
diff changeset
   763
fun effective_term_order ctxt atp =
16e2633f3b4b made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
blanchet
parents: 47053
diff changeset
   764
  let val ord = Config.get ctxt term_order in
16e2633f3b4b made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
blanchet
parents: 47053
diff changeset
   765
    if ord = smartN then
54788
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54197
diff changeset
   766
      {is_lpo = false, gen_weights = (atp = spassN), gen_prec = (atp = spassN),
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54197
diff changeset
   767
       gen_simp = String.isSuffix spass_pirateN atp}
47055
16e2633f3b4b made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
blanchet
parents: 47053
diff changeset
   768
    else
16e2633f3b4b made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
blanchet
parents: 47053
diff changeset
   769
      let val is_lpo = String.isSubstring lpoN ord in
54788
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54197
diff changeset
   770
        {is_lpo = is_lpo, gen_weights = not is_lpo andalso String.isSubstring xweightsN ord,
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54197
diff changeset
   771
         gen_prec = String.isSubstring xprecN ord, gen_simp = String.isSubstring xsimpN ord}
47055
16e2633f3b4b made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
blanchet
parents: 47053
diff changeset
   772
      end
16e2633f3b4b made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
blanchet
parents: 47053
diff changeset
   773
  end
16e2633f3b4b made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
blanchet
parents: 47053
diff changeset
   774
52073
ccb292952774 started adding agsyHOL as an experimental prover
blanchet
parents: 51998
diff changeset
   775
val atps =
54788
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54197
diff changeset
   776
  [agsyhol, alt_ergo, e, e_males, e_par, iprover, iprover_eq, leo2, satallax, spass, vampire,
57293
4e619ee65a61 added 'dummy_thf_ml' prover for experiments with HOLyHammer
blanchet
parents: 57269
diff changeset
   777
   z3_tptp, zipperposition, dummy_thf, dummy_thf_ml, remote_agsyhol, remote_e, remote_e_sine,
4e619ee65a61 added 'dummy_thf_ml' prover for experiments with HOLyHammer
blanchet
parents: 57269
diff changeset
   778
   remote_e_tofof, remote_iprover, remote_iprover_eq, remote_leo2, remote_satallax, remote_vampire,
4e619ee65a61 added 'dummy_thf_ml' prover for experiments with HOLyHammer
blanchet
parents: 57269
diff changeset
   779
   remote_snark, remote_spass_pirate, remote_waldmeister, remote_waldmeister_new]
47055
16e2633f3b4b made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
blanchet
parents: 47053
diff changeset
   780
57262
b2c629647a14 moved code around
blanchet
parents: 57261
diff changeset
   781
val _ = Theory.setup (fold add_atp atps)
35867
16279c4c7a33 move all ATP setup code into ATP_Wrapper
blanchet
parents: 35865
diff changeset
   782
28592
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
   783
end;