author  blanchet 
Mon, 15 Nov 2010 18:58:30 +0100  
changeset 40556  d66403b60b3b 
parent 40555  de581d7da0b6 
child 40558  e75614d0a859 
permissions  rwrr 
38021
e024504943d1
rename "ATP_Manager" ML module to "Sledgehammer";
blanchet
parents:
38020
diff
changeset

1 
(* Title: HOL/Tools/Sledgehammer/sledgehammer.ML 
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset

2 
Author: Fabian Immler, TU Muenchen 
32996
d2e48879e65a
removed disjunctive group cancellation  provers run independently;
wenzelm
parents:
32995
diff
changeset

3 
Author: Makarius 
35969  4 
Author: Jasmin Blanchette, TU Muenchen 
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset

5 

38021
e024504943d1
rename "ATP_Manager" ML module to "Sledgehammer";
blanchet
parents:
38020
diff
changeset

6 
Sledgehammer's heart. 
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset

7 
*) 
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset

8 

38021
e024504943d1
rename "ATP_Manager" ML module to "Sledgehammer";
blanchet
parents:
38020
diff
changeset

9 
signature SLEDGEHAMMER = 
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset

10 
sig 
40181  11 
type failure = ATP_Proof.failure 
38988  12 
type locality = Sledgehammer_Filter.locality 
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset

13 
type relevance_fudge = Sledgehammer_Filter.relevance_fudge 
38988  14 
type relevance_override = Sledgehammer_Filter.relevance_override 
40114  15 
type translated_formula = Sledgehammer_ATP_Translate.translated_formula 
40068  16 
type minimize_command = Sledgehammer_ATP_Reconstruct.minimize_command 
39493
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39492
diff
changeset

17 

35969  18 
type params = 
38982
820b8221ed48
added "blocking" option to Sledgehammer to run in synchronous mode;
blanchet
parents:
38893
diff
changeset

19 
{blocking: bool, 
820b8221ed48
added "blocking" option to Sledgehammer to run in synchronous mode;
blanchet
parents:
38893
diff
changeset

20 
debug: bool, 
35969  21 
verbose: bool, 
36143
6490319b1703
added "overlord" option (to get easy access to output files for debugging) + systematically use "raw_goal" rather than an inconsistent mixture
blanchet
parents:
36064
diff
changeset

22 
overlord: bool, 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

23 
provers: string list, 
35969  24 
full_types: bool, 
36235
61159615a0c5
added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)
blanchet
parents:
36231
diff
changeset

25 
explicit_apply: bool, 
38745
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset

26 
relevance_thresholds: real * real, 
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38741
diff
changeset

27 
max_relevant: int option, 
35969  28 
isar_proof: bool, 
36924  29 
isar_shrink_factor: int, 
38985
162bbbea4e4d
added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents:
38982
diff
changeset

30 
timeout: Time.time, 
162bbbea4e4d
added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents:
38982
diff
changeset

31 
expect: string} 
39493
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39492
diff
changeset

32 

40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40202
diff
changeset

33 
datatype fact = 
40114  34 
Untranslated of (string * locality) * thm  
35 
Translated of term * ((string * locality) * translated_formula) option 

40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

36 

71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

37 
type prover_problem = 
39318  38 
{state: Proof.state, 
38998  39 
goal: thm, 
40 
subgoal: int, 

40065  41 
subgoal_count: int, 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40202
diff
changeset

42 
facts: fact list, 
39366
f58fbb959826
handle relevance filter corner cases more gracefully;
blanchet
parents:
39364
diff
changeset

43 
only: bool} 
39493
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39492
diff
changeset

44 

40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

45 
type prover_result = 
36370
a4f601daa175
centralized ATPspecific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset

46 
{outcome: failure option, 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40202
diff
changeset

47 
used_facts: (string * locality) list, 
40062  48 
run_time_in_msecs: int option, 
49 
message: string} 

39493
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39492
diff
changeset

50 

40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

51 
type prover = params > minimize_command > prover_problem > prover_result 
35867  52 

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

53 
val smtN : string 
40072
27f2a45b0aab
more robust handling of "remote_" vs. non"remote_" provers
blanchet
parents:
40071
diff
changeset

54 
val is_prover_available : theory > string > bool 
27f2a45b0aab
more robust handling of "remote_" vs. non"remote_" provers
blanchet
parents:
40071
diff
changeset

55 
val is_prover_installed : Proof.context > string > bool 
40063
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset

56 
val default_max_relevant_for_prover : theory > string > int 
40369
53dca3bd4250
use the SMT integration's official list of builtins
blanchet
parents:
40341
diff
changeset

57 
val is_built_in_const_for_prover : 
53dca3bd4250
use the SMT integration's official list of builtins
blanchet
parents:
40341
diff
changeset

58 
Proof.context > string > string * typ > bool 
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset

59 
val relevance_fudge_for_prover : string > relevance_fudge 
38023  60 
val dest_dir : string Config.T 
61 
val problem_prefix : string Config.T 

39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset

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

63 
val available_provers : theory > unit 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

64 
val kill_provers : unit > unit 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

65 
val running_provers : unit > unit 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

66 
val messages : int option > unit 
40200  67 
val get_prover : theory > bool > string > prover 
38044  68 
val run_sledgehammer : 
39318  69 
params > bool > int > relevance_override > (string > minimize_command) 
70 
> Proof.state > bool * Proof.state 

38023  71 
val setup : theory > theory 
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset

72 
end; 
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset

73 

38021
e024504943d1
rename "ATP_Manager" ML module to "Sledgehammer";
blanchet
parents:
38020
diff
changeset

74 
structure Sledgehammer : SLEDGEHAMMER = 
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset

75 
struct 
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset

76 

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

78 
open ATP_Proof 
38028  79 
open ATP_Systems 
39494
bf7dd4902321
rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"
blanchet
parents:
39493
diff
changeset

