author  blanchet 
Tue, 08 Feb 2011 16:10:10 +0100  
changeset 41727  ab3f6d76fb23 
parent 41723  bb366da22483 
child 41741  839d1488045f 
permissions  rwrr 
41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
41066
diff
changeset

1 
(* Title: HOL/Tools/Sledgehammer/sledgehammer_provers.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 

41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
41066
diff
changeset

6 
Generic prover abstraction for Sledgehammer. 
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 

41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
41066
diff
changeset

9 
signature SLEDGEHAMMER_PROVERS = 
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 
40114  14 
type translated_formula = Sledgehammer_ATP_Translate.translated_formula 
41138
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41136
diff
changeset

15 
type type_system = Sledgehammer_ATP_Translate.type_system 
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 = 
41208
1b28c43a7074
make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive
blanchet
parents:
41171
diff
changeset

19 
{debug: bool, 
35969  20 
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

21 
overlord: bool, 
41208
1b28c43a7074
make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive
blanchet
parents:
41171
diff
changeset

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

23 
provers: string list, 
41138
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41136
diff
changeset

24 
type_sys: type_system, 
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 

41090  33 
datatype prover_fact = 
34 
Untranslated_Fact of (string * locality) * thm  

35 
ATP_Translated_Fact of 

41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset

36 
translated_formula option * ((string * locality) * thm)  
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset

37 
SMT_Weighted_Fact of (string * locality) * (int option * thm) 
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

38 

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

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

40065  43 
subgoal_count: int, 
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset

44 
facts: prover_fact list, 
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41336
diff
changeset

45 
smt_head: (string * locality) SMT_Solver.smt_filter_data option} 
39493
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39492
diff
changeset

46 

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

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

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

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

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

52 

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

53 
type prover = params > minimize_command > prover_problem > prover_result 
35867  54 

41168  55 
(* for experimentation purposes  do not use in production code *) 
41318
adcb92c0513b
run SPASS and Vampire in SOS mode only if >= 50 facts are passed  otherwise we are probably minimizing and then it's better if the prover is run only once with a full strategy
blanchet
parents:
41315
diff
changeset

56 
val atp_run_twice_threshold : int Unsynchronized.ref 
41313
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41259
diff
changeset

57 
val atp_first_iter_time_frac : real Unsynchronized.ref 
41335
66edbd0f7a2e
added "smt_triggers" option to experiment with triggers in Sledgehammer;
blanchet
parents:
41318
diff
changeset

58 
val smt_triggers : bool Unsynchronized.ref 
41256
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset

59 
val smt_weights : bool Unsynchronized.ref 
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset

60 
val smt_weight_min_facts : int Unsynchronized.ref 
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset

61 
val smt_min_weight : int Unsynchronized.ref 
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset

62 
val smt_max_weight : int Unsynchronized.ref 
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset

63 
val smt_max_weight_index : int Unsynchronized.ref 
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset

64 
val smt_weight_curve : (int > int) Unsynchronized.ref 
41222  65 
val smt_max_iters : int Unsynchronized.ref 
41169  66 
val smt_iter_fact_frac : real Unsynchronized.ref 
67 
val smt_iter_time_frac : real Unsynchronized.ref 

41168  68 
val smt_iter_min_msecs : int Unsynchronized.ref 
41335
66edbd0f7a2e
added "smt_triggers" option to experiment with triggers in Sledgehammer;
blanchet
parents:
41318
diff
changeset

69 
val smt_monomorphize_limit : int Unsynchronized.ref 
41168  70 

41089  71 
val das_Tool : string 
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset

72 
val select_smt_solver : string > Proof.context > Proof.context 
41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
41066
diff
changeset

73 
val is_smt_prover : Proof.context > string > bool 
41727
ab3f6d76fb23
available_provers ~> supported_provers (for clarity)
blanchet
parents:
41723
diff
changeset

74 
val is_prover_supported : Proof.context > string > bool 
40072
27f2a45b0aab
more robust handling of "remote_" vs. non"remote_" provers
blanchet
parents:
40071
diff
changeset

75 
val is_prover_installed : Proof.context > string > bool 
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3"  whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset

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

77 
val is_built_in_const_for_prover : 
41336
0ea5b9c7d233
proper handling of the arguments of SMT builtins  for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents:
41335
diff
changeset

78 
Proof.context > string > string * typ > term list > bool * term list 
41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
41066
diff
changeset

79 
val atp_relevance_fudge : relevance_fudge 
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
41066
diff
changeset

80 
val smt_relevance_fudge : relevance_fudge 
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3"  whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset

81 
val relevance_fudge_for_prover : Proof.context > string > relevance_fudge 
38023  82 
val dest_dir : string Config.T 
83 
val problem_prefix : string Config.T 

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

84 
val measure_run_time : bool Config.T 
41256
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset

85 
val weight_smt_fact : 
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset

86 
theory > int > ((string * locality) * thm) * int 
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset

87 
> (string * locality) * (int option * thm) 
41091
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41090
diff
changeset

88 
val untranslated_fact : prover_fact > (string * locality) * thm 
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset

89 
val smt_weighted_fact : 
41256
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset

90 
theory > int > prover_fact * int 
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset

91 
> (string * locality) * (int option * thm) 
41727
ab3f6d76fb23
available_provers ~> supported_provers (for clarity)
blanchet
parents:
41723
diff
changeset

92 
val supported_provers : Proof.context > unit 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

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

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

95 
val messages : int option > unit 
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3"  whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset

96 
val get_prover : Proof.context > bool > string > prover 
38023  97 
val setup : theory > theory 
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset

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

99 

41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
41066
diff
changeset

100 
structure Sledgehammer_Provers : SLEDGEHAMMER_PROVERS = 
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset

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

102 

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

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

106 
open Metis_Translate 
38023  107 
open Sledgehammer_Util 
38988  108 
open Sledgehammer_Filter 
40068  109 
open Sledgehammer_ATP_Translate 
110 
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

111 

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

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

113 

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

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

115 
"Async_Manager". *) 
37585  116 
val das_Tool = "Sledgehammer" 
117 

