author  blanchet 
Sun, 22 May 2011 14:51:42 +0200  
changeset 42944  9e620869a576 
parent 42943  62a14c80d194 
child 42953  26111aafab12 
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 
42577
78414ec6fa4e
made the format (TFF or FOF) of the TPTP problem a global argument of the problem again and have the ATPs report which formats they support
blanchet
parents:
42571
diff
changeset

10 
type format = ATP_Problem.format 
78414ec6fa4e
made the format (TFF or FOF) of the TPTP problem a global argument of the problem again and have the ATPs report which formats they support
blanchet
parents:
42571
diff
changeset

11 
type formula_kind = ATP_Problem.formula_kind 
39491
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39375
diff
changeset

12 
type failure = ATP_Proof.failure 
38023  13 

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

14 
type atp_config = 
42578
1eaf4d437d4c
define type system in ATP module so that ATPs can suggest a type system
blanchet
parents:
42577
diff
changeset

15 
{exec : string * string, 
1eaf4d437d4c
define type system in ATP module so that ATPs can suggest a type system
blanchet
parents:
42577
diff
changeset

16 
required_execs : (string * string) list, 
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

17 
arguments : 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

18 
Proof.context > int > Time.time > (unit > (string * real) list) 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

19 
> string, 
42578
1eaf4d437d4c
define type system in ATP module so that ATPs can suggest a type system
blanchet
parents:
42577
diff
changeset

20 
proof_delims : (string * string) list, 
1eaf4d437d4c
define type system in ATP module so that ATPs can suggest a type system
blanchet
parents:
42577
diff
changeset

21 
known_failures : (failure * string) list, 
42709
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42708
diff
changeset

22 
conj_sym_kind : formula_kind, 
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42708
diff
changeset

23 
prem_kind : formula_kind, 
42578
1eaf4d437d4c
define type system in ATP module so that ATPs can suggest a type system
blanchet
parents:
42577
diff
changeset

24 
formats : format list, 
42723  25 
best_slices : Proof.context > (real * (bool * (int * string list))) list} 
38023  26 

42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

27 
val e_weight_method : string Config.T 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

28 
val e_default_fun_weight : real Config.T 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

29 
val e_fun_weight_base : real Config.T 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

30 
val e_fun_weight_span : real Config.T 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

31 
val e_default_sym_offs_weight : real Config.T 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

32 
val e_sym_offs_weight_base : real Config.T 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

33 
val e_sym_offs_weight_span : real Config.T 
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

34 
val spass_force_sos : bool Config.T 
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

35 
val vampire_force_sos : bool Config.T 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

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

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

38 
val vampireN : string 
42535
3c1f302b3ee6
added support for ToFoF prover for experimenting with the TPTP TFF (typed firstorder) format
blanchet
parents:
42521
diff
changeset

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

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

41 
val snarkN : string 
42938  42 
val waldmeisterN : string 
41738
eb98c60a6cf0
added experimental "remote_z3_atp", Sutcliffe's TPTPsyntaxaware wrapper for Z3  allows to do headtohead comparison of Sledgehammer's ATP translation and of Sascha's SMT translation
blanchet
parents:
41727
diff
changeset

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

44 
val remote_prefix : string 
41738
eb98c60a6cf0
added experimental "remote_z3_atp", Sutcliffe's TPTPsyntaxaware wrapper for Z3  allows to do headtohead comparison of Sledgehammer's ATP translation and of Sascha's SMT translation
blanchet
parents:
41727
diff
changeset

45 
val remote_atp : 
eb98c60a6cf0
added experimental "remote_z3_atp", Sutcliffe's TPTPsyntaxaware wrapper for Z3  allows to do headtohead comparison of Sledgehammer's ATP translation and of Sascha's SMT translation
blanchet
parents:
41727
diff
changeset

46 
string > string > string list > (string * string) list 
42709
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42708
diff
changeset

47 
> (failure * string) list > formula_kind > formula_kind > format list 
42723  48 
> (Proof.context > int * string list) > string * atp_config 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

