author  blanchet 
Wed, 03 Nov 2010 23:01:30 +0100  
changeset 40344  df25b51af013 
parent 40060  5ef6747aa619 
child 40426  339f56417109 
permissions  rwrr 
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 
39491
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39375
diff
changeset

10 
type failure = ATP_Proof.failure 
38023  11 

40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

12 
type atp_config = 
38092
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38090
diff
changeset

13 
{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

14 
required_execs: (string * string) list, 
38023  15 
arguments: bool > Time.time > string, 
38645  16 
has_incomplete_mode: bool, 
38023  17 
proof_delims: (string * string) list, 
18 
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

19 
default_max_relevant: int, 
38631
979a0b37f981
prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible;
blanchet
parents:
38603
diff
changeset

20 
explicit_forall: bool, 
979a0b37f981
prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible;
blanchet
parents:
38603
diff
changeset

21 
use_conjecture_for_hypotheses: bool} 
38023  22 

40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

23 
val eN : string 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

24 
val spassN : string 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

25 
val vampireN : string 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

26 
val sine_eN : string 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

27 
val snarkN : string 
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

28 
val remote_prefix : string 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

29 
val add_atp : string * atp_config > theory > theory 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

30 
val get_atp : theory > string > atp_config 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

31 
val available_atps : theory > string list 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

32 
val is_atp_installed : theory > string > bool 
35867  33 
val refresh_systems_on_tptp : unit > unit 
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 

39491
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39375
diff
changeset

40 
open ATP_Proof 
32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

41 

40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

42 
(* ATP configuration *) 
32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

43 

40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

44 
type atp_config = 
38092
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38090
diff
changeset

45 
{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

46 
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

47 
arguments: bool > Time.time > string, 
38645  48 
has_incomplete_mode: bool, 
36370
a4f601daa175
centralized ATPspecific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset

49 
proof_delims: (string * string) list, 
a4f601daa175
centralized ATPspecific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset

50 
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

51 
default_max_relevant: int, 
38631
979a0b37f981
prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible;
blanchet
parents:
38603
diff
changeset

52 
explicit_forall: bool, 
979a0b37f981
prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible;
blanchet
parents:
38603
diff
changeset

53 
use_conjecture_for_hypotheses: bool} 
28596
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

54 

38061
685d1f0f75b3
handle Perl and "libwwwperl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents:
38049
diff
changeset

55 
val known_perl_failures = 
38094  56 
[(CantConnect, "HTTP error"), 
57 
(NoPerl, "env: perl"), 

38065  58 
(NoLibwwwPerl, "Can't locate HTTP")] 
28596
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

59 

40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

60 
(* named ATPs *) 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

61 

6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

62 
val eN = "e" 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

63 
val spassN = "spass" 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

64 
val vampireN = "vampire" 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

65 
val sine_eN = "sine_e" 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

66 
val snarkN = "snark" 
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

67 
val remote_prefix = "remote_" 
38001
a9b47b85ca24
reintroduced more preprocessing steps to Sledgehammer, adapted to the new FOF setting
blanchet
parents:
38000
diff
changeset

68 

38023  69 
structure Data = Theory_Data 
70 
( 

40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

71 
type T = (atp_config * stamp) Symtab.table 
38023  72 
val empty = Symtab.empty 
73 
val extend = I 

74 
fun merge data : T = Symtab.merge (eq_snd op =) data 

75 
handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".") 

76 
) 

38017
3ad3e3ca2451
move Sledgehammerspecific code out of "Sledgehammer_TPTP_Format"
blanchet
parents:
38015
diff
changeset

77 

38737
bdcb23701448
better workaround for E's offbyonesecond issue
blanchet
parents:
38691
diff
changeset

78 
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

79 

39491
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39375
diff
changeset

80 

40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

81 
(* E *) 
28596
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

82 

40344
df25b51af013
give E one more second, to prevent cases where it finds a proof but has no time to print it
blanchet
parents:
40060
diff
changeset

