author  wenzelm 
Sat, 16 Jul 2011 20:52:41 +0200  
changeset 43850  7f2cbc713344 
parent 43690  92f78a4a5628 
child 43981  404ae49ce29f 
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 : 
43473
fb2713b803e6
deal with ATP time slices in a more flexible/robust fashion
blanchet
parents:
43467
diff
changeset

18 
Proof.context > bool > string > Time.time 
43354
396aaa15dd8b
pass trim option to "eproof" script to speed up proof reconstruction
blanchet
parents:
43288
diff
changeset

19 
> (unit > (string * real) list) > 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, 
43473
fb2713b803e6
deal with ATP time slices in a more flexible/robust fashion
blanchet
parents:
43467
diff
changeset

25 
best_slices : 
43569
b342cd125533
removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
blanchet
parents:
43567
diff
changeset

26 
Proof.context > (real * (bool * (int * string * string))) list} 
38023  27 

43566
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43529
diff
changeset

28 
val e_smartN : string 
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43529
diff
changeset

29 
val e_autoN : string 
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43529
diff
changeset

30 
val e_fun_weightN : string 
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43529
diff
changeset

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

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

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

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

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

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

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

38 
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

39 
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

40 
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

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

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

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

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

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

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

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

48 
val tofof_eN : string 
42938  49 
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

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

51 
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

52 
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

53 
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

54 
> (failure * string) list > formula_kind > formula_kind > format list 
43569
b342cd125533
removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
blanchet
parents:
43567
diff
changeset

55 
> (Proof.context > int * string) > string * atp_config 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39491
diff
changeset

56 
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

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

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

59 
val is_atp_installed : theory > string > bool 
35867  60 
val refresh_systems_on_tptp : unit > unit 
61 
val setup : theory > theory 

28592  62 
end; 
63 

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

66 

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

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

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

69 

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

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

71 

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

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

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

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

75 
arguments : 
43473
fb2713b803e6
deal with ATP time slices in a more flexible/robust fashion
blanchet
parents:
43467
diff
changeset

76 
Proof.context > bool > string > Time.time 
fb2713b803e6
deal with ATP time slices in a more flexible/robust fashion
blanchet
parents:
43467
diff
changeset

77 
> (unit > (string * real) list) > string, 
42578
1eaf4d437d4c
define type system in ATP module so that ATPs can suggest a type system
blanchet
parents:
42577
diff
changeset

78 
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

79 
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

80 
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

81 
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

82 
formats : format list, 
43473
fb2713b803e6
deal with ATP time slices in a more flexible/robust fashion
blanchet
parents:
43467
diff
changeset

83 
best_slices : 
43569
b342cd125533
removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
blanchet
parents:
43567
diff
changeset

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

85 

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

43569
b342cd125533
removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
blanchet
parents:
43567
diff
changeset

88 
time available given to the slice and should add up to 1.0. The "bool" 
42723  89 
component indicates whether the slice's strategy is complete; the "int", the 
43569
b342cd125533
removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
blanchet
parents:
43567
diff
changeset

90 
preferred number of facts to pass; the first "string", the preferred type 
43575  91 
system (which should be sound or quasisound); the second "string", extra 
92 
information to the prover (e.g., SOS or no SOS). 

42723  93 

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

43569
b342cd125533
removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
blanchet
parents:
43567
diff
changeset

95 
time available if the other slices fail early and also because it is used if 
b342cd125533
removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
blanchet
parents:
43567
diff
changeset

96 
slicing is disabled (e.g., by the minimizer). *) 
42710
84fcce345b5d
further improved type system setup based on Judgment Days
blanchet
parents:
42709
diff
changeset

97 

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