49 
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

50 
val get_atp : theory > string > atp_config 
41727
ab3f6d76fb23
available_provers ~> supported_provers (for clarity)
blanchet
parents:
41725
diff
changeset

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

52 
val is_atp_installed : theory > string > bool 
35867  53 
val refresh_systems_on_tptp : unit > unit 
54 
val setup : theory > theory 

28592  55 
end; 
56 

36376  57 
structure ATP_Systems : ATP_SYSTEMS = 
28592  58 
struct 
28596
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

59 

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

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

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

62 

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

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

64 

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

65 
type atp_config = 
42578
1eaf4d437d4c
define type system in ATP module so that ATPs can suggest a type system
blanchet
parents:
42577
diff
changeset

66 
{exec : string * string, 
1eaf4d437d4c
define type system in ATP module so that ATPs can suggest a type system
blanchet
parents:
42577
diff
changeset

67 
required_execs : (string * string) list, 
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

68 
arguments : 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

69 
Proof.context > int > Time.time > (unit > (string * real) list) 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

70 
> string, 
42578
1eaf4d437d4c
define type system in ATP module so that ATPs can suggest a type system
blanchet
parents:
42577
diff
changeset

71 
proof_delims : (string * string) list, 
1eaf4d437d4c
define type system in ATP module so that ATPs can suggest a type system
blanchet
parents:
42577
diff
changeset

72 
known_failures : (failure * string) list, 
42709
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42708
diff
changeset

73 
conj_sym_kind : formula_kind, 
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42708
diff
changeset

74 
prem_kind : formula_kind, 
42578
1eaf4d437d4c
define type system in ATP module so that ATPs can suggest a type system
blanchet
parents:
42577
diff
changeset

75 
formats : format list, 
42723  76 
best_slices : Proof.context > (real * (bool * (int * string list))) list} 
28596
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

77 

42723  78 
(* "best_slices" must be found empirically, taking a wholistic approach since 
79 
the ATPs are run in parallel. The "real" components give the faction of the 

80 
time available given to the slice; these should add up to 1.0. The "bool" 

81 
component indicates whether the slice's strategy is complete; the "int", the 

82 
preferred number of facts to pass; the "string list", the preferred type 

83 
systems, which should be of the form [sound] or [unsound, sound], where 

84 
"sound" is a sound type system and "unsound" is an unsound one. 

85 

86 
The last slice should be the most "normal" one, because it will get all the 

87 
time available if the other slices fail early and also because it is used for 

88 
remote provers and if slicing is disabled. *) 

42710
84fcce345b5d
further improved type system setup based on Judgment Days
blanchet
parents:
42709
diff
changeset

89 

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