80 
open Metis_Translate 
38023  81 
open Sledgehammer_Util 
38988  82 
open Sledgehammer_Filter 
40068  83 
open Sledgehammer_ATP_Translate 
84 
open Sledgehammer_ATP_Reconstruct 

37583
9ce2451647d5
factored nonATP specific code from "ATP_Manager" out, so that it can be reused for the LEOII integration
blanchet
parents:
37581
diff
changeset

85 

38023  86 

37583
9ce2451647d5
factored nonATP specific code from "ATP_Manager" out, so that it can be reused for the LEOII integration
blanchet
parents:
37581
diff
changeset

87 
(** The Sledgehammer **) 
9ce2451647d5
factored nonATP specific code from "ATP_Manager" out, so that it can be reused for the LEOII integration
blanchet
parents:
37581
diff
changeset

88 

38102
019a49759829
fix bug in the newly introduced "bound concealing" code
blanchet
parents:
38100
diff
changeset

89 
(* Identifier to distinguish Sledgehammer from other tools using 
019a49759829
fix bug in the newly introduced "bound concealing" code
blanchet
parents:
38100
diff
changeset

90 
"Async_Manager". *) 
37585  91 
val das_Tool = "Sledgehammer" 
92 

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

93 
val smtN = "smt" 
40062  94 
val smt_prover_names = [smtN, remote_prefix ^ smtN] 
95 

40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset

96 
val is_smt_prover = member (op =) smt_prover_names 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset

97 

40072
27f2a45b0aab
more robust handling of "remote_" vs. non"remote_" provers
blanchet
parents:
40071
diff
changeset

98 
fun is_prover_available thy name = 
27f2a45b0aab
more robust handling of "remote_" vs. non"remote_" provers
blanchet
parents:
40071
diff
changeset

99 
is_smt_prover name orelse member (op =) (available_atps thy) name 
27f2a45b0aab
more robust handling of "remote_" vs. non"remote_" provers
blanchet
parents:
40071
diff
changeset

100 

27f2a45b0aab
more robust handling of "remote_" vs. non"remote_" provers
blanchet
parents:
40071
diff
changeset

101 
fun is_prover_installed ctxt name = 
27f2a45b0aab
more robust handling of "remote_" vs. non"remote_" provers
blanchet
parents:
40071
diff
changeset

102 
let val thy = ProofContext.theory_of ctxt in 
40181  103 
if is_smt_prover name then SMT_Solver.is_locally_installed ctxt 
40072
27f2a45b0aab
more robust handling of "remote_" vs. non"remote_" provers
blanchet
parents:
40071
diff
changeset

104 
else is_atp_installed thy name 
27f2a45b0aab
more robust handling of "remote_" vs. non"remote_" provers
blanchet
parents:
40071
diff
changeset

105 
end 
27f2a45b0aab
more robust handling of "remote_" vs. non"remote_" provers
blanchet
parents:
40071
diff
changeset

106 

40419
718b44dbd74d
make sure the SMT solver runs several iterations by lowering the timeout at each iteration  yields better results in practice
blanchet
parents:
40417
diff
changeset

107 
val smt_default_max_relevant = 200 (* FUDGE *) 
40062  108 
val auto_max_relevant_divisor = 2 (* FUDGE *) 
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

109 

40063
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset

110 
fun default_max_relevant_for_prover thy name = 
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset

111 
if is_smt_prover name then smt_default_max_relevant 
40063
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset

112 
else #default_max_relevant (get_atp thy name) 
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset

113 

40071
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset

114 
(* These are typically simplified away by "Meson.presimplify". Equality is 
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset

115 
handled specially via "fequal". *) 
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset

116 
val atp_irrelevant_consts = 
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset

117 
[@{const_name False}, @{const_name True}, @{const_name If}, @{const_name Let}, 
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset

118 
@{const_name HOL.eq}] 
40206  119 

40369
53dca3bd4250
use the SMT integration's official list of builtins
blanchet
parents:
40341
diff
changeset

120 
fun is_built_in_const_for_prover ctxt name (s, T) = 
53dca3bd4250
use the SMT integration's official list of builtins
blanchet
parents:
40341
diff
changeset

121 
if is_smt_prover name then SMT_Builtin.is_builtin ctxt (s, T) 
53dca3bd4250
use the SMT integration's official list of builtins
blanchet
parents:
40341
diff
changeset

122 
else member (op =) atp_irrelevant_consts s 
40071
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset

123 

40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset

124 
(* FUDGE *) 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset

125 
val atp_relevance_fudge = 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset

126 
{worse_irrel_freq = 100.0, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset

127 
higher_order_irrel_weight = 1.05, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset

128 
abs_rel_weight = 0.5, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset

129 
abs_irrel_weight = 2.0, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset

130 
skolem_irrel_weight = 0.75, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset

131 
theory_const_rel_weight = 0.5, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset

132 
theory_const_irrel_weight = 0.25, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset

133 
intro_bonus = 0.15, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset

134 
elim_bonus = 0.15, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset

135 
simp_bonus = 0.15, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset

136 
local_bonus = 0.55, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset

137 
assum_bonus = 1.05, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset

138 
chained_bonus = 1.5, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset

139 
max_imperfect = 11.5, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset

140 
max_imperfect_exp = 1.0, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset

141 
threshold_divisor = 2.0, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset

142 
ridiculous_threshold = 0.1} 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset

143 

40071
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset

144 
(* FUDGE (FIXME) *) 
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset

145 
val smt_relevance_fudge = 
40071
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset

