author | blanchet |
Fri, 27 Jul 2012 17:34:33 +0200 | |
changeset 48558 | fabbed3abc1e |
parent 48539 | 0debf65972c7 |
child 48651 | fb461f81e76e |
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 |
47976 | 12 |
type formula_role = ATP_Problem.formula_role |
39491
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39375
diff
changeset
|
13 |
type failure = ATP_Proof.failure |
38023 | 14 |
|
46409
d4754183ccce
made option available to users (mostly for experiments)
blanchet
parents:
46407
diff
changeset
|
15 |
type slice_spec = int * 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 = |
48376
416e4123baf3
use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents:
48232
diff
changeset
|
17 |
{exec : string list * string list, |
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset
|
18 |
arguments : |
43473
fb2713b803e6
deal with ATP time slices in a more flexible/robust fashion
blanchet
parents:
43467
diff
changeset
|
19 |
Proof.context -> bool -> string -> Time.time |
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47034
diff
changeset
|
20 |
-> term_order * (unit -> (string * int) list) |
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47034
diff
changeset
|
21 |
* (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
|
22 |
proof_delims : (string * string) list, |
1eaf4d437d4c
define type system in ATP module so that ATPs can suggest a type system
blanchet
parents:
42577
diff
changeset
|
23 |
known_failures : (failure * string) list, |
47976 | 24 |
prem_role : formula_role, |
43473
fb2713b803e6
deal with ATP time slices in a more flexible/robust fashion
blanchet
parents:
43467
diff
changeset
|
25 |
best_slices : |
47962
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47955
diff
changeset
|
26 |
Proof.context -> (real * (bool * (slice_spec * string))) list, |
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47955
diff
changeset
|
27 |
best_max_mono_iters : int, |
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47955
diff
changeset
|
28 |
best_max_new_mono_instances : int} |
38023 | 29 |
|
47962
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47955
diff
changeset
|
30 |
val default_max_mono_iters : int |
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47955
diff
changeset
|
31 |
val default_max_new_mono_instances : int |
44099 | 32 |
val force_sos : bool Config.T |
47032 | 33 |
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
|
34 |
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
|
35 |
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
|
36 |
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
|
37 |
val e_sym_offset_weightN : string |
47032 | 38 |
val e_selection_heuristic : string Config.T |
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset
|
39 |
val e_default_fun_weight : real Config.T |
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset
|
40 |
val e_fun_weight_base : real Config.T |
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset
|
41 |
val e_fun_weight_span : real Config.T |
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset
|
42 |
val e_default_sym_offs_weight : real Config.T |
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset
|
43 |
val e_sym_offs_weight_base : real Config.T |
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset
|
44 |
val e_sym_offs_weight_span : real Config.T |
46643
a88bccd2b567
added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46481
diff
changeset
|
45 |
val alt_ergoN : string |
a88bccd2b567
added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46481
diff
changeset
|
46 |
val dummy_thfN : string |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
47 |
val eN : string |
44590 | 48 |
val e_sineN : string |
49 |
val e_tofofN : string |
|
45338 | 50 |
val iproverN : string |
51 |
val iprover_eqN : string |
|
44590 | 52 |
val leo2N : string |
53 |
val satallaxN : string |
|
54 |
val snarkN : string |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
55 |
val spassN : string |
48131 | 56 |
val spass_polyN : string |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
57 |
val vampireN : string |
42938 | 58 |
val waldmeisterN : string |
44423
f74707e12d30
exploit TFF format in Z3 used as ATP, and renamed it "z3_tptp"
blanchet
parents:
44422
diff
changeset
|
59 |
val z3_tptpN : string |
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
60 |
val remote_prefix : string |
41738
eb98c60a6cf0
added experimental "remote_z3_atp", Sutcliffe's TPTP-syntax-aware wrapper for Z3 -- allows to do head-to-head comparison of Sledgehammer's ATP translation and of Sascha's SMT translation
blanchet
parents:
41727
diff
changeset
|
61 |
val remote_atp : |
eb98c60a6cf0
added experimental "remote_z3_atp", Sutcliffe's TPTP-syntax-aware wrapper for Z3 -- allows to do head-to-head comparison of Sledgehammer's ATP translation and of Sascha's SMT translation
blanchet
parents:
41727
diff
changeset
|
62 |
string -> string -> string list -> (string * string) list |
47976 | 63 |
-> (failure * string) list -> formula_role |
47606
06dde48a1503
true delayed evaluation of "SPASS_VERSION" environment variable
blanchet
parents:
47506
diff
changeset
|
64 |
-> (Proof.context -> slice_spec * string) -> string * (unit -> atp_config) |
06dde48a1503
true delayed evaluation of "SPASS_VERSION" environment variable
blanchet
parents:
47506
diff
changeset
|
65 |
val add_atp : string * (unit -> atp_config) -> theory -> theory |
06dde48a1503
true delayed evaluation of "SPASS_VERSION" environment variable
blanchet
parents:
47506
diff
changeset
|
66 |
val get_atp : theory -> string -> (unit -> atp_config) |
41727
ab3f6d76fb23
available_provers ~> supported_provers (for clarity)
blanchet
parents:
41725
diff
changeset
|
67 |
val supported_atps : theory -> string list |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
68 |
val is_atp_installed : theory -> string -> bool |
35867 | 69 |
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
|
70 |
val effective_term_order : Proof.context -> string -> term_order |
35867 | 71 |
val setup : theory -> theory |
28592 | 72 |
end; |
73 |
||
36376 | 74 |
structure ATP_Systems : ATP_SYSTEMS = |
28592 | 75 |
struct |
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
76 |
|
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
|
77 |
open ATP_Problem |
39491
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39375
diff
changeset
|
78 |
open ATP_Proof |
46320 | 79 |
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
|
80 |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
81 |
(* ATP configuration *) |
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset
|
82 |
|
47962
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47955
diff
changeset
|
83 |
val default_max_mono_iters = 3 (* FUDGE *) |
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47955
diff
changeset
|
84 |
val default_max_new_mono_instances = 200 (* FUDGE *) |
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47955
diff
changeset
|
85 |
|
46409
d4754183ccce
made option available to users (mostly for experiments)
blanchet
parents:
46407
diff
changeset
|
86 |
type slice_spec = int * atp_format * string * string * bool |
d4754183ccce
made option available to users (mostly for experiments)
blanchet
parents:
46407
diff
changeset
|
87 |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
88 |
type atp_config = |
48376
416e4123baf3
use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents:
48232
diff
changeset
|
89 |
{exec : string list * string list, |
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset
|
90 |
arguments : |
43473
fb2713b803e6
deal with ATP time slices in a more flexible/robust fashion
blanchet
parents:
43467
diff
changeset
|
91 |
Proof.context -> bool -> string -> Time.time |
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47034
diff
changeset
|
92 |
-> term_order * (unit -> (string * int) list) |
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47034
diff
changeset
|
93 |
* (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
|
94 |
proof_delims : (string * string) list, |
1eaf4d437d4c
define type system in ATP module so that ATPs can suggest a type system
blanchet
parents:
42577
diff
changeset
|
95 |
known_failures : (failure * string) list, |
47976 | 96 |
prem_role : formula_role, |
47962
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47955
diff
changeset
|
97 |
best_slices : Proof.context -> (real * (bool * (slice_spec * string))) list, |
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47955
diff
changeset
|
98 |
best_max_mono_iters : int, |
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47955
diff
changeset
|
99 |
best_max_new_mono_instances : int} |
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
100 |
|
42723 | 101 |
(* "best_slices" must be found empirically, taking a wholistic approach since |
46407
30e9720cc0b9
optimization: slice caching in case two consecutive slices are nearly identical
blanchet
parents:
46402
diff
changeset
|
102 |
the ATPs are run in parallel. The "real" component gives the faction of the |
46409
d4754183ccce
made option available to users (mostly for experiments)
blanchet
parents:
46407
diff
changeset
|
103 |
time available given to the slice and should add up to 1.0. The first "bool" |
42723 | 104 |
component indicates whether the slice's strategy is complete; the "int", the |
43569
b342cd125533
removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
blanchet
parents:
43567
diff
changeset
|
105 |
preferred number of facts to pass; the first "string", the preferred type |
45521 | 106 |
system (which should be sound or quasi-sound); the second "string", the |
46409
d4754183ccce
made option available to users (mostly for experiments)
blanchet
parents:
46407
diff
changeset
|
107 |
preferred lambda translation scheme; the second "bool", whether uncurried |
d4754183ccce
made option available to users (mostly for experiments)
blanchet
parents:
46407
diff
changeset
|
108 |
aliased should be generated; the third "string", extra information to |
45521 | 109 |
the prover (e.g., SOS or no SOS). |
42723 | 110 |
|
111 |
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
|
112 |
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
|
113 |
slicing is disabled (e.g., by the minimizer). *) |
42710
84fcce345b5d
further improved type system setup based on Judgment Days
blanchet
parents:
42709
diff
changeset
|
114 |
|
38061
685d1f0f75b3
handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents:
38049
diff
changeset
|
115 |
val known_perl_failures = |
38094 | 116 |
[(CantConnect, "HTTP error"), |
117 |
(NoPerl, "env: perl"), |
|
38065 | 118 |
(NoLibwwwPerl, "Can't locate HTTP")] |
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
119 |
|
45203 | 120 |
fun known_szs_failures wrap = |
121 |
[(Unprovable, wrap "CounterSatisfiable"), |
|
122 |
(Unprovable, wrap "Satisfiable"), |
|
123 |
(GaveUp, wrap "GaveUp"), |
|
124 |
(GaveUp, wrap "Unknown"), |
|
125 |
(GaveUp, wrap "Incomplete"), |
|
126 |
(ProofMissing, wrap "Theorem"), |
|
127 |
(ProofMissing, wrap "Unsatisfiable"), |
|
128 |
(TimedOut, wrap "Timeout"), |
|
129 |
(Inappropriate, wrap "Inappropriate"), |
|
130 |
(OutOfResources, wrap "ResourceOut"), |
|
131 |
(OutOfResources, wrap "MemoryOut"), |
|
132 |
(Interrupted, wrap "Forced"), |
|
133 |
(Interrupted, wrap "User")] |
|
134 |
||
135 |
val known_szs_status_failures = known_szs_failures (prefix "SZS status ") |
|
136 |
val known_says_failures = known_szs_failures (prefix " says ") |
|
137 |
||
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
138 |
(* named ATPs *) |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
139 |
|
46643
a88bccd2b567
added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46481
diff
changeset
|
140 |
val alt_ergoN = "alt_ergo" |
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
|
141 |
val dummy_thfN = "dummy_thf" (* for experiments *) |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
142 |
val eN = "e" |
44590 | 143 |
val e_sineN = "e_sine" |
144 |
val e_tofofN = "e_tofof" |
|
45338 | 145 |
val iproverN = "iprover" |
146 |
val iprover_eqN = "iprover_eq" |
|
44099 | 147 |
val leo2N = "leo2" |
148 |
val satallaxN = "satallax" |
|
44590 | 149 |
val snarkN = "snark" |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
150 |
val spassN = "spass" |
48131 | 151 |
val spass_polyN = "spass_poly" |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
152 |
val vampireN = "vampire" |
44590 | 153 |
val waldmeisterN = "waldmeister" |
44423
f74707e12d30
exploit TFF format in Z3 used as ATP, and renamed it "z3_tptp"
blanchet
parents:
44422
diff
changeset
|
154 |
val z3_tptpN = "z3_tptp" |
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
155 |
val remote_prefix = "remote_" |
38001
a9b47b85ca24
reintroduced more preprocessing steps to Sledgehammer, adapted to the new FOF setting
blanchet
parents:
38000
diff
changeset
|
156 |
|
38023 | 157 |
structure Data = Theory_Data |
158 |
( |
|
47606
06dde48a1503
true delayed evaluation of "SPASS_VERSION" environment variable
blanchet
parents:
47506
diff
changeset
|
159 |
type T = ((unit -> atp_config) * stamp) Symtab.table |
38023 | 160 |
val empty = Symtab.empty |
161 |
val extend = I |
|
46407
30e9720cc0b9
optimization: slice caching in case two consecutive slices are nearly identical
blanchet
parents:
46402
diff
changeset
|
162 |
fun merge data : T = |
30e9720cc0b9
optimization: slice caching in case two consecutive slices are nearly identical
blanchet
parents:
46402
diff
changeset
|
163 |
Symtab.merge (eq_snd (op =)) data |
38023 | 164 |
handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".") |
165 |
) |
|
38017
3ad3e3ca2451
move Sledgehammer-specific code out of "Sledgehammer_TPTP_Format"
blanchet
parents:
38015
diff
changeset
|
166 |
|
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
|
167 |
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
|
168 |
|
43473
fb2713b803e6
deal with ATP time slices in a more flexible/robust fashion
blanchet
parents:
43467
diff
changeset
|
169 |
val sosN = "sos" |
fb2713b803e6
deal with ATP time slices in a more flexible/robust fashion
blanchet
parents:
43467
diff
changeset
|
170 |
val no_sosN = "no_sos" |
fb2713b803e6
deal with ATP time slices in a more flexible/robust fashion
blanchet
parents:
43467
diff
changeset
|
171 |
|
44099 | 172 |
val force_sos = Attrib.setup_config_bool @{binding atp_force_sos} (K false) |
173 |
||
47032 | 174 |
val smartN = "smart" |
47073
c73f7b0c7ebc
generate weights and precedences for predicates as well
blanchet
parents:
47055
diff
changeset
|
175 |
(* val kboN = "kbo" *) |
47032 | 176 |
val lpoN = "lpo" |
47034
77da780ddd6b
implement term order attribute (for experiments)
blanchet
parents:
47033
diff
changeset
|
177 |
val xweightsN = "_weights" |
77da780ddd6b
implement term order attribute (for experiments)
blanchet
parents:
47033
diff
changeset
|
178 |
val xprecN = "_prec" |
77da780ddd6b
implement term order attribute (for experiments)
blanchet
parents:
47033
diff
changeset
|
179 |
val xsimpN = "_simp" (* SPASS-specific *) |
47032 | 180 |
|
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47034
diff
changeset
|
181 |
(* Possible values for "atp_term_order": |
47049 | 182 |
"smart", "(kbo|lpo)(_weights)?(_prec|_simp)?" *) |
47032 | 183 |
val term_order = |
184 |
Attrib.setup_config_string @{binding atp_term_order} (K smartN) |
|
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 |
|
48130 | 188 |
val alt_ergo_tff1 = TFF (Polymorphic, TPTP_Explicit) |
46643
a88bccd2b567
added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46481
diff
changeset
|
189 |
|
a88bccd2b567
added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46481
diff
changeset
|
190 |
val alt_ergo_config : atp_config = |
48376
416e4123baf3
use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents:
48232
diff
changeset
|
191 |
{exec = (["WHY3_HOME"], ["why3"]), |
46643
a88bccd2b567
added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46481
diff
changeset
|
192 |
arguments = |
a88bccd2b567
added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46481
diff
changeset
|
193 |
fn _ => fn _ => fn _ => fn timeout => fn _ => |
a88bccd2b567
added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46481
diff
changeset
|
194 |
"--format tff1 --prover alt-ergo --timelimit " ^ |
a88bccd2b567
added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46481
diff
changeset
|
195 |
string_of_int (to_secs 1 timeout), |
a88bccd2b567
added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46481
diff
changeset
|
196 |
proof_delims = [], |
a88bccd2b567
added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46481
diff
changeset
|
197 |
known_failures = |
a88bccd2b567
added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46481
diff
changeset
|
198 |
[(ProofMissing, ": Valid"), |
a88bccd2b567
added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46481
diff
changeset
|
199 |
(TimedOut, ": Timeout"), |
a88bccd2b567
added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46481
diff
changeset
|
200 |
(GaveUp, ": Unknown")], |
47976 | 201 |
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
|
202 |
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
|
203 |
(* FUDGE *) |
47962
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47955
diff
changeset
|
204 |
[(1.0, (false, ((100, alt_ergo_tff1, "poly_native", liftingN, false), "")))], |
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47955
diff
changeset
|
205 |
best_max_mono_iters = default_max_mono_iters, |
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47955
diff
changeset
|
206 |
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
|
207 |
|
47646 | 208 |
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
|
209 |
|
a88bccd2b567
added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46481
diff
changeset
|
210 |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
211 |
(* E *) |
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
212 |
|
48232
712d49104b13
don't ask E to generate a detailed proofs if not needed
blanchet
parents:
48131
diff
changeset
|
213 |
fun is_recent_e_version () = (string_ord (getenv "E_VERSION", "1.3") <> LESS) |
712d49104b13
don't ask E to generate a detailed proofs if not needed
blanchet
parents:
48131
diff
changeset
|
214 |
fun is_new_e_version () = (string_ord (getenv "E_VERSION", "1.6") <> LESS) |
44420 | 215 |
|
36369
d2cd0d04b8e6
handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents:
36289
diff
changeset
|
216 |
val tstp_proof_delims = |
42962
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42955
diff
changeset
|
217 |
[("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation"), |
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42955
diff
changeset
|
218 |
("% SZS output start CNFRefutation", "% SZS output end CNFRefutation")] |
36369
d2cd0d04b8e6
handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents:
36289
diff
changeset
|
219 |
|
43473
fb2713b803e6
deal with ATP time slices in a more flexible/robust fashion
blanchet
parents:
43467
diff
changeset
|
220 |
val e_smartN = "smart" |
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset
|
221 |
val e_autoN = "auto" |
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset
|
222 |
val e_fun_weightN = "fun_weight" |
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset
|
223 |
val e_sym_offset_weightN = "sym_offset_weight" |
41725
7cca2de89296
added support for bleeding-edge E weighting function "SymOffsetsWeight"
blanchet
parents:
41335
diff
changeset
|
224 |
|
47032 | 225 |
val e_selection_heuristic = |
226 |
Attrib.setup_config_string @{binding atp_e_selection_heuristic} (K e_smartN) |
|
41770 | 227 |
(* FUDGE *) |
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset
|
228 |
val e_default_fun_weight = |
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset
|
229 |
Attrib.setup_config_real @{binding atp_e_default_fun_weight} (K 20.0) |
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset
|
230 |
val e_fun_weight_base = |
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset
|
231 |
Attrib.setup_config_real @{binding atp_e_fun_weight_base} (K 0.0) |
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset
|
232 |
val e_fun_weight_span = |
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset
|
233 |
Attrib.setup_config_real @{binding atp_e_fun_weight_span} (K 40.0) |
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset
|
234 |
val e_default_sym_offs_weight = |
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset
|
235 |
Attrib.setup_config_real @{binding atp_e_default_sym_offs_weight} (K 1.0) |
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset
|
236 |
val e_sym_offs_weight_base = |
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset
|
237 |
Attrib.setup_config_real @{binding atp_e_sym_offs_weight_base} (K ~20.0) |
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset
|
238 |
val e_sym_offs_weight_span = |
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset
|
239 |
Attrib.setup_config_real @{binding atp_e_sym_offs_weight_span} (K 60.0) |
41725
7cca2de89296
added support for bleeding-edge E weighting function "SymOffsetsWeight"
blanchet
parents:
41335
diff
changeset
|
240 |
|
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47034
diff
changeset
|
241 |
fun e_selection_heuristic_case heuristic fw sow = |
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47034
diff
changeset
|
242 |
if heuristic = e_fun_weightN then fw |
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47034
diff
changeset
|
243 |
else if heuristic = e_sym_offset_weightN then sow |
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47034
diff
changeset
|
244 |
else raise Fail ("unexpected " ^ quote heuristic) |
41725
7cca2de89296
added support for bleeding-edge E weighting function "SymOffsetsWeight"
blanchet
parents:
41335
diff
changeset
|
245 |
|
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47034
diff
changeset
|
246 |
fun scaled_e_selection_weight ctxt heuristic w = |
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47034
diff
changeset
|
247 |
w * Config.get ctxt (e_selection_heuristic_case heuristic |
47029 | 248 |
e_fun_weight_span e_sym_offs_weight_span) |
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47034
diff
changeset
|
249 |
+ Config.get ctxt (e_selection_heuristic_case heuristic |
47029 | 250 |
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
|
251 |
|> 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
|
252 |
|
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47034
diff
changeset
|
253 |
fun e_selection_weight_arguments ctxt heuristic sel_weights = |
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47034
diff
changeset
|
254 |
if heuristic = e_autoN then |
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47034
diff
changeset
|
255 |
"-xAuto" |
41725
7cca2de89296
added support for bleeding-edge E weighting function "SymOffsetsWeight"
blanchet
parents:
41335
diff
changeset
|
256 |
else |
43622 | 257 |
(* supplied by Stephan Schulz *) |
41314
2dc1dfc1bc69
use the options provided by Stephan Schulz -- much better
blanchet
parents:
41313
diff
changeset
|
258 |
"--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
|
259 |
\--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
|
260 |
\--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
|
261 |
\--delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*" ^ |
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47034
diff
changeset
|
262 |
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
|
263 |
"(SimulateSOS," ^ |
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47034
diff
changeset
|
264 |
(e_selection_heuristic_case heuristic |
47029 | 265 |
e_default_fun_weight e_default_sym_offs_weight |
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset
|
266 |
|> 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
|
267 |
",20,1.5,1.5,1" ^ |
47030 | 268 |
(sel_weights () |
47029 | 269 |
|> map (fn (s, w) => "," ^ s ^ ":" ^ |
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47034
diff
changeset
|
270 |
scaled_e_selection_weight ctxt heuristic w) |
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset
|
271 |
|> implode) ^ |
41314
2dc1dfc1bc69
use the options provided by Stephan Schulz -- much better
blanchet
parents:
41313
diff
changeset
|
272 |
"),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
|
273 |
\1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*\ |
2dc1dfc1bc69
use the options provided by Stephan Schulz -- much better
blanchet
parents:
41313
diff
changeset
|
274 |
\FIFOWeight(PreferProcessed))'" |
41313
a96ac4d180b7
optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents:
41269
diff
changeset
|
275 |
|
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47034
diff
changeset
|
276 |
val e_ord_weights = |
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47034
diff
changeset
|
277 |
map (fn (s, w) => s ^ ":" ^ string_of_int w) #> space_implode "," |
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47034
diff
changeset
|
278 |
fun e_ord_precedence [_] = "" |
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47034
diff
changeset
|
279 |
| e_ord_precedence info = info |> map fst |> space_implode "<" |
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47034
diff
changeset
|
280 |
|
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
|
281 |
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
|
282 |
| e_term_order_info_arguments gen_weights gen_prec ord_info = |
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47034
diff
changeset
|
283 |
let val ord_info = ord_info () in |
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47034
diff
changeset
|
284 |
(if gen_weights then "--order-weights='" ^ e_ord_weights ord_info ^ "' " |
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47034
diff
changeset
|
285 |
else "") ^ |
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47034
diff
changeset
|
286 |
(if gen_prec then "--precedence='" ^ e_ord_precedence ord_info ^ "' " |
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47034
diff
changeset
|
287 |
else "") |
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47034
diff
changeset
|
288 |
end |
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47034
diff
changeset
|
289 |
|
48232
712d49104b13
don't ask E to generate a detailed proofs if not needed
blanchet
parents:
48131
diff
changeset
|
290 |
fun e_shell_level_argument full_proof = |
712d49104b13
don't ask E to generate a detailed proofs if not needed
blanchet
parents:
48131
diff
changeset
|
291 |
if is_new_e_version () then |
712d49104b13
don't ask E to generate a detailed proofs if not needed
blanchet
parents:
48131
diff
changeset
|
292 |
" --pcl-shell-level=" ^ (if full_proof then "0" else "2") |
712d49104b13
don't ask E to generate a detailed proofs if not needed
blanchet
parents:
48131
diff
changeset
|
293 |
else |
712d49104b13
don't ask E to generate a detailed proofs if not needed
blanchet
parents:
48131
diff
changeset
|
294 |
"" |
712d49104b13
don't ask E to generate a detailed proofs if not needed
blanchet
parents:
48131
diff
changeset
|
295 |
|
47032 | 296 |
fun effective_e_selection_heuristic ctxt = |
48232
712d49104b13
don't ask E to generate a detailed proofs if not needed
blanchet
parents:
48131
diff
changeset
|
297 |
if is_recent_e_version () then Config.get ctxt e_selection_heuristic |
712d49104b13
don't ask E to generate a detailed proofs if not needed
blanchet
parents:
48131
diff
changeset
|
298 |
else e_autoN |
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42332
diff
changeset
|
299 |
|
48232
712d49104b13
don't ask E to generate a detailed proofs if not needed
blanchet
parents:
48131
diff
changeset
|
300 |
fun e_kbo () = if is_recent_e_version () then "KBO6" else "KBO" |
47505
e33d957ae2bf
avoid option introduced in E 1.2 when invoking older versions of E
blanchet
parents:
47499
diff
changeset
|
301 |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
302 |
val e_config : atp_config = |
48376
416e4123baf3
use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents:
48232
diff
changeset
|
303 |
{exec = (["E_HOME"], ["eproof_ram", "eproof"]), |
43354
396aaa15dd8b
pass --trim option to "eproof" script to speed up proof reconstruction
blanchet
parents:
43288
diff
changeset
|
304 |
arguments = |
48232
712d49104b13
don't ask E to generate a detailed proofs if not needed
blanchet
parents:
48131
diff
changeset
|
305 |
fn ctxt => fn full_proof => fn heuristic => fn timeout => |
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47034
diff
changeset
|
306 |
fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) => |
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47034
diff
changeset
|
307 |
"--tstp-in --tstp-out --output-level=5 --silent " ^ |
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47034
diff
changeset
|
308 |
e_selection_weight_arguments ctxt heuristic sel_weights ^ " " ^ |
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
|
309 |
e_term_order_info_arguments gen_weights gen_prec ord_info ^ " " ^ |
47505
e33d957ae2bf
avoid option introduced in E 1.2 when invoking older versions of E
blanchet
parents:
47499
diff
changeset
|
310 |
"--term-ordering=" ^ (if is_lpo then "LPO4" else e_kbo ()) ^ " " ^ |
48232
712d49104b13
don't ask E to generate a detailed proofs if not needed
blanchet
parents:
48131
diff
changeset
|
311 |
"--cpu-limit=" ^ string_of_int (to_secs 2 timeout) ^ |
712d49104b13
don't ask E to generate a detailed proofs if not needed
blanchet
parents:
48131
diff
changeset
|
312 |
e_shell_level_argument full_proof, |
48376
416e4123baf3
use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents:
48232
diff
changeset
|
313 |
proof_delims = tstp_proof_delims, |
36265
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset
|
314 |
known_failures = |
45203 | 315 |
[(TimedOut, "Failure: Resource limit exceeded (time)"), |
47972 | 316 |
(TimedOut, "time limit exceeded")] @ |
317 |
known_szs_status_failures, |
|
47976 | 318 |
prem_role = Conjecture, |
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset
|
319 |
best_slices = fn ctxt => |
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47034
diff
changeset
|
320 |
let val heuristic = effective_e_selection_heuristic ctxt in |
43474
423cd1ecf714
optimized E's time slicing, based on latest exhaustive Judgment Day results
blanchet
parents:
43473
diff
changeset
|
321 |
(* FUDGE *) |
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47034
diff
changeset
|
322 |
if heuristic = e_smartN then |
46449 | 323 |
[(0.333, (true, ((500, FOF, "mono_tags??", combsN, false), e_fun_weightN))), |
324 |
(0.334, (true, ((50, FOF, "mono_guards??", combsN, false), e_fun_weightN))), |
|
325 |
(0.333, (true, ((1000, FOF, "mono_tags??", combsN, false), e_sym_offset_weightN)))] |
|
43473
fb2713b803e6
deal with ATP time slices in a more flexible/robust fashion
blanchet
parents:
43467
diff
changeset
|
326 |
else |
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
47034
diff
changeset
|
327 |
[(1.0, (true, ((500, FOF, "mono_tags??", combsN, false), heuristic)))] |
47962
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47955
diff
changeset
|
328 |
end, |
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47955
diff
changeset
|
329 |
best_max_mono_iters = default_max_mono_iters, |
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47955
diff
changeset
|
330 |
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
|
331 |
|
47646 | 332 |
val e = (eN, fn () => e_config) |
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
333 |
|
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
334 |
|
44099 | 335 |
(* LEO-II *) |
336 |
||
48004
989a34fa72b3
don't generate definitions for LEO-II -- this cuases more harm than good
blanchet
parents:
47985
diff
changeset
|
337 |
(* LEO-II supports definitions, but it performs significantly better on our |
989a34fa72b3
don't generate definitions for LEO-II -- this cuases more harm than good
blanchet
parents:
47985
diff
changeset
|
338 |
benchmarks when they are not used. *) |
989a34fa72b3
don't generate definitions for LEO-II -- this cuases more harm than good
blanchet
parents:
47985
diff
changeset
|
339 |
val leo2_thf0 = |
48130 | 340 |
THF (Monomorphic, TPTP_Explicit, THF_Without_Choice, THF_Without_Defs) |
44754 | 341 |
|
44099 | 342 |
val leo2_config : atp_config = |
48376
416e4123baf3
use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents:
48232
diff
changeset
|
343 |
{exec = (["LEO2_HOME"], ["leo"]), |
44099 | 344 |
arguments = |
47916 | 345 |
fn _ => fn _ => fn _ => fn timeout => fn _ => |
48084
e6cffd467ff5
robust LEO-II setup that doesn't rely on ".leoatprc"
blanchet
parents:
48077
diff
changeset
|
346 |
"--foatp e --atp e=\"$E_HOME\"/eprover \ |
e6cffd467ff5
robust LEO-II setup that doesn't rely on ".leoatprc"
blanchet
parents:
48077
diff
changeset
|
347 |
\--atp epclextract=\"$E_HOME\"/epclextract \ |
e6cffd467ff5
robust LEO-II setup that doesn't rely on ".leoatprc"
blanchet
parents:
48077
diff
changeset
|
348 |
\--proofoutput 1 --timeout " ^ |
e6cffd467ff5
robust LEO-II setup that doesn't rely on ".leoatprc"
blanchet
parents:
48077
diff
changeset
|
349 |
string_of_int (to_secs 1 timeout), |
44099 | 350 |
proof_delims = tstp_proof_delims, |
45207 | 351 |
known_failures = |
47974
08d2dcc2dab9
improved LEO-II definition handling -- still hoping for a fix directly in LEO-II
blanchet
parents:
47972
diff
changeset
|
352 |
[(TimedOut, "CPU time limit exceeded, terminating"), |
47972 | 353 |
(GaveUp, "No.of.Axioms")] @ |
354 |
known_szs_status_failures, |
|
47976 | 355 |
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
|
356 |
best_slices = |
44099 | 357 |
(* FUDGE *) |
48097
7618e1d9322c
pass more facts to LEO-II, in the light of latest evaluation
blanchet
parents:
48084
diff
changeset
|
358 |
K [(1.0, (true, ((40, leo2_thf0, "mono_native_higher", keep_lamsN, false), "")))], |
47962
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47955
diff
changeset
|
359 |
best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *), |
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47955
diff
changeset
|
360 |
best_max_new_mono_instances = default_max_new_mono_instances div 2 (* FUDGE *)} |
39491
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39375
diff
changeset
|
361 |
|
47646 | 362 |
val leo2 = (leo2N, fn () => leo2_config) |
44099 | 363 |
|
364 |
||
365 |
(* Satallax *) |
|
366 |
||
48004
989a34fa72b3
don't generate definitions for LEO-II -- this cuases more harm than good
blanchet
parents:
47985
diff
changeset
|
367 |
val satallax_thf0 = |
48130 | 368 |
THF (Monomorphic, TPTP_Explicit, THF_With_Choice, THF_With_Defs) |
44754 | 369 |
|
44099 | 370 |
val satallax_config : atp_config = |
48376
416e4123baf3
use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents:
48232
diff
changeset
|
371 |
{exec = (["SATALLAX_HOME"], ["satallax"]), |
44099 | 372 |
arguments = |
373 |
fn _ => fn _ => fn _ => fn timeout => fn _ => |
|
45162 | 374 |
"-p hocore -t " ^ string_of_int (to_secs 1 timeout), |
375 |
proof_delims = |
|
376 |
[("% Higher-Order Unsat Core BEGIN", "% Higher-Order Unsat Core END")], |
|
45203 | 377 |
known_failures = known_szs_status_failures, |
47981 | 378 |
prem_role = Hypothesis, |
44416
cabd06b69c18
added formats to the slice and use TFF for remote Vampire
blanchet
parents:
44391
diff
changeset
|
379 |
best_slices = |
44754 | 380 |
(* FUDGE *) |
47985 | 381 |
K [(1.0, (true, ((60, satallax_thf0, "mono_native_higher", keep_lamsN, false), "")))], |
47962
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47955
diff
changeset
|
382 |
best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *), |
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47955
diff
changeset
|
383 |
best_max_new_mono_instances = default_max_new_mono_instances div 2 (* FUDGE *)} |
44099 | 384 |
|
47646 | 385 |
val satallax = (satallaxN, fn () => satallax_config) |
44099 | 386 |
|
387 |
||
388 |
(* 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
|
389 |
|
48005
eeede26f2721
killed SPASS 3.5/3.7 FLOTTER hack -- requires users to upgrade to SPASS 3.8
blanchet
parents:
48004
diff
changeset
|
390 |
val spass_H1SOS = "-Heuristic=1 -SOS" |
eeede26f2721
killed SPASS 3.5/3.7 FLOTTER hack -- requires users to upgrade to SPASS 3.8
blanchet
parents:
48004
diff
changeset
|
391 |
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
|
392 |
val spass_H2SOS = "-Heuristic=2 -SOS" |
eeede26f2721
killed SPASS 3.5/3.7 FLOTTER hack -- requires users to upgrade to SPASS 3.8
blanchet
parents:
48004
diff
changeset
|
393 |
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
|
394 |
val spass_H2NuVS0Red2 = "-Heuristic=2 -RNuV=1 -Sorts=0 -RFRew=2 -RBRew=2 -RTaut=2" |
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
|
395 |
|
48005
eeede26f2721
killed SPASS 3.5/3.7 FLOTTER hack -- requires users to upgrade to SPASS 3.8
blanchet
parents:
48004
diff
changeset
|
396 |
(* FIXME: Make "SPASS_NEW_HOME" legacy. *) |
eeede26f2721
killed SPASS 3.5/3.7 FLOTTER hack -- requires users to upgrade to SPASS 3.8
blanchet
parents:
48004
diff
changeset
|
397 |
val spass_config : atp_config = |
48376
416e4123baf3
use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents:
48232
diff
changeset
|
398 |
{exec = (["SPASS_NEW_HOME", "SPASS_HOME"], ["SPASS"]), |
48005
eeede26f2721
killed SPASS 3.5/3.7 FLOTTER hack -- requires users to upgrade to SPASS 3.8
blanchet
parents:
48004
diff
changeset
|
399 |
arguments = fn _ => fn _ => fn extra_options => fn timeout => fn _ => |
eeede26f2721
killed SPASS 3.5/3.7 FLOTTER hack -- requires users to upgrade to SPASS 3.8
blanchet
parents:
48004
diff
changeset
|
400 |
("-Isabelle=1 -TimeLimit=" ^ string_of_int (to_secs 1 timeout)) |
eeede26f2721
killed SPASS 3.5/3.7 FLOTTER hack -- requires users to upgrade to SPASS 3.8
blanchet
parents:
48004
diff
changeset
|
401 |
|> extra_options <> "" ? prefix (extra_options ^ " "), |
36369
d2cd0d04b8e6
handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents:
36289
diff
changeset
|
402 |
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
|
403 |
known_failures = |
48005
eeede26f2721
killed SPASS 3.5/3.7 FLOTTER hack -- requires users to upgrade to SPASS 3.8
blanchet
parents:
48004
diff
changeset
|
404 |
[(OldSPASS, "Unrecognized option Isabelle"), |
47950
9cb132898ac8
invite users to upgrade their SPASS (so we can get rid of old code)
blanchet
parents:
47949
diff
changeset
|
405 |
(GaveUp, "SPASS beiseite: Completion found"), |
36370
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
406 |
(TimedOut, "SPASS beiseite: Ran out of time"), |
36965 | 407 |
(OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"), |
37413 | 408 |
(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
|
409 |
(MalformedInput, "Free Variable"), |
44391 | 410 |
(Unprovable, "No formulae and clauses found in input file"), |
47972 | 411 |
(InternalError, "Please report this error")] @ |
412 |
known_perl_failures, |
|
47976 | 413 |
prem_role = Conjecture, |
48005
eeede26f2721
killed SPASS 3.5/3.7 FLOTTER hack -- requires users to upgrade to SPASS 3.8
blanchet
parents:
48004
diff
changeset
|
414 |
best_slices = fn _ => |
42723 | 415 |
(* FUDGE *) |
48131 | 416 |
[(0.1667, (false, ((150, DFG Monomorphic, "mono_native", combsN, true), ""))), |
417 |
(0.1667, (false, ((500, DFG Monomorphic, "mono_native", liftingN, true), spass_H2SOS))), |
|
418 |
(0.1666, (false, ((50, DFG Monomorphic, "mono_native", liftingN, true), spass_H2LR0LT0))), |
|
419 |
(0.1000, (false, ((250, DFG Monomorphic, "mono_native", combsN, true), spass_H2NuVS0))), |
|
420 |
(0.1000, (false, ((1000, DFG Monomorphic, "mono_native", liftingN, true), spass_H1SOS))), |
|
421 |
(0.1000, (false, ((150, DFG Monomorphic, "poly_guards??", liftingN, false), spass_H2NuVS0Red2))), |
|
422 |
(0.1000, (false, ((300, DFG Monomorphic, "mono_native", combsN, true), spass_H2SOS))), |
|
48558
fabbed3abc1e
tweaks in preparation for type encoding evaluation
blanchet
parents:
48539
diff
changeset
|
423 |
(0.1000, (false, ((100, DFG Monomorphic, "mono_native", combs_and_liftingN, true), "")))], |
47962
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47955
diff
changeset
|
424 |
best_max_mono_iters = default_max_mono_iters, |
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47955
diff
changeset
|
425 |
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
|
426 |
|
48005
eeede26f2721
killed SPASS 3.5/3.7 FLOTTER hack -- requires users to upgrade to SPASS 3.8
blanchet
parents:
48004
diff
changeset
|
427 |
val spass = (spassN, fn () => spass_config) |
38454
9043eefe8d71
detect old Vampire and give a nicer error message
blanchet
parents:
38433
diff
changeset
|
428 |
|
37509
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
37506
diff
changeset
|
429 |
(* Vampire *) |
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
37506
diff
changeset
|
430 |
|
48007 | 431 |
(* Vampire 1.8 has TFF support, but the support was buggy until revision |
432 |
1435 (or shortly before). *) |
|
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
|
433 |
fun is_new_vampire_version () = |
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
|
434 |
string_ord (getenv "VAMPIRE_VERSION", "1.8") = GREATER |
44420 | 435 |
|
48130 | 436 |
val vampire_tff0 = TFF (Monomorphic, TPTP_Implicit) |
44589
0a1dfc6365e9
first step towards polymorphic TFF + changed defaults for Vampire
blanchet
parents:
44586
diff
changeset
|
437 |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
438 |
val vampire_config : atp_config = |
48376
416e4123baf3
use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents:
48232
diff
changeset
|
439 |
{exec = (["VAMPIRE_HOME"], ["vampire"]), |
43569
b342cd125533
removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
blanchet
parents:
43567
diff
changeset
|
440 |
arguments = fn _ => fn _ => fn sos => fn timeout => fn _ => |
44417 | 441 |
"--mode casc -t " ^ string_of_int (to_secs 1 timeout) ^ |
45234
5509362b924b
disable Vampire's BDD optimization, which sometimes yields so huge proofs that this causes problems for reconstruction
blanchet
parents:
45207
diff
changeset
|
442 |
" --proof tptp --output_axiom_names on\ |
5509362b924b
disable Vampire's BDD optimization, which sometimes yields so huge proofs that this causes problems for reconstruction
blanchet
parents:
45207
diff
changeset
|
443 |
\ --forced_options propositional_to_bdd=off\ |
44417 | 444 |
\ --thanks \"Andrei and Krystof\" --input_file" |
43473
fb2713b803e6
deal with ATP time slices in a more flexible/robust fashion
blanchet
parents:
43467
diff
changeset
|
445 |
|> 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
|
446 |
proof_delims = |
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
37506
diff
changeset
|
447 |
[("=========== Refutation ==========", |
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
37506
diff
changeset
|
448 |
"======= End of refutation ======="), |
38033 | 449 |
("% SZS output start Refutation", "% SZS output end Refutation"), |
450 |
("% SZS output start Proof", "% SZS output end Proof")], |
|
37509
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
37506
diff
changeset
|
451 |
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
|
452 |
[(GaveUp, "UNPROVABLE"), |
59284a13abc4
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents:
42999
diff
changeset
|
453 |
(GaveUp, "CANNOT PROVE"), |
37509
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
37506
diff
changeset
|
454 |
(Unprovable, "Satisfiability detected"), |
38647
5500241da479
play with fudge factor + parse one more Vampire error
blanchet
parents:
38646
diff
changeset
|
455 |
(Unprovable, "Termination reason: Satisfiable"), |
47972 | 456 |
(Interrupted, "Aborted by signal SIGINT")] @ |
457 |
known_szs_status_failures, |
|
47976 | 458 |
prem_role = Conjecture, |
42725
64dea91bbe0e
added "force_sos" options to control SPASS's and Vampire's use of SOS in experiments + added corresponding Mirabelle options
blanchet
parents:
42723
diff
changeset
|
459 |
best_slices = fn ctxt => |
42723 | 460 |
(* FUDGE *) |
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
|
461 |
(if is_new_vampire_version () then |
47948 | 462 |
[(0.333, (false, ((500, vampire_tff0, "mono_native", combs_or_liftingN, false), sosN))), |
463 |
(0.333, (false, ((150, vampire_tff0, "poly_guards??", combs_or_liftingN, false), sosN))), |
|
47055
16e2633f3b4b
made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
blanchet
parents:
47053
diff
changeset
|
464 |
(0.334, (true, ((50, vampire_tff0, "mono_native", combs_or_liftingN, false), no_sosN)))] |
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
|
465 |
else |
46449 | 466 |
[(0.333, (false, ((150, FOF, "poly_guards??", combs_or_liftingN, false), sosN))), |
467 |
(0.333, (false, ((500, FOF, "mono_tags??", combs_or_liftingN, false), sosN))), |
|
47055
16e2633f3b4b
made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
blanchet
parents:
47053
diff
changeset
|
468 |
(0.334, (true, ((50, FOF, "mono_guards??", combs_or_liftingN, false), no_sosN)))]) |
44099 | 469 |
|> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single |
47962
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47955
diff
changeset
|
470 |
else I), |
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47955
diff
changeset
|
471 |
best_max_mono_iters = default_max_mono_iters, |
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47955
diff
changeset
|
472 |
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
|
473 |
|
47646 | 474 |
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
|
475 |
|
38454
9043eefe8d71
detect old Vampire and give a nicer error message
blanchet
parents:
38433
diff
changeset
|
476 |
|
41740
4b09f8b9e012
added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents:
41738
diff
changeset
|
477 |
(* Z3 with TPTP syntax *) |
4b09f8b9e012
added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents:
41738
diff
changeset
|
478 |
|
48130 | 479 |
val z3_tff0 = TFF (Monomorphic, TPTP_Implicit) |
44589
0a1dfc6365e9
first step towards polymorphic TFF + changed defaults for Vampire
blanchet
parents:
44586
diff
changeset
|
480 |
|
44423
f74707e12d30
exploit TFF format in Z3 used as ATP, and renamed it "z3_tptp"
blanchet
parents:
44422
diff
changeset
|
481 |
val z3_tptp_config : atp_config = |
48376
416e4123baf3
use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents:
48232
diff
changeset
|
482 |
{exec = (["Z3_HOME"], ["z3"]), |
43354
396aaa15dd8b
pass --trim option to "eproof" script to speed up proof reconstruction
blanchet
parents:
43288
diff
changeset
|
483 |
arguments = fn _ => fn _ => fn _ => fn timeout => fn _ => |
48539 | 484 |
"MBQI=true DISPLAY_UNSAT_CORE=true -tptp -t:" ^ |
485 |
string_of_int (to_secs 1 timeout), |
|
486 |
proof_delims = [("\ncore(", ").")], |
|
45203 | 487 |
known_failures = known_szs_status_failures, |
47976 | 488 |
prem_role = Hypothesis, |
42723 | 489 |
best_slices = |
44423
f74707e12d30
exploit TFF format in Z3 used as ATP, and renamed it "z3_tptp"
blanchet
parents:
44422
diff
changeset
|
490 |
(* FUDGE *) |
46435 | 491 |
K [(0.5, (false, ((250, z3_tff0, "mono_native", combsN, false), ""))), |
492 |
(0.25, (false, ((125, z3_tff0, "mono_native", combsN, false), ""))), |
|
493 |
(0.125, (false, ((62, z3_tff0, "mono_native", combsN, false), ""))), |
|
47962
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47955
diff
changeset
|
494 |
(0.125, (false, ((31, z3_tff0, "mono_native", combsN, false), "")))], |
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47955
diff
changeset
|
495 |
best_max_mono_iters = default_max_mono_iters, |
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47955
diff
changeset
|
496 |
best_max_new_mono_instances = default_max_new_mono_instances} |
41740
4b09f8b9e012
added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents:
41738
diff
changeset
|
497 |
|
47646 | 498 |
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
|
499 |
|
44590 | 500 |
|
48131 | 501 |
(* Not really a prover: Experimental Polymorphic THF and DFG output *) |
44590 | 502 |
|
44754 | 503 |
fun dummy_config format type_enc : atp_config = |
48376
416e4123baf3
use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents:
48232
diff
changeset
|
504 |
{exec = (["ISABELLE_ATP"], ["scripts/dummy_atp"]), |
44590 | 505 |
arguments = K (K (K (K (K "")))), |
506 |
proof_delims = [], |
|
45203 | 507 |
known_failures = known_szs_status_failures, |
47976 | 508 |
prem_role = Hypothesis, |
45521 | 509 |
best_slices = |
46407
30e9720cc0b9
optimization: slice caching in case two consecutive slices are nearly identical
blanchet
parents:
46402
diff
changeset
|
510 |
K [(1.0, (false, ((200, format, type_enc, |
30e9720cc0b9
optimization: slice caching in case two consecutive slices are nearly identical
blanchet
parents:
46402
diff
changeset
|
511 |
if is_format_higher_order format then keep_lamsN |
47962
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47955
diff
changeset
|
512 |
else combsN, false), "")))], |
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47955
diff
changeset
|
513 |
best_max_mono_iters = default_max_mono_iters, |
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47955
diff
changeset
|
514 |
best_max_new_mono_instances = default_max_new_mono_instances} |
44590 | 515 |
|
48004
989a34fa72b3
don't generate definitions for LEO-II -- this cuases more harm than good
blanchet
parents:
47985
diff
changeset
|
516 |
val dummy_thf_format = |
48130 | 517 |
THF (Polymorphic, TPTP_Explicit, THF_With_Choice, THF_With_Defs) |
46435 | 518 |
val dummy_thf_config = dummy_config dummy_thf_format "poly_native_higher" |
47646 | 519 |
val dummy_thf = (dummy_thfN, fn () => dummy_thf_config) |
44754 | 520 |
|
48131 | 521 |
val spass_poly_format = DFG Polymorphic |
522 |
val spass_poly_config = dummy_config spass_poly_format "tc_native" |
|
523 |
val spass_poly = (spass_polyN, fn () => spass_poly_config) |
|
41740
4b09f8b9e012
added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents:
41738
diff
changeset
|
524 |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
525 |
(* Remote ATP invocation via SystemOnTPTP *) |
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
526 |
|
38061
685d1f0f75b3
handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents:
38049
diff
changeset
|
527 |
val systems = Synchronized.var "atp_systems" ([] : string list) |
31835 | 528 |
|
529 |
fun get_systems () = |
|
44589
0a1dfc6365e9
first step towards polymorphic TFF + changed defaults for Vampire
blanchet
parents:
44586
diff
changeset
|
530 |
case Isabelle_System.bash_output |
0a1dfc6365e9
first step towards polymorphic TFF + changed defaults for Vampire
blanchet
parents:
44586
diff
changeset
|
531 |
"\"$ISABELLE_ATP/scripts/remote_atp\" -w 2>&1" of |
39491
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39375
diff
changeset
|
532 |
(output, 0) => split_lines output |
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39375
diff
changeset
|
533 |
| (output, _) => |
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39375
diff
changeset
|
534 |
error (case extract_known_failure known_perl_failures output of |
41744 | 535 |
SOME failure => string_for_failure failure |
47499
4b0daca2bf88
redirect bash stderr to Isabelle warning as appropriate -- avoid raw process error output which may either get ignored or overload PIDE syslog in extreme cases;
wenzelm
parents:
47149
diff
changeset
|
536 |
| NONE => trim_line output ^ ".") |
31835 | 537 |
|
42537
25ceb855a18b
improve version handling -- prefer versions of ToFoF, SInE, and SNARK that are known to work
blanchet
parents:
42535
diff
changeset
|
538 |
fun find_system name [] systems = |
25ceb855a18b
improve version handling -- prefer versions of ToFoF, SInE, and SNARK that are known to work
blanchet
parents:
42535
diff
changeset
|
539 |
find_first (String.isPrefix (name ^ "---")) systems |
38690
38a926e033ad
make remote ATP versions more robust, by starting with "preferred" version numbers and falling back on any version
blanchet
parents:
38685
diff
changeset
|
540 |
| find_system name (version :: versions) systems = |
38a926e033ad
make remote ATP versions more robust, by starting with "preferred" version numbers and falling back on any version
blanchet
parents:
38685
diff
changeset
|
541 |
case find_first (String.isPrefix (name ^ "---" ^ version)) systems of |
38a926e033ad
make remote ATP versions more robust, by starting with "preferred" version numbers and falling back on any version
blanchet
parents:
38685
diff
changeset
|
542 |
NONE => find_system name versions systems |
38a926e033ad
make remote ATP versions more robust, by starting with "preferred" version numbers and falling back on any version
blanchet
parents:
38685
diff
changeset
|
543 |
| 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
|
544 |
|
38a926e033ad
make remote ATP versions more robust, by starting with "preferred" version numbers and falling back on any version
blanchet
parents:
38685
diff
changeset
|
545 |
fun get_system name versions = |
38589
b03f8fe043ec
added "max_relevant_per_iter" option to Sledgehammer
blanchet
parents:
38588
diff
changeset
|
546 |
Synchronized.change_result systems |
b03f8fe043ec
added "max_relevant_per_iter" option to Sledgehammer
blanchet
parents:
38588
diff
changeset
|
547 |
(fn systems => (if null systems then get_systems () else systems) |
42955 | 548 |
|> `(`(find_system name versions))) |
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset
|
549 |
|
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
|
550 |
fun the_system name versions = |
38a926e033ad
make remote ATP versions more robust, by starting with "preferred" version numbers and falling back on any version
blanchet
parents:
38685
diff
changeset
|
551 |
case get_system name versions of |
42955 | 552 |
(SOME sys, _) => sys |
46480 | 553 |
| (NONE, []) => error ("SystemOnTPTP is not available.") |
42955 | 554 |
| (NONE, syss) => |
46480 | 555 |
case syss |> filter_out (String.isPrefix "%") |
556 |
|> filter_out (curry (op =) "") of |
|
557 |
[] => error ("SystemOnTPTP is not available.") |
|
558 |
| [msg] => error ("SystemOnTPTP is not available: " ^ msg ^ ".") |
|
559 |
| syss => |
|
560 |
error ("System " ^ quote name ^ " is not available at SystemOnTPTP.\n" ^ |
|
561 |
"(Available systems: " ^ commas_quote syss ^ ".)") |
|
31835 | 562 |
|
41148 | 563 |
val max_remote_secs = 240 (* give Geoff Sutcliffe's servers a break *) |
564 |
||
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
|
565 |
fun remote_config system_name system_versions proof_delims known_failures |
47976 | 566 |
prem_role best_slice : atp_config = |
48376
416e4123baf3
use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents:
48232
diff
changeset
|
567 |
{exec = (["ISABELLE_ATP"], ["scripts/remote_atp"]), |
47074
101976132929
improve "remote_satallax" by exploiting unsat core
blanchet
parents:
47073
diff
changeset
|
568 |
arguments = fn _ => fn _ => fn command => fn timeout => fn _ => |
101976132929
improve "remote_satallax" by exploiting unsat core
blanchet
parents:
47073
diff
changeset
|
569 |
(if command <> "" then "-c " ^ quote command ^ " " else "") ^ |
101976132929
improve "remote_satallax" by exploiting unsat core
blanchet
parents:
47073
diff
changeset
|
570 |
"-s " ^ the_system system_name system_versions ^ " " ^ |
101976132929
improve "remote_satallax" by exploiting unsat core
blanchet
parents:
47073
diff
changeset
|
571 |
"-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout)), |
42962
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42955
diff
changeset
|
572 |
proof_delims = union (op =) tstp_proof_delims proof_delims, |
45203 | 573 |
known_failures = known_failures @ known_perl_failures @ known_says_failures, |
47976 | 574 |
prem_role = prem_role, |
47962
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47955
diff
changeset
|
575 |
best_slices = fn ctxt => [(1.0, (false, best_slice ctxt))], |
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47955
diff
changeset
|
576 |
best_max_mono_iters = default_max_mono_iters, |
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47955
diff
changeset
|
577 |
best_max_new_mono_instances = default_max_new_mono_instances} |
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42332
diff
changeset
|
578 |
|
43500
4c357b7aa710
provide appropriate type system and number of fact defaults for remote ATPs
blanchet
parents:
43497
diff
changeset
|
579 |
fun remotify_config system_name system_versions best_slice |
47976 | 580 |
({proof_delims, known_failures, prem_role, ...} : atp_config) |
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
|
581 |
: atp_config = |
38690
38a926e033ad
make remote ATP versions more robust, by starting with "preferred" version numbers and falling back on any version
blanchet
parents:
38685
diff
changeset
|
582 |
remote_config system_name system_versions proof_delims known_failures |
47976 | 583 |
prem_role best_slice |
38023 | 584 |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
585 |
fun remote_atp name system_name system_versions proof_delims known_failures |
47976 | 586 |
prem_role best_slice = |
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
587 |
(remote_prefix ^ name, |
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
|
588 |
fn () => remote_config system_name system_versions proof_delims |
47976 | 589 |
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
|
590 |
fun remotify_atp (name, config) system_name system_versions best_slice = |
4c357b7aa710
provide appropriate type system and number of fact defaults for remote ATPs
blanchet
parents:
43497
diff
changeset
|
591 |
(remote_prefix ^ name, |
47606
06dde48a1503
true delayed evaluation of "SPASS_VERSION" environment variable
blanchet
parents:
47506
diff
changeset
|
592 |
remotify_config system_name system_versions best_slice o config) |
28592 | 593 |
|
48130 | 594 |
val explicit_tff0 = TFF (Monomorphic, TPTP_Explicit) |
44589
0a1dfc6365e9
first step towards polymorphic TFF + changed defaults for Vampire
blanchet
parents:
44586
diff
changeset
|
595 |
|
43500
4c357b7aa710
provide appropriate type system and number of fact defaults for remote ATPs
blanchet
parents:
43497
diff
changeset
|
596 |
val remote_e = |
4c357b7aa710
provide appropriate type system and number of fact defaults for remote ATPs
blanchet
parents:
43497
diff
changeset
|
597 |
remotify_atp e "EP" ["1.0", "1.1", "1.2"] |
47074
101976132929
improve "remote_satallax" by exploiting unsat core
blanchet
parents:
47073
diff
changeset
|
598 |
(K ((750, FOF, "mono_tags??", combsN, false), "") (* FUDGE *)) |
44099 | 599 |
val remote_leo2 = |
600 |
remotify_atp leo2 "LEO-II" ["1.2.8", "1.2.6"] |
|
47074
101976132929
improve "remote_satallax" by exploiting unsat core
blanchet
parents:
47073
diff
changeset
|
601 |
(K ((100, leo2_thf0, "mono_native_higher", liftingN, false), "") (* FUDGE *)) |
44099 | 602 |
val remote_satallax = |
47074
101976132929
improve "remote_satallax" by exploiting unsat core
blanchet
parents:
47073
diff
changeset
|
603 |
remotify_atp satallax "Satallax" ["2.3", "2.2", "2"] |
47076
f4838ce57772
removed Satallax option, now that this is the default
blanchet
parents:
47074
diff
changeset
|
604 |
(K ((100, 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
|
605 |
val remote_vampire = |
48077 | 606 |
remotify_atp vampire "Vampire" ["2.6", "2.5", "1.8"] |
47074
101976132929
improve "remote_satallax" by exploiting unsat core
blanchet
parents:
47073
diff
changeset
|
607 |
(K ((250, vampire_tff0, "mono_native", combs_or_liftingN, false), "") (* FUDGE *)) |
44423
f74707e12d30
exploit TFF format in Z3 used as ATP, and renamed it "z3_tptp"
blanchet
parents:
44422
diff
changeset
|
608 |
val remote_z3_tptp = |
44754 | 609 |
remotify_atp z3_tptp "Z3" ["3.0"] |
47074
101976132929
improve "remote_satallax" by exploiting unsat core
blanchet
parents:
47073
diff
changeset
|
610 |
(K ((250, z3_tff0, "mono_native", combsN, false), "") (* FUDGE *)) |
44092
bf489e54d7f8
renamed E wrappers for consistency with CASC conventions
blanchet
parents:
43989
diff
changeset
|
611 |
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
|
612 |
remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Conjecture |
47074
101976132929
improve "remote_satallax" by exploiting unsat core
blanchet
parents:
47073
diff
changeset
|
613 |
(K ((500, FOF, "mono_guards??", combsN, false), "") (* FUDGE *)) |
45338 | 614 |
val remote_iprover = |
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
|
615 |
remote_atp iproverN "iProver" [] [] [] Conjecture |
47074
101976132929
improve "remote_satallax" by exploiting unsat core
blanchet
parents:
47073
diff
changeset
|
616 |
(K ((150, FOF, "mono_guards??", liftingN, false), "") (* FUDGE *)) |
45338 | 617 |
val remote_iprover_eq = |
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
|
618 |
remote_atp iprover_eqN "iProver-Eq" [] [] [] Conjecture |
47074
101976132929
improve "remote_satallax" by exploiting unsat core
blanchet
parents:
47073
diff
changeset
|
619 |
(K ((150, FOF, "mono_guards??", liftingN, false), "") (* FUDGE *)) |
41740
4b09f8b9e012
added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents:
41738
diff
changeset
|
620 |
val remote_snark = |
42939 | 621 |
remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"] |
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
|
622 |
[("refutation.", "end_refutation.")] [] Hypothesis |
47074
101976132929
improve "remote_satallax" by exploiting unsat core
blanchet
parents:
47073
diff
changeset
|
623 |
(K ((100, explicit_tff0, "mono_native", liftingN, false), "") (* FUDGE *)) |
44092
bf489e54d7f8
renamed E wrappers for consistency with CASC conventions
blanchet
parents:
43989
diff
changeset
|
624 |
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
|
625 |
remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config) Hypothesis |
47074
101976132929
improve "remote_satallax" by exploiting unsat core
blanchet
parents:
47073
diff
changeset
|
626 |
(K ((150, explicit_tff0, "mono_native", liftingN, false), "") (* FUDGE *)) |
42938 | 627 |
val remote_waldmeister = |
628 |
remote_atp waldmeisterN "Waldmeister" ["710"] |
|
45521 | 629 |
[("#START OF PROOF", "Proved Goals:")] |
630 |
[(OutOfResources, "Too many function symbols"), |
|
47506 | 631 |
(Inappropriate, "**** Unexpected end of file."), |
45521 | 632 |
(Crashed, "Unrecoverable Segmentation Fault")] |
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
|
633 |
Hypothesis |
47898
6213900d6d5f
use raw monomorphic encoding with Waldmeister, to avoid overloading it with too many function symbols (as would be the case using mangled monomorphic encodings)
blanchet
parents:
47787
diff
changeset
|
634 |
(K ((50, CNF_UEQ, "raw_mono_tags??", combsN, false), "") (* FUDGE *)) |
38454
9043eefe8d71
detect old Vampire and give a nicer error message
blanchet
parents:
38433
diff
changeset
|
635 |
|
9043eefe8d71
detect old Vampire and give a nicer error message
blanchet
parents:
38433
diff
changeset
|
636 |
(* Setup *) |
9043eefe8d71
detect old Vampire and give a nicer error message
blanchet
parents:
38433
diff
changeset
|
637 |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
638 |
fun add_atp (name, config) thy = |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
639 |
Data.map (Symtab.update_new (name, (config, stamp ()))) thy |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
640 |
handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".") |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
641 |
|
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
642 |
fun get_atp thy name = |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
643 |
the (Symtab.lookup (Data.get thy) name) |> fst |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
644 |
handle Option.Option => error ("Unknown ATP: " ^ name ^ ".") |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
645 |
|
41727
ab3f6d76fb23
available_provers ~> supported_provers (for clarity)
blanchet
parents:
41725
diff
changeset
|
646 |
val supported_atps = Symtab.keys o Data.get |
36371
8c83ea1a7740
move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents:
36370
diff
changeset
|
647 |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
648 |
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
|
649 |
let val {exec, ...} = get_atp thy name () in |
416e4123baf3
use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents:
48232
diff
changeset
|
650 |
exists (fn var => getenv var <> "") (fst exec) |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
651 |
end |
36371
8c83ea1a7740
move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents:
36370
diff
changeset
|
652 |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
653 |
fun refresh_systems_on_tptp () = |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
654 |
Synchronized.change systems (fn _ => get_systems ()) |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
655 |
|
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
|
656 |
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
|
657 |
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
|
658 |
if ord = smartN then |
48005
eeede26f2721
killed SPASS 3.5/3.7 FLOTTER hack -- requires users to upgrade to SPASS 3.8
blanchet
parents:
48004
diff
changeset
|
659 |
if atp = spassN then |
47073
c73f7b0c7ebc
generate weights and precedences for predicates as well
blanchet
parents:
47055
diff
changeset
|
660 |
{is_lpo = false, gen_weights = true, gen_prec = true, gen_simp = false} |
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
|
661 |
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
|
662 |
{is_lpo = false, gen_weights = false, gen_prec = false, |
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
|
663 |
gen_simp = false} |
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
|
664 |
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
|
665 |
let val is_lpo = String.isSubstring lpoN ord 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
|
666 |
{is_lpo = is_lpo, |
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
|
667 |
gen_weights = not is_lpo andalso String.isSubstring xweightsN ord, |
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
|
668 |
gen_prec = String.isSubstring xprecN ord, |
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
|
669 |
gen_simp = String.isSubstring xsimpN ord} |
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
|
670 |
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
|
671 |
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
|
672 |
|
47606
06dde48a1503
true delayed evaluation of "SPASS_VERSION" environment variable
blanchet
parents:
47506
diff
changeset
|
673 |
val atps= |
48131 | 674 |
[alt_ergo, e, leo2, satallax, spass, spass_poly, vampire, z3_tptp, dummy_thf, |
675 |
remote_e, remote_e_sine, remote_e_tofof, remote_iprover, remote_iprover_eq, |
|
47949 | 676 |
remote_leo2, remote_satallax, remote_vampire, remote_z3_tptp, remote_snark, |
677 |
remote_waldmeister] |
|
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
|
678 |
|
47606
06dde48a1503
true delayed evaluation of "SPASS_VERSION" environment variable
blanchet
parents:
47506
diff
changeset
|
679 |
val setup = fold add_atp atps |
35867 | 680 |
|
28592 | 681 |
end; |