83 
(* Give E an extra second to reconstruct the proof. Older versions even get two 
df25b51af013
give E one more second, to prevent cases where it finds a proof but has no time to print it
blanchet
parents:
40060
diff
changeset

84 
seconds, because the "eproof" script wrongly subtracted an entire second to 
df25b51af013
give E one more second, to prevent cases where it finds a proof but has no time to print it
blanchet
parents:
40060
diff
changeset

85 
account for the overhead of the script itself, which is in fact much 
df25b51af013
give E one more second, to prevent cases where it finds a proof but has no time to print it
blanchet
parents:
40060
diff
changeset

86 
lower. *) 
38737
bdcb23701448
better workaround for E's offbyonesecond issue
blanchet
parents:
38691
diff
changeset

87 
fun e_bonus () = 
bdcb23701448
better workaround for E's offbyonesecond issue
blanchet
parents:
38691
diff
changeset

88 
case getenv "E_VERSION" of 
40344
df25b51af013
give E one more second, to prevent cases where it finds a proof but has no time to print it
blanchet
parents:
40060
diff
changeset

89 
"" => 2000 
38737
bdcb23701448
better workaround for E's offbyonesecond issue
blanchet
parents:
38691
diff
changeset

90 
 version => 
40344
df25b51af013
give E one more second, to prevent cases where it finds a proof but has no time to print it
blanchet
parents:
40060
diff
changeset

91 
if exists (fn s => String.isPrefix s version) ["0.9", "1.0"] then 2000 
df25b51af013
give E one more second, to prevent cases where it finds a proof but has no time to print it
blanchet
parents:
40060
diff
changeset

92 
else 1000 
38737
bdcb23701448
better workaround for E's offbyonesecond issue
blanchet
parents:
38691
diff
changeset

93 

36369
d2cd0d04b8e6
handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents:
36289
diff
changeset

94 
val tstp_proof_delims = 
d2cd0d04b8e6
handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents:
36289
diff
changeset

95 
("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation") 
d2cd0d04b8e6
handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents:
36289
diff
changeset

96 

40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

97 
val e_config : atp_config = 
38092
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38090
diff
changeset

