author  blanchet 
Wed, 08 Jun 2011 16:20:18 +0200  
changeset 43288  7a4eebdebb23 
parent 43221  2c88166938eb 
child 43354  396aaa15dd8b 
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 
42962
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42955
diff
changeset

39 
val leo2N : string 
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42955
diff
changeset

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

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

42 
val snarkN : string 
42962
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42955
diff
changeset

43 
val tofof_eN : string 
42938  44 
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

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

46 
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

47 
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

48 
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

49 
> (failure * string) list > formula_kind > formula_kind > format list 
42723  50 
> (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

51 
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

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

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

54 
val is_atp_installed : theory > string > bool 
35867  55 
val refresh_systems_on_tptp : unit > unit 
56 
val setup : theory > theory 

28592  57 
end; 
58 

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

61 

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

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

63 
open ATP_Proof 
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 
(* ATP configuration *) 
32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

66 

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

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

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

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

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

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

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

73 
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

74 
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

75 
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

76 
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

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

79 

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

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

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

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

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

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

87 

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

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

90 
remote provers and if slicing is disabled. *) 

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

91 

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

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

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

96 

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

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

98 

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

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

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

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

102 
val z3_atpN = "z3_atp" 
42962
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42955
diff
changeset

103 
val leo2N = "leo2" 
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42955
diff
changeset

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

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

106 
val snarkN = "snark" 
42962
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42955
diff
changeset

107 
val tofof_eN = "tofof_e" 
42938  108 
val waldmeisterN = "waldmeister" 
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

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

110 

38023  111 
structure Data = Theory_Data 
112 
( 

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

113 
type T = (atp_config * stamp) Symtab.table 
38023  114 
val empty = Symtab.empty 
115 
val extend = I 

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

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

118 
) 

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

119 

43056
7a43449ffd86
no more bonus for E  with the soft timeout, this punishes everybody  the bonus was designed for a hard timeout
blanchet
parents:
43050
diff
changeset

120 
fun to_secs time = (Time.toMilliseconds time + 999) div 1000 
36142
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36064
diff
changeset

121 

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

122 

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

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

124 

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

125 
val tstp_proof_delims = 
42962
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42955
diff
changeset

126 
[("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation"), 
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42955
diff
changeset

127 
("% SZS output start CNFRefutation", "% SZS output end CNFRefutation")] 
36369
d2cd0d04b8e6
handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents:
36289
diff
changeset

128 

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

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

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

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

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

133 

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

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

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

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

138 
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

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

140 
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

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

142 
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

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

144 
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

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

146 
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

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

148 
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

149 

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

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

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

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

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

154 

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

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

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

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

158 
+ 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_base e_sym_offs_weight_base) 
41725
7cca2de89296
added support for bleedingedge E weighting function "SymOffsetsWeight"
blanchet
parents:
41335
diff
changeset

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

161 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

178 
"),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

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

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

181 

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

182 
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

183 

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

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

185 
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

186 

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

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

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

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

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

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

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

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

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

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

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

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

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

199 

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

200 
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

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

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

203 
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

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

205 
e_weight_arguments ctxt (method_for_slice ctxt slice) weights ^ 
43056
7a43449ffd86
no more bonus for E  with the soft timeout, this punishes everybody  the bonus was designed for a hard timeout
blanchet
parents:
43050
diff
changeset

206 
" tAutoDev silent cpulimit=" ^ string_of_int (to_secs timeout), 
42962
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42955
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

218 
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

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

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

223 
if effective_e_weight_method ctxt = e_slicesN then 
43060
e998e85e41ff
avoid monomorphic encoding with so many facts  it makes the old monomorphizer explode on some examples
blanchet
parents:
43056
diff
changeset