146 
{worse_irrel_freq = #worse_irrel_freq atp_relevance_fudge, 
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset

147 
higher_order_irrel_weight = #higher_order_irrel_weight atp_relevance_fudge, 
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset

148 
abs_rel_weight = #abs_rel_weight atp_relevance_fudge, 
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset

149 
abs_irrel_weight = #abs_irrel_weight atp_relevance_fudge, 
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset

150 
skolem_irrel_weight = #skolem_irrel_weight atp_relevance_fudge, 
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset

151 
theory_const_rel_weight = #theory_const_rel_weight atp_relevance_fudge, 
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset

152 
theory_const_irrel_weight = #theory_const_irrel_weight atp_relevance_fudge, 
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset

153 
intro_bonus = #intro_bonus atp_relevance_fudge, 
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset

154 
elim_bonus = #elim_bonus atp_relevance_fudge, 
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset

155 
simp_bonus = #simp_bonus atp_relevance_fudge, 
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset

156 
local_bonus = #local_bonus atp_relevance_fudge, 
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset

157 
assum_bonus = #assum_bonus atp_relevance_fudge, 
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset

158 
chained_bonus = #chained_bonus atp_relevance_fudge, 
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset

159 
max_imperfect = #max_imperfect atp_relevance_fudge, 
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset

160 
max_imperfect_exp = #max_imperfect_exp atp_relevance_fudge, 
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset

161 
threshold_divisor = #threshold_divisor atp_relevance_fudge, 
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset

162 
ridiculous_threshold = #ridiculous_threshold atp_relevance_fudge} 
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset

163 

bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset

164 
fun relevance_fudge_for_prover name = 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset

165 
if is_smt_prover name then smt_relevance_fudge else atp_relevance_fudge 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset

166 

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

167 
fun available_provers thy = 
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

168 
let 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

169 
val (remote_provers, local_provers) = 
40062  170 
sort_strings (available_atps thy) @ smt_prover_names 
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

171 
> List.partition (String.isPrefix remote_prefix) 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

172 
in 
40205
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset

173 
Output.urgent_message ("Available provers: " ^ 
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset

174 
commas (local_provers @ remote_provers) ^ ".") 
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

175 
end 
35969  176 

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

177 
fun kill_provers () = Async_Manager.kill_threads das_Tool "provers" 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

178 
fun running_provers () = Async_Manager.running_threads das_Tool "provers" 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

179 
val messages = Async_Manager.thread_messages das_Tool "prover" 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

180 

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

181 
(** problems, results, ATPs, etc. **) 
35969  182 

183 
type params = 

38982
820b8221ed48
added "blocking" option to Sledgehammer to run in synchronous mode;
blanchet
parents:
38893
diff
changeset

184 
{blocking: bool, 
820b8221ed48
added "blocking" option to Sledgehammer to run in synchronous mode;
blanchet
parents:
38893
diff
changeset

185 
debug: bool, 
35969  186 
verbose: bool, 
36143
6490319b1703
added "overlord" option (to get easy access to output files for debugging) + systematically use "raw_goal" rather than an inconsistent mixture
blanchet
parents:
36064
diff
changeset

187 
overlord: bool, 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

188 
provers: string list, 
35969  189 
full_types: bool, 
36235
61159615a0c5
added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)
blanchet
parents:
36231
diff
changeset

190 
explicit_apply: bool, 
38745
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset

191 
relevance_thresholds: real * real, 
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38741
diff
changeset

192 
max_relevant: int option, 
35969  193 
isar_proof: bool, 
36924  194 
isar_shrink_factor: int, 
38985
162bbbea4e4d
added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents:
38982
diff
changeset

195 
timeout: Time.time, 
162bbbea4e4d
added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents:
38982
diff
changeset

196 
expect: string} 
35867  197 

40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40202
diff
changeset

198 
datatype fact = 
40114  199 
Untranslated of (string * locality) * thm  
200 
Translated of term * ((string * locality) * translated_formula) option 

40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

201 

71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

202 
type prover_problem = 
39318  203 
{state: Proof.state, 
38998  204 
goal: thm, 
205 
subgoal: int, 

40065  206 
subgoal_count: int, 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40202
diff
changeset

207 
facts: fact list, 
39366
f58fbb959826
handle relevance filter corner cases more gracefully;
blanchet
parents:
39364
diff
changeset

208 
only: bool} 
35867  209 

40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

210 
type prover_result = 
36370
a4f601daa175
centralized ATPspecific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset

211 
{outcome: failure option, 
35969  212 
message: string, 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40202
diff
changeset

213 
used_facts: (string * locality) list, 
40062  214 
run_time_in_msecs: int option} 
35867  215 

40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

216 
type prover = params > minimize_command > prover_problem > prover_result 
35867  217 

38023  218 
(* configuration attributes *) 
219 

38991  220 
val (dest_dir, dest_dir_setup) = 
39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset

