author | blanchet |
Tue, 02 Aug 2022 13:23:57 +0200 | |
changeset 75718 | 3557f826362c |
parent 75465 | d9b23902692d |
child 75872 | 8bfad7bc74cb |
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 |
||
72400 | 8 |
signature SLEDGEHAMMER_ATP_SYSTEMS = |
28592 | 9 |
sig |
45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
45300
diff
changeset
|
10 |
type atp_format = ATP_Problem.atp_format |
53586
bd5fa6425993
prefixed types and some functions with "atp_" for disambiguation
blanchet
parents:
53515
diff
changeset
|
11 |
type atp_formula_role = ATP_Problem.atp_formula_role |
bd5fa6425993
prefixed types and some functions with "atp_" for disambiguation
blanchet
parents:
53515
diff
changeset
|
12 |
type atp_failure = ATP_Proof.atp_failure |
38023 | 13 |
|
75339
d9bb81999d2c
first step in making time slicing more flexible in Sledgehammer: label slices with 'slice size'
blanchet
parents:
75059
diff
changeset
|
14 |
type base_slice = int * int * string |
75026 | 15 |
type atp_slice = atp_format * string * string * bool * string |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
16 |
type atp_config = |
73374 | 17 |
{exec : string list * string list, |
75341 | 18 |
arguments : Proof.context -> bool -> string -> Time.time -> Path.T -> string list, |
42578
1eaf4d437d4c
define type system in ATP module so that ATPs can suggest a type system
blanchet
parents:
42577
diff
changeset
|
19 |
proof_delims : (string * string) list, |
53586
bd5fa6425993
prefixed types and some functions with "atp_" for disambiguation
blanchet
parents:
53515
diff
changeset
|
20 |
known_failures : (atp_failure * string) list, |
bd5fa6425993
prefixed types and some functions with "atp_" for disambiguation
blanchet
parents:
53515
diff
changeset
|
21 |
prem_role : atp_formula_role, |
75026 | 22 |
good_slices : Proof.context -> (base_slice * atp_slice) list, |
23 |
good_max_mono_iters : int, |
|
24 |
good_max_new_mono_instances : int} |
|
38023 | 25 |
|
47962
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47955
diff
changeset
|
26 |
val default_max_mono_iters : int |
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47955
diff
changeset
|
27 |
val default_max_new_mono_instances : int |
50950 | 28 |
val spass_H1SOS : string |
29 |
val spass_H2 : string |
|
30 |
val spass_H2LR0LT0 : string |
|
31 |
val spass_H2NuVS0 : string |
|
32 |
val spass_H2NuVS0Red2 : string |
|
33 |
val spass_H2SOS : string |
|
73435
1cc848548f21
invoke remote ATP via SystemOnTPTP.run_systems from Isabelle/Scala (without perl);
wenzelm
parents:
73432
diff
changeset
|
34 |
val isabelle_scala_function: string list * string list |
57671
dc5e1b1db9ba
avoid 'eproof' and 'eproof_ram' scripts if possible (i.e. if 'eprover' can produce reasonable enough proofs for one-liner reconstruction)
blanchet
parents:
57636
diff
changeset
|
35 |
val remote_atp : string -> string -> string list -> (string * string) list -> |
75026 | 36 |
(atp_failure * string) list -> atp_formula_role -> (Proof.context -> base_slice * atp_slice) -> |
57671
dc5e1b1db9ba
avoid 'eproof' and 'eproof_ram' scripts if possible (i.e. if 'eprover' can produce reasonable enough proofs for one-liner reconstruction)
blanchet
parents:
57636
diff
changeset
|
37 |
string * (unit -> atp_config) |
47606
06dde48a1503
true delayed evaluation of "SPASS_VERSION" environment variable
blanchet
parents:
47506
diff
changeset
|
38 |
val add_atp : string * (unit -> atp_config) -> theory -> theory |
06dde48a1503
true delayed evaluation of "SPASS_VERSION" environment variable
blanchet
parents:
47506
diff
changeset
|
39 |
val get_atp : theory -> string -> (unit -> atp_config) |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
40 |
val is_atp_installed : theory -> string -> bool |
35867 | 41 |
val refresh_systems_on_tptp : unit -> unit |
75036 | 42 |
val local_atps : string list |
43 |
val remote_atps : string list |
|
75465
d9b23902692d
excluded dummy ATPs from Sledgehammer's default provers
desharna
parents:
75433
diff
changeset
|
44 |
val dummy_atps : string list |
d9b23902692d
excluded dummy ATPs from Sledgehammer's default provers
desharna
parents:
75433
diff
changeset
|
45 |
val non_dummy_atps : string list |
d9b23902692d
excluded dummy ATPs from Sledgehammer's default provers
desharna
parents:
75433
diff
changeset
|
46 |
val all_atps : string list |
28592 | 47 |
end; |
48 |
||
72400 | 49 |
structure Sledgehammer_ATP_Systems : SLEDGEHAMMER_ATP_SYSTEMS = |
28592 | 50 |
struct |
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
51 |
|
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
|
52 |
open ATP_Problem |
39491
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39375
diff
changeset
|
53 |
open ATP_Proof |
46320 | 54 |
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
|
55 |
|
52073
ccb292952774
started adding agsyHOL as an experimental prover
blanchet
parents:
51998
diff
changeset
|
56 |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
57 |
(* ATP configuration *) |
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset
|
58 |
|
74890 | 59 |
val TF0 = TFF (Monomorphic, Without_FOOL) |
60 |
val TF1 = TFF (Polymorphic, Without_FOOL) |
|
61 |
val TX0 = TFF (Monomorphic, With_FOOL {with_ite = true, with_let = true}) |
|
62 |
val TX1 = TFF (Polymorphic, With_FOOL {with_ite = true, with_let = true}) |
|
63 |
val TH0 = THF (Monomorphic, {with_ite = true, with_let = true}, THF_With_Choice) |
|
74895
b605ebd87a47
proper polymorphism for TH1 format in Sledgehammer
desharna
parents:
74894
diff
changeset
|
64 |
val TH1 = THF (Polymorphic, {with_ite = true, with_let = true}, THF_With_Choice) |
74890 | 65 |
|
47962
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47955
diff
changeset
|
66 |
val default_max_mono_iters = 3 (* FUDGE *) |
53515
f5b678b155f6
adjusted number of generated monomorphic instances for new monomorphizer based on new evaluation (E, SPASS, Vampire)
blanchet
parents:
53225
diff
changeset
|
67 |
val default_max_new_mono_instances = 100 (* FUDGE *) |
47962
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47955
diff
changeset
|
68 |
|
75339
d9bb81999d2c
first step in making time slicing more flexible in Sledgehammer: label slices with 'slice size'
blanchet
parents:
75059
diff
changeset
|
69 |
(* desired slice size, desired number of facts, fact filter *) |
d9bb81999d2c
first step in making time slicing more flexible in Sledgehammer: label slices with 'slice size'
blanchet
parents:
75059
diff
changeset
|
70 |
type base_slice = int * int * string |
d9bb81999d2c
first step in making time slicing more flexible in Sledgehammer: label slices with 'slice size'
blanchet
parents:
75059
diff
changeset
|
71 |
|
75340
e1aa703c8cce
second and last step in making time slicing more flexible in Sledgehammer: try to honor desired slice size
blanchet
parents:
75339
diff
changeset
|
72 |
(* problem file format, type encoding, lambda translation scheme, uncurried aliases?, |
e1aa703c8cce
second and last step in making time slicing more flexible in Sledgehammer: try to honor desired slice size
blanchet
parents:
75339
diff
changeset
|
73 |
prover-specific extra information *) |
75026 | 74 |
type atp_slice = atp_format * string * string * bool * string |
46409
d4754183ccce
made option available to users (mostly for experiments)
blanchet
parents:
46407
diff
changeset
|
75 |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
76 |
type atp_config = |
73374 | 77 |
{exec : string list * string list, |
75341 | 78 |
arguments : Proof.context -> bool -> string -> Time.time -> Path.T -> string list, |
42578
1eaf4d437d4c
define type system in ATP module so that ATPs can suggest a type system
blanchet
parents:
42577
diff
changeset
|
79 |
proof_delims : (string * string) list, |
53586
bd5fa6425993
prefixed types and some functions with "atp_" for disambiguation
blanchet
parents:
53515
diff
changeset
|
80 |
known_failures : (atp_failure * string) list, |
bd5fa6425993
prefixed types and some functions with "atp_" for disambiguation
blanchet
parents:
53515
diff
changeset
|
81 |
prem_role : atp_formula_role, |
75026 | 82 |
good_slices : Proof.context -> (base_slice * atp_slice) list, |
83 |
good_max_mono_iters : int, |
|
84 |
good_max_new_mono_instances : int} |
|
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
85 |
|
75339
d9bb81999d2c
first step in making time slicing more flexible in Sledgehammer: label slices with 'slice size'
blanchet
parents:
75059
diff
changeset
|
86 |
(* "good_slices" must be found empirically, ideally taking a holistic approach since the ATPs are |
d9bb81999d2c
first step in making time slicing more flexible in Sledgehammer: label slices with 'slice size'
blanchet
parents:
75059
diff
changeset
|
87 |
run in parallel. *) |
42710
84fcce345b5d
further improved type system setup based on Judgment Days
blanchet
parents:
42709
diff
changeset
|
88 |
|
51011 | 89 |
val mepoN = "mepo" |
90 |
val mashN = "mash" |
|
91 |
val meshN = "mesh" |
|
92 |
||
52073
ccb292952774
started adding agsyHOL as an experimental prover
blanchet
parents:
51998
diff
changeset
|
93 |
val tstp_proof_delims = |
ccb292952774
started adding agsyHOL as an experimental prover
blanchet
parents:
51998
diff
changeset
|
94 |
[("% SZS output start CNFRefutation", "% SZS output end CNFRefutation"), |
ccb292952774
started adding agsyHOL as an experimental prover
blanchet
parents:
51998
diff
changeset
|
95 |
("% SZS output start Refutation", "% SZS output end Refutation"), |
ccb292952774
started adding agsyHOL as an experimental prover
blanchet
parents:
51998
diff
changeset
|
96 |
("% SZS output start Proof", "% SZS output end Proof")] |
ccb292952774
started adding agsyHOL as an experimental prover
blanchet
parents:
51998
diff
changeset
|
97 |
|
45203 | 98 |
fun known_szs_failures wrap = |
99 |
[(Unprovable, wrap "CounterSatisfiable"), |
|
100 |
(Unprovable, wrap "Satisfiable"), |
|
101 |
(GaveUp, wrap "GaveUp"), |
|
102 |
(GaveUp, wrap "Unknown"), |
|
103 |
(GaveUp, wrap "Incomplete"), |
|
104 |
(ProofMissing, wrap "Theorem"), |
|
105 |
(ProofMissing, wrap "Unsatisfiable"), |
|
106 |
(TimedOut, wrap "Timeout"), |
|
107 |
(Inappropriate, wrap "Inappropriate"), |
|
108 |
(OutOfResources, wrap "ResourceOut"), |
|
109 |
(OutOfResources, wrap "MemoryOut"), |
|
110 |
(Interrupted, wrap "Forced"), |
|
111 |
(Interrupted, wrap "User")] |
|
112 |
||
113 |
val known_szs_status_failures = known_szs_failures (prefix "SZS status ") |
|
114 |
val known_says_failures = known_szs_failures (prefix " says ") |
|
115 |
||
38023 | 116 |
structure Data = Theory_Data |
117 |
( |
|
47606
06dde48a1503
true delayed evaluation of "SPASS_VERSION" environment variable
blanchet
parents:
47506
diff
changeset
|
118 |
type T = ((unit -> atp_config) * stamp) Symtab.table |
38023 | 119 |
val empty = Symtab.empty |
46407
30e9720cc0b9
optimization: slice caching in case two consecutive slices are nearly identical
blanchet
parents:
46402
diff
changeset
|
120 |
fun merge data : T = |
30e9720cc0b9
optimization: slice caching in case two consecutive slices are nearly identical
blanchet
parents:
46402
diff
changeset
|
121 |
Symtab.merge (eq_snd (op =)) data |
63692 | 122 |
handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name) |
38023 | 123 |
) |
38017
3ad3e3ca2451
move Sledgehammer-specific code out of "Sledgehammer_TPTP_Format"
blanchet
parents:
38015
diff
changeset
|
124 |
|
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
|
125 |
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
|
126 |
|
43473
fb2713b803e6
deal with ATP time slices in a more flexible/robust fashion
blanchet
parents:
43467
diff
changeset
|
127 |
val sosN = "sos" |
fb2713b803e6
deal with ATP time slices in a more flexible/robust fashion
blanchet
parents:
43467
diff
changeset
|
128 |
val no_sosN = "no_sos" |
fb2713b803e6
deal with ATP time slices in a more flexible/robust fashion
blanchet
parents:
43467
diff
changeset
|
129 |
|
47032 | 130 |
|
52073
ccb292952774
started adding agsyHOL as an experimental prover
blanchet
parents:
51998
diff
changeset
|
131 |
(* agsyHOL *) |
ccb292952774
started adding agsyHOL as an experimental prover
blanchet
parents:
51998
diff
changeset
|
132 |
|
ccb292952774
started adding agsyHOL as an experimental prover
blanchet
parents:
51998
diff
changeset
|
133 |
val agsyhol_config : atp_config = |
73374 | 134 |
{exec = (["AGSYHOL_HOME"], ["agsyHOL"]), |
75341 | 135 |
arguments = fn _ => fn _ => fn _ => fn timeout => fn problem => |
73568
bdba138d462d
clarified signature: more structured arguments, notably for remote provers;
wenzelm
parents:
73437
diff
changeset
|
136 |
["--proof --time-out " ^ string_of_int (to_secs 1 timeout) ^ " " ^ File.bash_path problem], |
52073
ccb292952774
started adding agsyHOL as an experimental prover
blanchet
parents:
51998
diff
changeset
|
137 |
proof_delims = tstp_proof_delims, |
ccb292952774
started adding agsyHOL as an experimental prover
blanchet
parents:
51998
diff
changeset
|
138 |
known_failures = known_szs_status_failures, |
ccb292952774
started adding agsyHOL as an experimental prover
blanchet
parents:
51998
diff
changeset
|
139 |
prem_role = Hypothesis, |
75026 | 140 |
good_slices = |
52073
ccb292952774
started adding agsyHOL as an experimental prover
blanchet
parents:
51998
diff
changeset
|
141 |
(* FUDGE *) |
75339
d9bb81999d2c
first step in making time slicing more flexible in Sledgehammer: label slices with 'slice size'
blanchet
parents:
75059
diff
changeset
|
142 |
K [((1, 60, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, ""))], |
75026 | 143 |
good_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *), |
144 |
good_max_new_mono_instances = default_max_new_mono_instances} |
|
52073
ccb292952774
started adding agsyHOL as an experimental prover
blanchet
parents:
51998
diff
changeset
|
145 |
|
ccb292952774
started adding agsyHOL as an experimental prover
blanchet
parents:
51998
diff
changeset
|
146 |
val agsyhol = (agsyholN, fn () => agsyhol_config) |
ccb292952774
started adding agsyHOL as an experimental prover
blanchet
parents:
51998
diff
changeset
|
147 |
|
ccb292952774
started adding agsyHOL as an experimental prover
blanchet
parents:
51998
diff
changeset
|
148 |
|
46643
a88bccd2b567
added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46481
diff
changeset
|
149 |
(* Alt-Ergo *) |
a88bccd2b567
added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46481
diff
changeset
|
150 |
|
a88bccd2b567
added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46481
diff
changeset
|
151 |
val alt_ergo_config : atp_config = |
73374 | 152 |
{exec = (["WHY3_HOME"], ["why3"]), |
75341 | 153 |
arguments = fn _ => fn _ => fn _ => fn timeout => fn problem => |
73568
bdba138d462d
clarified signature: more structured arguments, notably for remote provers;
wenzelm
parents:
73437
diff
changeset
|
154 |
["--format tptp --prover 'Alt-Ergo,0.95.2,' --timelimit " ^ string_of_int (to_secs 1 timeout) ^ |
bdba138d462d
clarified signature: more structured arguments, notably for remote provers;
wenzelm
parents:
73437
diff
changeset
|
155 |
" " ^ File.bash_path problem], |
46643
a88bccd2b567
added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46481
diff
changeset
|
156 |
proof_delims = [], |
a88bccd2b567
added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46481
diff
changeset
|
157 |
known_failures = |
a88bccd2b567
added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46481
diff
changeset
|
158 |
[(ProofMissing, ": Valid"), |
a88bccd2b567
added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46481
diff
changeset
|
159 |
(TimedOut, ": Timeout"), |
a88bccd2b567
added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46481
diff
changeset
|
160 |
(GaveUp, ": Unknown")], |
47976 | 161 |
prem_role = Hypothesis, |
75026 | 162 |
good_slices = |
46643
a88bccd2b567
added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46481
diff
changeset
|
163 |
(* FUDGE *) |
75339
d9bb81999d2c
first step in making time slicing more flexible in Sledgehammer: label slices with 'slice size'
blanchet
parents:
75059
diff
changeset
|
164 |
K [((1000 (* infinity *), 100, meshN), (TF1, "poly_native", liftingN, false, ""))], |
75026 | 165 |
good_max_mono_iters = default_max_mono_iters, |
166 |
good_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
|
167 |
|
47646 | 168 |
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
|
169 |
|
a88bccd2b567
added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46481
diff
changeset
|
170 |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
171 |
(* E *) |
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
172 |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
173 |
val e_config : atp_config = |
73973 | 174 |
{exec = (["E_HOME"], ["eprover-ho", "eprover"]), |
75342 | 175 |
arguments = fn _ => fn _ => fn extra_options => fn timeout => fn problem => |
75413
9c0300345e17
enable an E option suggested by Petar Vukmirovic
blanchet
parents:
75370
diff
changeset
|
176 |
["--tstp-in --tstp-out --silent " ^ extra_options ^ |
75433 | 177 |
" --cpu-limit=" ^ string_of_int (to_secs 2 timeout) ^ " --proof-object=1 " ^ |
178 |
File.bash_path problem], |
|
52073
ccb292952774
started adding agsyHOL as an experimental prover
blanchet
parents:
51998
diff
changeset
|
179 |
proof_delims = |
ccb292952774
started adding agsyHOL as an experimental prover
blanchet
parents:
51998
diff
changeset
|
180 |
[("# SZS output start CNFRefutation", "# SZS output end CNFRefutation")] @ |
ccb292952774
started adding agsyHOL as an experimental prover
blanchet
parents:
51998
diff
changeset
|
181 |
tstp_proof_delims, |
36265
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset
|
182 |
known_failures = |
45203 | 183 |
[(TimedOut, "Failure: Resource limit exceeded (time)"), |
47972 | 184 |
(TimedOut, "time limit exceeded")] @ |
185 |
known_szs_status_failures, |
|
47976 | 186 |
prem_role = Conjecture, |
75029 | 187 |
good_slices = |
70939
3218999b3715
folded experimental Ehoh into E now that E 2.3 has been released
blanchet
parents:
70938
diff
changeset
|
188 |
let |
75342 | 189 |
val (format, type_enc, lam_trans, extra_options) = |
73974 | 190 |
if string_ord (getenv "E_VERSION", "2.7") <> LESS then |
75433 | 191 |
(THF (Monomorphic, {with_ite = true, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, "--auto-schedule=4 --serialize-schedule=true --demod-under-lambda=true") |
73974 | 192 |
else if string_ord (getenv "E_VERSION", "2.6") <> LESS then |
75342 | 193 |
(THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, "--auto-schedule") |
72588 | 194 |
else |
75342 | 195 |
(THF (Monomorphic, {with_ite = false, with_let = false}, THF_Lambda_Free), "mono_native_higher", combsN, "--auto-schedule") |
70939
3218999b3715
folded experimental Ehoh into E now that E 2.3 has been released
blanchet
parents:
70938
diff
changeset
|
196 |
in |
43474
423cd1ecf714
optimized E's time slicing, based on latest exhaustive Judgment Day results
blanchet
parents:
43473
diff
changeset
|
197 |
(* FUDGE *) |
75369 | 198 |
K [((1000 (* infinity *), 512, meshN), (format, type_enc, lam_trans, false, extra_options)), |
199 |
((1000 (* infinity *), 1024, meshN), (format, type_enc, lam_trans, false, extra_options)), |
|
75342 | 200 |
((1000 (* infinity *), 128, mepoN), (format, type_enc, lam_trans, false, extra_options)), |
201 |
((1000 (* infinity *), 724, meshN), (TF0, "poly_guards??", lam_trans, false, extra_options)), |
|
202 |
((1000 (* infinity *), 256, mepoN), (format, type_enc, liftingN, false, extra_options)), |
|
203 |
((1000 (* infinity *), 64, mashN), (format, type_enc, combsN, false, extra_options))] |
|
47962
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47955
diff
changeset
|
204 |
end, |
75026 | 205 |
good_max_mono_iters = default_max_mono_iters, |
206 |
good_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
|
207 |
|
47646 | 208 |
val e = (eN, fn () => e_config) |
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
209 |
|
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
210 |
|
48700 | 211 |
(* iProver *) |
212 |
||
213 |
val iprover_config : atp_config = |
|
73374 | 214 |
{exec = (["IPROVER_HOME"], ["iproveropt", "iprover"]), |
75341 | 215 |
arguments = fn _ => fn _ => fn _ => fn timeout => fn problem => |
74350 | 216 |
["--clausifier \"$VAMPIRE_HOME\"/vampire " ^ |
74046
462d652ad910
use Vampire's clausifier with iProver, now that E's is no longer supported
blanchet
parents:
74005
diff
changeset
|
217 |
"--clausifier_options \"--mode clausify\" " ^ |
73568
bdba138d462d
clarified signature: more structured arguments, notably for remote provers;
wenzelm
parents:
73437
diff
changeset
|
218 |
"--time_out_real " ^ string_of_real (Time.toReal timeout) ^ " " ^ File.bash_path problem], |
48700 | 219 |
proof_delims = tstp_proof_delims, |
220 |
known_failures = |
|
221 |
[(ProofIncomplete, "% SZS output start CNFRefutation")] @ |
|
222 |
known_szs_status_failures, |
|
223 |
prem_role = Hypothesis, |
|
75026 | 224 |
good_slices = |
48700 | 225 |
(* FUDGE *) |
75339
d9bb81999d2c
first step in making time slicing more flexible in Sledgehammer: label slices with 'slice size'
blanchet
parents:
75059
diff
changeset
|
226 |
K [((1, 32, meshN), (TF0, "mono_native", liftingN, false, "")), |
d9bb81999d2c
first step in making time slicing more flexible in Sledgehammer: label slices with 'slice size'
blanchet
parents:
75059
diff
changeset
|
227 |
((1, 512, meshN), (TX0, "mono_native", liftingN, false, "")), |
d9bb81999d2c
first step in making time slicing more flexible in Sledgehammer: label slices with 'slice size'
blanchet
parents:
75059
diff
changeset
|
228 |
((1, 128, mashN), (TF0, "mono_native", combsN, false, "")), |
d9bb81999d2c
first step in making time slicing more flexible in Sledgehammer: label slices with 'slice size'
blanchet
parents:
75059
diff
changeset
|
229 |
((1, 1024, meshN), (TF0, "mono_native", liftingN, false, "")), |
d9bb81999d2c
first step in making time slicing more flexible in Sledgehammer: label slices with 'slice size'
blanchet
parents:
75059
diff
changeset
|
230 |
((1, 256, mepoN), (TF0, "mono_native", combsN, false, ""))], |
75026 | 231 |
good_max_mono_iters = default_max_mono_iters, |
232 |
good_max_new_mono_instances = default_max_new_mono_instances} |
|
48700 | 233 |
|
234 |
val iprover = (iproverN, fn () => iprover_config) |
|
235 |
||
236 |
||
44099 | 237 |
(* LEO-II *) |
238 |
||
239 |
val leo2_config : atp_config = |
|
73374 | 240 |
{exec = (["LEO2_HOME"], ["leo.opt", "leo"]), |
75341 | 241 |
arguments = fn _ => fn full_proofs => fn _ => fn timeout => fn problem => |
73568
bdba138d462d
clarified signature: more structured arguments, notably for remote provers;
wenzelm
parents:
73437
diff
changeset
|
242 |
["--foatp e --atp e=\"$E_HOME\"/eprover \ |
bdba138d462d
clarified signature: more structured arguments, notably for remote provers;
wenzelm
parents:
73437
diff
changeset
|
243 |
\--atp epclextract=\"$E_HOME\"/epclextract \ |
bdba138d462d
clarified signature: more structured arguments, notably for remote provers;
wenzelm
parents:
73437
diff
changeset
|
244 |
\--proofoutput 1 --timeout " ^ string_of_int (to_secs 1 timeout) ^ " " ^ |
bdba138d462d
clarified signature: more structured arguments, notably for remote provers;
wenzelm
parents:
73437
diff
changeset
|
245 |
(if full_proofs then "--notReplLeibnizEQ --notReplAndrewsEQ --notUseExtCnfCmbd " else "") ^ |
bdba138d462d
clarified signature: more structured arguments, notably for remote provers;
wenzelm
parents:
73437
diff
changeset
|
246 |
File.bash_path problem], |
44099 | 247 |
proof_delims = tstp_proof_delims, |
45207 | 248 |
known_failures = |
47974
08d2dcc2dab9
improved LEO-II definition handling -- still hoping for a fix directly in LEO-II
blanchet
parents:
47972
diff
changeset
|
249 |
[(TimedOut, "CPU time limit exceeded, terminating"), |
47972 | 250 |
(GaveUp, "No.of.Axioms")] @ |
251 |
known_szs_status_failures, |
|
47976 | 252 |
prem_role = Hypothesis, |
75026 | 253 |
good_slices = |
44099 | 254 |
(* FUDGE *) |
75339
d9bb81999d2c
first step in making time slicing more flexible in Sledgehammer: label slices with 'slice size'
blanchet
parents:
75059
diff
changeset
|
255 |
K [((1, 40, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, ""))], |
75026 | 256 |
good_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *), |
257 |
good_max_new_mono_instances = default_max_new_mono_instances} |
|
39491
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39375
diff
changeset
|
258 |
|
47646 | 259 |
val leo2 = (leo2N, fn () => leo2_config) |
44099 | 260 |
|
261 |
||
67021
41f1f8c4259b
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
blanchet
parents:
66544
diff
changeset
|
262 |
(* Leo-III *) |
41f1f8c4259b
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
blanchet
parents:
66544
diff
changeset
|
263 |
|
69717 | 264 |
(* Include choice? Disabled now since it's disabled for Satallax as well. *) |
67021
41f1f8c4259b
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
blanchet
parents:
66544
diff
changeset
|
265 |
val leo3_config : atp_config = |
73374 | 266 |
{exec = (["LEO3_HOME"], ["leo3"]), |
75341 | 267 |
arguments = fn _ => fn full_proofs => fn _ => fn timeout => fn problem => |
73568
bdba138d462d
clarified signature: more structured arguments, notably for remote provers;
wenzelm
parents:
73437
diff
changeset
|
268 |
[File.bash_path problem ^ " " ^ "--atp cvc=\"$CVC4_SOLVER\" --atp e=\"$E_HOME\"/eprover \ |
bdba138d462d
clarified signature: more structured arguments, notably for remote provers;
wenzelm
parents:
73437
diff
changeset
|
269 |
\-p -t " ^ string_of_int (to_secs 1 timeout) ^ " " ^ |
bdba138d462d
clarified signature: more structured arguments, notably for remote provers;
wenzelm
parents:
73437
diff
changeset
|
270 |
(if full_proofs then "--nleq --naeq " else "")], |
67021
41f1f8c4259b
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
blanchet
parents:
66544
diff
changeset
|
271 |
proof_delims = tstp_proof_delims, |
41f1f8c4259b
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
blanchet
parents:
66544
diff
changeset
|
272 |
known_failures = known_szs_status_failures, |
41f1f8c4259b
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
blanchet
parents:
66544
diff
changeset
|
273 |
prem_role = Hypothesis, |
75026 | 274 |
good_slices = |
67021
41f1f8c4259b
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
blanchet
parents:
66544
diff
changeset
|
275 |
(* FUDGE *) |
75339
d9bb81999d2c
first step in making time slicing more flexible in Sledgehammer: label slices with 'slice size'
blanchet
parents:
75059
diff
changeset
|
276 |
K [((3, 512, meshN), (TH0, "mono_native_higher", keep_lamsN, false, "")), |
d9bb81999d2c
first step in making time slicing more flexible in Sledgehammer: label slices with 'slice size'
blanchet
parents:
75059
diff
changeset
|
277 |
((3, 512, meshN), (TF0, "mono_native", liftingN, false, ""))], |
75026 | 278 |
good_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *), |
279 |
good_max_new_mono_instances = default_max_new_mono_instances} |
|
67021
41f1f8c4259b
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
blanchet
parents:
66544
diff
changeset
|
280 |
|
41f1f8c4259b
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
blanchet
parents:
66544
diff
changeset
|
281 |
val leo3 = (leo3N, fn () => leo3_config) |
41f1f8c4259b
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
blanchet
parents:
66544
diff
changeset
|
282 |
|
41f1f8c4259b
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
blanchet
parents:
66544
diff
changeset
|
283 |
|
44099 | 284 |
(* Satallax *) |
285 |
||
52097 | 286 |
(* Choice is disabled until there is proper reconstruction for it. *) |
44099 | 287 |
val satallax_config : atp_config = |
73374 | 288 |
{exec = (["SATALLAX_HOME"], ["satallax.opt", "satallax"]), |
75341 | 289 |
arguments = fn _ => fn _ => fn _ => fn timeout => fn problem => |
73568
bdba138d462d
clarified signature: more structured arguments, notably for remote provers;
wenzelm
parents:
73437
diff
changeset
|
290 |
[(case getenv "E_HOME" of |
bdba138d462d
clarified signature: more structured arguments, notably for remote provers;
wenzelm
parents:
73437
diff
changeset
|
291 |
"" => "" |
bdba138d462d
clarified signature: more structured arguments, notably for remote provers;
wenzelm
parents:
73437
diff
changeset
|
292 |
| home => "-E " ^ home ^ "/eprover ") ^ |
bdba138d462d
clarified signature: more structured arguments, notably for remote provers;
wenzelm
parents:
73437
diff
changeset
|
293 |
"-p tstp -t " ^ string_of_int (to_secs 1 timeout) ^ " " ^ File.bash_path problem], |
45162 | 294 |
proof_delims = |
57707
0242e9578828
imported patch satallax_proof_support_Sledgehammer
fleury
parents:
57672
diff
changeset
|
295 |
[("% SZS output start Proof", "% SZS output end Proof")], |
45203 | 296 |
known_failures = known_szs_status_failures, |
47981 | 297 |
prem_role = Hypothesis, |
75026 | 298 |
good_slices = |
44754 | 299 |
(* FUDGE *) |
75339
d9bb81999d2c
first step in making time slicing more flexible in Sledgehammer: label slices with 'slice size'
blanchet
parents:
75059
diff
changeset
|
300 |
K [((6, 256, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, ""))], |
75026 | 301 |
good_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *), |
302 |
good_max_new_mono_instances = default_max_new_mono_instances} |
|
44099 | 303 |
|
47646 | 304 |
val satallax = (satallaxN, fn () => satallax_config) |
44099 | 305 |
|
306 |
||
307 |
(* 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
|
308 |
|
48005
eeede26f2721
killed SPASS 3.5/3.7 FLOTTER hack -- requires users to upgrade to SPASS 3.8
blanchet
parents:
48004
diff
changeset
|
309 |
val spass_H1SOS = "-Heuristic=1 -SOS" |
50333
20c69b00e73c
tweak SPASS default a tiny bit, so that a more interesting heuristic is chosen when "slicing=false" (for experiments)
blanchet
parents:
49991
diff
changeset
|
310 |
val spass_H2 = "-Heuristic=2" |
48005
eeede26f2721
killed SPASS 3.5/3.7 FLOTTER hack -- requires users to upgrade to SPASS 3.8
blanchet
parents:
48004
diff
changeset
|
311 |
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
|
312 |
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
|
313 |
val spass_H2NuVS0Red2 = "-Heuristic=2 -RNuV=1 -Sorts=0 -RFRew=2 -RBRew=2 -RTaut=2" |
50333
20c69b00e73c
tweak SPASS default a tiny bit, so that a more interesting heuristic is chosen when "slicing=false" (for experiments)
blanchet
parents:
49991
diff
changeset
|
314 |
val spass_H2SOS = "-Heuristic=2 -SOS" |
47055
16e2633f3b4b
made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
blanchet
parents:
47053
diff
changeset
|
315 |
|
48005
eeede26f2721
killed SPASS 3.5/3.7 FLOTTER hack -- requires users to upgrade to SPASS 3.8
blanchet
parents:
48004
diff
changeset
|
316 |
val spass_config : atp_config = |
73375 | 317 |
let |
318 |
val format = DFG Monomorphic |
|
319 |
in |
|
320 |
{exec = (["SPASS_HOME"], ["SPASS"]), |
|
75341 | 321 |
arguments = fn _ => fn full_proofs => fn extra_options => fn timeout => fn problem => |
73568
bdba138d462d
clarified signature: more structured arguments, notably for remote provers;
wenzelm
parents:
73437
diff
changeset
|
322 |
["-Isabelle=1 " ^ (if full_proofs then "-CNFRenaming=0 -Splits=0 " else "") ^ |
bdba138d462d
clarified signature: more structured arguments, notably for remote provers;
wenzelm
parents:
73437
diff
changeset
|
323 |
"-TimeLimit=" ^ string_of_int (to_secs 1 timeout) ^ " " ^ File.bash_path problem |
bdba138d462d
clarified signature: more structured arguments, notably for remote provers;
wenzelm
parents:
73437
diff
changeset
|
324 |
|> extra_options <> "" ? prefix (extra_options ^ " ")], |
73375 | 325 |
proof_delims = [("Here is a proof", "Formulae used in the proof")], |
326 |
known_failures = |
|
327 |
[(GaveUp, "SPASS beiseite: Completion found"), |
|
328 |
(TimedOut, "SPASS beiseite: Ran out of time"), |
|
329 |
(OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"), |
|
330 |
(MalformedInput, "Undefined symbol"), |
|
331 |
(MalformedInput, "Free Variable"), |
|
332 |
(Unprovable, "No formulae and clauses found in input file"), |
|
73436
e92f2e44e4d8
removed spurious references to perl / libwww-perl;
wenzelm
parents:
73435
diff
changeset
|
333 |
(InternalError, "Please report this error")], |
73375 | 334 |
prem_role = Conjecture, |
75026 | 335 |
good_slices = |
73375 | 336 |
(* FUDGE *) |
75339
d9bb81999d2c
first step in making time slicing more flexible in Sledgehammer: label slices with 'slice size'
blanchet
parents:
75059
diff
changeset
|
337 |
K [((1, 150, meshN), (format, "mono_native", combsN, true, "")), |
d9bb81999d2c
first step in making time slicing more flexible in Sledgehammer: label slices with 'slice size'
blanchet
parents:
75059
diff
changeset
|
338 |
((1, 500, meshN), (format, "mono_native", liftingN, true, spass_H2SOS)), |
d9bb81999d2c
first step in making time slicing more flexible in Sledgehammer: label slices with 'slice size'
blanchet
parents:
75059
diff
changeset
|
339 |
((1, 50, meshN), (format, "mono_native", liftingN, true, spass_H2LR0LT0)), |
d9bb81999d2c
first step in making time slicing more flexible in Sledgehammer: label slices with 'slice size'
blanchet
parents:
75059
diff
changeset
|
340 |
((1, 250, meshN), (format, "mono_native", combsN, true, spass_H2NuVS0)), |
d9bb81999d2c
first step in making time slicing more flexible in Sledgehammer: label slices with 'slice size'
blanchet
parents:
75059
diff
changeset
|
341 |
((1, 1000, mepoN), (format, "mono_native", liftingN, true, spass_H1SOS)), |
d9bb81999d2c
first step in making time slicing more flexible in Sledgehammer: label slices with 'slice size'
blanchet
parents:
75059
diff
changeset
|
342 |
((1, 150, meshN), (format, "poly_guards??", liftingN, false, spass_H2NuVS0Red2)), |
d9bb81999d2c
first step in making time slicing more flexible in Sledgehammer: label slices with 'slice size'
blanchet
parents:
75059
diff
changeset
|
343 |
((1, 300, meshN), (format, "mono_native", combsN, true, spass_H2SOS)), |
d9bb81999d2c
first step in making time slicing more flexible in Sledgehammer: label slices with 'slice size'
blanchet
parents:
75059
diff
changeset
|
344 |
((1, 100, meshN), (format, "mono_native", combs_and_liftingN, true, spass_H2))], |
75026 | 345 |
good_max_mono_iters = default_max_mono_iters, |
346 |
good_max_new_mono_instances = default_max_new_mono_instances} |
|
73375 | 347 |
end |
38454
9043eefe8d71
detect old Vampire and give a nicer error message
blanchet
parents:
38433
diff
changeset
|
348 |
|
48005
eeede26f2721
killed SPASS 3.5/3.7 FLOTTER hack -- requires users to upgrade to SPASS 3.8
blanchet
parents:
48004
diff
changeset
|
349 |
val spass = (spassN, fn () => spass_config) |
38454
9043eefe8d71
detect old Vampire and give a nicer error message
blanchet
parents:
38433
diff
changeset
|
350 |
|
52073
ccb292952774
started adding agsyHOL as an experimental prover
blanchet
parents:
51998
diff
changeset
|
351 |
|
37509
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
37506
diff
changeset
|
352 |
(* Vampire *) |
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
37506
diff
changeset
|
353 |
|
74311
19022ea3f8cc
clarified name and options for old vampire-4.2.2;
wenzelm
parents:
74207
diff
changeset
|
354 |
val vampire_basic_options = |
19022ea3f8cc
clarified name and options for old vampire-4.2.2;
wenzelm
parents:
74207
diff
changeset
|
355 |
"--proof tptp --output_axiom_names on" ^ |
19022ea3f8cc
clarified name and options for old vampire-4.2.2;
wenzelm
parents:
74207
diff
changeset
|
356 |
(if ML_System.platform_is_windows |
19022ea3f8cc
clarified name and options for old vampire-4.2.2;
wenzelm
parents:
74207
diff
changeset
|
357 |
then "" (*time slicing is not support in the Windows version of Vampire*) |
19022ea3f8cc
clarified name and options for old vampire-4.2.2;
wenzelm
parents:
74207
diff
changeset
|
358 |
else " --mode casc") |
58084 | 359 |
|
360 |
val vampire_full_proof_options = |
|
71793 | 361 |
" --proof_extra free --forced_options avatar=off:equality_proxy=off:general_splitting=off:inequality_splitting=0:naming=0" |
58084 | 362 |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
363 |
val vampire_config : atp_config = |
74890 | 364 |
{exec = (["VAMPIRE_HOME"], ["vampire"]), |
75341 | 365 |
arguments = fn _ => fn full_proofs => fn sos => fn timeout => fn problem => |
74890 | 366 |
[vampire_basic_options ^ (if full_proofs then " " ^ vampire_full_proof_options else "") ^ |
367 |
" -t " ^ string_of_int (to_secs 1 timeout) ^ " --input_file " ^ File.bash_path problem |
|
368 |
|> sos = sosN ? prefix "--sos on "], |
|
369 |
proof_delims = |
|
370 |
[("=========== Refutation ==========", |
|
371 |
"======= End of refutation =======")] @ |
|
372 |
tstp_proof_delims, |
|
373 |
known_failures = |
|
374 |
[(GaveUp, "UNPROVABLE"), |
|
375 |
(GaveUp, "CANNOT PROVE"), |
|
376 |
(Unprovable, "Satisfiability detected"), |
|
377 |
(Unprovable, "Termination reason: Satisfiable"), |
|
378 |
(Interrupted, "Aborted by signal SIGINT")] @ |
|
379 |
known_szs_status_failures, |
|
380 |
prem_role = Hypothesis, |
|
75026 | 381 |
good_slices = |
74890 | 382 |
(* FUDGE *) |
75339
d9bb81999d2c
first step in making time slicing more flexible in Sledgehammer: label slices with 'slice size'
blanchet
parents:
75059
diff
changeset
|
383 |
K [((1, 512, meshN), (TX1, "mono_native_fool", combsN, false, sosN)), |
d9bb81999d2c
first step in making time slicing more flexible in Sledgehammer: label slices with 'slice size'
blanchet
parents:
75059
diff
changeset
|
384 |
((1, 1024, meshN), (TX1, "mono_native_fool", liftingN, false, sosN)), |
d9bb81999d2c
first step in making time slicing more flexible in Sledgehammer: label slices with 'slice size'
blanchet
parents:
75059
diff
changeset
|
385 |
((1, 256, mashN), (TX1, "mono_native_fool", liftingN, false, no_sosN)), |
d9bb81999d2c
first step in making time slicing more flexible in Sledgehammer: label slices with 'slice size'
blanchet
parents:
75059
diff
changeset
|
386 |
((1, 512, mepoN), (TF1, "poly_native", liftingN, false, no_sosN)), |
d9bb81999d2c
first step in making time slicing more flexible in Sledgehammer: label slices with 'slice size'
blanchet
parents:
75059
diff
changeset
|
387 |
((1, 16, meshN), (TX1, "mono_native_fool", liftingN, false, no_sosN)), |
d9bb81999d2c
first step in making time slicing more flexible in Sledgehammer: label slices with 'slice size'
blanchet
parents:
75059
diff
changeset
|
388 |
((1, 32, meshN), (TX1, "mono_native_fool", combsN, false, no_sosN)), |
d9bb81999d2c
first step in making time slicing more flexible in Sledgehammer: label slices with 'slice size'
blanchet
parents:
75059
diff
changeset
|
389 |
((1, 64, meshN), (TX1, "mono_native_fool", combs_or_liftingN, false, no_sosN)), |
d9bb81999d2c
first step in making time slicing more flexible in Sledgehammer: label slices with 'slice size'
blanchet
parents:
75059
diff
changeset
|
390 |
((1, 128, meshN), (TX1, "mono_native_fool", liftingN, false, no_sosN))], |
75026 | 391 |
good_max_mono_iters = default_max_mono_iters, |
392 |
good_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)} |
|
38454
9043eefe8d71
detect old Vampire and give a nicer error message
blanchet
parents:
38433
diff
changeset
|
393 |
|
47646 | 394 |
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
|
395 |
|
68563 | 396 |
|
69717 | 397 |
(* Zipperposition *) |
398 |
||
57154 | 399 |
val zipperposition_config : atp_config = |
73375 | 400 |
let |
74890 | 401 |
val format = |
402 |
THF (Polymorphic, {with_ite = true, with_let = false}, THF_Without_Choice) |
|
73375 | 403 |
in |
404 |
{exec = (["ZIPPERPOSITION_HOME"], ["zipperposition"]), |
|
75341 | 405 |
arguments = fn _ => fn _ => fn extra_options => fn timeout => fn problem => |
74471 | 406 |
["--input tptp", "--output tptp", "--timeout " ^ Time.toString timeout, extra_options, |
407 |
File.bash_path problem], |
|
73375 | 408 |
proof_delims = tstp_proof_delims, |
74207 | 409 |
known_failures = |
410 |
[(TimedOut, "SZS status ResourceOut")] @ (* odd way of timing out *) |
|
411 |
known_szs_status_failures, |
|
73375 | 412 |
prem_role = Hypothesis, |
75026 | 413 |
good_slices = |
75718
3557f826362c
changed the order of Zipperposition slices in Sledgehammer
blanchet
parents:
75465
diff
changeset
|
414 |
K [((1, 256, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --boolean-reasoning=simpl-only --ho-unif-max-depth=0 --ho-prim-enum=none -q \"2|prefer-ho-steps|conjecture-relative-e(0.1,0.5,100,100,100,100,1.5,1.5,1.5)\" -q \"1|prefer-sos|pnrefined(1,1,1,2,2,2,0.5)\" -q \"2|prefer-ground|default\" -q \"2|prefer-empty-trail|conjecture-relative-e(0.1,0.5,100,100,100,100,1.5,1.5,1.5)\" -q \"1|prefer-processed|fifo\" --select=bb+e-selection7 --ho-pattern-decider=false --ho-fixpoint-decider=true --ho-solid-decider=false --sine=150 --sine-tolerance=2 --sine-depth-max=3 --sine-depth-min=1 --prec-gen-fun=invfreqhack --lazy-cnf=true --lazy-cnf-kind=simp --lazy-cnf-renaming-threshold=2 --fluid-log-hoist=false --tptp-def-as-rewrite --rewrite-before-cnf=true --ho-prim-enum=eq --ho-prim-enum-add-var=true --ho-prim-max=1 --ho-prim-enum-early-bird=true -o tptp --avatar=eager --split-only-ground=true")), |
3557f826362c
changed the order of Zipperposition slices in Sledgehammer
blanchet
parents:
75465
diff
changeset
|
415 |
((1, 64, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-comb-complete --boolean-reasoning=simpl-only --ext-rules=off --kbo-weight-fun=lambda-def-sqarity --ho-prim-enum=none --tptp-def-as-rewrite -q \"4|prefer-sos|orient-lmax(2,1,2,1,1)\" -q \"4|defer-sos|conjecture-relative-var(1,s,f)\" -q \"3|const|default\" -q \"1|prefer-processed|fifo\" --ho-elim-leibniz=1 --select=NoSelection --solve-formulas=true --lazy-cnf=true --lazy-cnf-kind=simp --lazy-cnf-renaming-threshold=8 --sine=60 --sine-tolerance=2 --sine-depth-max=5 --sine-depth-min=1 --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=3 --e-auto=true --e-max-derived=50 --e-encode-lambdas=ignore --scan-clause-ac=false --presaturate=true --comb-b-penalty=3 --comb-c-penalty=3 --comb-k-penalty=1 --comb-s-penalty=5 --subvarsup=false --e-call-point=0.15 --lazy-cnf-kind=simp --trigger-bool-ind=1")), |
75339
d9bb81999d2c
first step in making time slicing more flexible in Sledgehammer: label slices with 'slice size'
blanchet
parents:
75059
diff
changeset
|
416 |
((1, 32, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic -nc --tptp-def-as-rewrite --rewrite-before-cnf=true --mode=ho-competitive --boolean-reasoning=simpl-only --ext-rules=ext-family --ext-rules-max-depth=1 --ho-prim-enum=none --avatar=off --recognize-injectivity=true --ho-elim-leibniz=1 --ho-unif-level=pragmatic-framework --no-max-vars --max-inferences=4 --ho-max-app-projections=1 --ho-max-elims=0 --ho-max-rigid-imitations=2 --ho-max-identifications=0 --ho-unif-max-depth=3 -q \"6|prefer-sos|pnrefined(1,1,1,2,2,2,0.5)\" -q \"6|const|conjecture-relative-var(1.02,l,f)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-var(1,l,f)\" -q \"4|prefer-easy-ho|conjecture-relative-var(1.01,s,f)\" --select=e-selection7 --ho-choice-inst=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=7 --sine=50 --sine-tolerance=1 --sine-depth-max=2 --sine-depth-min=1 --e-max-derived=64 --sine-ignore-k-most-common-syms=2 --sine-trim-implications=true --e-encode-lambdas=lift --scan-clause-ac=false --lambdasup=0 --kbo-weight-fun=lambda-def-invfreqrank --demod-in-var-args=true --bool-demod=true --lambda-demod=true --e-call-point=0.1 --lazy-cnf-kind=simp")), |
75718
3557f826362c
changed the order of Zipperposition slices in Sledgehammer
blanchet
parents:
75465
diff
changeset
|
417 |
((1, 512, mashN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --tptp-def-as-rewrite --rewrite-before-cnf=true --mode=ho-competitive --boolean-reasoning=simpl-only --ext-rules=ext-family --ext-rules-max-depth=1 --ho-prim-enum=none --avatar=off --recognize-injectivity=true --ho-elim-leibniz=1 --ho-unif-level=pragmatic-framework --no-max-vars --max-inferences=2 --ho-unif-max-depth=1 -q \"6|prefer-sos|pnrefined(1,1,1,2,2,2,0.5)\" -q \"6|const|conjecture-relative-var(1.02,l,f)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-var(1,l,f)\" -q \"4|prefer-easy-ho|conjecture-relative-var(1.01,s,f)\" --select=e-selection16 --ho-choice-inst=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=3 --e-auto=true --sine=50 --sine-tolerance=1.0 --sine-depth-max=3 --sine-depth-min=1 --sine-trim-implications=true --ho-unif-level=pragmatic-framework --e-encode-lambdas=lift --scan-clause-ac=false --kbo-weight-fun=lambda-def-invfreqrank --e-call-point=0.1")), |
3557f826362c
changed the order of Zipperposition slices in Sledgehammer
blanchet
parents:
75465
diff
changeset
|
418 |
((1, 1024, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --tptp-def-as-rewrite --rewrite-before-cnf=true --max-inferences=1 --ho-unif-max-depth=1 --ho-max-elims=0 --ho-max-app-projections=0 --ho-max-rigid-imitations=1 --ho-max-identifications=0 --boolean-reasoning=bool-hoist --bool-hoist-simpl=true --bool-select=LI --recognize-injectivity=true --ext-rules=ext-family --ext-rules-max-depth=1 --ho-choice-inst=true --ho-prim-enum=none --ho-elim-leibniz=0 --interpret-bool-funs=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --ho-unif-level=pragmatic-framework --select=bb+e-selection2 --post-cnf-lambda-lifting=true -q \"4|prefer-sos|pnrefined(2,1,1,1,2,2,2)\" -q \"6|prefer-processed|conjecture-relative-struct(1.5,3.5,2,3)\" -q \"1|const|fifo\" -q \"4|prefer-ground|orient-lmax(2,1,2,1,1)\" -q \"4|defer-sos|conjecture-relative-struct(1,5,2,3)\" --avatar=off --recognize-injectivity=true --ho-neg-ext=true --e-timeout=2 --ho-pattern-decider=true --ho-fixpoint-decider=true --e-max-derived=50 --ignore-orphans=true --e-auto=true --presaturate=true --e-call-point=0.1")), |
3557f826362c
changed the order of Zipperposition slices in Sledgehammer
blanchet
parents:
75465
diff
changeset
|
419 |
((1, 128, mepoN), (format, "mono_native_higher_fool", keep_lamsN, false, "-nc --tptp-def-as-rewrite --rewrite-before-cnf=true --mode=ho-competitive --boolean-reasoning=simpl-only --ext-rules=off --ho-prim-enum=full --ho-prim-max=1 --avatar=off --recognize-injectivity=true --ho-elim-leibniz=4 --ho-unif-level=full-framework --no-max-vars -q \"2|prefer-goals|conjecture-relative-e(0.5,1,100,100,100,100,1.5,1.5,1)\" -q \"4|const|conjecture-relative-e(0.1,1,100,100,100,100,1.5,1.5,1.5)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-e(0.5,1,100,100,100,100,1.5,1.5,1.5)\" -q \"4|prefer-sos|pnrefined(1,1,1,1,2,1.5,2)\" --select=ho-selection5 --ho-choice-inst=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=5 --e-call-point=0.25 --e-auto=true --sine=50 --sine-tolerance=2 --sine-depth-max=4 --sine-depth-min=1 --e-max-derived=96 --e-encode-lambdas=lift --scan-clause-ac=false --kbo-weight-fun=arity0 --prec-gen-fun=invfreq_conj"))], |
75026 | 420 |
good_max_mono_iters = default_max_mono_iters, |
421 |
good_max_new_mono_instances = default_max_new_mono_instances} |
|
73375 | 422 |
end |
57154 | 423 |
|
424 |
val zipperposition = (zipperpositionN, fn () => zipperposition_config) |
|
425 |
||
426 |
||
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
427 |
(* Remote ATP invocation via SystemOnTPTP *) |
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
428 |
|
73426
bd8bce50b9d4
use SystemOnTPTP.list_systems from Isabelle/Scala, with dynamic URL option and more elementary error messages;
wenzelm
parents:
73375
diff
changeset
|
429 |
val no_remote_systems = {url = "", systems = [] : string list} |
bd8bce50b9d4
use SystemOnTPTP.list_systems from Isabelle/Scala, with dynamic URL option and more elementary error messages;
wenzelm
parents:
73375
diff
changeset
|
430 |
val remote_systems = Synchronized.var "atp_remote_systems" no_remote_systems |
31835 | 431 |
|
49984 | 432 |
fun get_remote_systems () = |
73426
bd8bce50b9d4
use SystemOnTPTP.list_systems from Isabelle/Scala, with dynamic URL option and more elementary error messages;
wenzelm
parents:
73375
diff
changeset
|
433 |
Timeout.apply (seconds 10.0) SystemOnTPTP.list_systems () |
bd8bce50b9d4
use SystemOnTPTP.list_systems from Isabelle/Scala, with dynamic URL option and more elementary error messages;
wenzelm
parents:
73375
diff
changeset
|
434 |
handle ERROR msg => (warning msg; no_remote_systems) |
bd8bce50b9d4
use SystemOnTPTP.list_systems from Isabelle/Scala, with dynamic URL option and more elementary error messages;
wenzelm
parents:
73375
diff
changeset
|
435 |
| Timeout.TIMEOUT _ => no_remote_systems |
31835 | 436 |
|
49984 | 437 |
fun find_remote_system name [] systems = |
42537
25ceb855a18b
improve version handling -- prefer versions of ToFoF, SInE, and SNARK that are known to work
blanchet
parents:
42535
diff
changeset
|
438 |
find_first (String.isPrefix (name ^ "---")) systems |
49984 | 439 |
| find_remote_system name (version :: versions) systems = |
38690
38a926e033ad
make remote ATP versions more robust, by starting with "preferred" version numbers and falling back on any version
blanchet
parents:
38685
diff
changeset
|
440 |
case find_first (String.isPrefix (name ^ "---" ^ version)) systems of |
49984 | 441 |
NONE => find_remote_system name versions systems |
38690
38a926e033ad
make remote ATP versions more robust, by starting with "preferred" version numbers and falling back on any version
blanchet
parents:
38685
diff
changeset
|
442 |
| 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
|
443 |
|
49984 | 444 |
fun get_remote_system name versions = |
73426
bd8bce50b9d4
use SystemOnTPTP.list_systems from Isabelle/Scala, with dynamic URL option and more elementary error messages;
wenzelm
parents:
73375
diff
changeset
|
445 |
Synchronized.change_result remote_systems (fn remote => |
bd8bce50b9d4
use SystemOnTPTP.list_systems from Isabelle/Scala, with dynamic URL option and more elementary error messages;
wenzelm
parents:
73375
diff
changeset
|
446 |
(if #url remote <> SystemOnTPTP.get_url () orelse null (#systems remote) |
bd8bce50b9d4
use SystemOnTPTP.list_systems from Isabelle/Scala, with dynamic URL option and more elementary error messages;
wenzelm
parents:
73375
diff
changeset
|
447 |
then get_remote_systems () else remote) |> ` #systems) |
bd8bce50b9d4
use SystemOnTPTP.list_systems from Isabelle/Scala, with dynamic URL option and more elementary error messages;
wenzelm
parents:
73375
diff
changeset
|
448 |
|> `(find_remote_system name versions) |
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset
|
449 |
|
49984 | 450 |
fun the_remote_system name versions = |
54788
a898e15b522a
primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents:
54197
diff
changeset
|
451 |
(case get_remote_system name versions of |
42955 | 452 |
(SOME sys, _) => sys |
63692 | 453 |
| (NONE, []) => error "SystemOnTPTP is currently not available" |
42955 | 454 |
| (NONE, syss) => |
54788
a898e15b522a
primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents:
54197
diff
changeset
|
455 |
(case syss |> filter_out (String.isPrefix "%") |> filter_out (curry (op =) "") of |
63692 | 456 |
[] => error "SystemOnTPTP is currently not available" |
457 |
| [msg] => error ("SystemOnTPTP is currently not available: " ^ msg) |
|
46480 | 458 |
| syss => |
54788
a898e15b522a
primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents:
54197
diff
changeset
|
459 |
error ("System " ^ quote name ^ " is not available at SystemOnTPTP.\n(Available systems: " ^ |
a898e15b522a
primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents:
54197
diff
changeset
|
460 |
commas_quote syss ^ ".)"))) |
31835 | 461 |
|
72174 | 462 |
val max_remote_secs = 1000 (* give Geoff Sutcliffe's servers a break *) |
41148 | 463 |
|
73435
1cc848548f21
invoke remote ATP via SystemOnTPTP.run_systems from Isabelle/Scala (without perl);
wenzelm
parents:
73432
diff
changeset
|
464 |
val isabelle_scala_function = (["SCALA_HOME"], ["bin/scala"]) |
1cc848548f21
invoke remote ATP via SystemOnTPTP.run_systems from Isabelle/Scala (without perl);
wenzelm
parents:
73432
diff
changeset
|
465 |
|
75026 | 466 |
fun remote_config system_name system_versions proof_delims known_failures prem_role good_slice = |
73435
1cc848548f21
invoke remote ATP via SystemOnTPTP.run_systems from Isabelle/Scala (without perl);
wenzelm
parents:
73432
diff
changeset
|
467 |
{exec = isabelle_scala_function, |
75341 | 468 |
arguments = fn _ => fn _ => fn command => fn timeout => fn problem => |
73435
1cc848548f21
invoke remote ATP via SystemOnTPTP.run_systems from Isabelle/Scala (without perl);
wenzelm
parents:
73432
diff
changeset
|
469 |
[the_remote_system system_name system_versions, |
1cc848548f21
invoke remote ATP via SystemOnTPTP.run_systems from Isabelle/Scala (without perl);
wenzelm
parents:
73432
diff
changeset
|
470 |
Isabelle_System.absolute_path problem, |
73568
bdba138d462d
clarified signature: more structured arguments, notably for remote provers;
wenzelm
parents:
73437
diff
changeset
|
471 |
command, string_of_int (Int.min (max_remote_secs, to_secs 1 timeout) * 1000)], |
42962
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42955
diff
changeset
|
472 |
proof_delims = union (op =) tstp_proof_delims proof_delims, |
73436
e92f2e44e4d8
removed spurious references to perl / libwww-perl;
wenzelm
parents:
73435
diff
changeset
|
473 |
known_failures = known_failures @ known_says_failures, |
47976 | 474 |
prem_role = prem_role, |
75026 | 475 |
good_slices = fn ctxt => [good_slice ctxt], |
476 |
good_max_mono_iters = default_max_mono_iters, |
|
477 |
good_max_new_mono_instances = default_max_new_mono_instances} : atp_config |
|
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42332
diff
changeset
|
478 |
|
75026 | 479 |
fun remotify_config system_name system_versions good_slice |
58084 | 480 |
({proof_delims, known_failures, prem_role, ...} : atp_config) = |
75026 | 481 |
remote_config system_name system_versions proof_delims known_failures prem_role good_slice |
38023 | 482 |
|
75026 | 483 |
fun remote_atp name system_name system_versions proof_delims known_failures prem_role good_slice = |
58084 | 484 |
(remote_prefix ^ name, fn () => |
75026 | 485 |
remote_config system_name system_versions proof_delims known_failures prem_role good_slice) |
486 |
fun remotify_atp (name, config) system_name system_versions good_slice = |
|
487 |
(remote_prefix ^ name, remotify_config system_name system_versions good_slice o config) |
|
28592 | 488 |
|
57269
1df6f747f164
changed type encoding for new Waldmeister, to trigger filtering of 'dangerous' lemmas
blanchet
parents:
57265
diff
changeset
|
489 |
fun gen_remote_waldmeister name type_enc = |
57265 | 490 |
remote_atp name "Waldmeister" ["710"] tstp_proof_delims |
491 |
([(OutOfResources, "Too many function symbols"), |
|
492 |
(Inappropriate, "**** Unexpected end of file."), |
|
493 |
(Crashed, "Unrecoverable Segmentation Fault")] |
|
494 |
@ known_szs_status_failures) |
|
57264 | 495 |
Hypothesis |
75339
d9bb81999d2c
first step in making time slicing more flexible in Sledgehammer: label slices with 'slice size'
blanchet
parents:
75059
diff
changeset
|
496 |
(K ((1000 (* infinity *), 50, meshN), (CNF_UEQ, type_enc, combsN, false, "")) (* FUDGE *)) |
57264 | 497 |
|
52094 | 498 |
val remote_agsyhol = |
499 |
remotify_atp agsyhol "agsyHOL" ["1.0", "1"] |
|
75339
d9bb81999d2c
first step in making time slicing more flexible in Sledgehammer: label slices with 'slice size'
blanchet
parents:
75059
diff
changeset
|
500 |
(K ((1000 (* infinity *), 60, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, "")) (* FUDGE *)) |
70937 | 501 |
val remote_alt_ergo = |
502 |
remotify_atp alt_ergo "Alt-Ergo" ["0.95.2"] |
|
75339
d9bb81999d2c
first step in making time slicing more flexible in Sledgehammer: label slices with 'slice size'
blanchet
parents:
75059
diff
changeset
|
503 |
(K ((1000 (* infinity *), 250, meshN), (TF1, "poly_native", keep_lamsN, false, "")) (* FUDGE *)) |
43500
4c357b7aa710
provide appropriate type system and number of fact defaults for remote ATPs
blanchet
parents:
43497
diff
changeset
|
504 |
val remote_e = |
63768 | 505 |
remotify_atp e "E" ["2.0", "1.9.1", "1.8"] |
75339
d9bb81999d2c
first step in making time slicing more flexible in Sledgehammer: label slices with 'slice size'
blanchet
parents:
75059
diff
changeset
|
506 |
(K ((1000 (* infinity *), 750, meshN), (TF0, "mono_native", combsN, false, "")) (* FUDGE *)) |
48700 | 507 |
val remote_iprover = |
52094 | 508 |
remotify_atp iprover "iProver" ["0.99"] |
75339
d9bb81999d2c
first step in making time slicing more flexible in Sledgehammer: label slices with 'slice size'
blanchet
parents:
75059
diff
changeset
|
509 |
(K ((1000 (* infinity *), 150, meshN), (FOF, "mono_guards??", liftingN, false, "")) (* FUDGE *)) |
44099 | 510 |
val remote_leo2 = |
52094 | 511 |
remotify_atp leo2 "LEO-II" ["1.5.0", "1.4", "1.3", "1.2", "1"] |
75339
d9bb81999d2c
first step in making time slicing more flexible in Sledgehammer: label slices with 'slice size'
blanchet
parents:
75059
diff
changeset
|
512 |
(K ((1000 (* infinity *), 40, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", liftingN, false, "")) (* FUDGE *)) |
67021
41f1f8c4259b
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
blanchet
parents:
66544
diff
changeset
|
513 |
val remote_leo3 = |
41f1f8c4259b
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
blanchet
parents:
66544
diff
changeset
|
514 |
remotify_atp leo3 "Leo-III" ["1.1"] |
75339
d9bb81999d2c
first step in making time slicing more flexible in Sledgehammer: label slices with 'slice size'
blanchet
parents:
75059
diff
changeset
|
515 |
(K ((1000 (* infinity *), 150, meshN), (THF (Polymorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "poly_native_higher", keep_lamsN, false, "")) (* FUDGE *)) |
57269
1df6f747f164
changed type encoding for new Waldmeister, to trigger filtering of 'dangerous' lemmas
blanchet
parents:
57265
diff
changeset
|
516 |
val remote_waldmeister = gen_remote_waldmeister waldmeisterN "raw_mono_tags??" |
70940
ce3a05ad07b7
added support for Zipperposition on SystemOnTPTP
blanchet
parents:
70939
diff
changeset
|
517 |
val remote_zipperposition = |
74468 | 518 |
remotify_atp zipperposition "Zipperpin" ["2.1", "2.0"] |
75339
d9bb81999d2c
first step in making time slicing more flexible in Sledgehammer: label slices with 'slice size'
blanchet
parents:
75059
diff
changeset
|
519 |
(K ((1000 (* infinity *), 512, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, "")) (* FUDGE *)) |
72588 | 520 |
|
521 |
||
522 |
(* Dummy prover *) |
|
523 |
||
524 |
fun dummy_config prem_role format type_enc uncurried_aliases : atp_config = |
|
73374 | 525 |
{exec = (["ISABELLE_ATP"], ["scripts/dummy_atp"]), |
75341 | 526 |
arguments = K (K (K (K (K [])))), |
72588 | 527 |
proof_delims = [], |
528 |
known_failures = known_szs_status_failures, |
|
529 |
prem_role = prem_role, |
|
75026 | 530 |
good_slices = |
75339
d9bb81999d2c
first step in making time slicing more flexible in Sledgehammer: label slices with 'slice size'
blanchet
parents:
75059
diff
changeset
|
531 |
K [((1, 256, "mepo"), (format, type_enc, |
75026 | 532 |
if is_format_higher_order format then keep_lamsN else combsN, uncurried_aliases, ""))], |
533 |
good_max_mono_iters = default_max_mono_iters, |
|
534 |
good_max_new_mono_instances = default_max_new_mono_instances} |
|
72588 | 535 |
|
74894
a64a8f7d593e
refactored $ite and $let configuration and added dummy_thf_reduced prover
desharna
parents:
74890
diff
changeset
|
536 |
val dummy_fof = |
75024
114eb0af123d
simplified 'best_slice' data structure and made minor changes to slices
blanchet
parents:
74999
diff
changeset
|
537 |
(dummy_fofN, fn () => dummy_config Hypothesis FOF "mono_guards??" false) |
74117 | 538 |
|
74894
a64a8f7d593e
refactored $ite and $let configuration and added dummy_thf_reduced prover
desharna
parents:
74890
diff
changeset
|
539 |
val dummy_tfx = |
75024
114eb0af123d
simplified 'best_slice' data structure and made minor changes to slices
blanchet
parents:
74999
diff
changeset
|
540 |
(dummy_tfxN, fn () => dummy_config Hypothesis TX1 "poly_native_fool" false) |
74117 | 541 |
|
74894
a64a8f7d593e
refactored $ite and $let configuration and added dummy_thf_reduced prover
desharna
parents:
74890
diff
changeset
|
542 |
val dummy_thf = |
75024
114eb0af123d
simplified 'best_slice' data structure and made minor changes to slices
blanchet
parents:
74999
diff
changeset
|
543 |
(dummy_thfN, fn () => dummy_config Hypothesis TH1 "poly_native_higher" false) |
38454
9043eefe8d71
detect old Vampire and give a nicer error message
blanchet
parents:
38433
diff
changeset
|
544 |
|
74894
a64a8f7d593e
refactored $ite and $let configuration and added dummy_thf_reduced prover
desharna
parents:
74890
diff
changeset
|
545 |
val dummy_thf_reduced = |
a64a8f7d593e
refactored $ite and $let configuration and added dummy_thf_reduced prover
desharna
parents:
74890
diff
changeset
|
546 |
let |
74895
b605ebd87a47
proper polymorphism for TH1 format in Sledgehammer
desharna
parents:
74894
diff
changeset
|
547 |
val format = THF (Polymorphic, {with_ite = false, with_let = false}, THF_Without_Choice) |
74894
a64a8f7d593e
refactored $ite and $let configuration and added dummy_thf_reduced prover
desharna
parents:
74890
diff
changeset
|
548 |
val config = dummy_config Hypothesis format "poly_native_higher" false |
a64a8f7d593e
refactored $ite and $let configuration and added dummy_thf_reduced prover
desharna
parents:
74890
diff
changeset
|
549 |
in (dummy_thfN ^ "_reduced", fn () => config) end |
52073
ccb292952774
started adding agsyHOL as an experimental prover
blanchet
parents:
51998
diff
changeset
|
550 |
|
38454
9043eefe8d71
detect old Vampire and give a nicer error message
blanchet
parents:
38433
diff
changeset
|
551 |
(* Setup *) |
9043eefe8d71
detect old Vampire and give a nicer error message
blanchet
parents:
38433
diff
changeset
|
552 |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
553 |
fun add_atp (name, config) thy = |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
554 |
Data.map (Symtab.update_new (name, (config, stamp ()))) thy |
63692 | 555 |
handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name) |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
556 |
|
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
557 |
fun get_atp thy name = |
54788
a898e15b522a
primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents:
54197
diff
changeset
|
558 |
fst (the (Symtab.lookup (Data.get thy) name)) |
63692 | 559 |
handle Option.Option => error ("Unknown ATP: " ^ name) |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
560 |
|
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
561 |
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
|
562 |
let val {exec, ...} = get_atp thy name () in |
73374 | 563 |
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
|
564 |
end |
36371
8c83ea1a7740
move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents:
36370
diff
changeset
|
565 |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
566 |
fun refresh_systems_on_tptp () = |
49984 | 567 |
Synchronized.change remote_systems (fn _ => get_remote_systems ()) |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset
|
568 |
|
75036 | 569 |
val local_atps = |
75038 | 570 |
[agsyhol, alt_ergo, e, iprover, leo2, leo3, satallax, spass, vampire, zipperposition] |
75036 | 571 |
val remote_atps = |
572 |
[remote_agsyhol, remote_alt_ergo, remote_e, remote_iprover, remote_leo2, remote_leo3, |
|
75465
d9b23902692d
excluded dummy ATPs from Sledgehammer's default provers
desharna
parents:
75433
diff
changeset
|
573 |
remote_waldmeister, remote_zipperposition] |
d9b23902692d
excluded dummy ATPs from Sledgehammer's default provers
desharna
parents:
75433
diff
changeset
|
574 |
val dummy_atps = |
d9b23902692d
excluded dummy ATPs from Sledgehammer's default provers
desharna
parents:
75433
diff
changeset
|
575 |
[dummy_fof, dummy_tfx, dummy_thf, dummy_thf_reduced] |
d9b23902692d
excluded dummy ATPs from Sledgehammer's default provers
desharna
parents:
75433
diff
changeset
|
576 |
val non_dummy_atps = local_atps @ remote_atps |
d9b23902692d
excluded dummy ATPs from Sledgehammer's default provers
desharna
parents:
75433
diff
changeset
|
577 |
val all_atps = non_dummy_atps @ dummy_atps |
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
|
578 |
|
75465
d9b23902692d
excluded dummy ATPs from Sledgehammer's default provers
desharna
parents:
75433
diff
changeset
|
579 |
val _ = Theory.setup (fold add_atp all_atps) |
35867 | 580 |
|
75036 | 581 |
val local_atps = map fst local_atps |
582 |
val remote_atps = map fst remote_atps |
|
75465
d9b23902692d
excluded dummy ATPs from Sledgehammer's default provers
desharna
parents:
75433
diff
changeset
|
583 |
val dummy_atps = map fst dummy_atps |
d9b23902692d
excluded dummy ATPs from Sledgehammer's default provers
desharna
parents:
75433
diff
changeset
|
584 |
val non_dummy_atps = map fst non_dummy_atps |
d9b23902692d
excluded dummy ATPs from Sledgehammer's default provers
desharna
parents:
75433
diff
changeset
|
585 |
val all_atps = map fst all_atps |
75036 | 586 |
|
28592 | 587 |
end; |