90 
val known_perl_failures = 
38094  91 
[(CantConnect, "HTTP error"), 
92 
(NoPerl, "env: perl"), 

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

94 

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

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

96 

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

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

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

99 
val vampireN = "vampire" 
41740
4b09f8b9e012
added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents:
41738
diff
changeset

100 
val z3_atpN = "z3_atp" 
42535
3c1f302b3ee6
added support for ToFoF prover for experimenting with the TPTP TFF (typed firstorder) format
blanchet
parents:
42521
diff
changeset

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

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

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

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

106 

38023  107 
structure Data = Theory_Data 
108 
( 

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

109 
type T = (atp_config * stamp) Symtab.table 
38023  110 
val empty = Symtab.empty 
111 
val extend = I 

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

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

114 
) 

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

115 

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

116 
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

117 

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

118 

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

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

120 

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

121 
(* 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

122 
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

123 
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

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

125 
fun e_bonus () = 
41334
3cb52cbf0eed
enable E weight generation with unofficial latest version of E (tentatively called E 1.2B)  backed by Judgment Day
blanchet
parents:
41317
diff
changeset

126 
if string_ord (getenv "E_VERSION", "1.1") = LESS then 2000 else 1000 
38737
bdcb23701448
better workaround for E's offbyonesecond issue
blanchet
parents:
38691
diff
changeset

127 

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

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

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

130 

42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

131 
val e_slicesN = "slices" 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

132 
val e_autoN = "auto" 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

133 
val e_fun_weightN = "fun_weight" 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

134 
val e_sym_offset_weightN = "sym_offset_weight" 
41725
7cca2de89296
added support for bleedingedge E weighting function "SymOffsetsWeight"
blanchet
parents:
41335
diff
changeset

135 

42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

136 
val e_weight_method = 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

137 
Attrib.setup_config_string @{binding atp_e_weight_method} (K e_slicesN) 
41770  138 
(* FUDGE *) 
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

139 
val e_default_fun_weight = 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

140 
Attrib.setup_config_real @{binding atp_e_default_fun_weight} (K 20.0) 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

141 
val e_fun_weight_base = 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

142 
Attrib.setup_config_real @{binding atp_e_fun_weight_base} (K 0.0) 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

143 
val e_fun_weight_span = 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

144 
Attrib.setup_config_real @{binding atp_e_fun_weight_span} (K 40.0) 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

145 
val e_default_sym_offs_weight = 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

146 
Attrib.setup_config_real @{binding atp_e_default_sym_offs_weight} (K 1.0) 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

147 
val e_sym_offs_weight_base = 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

148 
Attrib.setup_config_real @{binding atp_e_sym_offs_weight_base} (K ~20.0) 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

149 
val e_sym_offs_weight_span = 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

150 
Attrib.setup_config_real @{binding atp_e_sym_offs_weight_span} (K 60.0) 
41725
7cca2de89296
added support for bleedingedge E weighting function "SymOffsetsWeight"
blanchet
parents:
41335
diff
changeset

151 

42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42332
diff
changeset

152 
fun e_weight_method_case method fw sow = 
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

153 
if method = e_fun_weightN then fw 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

154 
else if method = e_sym_offset_weightN then sow 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

155 
else raise Fail ("unexpected" ^ quote method) 
41725
7cca2de89296
added support for bleedingedge E weighting function "SymOffsetsWeight"
blanchet
parents:
41335
diff
changeset

156 

42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

157 
fun scaled_e_weight ctxt method w = 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

158 
w * Config.get ctxt 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

159 
(e_weight_method_case method e_fun_weight_span e_sym_offs_weight_span) 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

160 
+ Config.get ctxt 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

161 
(e_weight_method_case method e_fun_weight_base e_sym_offs_weight_base) 
41725
7cca2de89296
added support for bleedingedge E weighting function "SymOffsetsWeight"
blanchet
parents:
41335
diff
changeset

162 
> Real.ceil > signed_string_of_int 
41313
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41269
diff
changeset

163 

42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

164 
fun e_weight_arguments ctxt method weights = 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

165 
if method = e_autoN then 
41725
7cca2de89296
added support for bleedingedge E weighting function "SymOffsetsWeight"
blanchet
parents:
41335
diff
changeset

166 
"xAutoDev" 
7cca2de89296
added support for bleedingedge E weighting function "SymOffsetsWeight"
blanchet
parents:
41335
diff
changeset

167 
else 
41314
2dc1dfc1bc69
use the options provided by Stephan Schulz  much better
blanchet
parents:
41313
diff
changeset

168 
"splitclauses=4 splitreusedefs simulparamod forwardcontextsr \ 
2dc1dfc1bc69
use the options provided by Stephan Schulz  much better
blanchet
parents:
41313
diff
changeset

169 
\destructiveeraggressive destructiveer presatsimplify \ 
2dc1dfc1bc69
use the options provided by Stephan Schulz  much better
blanchet
parents:
41313
diff
changeset

170 
\preferinitialclauses tKBO6 winvfreqrank c1 Ginvfreqconjmax F1 \ 
2dc1dfc1bc69
use the options provided by Stephan Schulz  much better
blanchet
parents:
41313
diff
changeset

171 
\deletebadlimit=150000000 WSelectMaxLComplexAvoidPosPred \ 
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42332
diff
changeset

172 
\H'(4*" ^ e_weight_method_case method "FunWeight" "SymOffsetWeight" ^ 
41725
7cca2de89296
added support for bleedingedge E weighting function "SymOffsetsWeight"
blanchet
parents:
41335
diff
changeset

173 
"(SimulateSOS, " ^ 
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

174 
(e_weight_method_case method e_default_fun_weight e_default_sym_offs_weight 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

175 
> Config.get ctxt > Real.ceil > signed_string_of_int) ^ 
41314
2dc1dfc1bc69
use the options provided by Stephan Schulz  much better
blanchet
parents:
41313
diff
changeset

176 
",20,1.5,1.5,1" ^ 
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

177 
(weights () 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

178 
> map (fn (s, w) => "," ^ s ^ ":" ^ scaled_e_weight ctxt method w) 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

179 
> implode) ^ 
41314
2dc1dfc1bc69
use the options provided by Stephan Schulz  much better
blanchet
parents:
41313
diff
changeset

180 
"),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,\ 
2dc1dfc1bc69
use the options provided by Stephan Schulz  much better
blanchet
parents:
41313
diff
changeset

181 
\1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*\ 
2dc1dfc1bc69
use the options provided by Stephan Schulz  much better
blanchet
parents:
41313
diff
changeset

182 
\FIFOWeight(PreferProcessed))'" 
41313
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41269
diff
changeset

183 

42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42332
diff
changeset

184 
fun is_old_e_version () = (string_ord (getenv "E_VERSION", "1.2w") = LESS) 
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42332
diff
changeset

185 

42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

186 
fun effective_e_weight_method ctxt = 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

187 
if is_old_e_version () then e_autoN else Config.get ctxt e_weight_method 
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42332
diff
changeset

188 

724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42332
diff
changeset

189 
(* The order here must correspond to the order in "e_config" below. *) 
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

190 
fun method_for_slice ctxt slice = 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

191 
let val method = effective_e_weight_method ctxt in 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

192 
if method = e_slicesN then 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

193 
case slice of 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

194 
0 => e_sym_offset_weightN 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

195 
 1 => e_autoN 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

196 
 2 => e_fun_weightN 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

197 
 _ => raise Fail "no such slice" 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

198 
else 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

199 
method 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

200 
end 
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42332
diff
changeset

201 

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

202 
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

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

204 
required_execs = [], 
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

205 
arguments = fn ctxt => fn slice => fn timeout => fn weights => 
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42332
diff
changeset

206 
"tstpin tstpout l5 " ^ 
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

207 
e_weight_arguments ctxt (method_for_slice ctxt slice) weights ^ 
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42332
diff
changeset

208 
" tAutoDev silent cpulimit=" ^ 
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42332
diff
changeset

209 
string_of_int (to_secs (e_bonus ()) timeout), 
36369
d2cd0d04b8e6
handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents:
36289
diff
changeset

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

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

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

213 
(Unprovable, "SZS status CounterSatisfiable"), 
42844
f133c030856a
better error reporting: detect missing E proofs and remove Vampire native format error
blanchet
parents:
42779
diff
changeset

214 
(ProofMissing, "SZS status Theorem"), 
36370
a4f601daa175
centralized ATPspecific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset

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

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

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

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

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

220 
(OutOfResources, "SZS status ResourceOut")], 
42709
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42708
diff
changeset

