author | blanchet |
Thu, 02 Sep 2010 00:15:53 +0200 | |
changeset 39010 | 344028ecc00e |
parent 39002 | a2d7be688ea1 |
child 39011 | af0ebd2fb433 |
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 |
38023 | 10 |
datatype failure = |
38519 | 11 |
Unprovable | IncompleteUnprovable | CantConnect | TimedOut | |
12 |
OutOfResources | SpassTooOld | VampireTooOld | NoPerl | NoLibwwwPerl | |
|
13 |
MalformedInput | MalformedOutput | UnknownError |
|
38023 | 14 |
|
15 |
type prover_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
|
16 |
{exec: string * string, |
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
|
17 |
required_execs: (string * string) list, |
38023 | 18 |
arguments: bool -> Time.time -> string, |
38645 | 19 |
has_incomplete_mode: bool, |
38023 | 20 |
proof_delims: (string * string) list, |
21 |
known_failures: (failure * string) list, |
|
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38740
diff
changeset
|
22 |
default_max_relevant: int, |
38631
979a0b37f981
prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible;
blanchet
parents:
38603
diff
changeset
|
23 |
explicit_forall: bool, |
979a0b37f981
prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible;
blanchet
parents:
38603
diff
changeset
|
24 |
use_conjecture_for_hypotheses: bool} |
38023 | 25 |
|
38061
685d1f0f75b3
handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents:
38049
diff
changeset
|
26 |
val string_for_failure : failure -> string |
685d1f0f75b3
handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents:
38049
diff
changeset
|
27 |
val known_failure_in_output : |
685d1f0f75b3
handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents:
38049
diff
changeset
|
28 |
string -> (failure * string) list -> failure option |
38023 | 29 |
val add_prover: string * prover_config -> theory -> theory |
30 |
val get_prover: theory -> string -> prover_config |
|
31 |
val available_atps: theory -> unit |
|
35867 | 32 |
val refresh_systems_on_tptp : unit -> unit |
36371
8c83ea1a7740
move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents:
36370
diff
changeset
|
33 |
val default_atps_param_value : unit -> string |
35867 | 34 |
val setup : theory -> theory |
28592 | 35 |
end; |
36 |
||
36376 | 37 |
structure ATP_Systems : ATP_SYSTEMS = |
28592 | 38 |
struct |
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
39 |
|
38023 | 40 |
(* prover configuration *) |
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset
|
41 |
|
38023 | 42 |
datatype failure = |
38454
9043eefe8d71
detect old Vampire and give a nicer error message
blanchet
parents:
38433
diff
changeset
|
43 |
Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources | |
38519 | 44 |
SpassTooOld | VampireTooOld | NoPerl | NoLibwwwPerl | MalformedInput | |
38454
9043eefe8d71
detect old Vampire and give a nicer error message
blanchet
parents:
38433
diff
changeset
|
45 |
MalformedOutput | UnknownError |
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset
|
46 |
|
32941
72d48e333b77
eliminated extraneous wrapping of public records;
wenzelm
parents:
32936
diff
changeset
|
47 |
type prover_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
|
48 |
{exec: string * string, |
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
|
49 |
required_execs: (string * string) list, |
37514
b147d01b8ebc
if SPASS fails at finding a proof with the SOS option turned on, turn it off and try again
blanchet
parents:
37509
diff
changeset
|
50 |
arguments: bool -> Time.time -> string, |
38645 | 51 |
has_incomplete_mode: bool, |
36370
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
52 |
proof_delims: (string * string) list, |
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
53 |
known_failures: (failure * string) list, |
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38740
diff
changeset
|
54 |
default_max_relevant: int, |
38631
979a0b37f981
prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible;
blanchet
parents:
38603
diff
changeset
|
55 |
explicit_forall: bool, |
979a0b37f981
prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible;
blanchet
parents:
38603
diff
changeset
|
56 |
use_conjecture_for_hypotheses: bool} |
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
57 |
|
38061
685d1f0f75b3
handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents:
38049
diff
changeset
|
58 |
val missing_message_tail = |
685d1f0f75b3
handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents:
38049
diff
changeset
|
59 |
" appears to be missing. You will need to install it if you want to run \ |
685d1f0f75b3
handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents:
38049
diff
changeset
|
60 |
\ATPs remotely." |
685d1f0f75b3
handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents:
38049
diff
changeset
|
61 |
|
685d1f0f75b3
handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents:
38049
diff
changeset
|
62 |
fun string_for_failure Unprovable = "The ATP problem is unprovable." |
685d1f0f75b3
handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents:
38049
diff
changeset
|
63 |
| string_for_failure IncompleteUnprovable = |
685d1f0f75b3
handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents:
38049
diff
changeset
|
64 |
"The ATP cannot prove the problem." |
38094 | 65 |
| string_for_failure CantConnect = "Can't connect to remote server." |
38061
685d1f0f75b3
handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents:
38049
diff
changeset
|
66 |
| string_for_failure TimedOut = "Timed out." |
685d1f0f75b3
handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents:
38049
diff
changeset
|
67 |
| string_for_failure OutOfResources = "The ATP ran out of resources." |
38519 | 68 |
| string_for_failure SpassTooOld = |
38096 | 69 |
"Isabelle requires a more recent version of SPASS with support for the \ |
70 |
\TPTP syntax. To install it, download and extract the package \ |
|
71 |
\\"http://isabelle.in.tum.de/dist/contrib/spass-3.7.tar.gz\" and add the \ |
|
72 |
\\"spass-3.7\" directory's absolute path to " ^ |
|
38061
685d1f0f75b3
handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents:
38049
diff
changeset
|
73 |
quote (Path.implode (Path.expand (Path.appends |
685d1f0f75b3
handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents:
38049
diff
changeset
|
74 |
(Path.variable "ISABELLE_HOME_USER" :: |
685d1f0f75b3
handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents:
38049
diff
changeset
|
75 |
map Path.basic ["etc", "components"])))) ^ |
685d1f0f75b3
handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents:
38049
diff
changeset
|
76 |
" on a line of its own." |
38519 | 77 |
| string_for_failure VampireTooOld = |
38454
9043eefe8d71
detect old Vampire and give a nicer error message
blanchet
parents:
38433
diff
changeset
|
78 |
"Isabelle requires a more recent version of Vampire. To install it, follow \ |
9043eefe8d71
detect old Vampire and give a nicer error message
blanchet
parents:
38433
diff
changeset
|
79 |
\the instructions from the Sledgehammer manual (\"isabelle doc\ |
9043eefe8d71
detect old Vampire and give a nicer error message
blanchet
parents:
38433
diff
changeset
|
80 |
\ sledgehammer\")." |
38061
685d1f0f75b3
handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents:
38049
diff
changeset
|
81 |
| string_for_failure NoPerl = "Perl" ^ missing_message_tail |
685d1f0f75b3
handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents:
38049
diff
changeset
|
82 |
| string_for_failure NoLibwwwPerl = |
685d1f0f75b3
handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents:
38049
diff
changeset
|
83 |
"The Perl module \"libwww-perl\"" ^ missing_message_tail |
685d1f0f75b3
handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents:
38049
diff
changeset
|
84 |
| string_for_failure MalformedInput = |
38096 | 85 |
"The ATP problem is malformed. Please report this to the Isabelle \ |
86 |
\developers." |
|
87 |
| string_for_failure MalformedOutput = "The ATP output is malformed." |
|
88 |
| string_for_failure UnknownError = "An unknown ATP error occurred." |
|
38061
685d1f0f75b3
handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents:
38049
diff
changeset
|
89 |
|
685d1f0f75b3
handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents:
38049
diff
changeset
|
90 |
fun known_failure_in_output output = |
685d1f0f75b3
handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents:
38049
diff
changeset
|
91 |
find_first (fn (_, pattern) => String.isSubstring pattern output) |
685d1f0f75b3
handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents:
38049
diff
changeset
|
92 |
#> Option.map fst |
685d1f0f75b3
handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents:
38049
diff
changeset
|
93 |
|
685d1f0f75b3
handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents:
38049
diff
changeset
|
94 |
val known_perl_failures = |
38094 | 95 |
[(CantConnect, "HTTP error"), |
96 |
(NoPerl, "env: perl"), |
|
38065 | 97 |
(NoLibwwwPerl, "Can't locate HTTP")] |
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
98 |
|
38023 | 99 |
(* named provers *) |
38001
a9b47b85ca24
reintroduced more preprocessing steps to Sledgehammer, adapted to the new FOF setting
blanchet
parents:
38000
diff
changeset
|
100 |
|
38023 | 101 |
structure Data = Theory_Data |
102 |
( |
|
103 |
type T = (prover_config * stamp) Symtab.table |
|
104 |
val empty = Symtab.empty |
|
105 |
val extend = I |
|
106 |
fun merge data : T = Symtab.merge (eq_snd op =) data |
|
107 |
handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".") |
|
108 |
) |
|
38017
3ad3e3ca2451
move Sledgehammer-specific code out of "Sledgehammer_TPTP_Format"
blanchet
parents:
38015
diff
changeset
|
109 |
|
38023 | 110 |
fun add_prover (name, config) thy = |
111 |
Data.map (Symtab.update_new (name, (config, stamp ()))) thy |
|
112 |
handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".") |
|
38017
3ad3e3ca2451
move Sledgehammer-specific code out of "Sledgehammer_TPTP_Format"
blanchet
parents:
38015
diff
changeset
|
113 |
|
38023 | 114 |
fun get_prover thy name = |
115 |
the (Symtab.lookup (Data.get thy) name) |> fst |
|
116 |
handle Option.Option => error ("Unknown ATP: " ^ name ^ ".") |
|
37962
d7dbe01f48d7
keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems;
blanchet
parents:
37926
diff
changeset
|
117 |
|
38023 | 118 |
fun available_atps thy = |
119 |
priority ("Available ATPs: " ^ |
|
120 |
commas (sort_strings (Symtab.keys (Data.get thy))) ^ ".") |
|
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset
|
121 |
|
38023 | 122 |
fun available_atps thy = |
123 |
priority ("Available ATPs: " ^ |
|
124 |
commas (sort_strings (Symtab.keys (Data.get thy))) ^ ".") |
|
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
125 |
|
38737
bdcb23701448
better workaround for E's off-by-one-second issue
blanchet
parents:
38691
diff
changeset
|
126 |
fun to_secs bonus time = (Time.toMilliseconds time + bonus + 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
|
127 |
|
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
128 |
(* E prover *) |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
129 |
|
38737
bdcb23701448
better workaround for E's off-by-one-second issue
blanchet
parents:
38691
diff
changeset
|
130 |
(* Give older versions of E an extra second, because the "eproof" script wrongly |
bdcb23701448
better workaround for E's off-by-one-second issue
blanchet
parents:
38691
diff
changeset
|
131 |
subtracted an entire second to account for the overhead of the script |
bdcb23701448
better workaround for E's off-by-one-second issue
blanchet
parents:
38691
diff
changeset
|
132 |
itself, which is in fact much lower. *) |
bdcb23701448
better workaround for E's off-by-one-second issue
blanchet
parents:
38691
diff
changeset
|
133 |
fun e_bonus () = |
bdcb23701448
better workaround for E's off-by-one-second issue
blanchet
parents:
38691
diff
changeset
|
134 |
case getenv "E_VERSION" of |
bdcb23701448
better workaround for E's off-by-one-second issue
blanchet
parents:
38691
diff
changeset
|
135 |
"" => 1000 |
bdcb23701448
better workaround for E's off-by-one-second issue
blanchet
parents:
38691
diff
changeset
|
136 |
| version => |
bdcb23701448
better workaround for E's off-by-one-second issue
blanchet
parents:
38691
diff
changeset
|
137 |
if exists (fn s => String.isPrefix s version) ["0.9", "1.0"] then 1000 |
bdcb23701448
better workaround for E's off-by-one-second issue
blanchet
parents:
38691
diff
changeset
|
138 |
else 0 |
bdcb23701448
better workaround for E's off-by-one-second issue
blanchet
parents:
38691
diff
changeset
|
139 |
|
36369
d2cd0d04b8e6
handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents:
36289
diff
changeset
|
140 |
val tstp_proof_delims = |
d2cd0d04b8e6
handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents:
36289
diff
changeset
|
141 |
("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation") |
d2cd0d04b8e6
handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents:
36289
diff
changeset
|
142 |
|
35969 | 143 |
val e_config : prover_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
|
144 |
{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
|
145 |
required_execs = [], |
37514
b147d01b8ebc
if SPASS fails at finding a proof with the SOS option turned on, turn it off and try again
blanchet
parents:
37509
diff
changeset
|
146 |
arguments = fn _ => fn timeout => |
38691 | 147 |
"--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent \ |
38737
bdcb23701448
better workaround for E's off-by-one-second issue
blanchet
parents:
38691
diff
changeset
|
148 |
\--cpu-limit=" ^ string_of_int (to_secs (e_bonus ()) timeout), |
38645 | 149 |
has_incomplete_mode = false, |
36369
d2cd0d04b8e6
handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents:
36289
diff
changeset
|
150 |
proof_delims = [tstp_proof_delims], |
36265
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset
|
151 |
known_failures = |
37995
06f02b15ef8a
generate full first-order formulas (FOF) in Sledgehammer
blanchet
parents:
37994
diff
changeset
|
152 |
[(Unprovable, "SZS status: CounterSatisfiable"), |
06f02b15ef8a
generate full first-order formulas (FOF) in Sledgehammer
blanchet
parents:
37994
diff
changeset
|
153 |
(Unprovable, "SZS status CounterSatisfiable"), |
36370
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
154 |
(TimedOut, "Failure: Resource limit exceeded (time)"), |
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
155 |
(TimedOut, "time limit exceeded"), |
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
156 |
(OutOfResources, |
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
157 |
"# Cannot determine problem status within resource limit"), |
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
158 |
(OutOfResources, "SZS status: ResourceOut"), |
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
159 |
(OutOfResources, "SZS status ResourceOut")], |
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38740
diff
changeset
|
160 |
default_max_relevant = 500 (* FUDGE *), |
38631
979a0b37f981
prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible;
blanchet
parents:
38603
diff
changeset
|
161 |
explicit_forall = false, |
979a0b37f981
prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible;
blanchet
parents:
38603
diff
changeset
|
162 |
use_conjecture_for_hypotheses = true} |
38454
9043eefe8d71
detect old Vampire and give a nicer error message
blanchet
parents:
38433
diff
changeset
|
163 |
|
38023 | 164 |
val e = ("e", e_config) |
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
165 |
|
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
166 |
|
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
|
167 |
(* The "-VarWeight=3" option helps the higher-order problems, probably by |
16670b4f0baa
set SPASS option on the command-line, so that it doesn't vanish when moving to TPTP format
blanchet
parents:
36190
diff
changeset
|
168 |
counteracting the presence of "hAPP". *) |
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37480
diff
changeset
|
169 |
val spass_config : prover_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
|
170 |
{exec = ("ISABELLE_ATP", "scripts/spass"), |
39002 | 171 |
required_execs = [("SPASS_HOME", "SPASS"), ("SPASS_HOME", "tptp2dfg")], |
37514
b147d01b8ebc
if SPASS fails at finding a proof with the SOS option turned on, turn it off and try again
blanchet
parents:
37509
diff
changeset
|
172 |
arguments = fn complete => fn timeout => |
37962
d7dbe01f48d7
keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems;
blanchet
parents:
37926
diff
changeset
|
173 |
("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \ |
38737
bdcb23701448
better workaround for E's off-by-one-second issue
blanchet
parents:
38691
diff
changeset
|
174 |
\-VarWeight=3 -TimeLimit=" ^ string_of_int (to_secs 0 timeout)) |
37514
b147d01b8ebc
if SPASS fails at finding a proof with the SOS option turned on, turn it off and try again
blanchet
parents:
37509
diff
changeset
|
175 |
|> not complete ? prefix "-SOS=1 ", |
38645 | 176 |
has_incomplete_mode = true, |
36369
d2cd0d04b8e6
handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents:
36289
diff
changeset
|
177 |
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
|
178 |
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
|
179 |
known_perl_failures @ |
37413 | 180 |
[(IncompleteUnprovable, "SPASS beiseite: Completion found"), |
36370
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
181 |
(TimedOut, "SPASS beiseite: Ran out of time"), |
36965 | 182 |
(OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"), |
37413 | 183 |
(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
|
184 |
(MalformedInput, "Free Variable"), |
38519 | 185 |
(SpassTooOld, "tptp2dfg")], |
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38740
diff
changeset
|
186 |
default_max_relevant = 350 (* FUDGE *), |
38631
979a0b37f981
prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible;
blanchet
parents:
38603
diff
changeset
|
187 |
explicit_forall = true, |
979a0b37f981
prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible;
blanchet
parents:
38603
diff
changeset
|
188 |
use_conjecture_for_hypotheses = true} |
38454
9043eefe8d71
detect old Vampire and give a nicer error message
blanchet
parents:
38433
diff
changeset
|
189 |
|
38023 | 190 |
val spass = ("spass", spass_config) |
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
191 |
|
38454
9043eefe8d71
detect old Vampire and give a nicer error message
blanchet
parents:
38433
diff
changeset
|
192 |
|
37509
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
37506
diff
changeset
|
193 |
(* Vampire *) |
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
37506
diff
changeset
|
194 |
|
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
37506
diff
changeset
|
195 |
val vampire_config : prover_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
|
196 |
{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
|
197 |
required_execs = [], |
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38740
diff
changeset
|
198 |
arguments = fn complete => fn timeout => |
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38740
diff
changeset
|
199 |
("--mode casc -t " ^ string_of_int (to_secs 0 timeout) ^ |
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38740
diff
changeset
|
200 |
" --thanks Andrei --input_file") |
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38740
diff
changeset
|
201 |
|> not complete ? prefix "--sos on ", |
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38740
diff
changeset
|
202 |
has_incomplete_mode = true, |
37509
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
37506
diff
changeset
|
203 |
proof_delims = |
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
37506
diff
changeset
|
204 |
[("=========== Refutation ==========", |
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
37506
diff
changeset
|
205 |
"======= End of refutation ======="), |
38033 | 206 |
("% SZS output start Refutation", "% SZS output end Refutation"), |
207 |
("% 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
|
208 |
known_failures = |
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
37506
diff
changeset
|
209 |
[(Unprovable, "UNPROVABLE"), |
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
37506
diff
changeset
|
210 |
(IncompleteUnprovable, "CANNOT PROVE"), |
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
|
211 |
(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
|
212 |
(Unprovable, "Satisfiability detected"), |
38647
5500241da479
play with fudge factor + parse one more Vampire error
blanchet
parents:
38646
diff
changeset
|
213 |
(Unprovable, "Termination reason: Satisfiable"), |
38519 | 214 |
(VampireTooOld, "not a valid option")], |
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38740
diff
changeset
|
215 |
default_max_relevant = 400 (* FUDGE *), |
38631
979a0b37f981
prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible;
blanchet
parents:
38603
diff
changeset
|
216 |
explicit_forall = false, |
38680 | 217 |
use_conjecture_for_hypotheses = true} |
38454
9043eefe8d71
detect old Vampire and give a nicer error message
blanchet
parents:
38433
diff
changeset
|
218 |
|
38023 | 219 |
val vampire = ("vampire", vampire_config) |
37509
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
37506
diff
changeset
|
220 |
|
38454
9043eefe8d71
detect old Vampire and give a nicer error message
blanchet
parents:
38433
diff
changeset
|
221 |
|
37509
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
37506
diff
changeset
|
222 |
(* Remote prover invocation via SystemOnTPTP *) |
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
223 |
|
38061
685d1f0f75b3
handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents:
38049
diff
changeset
|
224 |
val systems = Synchronized.var "atp_systems" ([] : string list) |
31835 | 225 |
|
226 |
fun get_systems () = |
|
38061
685d1f0f75b3
handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents:
38049
diff
changeset
|
227 |
case bash_output "\"$ISABELLE_ATP/scripts/remote_atp\" -w 2>&1" of |
36370
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
228 |
(answer, 0) => split_lines answer |
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
229 |
| (answer, _) => |
38065 | 230 |
error (case known_failure_in_output answer known_perl_failures of |
231 |
SOME failure => string_for_failure failure |
|
232 |
| NONE => perhaps (try (unsuffix "\n")) answer ^ ".") |
|
31835 | 233 |
|
35867 | 234 |
fun refresh_systems_on_tptp () = |
37509
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
37506
diff
changeset
|
235 |
Synchronized.change systems (fn _ => get_systems ()) |
31835 | 236 |
|
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
|
237 |
fun find_system name [] systems = find_first (String.isPrefix name) 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
|
238 |
| 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
|
239 |
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
|
240 |
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
|
241 |
| 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
|
242 |
|
38a926e033ad
make remote ATP versions more robust, by starting with "preferred" version numbers and falling back on any version
blanchet
parents:
38685
diff
changeset
|
243 |
fun get_system name versions = |
38589
b03f8fe043ec
added "max_relevant_per_iter" option to Sledgehammer
blanchet
parents:
38588
diff
changeset
|
244 |
Synchronized.change_result systems |
b03f8fe043ec
added "max_relevant_per_iter" option to Sledgehammer
blanchet
parents:
38588
diff
changeset
|
245 |
(fn systems => (if null systems then get_systems () else 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
|
246 |
|> `(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
|
247 |
|
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
|
248 |
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
|
249 |
case get_system name versions of |
39010 | 250 |
SOME sys => sys |
251 |
| NONE => error ("System " ^ quote name ^ " not available at SystemOnTPTP.") |
|
31835 | 252 |
|
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
|
253 |
fun remote_config system_name system_versions proof_delims known_failures |
38997 | 254 |
default_max_relevant use_conjecture_for_hypotheses |
255 |
: prover_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
|
256 |
{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
|
257 |
required_execs = [], |
37514
b147d01b8ebc
if SPASS fails at finding a proof with the SOS option turned on, turn it off and try again
blanchet
parents:
37509
diff
changeset
|
258 |
arguments = fn _ => fn timeout => |
38737
bdcb23701448
better workaround for E's off-by-one-second issue
blanchet
parents:
38691
diff
changeset
|
259 |
" -t " ^ string_of_int (to_secs 0 timeout) ^ " -s " ^ |
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
|
260 |
the_system system_name system_versions, |
38645 | 261 |
has_incomplete_mode = false, |
36369
d2cd0d04b8e6
handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents:
36289
diff
changeset
|
262 |
proof_delims = insert (op =) tstp_proof_delims proof_delims, |
38061
685d1f0f75b3
handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents:
38049
diff
changeset
|
263 |
known_failures = |
685d1f0f75b3
handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents:
38049
diff
changeset
|
264 |
known_failures @ known_perl_failures @ |
38094 | 265 |
[(TimedOut, "says Timeout")], |
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38740
diff
changeset
|
266 |
default_max_relevant = default_max_relevant, |
38631
979a0b37f981
prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible;
blanchet
parents:
38603
diff
changeset
|
267 |
explicit_forall = true, |
979a0b37f981
prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible;
blanchet
parents:
38603
diff
changeset
|
268 |
use_conjecture_for_hypotheses = use_conjecture_for_hypotheses} |
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
269 |
|
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
|
270 |
fun remotify_config system_name system_versions |
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38740
diff
changeset
|
271 |
({proof_delims, known_failures, default_max_relevant, |
38997 | 272 |
use_conjecture_for_hypotheses, ...} : prover_config) : prover_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
|
273 |
remote_config system_name system_versions proof_delims known_failures |
38997 | 274 |
default_max_relevant use_conjecture_for_hypotheses |
38023 | 275 |
|
38598 | 276 |
val remotify_name = prefix "remote_" |
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
|
277 |
fun remote_prover name system_name system_versions proof_delims known_failures |
38997 | 278 |
default_max_relevant use_conjecture_for_hypotheses = |
38598 | 279 |
(remotify_name 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
|
280 |
remote_config system_name system_versions proof_delims known_failures |
38997 | 281 |
default_max_relevant use_conjecture_for_hypotheses) |
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
|
282 |
fun remotify_prover (name, config) system_name system_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
|
283 |
(remotify_name name, remotify_config system_name system_versions config) |
28592 | 284 |
|
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
|
285 |
val remote_e = remotify_prover e "EP" ["1.0", "1.1", "1.2"] |
38817 | 286 |
val remote_vampire = remotify_prover vampire "Vampire" ["9.0", "1.0", "0.6"] |
38603
a57d04dd1b25
fix SInE's error handling + run "vampire" locally if either SPASS or E is missing
blanchet
parents:
38598
diff
changeset
|
287 |
val remote_sine_e = |
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38740
diff
changeset
|
288 |
remote_prover "sine_e" "SInE" [] [] [(Unprovable, "says Unknown")] |
38999 | 289 |
800 (* FUDGE *) true |
38598 | 290 |
val remote_snark = |
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
|
291 |
remote_prover "snark" "SNARK---" [] [("refutation.", "end_refutation.")] [] |
38997 | 292 |
350 (* FUDGE *) true |
38454
9043eefe8d71
detect old Vampire and give a nicer error message
blanchet
parents:
38433
diff
changeset
|
293 |
|
9043eefe8d71
detect old Vampire and give a nicer error message
blanchet
parents:
38433
diff
changeset
|
294 |
(* Setup *) |
9043eefe8d71
detect old Vampire and give a nicer error message
blanchet
parents:
38433
diff
changeset
|
295 |
|
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
|
296 |
fun is_installed ({exec, required_execs, ...} : prover_config) = |
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
|
297 |
forall (curry (op <>) "" o getenv o fst) (exec :: required_execs) |
38041
3b80d6082131
remove "remote_spass" because there's no way to find out which clauses come from which facts + rename scripts
blanchet
parents:
38033
diff
changeset
|
298 |
fun maybe_remote (name, config) = |
38598 | 299 |
name |> not (is_installed config) ? remotify_name |
36371
8c83ea1a7740
move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents:
36370
diff
changeset
|
300 |
|
8c83ea1a7740
move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents:
36370
diff
changeset
|
301 |
fun default_atps_param_value () = |
38041
3b80d6082131
remove "remote_spass" because there's no way to find out which clauses come from which facts + rename scripts
blanchet
parents:
38033
diff
changeset
|
302 |
space_implode " " ([maybe_remote e] @ |
3b80d6082131
remove "remote_spass" because there's no way to find out which clauses come from which facts + rename scripts
blanchet
parents:
38033
diff
changeset
|
303 |
(if is_installed (snd spass) then [fst spass] else []) @ |
38603
a57d04dd1b25
fix SInE's error handling + run "vampire" locally if either SPASS or E is missing
blanchet
parents:
38598
diff
changeset
|
304 |
[if forall (is_installed o snd) [e, spass] then |
a57d04dd1b25
fix SInE's error handling + run "vampire" locally if either SPASS or E is missing
blanchet
parents:
38598
diff
changeset
|
305 |
remotify_name (fst vampire) |
a57d04dd1b25
fix SInE's error handling + run "vampire" locally if either SPASS or E is missing
blanchet
parents:
38598
diff
changeset
|
306 |
else |
a57d04dd1b25
fix SInE's error handling + run "vampire" locally if either SPASS or E is missing
blanchet
parents:
38598
diff
changeset
|
307 |
maybe_remote vampire, |
a57d04dd1b25
fix SInE's error handling + run "vampire" locally if either SPASS or E is missing
blanchet
parents:
38598
diff
changeset
|
308 |
fst remote_sine_e]) |
36371
8c83ea1a7740
move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents:
36370
diff
changeset
|
309 |
|
38598 | 310 |
val provers = [e, spass, vampire, remote_e, remote_vampire, remote_sine_e, |
311 |
remote_snark] |
|
38023 | 312 |
val setup = fold add_prover provers |
35867 | 313 |
|
28592 | 314 |
end; |