98 
val known_perl_failures = 
38094  99 
[(CantConnect, "HTTP error"), 
100 
(NoPerl, "env: perl"), 

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

102 

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

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

104 

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

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

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

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

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

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

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

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

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

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

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

116 

38023  117 
structure Data = Theory_Data 
118 
( 

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

119 
type T = (atp_config * stamp) Symtab.table 
38023  120 
val empty = Symtab.empty 
121 
val extend = I 

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

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

124 
) 

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

125 

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

126 
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

127 

43473
fb2713b803e6
deal with ATP time slices in a more flexible/robust fashion
blanchet
parents:
43467
diff
changeset

128 
val sosN = "sos" 
fb2713b803e6
deal with ATP time slices in a more flexible/robust fashion
blanchet
parents:
43467
diff
changeset

129 
val no_sosN = "no_sos" 
fb2713b803e6
deal with ATP time slices in a more flexible/robust fashion
blanchet
parents:
43467
diff
changeset

130 

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

131 

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

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

133 

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

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

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

136 
("% 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

137 

43473
fb2713b803e6
deal with ATP time slices in a more flexible/robust fashion
blanchet
parents:
43467
diff
changeset

138 
val e_smartN = "smart" 
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42643
diff
changeset

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

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

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

142 

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

143 
val e_weight_method = 
43473
fb2713b803e6
deal with ATP time slices in a more flexible/robust fashion
blanchet
parents:
43467
diff
changeset

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

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

147 
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

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

149 
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

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

151 
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

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

153 
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

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

155 
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

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

157 
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

158 

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

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

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

161 
else if method = e_sym_offset_weightN then sow 
43478  162 
else raise Fail ("unexpected " ^ quote method) 
41725
7cca2de89296
added support for bleedingedge E weighting function "SymOffsetsWeight"
blanchet
parents:
41335
diff
changeset

163 

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

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

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

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

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

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

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

170 

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

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

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

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

174 
else 
43622  175 
(* supplied by Stephan Schulz *) 
41314
2dc1dfc1bc69
use the options provided by Stephan Schulz  much better
blanchet
parents:
41313
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

191 

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

192 
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

193 

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

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

195 
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

196 

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

197 
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

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

199 
required_execs = [], 
43354
396aaa15dd8b
pass trim option to "eproof" script to speed up proof reconstruction
blanchet
parents:
43288
diff
changeset

200 
arguments = 
43567
dda3e38cc351
remove experimental trimming feature  it slowed down things on Linux for some reason
blanchet
parents:
43566
diff
changeset

201 
fn ctxt => fn _ => fn method => fn timeout => fn weights => 
43473
fb2713b803e6
deal with ATP time slices in a more flexible/robust fashion
blanchet
parents:
43467
diff
changeset

202 
"tstpin tstpout l5 " ^ e_weight_arguments ctxt method weights ^ 
43567
dda3e38cc351
remove experimental trimming feature  it slowed down things on Linux for some reason
blanchet
parents:
43566
diff
changeset

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

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

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

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

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

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

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

210 
(TimedOut, "time limit exceeded"), 
43467  211 
(OutOfResources, "# Cannot determine problem status"), 
36370
a4f601daa175
centralized ATPspecific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset

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

213 
(OutOfResources, "SZS status ResourceOut")], 
43466
52f040bcfae7
tweaked TPTP formula kind for typing information used in the conjecture
blanchet
parents:
43354
diff
changeset

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

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

217 
best_slices = fn ctxt => 
43473
fb2713b803e6
deal with ATP time slices in a more flexible/robust fashion
blanchet
parents:
43467
diff
changeset

218 
let val method = effective_e_weight_method ctxt in 
43474
423cd1ecf714
optimized E's time slicing, based on latest exhaustive Judgment Day results
blanchet
parents:
43473
diff
changeset

219 
(* FUDGE *) 
43473
fb2713b803e6
deal with ATP time slices in a more flexible/robust fashion
blanchet
parents:
43467
diff
changeset

220 
if method = e_smartN then 
43569
b342cd125533
removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
blanchet
parents:
43567
diff
changeset

221 
[(0.333, (true, (500, "mangled_tags?", e_fun_weightN))), 
b342cd125533
removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
blanchet
parents:
43567
diff
changeset

222 
(0.334, (true, (50, "mangled_preds?", e_fun_weightN))), 
b342cd125533
removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
blanchet
parents:
43567
diff
changeset

223 
(0.333, (true, (1000, "mangled_tags?", e_sym_offset_weightN)))] 
43473
fb2713b803e6
deal with ATP time slices in a more flexible/robust fashion
blanchet
parents:
43467
diff
changeset

224 
else 
43569
b342cd125533
removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
blanchet
parents:
43567
diff
changeset

225 
[(1.0, (true, (500, "mangled_tags?", method)))] 
43473
fb2713b803e6
deal with ATP time slices in a more flexible/robust fashion
blanchet
parents:
43467
diff
changeset

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

227 

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

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

229 

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

230 

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

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

232 

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

233 
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

234 
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

235 

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

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

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

238 
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

239 
{exec = ("ISABELLE_ATP", "scripts/spass"), 
39002  240 
required_execs = [("SPASS_HOME", "SPASS"), ("SPASS_HOME", "tptp2dfg")], 
43569
b342cd125533
removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
blanchet
parents:
43567
diff
changeset

241 
arguments = fn _ => fn _ => fn sos => 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

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

243 
\VarWeight=3 TimeLimit=" ^ string_of_int (to_secs timeout)) 
43473
fb2713b803e6
deal with ATP time slices in a more flexible/robust fashion
blanchet
parents:
43467
diff
changeset

244 
> sos = sosN ? prefix "SOS=1 ", 
36369
d2cd0d04b8e6
handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents:
36289
diff
changeset

245 
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

246 
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

247 
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

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

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

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

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

254 
(InternalError, "Please report this error")], 
43466
52f040bcfae7
tweaked TPTP formula kind for typing information used in the conjecture
blanchet
parents:
43354
diff
changeset

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

256 
prem_kind = Conjecture, 
42937  257 
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

258 
best_slices = fn ctxt => 
42723  259 
(* FUDGE *) 
43569
b342cd125533
removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
blanchet
parents:
43567
diff
changeset

260 
[(0.333, (false, (150, "mangled_tags", sosN))), 
b342cd125533
removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
blanchet
parents:
43567
diff
changeset

261 
(0.333, (false, (300, "poly_tags?", sosN))), 
b342cd125533
removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
blanchet
parents:
43567
diff
changeset

262 
(0.334, (true, (50, "mangled_tags?", no_sosN)))] 
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

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

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

265 

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

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

267 

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

268 

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

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

270 

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

271 
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

272 
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

273 

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

274 
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

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

276 
required_execs = [], 
43569
b342cd125533
removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
blanchet
parents:
43567
diff
changeset

277 
arguments = fn _ => fn _ => fn sos => 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

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

279 
" thanks \"Andrei and Krystof\" input_file" 
43473
fb2713b803e6
deal with ATP time slices in a more flexible/robust fashion
blanchet
parents:
43467
diff
changeset

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

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

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

283 
"======= End of refutation ======="), 
38033  284 
("% SZS output start Refutation", "% SZS output end Refutation"), 
285 
("% 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

286 
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

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

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

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

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

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

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

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

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

295 
(Interrupted, "Aborted by signal SIGINT")], 
43466
52f040bcfae7
tweaked TPTP formula kind for typing information used in the conjecture
blanchet
parents:
43354
diff
changeset

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