221 
conj_sym_kind = Conjecture, (* FIXME: try out Hypothesis *) 
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42708
diff
changeset

222 
prem_kind = Conjecture, 
42937  223 
formats = [FOF], 
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

224 
best_slices = fn ctxt => 
42723  225 
(* FUDGE *) 
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

226 
if effective_e_weight_method ctxt = e_slicesN then 
42853
de1fe9eaf3f4
tweaked ATP type systems further based on Judgment Day
blanchet
parents:
42844
diff
changeset

227 
[(0.333, (true, (100, ["poly_preds"]))) (* sym_offset_weight *), 
de1fe9eaf3f4
tweaked ATP type systems further based on Judgment Day
blanchet
parents:
42844
diff
changeset

228 
(0.333, (true, (800, ["mangled_preds_heavy"]))) (* auto *), 
de1fe9eaf3f4
tweaked ATP type systems further based on Judgment Day
blanchet
parents:
42844
diff
changeset

229 
(0.334, (true, (200, ["mangled_tags!", "mangled_tags?"]))) 
de1fe9eaf3f4
tweaked ATP type systems further based on Judgment Day
blanchet
parents:
42844
diff
changeset

230 
(* fun_weight *)] 
42578
1eaf4d437d4c
define type system in ATP module so that ATPs can suggest a type system
blanchet
parents:
42577
diff
changeset