221 
Attrib.config_string "sledgehammer_dest_dir" (K "") 
38991  222 
(* Empty string means create files in Isabelle's temporary files directory. *) 
38023  223 

224 
val (problem_prefix, problem_prefix_setup) = 

39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset

225 
Attrib.config_string "sledgehammer_problem_prefix" (K "prob") 
38023  226 

39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset

227 
val (measure_run_time, measure_run_time_setup) = 
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset

228 
Attrib.config_bool "sledgehammer_measure_run_time" (K false) 
28484  229 

38023  230 
fun with_path cleanup after f path = 
231 
Exn.capture f path 

232 
> tap (fn _ => cleanup path) 

233 
> Exn.release 

234 
> tap (after path) 

235 

40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40202
diff
changeset

236 
fun prover_description ctxt ({blocking, verbose, ...} : params) name num_facts i 
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40202
diff
changeset

237 
n goal = 
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

238 
quote name ^ 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

239 
(if verbose then 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40202
diff
changeset

240 
" with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts 
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

241 
else 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

242 
"") ^ 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

243 
" on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^ ":" ^ 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

244 
(if blocking then 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

245 
"" 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

246 
else 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

247 
"\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i))) 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

248 

5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

249 
fun proof_banner auto = 
40224  250 
if auto then "Auto Sledgehammer found a proof" else "Try this command" 
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

251 

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

252 
(* generic TPTPbased ATPs *) 
38023  253 

40114  254 
fun dest_Untranslated (Untranslated p) = p 
255 
 dest_Untranslated (Translated _) = raise Fail "dest_Untranslated" 

40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40202
diff
changeset

256 
fun translated_fact ctxt (Untranslated p) = translate_fact ctxt p 
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40202
diff
changeset

257 
 translated_fact _ (Translated p) = p 
40205
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset

258 
fun fact_name (Untranslated ((name, _), _)) = SOME name 
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset

259 
 fact_name (Translated (_, p)) = Option.map (fst o fst) p 
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

260 

40409
3642dc3b72e8
invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents:
40370
diff
changeset

261 
fun int_opt_add (SOME m) (SOME n) = SOME (m + n) 
3642dc3b72e8
invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents:
40370
diff
changeset

262 
 int_opt_add _ _ = NONE 
40062  263 

39492  264 
(* Important messages are important but not so important that users want to see 
265 
them each time. *) 

39493
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39492
diff
changeset

266 
val important_message_keep_factor = 0.1 
39492  267 

40063
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset

268 
fun run_atp auto atp_name 
38645  269 
{exec, required_execs, arguments, has_incomplete_mode, proof_delims, 
38997  270 
known_failures, default_max_relevant, explicit_forall, 
271 
use_conjecture_for_hypotheses} 

38455  272 
({debug, verbose, overlord, full_types, explicit_apply, 
38998  273 
max_relevant, isar_proof, isar_shrink_factor, timeout, ...} : params) 
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

274 
minimize_command 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40202
diff
changeset

275 
({state, goal, subgoal, facts, only, ...} : prover_problem) = 
38023  276 
let 
39318  277 
val ctxt = Proof.context_of state 
38998  278 
val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40202
diff
changeset

279 
val facts = 
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40202
diff
changeset

280 
facts > not only ? take (the_default default_max_relevant max_relevant) 
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40202
diff
changeset

281 
> map (translated_fact ctxt) 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

282 
val dest_dir = if overlord then getenv "ISABELLE_HOME_USER" 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

283 
else Config.get ctxt dest_dir 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

284 
val problem_prefix = Config.get ctxt problem_prefix 
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

285 
val problem_file_name = 
39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset

286 
Path.basic ((if overlord then "prob_" ^ atp_name 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

287 
else problem_prefix ^ serial_string ()) 
39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset

288 
^ "_" ^ string_of_int subgoal) 
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

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

290 
if dest_dir = "" then 
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

291 
File.tmp_path problem_file_name 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

292 
else if File.exists (Path.explode dest_dir) then 
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

293 
Path.append (Path.explode dest_dir) problem_file_name 
39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset

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

295 
error ("No such directory: " ^ quote dest_dir ^ ".") 
39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset

296 
val measure_run_time = verbose orelse Config.get ctxt measure_run_time 
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:
38091
diff
changeset

297 
val command = Path.explode (getenv (fst exec) ^ "/" ^ snd exec) 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

298 
(* write out problem file and call ATP *) 
38645  299 
fun command_line complete timeout probfile = 
38023  300 
let 
301 
val core = File.shell_path command ^ " " ^ arguments complete timeout ^ 

302 
" " ^ File.shell_path probfile 

303 
in 

39010  304 
(if measure_run_time then "TIMEFORMAT='%3R'; { time " ^ core ^ " ; }" 
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38741
diff
changeset

305 
else "exec " ^ core) ^ " 2>&1" 
38023  306 
end 
307 
fun split_time s = 

308 
let 

309 
val split = String.tokens (fn c => str c = "\n"); 

310 
val (output, t) = s > split > split_last > apfst cat_lines; 

311 
fun as_num f = f >> (fst o read_int); 

312 
val num = as_num (Scan.many1 Symbol.is_ascii_digit); 

313 
val digit = Scan.one Symbol.is_ascii_digit; 

314 
val num3 = as_num (digit ::: digit ::: (digit >> single)); 

315 
val time = num  Scan.$$ "."  num3 >> (fn (a, b) => a * 1000 + b); 

40062  316 
val as_time = Scan.read Symbol.stopper time o explode 
38023  317 
in (output, as_time t) end; 
318 
fun run_on probfile = 

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:
38091
diff
changeset

319 
case filter (curry (op =) "" o getenv o fst) (exec :: required_execs) of 
38032  320 
(home_var, _) :: _ => 
38023  321 
error ("The environment variable " ^ quote home_var ^ " is not set.") 
38032  322 
 [] => 
323 
if File.exists command then 

324 
let 

39318  325 
fun run complete timeout = 
38032  326 
let 
38645  327 
val command = command_line complete timeout probfile 
38032  328 
val ((output, msecs), res_code) = 
329 
bash_output command 

330 
>> (if overlord then 

331 
prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") 

332 
else 

333 
I) 

40062  334 
>> (if measure_run_time then split_time else rpair NONE) 
39452  335 
val (tstplike_proof, outcome) = 
336 
extract_tstplike_proof_and_outcome complete res_code 

337 
proof_delims known_failures output 

338 
in (output, msecs, tstplike_proof, outcome) end 

38032  339 
val readable_names = debug andalso overlord 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40202
diff
changeset

340 
val (atp_problem, pool, conjecture_offset, fact_names) = 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

341 
prepare_atp_problem ctxt readable_names explicit_forall full_types 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40202
diff
changeset

342 
explicit_apply hyp_ts concl_t facts 
39452  343 
val ss = tptp_strings_for_atp_problem use_conjecture_for_hypotheses 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

344 
atp_problem 
38631
979a0b37f981
prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible;
blanchet
parents:
38600
diff
changeset

345 
val _ = File.write_list probfile ss 
38032  346 
val conjecture_shape = 
347 
conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1 

38040
174568533593
fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
blanchet
parents:
38039
diff
changeset

348 
> map single 
39318  349 
val run_twice = has_incomplete_mode andalso not auto 
38645  350 
val timer = Timer.startRealTimer () 
38032  351 
val result = 
39318  352 
run false (if run_twice then 
353 
Time.fromMilliseconds 

38645  354 
(2 * Time.toMilliseconds timeout div 3) 
39318  355 
else 
356 
timeout) 

357 
> run_twice 

38645  358 
? (fn (_, msecs0, _, SOME _) => 
39318  359 
run true (Time. (timeout, Timer.checkRealTimer timer)) 
39452  360 
> (fn (output, msecs, tstplike_proof, outcome) => 
40409
3642dc3b72e8
invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents:
40370
diff
changeset

361 
(output, int_opt_add msecs0 msecs, tstplike_proof, 
3642dc3b72e8
invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents:
40370
diff
changeset

362 
outcome)) 
38645  363 
 result => result) 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40202
diff
changeset

364 
in ((pool, conjecture_shape, fact_names), result) end 
38032  365 
else 
366 
error ("Bad executable: " ^ Path.implode command ^ ".") 

38023  367 

368 
(* If the problem file has not been exported, remove it; otherwise, export 

369 
the proof file too. *) 

370 
fun cleanup probfile = 

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

371 
if dest_dir = "" then try File.rm probfile else NONE 
38023  372 
fun export probfile (_, (output, _, _, _)) = 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

373 
if dest_dir = "" then 
38023  374 
() 
375 
else 

376 
File.write (Path.explode (Path.implode probfile ^ "_proof")) output 

40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40202
diff
changeset

377 
val ((pool, conjecture_shape, fact_names), 
39452  378 
(output, msecs, tstplike_proof, outcome)) = 
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

379 
with_path cleanup export run_on problem_path_name 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40202
diff
changeset

380 
val (conjecture_shape, fact_names) = 
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40202
diff
changeset

381 
repair_conjecture_shape_and_fact_names output conjecture_shape fact_names 
39492  382 
val important_message = 
40224  383 
if not auto andalso random () <= important_message_keep_factor then 
39492  384 
extract_important_message output 
385 
else 

386 
"" 

40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40202
diff
changeset

387 
val (message, used_facts) = 
38023  388 
case outcome of 
389 
NONE => 

390 
proof_text isar_proof 

391 
(pool, debug, isar_shrink_factor, ctxt, conjecture_shape) 

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

392 
(proof_banner auto, full_types, minimize_command, tstplike_proof, 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40202
diff
changeset

393 
fact_names, goal, subgoal) 
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38741
diff
changeset

394 
>> (fn message => 
40341
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
40224
diff
changeset

395 
message ^ 
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
40224
diff
changeset

396 
(if verbose then 
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
40224
diff
changeset

397 
"\nATP real CPU time: " ^ 
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
40224
diff
changeset

398 
string_from_time (Time.fromMilliseconds (the msecs)) ^ "." 
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
40224
diff
changeset

399 
else 
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
40224
diff
changeset

400 
"") ^ 
39107
0a62f8a94af3
If Geoff puts some important message in his TPTP problems (e.g., money requests), we should show them to the user
blanchet
parents:
39010
diff
changeset

401 
(if important_message <> "" then 
0a62f8a94af3
If Geoff puts some important message in his TPTP problems (e.g., money requests), we should show them to the user
blanchet
parents:
39010
diff
changeset

402 
"\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^ 
0a62f8a94af3
If Geoff puts some important message in his TPTP problems (e.g., money requests), we should show them to the user
blanchet
parents:
39010
diff
changeset

403 
important_message 
0a62f8a94af3
If Geoff puts some important message in his TPTP problems (e.g., money requests), we should show them to the user
blanchet
parents:
39010
diff
changeset

404 
else 
0a62f8a94af3
If Geoff puts some important message in his TPTP problems (e.g., money requests), we should show them to the user
blanchet
parents:
39010
diff
changeset

405 
"")) 
38597
db482afec7f0
no spurious trailing "\n" at the end of Sledgehammer's output
blanchet
parents:
38590
diff
changeset

406 
 SOME failure => (string_for_failure failure, []) 
38023  407 
in 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40202
diff
changeset

408 
{outcome = outcome, message = message, used_facts = used_facts, 
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

409 
run_time_in_msecs = msecs} 
38023  410 
end 
411 

40555  412 
(* "SMT_Failure.Solver_Crashed" is a misnomer; it should really be called 
413 
"Abnormal_Termination". Return codes 1 to 127 are applicationspecific, 

414 
whereas (at least on Unix) 128 to 255 are reserved for signals (e.g., 

415 
SIGSEGV) and other system codes. *) 

416 

40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40419
diff
changeset

417 
fun failure_from_smt_failure (SMT_Failure.Counterexample _) = Unprovable 
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40419
diff
changeset

418 
 failure_from_smt_failure SMT_Failure.Time_Out = TimedOut 
40555  419 
 failure_from_smt_failure (SMT_Failure.Solver_Crashed code) = 
420 
if code >= 128 then Crashed else IncompleteUnprovable 

40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40419
diff
changeset

421 
 failure_from_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources 
40207
5da3e8ede850
adapted SMT solver error handling to reflect latest changes in "SMT_Solver"
blanchet
parents:
40206
diff
changeset

422 
 failure_from_smt_failure _ = UnknownError 
40063
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset

423 

40553
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

424 
val smt_max_iter = 8 
40419
718b44dbd74d
make sure the SMT solver runs several iterations by lowering the timeout at each iteration  yields better results in practice
blanchet
parents:
40417
diff
changeset

425 
val smt_iter_fact_divisor = 2 
718b44dbd74d
make sure the SMT solver runs several iterations by lowering the timeout at each iteration  yields better results in practice
blanchet
parents:
40417
diff
changeset

426 
val smt_iter_min_msecs = 5000 
718b44dbd74d
make sure the SMT solver runs several iterations by lowering the timeout at each iteration  yields better results in practice
blanchet
parents:
40417
diff
changeset

427 
val smt_iter_timeout_divisor = 2 
40439
fb6ee11e776a
reduce the number of monomorphization iterations from 10 (the default) to 4, in the interest of faster SMT solving
blanchet
parents:
40428
diff
changeset

428 
val smt_monomorph_limit = 4 
40409
3642dc3b72e8
invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents:
40370
diff
changeset

429 

40553
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

430 
fun smt_filter_loop ({debug, verbose, timeout, ...} : params) remote state i = 
40409
3642dc3b72e8
invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents:
40370
diff
changeset

431 
let 
40553
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

432 
val ctxt = Proof.context_of state 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

433 
fun iter timeout iter_num outcome0 msecs_so_far facts = 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

434 
let 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

435 
val timer = Timer.startRealTimer () 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

436 
val ms = timeout > Time.toMilliseconds 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

437 
val iter_timeout = 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

438 
if iter_num < smt_max_iter then 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

439 
Int.min (ms, Int.max (smt_iter_min_msecs, 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

440 
ms div smt_iter_timeout_divisor)) 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

441 
> Time.fromMilliseconds 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

442 
else 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

443 
timeout 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

444 
val num_facts = length facts 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

445 
val _ = 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

446 
if verbose then 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

447 
"SMT iteration with " ^ string_of_int num_facts ^ " fact" ^ 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

448 
plural_s num_facts ^ " for " ^ string_from_time iter_timeout ^ 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

449 
"..." 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

450 
> Output.urgent_message 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

451 
else 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

452 
() 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

453 
val {outcome, used_facts, run_time_in_msecs} = 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

454 
TimeLimit.timeLimit iter_timeout 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

455 
(SMT_Solver.smt_filter remote iter_timeout state facts) i 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

456 
handle TimeLimit.TimeOut => 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

457 
{outcome = SOME SMT_Failure.Time_Out, used_facts = [], 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

458 
run_time_in_msecs = NONE} 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

459 
val _ = 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

460 
if verbose andalso is_some outcome then 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

461 
"SMT outcome: " ^ SMT_Failure.string_of_failure ctxt (the outcome) 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

462 
> Output.urgent_message 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

463 
else 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

464 
() 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

465 
val outcome0 = if is_none outcome0 then SOME outcome else outcome0 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

466 
val msecs_so_far = int_opt_add run_time_in_msecs msecs_so_far 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

467 
val too_many_facts_perhaps = 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

468 
case outcome of 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

469 
NONE => false 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

470 
 SOME (SMT_Failure.Counterexample _) => false 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

471 
 SOME SMT_Failure.Time_Out => iter_timeout <> timeout 
40555  472 
 SOME (SMT_Failure.Solver_Crashed code) => 
40553
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

473 
(if verbose then 
40555  474 
"The SMT solver invoked with " ^ string_of_int num_facts ^ 
475 
" fact" ^ plural_s num_facts ^ " terminated abnormally with \ 

40556  476 
\exit code " ^ string_of_int code ^ "." 
40553
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

477 
> (if debug then error else warning) 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

478 
else 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

479 
(); 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

480 
true (* kind of *)) 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

481 
 SOME SMT_Failure.Out_Of_Memory => true 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

482 
 SOME _ => true 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

483 
val timeout = Time. (timeout, Timer.checkRealTimer timer) 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

484 
in 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

485 
if too_many_facts_perhaps andalso iter_num < smt_max_iter andalso 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

486 
num_facts > 0 andalso Time.> (timeout, Time.zeroTime) then 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

487 
let val facts = take (num_facts div smt_iter_fact_divisor) facts in 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

488 
iter timeout (iter_num + 1) outcome0 msecs_so_far facts 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

489 
end 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

490 
else 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

491 
{outcome = if is_none outcome then NONE else the outcome0, 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

492 
used_facts = used_facts, run_time_in_msecs = msecs_so_far} 
40409
3642dc3b72e8
invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents:
40370
diff
changeset

493 
end 
40553
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

494 
in iter timeout 1 NONE (SOME 0) end 
40409
3642dc3b72e8
invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents:
40370
diff
changeset

495 

40553
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

496 
fun run_smt_solver auto remote (params as {debug, ...}) minimize_command 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

497 
({state, subgoal, subgoal_count, facts, ...} : prover_problem) = 
36379
20ef039bccff
make "ATP_Manager.get_prover" a total function, since we always want to show the same error text
blanchet
parents:
36373
diff
changeset

498 
let 
40439
fb6ee11e776a
reduce the number of monomorphization iterations from 10 (the default) to 4, in the interest of faster SMT solving
blanchet
parents:
40428
diff
changeset

499 
val repair_context = 
fb6ee11e776a
reduce the number of monomorphization iterations from 10 (the default) to 4, in the interest of faster SMT solving
blanchet
parents:
40428
diff
changeset

500 
Config.put SMT_Config.verbose debug 
fb6ee11e776a
reduce the number of monomorphization iterations from 10 (the default) to 4, in the interest of faster SMT solving
blanchet
parents:
40428
diff
changeset

501 
#> Config.put SMT_Config.monomorph_limit smt_monomorph_limit 
fb6ee11e776a
reduce the number of monomorphization iterations from 10 (the default) to 4, in the interest of faster SMT solving
blanchet
parents:
40428
diff
changeset

502 
val state = state > Proof.map_context repair_context 
40207
5da3e8ede850
adapted SMT solver error handling to reflect latest changes in "SMT_Solver"
blanchet
parents:
40206
diff
changeset

503 
val ctxt = Proof.context_of state 
40181  504 
val {outcome, used_facts, run_time_in_msecs} = 
40553
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

505 
smt_filter_loop params remote state subgoal 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

506 
(map_filter (try dest_Untranslated) facts) 
40063
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset

507 
val message = 
40184
91b4b73dbafb
proper error handling for SMT solvers in Sledgehammer
blanchet
parents:
40181
diff
changeset

508 
case outcome of 
91b4b73dbafb
proper error handling for SMT solvers in Sledgehammer
blanchet
parents:
40181
diff
changeset

509 
NONE => 
40224  510 
try_command_line (proof_banner auto) 
40065  511 
(apply_on_subgoal subgoal subgoal_count ^ 
40181  512 
command_call smtN (map fst used_facts)) ^ 
513 
minimize_line minimize_command (map fst used_facts) 

40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40419
diff
changeset

514 
 SOME SMT_Failure.Time_Out => "Timed out." 
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40419
diff
changeset

515 
 SOME (SMT_Failure.Counterexample _) => "The SMT problem is unprovable." 
40207
5da3e8ede850
adapted SMT solver error handling to reflect latest changes in "SMT_Solver"
blanchet
parents:
40206
diff
changeset

516 
 SOME failure => 
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40419
diff
changeset

517 
SMT_Failure.string_of_failure ctxt failure 
40200  518 
val outcome = outcome > Option.map failure_from_smt_failure (* FIXME *) 
40063
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset

519 
in 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40202
diff
changeset

520 
{outcome = outcome, used_facts = used_facts, 
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40202
diff
changeset

521 
run_time_in_msecs = run_time_in_msecs, message = message} 
40063
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset

522 
end 
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset

523 

40200  524 
fun get_prover thy auto name = 
40224  525 
if is_smt_prover name then 
526 
run_smt_solver auto (String.isPrefix remote_prefix name) 

527 
else 

528 
run_atp auto name (get_atp thy name) 

40063
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset

529 

d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset

530 
fun run_prover (params as {blocking, debug, max_relevant, timeout, expect, ...}) 
40065  531 
auto minimize_command 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40202
diff
changeset

532 
(problem as {state, goal, subgoal, subgoal_count, facts, ...}) 
40063
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset

533 
name = 
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset

534 
let 
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset

535 
val thy = Proof.theory_of state 
39318  536 
val ctxt = Proof.context_of state 
37584  537 
val birth_time = Time.now () 
538 
val death_time = Time.+ (birth_time, timeout) 

40063
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset

539 
val max_relevant = 
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset

540 
the_default (default_max_relevant_for_prover thy name) max_relevant 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40202
diff
changeset

541 
val num_facts = Int.min (length facts, max_relevant) 
40065  542 
val desc = 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40202
diff
changeset

543 
prover_description ctxt params name num_facts subgoal subgoal_count goal 
39318  544 
fun go () = 
38982
820b8221ed48
added "blocking" option to Sledgehammer to run in synchronous mode;
blanchet
parents:
38893
diff
changeset

545 
let 
39453
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for oneliners as for Isar proofs
blanchet
parents:
39452
diff
changeset

546 
fun really_go () = 
40200  547 
get_prover thy auto name params (minimize_command name) problem 
38985
162bbbea4e4d
added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents:
38982
diff
changeset

548 
> (fn {outcome, message, ...} => 
162bbbea4e4d
added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents:
38982
diff
changeset

549 
(if is_some outcome then "none" else "some", message)) 
39453
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for oneliners as for Isar proofs
blanchet
parents:
39452
diff
changeset

550 
val (outcome_code, message) = 
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for oneliners as for Isar proofs
blanchet
parents:
39452
diff
changeset

551 
if debug then 
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for oneliners as for Isar proofs
blanchet
parents:
39452
diff
changeset

552 
really_go () 
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for oneliners as for Isar proofs
blanchet
parents:
39452
diff
changeset

553 
else 
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for oneliners as for Isar proofs
blanchet
parents:
39452
diff
changeset

554 
(really_go () 
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for oneliners as for Isar proofs
blanchet
parents:
39452
diff
changeset

555 
handle ERROR message => ("unknown", "Error: " ^ message ^ "\n") 
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for oneliners as for Isar proofs
blanchet
parents:
39452
diff
changeset

556 
 exn => ("unknown", "Internal error:\n" ^ 
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for oneliners as for Isar proofs
blanchet
parents:
39452
diff
changeset

557 
ML_Compiler.exn_message exn ^ "\n")) 
39318  558 
val _ = 
559 
if expect = "" orelse outcome_code = expect then 

560 
() 

561 
else if blocking then 

562 
error ("Unexpected outcome: " ^ quote outcome_code ^ ".") 

563 
else 

564 
warning ("Unexpected outcome: " ^ quote outcome_code ^ "."); 

565 
in (outcome_code = "some", message) end 

566 
in 

567 
if auto then 

568 
let val (success, message) = TimeLimit.timeLimit timeout go () in 

569 
(success, state > success ? Proof.goal_message (fn () => 

570 
Pretty.chunks [Pretty.str "", Pretty.mark Markup.hilite 

39327  571 
(Pretty.str message)])) 
38982
820b8221ed48
added "blocking" option to Sledgehammer to run in synchronous mode;
blanchet
parents:
38893
diff
changeset

572 
end 
39318  573 
else if blocking then 
574 
let val (success, message) = TimeLimit.timeLimit timeout go () in 

40132
7ee65dbffa31
renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
wenzelm
parents:
40114
diff
changeset

575 
List.app Output.urgent_message 
39370
f8292d3020db
use same hack as in "Async_Manager" to work around Proof General bug
blanchet
parents:
39366
diff
changeset

576 
(Async_Manager.break_into_chunks [desc ^ "\n" ^ message]); 
f8292d3020db
use same hack as in "Async_Manager" to work around Proof General bug
blanchet
parents:
39366
diff
changeset

577 
(success, state) 
39318  578 
end 
579 
else 

580 
(Async_Manager.launch das_Tool birth_time death_time desc (snd o go); 

581 
(false, state)) 

37584  582 
end 
28582  583 

40205
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset

584 
fun run_sledgehammer (params as {blocking, debug, provers, full_types, 
40069  585 
relevance_thresholds, max_relevant, ...}) 
39366
f58fbb959826
handle relevance filter corner cases more gracefully;
blanchet
parents:
39364
diff
changeset

586 
auto i (relevance_override as {only, ...}) minimize_command 
f58fbb959826
handle relevance filter corner cases more gracefully;
blanchet
parents:
39364
diff
changeset

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

588 
if null provers then 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

589 
error "No prover is set." 
39318  590 
else case subgoal_count state of 
40132
7ee65dbffa31
renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
wenzelm
parents:
40114
diff
changeset

591 
0 => (Output.urgent_message "No subgoal!"; (false, state)) 
39318  592 
 n => 
593 
let 

39364  594 
val _ = Proof.assert_backward state 
39318  595 
val thy = Proof.theory_of state 
40200  596 
val ctxt = Proof.context_of state 
597 
val {facts = chained_ths, goal, ...} = Proof.goal state 

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

598 
val (_, hyp_ts, concl_t) = strip_subgoal goal i 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

599 
val _ = () > not blocking ? kill_provers 
40132
7ee65dbffa31
renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
wenzelm
parents:
40114
diff
changeset

600 
val _ = if auto then () else Output.urgent_message "Sledgehammering..." 
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset

601 
val (smts, atps) = provers > List.partition is_smt_prover 
40369
53dca3bd4250
use the SMT integration's official list of builtins
blanchet
parents:
40341
diff
changeset

602 
fun run_provers label full_types relevance_fudge maybe_translate provers 
53dca3bd4250
use the SMT integration's official list of builtins
blanchet
parents:
40341
diff
changeset

603 
(res as (success, state)) = 
40065  604 
if success orelse null provers then 
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

605 
res 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

606 
else 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

607 
let 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

608 
val max_max_relevant = 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

609 
case max_relevant of 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

610 
SOME n => n 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

611 
 NONE => 
40063
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset

612 
0 > fold (Integer.max o default_max_relevant_for_prover thy) 
40065  613 
provers 
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

614 
> auto ? (fn n => n div auto_max_relevant_divisor) 
40369
53dca3bd4250
use the SMT integration's official list of builtins
blanchet
parents:
40341
diff
changeset

615 
val is_built_in_const = 
53dca3bd4250
use the SMT integration's official list of builtins
blanchet
parents:
40341
diff
changeset

616 
is_built_in_const_for_prover ctxt (hd provers) 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40202
diff
changeset

617 
val facts = 
40065  618 
relevant_facts ctxt full_types relevance_thresholds 
40369
53dca3bd4250
use the SMT integration's official list of builtins
blanchet
parents:
40341
diff
changeset

619 
max_max_relevant is_built_in_const relevance_fudge 
40071
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset

620 
relevance_override chained_ths hyp_ts concl_t 
40114  621 
> map maybe_translate 
40062  622 
val problem = 
40065  623 
{state = state, goal = goal, subgoal = i, subgoal_count = n, 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40202
diff
changeset

624 
facts = facts, only = only} 
40065  625 
val run_prover = run_prover params auto minimize_command 
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

626 
in 
40205
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset

627 
if debug then 
40370  628 
Output.urgent_message (label ^ plural_s (length provers) ^ ": " ^ 
40205
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset

629 
(if null facts then 
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset

630 
"Found no relevant facts." 
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset

631 
else 
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset

632 
"Including (up to) " ^ string_of_int (length facts) ^ 
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset

633 
" relevant fact" ^ plural_s (length facts) ^ ":\n" ^ 
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset

634 
(facts > map_filter fact_name 
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset

635 
> space_implode " ") ^ ".")) 
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset

636 
else 
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset

637 
(); 
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

638 
if auto then 
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

639 
fold (fn prover => fn (true, state) => (true, state) 
40064
db8413d82c3b
got rid of duplicate functionality ("run_smt_solver_somehow");
blanchet
parents:
40063
diff
changeset

640 
 (false, _) => run_prover problem prover) 
40065  641 
provers (false, state) 
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

642 
else 
40065  643 
provers > (if blocking then Par_List.map else map) 
644 
(run_prover problem) 

645 
> exists fst > rpair state 

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

646 
end 
40071
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset

647 
val run_atps = 
40370  648 
run_provers "ATP" full_types atp_relevance_fudge 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40202
diff
changeset

649 
(Translated o translate_fact ctxt) atps 
40071
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset

650 
val run_smts = 
40370  651 
run_provers "SMT solver" true smt_relevance_fudge Untranslated smts 
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

652 
fun run_atps_and_smt_solvers () = 
40065  653 
[run_atps, run_smts] > Par_List.map (fn f => f (false, state) > K ()) 
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

654 
in 
40065  655 
(false, state) 
656 
> (if blocking then run_atps #> not auto ? run_smts 

657 
else (fn p => Future.fork (tap run_atps_and_smt_solvers) > K p)) 

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

658 
end 
38044  659 

38023  660 
val setup = 
661 
dest_dir_setup 

662 
#> problem_prefix_setup 

39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset

663 
#> measure_run_time_setup 
38023  664 

28582  665 
end; 