297 
prem_kind = Conjecture, 
42937  298 
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

299 
best_slices = fn ctxt => 
42723  300 
(* FUDGE *) 
43569
b342cd125533
removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
blanchet
parents:
43567
diff
changeset

301 
[(0.333, (false, (150, "poly_preds", sosN))), 
b342cd125533
removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
blanchet
parents:
43567
diff
changeset

302 
(0.334, (true, (50, "mangled_preds?", no_sosN))), 
b342cd125533
removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
blanchet
parents:
43567
diff
changeset

303 
(0.333, (false, (500, "mangled_tags?", sosN)))] 
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

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

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

306 

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

307 
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

308 

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

309 

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

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

311 

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

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

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

314 
required_execs = [], 
43354
396aaa15dd8b
pass trim option to "eproof" script to speed up proof reconstruction
blanchet
parents:
43288
diff
changeset

315 
arguments = fn _ => 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

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

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

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

319 
[(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

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

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

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

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

324 
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

325 
prem_kind = Hypothesis, 
42937  326 
formats = [FOF], 
42723  327 
best_slices = 
328 
(* FUDGE (FIXME) *) 

43690  329 
K [(0.5, (false, (250, "mangled_preds?", ""))), 
330 
(0.25, (false, (125, "mangled_preds?", ""))), 

331 
(0.125, (false, (62, "mangled_preds?", ""))), 

332 
(0.125, (false, (31, "mangled_preds?", "")))]} 

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

333 

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

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

335 

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

336 

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

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

338 

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

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

341 
fun get_systems () = 

43850
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
43690
diff
changeset

342 
case Isabelle_System.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

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

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

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

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

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

349 
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

350 
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

351 
 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

352 
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

353 
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

354 
 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

355 

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

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

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

360 

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

361 
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

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

365 
 (NONE, syss) => 

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

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

31835  368 

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

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

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

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

374 
required_execs = [], 
43354
396aaa15dd8b
pass trim option to "eproof" script to speed up proof reconstruction
blanchet
parents:
43288
diff
changeset

375 
arguments = fn _ => 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

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

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

379 
known_failures = known_failures @ known_perl_failures @ 
42941  380 
[(Unprovable, "says Satisfiable"), 
42999  381 
(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

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

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

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

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

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

388 
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

389 
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

390 
formats = formats, 
43473
fb2713b803e6
deal with ATP time slices in a more flexible/robust fashion
blanchet
parents:
43467
diff
changeset

391 
best_slices = fn ctxt => 
43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43624
diff
changeset

392 
let val (max_relevant, type_enc) = best_slice ctxt in 
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43624
diff
changeset

393 
[(1.0, (false, (max_relevant, type_enc, "")))] 
43473
fb2713b803e6
deal with ATP time slices in a more flexible/robust fashion
blanchet
parents:
43467
diff
changeset

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

395 

43500
4c357b7aa710
provide appropriate type system and number of fact defaults for remote ATPs
blanchet
parents:
43497
diff
changeset

396 
fun remotify_config system_name system_versions best_slice 
4c357b7aa710
provide appropriate type system and number of fact defaults for remote ATPs
blanchet
parents:
43497
diff
changeset

397 
({proof_delims, known_failures, conj_sym_kind, prem_kind, formats, ...} 
4c357b7aa710
provide appropriate type system and number of fact defaults for remote ATPs
blanchet
parents:
43497
diff
changeset

398 
: 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

399 
remote_config system_name system_versions proof_delims known_failures 
43500
4c357b7aa710
provide appropriate type system and number of fact defaults for remote ATPs
blanchet
parents:
43497
diff
changeset

400 
conj_sym_kind prem_kind formats best_slice 
38023  401 

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

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

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

405 
remote_config system_name system_versions proof_delims known_failures 
42723  406 
conj_sym_kind prem_kind formats best_slice) 
43500
4c357b7aa710
provide appropriate type system and number of fact defaults for remote ATPs
blanchet
parents:
43497
diff
changeset

407 
fun remotify_atp (name, config) system_name system_versions best_slice = 
4c357b7aa710
provide appropriate type system and number of fact defaults for remote ATPs
blanchet
parents:
43497
diff
changeset

408 
(remote_prefix ^ name, 
4c357b7aa710
provide appropriate type system and number of fact defaults for remote ATPs
blanchet
parents:
43497
diff
changeset

409 
remotify_config system_name system_versions best_slice config) 
28592  410 

43500
4c357b7aa710
provide appropriate type system and number of fact defaults for remote ATPs
blanchet
parents:
43497
diff
changeset

411 
val remote_e = 
4c357b7aa710
provide appropriate type system and number of fact defaults for remote ATPs
blanchet
parents:
43497
diff
changeset

412 
remotify_atp e "EP" ["1.0", "1.1", "1.2"] 
43569
b342cd125533
removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
blanchet
parents:
43567
diff
changeset

413 
(K (750, "mangled_tags?") (* FUDGE *)) 
43500
4c357b7aa710
provide appropriate type system and number of fact defaults for remote ATPs
blanchet
parents:
43497
diff
changeset

414 
val remote_vampire = 
4c357b7aa710
provide appropriate type system and number of fact defaults for remote ATPs
blanchet
parents:
43497
diff
changeset

415 
remotify_atp vampire "Vampire" ["0.6", "9.0", "1.0"] 
43569
b342cd125533
removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
blanchet
parents:
43567
diff
changeset

416 
(K (200, "mangled_preds?") (* FUDGE *)) 
43500
4c357b7aa710
provide appropriate type system and number of fact defaults for remote ATPs
blanchet
parents:
43497
diff
changeset

417 
val remote_z3_atp = 
43569
b342cd125533
removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
blanchet
parents:
43567
diff
changeset

418 
remotify_atp z3_atp "Z3" ["2.18"] (K (250, "mangled_preds?") (* FUDGE *)) 
42962
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42955
diff
changeset

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

420 
remote_atp leo2N "LEOII" ["1.2.6"] [] [] Axiom Hypothesis [THF] 
43624
de026aecab9b
cleaner handling of higherorder simple types, so that it's also possible to use firstorder simple types with LEOII and company
blanchet
parents:
43622
diff
changeset

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

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

423 
remote_atp satallaxN "Satallax" ["2.0"] [] [] Axiom Hypothesis [THF] 
43624
de026aecab9b
cleaner handling of higherorder simple types, so that it's also possible to use firstorder simple types with LEOII and company
blanchet
parents:
43622
diff
changeset

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

425 
val remote_sine_e = 
43569
b342cd125533
removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
blanchet
parents:
43567
diff
changeset

426 
remote_atp sine_eN "SInE" ["0.4"] [] (#known_failures e_config) Axiom 
b342cd125533
removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
blanchet
parents:
43567
diff
changeset

427 
Conjecture [FOF] (K (500, "mangled_preds?") (* FUDGE *)) 
41740
4b09f8b9e012
added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents:
41738
diff
changeset

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

430 
[("refutation.", "end_refutation.")] [] Hypothesis Hypothesis 
43569
b342cd125533
removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
blanchet
parents:
43567
diff
changeset

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

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

433 
remote_atp tofof_eN "ToFoF" ["0.1"] [] (#known_failures e_config) 
43569
b342cd125533
removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
blanchet
parents:
43567
diff
changeset

434 
Axiom Hypothesis [TFF] (K (150, "simple") (* FUDGE *)) 
42938  435 
val remote_waldmeister = 
436 
remote_atp waldmeisterN "Waldmeister" ["710"] 

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

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

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

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

440 
Hypothesis Hypothesis [CNF_UEQ] 
43569
b342cd125533
removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
blanchet
parents:
43567
diff
changeset

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

442 

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

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

444 

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

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

446 
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

447 
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

448 

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

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

450 
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

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

452 

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

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

454 

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

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

456 
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

457 
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

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

459 

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

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

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

462 

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

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

464 
[e, spass, vampire, z3_atp, remote_e, remote_vampire, remote_z3_atp, 
42963  465 
remote_leo2, remote_satallax, remote_sine_e, remote_snark, remote_tofof_e, 
466 
remote_waldmeister] 

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

467 
val setup = fold add_atp atps 
35867  468 

28592  469 
end; 