231 
else 
42853
de1fe9eaf3f4
tweaked ATP type systems further based on Judgment Day
blanchet
parents:
42844
diff
changeset

232 
[(1.0, (true, (200, ["mangled_tags!", "mangled_tags?"])))]} 
38454
9043eefe8d71
detect old Vampire and give a nicer error message
blanchet
parents:
38433
diff
changeset

233 

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

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

235 

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

236 

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

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

238 

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

239 
val spass_force_sos = 
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

240 
Attrib.setup_config_bool @{binding atp_spass_force_sos} (K false) 
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

241 

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

242 
(* 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

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

244 
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

245 
{exec = ("ISABELLE_ATP", "scripts/spass"), 
39002  246 
required_execs = [("SPASS_HOME", "SPASS"), ("SPASS_HOME", "tptp2dfg")], 
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

247 
arguments = fn ctxt => fn slice => fn timeout => fn _ => 
37962
d7dbe01f48d7
keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems;
blanchet
parents:
37926
diff
changeset

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

249 
\VarWeight=3 TimeLimit=" ^ string_of_int (to_secs 0 timeout)) 
42853
de1fe9eaf3f4
tweaked ATP type systems further based on Judgment Day
blanchet
parents:
42844
diff
changeset

250 
> (slice < 2 orelse Config.get ctxt spass_force_sos) ? prefix "SOS=1 ", 
36369
d2cd0d04b8e6
handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents:
36289
diff
changeset

251 
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

252 
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

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

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

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

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

260 
(InternalError, "Please report this error")], 
42709
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42708
diff
changeset

261 
conj_sym_kind = Axiom, (* FIXME: try out Hypothesis *) 
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42708
diff
changeset

262 
prem_kind = Conjecture, 
42937  263 
formats = [FOF], 
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

264 
best_slices = fn ctxt => 
42723  265 
(* FUDGE *) 
42853
de1fe9eaf3f4
tweaked ATP type systems further based on Judgment Day
blanchet
parents:
42844
diff
changeset

266 
[(0.333, (false, (150, ["mangled_preds_heavy"]))) (* SOS *), 
de1fe9eaf3f4
tweaked ATP type systems further based on Judgment Day
blanchet
parents:
42844
diff
changeset

267 
(0.333, (false, (150, ["mangled_preds?"]))) (* SOS *), 
de1fe9eaf3f4
tweaked ATP type systems further based on Judgment Day
blanchet
parents:
42844
diff
changeset

268 
(0.334, (true, (150, ["poly_preds"]))) (* ~SOS *)] 
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

269 
> (if Config.get ctxt spass_force_sos then hd #> apfst (K 1.0) #> single 
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

270 
else I)} 
38454
9043eefe8d71
detect old Vampire and give a nicer error message
blanchet
parents:
38433
diff
changeset

271 

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

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

273 

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

274 

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

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

276 

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

277 
val vampire_force_sos = 
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

278 
Attrib.setup_config_bool @{binding atp_vampire_force_sos} (K false) 
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

279 

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

280 
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

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

282 
required_execs = [], 
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