41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset

118 
val select_smt_solver = 
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41336
diff
changeset

119 
Context.proof_map o SMT_Config.select_solver 
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset

120 

40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3"  whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset

121 
fun is_smt_prover ctxt name = 
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41336
diff
changeset

122 
member (op =) (SMT_Solver.available_solvers_of ctxt) name 
40062  123 

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

124 
fun is_prover_supported ctxt name = 
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3"  whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset

125 
let val thy = ProofContext.theory_of ctxt in 
41727
ab3f6d76fb23
available_provers ~> supported_provers (for clarity)
blanchet
parents:
41723
diff
changeset

126 
is_smt_prover ctxt name orelse member (op =) (supported_atps thy) name 
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3"  whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset

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

128 

41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41336
diff
changeset

129 
fun is_prover_installed ctxt = 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41336
diff
changeset

130 
is_smt_prover ctxt orf is_atp_installed (ProofContext.theory_of ctxt) 
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3"  whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset

131 

a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3"  whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset

132 
fun default_max_relevant_for_prover ctxt name = 
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3"  whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset

133 
let val thy = ProofContext.theory_of ctxt in 
40982
d06ffd777f1f
honor the default max relevant facts setting from the SMT solvers in Sledgehammer
blanchet
parents:
40979
diff
changeset

134 
if is_smt_prover ctxt name then 
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41336
diff
changeset

135 
SMT_Solver.default_max_relevant ctxt name 
40982
d06ffd777f1f
honor the default max relevant facts setting from the SMT solvers in Sledgehammer
blanchet
parents:
40979
diff
changeset

136 
else 
d06ffd777f1f
honor the default max relevant facts setting from the SMT solvers in Sledgehammer
blanchet
parents:
40979
diff
changeset

137 
#default_max_relevant (get_atp thy name) 
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3"  whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset

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

139 

41140
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

140 
(* These are either simplified away by "Meson.presimplify" (most of the time) or 
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

141 
handled specially via "fFalse", "fTrue", ..., "fequal". *) 
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

142 
val atp_irrelevant_consts = 
41140
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

143 
[@{const_name False}, @{const_name True}, @{const_name Not}, 
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

144 
@{const_name conj}, @{const_name disj}, @{const_name implies}, 
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

145 
@{const_name HOL.eq}, @{const_name If}, @{const_name Let}] 
40206  146 

41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset

147 
fun is_built_in_const_for_prover ctxt name = 
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset

148 
if is_smt_prover ctxt name then 
41336
0ea5b9c7d233
proper handling of the arguments of SMT builtins  for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents:
41335
diff
changeset

149 
let val ctxt = ctxt > select_smt_solver name in 
0ea5b9c7d233
proper handling of the arguments of SMT builtins  for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents:
41335
diff
changeset

150 
fn x => fn ts => 
0ea5b9c7d233
proper handling of the arguments of SMT builtins  for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents:
41335
diff
changeset

151 
if SMT_Builtin.is_builtin_num_ext ctxt (list_comb (Const x, ts)) then 
0ea5b9c7d233
proper handling of the arguments of SMT builtins  for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents:
41335
diff
changeset

152 
(true, []) 
0ea5b9c7d233
proper handling of the arguments of SMT builtins  for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents:
41335
diff
changeset

153 
else if SMT_Builtin.is_builtin_fun_ext ctxt x ts then 
0ea5b9c7d233
proper handling of the arguments of SMT builtins  for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents:
41335
diff
changeset

154 
(true, ts) 
0ea5b9c7d233
proper handling of the arguments of SMT builtins  for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents:
41335
diff
changeset

155 
else 
0ea5b9c7d233
proper handling of the arguments of SMT builtins  for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents:
41335
diff
changeset

156 
(false, ts) 
0ea5b9c7d233
proper handling of the arguments of SMT builtins  for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents:
41335
diff
changeset

157 
end 
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset

158 
else 
41336
0ea5b9c7d233
proper handling of the arguments of SMT builtins  for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents:
41335
diff
changeset

159 
fn (s, _) => fn ts => (member (op =) atp_irrelevant_consts s, ts) 
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

160 

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

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

162 
val atp_relevance_fudge = 
41159
1e12d6495423
honor "overlord" option for SMT solvers as well and don't pass "ext" to them
blanchet
parents:
41152
diff
changeset

163 
{allow_ext = true, 
1e12d6495423
honor "overlord" option for SMT solvers as well and don't pass "ext" to them
blanchet
parents:
41152
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

179 
threshold_divisor = 2.0, 
41093  180 
ridiculous_threshold = 0.01} 
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset

181 

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

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

183 
val smt_relevance_fudge = 
41159
1e12d6495423
honor "overlord" option for SMT solvers as well and don't pass "ext" to them
blanchet
parents:
41152
diff
changeset

184 
{allow_ext = false, 
1e12d6495423
honor "overlord" option for SMT solvers as well and don't pass "ext" to them
blanchet
parents:
41152
diff
changeset

185 
worse_irrel_freq = #worse_irrel_freq atp_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

186 
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

187 
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

188 
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

189 
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

190 
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

191 
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

192 
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

193 
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

194 
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

195 
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

196 
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

197 
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

198 
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

199 
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

200 
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

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

202 

40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3"  whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset

203 
fun relevance_fudge_for_prover ctxt name = 
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3"  whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset

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

205 

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

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

207 
let 
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3"  whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset

208 
val thy = ProofContext.theory_of ctxt 
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

209 
val (remote_provers, local_provers) = 
41727
ab3f6d76fb23
available_provers ~> supported_provers (for clarity)
blanchet
parents:
41723
diff
changeset

210 
sort_strings (supported_atps thy) @ 
ab3f6d76fb23
available_provers ~> supported_provers (for clarity)
blanchet
parents:
41723
diff
changeset

211 
sort_strings (SMT_Solver.available_solvers_of ctxt) 
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

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

213 
in 
41727
ab3f6d76fb23
available_provers ~> supported_provers (for clarity)
blanchet
parents:
41723
diff
changeset

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

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

216 
end 
35969  217 

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

218 
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

219 
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

220 
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

221 

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

222 
(** problems, results, ATPs, etc. **) 
35969  223 

224 
type params = 

41208
1b28c43a7074
make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive
blanchet
parents:
41171
diff
changeset

225 
{debug: bool, 
35969  226 
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

227 
overlord: bool, 
41208
1b28c43a7074
make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive
blanchet
parents:
41171
diff
changeset

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

229 
provers: string list, 
41138
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41136
diff
changeset

230 
type_sys: type_system, 
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

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

232 
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

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

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

237 
expect: string} 
35867  238 

41090  239 
datatype prover_fact = 
240 
Untranslated_Fact of (string * locality) * thm  

41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset

241 
ATP_Translated_Fact of 
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset

242 
translated_formula option * ((string * locality) * thm)  
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset

243 
SMT_Weighted_Fact of (string * locality) * (int option * thm) 
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

244 

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

245 
type prover_problem = 
39318  246 
{state: Proof.state, 
38998  247 
goal: thm, 
248 
subgoal: int, 

40065  249 
subgoal_count: int, 
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset

250 
facts: prover_fact list, 
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41336
diff
changeset

251 
smt_head: (string * locality) SMT_Solver.smt_filter_data option} 
35867  252 

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

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

254 
{outcome: failure option, 
35969  255 
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

256 
used_facts: (string * locality) list, 
40062  257 
run_time_in_msecs: int option} 
35867  258 

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

259 
type prover = params > minimize_command > prover_problem > prover_result 
35867  260 

38023  261 
(* configuration attributes *) 
262 

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

264 
Attrib.config_string "sledgehammer_dest_dir" (K "") 
38991  265 
(* Empty string means create files in Isabelle's temporary files directory. *) 
38023  266 

267 
val (problem_prefix, problem_prefix_setup) = 

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

268 
Attrib.config_string "sledgehammer_problem_prefix" (K "prob") 
38023  269 

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

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

271 
Attrib.config_bool "sledgehammer_measure_run_time" (K false) 
28484  272 

38023  273 
fun with_path cleanup after f path = 
274 
Exn.capture f path 

275 
> tap (fn _ => cleanup path) 

276 
> Exn.release 

277 
> tap (after path) 

278 

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

279 
fun proof_banner auto = 
40224  280 
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

281 

41723
bb366da22483
enable SMT weights and triggers, since they lead to slight improvements according to the Judgment Day suite
blanchet
parents:
41432
diff
changeset

282 
val smt_triggers = Unsynchronized.ref true 
bb366da22483
enable SMT weights and triggers, since they lead to slight improvements according to the Judgment Day suite
blanchet
parents:
41432
diff
changeset

283 
val smt_weights = Unsynchronized.ref true 
41256
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset

284 
val smt_weight_min_facts = Unsynchronized.ref 20 
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset

285 

0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset

286 
(* FUDGE *) 
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset

287 
val smt_min_weight = Unsynchronized.ref 0 
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset

288 
val smt_max_weight = Unsynchronized.ref 10 
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset

289 
val smt_max_weight_index = Unsynchronized.ref 200 
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset

290 
val smt_weight_curve = Unsynchronized.ref (fn x : int => x * x) 
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset

291 

0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset

292 
fun smt_fact_weight j num_facts = 
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset

293 
if !smt_weights andalso num_facts >= !smt_weight_min_facts then 
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset

294 
SOME (!smt_max_weight 
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset

295 
 (!smt_max_weight  !smt_min_weight + 1) 
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset

296 
* !smt_weight_curve (Int.max (0, !smt_max_weight_index  j  1)) 
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset

297 
div !smt_weight_curve (!smt_max_weight_index)) 
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset

298 
else 
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset

299 
NONE 
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset

300 

0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset

301 
fun weight_smt_fact thy num_facts ((info, th), j) = 
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset

302 
(info, (smt_fact_weight j num_facts, th > Thm.transfer thy)) 
38023  303 

41091
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41090
diff
changeset

304 
fun untranslated_fact (Untranslated_Fact p) = p 
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41090
diff
changeset

305 
 untranslated_fact (ATP_Translated_Fact (_, p)) = p 
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset

306 
 untranslated_fact (SMT_Weighted_Fact (info, (_, th))) = (info, th) 
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset

307 
fun atp_translated_fact _ (ATP_Translated_Fact p) = p 
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset

308 
 atp_translated_fact ctxt fact = 
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset

309 
translate_atp_fact ctxt (untranslated_fact fact) 
41256
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset

310 
fun smt_weighted_fact _ _ (SMT_Weighted_Fact p, _) = p 
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset

311 
 smt_weighted_fact thy num_facts (fact, j) = 
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset

312 
(untranslated_fact fact, j) > weight_smt_fact thy num_facts 
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset

313 

41313
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41259
diff
changeset

314 
fun overlord_file_location_for_prover prover = 
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41259
diff
changeset

315 
(getenv "ISABELLE_HOME_USER", "prob_" ^ prover) 
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41259
diff
changeset

316 

a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41259
diff
changeset

317 

41256
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset

318 
(* generic TPTPbased ATPs *) 
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

319 

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

320 
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

321 
 int_opt_add _ _ = NONE 
40062  322 

41318
adcb92c0513b
run SPASS and Vampire in SOS mode only if >= 50 facts are passed  otherwise we are probably minimizing and then it's better if the prover is run only once with a full strategy
blanchet
parents:
41315
diff
changeset

323 
val atp_run_twice_threshold = Unsynchronized.ref 50 
41313
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41259
diff
changeset

324 
val atp_first_iter_time_frac = Unsynchronized.ref 0.67 
41168  325 

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

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

328 
val important_message_keep_factor = 0.1 
39492  329 

41159
1e12d6495423
honor "overlord" option for SMT solvers as well and don't pass "ext" to them
blanchet
parents:
41152
diff
changeset

330 
fun run_atp auto name 
41103  331 
({exec, required_execs, arguments, has_incomplete_mode, proof_delims, 
41138
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41136
diff
changeset

332 
known_failures, explicit_forall, use_conjecture_for_hypotheses, ...} 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41136
diff
changeset

333 
: atp_config) 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41136
diff
changeset

334 
({debug, verbose, overlord, type_sys, explicit_apply, isar_proof, 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41136
diff
changeset

335 
isar_shrink_factor, timeout, ...} : params) 
40983  336 
minimize_command ({state, goal, subgoal, facts, ...} : prover_problem) = 
38023  337 
let 
39318  338 
val ctxt = Proof.context_of state 
38998  339 
val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal 
41091
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41090
diff
changeset

340 
val facts = facts > map (atp_translated_fact ctxt) 
41159
1e12d6495423
honor "overlord" option for SMT solvers as well and don't pass "ext" to them
blanchet
parents:
41152
diff
changeset

341 
val (dest_dir, problem_prefix) = 
1e12d6495423
honor "overlord" option for SMT solvers as well and don't pass "ext" to them
blanchet
parents:
41152
diff
changeset

342 
if overlord then overlord_file_location_for_prover name 
1e12d6495423
honor "overlord" option for SMT solvers as well and don't pass "ext" to them
blanchet
parents:
41152
diff
changeset

343 
else (Config.get ctxt dest_dir, 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

344 
val problem_file_name = 
41159
1e12d6495423
honor "overlord" option for SMT solvers as well and don't pass "ext" to them
blanchet
parents:
41152
diff
changeset

345 
Path.basic (problem_prefix ^ (if overlord then "" else serial_string ()) ^ 
1e12d6495423
honor "overlord" option for SMT solvers as well and don't pass "ext" to them
blanchet
parents:
41152
diff
changeset

346 
"_" ^ 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

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

348 
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

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

350 
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

351 
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

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

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

354 
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

355 
val command = Path.explode (getenv (fst exec) ^ "/" ^ snd exec) 
38023  356 
fun split_time s = 
357 
let 

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

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

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

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

362 
val digit = Scan.one Symbol.is_ascii_digit; 

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

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

40627
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
40562
diff
changeset

365 
val as_time = Scan.read Symbol.stopper time o raw_explode 
38023  366 
in (output, as_time t) end; 
41313
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41259
diff
changeset

367 
fun run_on prob_file = 
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

368 
case filter (curry (op =) "" o getenv o fst) (exec :: required_execs) of 
38032  369 
(home_var, _) :: _ => 
38023  370 
error ("The environment variable " ^ quote home_var ^ " is not set.") 
38032  371 
 [] => 
372 
if File.exists command then 

373 
let 

41313
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41259
diff
changeset

374 
val readable_names = debug andalso overlord 
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41259
diff
changeset

375 
val (atp_problem, pool, conjecture_offset, fact_names) = 
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41259
diff
changeset

376 
prepare_atp_problem ctxt readable_names explicit_forall type_sys 
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41259
diff
changeset

377 
explicit_apply hyp_ts concl_t facts 
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41259
diff
changeset

378 
val ss = tptp_strings_for_atp_problem use_conjecture_for_hypotheses 
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41259
diff
changeset

379 
atp_problem 
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41259
diff
changeset

380 
val _ = File.write_list prob_file ss 
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41259
diff
changeset

381 
val conjecture_shape = 
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41259
diff
changeset

382 
conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1 
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41259
diff
changeset

383 
> map single 
39318  384 
fun run complete timeout = 
38032  385 
let 
41313
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41259
diff
changeset

386 
fun weights () = atp_problem_weights atp_problem 
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41259
diff
changeset

387 
val core = 
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41259
diff
changeset

388 
File.shell_path command ^ " " ^ 
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41259
diff
changeset

389 
arguments complete timeout weights ^ " " ^ 
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41259
diff
changeset

390 
File.shell_path prob_file 
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41259
diff
changeset

391 
val command = 
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41259
diff
changeset

392 
(if measure_run_time then 
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41259
diff
changeset

393 
"TIMEFORMAT='%3R'; { time " ^ core ^ " ; }" 
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41259
diff
changeset

394 
else 
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41259
diff
changeset

395 
"exec " ^ core) ^ " 2>&1" 
38032  396 
val ((output, msecs), res_code) = 
397 
bash_output command 

398 
>> (if overlord then 

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

400 
else 

401 
I) 

40062  402 
>> (if measure_run_time then split_time else rpair NONE) 
39452  403 
val (tstplike_proof, outcome) = 
41259
13972ced98d9
more precise error messages in "verbose" (or "debug") mode, following this morning's permission debacle
blanchet
parents:
41256
diff
changeset

404 
extract_tstplike_proof_and_outcome verbose complete res_code 
39452  405 
proof_delims known_failures output 
406 
in (output, msecs, tstplike_proof, outcome) end 

41318
adcb92c0513b
run SPASS and Vampire in SOS mode only if >= 50 facts are passed  otherwise we are probably minimizing and then it's better if the prover is run only once with a full strategy
blanchet
parents:
41315
diff
changeset

407 
val run_twice = 
adcb92c0513b
run SPASS and Vampire in SOS mode only if >= 50 facts are passed  otherwise we are probably minimizing and then it's better if the prover is run only once with a full strategy
blanchet
parents:
41315
diff
changeset

408 
has_incomplete_mode andalso not auto andalso 
adcb92c0513b
run SPASS and Vampire in SOS mode only if >= 50 facts are passed  otherwise we are probably minimizing and then it's better if the prover is run only once with a full strategy
blanchet
parents:
41315
diff
changeset

409 
length facts >= !atp_run_twice_threshold 
38645  410 
val timer = Timer.startRealTimer () 
38032  411 
val result = 
41318
adcb92c0513b
run SPASS and Vampire in SOS mode only if >= 50 facts are passed  otherwise we are probably minimizing and then it's better if the prover is run only once with a full strategy
blanchet
parents:
41315
diff
changeset

412 
run (not run_twice) 
41168  413 
(if run_twice then 
41313
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41259
diff
changeset

414 
seconds (0.001 * !atp_first_iter_time_frac 
41168  415 
* Real.fromInt (Time.toMilliseconds timeout)) 
416 
else 

417 
timeout) 

39318  418 
> run_twice 
38645  419 
? (fn (_, msecs0, _, SOME _) => 
39318  420 
run true (Time. (timeout, Timer.checkRealTimer timer)) 
39452  421 
> (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

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

423 
outcome)) 
38645  424 
 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

425 
in ((pool, conjecture_shape, fact_names), result) end 
38032  426 
else 
427 
error ("Bad executable: " ^ Path.implode command ^ ".") 

38023  428 

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

430 
the proof file too. *) 

41313
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41259
diff
changeset

431 
fun cleanup prob_file = 
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41259
diff
changeset

432 
if dest_dir = "" then try File.rm prob_file else NONE 
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41259
diff
changeset

433 
fun export prob_file (_, (output, _, _, _)) = 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

434 
if dest_dir = "" then 
38023  435 
() 
436 
else 

41313
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41259
diff
changeset

437 
File.write (Path.explode (Path.implode prob_file ^ "_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

438 
val ((pool, conjecture_shape, fact_names), 
39452  439 
(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

440 
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

441 
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

442 
repair_conjecture_shape_and_fact_names output conjecture_shape fact_names 
39492  443 
val important_message = 
40224  444 
if not auto andalso random () <= important_message_keep_factor then 
39492  445 
extract_important_message output 
446 
else 

447 
"" 

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

448 
val (message, used_facts) = 
38023  449 
case outcome of 
450 
NONE => 

451 
proof_text isar_proof 

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

41136
30bedf58b177
implemented new type system encoding "overload_args", which is more lightweight than "const_args" (the unsound default) and hopefully almost as sound
blanchet
parents:
41134
diff
changeset

453 
(proof_banner auto, type_sys, 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

454 
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

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

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

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

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

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

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

461 
"") ^ 
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

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

463 
"\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

464 
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

465 
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

466 
"")) 
40669  467 
 SOME failure => (string_for_failure "ATP" failure, []) 
38023  468 
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

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

470 
run_time_in_msecs = msecs} 
38023  471 
end 
472 

40669  473 
(* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until 
474 
these are sorted out properly in the SMT module, we have to interpret these 

475 
ourselves. *) 

41222  476 
val perl_failures = 
477 
[(127, NoPerl)] 

40684
c7ba327eb58c
more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents:
40669
diff
changeset

478 
val remote_smt_failures = 
c7ba327eb58c
more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents:
40669
diff
changeset

479 
[(22, CantConnect), 
c7ba327eb58c
more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents:
40669
diff
changeset

480 
(2, NoLibwwwPerl)] 
41222  481 
val z3_wrapper_failures = 
482 
[(10, NoRealZ3), 

483 
(11, InternalError), 

484 
(12, InternalError), 

485 
(13, InternalError)] 

40684
c7ba327eb58c
more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents:
40669
diff
changeset

486 
val z3_failures = 
41236  487 
[(101, OutOfResources), 
488 
(103, MalformedInput), 

41222  489 
(110, MalformedInput)] 
40684
c7ba327eb58c
more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents:
40669
diff
changeset

490 
val unix_failures = 
c7ba327eb58c
more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents:
40669
diff
changeset

491 
[(139, Crashed)] 
41222  492 
val smt_failures = 
493 
perl_failures @ remote_smt_failures @ z3_wrapper_failures @ z3_failures @ 

494 
unix_failures 

40555  495 

41209  496 
val internal_error_prefix = "Internal error: " 
497 

41222  498 
fun failure_from_smt_failure (SMT_Failure.Counterexample _) = Unprovable 
499 
 failure_from_smt_failure SMT_Failure.Time_Out = TimedOut 

500 
 failure_from_smt_failure (SMT_Failure.Abnormal_Termination code) = 

501 
(case AList.lookup (op =) smt_failures code of 

40684
c7ba327eb58c
more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents:
40669
diff
changeset

502 
SOME failure => failure 
41259
13972ced98d9
more precise error messages in "verbose" (or "debug") mode, following this morning's permission debacle
blanchet
parents:
41256
diff
changeset

503 
 NONE => UnknownError ("Abnormal termination with exit code " ^ 
13972ced98d9
more precise error messages in "verbose" (or "debug") mode, following this morning's permission debacle
blanchet
parents:
41256
diff
changeset

504 
string_of_int code ^ ".")) 
41222  505 
 failure_from_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources 
506 
 failure_from_smt_failure (SMT_Failure.Other_Failure msg) = 

41209  507 
if String.isPrefix internal_error_prefix msg then InternalError 
41259
13972ced98d9
more precise error messages in "verbose" (or "debug") mode, following this morning's permission debacle
blanchet
parents:
41256
diff
changeset

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

509 

40698  510 
(* FUDGE *) 
41222  511 
val smt_max_iters = Unsynchronized.ref 8 
41169  512 
val smt_iter_fact_frac = Unsynchronized.ref 0.5 
513 
val smt_iter_time_frac = Unsynchronized.ref 0.5 

41168  514 
val smt_iter_min_msecs = Unsynchronized.ref 5000 
41335
66edbd0f7a2e
added "smt_triggers" option to experiment with triggers in Sledgehammer;
blanchet
parents:
41318
diff
changeset

515 
val smt_monomorphize_limit = Unsynchronized.ref 4 
40409
3642dc3b72e8
invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents:
40370
diff
changeset

516 

41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset

517 
fun smt_filter_loop name ({debug, verbose, overlord, timeout, ...} : params) 
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset

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

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

520 
val ctxt = Proof.context_of state 
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset

521 
val repair_context = 
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41336
diff
changeset

522 
select_smt_solver name 
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset

523 
#> Config.put SMT_Config.verbose debug 
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset

524 
#> (if overlord then 
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset

525 
Config.put SMT_Config.debug_files 
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset

526 
(overlord_file_location_for_prover name 
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41336
diff
changeset

527 
> (fn (path, name) => path ^ "/" ^ name)) 
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset

528 
else 
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset

529 
I) 
41335
66edbd0f7a2e
added "smt_triggers" option to experiment with triggers in Sledgehammer;
blanchet
parents:
41318
diff
changeset

530 
#> Config.put SMT_Config.infer_triggers (!smt_triggers) 
66edbd0f7a2e
added "smt_triggers" option to experiment with triggers in Sledgehammer;
blanchet
parents:
41318
diff
changeset

531 
#> Config.put SMT_Config.monomorph_limit (!smt_monomorphize_limit) 
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset

532 
val state = state > Proof.map_context repair_context 
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset

533 

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

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

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

537 
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

538 
val iter_timeout = 
41222  539 
if iter_num < !smt_max_iters then 
41169  540 
Int.min (ms, 
541 
Int.max (!smt_iter_min_msecs, 

542 
Real.ceil (!smt_iter_time_frac * Real.fromInt ms))) 

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

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

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

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

546 
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

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

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

549 
"SMT iteration with " ^ string_of_int num_facts ^ " fact" ^ 
40668
661e334d31f0
use "Thm.transfer" in Sledgehammer to prevent theory merger issues in "SMT_Solver.smt_filter" later on
blanchet
parents:
40666
diff
changeset

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

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

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

553 
() 
41168  554 
val birth = Timer.checkRealTimer timer 
41171  555 
val _ = 
41211
1e2e16bc0077
no need to do a superduper atomization if Metis fails afterwards anyway
blanchet
parents:
41209
diff
changeset

556 
if debug then Output.urgent_message "Invoking SMT solver..." else () 
41209  557 
val (outcome, used_facts) = 
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset

558 
(case (iter_num, smt_head) of 
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41336
diff
changeset

559 
(1, SOME head) => head > apsnd (apsnd repair_context) 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41336
diff
changeset

560 
 _ => SMT_Solver.smt_filter_preprocess state facts i) 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41336
diff
changeset

561 
> SMT_Solver.smt_filter_apply iter_timeout 
41239  562 
> (fn {outcome, used_facts} => (outcome, used_facts)) 
41209  563 
handle exn => if Exn.is_interrupt exn then 
564 
reraise exn 

565 
else 

566 
(internal_error_prefix ^ ML_Compiler.exn_message exn 

567 
> SMT_Failure.Other_Failure > SOME, []) 

41168  568 
val death = Timer.checkRealTimer timer 
40553
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

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

570 
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

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

572 
> Output.urgent_message 
41171  573 
else if debug then 
574 
Output.urgent_message "SMT solver returned." 

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

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

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

577 
val outcome0 = if is_none outcome0 then SOME outcome else outcome0 
41168  578 
val time_so_far = Time.+ (time_so_far, Time. (death, birth)) 
40553
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

579 
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

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

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

582 
 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

583 
 SOME SMT_Failure.Time_Out => iter_timeout <> timeout 
40561
0125cbb5d3c7
renamed SMT failure: Abnormal_Termination is indeed more appropriate than Solver_Crashed
boehmes
parents:
40558
diff
changeset

584 
 SOME (SMT_Failure.Abnormal_Termination code) => 
40553
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

585 
(if verbose then 
40555  586 
"The SMT solver invoked with " ^ string_of_int num_facts ^ 
40692
7fa054c3f810
make "debug" mode of Sledgehammer/SMT more liberal
blanchet
parents:
40684
diff
changeset

587 
" fact" ^ plural_s num_facts ^ " terminated abnormally with \ 
7fa054c3f810
make "debug" mode of Sledgehammer/SMT more liberal
blanchet
parents:
40684
diff
changeset

588 
\exit code " ^ string_of_int code ^ "." 
7fa054c3f810
make "debug" mode of Sledgehammer/SMT more liberal
blanchet
parents:
40684
diff
changeset

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

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

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

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

593 
 SOME SMT_Failure.Out_Of_Memory => true 
41211
1e2e16bc0077
no need to do a superduper atomization if Metis fails afterwards anyway
blanchet
parents:
41209
diff
changeset

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

595 
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

596 
in 
41222  597 
if too_many_facts_perhaps andalso iter_num < !smt_max_iters andalso 
40553
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

598 
num_facts > 0 andalso Time.> (timeout, Time.zeroTime) then 
41169  599 
let 
600 
val n = Real.ceil (!smt_iter_fact_frac * Real.fromInt num_facts) 

601 
in iter timeout (iter_num + 1) outcome0 time_so_far (take n facts) end 

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

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

603 
{outcome = if is_none outcome then NONE else the outcome0, 
41168  604 
used_facts = used_facts, 
605 
run_time_in_msecs = SOME (Time.toMilliseconds time_so_far)} 

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

606 
end 
41168  607 
in iter timeout 1 NONE Time.zeroTime end 
40409
3642dc3b72e8
invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents:
40370
diff
changeset

608 

40666
8db6c2b1591d
try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
blanchet
parents:
40627
diff
changeset

609 
(* taken from "Mirabelle" and generalized *) 
8db6c2b1591d
try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
blanchet
parents:
40627
diff
changeset

610 
fun can_apply timeout tac state i = 
8db6c2b1591d
try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
blanchet
parents:
40627
diff
changeset

611 
let 
8db6c2b1591d
try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
blanchet
parents:
40627
diff
changeset

612 
val {context = ctxt, facts, goal} = Proof.goal state 
8db6c2b1591d
try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
blanchet
parents:
40627
diff
changeset

613 
val full_tac = Method.insert_tac facts i THEN tac ctxt i 
8db6c2b1591d
try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
blanchet
parents:
40627
diff
changeset

614 
in 
8db6c2b1591d
try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
blanchet
parents:
40627
diff
changeset

615 
case try (TimeLimit.timeLimit timeout (Seq.pull o full_tac)) goal of 
8db6c2b1591d
try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
blanchet
parents:
40627
diff
changeset

616 
SOME (SOME _) => true 
8db6c2b1591d
try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
blanchet
parents:
40627
diff
changeset

617 
 _ => false 
8db6c2b1591d
try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
blanchet
parents:
40627
diff
changeset

618 
end 
8db6c2b1591d
try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
blanchet
parents:
40627
diff
changeset

619 

41152
4a7410be4dfc
crank up Metis's timeout for SMT solvers, since users love Metis
blanchet
parents:
41151
diff
changeset

620 
val smt_metis_timeout = seconds 1.0 
40666
8db6c2b1591d
try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
blanchet
parents:
40627
diff
changeset

621 

40693
a4171afcc3c4
set Metis option on correct context, lest it be ignored
blanchet
parents:
40692
diff
changeset

622 
fun can_apply_metis debug state i ths = 
a4171afcc3c4
set Metis option on correct context, lest it be ignored
blanchet
parents:
40692
diff
changeset

623 
can_apply smt_metis_timeout 
a4171afcc3c4
set Metis option on correct context, lest it be ignored
blanchet
parents:
40692
diff
changeset

624 
(Config.put Metis_Tactics.verbose debug 
a4171afcc3c4
set Metis option on correct context, lest it be ignored
blanchet
parents:
40692
diff
changeset

625 
#> (fn ctxt => Metis_Tactics.metis_tac ctxt ths)) state i 
40666
8db6c2b1591d
try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
blanchet
parents:
40627
diff
changeset

626 

41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset

627 
fun run_smt_solver auto name (params as {debug, verbose, ...}) minimize_command 
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset

628 
({state, subgoal, subgoal_count, facts, smt_head, ...} 
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset

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

630 
let 
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset

631 
val ctxt = Proof.context_of state 
41256
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset

632 
val thy = Proof.theory_of state 
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset

633 
val num_facts = length facts 
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset

634 
val facts = facts ~~ (0 upto num_facts  1) 
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset

635 
> map (smt_weighted_fact thy num_facts) 
40181  636 
val {outcome, used_facts, run_time_in_msecs} = 
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset

637 
smt_filter_loop name params state subgoal smt_head facts 
40723
a82badd0e6ef
put facts found by SMT solver in alphabetical order and omit chained facts, as was done already for ATP proofs
blanchet
parents:
40701
diff
changeset

638 
val (chained_lemmas, other_lemmas) = split_used_facts (map fst used_facts) 
41222  639 
val outcome = outcome > Option.map failure_from_smt_failure 
40063
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset

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

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

642 
NONE => 
40666
8db6c2b1591d
try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
blanchet
parents:
40627
diff
changeset

643 
let 
41151
d58157bb1ae7
generate a "using [[smt_solver = ...]]" command if a proof is found by another SMT solver than the current one, to ensure it's also used for reconstruction
blanchet
parents:
41140
diff
changeset

644 
val (method, settings) = 
40693
a4171afcc3c4
set Metis option on correct context, lest it be ignored
blanchet
parents:
40692
diff
changeset

645 
if can_apply_metis debug state subgoal (map snd used_facts) then 
41151
d58157bb1ae7
generate a "using [[smt_solver = ...]]" command if a proof is found by another SMT solver than the current one, to ensure it's also used for reconstruction
blanchet
parents:
41140
diff
changeset

646 
("metis", "") 
40693
a4171afcc3c4
set Metis option on correct context, lest it be ignored
blanchet
parents:
40692
diff
changeset

647 
else 
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41336
diff
changeset

648 
("smt", if name = SMT_Solver.solver_name_of ctxt then "" 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41336
diff
changeset

649 
else "smt_solver = " ^ maybe_quote name) 
40666
8db6c2b1591d
try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
blanchet
parents:
40627
diff
changeset

650 
in 
8db6c2b1591d
try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
blanchet
parents:
40627
diff
changeset

651 
try_command_line (proof_banner auto) 
41151
d58157bb1ae7
generate a "using [[smt_solver = ...]]" command if a proof is found by another SMT solver than the current one, to ensure it's also used for reconstruction
blanchet
parents:
41140
diff
changeset

652 
(apply_on_subgoal settings subgoal subgoal_count ^ 
d58157bb1ae7
generate a "using [[smt_solver = ...]]" command if a proof is found by another SMT solver than the current one, to ensure it's also used for reconstruction
blanchet
parents:
41140
diff
changeset

653 
command_call method (map fst other_lemmas)) ^ 
40723
a82badd0e6ef
put facts found by SMT solver in alphabetical order and omit chained facts, as was done already for ATP proofs
blanchet
parents:
40701
diff
changeset

654 
minimize_line minimize_command 
41168  655 
(map fst (other_lemmas @ chained_lemmas)) ^ 
656 
(if verbose then 

657 
"\nSMT solver real CPU time: " ^ 

658 
string_from_time (Time.fromMilliseconds (the run_time_in_msecs)) ^ 

659 
"." 

660 
else 

661 
"") 

40666
8db6c2b1591d
try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
blanchet
parents:
40627
diff
changeset

662 
end 
40669  663 
 SOME failure => string_for_failure "SMT solver" failure 
40063
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset

664 
in 
40666
8db6c2b1591d
try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
blanchet
parents:
40627
diff
changeset

665 
{outcome = outcome, used_facts = map fst used_facts, 
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

666 
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

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

668 

40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3"  whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset

669 
fun get_prover ctxt auto name = 
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3"  whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset

670 
let val thy = ProofContext.theory_of ctxt in 
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3"  whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset

671 
if is_smt_prover ctxt name then 
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3"  whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset

672 
run_smt_solver auto name 
41727
ab3f6d76fb23
available_provers ~> supported_provers (for clarity)
blanchet
parents:
41723
diff
changeset

673 
else if member (op =) (supported_atps thy) name then 
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3"  whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset

674 
run_atp auto name (get_atp thy name) 
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3"  whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset

675 
else 
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3"  whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset

676 
error ("No such prover: " ^ name ^ ".") 
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3"  whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset

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

678 

38023  679 
val setup = 
680 
dest_dir_setup 

681 
#> problem_prefix_setup 

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

682 
#> measure_run_time_setup 
38023  683 

28582  684 
end; 