224 
[(0.333, (true, (100, ["mangled_preds_heavy"]))) (* sym_offset_weight *), 
e998e85e41ff
avoid monomorphic encoding with so many facts  it makes the old monomorphizer explode on some examples
blanchet
parents:
43056
diff
changeset

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

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

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

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

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

230 

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

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

232 

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

233 

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

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

235 

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

236 
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

237 
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

238 

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

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

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

241 
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

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

244 
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

245 
("Auto PGiven=0 PProblem=0 Splits=0 FullRed=0 DocProof \ 
43056
7a43449ffd86
no more bonus for E  with the soft timeout, this punishes everybody  the bonus was designed for a hard timeout
blanchet
parents:
43050
diff
changeset

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

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

248 
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

249 
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

250 
known_perl_failures @ 
43050
59284a13abc4
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents:
42999
diff
changeset

251 
[(GaveUp, "SPASS beiseite: Completion found"), 
36370
a4f601daa175
centralized ATPspecific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset

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

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

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

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

258 
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

259 
prem_kind = Conjecture, 
42937  260 
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

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

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

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

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

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

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

268 

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

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

270 

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

271 

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

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

273 

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

274 
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

275 
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

276 

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

277 
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

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

279 
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

280 
arguments = fn ctxt => fn slice => fn timeout => fn _ => 
43056
7a43449ffd86
no more bonus for E  with the soft timeout, this punishes everybody  the bonus was designed for a hard timeout
blanchet
parents:
43050
diff
changeset

281 
"proof tptp mode casc t " ^ string_of_int (to_secs 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

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

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

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

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

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

287 
"======= End of refutation ======="), 
38033  288 
("% SZS output start Refutation", "% SZS output end Refutation"), 
289 
("% 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

290 
known_failures = 
43050
59284a13abc4
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents:
42999
diff
changeset

291 
[(GaveUp, "UNPROVABLE"), 
59284a13abc4
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents:
42999
diff
changeset

292 
(GaveUp, "CANNOT PROVE"), 
59284a13abc4
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents:
42999
diff
changeset

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

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

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

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

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

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

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

300 
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

301 
prem_kind = Conjecture, 
42937  302 
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

303 
best_slices = fn ctxt => 
42723  304 
(* FUDGE *) 
43221
2c88166938eb
slighly more reasonable Vampire slices (until new monomorphizer is used)
blanchet
parents:
43060
diff
changeset

305 
[(0.333, (false, (200, ["mangled_preds_heavy"]))) (* SOS *), 
2c88166938eb
slighly more reasonable Vampire slices (until new monomorphizer is used)
blanchet
parents:
43060
diff
changeset

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

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

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

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

310 

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

311 
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

312 

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

313 

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

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

315 

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

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

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

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

319 
arguments = fn _ => fn _ => fn timeout => fn _ => 
43056
7a43449ffd86
no more bonus for E  with the soft timeout, this punishes everybody  the bonus was designed for a hard timeout
blanchet
parents:
43050
diff
changeset

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

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

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

323 
[(Unprovable, "\nsat"), 
43050
59284a13abc4
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents:
42999
diff
changeset

324 
(GaveUp, "\nunknown"), 
59284a13abc4
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents:
42999
diff
changeset

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

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

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

328 
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

329 
prem_kind = Hypothesis, 
42937  330 
formats = [FOF], 
42723  331 
best_slices = 
332 
(* FUDGE (FIXME) *) 

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

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

334 

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

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

336 

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

337 

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

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

339 

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

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

342 
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

343 
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

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

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

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

348 
 NONE => perhaps (try (unsuffix "\n")) output ^ ".") 
31835  349 

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

350 
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

351 
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

352 
 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

353 
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

354 
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

355 
 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

356 

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 
fun get_system name versions = 
38589
b03f8fe043ec
added "max_relevant_per_iter" option to Sledgehammer
blanchet
parents:
38588
diff
changeset

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

359 
(fn systems => (if null systems then get_systems () else systems) 
42955  360 
> `(`(find_system name versions))) 
32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

361 

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

362 
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

363 
case get_system name versions of 
42955  364 
(SOME sys, _) => sys 
365 
 (NONE, []) => error ("SystemOnTPTP is currently not available.") 

366 
 (NONE, syss) => 

367 
error ("System " ^ quote name ^ " is not available at SystemOnTPTP.\n" ^ 

368 
"(Available systems: " ^ commas_quote syss ^ ".)") 

31835  369 

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

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

372 
fun remote_config system_name system_versions proof_delims known_failures 
42723  373 
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

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

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

376 
arguments = fn _ => fn _ => fn timeout => fn _ => 
43056
7a43449ffd86
no more bonus for E  with the soft timeout, this punishes everybody  the bonus was designed for a hard timeout
blanchet
parents:
43050
diff
changeset

377 
"t " ^ string_of_int (Int.min (max_remote_secs, to_secs timeout)) 
41148  378 
^ " s " ^ the_system system_name system_versions, 
42962
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42955
diff
changeset

379 
proof_delims = union (op =) tstp_proof_delims proof_delims, 
42965
1403595ec38c
slightly gracefuller handling of LEOII and Satallax output
blanchet
parents:
42963
diff
changeset

380 
known_failures = known_failures @ known_perl_failures @ 
42941  381 
[(Unprovable, "says Satisfiable"), 
42999  382 
(Unprovable, "says CounterSatisfiable"), 
43050
59284a13abc4
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents:
42999
diff
changeset

383 
(GaveUp, "says Unknown"), 
59284a13abc4
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents:
42999
diff
changeset

384 
(GaveUp, "says GaveUp"), 
42965
1403595ec38c
slightly gracefuller handling of LEOII and Satallax output
blanchet
parents:
42963
diff
changeset

385 
(ProofMissing, "says Theorem"), 
42999  386 
(ProofMissing, "says Unsatisfiable"), 
42953
26111aafab12
detect inappropriate problems and crashes better in Waldmeister
blanchet
parents:
42944
diff
changeset

387 
(TimedOut, "says Timeout"), 
26111aafab12
detect inappropriate problems and crashes better in Waldmeister
blanchet
parents:
42944
diff
changeset

388 
(Inappropriate, "says Inappropriate")], 
42709
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42708
diff
changeset

389 
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

390 
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

391 
formats = formats, 
42723  392 
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

393 

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

394 
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

395 
({proof_delims, known_failures, conj_sym_kind, prem_kind, formats, 
42723  396 
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

397 
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

398 
conj_sym_kind prem_kind formats 
42723  399 
(best_slices #> List.last #> snd #> snd) 
38023  400 

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

401 
fun remote_atp name system_name system_versions proof_delims known_failures 
42723  402 
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

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

404 
remote_config system_name system_versions proof_delims known_failures 
42723  405 
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

406 
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

407 
(remote_prefix ^ name, remotify_config system_name system_versions config) 
28592  408 

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

409 
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

410 
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

411 
val remote_z3_atp = remotify_atp z3_atp "Z3" ["2.18"] 
42962
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42955
diff
changeset

412 
val remote_leo2 = 
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42955
diff
changeset

413 
remote_atp leo2N "LEOII" ["1.2.6"] [] [] Axiom Hypothesis [THF] 
42971
b01cbbf0bcc5
further reduce the number of facts passed to less used remote ATPs
blanchet
parents:
42969
diff
changeset

414 
(K (100, ["simple"]) (* FUDGE *)) 
42962
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42955
diff
changeset

415 
val remote_satallax = 
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42955
diff
changeset

416 
remote_atp satallaxN "Satallax" ["2.0"] [] [] Axiom Hypothesis [THF] 
42971
b01cbbf0bcc5
further reduce the number of facts passed to less used remote ATPs
blanchet
parents:
42969
diff
changeset

417 
(K (64, ["simple"]) (* FUDGE *)) 
41740
4b09f8b9e012
added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents:
41738
diff
changeset

418 
val remote_sine_e = 
42962
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42955
diff
changeset

419 
remote_atp sine_eN "SInE" ["0.4"] [] (#known_failures e_config) 
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42955
diff
changeset

420 
Axiom Conjecture [FOF] 
42853
de1fe9eaf3f4
tweaked ATP type systems further based on Judgment Day
blanchet
parents:
42844
diff
changeset

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

422 
val remote_snark = 
42939  423 
remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"] 
42962
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42955
diff
changeset

424 
[("refutation.", "end_refutation.")] [] Hypothesis Hypothesis 
42971
b01cbbf0bcc5
further reduce the number of facts passed to less used remote ATPs
blanchet
parents:
42969
diff
changeset

425 
[TFF, FOF] (K (100, ["simple"]) (* FUDGE *)) 
42962
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42955
diff
changeset

426 
val remote_tofof_e = 
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42955
diff
changeset

427 
remote_atp tofof_eN "ToFoF" ["0.1"] [] (#known_failures e_config) 
42969
10baeee358a5
pass fewer relevant facts to less used remote systems
blanchet
parents:
42965
diff
changeset

428 
Axiom Hypothesis [TFF] (K (150, ["simple"]) (* FUDGE *)) 
42938  429 
val remote_waldmeister = 
430 
remote_atp waldmeisterN "Waldmeister" ["710"] 

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

431 
[("#START OF PROOF", "Proved Goals:")] 
42953
26111aafab12
detect inappropriate problems and crashes better in Waldmeister
blanchet
parents:
42944
diff
changeset

432 
[(OutOfResources, "Too many function symbols"), 
26111aafab12
detect inappropriate problems and crashes better in Waldmeister
blanchet
parents:
42944
diff
changeset

433 
(Crashed, "Unrecoverable Segmentation Fault")] 
26111aafab12
detect inappropriate problems and crashes better in Waldmeister
blanchet
parents:
42944
diff
changeset

434 
Hypothesis Hypothesis [CNF_UEQ] 
43288
7a4eebdebb23
better default type system for Waldmeister, with fewer predicates (for types or type classes)
blanchet
parents:
43221
diff
changeset

435 
(K (50, ["mangled_args", "mangled_tags?"]) (* FUDGE *)) 
38454
9043eefe8d71
detect old Vampire and give a nicer error message
blanchet
parents:
38433
diff
changeset

436 

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

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

438 

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

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

440 
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

441 
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

442 

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

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

444 
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

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

446 

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

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

448 

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

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

450 
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

451 
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

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

453 

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

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

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

456 

42962
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42955
diff
changeset

457 
val atps = 
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42955
diff
changeset

458 
[e, spass, vampire, z3_atp, remote_e, remote_vampire, remote_z3_atp, 
42963  459 
remote_leo2, remote_satallax, remote_sine_e, remote_snark, remote_tofof_e, 
460 
remote_waldmeister] 

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

461 
val setup = fold add_atp atps 
35867  462 

28592  463 
end; 