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