author | wenzelm |
Fri, 04 Jan 2019 23:22:53 +0100 | |
changeset 69593 | 3dda49e08b9d |
parent 68563 | 05fb05f94686 |
child 69717 | eb74ff534b27 |
permissions | -rw-r--r-- |
38047 | 1 |
(* Title: HOL/Tools/ATP/atp_systems.ML |
28592 | 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 | 4 |
|
36376 | 5 |
Setup for supported ATPs. |
28592 | 6 |
*) |
7 |
||
36376 | 8 |
signature ATP_SYSTEMS = |
28592 | 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 | 14 |
|
51011 | 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 | 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 | 29 |
val force_sos : bool Config.T |
47032 | 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 | 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 | 42 |
val spass_H1SOS : string |
43 |
val spass_H2 : string |
|
44 |
val spass_H2LR0LT0 : string |
|
45 |
val spass_H2NuVS0 : string |
|
46 |
val spass_H2NuVS0Red2 : string |
|
47 |
val spass_H2SOS : string |
|
48 |
val spass_extra_options : string Config.T |
|
68563 | 49 |
val is_vampire_noncommercial_license_accepted : unit -> bool option |
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
|
50 |
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
|
51 |
(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
|
52 |
string * (unit -> atp_config) |
47606
06dde48a1503
true delayed evaluation of "SPASS_VERSION" environment variable
blanchet
parents:
47506
diff
changeset
|
53 |
val add_atp : string * (unit -> atp_config) -> theory -> theory |
06dde48a1503
true delayed evaluation of "SPASS_VERSION" environment variable
blanchet
parents:
47506
diff
changeset
|
54 |
val get_atp : theory -> string -> (unit -> atp_config) |
41727
ab3f6d76fb23
available_provers ~> supported_provers (for clarity)
blanchet
parents:
41725
diff
changeset
|
55 |
val supported_atps : theory -> string list |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
56 |
val is_atp_installed : theory -> string -> bool |
35867 | 57 |
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
|
58 |
val effective_term_order : Proof.context -> string -> term_order |
28592 | 59 |
end; |
60 |
||
36376 | 61 |
structure ATP_Systems : ATP_SYSTEMS = |
28592 | 62 |
struct |
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
63 |
|
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
|
64 |
open ATP_Problem |
39491
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39375
diff
changeset
|
65 |
open ATP_Proof |
46320 | 66 |
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
|
67 |
|
52073
ccb292952774
started adding agsyHOL as an experimental prover
blanchet
parents:
51998
diff
changeset
|
68 |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
69 |
(* ATP configuration *) |
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset
|
70 |
|
47962
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47955
diff
changeset
|
71 |
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
|
72 |
val default_max_new_mono_instances = 100 (* FUDGE *) |
47962
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47955
diff
changeset
|
73 |
|
51011 | 74 |
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
|
75 |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
76 |
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
|
77 |
{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
|
78 |
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
|
79 |
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
|
80 |
proof_delims : (string * string) list, |
53586
bd5fa6425993
prefixed types and some functions with "atp_" for disambiguation
blanchet
parents:
53515
diff
changeset
|
81 |
known_failures : (atp_failure * string) list, |
bd5fa6425993
prefixed types and some functions with "atp_" for disambiguation
blanchet
parents:
53515
diff
changeset
|
82 |
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
|
83 |
best_slices : Proof.context -> (real * (slice_spec * string)) list, |
47962
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47955
diff
changeset
|
84 |
best_max_mono_iters : int, |
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47955
diff
changeset
|
85 |
best_max_new_mono_instances : int} |
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
86 |
|
42723 | 87 |
(* "best_slices" must be found empirically, taking a wholistic approach since |
51011 | 88 |
the ATPs are run in parallel. Each slice has the format |
89 |
||
90 |
(time_frac, ((max_facts, fact_filter), format, type_enc, |
|
91 |
lam_trans, uncurried_aliases), extra) |
|
92 |
||
93 |
where |
|
94 |
||
95 |
time_frac = faction of the time available given to the slice (which should |
|
96 |
add up to 1.0) |
|
97 |
||
98 |
extra = extra information to the prover (e.g., SOS or no SOS). |
|
42723 | 99 |
|
100 |
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
|
101 |
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
|
102 |
slicing is disabled (e.g., by the minimizer). *) |
42710
84fcce345b5d
further improved type system setup based on Judgment Days
blanchet
parents:
42709
diff
changeset
|
103 |
|
51011 | 104 |
val mepoN = "mepo" |
105 |
val mashN = "mash" |
|
106 |
val meshN = "mesh" |
|
107 |
||
52073
ccb292952774
started adding agsyHOL as an experimental prover
blanchet
parents:
51998
diff
changeset
|
108 |
val tstp_proof_delims = |
ccb292952774
started adding agsyHOL as an experimental prover
blanchet
parents:
51998
diff
changeset
|
109 |
[("% SZS output start CNFRefutation", "% SZS output end CNFRefutation"), |
ccb292952774
started adding agsyHOL as an experimental prover
blanchet
parents:
51998
diff
changeset
|
110 |
("% SZS output start Refutation", "% SZS output end Refutation"), |
ccb292952774
started adding agsyHOL as an experimental prover
blanchet
parents:
51998
diff
changeset
|
111 |
("% SZS output start Proof", "% SZS output end Proof")] |
ccb292952774
started adding agsyHOL as an experimental prover
blanchet
parents:
51998
diff
changeset
|
112 |
|
38061
685d1f0f75b3
handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents:
38049
diff
changeset
|
113 |
val known_perl_failures = |
38094 | 114 |
[(CantConnect, "HTTP error"), |
115 |
(NoPerl, "env: perl"), |
|
38065 | 116 |
(NoLibwwwPerl, "Can't locate HTTP")] |
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
117 |
|
45203 | 118 |
fun known_szs_failures wrap = |
119 |
[(Unprovable, wrap "CounterSatisfiable"), |
|
120 |
(Unprovable, wrap "Satisfiable"), |
|
121 |
(GaveUp, wrap "GaveUp"), |
|
122 |
(GaveUp, wrap "Unknown"), |
|
123 |
(GaveUp, wrap "Incomplete"), |
|
124 |
(ProofMissing, wrap "Theorem"), |
|
125 |
(ProofMissing, wrap "Unsatisfiable"), |
|
126 |
(TimedOut, wrap "Timeout"), |
|
127 |
(Inappropriate, wrap "Inappropriate"), |
|
128 |
(OutOfResources, wrap "ResourceOut"), |
|
129 |
(OutOfResources, wrap "MemoryOut"), |
|
130 |
(Interrupted, wrap "Forced"), |
|
131 |
(Interrupted, wrap "User")] |
|
132 |
||
133 |
val known_szs_status_failures = known_szs_failures (prefix "SZS status ") |
|
134 |
val known_says_failures = known_szs_failures (prefix " says ") |
|
135 |
||
38023 | 136 |
structure Data = Theory_Data |
137 |
( |
|
47606
06dde48a1503
true delayed evaluation of "SPASS_VERSION" environment variable
blanchet
parents:
47506
diff
changeset
|
138 |
type T = ((unit -> atp_config) * stamp) Symtab.table |
38023 | 139 |
val empty = Symtab.empty |
140 |
val extend = I |
|
46407
30e9720cc0b9
optimization: slice caching in case two consecutive slices are nearly identical
blanchet
parents:
46402
diff
changeset
|
141 |
fun merge data : T = |
30e9720cc0b9
optimization: slice caching in case two consecutive slices are nearly identical
blanchet
parents:
46402
diff
changeset
|
142 |
Symtab.merge (eq_snd (op =)) data |
63692 | 143 |
handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name) |
38023 | 144 |
) |
38017
3ad3e3ca2451
move Sledgehammer-specific code out of "Sledgehammer_TPTP_Format"
blanchet
parents:
38015
diff
changeset
|
145 |
|
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
|
146 |
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
|
147 |
|
43473
fb2713b803e6
deal with ATP time slices in a more flexible/robust fashion
blanchet
parents:
43467
diff
changeset
|
148 |
val sosN = "sos" |
fb2713b803e6
deal with ATP time slices in a more flexible/robust fashion
blanchet
parents:
43467
diff
changeset
|
149 |
val no_sosN = "no_sos" |
fb2713b803e6
deal with ATP time slices in a more flexible/robust fashion
blanchet
parents:
43467
diff
changeset
|
150 |
|
69593 | 151 |
val force_sos = Attrib.setup_config_bool \<^binding>\<open>atp_force_sos\<close> (K false) |
44099 | 152 |
|
47032 | 153 |
val smartN = "smart" |
47073
c73f7b0c7ebc
generate weights and precedences for predicates as well
blanchet
parents:
47055
diff
changeset
|
154 |
(* val kboN = "kbo" *) |
47032 | 155 |
val lpoN = "lpo" |
47034
77da780ddd6b
implement term order attribute (for experiments)
blanchet
parents:
47033
diff
changeset
|
156 |
val xweightsN = "_weights" |
77da780ddd6b
implement term order attribute (for experiments)
blanchet
parents:
47033
diff
changeset
|
157 |
val xprecN = "_prec" |
77da780ddd6b
implement term order attribute (for experiments)
blanchet
parents:
47033
diff
changeset
|
158 |
val xsimpN = "_simp" (* SPASS-specific *) |
47032 | 159 |
|
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47034
diff
changeset
|
160 |
(* Possible values for "atp_term_order": |
47049 | 161 |
"smart", "(kbo|lpo)(_weights)?(_prec|_simp)?" *) |
47032 | 162 |
val term_order = |
69593 | 163 |
Attrib.setup_config_string \<^binding>\<open>atp_term_order\<close> (K smartN) |
47032 | 164 |
|
52073
ccb292952774
started adding agsyHOL as an experimental prover
blanchet
parents:
51998
diff
changeset
|
165 |
|
ccb292952774
started adding agsyHOL as an experimental prover
blanchet
parents:
51998
diff
changeset
|
166 |
(* agsyHOL *) |
ccb292952774
started adding agsyHOL as an experimental prover
blanchet
parents:
51998
diff
changeset
|
167 |
|
54197
994ebb795b75
use definitions for LEO-II as well -- this simplifies the code and matches some users' expectations
blanchet
parents:
53586
diff
changeset
|
168 |
val agsyhol_thf0 = THF (Monomorphic, THF_Without_Choice) |
52073
ccb292952774
started adding agsyHOL as an experimental prover
blanchet
parents:
51998
diff
changeset
|
169 |
|
ccb292952774
started adding agsyHOL as an experimental prover
blanchet
parents:
51998
diff
changeset
|
170 |
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
|
171 |
{exec = K (["AGSYHOL_HOME"], ["agsyHOL"]), |
52073
ccb292952774
started adding agsyHOL as an experimental prover
blanchet
parents:
51998
diff
changeset
|
172 |
arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => |
68563 | 173 |
"--proof --time-out " ^ string_of_int (to_secs 1 timeout) ^ " " ^ file_name, |
52073
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 | 190 |
arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => |
68563 | 191 |
"--format tptp --prover 'Alt-Ergo,0.95.2,' --timelimit " ^ string_of_int (to_secs 1 timeout) ^ |
192 |
" " ^ 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 | 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 | 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 |
|
43473
fb2713b803e6
deal with ATP time slices in a more flexible/robust fashion
blanchet
parents:
43467
diff
changeset
|
210 |
val e_smartN = "smart" |
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset
|
211 |
val e_autoN = "auto" |
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset
|
212 |
val e_fun_weightN = "fun_weight" |
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset
|
213 |
val e_sym_offset_weightN = "sym_offset_weight" |
41725
7cca2de89296
added support for bleeding-edge E weighting function "SymOffsetsWeight"
blanchet
parents:
41335
diff
changeset
|
214 |
|
47032 | 215 |
val e_selection_heuristic = |
69593 | 216 |
Attrib.setup_config_string \<^binding>\<open>atp_e_selection_heuristic\<close> (K e_smartN) |
41770 | 217 |
(* FUDGE *) |
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset
|
218 |
val e_default_fun_weight = |
69593 | 219 |
Attrib.setup_config_real \<^binding>\<open>atp_e_default_fun_weight\<close> (K 20.0) |
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset
|
220 |
val e_fun_weight_base = |
69593 | 221 |
Attrib.setup_config_real \<^binding>\<open>atp_e_fun_weight_base\<close> (K 0.0) |
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset
|
222 |
val e_fun_weight_span = |
69593 | 223 |
Attrib.setup_config_real \<^binding>\<open>atp_e_fun_weight_span\<close> (K 40.0) |
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset
|
224 |
val e_default_sym_offs_weight = |
69593 | 225 |
Attrib.setup_config_real \<^binding>\<open>atp_e_default_sym_offs_weight\<close> (K 1.0) |
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset
|
226 |
val e_sym_offs_weight_base = |
69593 | 227 |
Attrib.setup_config_real \<^binding>\<open>atp_e_sym_offs_weight_base\<close> (K ~20.0) |
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset
|
228 |
val e_sym_offs_weight_span = |
69593 | 229 |
Attrib.setup_config_real \<^binding>\<open>atp_e_sym_offs_weight_span\<close> (K 60.0) |
41725
7cca2de89296
added support for bleeding-edge E weighting function "SymOffsetsWeight"
blanchet
parents:
41335
diff
changeset
|
230 |
|
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47034
diff
changeset
|
231 |
fun e_selection_heuristic_case heuristic fw sow = |
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47034
diff
changeset
|
232 |
if heuristic = e_fun_weightN then fw |
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47034
diff
changeset
|
233 |
else if heuristic = e_sym_offset_weightN then sow |
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47034
diff
changeset
|
234 |
else raise Fail ("unexpected " ^ quote heuristic) |
41725
7cca2de89296
added support for bleeding-edge E weighting function "SymOffsetsWeight"
blanchet
parents:
41335
diff
changeset
|
235 |
|
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47034
diff
changeset
|
236 |
fun scaled_e_selection_weight ctxt heuristic w = |
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47034
diff
changeset
|
237 |
w * Config.get ctxt (e_selection_heuristic_case heuristic |
47029 | 238 |
e_fun_weight_span e_sym_offs_weight_span) |
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47034
diff
changeset
|
239 |
+ Config.get ctxt (e_selection_heuristic_case heuristic |
47029 | 240 |
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
|
241 |
|> 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
|
242 |
|
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47034
diff
changeset
|
243 |
fun e_selection_weight_arguments ctxt heuristic sel_weights = |
51631 | 244 |
if heuristic = e_fun_weightN orelse heuristic = e_sym_offset_weightN then |
43622 | 245 |
(* supplied by Stephan Schulz *) |
41314
2dc1dfc1bc69
use the options provided by Stephan Schulz -- much better
blanchet
parents:
41313
diff
changeset
|
246 |
"--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
|
247 |
\--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
|
248 |
\--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
|
249 |
\--delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*" ^ |
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47034
diff
changeset
|
250 |
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
|
251 |
"(SimulateSOS," ^ |
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47034
diff
changeset
|
252 |
(e_selection_heuristic_case heuristic |
47029 | 253 |
e_default_fun_weight e_default_sym_offs_weight |
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset
|
254 |
|> 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
|
255 |
",20,1.5,1.5,1" ^ |
47030 | 256 |
(sel_weights () |
47029 | 257 |
|> map (fn (s, w) => "," ^ s ^ ":" ^ |
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47034
diff
changeset
|
258 |
scaled_e_selection_weight ctxt heuristic w) |
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset
|
259 |
|> implode) ^ |
41314
2dc1dfc1bc69
use the options provided by Stephan Schulz -- much better
blanchet
parents:
41313
diff
changeset
|
260 |
"),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
|
261 |
\1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*\ |
57672 | 262 |
\FIFOWeight(PreferProcessed))' " |
51631 | 263 |
else |
57672 | 264 |
"-xAuto " |
41313
a96ac4d180b7
optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents:
41269
diff
changeset
|
265 |
|
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47034
diff
changeset
|
266 |
val e_ord_weights = |
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47034
diff
changeset
|
267 |
map (fn (s, w) => s ^ ":" ^ string_of_int w) #> space_implode "," |
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47034
diff
changeset
|
268 |
fun e_ord_precedence [_] = "" |
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47034
diff
changeset
|
269 |
| e_ord_precedence info = info |> map fst |> space_implode "<" |
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47034
diff
changeset
|
270 |
|
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
|
271 |
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
|
272 |
| e_term_order_info_arguments gen_weights gen_prec ord_info = |
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47034
diff
changeset
|
273 |
let val ord_info = ord_info () in |
57672 | 274 |
(if gen_weights then "--order-weights='" ^ e_ord_weights ord_info ^ "' " else "") ^ |
275 |
(if gen_prec then "--precedence='" ^ e_ord_precedence ord_info ^ "' " else "") |
|
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47034
diff
changeset
|
276 |
end |
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47034
diff
changeset
|
277 |
|
66363 | 278 |
val e_tff0 = TFF Monomorphic |
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 = |
66363 | 281 |
{exec = fn _ => (["E_HOME"], ["eprover"]), |
282 |
arguments = fn ctxt => fn _ => fn heuristic => fn timeout => fn file_name => |
|
57008 | 283 |
fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) => |
66363 | 284 |
"--auto-schedule --tstp-in --tstp-out --silent " ^ |
57672 | 285 |
e_selection_weight_arguments ctxt heuristic sel_weights ^ |
286 |
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
|
287 |
"--term-ordering=" ^ (if is_lpo then "LPO4" else "KBO6") ^ " " ^ |
48651 | 288 |
"--cpu-limit=" ^ string_of_int (to_secs 2 timeout) ^ |
66363 | 289 |
" --proof-object=1 " ^ |
290 |
file_name, |
|
52073
ccb292952774
started adding agsyHOL as an experimental prover
blanchet
parents:
51998
diff
changeset
|
291 |
proof_delims = |
ccb292952774
started adding agsyHOL as an experimental prover
blanchet
parents:
51998
diff
changeset
|
292 |
[("# SZS output start CNFRefutation", "# SZS output end CNFRefutation")] @ |
ccb292952774
started adding agsyHOL as an experimental prover
blanchet
parents:
51998
diff
changeset
|
293 |
tstp_proof_delims, |
36265
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset
|
294 |
known_failures = |
45203 | 295 |
[(TimedOut, "Failure: Resource limit exceeded (time)"), |
47972 | 296 |
(TimedOut, "time limit exceeded")] @ |
297 |
known_szs_status_failures, |
|
47976 | 298 |
prem_role = Conjecture, |
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset
|
299 |
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
|
300 |
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
|
301 |
(* FUDGE *) |
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47034
diff
changeset
|
302 |
if heuristic = e_smartN then |
66363 | 303 |
[(0.15, (((128, meshN), e_tff0, "mono_native", combsN, false), e_fun_weightN)), |
304 |
(0.15, (((128, mashN), e_tff0, "mono_native", combsN, false), e_sym_offset_weightN)), |
|
305 |
(0.15, (((91, mepoN), e_tff0, "mono_native", combsN, false), e_autoN)), |
|
306 |
(0.15, (((1000, meshN), e_tff0, "poly_guards??", combsN, false), e_sym_offset_weightN)), |
|
307 |
(0.15, (((256, mepoN), e_tff0, "mono_native", liftingN, false), e_fun_weightN)), |
|
308 |
(0.25, (((64, mashN), e_tff0, "mono_native", combsN, false), e_fun_weightN))] |
|
43473
fb2713b803e6
deal with ATP time slices in a more flexible/robust fashion
blanchet
parents:
43467
diff
changeset
|
309 |
else |
66363 | 310 |
[(1.0, (((500, ""), e_tff0, "mono_native", combsN, false), heuristic))] |
47962
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47955
diff
changeset
|
311 |
end, |
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47955
diff
changeset
|
312 |
best_max_mono_iters = default_max_mono_iters, |
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47955
diff
changeset
|
313 |
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
|
314 |
|
47646 | 315 |
val e = (eN, fn () => e_config) |
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
316 |
|
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
317 |
|
48651 | 318 |
(* E-MaLeS *) |
319 |
||
320 |
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
|
321 |
{exec = K (["E_MALES_HOME"], ["emales.py"]), |
50927 | 322 |
arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => |
68563 | 323 |
"-t " ^ string_of_int (to_secs 1 timeout) ^ " -p " ^ file_name, |
48651 | 324 |
proof_delims = tstp_proof_delims, |
325 |
known_failures = #known_failures e_config, |
|
326 |
prem_role = Conjecture, |
|
327 |
best_slices = |
|
328 |
(* FUDGE *) |
|
51018 | 329 |
K [(0.25, (((500, meshN), FOF, "mono_guards??", combs_or_liftingN, false), "")), |
330 |
(0.25, (((150, meshN), FOF, "poly_tags??", combs_or_liftingN, false), "")), |
|
331 |
(0.25, (((50, meshN), FOF, "mono_tags??", combs_or_liftingN, false), "")), |
|
332 |
(0.25, (((1000, meshN), FOF, "poly_guards??", combsN, false), ""))], |
|
48651 | 333 |
best_max_mono_iters = default_max_mono_iters, |
334 |
best_max_new_mono_instances = default_max_new_mono_instances} |
|
335 |
||
336 |
val e_males = (e_malesN, fn () => e_males_config) |
|
337 |
||
338 |
||
50927 | 339 |
(* E-Par *) |
340 |
||
341 |
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
|
342 |
{exec = K (["E_HOME"], ["runepar.pl"]), |
50927 | 343 |
arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => |
68563 | 344 |
string_of_int (to_secs 1 timeout) ^ " 1 " (* SInE *) ^ file_name ^ " 2" (* proofs *), |
50927 | 345 |
proof_delims = tstp_proof_delims, |
346 |
known_failures = #known_failures e_config, |
|
347 |
prem_role = Conjecture, |
|
348 |
best_slices = #best_slices e_males_config, |
|
349 |
best_max_mono_iters = default_max_mono_iters, |
|
350 |
best_max_new_mono_instances = default_max_new_mono_instances} |
|
351 |
||
352 |
val e_par = (e_parN, fn () => e_par_config) |
|
353 |
||
354 |
||
68250
c45067867860
added lambda-free HO output for Ehoh (higher-order E prototype)
blanchet
parents:
68224
diff
changeset
|
355 |
(* Ehoh *) |
c45067867860
added lambda-free HO output for Ehoh (higher-order E prototype)
blanchet
parents:
68224
diff
changeset
|
356 |
|
c45067867860
added lambda-free HO output for Ehoh (higher-order E prototype)
blanchet
parents:
68224
diff
changeset
|
357 |
val ehoh_thf0 = THF (Monomorphic, THF_Lambda_Free) |
c45067867860
added lambda-free HO output for Ehoh (higher-order E prototype)
blanchet
parents:
68224
diff
changeset
|
358 |
|
c45067867860
added lambda-free HO output for Ehoh (higher-order E prototype)
blanchet
parents:
68224
diff
changeset
|
359 |
val ehoh_config : atp_config = |
c45067867860
added lambda-free HO output for Ehoh (higher-order E prototype)
blanchet
parents:
68224
diff
changeset
|
360 |
{exec = fn _ => (["E_HOME"], ["eprover"]), |
c45067867860
added lambda-free HO output for Ehoh (higher-order E prototype)
blanchet
parents:
68224
diff
changeset
|
361 |
arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => |
68563 | 362 |
"--auto-schedule --tstp-in --tstp-out --silent --cpu-limit=" ^ |
363 |
string_of_int (to_secs 2 timeout) ^ " --proof-object=1 " ^ file_name, |
|
68250
c45067867860
added lambda-free HO output for Ehoh (higher-order E prototype)
blanchet
parents:
68224
diff
changeset
|
364 |
proof_delims = |
c45067867860
added lambda-free HO output for Ehoh (higher-order E prototype)
blanchet
parents:
68224
diff
changeset
|
365 |
[("# SZS output start CNFRefutation", "# SZS output end CNFRefutation")] @ |
c45067867860
added lambda-free HO output for Ehoh (higher-order E prototype)
blanchet
parents:
68224
diff
changeset
|
366 |
tstp_proof_delims, |
c45067867860
added lambda-free HO output for Ehoh (higher-order E prototype)
blanchet
parents:
68224
diff
changeset
|
367 |
known_failures = |
c45067867860
added lambda-free HO output for Ehoh (higher-order E prototype)
blanchet
parents:
68224
diff
changeset
|
368 |
[(TimedOut, "Failure: Resource limit exceeded (time)"), |
c45067867860
added lambda-free HO output for Ehoh (higher-order E prototype)
blanchet
parents:
68224
diff
changeset
|
369 |
(TimedOut, "time limit exceeded")] @ |
c45067867860
added lambda-free HO output for Ehoh (higher-order E prototype)
blanchet
parents:
68224
diff
changeset
|
370 |
known_szs_status_failures, |
68328
0d751da653d9
more conservative output, avoiding nonstandard feature of E
blanchet
parents:
68250
diff
changeset
|
371 |
prem_role = Hypothesis, |
68250
c45067867860
added lambda-free HO output for Ehoh (higher-order E prototype)
blanchet
parents:
68224
diff
changeset
|
372 |
best_slices = |
c45067867860
added lambda-free HO output for Ehoh (higher-order E prototype)
blanchet
parents:
68224
diff
changeset
|
373 |
(* FUDGE *) |
c45067867860
added lambda-free HO output for Ehoh (higher-order E prototype)
blanchet
parents:
68224
diff
changeset
|
374 |
K [(1.0, (((500, ""), ehoh_thf0, "mono_native_higher", liftingN, false), ""))], |
c45067867860
added lambda-free HO output for Ehoh (higher-order E prototype)
blanchet
parents:
68224
diff
changeset
|
375 |
best_max_mono_iters = default_max_mono_iters, |
c45067867860
added lambda-free HO output for Ehoh (higher-order E prototype)
blanchet
parents:
68224
diff
changeset
|
376 |
best_max_new_mono_instances = default_max_new_mono_instances} |
c45067867860
added lambda-free HO output for Ehoh (higher-order E prototype)
blanchet
parents:
68224
diff
changeset
|
377 |
|
c45067867860
added lambda-free HO output for Ehoh (higher-order E prototype)
blanchet
parents:
68224
diff
changeset
|
378 |
val ehoh = (ehohN, fn () => ehoh_config) |
c45067867860
added lambda-free HO output for Ehoh (higher-order E prototype)
blanchet
parents:
68224
diff
changeset
|
379 |
|
c45067867860
added lambda-free HO output for Ehoh (higher-order E prototype)
blanchet
parents:
68224
diff
changeset
|
380 |
|
48700 | 381 |
(* iProver *) |
382 |
||
383 |
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
|
384 |
{exec = K (["IPROVER_HOME"], ["iprover"]), |
50927 | 385 |
arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => |
68563 | 386 |
"--clausifier \"$IPROVER_HOME\"/vclausify_rel --time_out_real " ^ |
387 |
string_of_real (Time.toReal timeout) ^ " " ^ file_name, |
|
48700 | 388 |
proof_delims = tstp_proof_delims, |
389 |
known_failures = |
|
390 |
[(ProofIncomplete, "% SZS output start CNFRefutation")] @ |
|
391 |
known_szs_status_failures, |
|
392 |
prem_role = Hypothesis, |
|
393 |
best_slices = |
|
394 |
(* FUDGE *) |
|
51011 | 395 |
K [(1.0, (((150, ""), FOF, "mono_guards??", liftingN, false), ""))], |
48700 | 396 |
best_max_mono_iters = default_max_mono_iters, |
397 |
best_max_new_mono_instances = default_max_new_mono_instances} |
|
398 |
||
399 |
val iprover = (iproverN, fn () => iprover_config) |
|
400 |
||
401 |
||
402 |
(* iProver-Eq *) |
|
403 |
||
404 |
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
|
405 |
{exec = K (["IPROVER_EQ_HOME"], ["iprover-eq"]), |
48700 | 406 |
arguments = #arguments iprover_config, |
407 |
proof_delims = #proof_delims iprover_config, |
|
408 |
known_failures = #known_failures iprover_config, |
|
409 |
prem_role = #prem_role iprover_config, |
|
410 |
best_slices = #best_slices iprover_config, |
|
411 |
best_max_mono_iters = #best_max_mono_iters iprover_config, |
|
412 |
best_max_new_mono_instances = #best_max_new_mono_instances iprover_config} |
|
413 |
||
414 |
val iprover_eq = (iprover_eqN, fn () => iprover_eq_config) |
|
415 |
||
416 |
||
44099 | 417 |
(* LEO-II *) |
418 |
||
54197
994ebb795b75
use definitions for LEO-II as well -- this simplifies the code and matches some users' expectations
blanchet
parents:
53586
diff
changeset
|
419 |
val leo2_thf0 = THF (Monomorphic, THF_Without_Choice) |
44754 | 420 |
|
44099 | 421 |
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
|
422 |
{exec = K (["LEO2_HOME"], ["leo.opt", "leo"]), |
57759 | 423 |
arguments = fn _ => fn full_proofs => fn _ => fn timeout => fn file_name => fn _ => |
424 |
"--foatp e --atp e=\"$E_HOME\"/eprover \ |
|
425 |
\--atp epclextract=\"$E_HOME\"/epclextract \ |
|
426 |
\--proofoutput 1 --timeout " ^ string_of_int (to_secs 1 timeout) ^ " " ^ |
|
427 |
(if full_proofs then "--notReplLeibnizEQ --notReplAndrewsEQ --notUseExtCnfCmbd " else "") ^ |
|
428 |
file_name, |
|
44099 | 429 |
proof_delims = tstp_proof_delims, |
45207 | 430 |
known_failures = |
47974
08d2dcc2dab9
improved LEO-II definition handling -- still hoping for a fix directly in LEO-II
blanchet
parents:
47972
diff
changeset
|
431 |
[(TimedOut, "CPU time limit exceeded, terminating"), |
47972 | 432 |
(GaveUp, "No.of.Axioms")] @ |
433 |
known_szs_status_failures, |
|
47976 | 434 |
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
|
435 |
best_slices = |
44099 | 436 |
(* FUDGE *) |
51011 | 437 |
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
|
438 |
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
|
439 |
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
|
440 |
|
47646 | 441 |
val leo2 = (leo2N, fn () => leo2_config) |
44099 | 442 |
|
443 |
||
67021
41f1f8c4259b
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
blanchet
parents:
66544
diff
changeset
|
444 |
(* Leo-III *) |
41f1f8c4259b
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
blanchet
parents:
66544
diff
changeset
|
445 |
|
41f1f8c4259b
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
blanchet
parents:
66544
diff
changeset
|
446 |
(* include choice? Disabled now since its disabled for satallax as well. *) |
41f1f8c4259b
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
blanchet
parents:
66544
diff
changeset
|
447 |
val leo3_thf1 = THF (Polymorphic, THF_Without_Choice) |
41f1f8c4259b
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
blanchet
parents:
66544
diff
changeset
|
448 |
|
41f1f8c4259b
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
blanchet
parents:
66544
diff
changeset
|
449 |
val leo3_config : atp_config = |
41f1f8c4259b
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
blanchet
parents:
66544
diff
changeset
|
450 |
{exec = K (["LEO3_HOME"], ["leo3"]), |
41f1f8c4259b
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
blanchet
parents:
66544
diff
changeset
|
451 |
arguments = fn _ => fn full_proofs => fn _ => fn timeout => fn file_name => fn _ => |
41f1f8c4259b
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
blanchet
parents:
66544
diff
changeset
|
452 |
file_name ^ " " ^ "--atp cvc=$CVC4_SOLVER --atp e=\"$E_HOME\"/eprover \ |
41f1f8c4259b
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
blanchet
parents:
66544
diff
changeset
|
453 |
\-p -t " ^ string_of_int (to_secs 1 timeout) ^ " " ^ |
41f1f8c4259b
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
blanchet
parents:
66544
diff
changeset
|
454 |
(if full_proofs then "--nleq --naeq " else ""), |
41f1f8c4259b
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
blanchet
parents:
66544
diff
changeset
|
455 |
proof_delims = tstp_proof_delims, |
41f1f8c4259b
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
blanchet
parents:
66544
diff
changeset
|
456 |
known_failures = known_szs_status_failures, |
41f1f8c4259b
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
blanchet
parents:
66544
diff
changeset
|
457 |
prem_role = Hypothesis, |
41f1f8c4259b
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
blanchet
parents:
66544
diff
changeset
|
458 |
best_slices = |
41f1f8c4259b
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
blanchet
parents:
66544
diff
changeset
|
459 |
(* FUDGE *) |
41f1f8c4259b
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
blanchet
parents:
66544
diff
changeset
|
460 |
K [(1.0, (((150, ""), leo3_thf1, "poly_native_higher", keep_lamsN, false), ""))], |
41f1f8c4259b
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
blanchet
parents:
66544
diff
changeset
|
461 |
best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *), |
41f1f8c4259b
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
blanchet
parents:
66544
diff
changeset
|
462 |
best_max_new_mono_instances = default_max_new_mono_instances} |
41f1f8c4259b
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
blanchet
parents:
66544
diff
changeset
|
463 |
|
41f1f8c4259b
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
blanchet
parents:
66544
diff
changeset
|
464 |
val leo3 = (leo3N, fn () => leo3_config) |
41f1f8c4259b
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
blanchet
parents:
66544
diff
changeset
|
465 |
|
41f1f8c4259b
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
blanchet
parents:
66544
diff
changeset
|
466 |
|
44099 | 467 |
(* Satallax *) |
468 |
||
52097 | 469 |
(* 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
|
470 |
val satallax_thf0 = THF (Monomorphic, THF_Without_Choice) |
44754 | 471 |
|
44099 | 472 |
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
|
473 |
{exec = K (["SATALLAX_HOME"], ["satallax.opt", "satallax"]), |
50927 | 474 |
arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => |
68563 | 475 |
"-p tstp -t " ^ string_of_int (to_secs 1 timeout) ^ " " ^ file_name, |
45162 | 476 |
proof_delims = |
57707
0242e9578828
imported patch satallax_proof_support_Sledgehammer
fleury
parents:
57672
diff
changeset
|
477 |
[("% SZS output start Proof", "% SZS output end Proof")], |
45203 | 478 |
known_failures = known_szs_status_failures, |
47981 | 479 |
prem_role = Hypothesis, |
44416
cabd06b69c18
added formats to the slice and use TFF for remote Vampire
blanchet
parents:
44391
diff
changeset
|
480 |
best_slices = |
44754 | 481 |
(* FUDGE *) |
67021
41f1f8c4259b
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
blanchet
parents:
66544
diff
changeset
|
482 |
K [(1.0, (((150, ""), satallax_thf0, "mono_native_higher", keep_lamsN, false), ""))], |
47962
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47955
diff
changeset
|
483 |
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
|
484 |
best_max_new_mono_instances = default_max_new_mono_instances} |
44099 | 485 |
|
47646 | 486 |
val satallax = (satallaxN, fn () => satallax_config) |
44099 | 487 |
|
488 |
||
489 |
(* 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
|
490 |
|
48005
eeede26f2721
killed SPASS 3.5/3.7 FLOTTER hack -- requires users to upgrade to SPASS 3.8
blanchet
parents:
48004
diff
changeset
|
491 |
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
|
492 |
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
|
493 |
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
|
494 |
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
|
495 |
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
|
496 |
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
|
497 |
|
50950 | 498 |
val spass_extra_options = |
69593 | 499 |
Attrib.setup_config_string \<^binding>\<open>atp_spass_extra_options\<close> (K "") |
50950 | 500 |
|
48005
eeede26f2721
killed SPASS 3.5/3.7 FLOTTER hack -- requires users to upgrade to SPASS 3.8
blanchet
parents:
48004
diff
changeset
|
501 |
val spass_config : atp_config = |
66363 | 502 |
{exec = K (["SPASS_HOME"], ["SPASS"]), |
68563 | 503 |
arguments = fn _ => fn full_proofs => fn extra_options => fn timeout => fn file_name => fn _ => |
504 |
"-Isabelle=1 " ^ (if full_proofs then "-CNFRenaming=0 -Splits=0 " else "") ^ |
|
505 |
"-TimeLimit=" ^ string_of_int (to_secs 1 timeout) ^ " " ^ file_name |
|
506 |
|> extra_options <> "" ? prefix (extra_options ^ " "), |
|
36369
d2cd0d04b8e6
handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents:
36289
diff
changeset
|
507 |
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
|
508 |
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
|
509 |
[(GaveUp, "SPASS beiseite: Completion found"), |
36370
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
510 |
(TimedOut, "SPASS beiseite: Ran out of time"), |
36965 | 511 |
(OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"), |
37413 | 512 |
(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
|
513 |
(MalformedInput, "Free Variable"), |
44391 | 514 |
(Unprovable, "No formulae and clauses found in input file"), |
47972 | 515 |
(InternalError, "Please report this error")] @ |
516 |
known_perl_failures, |
|
47976 | 517 |
prem_role = Conjecture, |
50950 | 518 |
best_slices = fn ctxt => |
42723 | 519 |
(* FUDGE *) |
51016 | 520 |
[(0.1667, (((150, meshN), DFG Monomorphic, "mono_native", combsN, true), "")), |
521 |
(0.1667, (((500, meshN), DFG Monomorphic, "mono_native", liftingN, true), spass_H2SOS)), |
|
522 |
(0.1666, (((50, meshN), DFG Monomorphic, "mono_native", liftingN, true), spass_H2LR0LT0)), |
|
523 |
(0.1000, (((250, meshN), DFG Monomorphic, "mono_native", combsN, true), spass_H2NuVS0)), |
|
524 |
(0.1000, (((1000, mepoN), DFG Monomorphic, "mono_native", liftingN, true), spass_H1SOS)), |
|
525 |
(0.1000, (((150, meshN), DFG Monomorphic, "poly_guards??", liftingN, false), spass_H2NuVS0Red2)), |
|
526 |
(0.1000, (((300, meshN), DFG Monomorphic, "mono_native", combsN, true), spass_H2SOS)), |
|
527 |
(0.1000, (((100, meshN), DFG Monomorphic, "mono_native", combs_and_liftingN, true), spass_H2))] |
|
50950 | 528 |
|> (case Config.get ctxt spass_extra_options of |
529 |
"" => I |
|
530 |
| opts => map (apsnd (apsnd (K opts)))), |
|
47962
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47955
diff
changeset
|
531 |
best_max_mono_iters = default_max_mono_iters, |
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47955
diff
changeset
|
532 |
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
|
533 |
|
48005
eeede26f2721
killed SPASS 3.5/3.7 FLOTTER hack -- requires users to upgrade to SPASS 3.8
blanchet
parents:
48004
diff
changeset
|
534 |
val spass = (spassN, fn () => spass_config) |
38454
9043eefe8d71
detect old Vampire and give a nicer error message
blanchet
parents:
38433
diff
changeset
|
535 |
|
52073
ccb292952774
started adding agsyHOL as an experimental prover
blanchet
parents:
51998
diff
changeset
|
536 |
|
37509
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
37506
diff
changeset
|
537 |
(* Vampire *) |
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
37506
diff
changeset
|
538 |
|
68563 | 539 |
fun is_vampire_noncommercial_license_accepted () = |
540 |
let |
|
69593 | 541 |
val flag = Options.default_string \<^system_option>\<open>vampire_noncommercial\<close> |
68563 | 542 |
|> String.map Char.toLower |
543 |
in |
|
544 |
if flag = "yes" then |
|
545 |
SOME true |
|
546 |
else if flag = "no" then |
|
547 |
SOME false |
|
548 |
else |
|
549 |
NONE |
|
550 |
end |
|
551 |
||
552 |
fun check_vampire_noncommercial () = |
|
553 |
(case is_vampire_noncommercial_license_accepted () of |
|
554 |
SOME true => () |
|
555 |
| SOME false => |
|
556 |
error (Pretty.string_of (Pretty.para |
|
557 |
"The Vampire prover may be used only for noncommercial applications")) |
|
558 |
| NONE => |
|
559 |
error (Pretty.string_of (Pretty.para |
|
560 |
"The Vampire prover is not activated; to activate it, set the Isabelle system option \ |
|
561 |
\\"vampire_noncommercial\" to \"yes\" (e.g. via the Isabelle/jEdit menu Plugin Options \ |
|
562 |
\/ Isabelle / General)"))) |
|
44420 | 563 |
|
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
|
564 |
val vampire_tff0 = TFF Monomorphic |
44589
0a1dfc6365e9
first step towards polymorphic TFF + changed defaults for Vampire
blanchet
parents:
44586
diff
changeset
|
565 |
|
68563 | 566 |
val vampire_basic_options = "--proof tptp --output_axiom_names on $VAMPIRE_EXTRA_OPTIONS" |
58084 | 567 |
|
68224 | 568 |
(* cf. p. 20 of https://www.complang.tuwien.ac.at/lkovacs/Cade23_Tutorial_Slides/Session2_Slides.pdf *) |
58084 | 569 |
val vampire_full_proof_options = |
570 |
" --forced_options splitting=off:equality_proxy=off:general_splitting=off:inequality_splitting=0:\ |
|
571 |
\naming=0" |
|
572 |
||
573 |
val remote_vampire_full_proof_command = |
|
574 |
"vampire " ^ vampire_basic_options ^ " " ^ vampire_full_proof_options ^ " -t %d %s" |
|
575 |
||
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
576 |
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
|
577 |
{exec = K (["VAMPIRE_HOME"], ["vampire"]), |
58084 | 578 |
arguments = fn _ => fn full_proofs => fn sos => fn timeout => fn file_name => fn _ => |
68563 | 579 |
(check_vampire_noncommercial (); |
580 |
vampire_basic_options ^ (if full_proofs then " " ^ vampire_full_proof_options else "") ^ |
|
581 |
" -t " ^ string_of_int (to_secs 1 timeout) ^ " --input_file " ^ file_name |
|
582 |
|> 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
|
583 |
proof_delims = |
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
37506
diff
changeset
|
584 |
[("=========== Refutation ==========", |
52073
ccb292952774
started adding agsyHOL as an experimental prover
blanchet
parents:
51998
diff
changeset
|
585 |
"======= End of refutation =======")] @ |
ccb292952774
started adding agsyHOL as an experimental prover
blanchet
parents:
51998
diff
changeset
|
586 |
tstp_proof_delims, |
37509
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
37506
diff
changeset
|
587 |
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
|
588 |
[(GaveUp, "UNPROVABLE"), |
59284a13abc4
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents:
42999
diff
changeset
|
589 |
(GaveUp, "CANNOT PROVE"), |
37509
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
37506
diff
changeset
|
590 |
(Unprovable, "Satisfiability detected"), |
38647
5500241da479
play with fudge factor + parse one more Vampire error
blanchet
parents:
38646
diff
changeset
|
591 |
(Unprovable, "Termination reason: Satisfiable"), |
47972 | 592 |
(Interrupted, "Aborted by signal SIGINT")] @ |
593 |
known_szs_status_failures, |
|
63116 | 594 |
prem_role = Hypothesis, |
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
|
595 |
best_slices = fn ctxt => |
42723 | 596 |
(* FUDGE *) |
68563 | 597 |
[(0.333, (((500, meshN), vampire_tff0, "mono_native", combs_or_liftingN, false), sosN)), |
598 |
(0.333, (((150, meshN), vampire_tff0, "poly_tags??", combs_or_liftingN, false), sosN)), |
|
599 |
(0.334, (((50, meshN), vampire_tff0, "mono_native", combs_or_liftingN, false), no_sosN))] |
|
58084 | 600 |
|> 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
|
601 |
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
|
602 |
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
|
603 |
|
47646 | 604 |
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
|
605 |
|
68563 | 606 |
|
48803
ffa31bf5c662
tone down "z3_tptp", now that Z3 (starting with 4.1) no longer supports TPTP TFF0
blanchet
parents:
48801
diff
changeset
|
607 |
(* Z3 with TPTP syntax (half experimental, half legacy) *) |
41740
4b09f8b9e012
added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents:
41738
diff
changeset
|
608 |
|
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
|
609 |
val z3_tff0 = TFF Monomorphic |
44589
0a1dfc6365e9
first step towards polymorphic TFF + changed defaults for Vampire
blanchet
parents:
44586
diff
changeset
|
610 |
|
44423
f74707e12d30
exploit TFF format in Z3 used as ATP, and renamed it "z3_tptp"
blanchet
parents:
44422
diff
changeset
|
611 |
val z3_tptp_config : atp_config = |
56378 | 612 |
{exec = K (["Z3_TPTP_HOME"], ["z3_tptp"]), |
50927 | 613 |
arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => |
57261 | 614 |
"-proof -t:" ^ string_of_int (to_secs 1 timeout) ^ " -file:" ^ file_name, |
56397 | 615 |
proof_delims = [("SZS status Theorem", "")], |
45203 | 616 |
known_failures = known_szs_status_failures, |
47976 | 617 |
prem_role = Hypothesis, |
42723 | 618 |
best_slices = |
44423
f74707e12d30
exploit TFF format in Z3 used as ATP, and renamed it "z3_tptp"
blanchet
parents:
44422
diff
changeset
|
619 |
(* FUDGE *) |
51011 | 620 |
K [(0.5, (((250, meshN), z3_tff0, "mono_native", combsN, false), "")), |
621 |
(0.25, (((125, mepoN), z3_tff0, "mono_native", combsN, false), "")), |
|
622 |
(0.125, (((62, mashN), z3_tff0, "mono_native", combsN, false), "")), |
|
623 |
(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
|
624 |
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
|
625 |
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
|
626 |
|
47646 | 627 |
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
|
628 |
|
44590 | 629 |
|
57154 | 630 |
(* Zipperposition*) |
631 |
||
632 |
val zipperposition_config : atp_config = |
|
633 |
{exec = K (["ZIPPERPOSITION_HOME"], ["zipperposition"]), |
|
634 |
arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => |
|
68563 | 635 |
"-print none -proof tstp -print-types -timeout " ^ string_of_int (to_secs 1 timeout) ^ " " ^ |
636 |
file_name, |
|
57154 | 637 |
proof_delims = tstp_proof_delims, |
638 |
known_failures = known_szs_status_failures, |
|
639 |
prem_role = Hypothesis, |
|
640 |
best_slices = fn _ => |
|
641 |
(* FUDGE *) |
|
57547
677b07d777c3
don't generate TPTP THF 'Definition's, because they complicate reconstruction for AgsyHOL and Satallax
blanchet
parents:
57293
diff
changeset
|
642 |
[(1.0, (((100, ""), TFF Polymorphic, "poly_native", liftingN, false), ""))], |
57154 | 643 |
best_max_mono_iters = default_max_mono_iters, |
644 |
best_max_new_mono_instances = default_max_new_mono_instances} |
|
645 |
||
646 |
val zipperposition = (zipperpositionN, fn () => zipperposition_config) |
|
647 |
||
648 |
||
48131 | 649 |
(* Not really a prover: Experimental Polymorphic THF and DFG output *) |
44590 | 650 |
|
51919
097b191d1f0d
use right default for "uncurried_aliases" with polymorphic SPASS
blanchet
parents:
51873
diff
changeset
|
651 |
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
|
652 |
{exec = K (["ISABELLE_ATP"], ["scripts/dummy_atp"]), |
50927 | 653 |
arguments = K (K (K (K (K (K ""))))), |
44590 | 654 |
proof_delims = [], |
45203 | 655 |
known_failures = known_szs_status_failures, |
51467 | 656 |
prem_role = prem_role, |
45521 | 657 |
best_slices = |
51011 | 658 |
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
|
659 |
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
|
660 |
else combsN, uncurried_aliases), ""))], |
47962
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47955
diff
changeset
|
661 |
best_max_mono_iters = default_max_mono_iters, |
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47955
diff
changeset
|
662 |
best_max_new_mono_instances = default_max_new_mono_instances} |
44590 | 663 |
|
54197
994ebb795b75
use definitions for LEO-II as well -- this simplifies the code and matches some users' expectations
blanchet
parents:
53586
diff
changeset
|
664 |
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
|
665 |
|
54788
a898e15b522a
primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents:
54197
diff
changeset
|
666 |
val dummy_thf_config = dummy_config Hypothesis dummy_thf_format "poly_native_higher" false |
47646 | 667 |
val dummy_thf = (dummy_thfN, fn () => dummy_thf_config) |
44754 | 668 |
|
57293
4e619ee65a61
added 'dummy_thf_ml' prover for experiments with HOLyHammer
blanchet
parents:
57269
diff
changeset
|
669 |
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
|
670 |
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
|
671 |
|
59577 | 672 |
val pirate_format = DFG Polymorphic |
673 |
val remote_pirate_config : atp_config = |
|
674 |
{exec = K (["ISABELLE_ATP"], ["scripts/remote_pirate"]), |
|
54788
a898e15b522a
primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents:
54197
diff
changeset
|
675 |
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
|
676 |
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
|
677 |
proof_delims = [("Involved clauses:", "Involved clauses:")], |
a898e15b522a
primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents:
54197
diff
changeset
|
678 |
known_failures = known_szs_status_failures, |
a898e15b522a
primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents:
54197
diff
changeset
|
679 |
prem_role = #prem_role spass_config, |
59577 | 680 |
best_slices = K [(1.0, (((200, ""), pirate_format, "tc_native", combsN, true), ""))], |
54788
a898e15b522a
primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents:
54197
diff
changeset
|
681 |
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
|
682 |
best_max_new_mono_instances = default_max_new_mono_instances} |
59577 | 683 |
val remote_pirate = (remote_prefix ^ pirateN, fn () => remote_pirate_config) |
41740
4b09f8b9e012
added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents:
41738
diff
changeset
|
684 |
|
52073
ccb292952774
started adding agsyHOL as an experimental prover
blanchet
parents:
51998
diff
changeset
|
685 |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
686 |
(* Remote ATP invocation via SystemOnTPTP *) |
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
687 |
|
49984 | 688 |
val remote_systems = Synchronized.var "atp_remote_systems" ([] : string list) |
31835 | 689 |
|
49984 | 690 |
fun get_remote_systems () = |
62519 | 691 |
Timeout.apply (seconds 10.0) (fn () => |
58084 | 692 |
(case Isabelle_System.bash_output "\"$ISABELLE_ATP/scripts/remote_atp\" -w 2>&1" of |
693 |
(output, 0) => split_lines output |
|
694 |
| (output, _) => |
|
695 |
(warning |
|
696 |
(case extract_known_atp_failure known_perl_failures output of |
|
697 |
SOME failure => string_of_atp_failure failure |
|
63692 | 698 |
| NONE => trim_line output); []))) () |
62519 | 699 |
handle Timeout.TIMEOUT _ => [] |
31835 | 700 |
|
49984 | 701 |
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
|
702 |
find_first (String.isPrefix (name ^ "---")) systems |
49984 | 703 |
| 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
|
704 |
case find_first (String.isPrefix (name ^ "---" ^ version)) systems of |
49984 | 705 |
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
|
706 |
| 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
|
707 |
|
49984 | 708 |
fun get_remote_system name versions = |
709 |
Synchronized.change_result remote_systems |
|
710 |
(fn systems => (if null systems then get_remote_systems () else systems) |
|
711 |
|> `(`(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
|
712 |
|
49984 | 713 |
fun the_remote_system name versions = |
54788
a898e15b522a
primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents:
54197
diff
changeset
|
714 |
(case get_remote_system name versions of |
42955 | 715 |
(SOME sys, _) => sys |
63692 | 716 |
| (NONE, []) => error "SystemOnTPTP is currently not available" |
42955 | 717 |
| (NONE, syss) => |
54788
a898e15b522a
primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents:
54197
diff
changeset
|
718 |
(case syss |> filter_out (String.isPrefix "%") |> filter_out (curry (op =) "") of |
63692 | 719 |
[] => error "SystemOnTPTP is currently not available" |
720 |
| [msg] => error ("SystemOnTPTP is currently not available: " ^ msg) |
|
46480 | 721 |
| syss => |
54788
a898e15b522a
primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents:
54197
diff
changeset
|
722 |
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
|
723 |
commas_quote syss ^ ".)"))) |
31835 | 724 |
|
41148 | 725 |
val max_remote_secs = 240 (* give Geoff Sutcliffe's servers a break *) |
726 |
||
58084 | 727 |
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
|
728 |
{exec = K (["ISABELLE_ATP"], ["scripts/remote_atp"]), |
58084 | 729 |
arguments = fn _ => fn full_proofs => fn full_proof_command => fn timeout => fn file_name => fn _ => |
730 |
(if full_proofs andalso full_proof_command <> "" then "-c " ^ quote full_proof_command ^ " " |
|
731 |
else "") ^ |
|
54788
a898e15b522a
primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents:
54197
diff
changeset
|
732 |
"-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
|
733 |
"-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
|
734 |
" " ^ file_name, |
42962
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42955
diff
changeset
|
735 |
proof_delims = union (op =) tstp_proof_delims proof_delims, |
45203 | 736 |
known_failures = known_failures @ known_perl_failures @ known_says_failures, |
47976 | 737 |
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
|
738 |
best_slices = fn ctxt => [(1.0, best_slice ctxt)], |
47962
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47955
diff
changeset
|
739 |
best_max_mono_iters = default_max_mono_iters, |
58084 | 740 |
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
|
741 |
|
43500
4c357b7aa710
provide appropriate type system and number of fact defaults for remote ATPs
blanchet
parents:
43497
diff
changeset
|
742 |
fun remotify_config system_name system_versions best_slice |
58084 | 743 |
({proof_delims, known_failures, prem_role, ...} : atp_config) = |
744 |
remote_config system_name system_versions proof_delims known_failures prem_role best_slice |
|
38023 | 745 |
|
58084 | 746 |
fun remote_atp name system_name system_versions proof_delims known_failures prem_role best_slice = |
747 |
(remote_prefix ^ name, fn () => |
|
748 |
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
|
749 |
fun remotify_atp (name, config) system_name system_versions best_slice = |
58084 | 750 |
(remote_prefix ^ name, remotify_config system_name system_versions best_slice o config) |
28592 | 751 |
|
57269
1df6f747f164
changed type encoding for new Waldmeister, to trigger filtering of 'dangerous' lemmas
blanchet
parents:
57265
diff
changeset
|
752 |
fun gen_remote_waldmeister name type_enc = |
57265 | 753 |
remote_atp name "Waldmeister" ["710"] tstp_proof_delims |
754 |
([(OutOfResources, "Too many function symbols"), |
|
755 |
(Inappropriate, "**** Unexpected end of file."), |
|
756 |
(Crashed, "Unrecoverable Segmentation Fault")] |
|
757 |
@ known_szs_status_failures) |
|
57264 | 758 |
Hypothesis |
57269
1df6f747f164
changed type encoding for new Waldmeister, to trigger filtering of 'dangerous' lemmas
blanchet
parents:
57265
diff
changeset
|
759 |
(K (((50, ""), CNF_UEQ, type_enc, combsN, false), "") (* FUDGE *)) |
57264 | 760 |
|
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
|
761 |
val explicit_tff0 = TFF Monomorphic |
44589
0a1dfc6365e9
first step towards polymorphic TFF + changed defaults for Vampire
blanchet
parents:
44586
diff
changeset
|
762 |
|
52094 | 763 |
val remote_agsyhol = |
764 |
remotify_atp agsyhol "agsyHOL" ["1.0", "1"] |
|
58084 | 765 |
(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
|
766 |
val remote_e = |
63768 | 767 |
remotify_atp e "E" ["2.0", "1.9.1", "1.8"] |
66363 | 768 |
(K (((750, ""), e_tff0, "mono_native", combsN, false), "") (* FUDGE *)) |
48700 | 769 |
val remote_iprover = |
52094 | 770 |
remotify_atp iprover "iProver" ["0.99"] |
58084 | 771 |
(K (((150, ""), FOF, "mono_guards??", liftingN, false), "") (* FUDGE *)) |
48700 | 772 |
val remote_iprover_eq = |
52094 | 773 |
remotify_atp iprover_eq "iProver-Eq" ["0.8"] |
58084 | 774 |
(K (((150, ""), FOF, "mono_guards??", liftingN, false), "") (* FUDGE *)) |
44099 | 775 |
val remote_leo2 = |
52094 | 776 |
remotify_atp leo2 "LEO-II" ["1.5.0", "1.4", "1.3", "1.2", "1"] |
58084 | 777 |
(K (((40, ""), leo2_thf0, "mono_native_higher", liftingN, false), "") (* FUDGE *)) |
67021
41f1f8c4259b
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
blanchet
parents:
66544
diff
changeset
|
778 |
val remote_leo3 = |
41f1f8c4259b
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
blanchet
parents:
66544
diff
changeset
|
779 |
remotify_atp leo3 "Leo-III" ["1.1"] |
41f1f8c4259b
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
blanchet
parents:
66544
diff
changeset
|
780 |
(K (((150, ""), leo3_thf1, "poly_native_higher", keep_lamsN, false), "") (* FUDGE *)) |
44099 | 781 |
val remote_satallax = |
52094 | 782 |
remotify_atp satallax "Satallax" ["2.7", "2.3", "2"] |
67021
41f1f8c4259b
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
blanchet
parents:
66544
diff
changeset
|
783 |
(K (((150, ""), 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
|
784 |
val remote_vampire = |
66544 | 785 |
remotify_atp vampire "Vampire" ["4.2", "4.1", "4.0"] |
58084 | 786 |
(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
|
787 |
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
|
788 |
remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Conjecture |
58084 | 789 |
(K (((500, ""), FOF, "mono_guards??", combsN, false), "") (* FUDGE *)) |
41740
4b09f8b9e012
added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents:
41738
diff
changeset
|
790 |
val remote_snark = |
52094 | 791 |
remote_atp snarkN "SNARK" ["20120808r022", "20080805r029", "20080805r024"] |
58084 | 792 |
[("refutation.", "end_refutation.")] [] Hypothesis |
793 |
(K (((100, ""), explicit_tff0, "mono_native", liftingN, false), "") (* FUDGE *)) |
|
44092
bf489e54d7f8
renamed E wrappers for consistency with CASC conventions
blanchet
parents:
43989
diff
changeset
|
794 |
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
|
795 |
remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config) Hypothesis |
58084 | 796 |
(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
|
797 |
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
|
798 |
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
|
799 |
|
52073
ccb292952774
started adding agsyHOL as an experimental prover
blanchet
parents:
51998
diff
changeset
|
800 |
|
38454
9043eefe8d71
detect old Vampire and give a nicer error message
blanchet
parents:
38433
diff
changeset
|
801 |
(* Setup *) |
9043eefe8d71
detect old Vampire and give a nicer error message
blanchet
parents:
38433
diff
changeset
|
802 |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
803 |
fun add_atp (name, config) thy = |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
804 |
Data.map (Symtab.update_new (name, (config, stamp ()))) thy |
63692 | 805 |
handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name) |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
806 |
|
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
807 |
fun get_atp thy name = |
54788
a898e15b522a
primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents:
54197
diff
changeset
|
808 |
fst (the (Symtab.lookup (Data.get thy) name)) |
63692 | 809 |
handle Option.Option => error ("Unknown ATP: " ^ name) |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
810 |
|
41727
ab3f6d76fb23
available_provers ~> supported_provers (for clarity)
blanchet
parents:
41725
diff
changeset
|
811 |
val supported_atps = Symtab.keys o Data.get |
36371
8c83ea1a7740
move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents:
36370
diff
changeset
|
812 |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
813 |
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
|
814 |
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
|
815 |
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
|
816 |
end |
36371
8c83ea1a7740
move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents:
36370
diff
changeset
|
817 |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
818 |
fun refresh_systems_on_tptp () = |
49984 | 819 |
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
|
820 |
|
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
|
821 |
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
|
822 |
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
|
823 |
if ord = smartN then |
54788
a898e15b522a
primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents:
54197
diff
changeset
|
824 |
{is_lpo = false, gen_weights = (atp = spassN), gen_prec = (atp = spassN), |
59577 | 825 |
gen_simp = String.isSuffix 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
|
826 |
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
|
827 |
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
|
828 |
{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
|
829 |
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
|
830 |
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
|
831 |
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
|
832 |
|
52073
ccb292952774
started adding agsyHOL as an experimental prover
blanchet
parents:
51998
diff
changeset
|
833 |
val atps = |
68250
c45067867860
added lambda-free HO output for Ehoh (higher-order E prototype)
blanchet
parents:
68224
diff
changeset
|
834 |
[agsyhol, alt_ergo, e, e_males, e_par, ehoh, iprover, iprover_eq, leo2, leo3, satallax, spass, |
c45067867860
added lambda-free HO output for Ehoh (higher-order E prototype)
blanchet
parents:
68224
diff
changeset
|
835 |
vampire, z3_tptp, zipperposition, dummy_thf, dummy_thf_ml, remote_agsyhol, remote_e, |
c45067867860
added lambda-free HO output for Ehoh (higher-order E prototype)
blanchet
parents:
68224
diff
changeset
|
836 |
remote_e_sine, remote_e_tofof, remote_iprover, remote_iprover_eq, remote_leo2, remote_leo3, |
c45067867860
added lambda-free HO output for Ehoh (higher-order E prototype)
blanchet
parents:
68224
diff
changeset
|
837 |
remote_satallax, remote_vampire, remote_snark, remote_pirate, remote_waldmeister, |
c45067867860
added lambda-free HO output for Ehoh (higher-order E prototype)
blanchet
parents:
68224
diff
changeset
|
838 |
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
|
839 |
|
57262 | 840 |
val _ = Theory.setup (fold add_atp atps) |
35867 | 841 |
|
28592 | 842 |
end; |