283 
arguments = fn ctxt => fn slice => fn timeout => fn _ => 
42748
a37095d03074
drop support for Vampire's native output format  it has too many undocumented oddities, e.g. "BDD definition:" lines
blanchet
parents:
42725
diff
changeset

284 
"proof tptp mode casc t " ^ string_of_int (to_secs 0 timeout) ^ 
41203
1393514094d7
fixed more issues with the Vampire output parser, and added support for Vampire's TSTP output (proof tptp)
blanchet
parents:
41148
diff
changeset

285 
" thanks \"Andrei and Krystof\" input_file" 
42853
de1fe9eaf3f4
tweaked ATP type systems further based on Judgment Day
blanchet
parents:
42844
diff
changeset

286 
> (slice < 2 orelse Config.get ctxt vampire_force_sos) 
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

287 
? prefix "sos on ", 
37509
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
37506
diff
changeset

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

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

290 
"======= End of refutation ======="), 
38033  291 
("% SZS output start Refutation", "% SZS output end Refutation"), 
292 
("% 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

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

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

295 
(IncompleteUnprovable, "CANNOT PROVE"), 
42449
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42443
diff
changeset

296 
(IncompleteUnprovable, "SZS status GaveUp"), 
42882
391e41ac038b
make sure the Vampire incomplete proof detection code kicks in
blanchet
parents:
42855
diff
changeset

297 
(ProofIncomplete, "predicate_definition_introduction,[]"), 
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

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

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

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

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

302 
(Interrupted, "Aborted by signal SIGINT")], 
42709
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42708
diff
changeset

303 
conj_sym_kind = Conjecture, (* FIXME: try out Hypothesis *) 
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42708
diff
changeset

304 
prem_kind = Conjecture, 
42937  305 
formats = [FOF], 
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

306 
best_slices = fn ctxt => 
42723  307 
(* FUDGE *) 
42853
de1fe9eaf3f4
tweaked ATP type systems further based on Judgment Day
blanchet
parents:
42844
diff
changeset

308 
[(0.333, (false, (400, ["mangled_preds_heavy"]))) (* SOS *), 
de1fe9eaf3f4
tweaked ATP type systems further based on Judgment Day
blanchet
parents:
42844
diff
changeset

309 
(0.333, (false, (400, ["mangled_tags?"]))) (* SOS *), 
de1fe9eaf3f4
tweaked ATP type systems further based on Judgment Day
blanchet
parents:
42844
diff
changeset

310 
(0.334, (true, (400, ["poly_preds"]))) (* ~SOS *)] 
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

311 
> (if Config.get ctxt vampire_force_sos then hd #> apfst (K 1.0) #> single 
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

312 
else I)} 
38454
9043eefe8d71
detect old Vampire and give a nicer error message
blanchet
parents:
38433
diff
changeset

313 

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

314 
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

315 

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

316 

41740
4b09f8b9e012
added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents:
41738
diff
changeset

317 
(* Z3 with TPTP syntax *) 
4b09f8b9e012
added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents:
41738
diff
changeset

318 

4b09f8b9e012
added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents:
41738
diff
changeset

319 
val z3_atp_config : atp_config = 
4b09f8b9e012
added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents:
41738
diff
changeset