98 
{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

99 
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

100 
arguments = fn _ => fn timeout => 
38691  101 
"tstpin tstpout l5 xAutoDev tAutoDev silent \ 
38737
bdcb23701448
better workaround for E's offbyonesecond issue
blanchet
parents:
38691
diff
changeset

102 
\cpulimit=" ^ string_of_int (to_secs (e_bonus ()) timeout), 
38645  103 
has_incomplete_mode = false, 
36369
d2cd0d04b8e6
handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents:
36289
diff
changeset

104 
proof_delims = [tstp_proof_delims], 
36265
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

105 
known_failures = 
37995
06f02b15ef8a
generate full firstorder formulas (FOF) in Sledgehammer
blanchet
parents:
37994
diff
changeset

106 
[(Unprovable, "SZS status: CounterSatisfiable"), 
06f02b15ef8a
generate full firstorder formulas (FOF) in Sledgehammer
blanchet
parents:
37994
diff
changeset

107 
(Unprovable, "SZS status CounterSatisfiable"), 
36370
a4f601daa175
centralized ATPspecific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset

108 
(TimedOut, "Failure: Resource limit exceeded (time)"), 
a4f601daa175
centralized ATPspecific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset

109 
(TimedOut, "time limit exceeded"), 
a4f601daa175
centralized ATPspecific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset

110 
(OutOfResources, 
a4f601daa175
centralized ATPspecific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset

111 
"# Cannot determine problem status within resource limit"), 
a4f601daa175
centralized ATPspecific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset

112 
(OutOfResources, "SZS status: ResourceOut"), 
a4f601daa175
centralized ATPspecific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset

113 
(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

114 
default_max_relevant = 500 (* FUDGE *), 
38631
979a0b37f981
prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible;
blanchet
parents:
38603
diff
changeset

115 
explicit_forall = false, 
979a0b37f981
prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible;
blanchet
parents:
38603
diff
changeset

116 
use_conjecture_for_hypotheses = true} 
38454
9043eefe8d71
detect old Vampire and give a nicer error message
blanchet
parents:
38433
diff
changeset

117 

40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

118 
val e = (eN, e_config) 
28596
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

119 

fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

120 

39491
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39375
diff
changeset

121 
(* SPASS *) 
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39375
diff
changeset

122 

36219
16670b4f0baa
set SPASS option on the commandline, so that it doesn't vanish when moving to TPTP format
blanchet
parents:
36190
diff
changeset

123 
(* The "VarWeight=3" option helps the higherorder problems, probably by 
16670b4f0baa
set SPASS option on the commandline, so that it doesn't vanish when moving to TPTP format
blanchet
parents:
36190
diff
changeset

124 
counteracting the presence of "hAPP". *) 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

125 
val spass_config : atp_config = 
38092
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38090
diff
changeset

126 
{exec = ("ISABELLE_ATP", "scripts/spass"), 
39002  127 
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

128 
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

129 
("Auto PGiven=0 PProblem=0 Splits=0 FullRed=0 DocProof \ 
38737
bdcb23701448
better workaround for E's offbyonesecond issue
blanchet
parents:
38691
diff
changeset

130 
\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

131 
> not complete ? prefix "SOS=1 ", 
38645  132 
has_incomplete_mode = true, 
36369
d2cd0d04b8e6
handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents:
36289
diff
changeset

133 
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

134 
known_failures = 
38061
685d1f0f75b3
handle Perl and "libwwwperl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents:
38049
diff
changeset

135 
known_perl_failures @ 
37413  136 
[(IncompleteUnprovable, "SPASS beiseite: Completion found"), 
36370
a4f601daa175
centralized ATPspecific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset

137 
(TimedOut, "SPASS beiseite: Ran out of time"), 
36965  138 
(OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"), 
37413  139 
(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

140 
(MalformedInput, "Free Variable"), 
39263
e2a3c435334b
more precise error messages when Vampire is interrupted or SPASS runs into an internal bug
blanchet
parents:
39262
diff
changeset

141 
(SpassTooOld, "tptp2dfg"), 
e2a3c435334b
more precise error messages when Vampire is interrupted or SPASS runs into an internal bug
blanchet
parents:
39262
diff
changeset

142 
(InternalError, "Please report this error")], 
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38740
diff
changeset

143 
default_max_relevant = 350 (* FUDGE *), 
38631
979a0b37f981
prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible;
blanchet
parents:
38603
diff
changeset

144 
explicit_forall = true, 
979a0b37f981
prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible;
blanchet
parents:
38603
diff
changeset

145 
use_conjecture_for_hypotheses = true} 
38454
9043eefe8d71
detect old Vampire and give a nicer error message
blanchet
parents:
38433
diff
changeset

146 

40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

147 
val spass = (spassN, spass_config) 
28596
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

148 

38454
9043eefe8d71
detect old Vampire and give a nicer error message
blanchet
parents:
38433
diff
changeset

149 

37509
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
37506
diff
changeset

150 
(* Vampire *) 
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
37506
diff
changeset

151 

40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

152 
val vampire_config : atp_config = 
38092
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38090
diff
changeset

153 
{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

154 
required_execs = [], 
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38740
diff
changeset

155 
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

156 
("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

157 
" thanks Andrei input_file") 
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38740
diff
changeset

158 
> 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

159 
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

160 
proof_delims = 
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
37506
diff
changeset

161 
[("=========== Refutation ==========", 
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
37506
diff
changeset

162 
"======= End of refutation ======="), 
38033  163 
("% SZS output start Refutation", "% SZS output end Refutation"), 
164 
("% 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

165 
known_failures = 
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
37506
diff
changeset

166 
[(Unprovable, "UNPROVABLE"), 
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
37506
diff
changeset

167 
(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

168 
(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

169 
(Unprovable, "Satisfiability detected"), 
38647
5500241da479
play with fudge factor + parse one more Vampire error
blanchet
parents:
38646
diff
changeset

170 
(Unprovable, "Termination reason: Satisfiable"), 
39263
e2a3c435334b
more precise error messages when Vampire is interrupted or SPASS runs into an internal bug
blanchet
parents:
39262
diff
changeset

171 
(VampireTooOld, "not a valid option"), 
e2a3c435334b
more precise error messages when Vampire is interrupted or SPASS runs into an internal bug
blanchet
parents:
39262
diff
changeset

172 
(Interrupted, "Aborted by signal SIGINT")], 
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38740
diff
changeset

173 
default_max_relevant = 400 (* FUDGE *), 
38631
979a0b37f981
prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible;
blanchet
parents:
38603
diff
changeset

174 
explicit_forall = false, 
38680  175 
use_conjecture_for_hypotheses = true} 
38454
9043eefe8d71
detect old Vampire and give a nicer error message
blanchet
parents:
38433
diff
changeset

176 

40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

177 
val vampire = (vampireN, vampire_config) 
37509
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
37506
diff
changeset

178 

38454
9043eefe8d71
detect old Vampire and give a nicer error message
blanchet
parents:
38433
diff
changeset

179 

40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

180 
(* Remote ATP invocation via SystemOnTPTP *) 
28596
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

181 

38061
685d1f0f75b3
handle Perl and "libwwwperl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents:
38049
diff
changeset

182 
val systems = Synchronized.var "atp_systems" ([] : string list) 
31835  183 

184 
fun get_systems () = 

38061
685d1f0f75b3
handle Perl and "libwwwperl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents:
38049
diff
changeset

185 
case bash_output "\"$ISABELLE_ATP/scripts/remote_atp\" w 2>&1" of 
39491
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39375
diff
changeset

186 
(output, 0) => split_lines output 
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39375
diff
changeset

187 
 (output, _) => 
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39375
diff
changeset

188 
error (case extract_known_failure known_perl_failures output of 
38065  189 
SOME failure => string_for_failure failure 
39491
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39375
diff
changeset

190 
 NONE => perhaps (try (unsuffix "\n")) output ^ ".") 
31835  191 

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

192 
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

193 
 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

194 
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

195 
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

196 
 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

197 

38a926e033ad
make remote ATP versions more robust, by starting with "preferred" version numbers and falling back on any version
blanchet
parents:
38685
diff
changeset

198 
fun get_system name versions = 
38589
b03f8fe043ec
added "max_relevant_per_iter" option to Sledgehammer
blanchet
parents:
38588
diff
changeset

199 
Synchronized.change_result systems 
b03f8fe043ec
added "max_relevant_per_iter" option to Sledgehammer
blanchet
parents:
38588
diff
changeset

200 
(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

201 
> `(find_system name versions)) 
32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

202 

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

203 
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

204 
case get_system name versions of 
39010  205 
SOME sys => sys 
206 
 NONE => error ("System " ^ quote name ^ " not available at SystemOnTPTP.") 

31835  207 

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

208 
fun remote_config system_name system_versions proof_delims known_failures 
38997  209 
default_max_relevant use_conjecture_for_hypotheses 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

210 
: atp_config = 
38092
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38090
diff
changeset

211 
{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

212 
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

213 
arguments = fn _ => fn timeout => 
38737
bdcb23701448
better workaround for E's offbyonesecond issue
blanchet
parents:
38691
diff
changeset

214 
" 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

215 
the_system system_name system_versions, 
38645  216 
has_incomplete_mode = false, 
36369
d2cd0d04b8e6
handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents:
36289
diff
changeset

217 
proof_delims = insert (op =) tstp_proof_delims proof_delims, 
38061
685d1f0f75b3
handle Perl and "libwwwperl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents:
38049
diff
changeset

218 
known_failures = 
685d1f0f75b3
handle Perl and "libwwwperl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents:
38049
diff
changeset

219 
known_failures @ known_perl_failures @ 
38094  220 
[(TimedOut, "says Timeout")], 
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38740
diff
changeset

221 
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

222 
explicit_forall = true, 
979a0b37f981
prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible;
blanchet
parents:
38603
diff
changeset

223 
use_conjecture_for_hypotheses = use_conjecture_for_hypotheses} 
28596
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

224 

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

225 
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

226 
({proof_delims, known_failures, default_max_relevant, 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

227 
use_conjecture_for_hypotheses, ...} : atp_config) : atp_config = 
38690
38a926e033ad
make remote ATP versions more robust, by starting with "preferred" version numbers and falling back on any version
blanchet
parents:
38685
diff
changeset

228 
remote_config system_name system_versions proof_delims known_failures 
38997  229 
default_max_relevant use_conjecture_for_hypotheses 
38023  230 

40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

231 
fun remote_atp name system_name system_versions proof_delims known_failures 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

232 
default_max_relevant use_conjecture_for_hypotheses = 
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

233 
(remote_prefix ^ name, 
38690
38a926e033ad
make remote ATP versions more robust, by starting with "preferred" version numbers and falling back on any version
blanchet
parents:
38685
diff
changeset

234 
remote_config system_name system_versions proof_delims known_failures 
38997  235 
default_max_relevant use_conjecture_for_hypotheses) 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

236 
fun remotify_atp (name, config) system_name system_versions = 
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

237 
(remote_prefix ^ name, remotify_config system_name system_versions config) 
28592  238 

40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

239 
val remote_e = remotify_atp e "EP" ["1.0", "1.1", "1.2"] 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

240 
val remote_vampire = remotify_atp vampire "Vampire" ["0.6", "9.0", "1.0"] 
38603
a57d04dd1b25
fix SInE's error handling + run "vampire" locally if either SPASS or E is missing
blanchet
parents:
38598
diff
changeset

241 
val remote_sine_e = 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

242 
remote_atp sine_eN "SInE" [] [] [(IncompleteUnprovable, "says Unknown")] 
38999  243 
800 (* FUDGE *) true 
38598  244 
val remote_snark = 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

245 
remote_atp snarkN "SNARK" [] [("refutation.", "end_refutation.")] [] 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

246 
250 (* FUDGE *) true 
38454
9043eefe8d71
detect old Vampire and give a nicer error message
blanchet
parents:
38433
diff
changeset

247 

9043eefe8d71
detect old Vampire and give a nicer error message
blanchet
parents:
38433
diff
changeset

248 
(* Setup *) 
9043eefe8d71
detect old Vampire and give a nicer error message
blanchet
parents:
38433
diff
changeset

249 

40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

250 
fun add_atp (name, config) thy = 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

251 
Data.map (Symtab.update_new (name, (config, stamp ()))) thy 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

252 
handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".") 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

253 

6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

254 
fun get_atp thy name = 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

255 
the (Symtab.lookup (Data.get thy) name) > fst 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

256 
handle Option.Option => error ("Unknown ATP: " ^ name ^ ".") 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

257 

6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

258 
val available_atps = Symtab.keys o Data.get 
36371
8c83ea1a7740
move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents:
36370
diff
changeset

259 

40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

260 
fun is_atp_installed thy name = 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

261 
let val {exec, required_execs, ...} = get_atp thy name in 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

262 
forall (curry (op <>) "" o getenv o fst) (exec :: required_execs) 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

263 
end 
36371
8c83ea1a7740
move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents:
36370
diff
changeset

264 

40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

265 
fun refresh_systems_on_tptp () = 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

266 
Synchronized.change systems (fn _ => get_systems ()) 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

267 

6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

268 
val atps = [e, spass, vampire, remote_e, remote_vampire, remote_sine_e, 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

269 
remote_snark] 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

270 
val setup = fold add_atp atps 
35867  271 

28592  272 
end; 