320 
{exec = ("Z3_HOME", "z3"), 
4b09f8b9e012
added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents:
41738
diff
changeset

321 
required_execs = [], 
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

322 
arguments = fn _ => fn _ => fn timeout => fn _ => 
41766
26dab6eca1c2
make experimental "Z3 ATP" work on Linux as well
blanchet
parents:
41765
diff
changeset

323 
"MBQI=true p t:" ^ string_of_int (to_secs 0 timeout), 
41740
4b09f8b9e012
added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents:
41738
diff
changeset

324 
proof_delims = [], 
4b09f8b9e012
added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents:
41738
diff
changeset

325 
known_failures = 
41742
11e862c68b40
automatically minimize Z3asanATP proofs (cf. CVC3 and Yices)
blanchet
parents:
41741
diff
changeset

326 
[(Unprovable, "\nsat"), 
11e862c68b40
automatically minimize Z3asanATP proofs (cf. CVC3 and Yices)
blanchet
parents:
41741
diff
changeset

327 
(IncompleteUnprovable, "\nunknown"), 
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42332
diff
changeset

328 
(IncompleteUnprovable, "SZS status Satisfiable"), 
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42332
diff
changeset

329 
(ProofMissing, "\nunsat"), 
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42332
diff
changeset

330 
(ProofMissing, "SZS status Unsatisfiable")], 
42709
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42708
diff
changeset

331 
conj_sym_kind = Hypothesis, 
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42708
diff
changeset

332 
prem_kind = Hypothesis, 
42937  333 
formats = [FOF], 
42723  334 
best_slices = 
335 
(* FUDGE (FIXME) *) 

336 
K [(1.0, (false, (250, [])))]} 

41740
4b09f8b9e012
added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents:
41738
diff
changeset

337 

4b09f8b9e012
added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents:
41738
diff
changeset

338 
val z3_atp = (z3_atpN, z3_atp_config) 
4b09f8b9e012
added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents:
41738
diff
changeset

339 

4b09f8b9e012
added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents:
41738
diff
changeset

340 

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

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

342 

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

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

345 
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

346 
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

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

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

349 
error (case extract_known_failure known_perl_failures output of 
41744  350 
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

351 
 NONE => perhaps (try (unsuffix "\n")) output ^ ".") 
31835  352 

42537
25ceb855a18b
improve version handling  prefer versions of ToFoF, SInE, and SNARK that are known to work
blanchet
parents:
42535
diff
changeset

353 
fun find_system name [] systems = 
25ceb855a18b
improve version handling  prefer versions of ToFoF, SInE, and SNARK that are known to work
blanchet
parents:
42535
diff
changeset

354 
find_first (String.isPrefix (name ^ "")) systems 
38690
38a926e033ad
make remote ATP versions more robust, by starting with "preferred" version numbers and falling back on any version
blanchet
parents:
38685
diff
changeset

355 
 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

356 
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

357 
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

358 
 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

359 

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

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

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

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

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

364 

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

365 
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

366 
case get_system name versions of 
39010  367 
SOME sys => sys 
41269  368 
 NONE => error ("System " ^ quote name ^ 
369 
" is not available at SystemOnTPTP.") 

31835  370 

41148  371 
val max_remote_secs = 240 (* give Geoff Sutcliffe's servers a break *) 
372 

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

373 
fun remote_config system_name system_versions proof_delims known_failures 
42723  374 
conj_sym_kind prem_kind formats best_slice : atp_config = 
38092
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38090
diff
changeset

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

376 
required_execs = [], 
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

377 
arguments = fn _ => fn _ => fn timeout => fn _ => 
41148  378 
" t " ^ string_of_int (Int.min (max_remote_secs, (to_secs 0 timeout))) 
379 
^ " s " ^ the_system system_name system_versions, 

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

380 
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

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

382 
known_failures @ known_perl_failures @ 
42941  383 
[(Unprovable, "says Satisfiable"), 
384 
(IncompleteUnprovable, "says Unknown"), 

42584  385 
(IncompleteUnprovable, "says GaveUp"), 
42571  386 
(TimedOut, "says Timeout")], 
42709
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42708
diff
changeset

387 
conj_sym_kind = conj_sym_kind, 
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42708
diff
changeset

388 
prem_kind = prem_kind, 
42578
1eaf4d437d4c
define type system in ATP module so that ATPs can suggest a type system
blanchet
parents:
42577
diff
changeset

389 
formats = formats, 
42723  390 
best_slices = fn ctxt => [(1.0, (false, best_slice ctxt))]} 
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42332
diff
changeset

391 

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

392 
fun remotify_config system_name system_versions 
42709
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42708
diff
changeset

393 
({proof_delims, known_failures, conj_sym_kind, prem_kind, formats, 
42723  394 
best_slices, ...} : 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

395 
remote_config system_name system_versions proof_delims known_failures 
42709
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42708
diff
changeset

396 
conj_sym_kind prem_kind formats 
42723  397 
(best_slices #> List.last #> snd #> snd) 
38023  398 

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

399 
fun remote_atp name system_name system_versions proof_delims known_failures 
42723  400 
conj_sym_kind prem_kind formats best_slice = 
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

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

402 
remote_config system_name system_versions proof_delims known_failures 
42723  403 
conj_sym_kind prem_kind formats best_slice) 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

404 
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

405 
(remote_prefix ^ name, remotify_config system_name system_versions config) 
28592  406 

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

407 
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

408 
val remote_vampire = remotify_atp vampire "Vampire" ["0.6", "9.0", "1.0"] 
42537
25ceb855a18b
improve version handling  prefer versions of ToFoF, SInE, and SNARK that are known to work
blanchet
parents:
42535
diff
changeset

409 
val remote_z3_atp = remotify_atp z3_atp "Z3" ["2.18"] 
42535
3c1f302b3ee6
added support for ToFoF prover for experimenting with the TPTP TFF (typed firstorder) format
blanchet
parents:
42521
diff
changeset

410 
val remote_tofof_e = 
42559  411 
remote_atp tofof_eN "ToFoF" ["0.1"] [] (#known_failures e_config) 
42937  412 
Axiom Conjecture [TFF] (K (200, ["simple"]) (* FUDGE *)) 
41740
4b09f8b9e012
added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents:
41738
diff
changeset

413 
val remote_sine_e = 
42937  414 
remote_atp sine_eN "SInE" ["0.4"] [] [] Axiom Conjecture [FOF] 
42853
de1fe9eaf3f4
tweaked ATP type systems further based on Judgment Day
blanchet
parents:
42844
diff
changeset

415 
(K (500, ["poly_tags_heavy!", "poly_tags_heavy"]) (* FUDGE *)) 
41740
4b09f8b9e012
added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents:
41738
diff
changeset

416 
val remote_snark = 
42939  417 
remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"] 
42709
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42708
diff
changeset

418 
[("refutation.", "end_refutation.")] [] Hypothesis Conjecture 
42937  419 
[TFF, FOF] (K (250, ["simple"]) (* FUDGE *)) 
42938  420 
val remote_waldmeister = 
421 
remote_atp waldmeisterN "Waldmeister" ["710"] 

42944
9e620869a576
improved Waldmeister support  even run it by default on unit equational goals
blanchet
parents:
42943
diff
changeset

422 
[("#START OF PROOF", "Proved Goals:")] 
9e620869a576
improved Waldmeister support  even run it by default on unit equational goals
blanchet
parents:
42943
diff
changeset

423 
[(OutOfResources, "Too many function symbols")] Hypothesis 
9e620869a576
improved Waldmeister support  even run it by default on unit equational goals
blanchet
parents:
42943
diff
changeset

424 
Hypothesis [CNF_UEQ] (K (100, ["poly_args"]) (* FUDGE *)) 
38454
9043eefe8d71
detect old Vampire and give a nicer error message
blanchet
parents:
38433
diff
changeset

425 

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

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

427 

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

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

429 
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

430 
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

431 

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

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

433 
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

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

435 

41727
ab3f6d76fb23
available_provers ~> supported_provers (for clarity)
blanchet
parents:
41725
diff
changeset

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

437 

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

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

439 
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

440 
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

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

442 

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

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

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

445 

41740
4b09f8b9e012
added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents:
41738
diff
changeset

446 
val atps = [e, spass, vampire, z3_atp, remote_e, remote_vampire, remote_z3_atp, 
42938  447 
remote_tofof_e, remote_sine_e, remote_snark, remote_waldmeister] 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

448 
val setup = fold add_atp atps 
35867  449 

28592  450 
end; 