author  blanchet 
Fri, 22 Oct 2010 13:48:21 +0200  
changeset 40065  1e4c7185f3f9 
parent 40064  db8413d82c3b 
child 40068  ed2869dd9bfa 
permissions  rwrr 
38021
e024504943d1
rename "ATP_Manager" ML module to "Sledgehammer";
blanchet
parents:
38020
diff
changeset

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

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

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

5 

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

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

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

8 

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

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

10 
sig 
38023  11 
type failure = ATP_Systems.failure 
38988  12 
type locality = Sledgehammer_Filter.locality 
13 
type relevance_override = Sledgehammer_Filter.relevance_override 

39004
f1b465f889b5
translate the axioms to FOF once and for all ATPs
blanchet
parents:
39003
diff
changeset

14 
type fol_formula = Sledgehammer_Translate.fol_formula 
38988  15 
type minimize_command = Sledgehammer_Reconstruct.minimize_command 
39493
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39492
diff
changeset

16 

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

18 
{blocking: bool, 
820b8221ed48
added "blocking" option to Sledgehammer to run in synchronous mode;
blanchet
parents:
38893
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, 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

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

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

25 
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

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

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

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

31 

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

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

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

34 
Prepared of term * ((string * locality) * fol_formula) option 
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

35 

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

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

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

41 
axioms: axiom list, 
39366
f58fbb959826
handle relevance filter corner cases more gracefully;
blanchet
parents:
39364
diff
changeset

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

43 

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

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

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

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

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

49 

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

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

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

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

53 
val default_max_relevant_for_prover : theory > string > int 
38023  54 
val dest_dir : string Config.T 
55 
val problem_prefix : string Config.T 

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

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

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

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

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

60 
val messages : int option > unit 
40063
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset

61 
val get_prover : theory > bool > string > prover 
38044  62 
val run_sledgehammer : 
39318  63 
params > bool > int > relevance_override > (string > minimize_command) 
64 
> Proof.state > bool * Proof.state 

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

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

67 

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

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

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

70 

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

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

74 
open Metis_Translate 
38023  75 
open Sledgehammer_Util 
38988  76 
open Sledgehammer_Filter 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38277
diff
changeset

77 
open Sledgehammer_Translate 
38988  78 
open Sledgehammer_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

79 

38023  80 

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

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

82 

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

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

84 
"Async_Manager". *) 
37585  85 
val das_Tool = "Sledgehammer" 
86 

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

87 
val smtN = "smt" 
40062  88 
val smt_prover_names = [smtN, remote_prefix ^ smtN] 
89 

90 
val smt_default_max_relevant = 300 (* FUDGE *) 

91 
val auto_max_relevant_divisor = 2 (* FUDGE *) 

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

92 

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

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

94 
if member (op =) smt_prover_names name then smt_default_max_relevant 
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset

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

96 

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

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

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

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

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

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

103 
priority ("Available provers: " ^ commas (local_provers @ remote_provers) ^ 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

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

105 
end 
35969  106 

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

107 
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

108 
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

109 
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

110 

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

111 
(** problems, results, ATPs, etc. **) 
35969  112 

113 
type params = 

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

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

115 
debug: bool, 
35969  116 
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

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

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

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

121 
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

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

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

126 
expect: string} 
35867  127 

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

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

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

130 
Prepared of term * ((string * locality) * fol_formula) option 
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

131 

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

132 
type prover_problem = 
39318  133 
{state: Proof.state, 
38998  134 
goal: thm, 
135 
subgoal: int, 

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

137 
axioms: axiom list, 
39366
f58fbb959826
handle relevance filter corner cases more gracefully;
blanchet
parents:
39364
diff
changeset

138 
only: bool} 
35867  139 

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

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

141 
{outcome: failure option, 
35969  142 
message: string, 
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

143 
used_axioms: (string * locality) list, 
40062  144 
run_time_in_msecs: int option} 
35867  145 

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

146 
type prover = params > minimize_command > prover_problem > prover_result 
35867  147 

38023  148 
(* configuration attributes *) 
149 

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

151 
Attrib.config_string "sledgehammer_dest_dir" (K "") 
38991  152 
(* Empty string means create files in Isabelle's temporary files directory. *) 
38023  153 

154 
val (problem_prefix, problem_prefix_setup) = 

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

155 
Attrib.config_string "sledgehammer_problem_prefix" (K "prob") 
38023  156 

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

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

158 
Attrib.config_bool "sledgehammer_measure_run_time" (K false) 
28484  159 

38023  160 
fun with_path cleanup after f path = 
161 
Exn.capture f path 

162 
> tap (fn _ => cleanup path) 

163 
> Exn.release 

164 
> tap (after path) 

165 

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

166 
fun prover_description ctxt ({blocking, verbose, ...} : params) name num_axioms 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

178 

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

179 
fun proof_banner auto = 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

180 
if auto then "Sledgehammer found a proof" else "Try this command" 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

181 

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

182 
(* generic TPTPbased ATPs *) 
38023  183 

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

184 
fun dest_Unprepared (Unprepared p) = p 
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

185 
 dest_Unprepared (Prepared _) = raise Fail "dest_Unprepared" 
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

186 
fun prepared_axiom ctxt (Unprepared p) = prepare_axiom ctxt p 
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

187 
 prepared_axiom _ (Prepared p) = p 
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

188 

40062  189 
fun int_option_add (SOME m) (SOME n) = SOME (m + n) 
190 
 int_option_add _ _ = NONE 

191 

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

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

194 
val important_message_keep_factor = 0.1 
39492  195 

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

196 
fun run_atp auto atp_name 
38645  197 
{exec, required_execs, arguments, has_incomplete_mode, proof_delims, 
38997  198 
known_failures, default_max_relevant, explicit_forall, 
199 
use_conjecture_for_hypotheses} 

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

202 
minimize_command 
40065  203 
({state, goal, subgoal, axioms, only, ...} : prover_problem) = 
38023  204 
let 
39318  205 
val ctxt = Proof.context_of state 
38998  206 
val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal 
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

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

208 
axioms > not only ? take (the_default default_max_relevant max_relevant) 
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

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

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

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

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

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

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

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

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

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

218 
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

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

220 
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

221 
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

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

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

224 
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

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

226 
(* write out problem file and call ATP *) 
38645  227 
fun command_line complete timeout probfile = 
38023  228 
let 
229 
val core = File.shell_path command ^ " " ^ arguments complete timeout ^ 

230 
" " ^ File.shell_path probfile 

231 
in 

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

233 
else "exec " ^ core) ^ " 2>&1" 
38023  234 
end 
235 
fun split_time s = 

236 
let 

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

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

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

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

241 
val digit = Scan.one Symbol.is_ascii_digit; 

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

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

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

38092
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38091
diff
changeset

247 
case filter (curry (op =) "" o getenv o fst) (exec :: required_execs) of 
38032  248 
(home_var, _) :: _ => 
38023  249 
error ("The environment variable " ^ quote home_var ^ " is not set.") 
38032  250 
 [] => 
251 
if File.exists command then 

252 
let 

39318  253 
fun run complete timeout = 
38032  254 
let 
38645  255 
val command = command_line complete timeout probfile 
38032  256 
val ((output, msecs), res_code) = 
257 
bash_output command 

258 
>> (if overlord then 

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

260 
else 

261 
I) 

40062  262 
>> (if measure_run_time then split_time else rpair NONE) 
39452  263 
val (tstplike_proof, outcome) = 
264 
extract_tstplike_proof_and_outcome complete res_code 

265 
proof_delims known_failures output 

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

38032  267 
val readable_names = debug andalso overlord 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

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

269 
prepare_atp_problem ctxt readable_names explicit_forall full_types 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

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

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

273 
val _ = File.write_list probfile ss 
38032  274 
val conjecture_shape = 
275 
conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1 

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

276 
> map single 
39318  277 
val run_twice = has_incomplete_mode andalso not auto 
38645  278 
val timer = Timer.startRealTimer () 
38032  279 
val result = 
39318  280 
run false (if run_twice then 
281 
Time.fromMilliseconds 

38645  282 
(2 * Time.toMilliseconds timeout div 3) 
39318  283 
else 
284 
timeout) 

285 
> run_twice 

38645  286 
? (fn (_, msecs0, _, SOME _) => 
39318  287 
run true (Time. (timeout, Timer.checkRealTimer timer)) 
39452  288 
> (fn (output, msecs, tstplike_proof, outcome) => 
40062  289 
(output, int_option_add msecs0 msecs, 
290 
tstplike_proof, outcome)) 

38645  291 
 result => result) 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38277
diff
changeset

292 
in ((pool, conjecture_shape, axiom_names), result) end 
38032  293 
else 
294 
error ("Bad executable: " ^ Path.implode command ^ ".") 

38023  295 

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

297 
the proof file too. *) 

298 
fun cleanup probfile = 

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

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

301 
if dest_dir = "" then 
38023  302 
() 
303 
else 

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

38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38277
diff
changeset

305 
val ((pool, conjecture_shape, axiom_names), 
39452  306 
(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

307 
with_path cleanup export run_on problem_path_name 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38277
diff
changeset

308 
val (conjecture_shape, axiom_names) = 
39493
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39492
diff
changeset

309 
repair_conjecture_shape_and_axiom_names output conjecture_shape 
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39492
diff
changeset

310 
axiom_names 
39492  311 
val important_message = 
39493
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39492
diff
changeset

312 
if random () <= important_message_keep_factor then 
39492  313 
extract_important_message output 
314 
else 

315 
"" 

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

316 
val (message, used_axioms) = 
38023  317 
case outcome of 
318 
NONE => 

319 
proof_text isar_proof 

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

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

321 
(proof_banner auto, full_types, minimize_command, tstplike_proof, 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

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

323 
>> (fn message => 
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38741
diff
changeset

324 
message ^ (if verbose then 
40062  325 
"\nATP real CPU time: " ^ 
326 
string_of_int (the msecs) ^ " ms." 

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

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

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

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

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

331 
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

332 
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

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

334 
 SOME failure => (string_for_failure failure, []) 
38023  335 
in 
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

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

337 
run_time_in_msecs = msecs} 
38023  338 
end 
339 

40064
db8413d82c3b
got rid of duplicate functionality ("run_smt_solver_somehow");
blanchet
parents:
40063
diff
changeset

340 
(* FIXME: dummy *) 
db8413d82c3b
got rid of duplicate functionality ("run_smt_solver_somehow");
blanchet
parents:
40063
diff
changeset

341 
fun saschas_run_smt_solver remote timeout state axioms i = 
db8413d82c3b
got rid of duplicate functionality ("run_smt_solver_somehow");
blanchet
parents:
40063
diff
changeset

342 
(OS.Process.sleep (Time.fromMilliseconds 1500); 
db8413d82c3b
got rid of duplicate functionality ("run_smt_solver_somehow");
blanchet
parents:
40063
diff
changeset

343 
{outcome = NONE, used_axioms = axioms > take 5 > map fst, 
db8413d82c3b
got rid of duplicate functionality ("run_smt_solver_somehow");
blanchet
parents:
40063
diff
changeset

344 
run_time_in_msecs = NONE}) 
40063
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset

345 

40064
db8413d82c3b
got rid of duplicate functionality ("run_smt_solver_somehow");
blanchet
parents:
40063
diff
changeset

346 
fun run_smt_solver remote ({timeout, ...} : params) minimize_command 
40065  347 
({state, subgoal, subgoal_count, axioms, ...} 
348 
: 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

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

350 
val {outcome, used_axioms, run_time_in_msecs} = 
40064
db8413d82c3b
got rid of duplicate functionality ("run_smt_solver_somehow");
blanchet
parents:
40063
diff
changeset

351 
saschas_run_smt_solver remote timeout state 
db8413d82c3b
got rid of duplicate functionality ("run_smt_solver_somehow");
blanchet
parents:
40063
diff
changeset

352 
(map_filter (try dest_Unprepared) axioms) subgoal 
40063
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset

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

354 
if outcome = NONE then 
40064
db8413d82c3b
got rid of duplicate functionality ("run_smt_solver_somehow");
blanchet
parents:
40063
diff
changeset

355 
try_command_line (proof_banner false) 
40065  356 
(apply_on_subgoal subgoal subgoal_count ^ 
40064
db8413d82c3b
got rid of duplicate functionality ("run_smt_solver_somehow");
blanchet
parents:
40063
diff
changeset

357 
command_call smtN (map fst used_axioms)) ^ 
db8413d82c3b
got rid of duplicate functionality ("run_smt_solver_somehow");
blanchet
parents:
40063
diff
changeset

358 
minimize_line minimize_command (map fst used_axioms) 
40063
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset

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

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

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

362 
{outcome = outcome, used_axioms = used_axioms, 
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset

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

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

365 

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

366 
fun get_prover thy auto name = 
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset

367 
if member (op =) smt_prover_names name then 
40064
db8413d82c3b
got rid of duplicate functionality ("run_smt_solver_somehow");
blanchet
parents:
40063
diff
changeset

368 
run_smt_solver (String.isPrefix remote_prefix) 
40063
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset

369 
else 
40064
db8413d82c3b
got rid of duplicate functionality ("run_smt_solver_somehow");
blanchet
parents:
40063
diff
changeset

370 
run_atp auto name (get_atp thy name) 
40063
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset

371 

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

372 
fun run_prover (params as {blocking, debug, max_relevant, timeout, expect, ...}) 
40065  373 
auto minimize_command 
374 
(problem as {state, goal, subgoal, subgoal_count, axioms, ...}) 

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

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

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

377 
val thy = Proof.theory_of state 
39318  378 
val ctxt = Proof.context_of state 
37584  379 
val birth_time = Time.now () 
380 
val death_time = Time.+ (birth_time, timeout) 

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

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

382 
the_default (default_max_relevant_for_prover thy name) max_relevant 
39110
a74bd9bfa880
show the number of facts for each prover in "verbose" mode
blanchet
parents:
39108
diff
changeset

383 
val num_axioms = Int.min (length axioms, max_relevant) 
40065  384 
val desc = 
385 
prover_description ctxt params name num_axioms subgoal subgoal_count goal 

39318  386 
fun go () = 
38982
820b8221ed48
added "blocking" option to Sledgehammer to run in synchronous mode;
blanchet
parents:
38893
diff
changeset

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

388 
fun really_go () = 
40063
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset

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

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

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

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

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

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

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

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

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

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

399 
ML_Compiler.exn_message exn ^ "\n")) 
39318  400 
val _ = 
401 
if expect = "" orelse outcome_code = expect then 

402 
() 

403 
else if blocking then 

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

405 
else 

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

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

408 
in 

409 
if auto then 

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

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

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

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

414 
end 
39318  415 
else if blocking then 
416 
let val (success, message) = TimeLimit.timeLimit timeout go () in 

39370
f8292d3020db
use same hack as in "Async_Manager" to work around Proof General bug
blanchet
parents:
39366
diff
changeset

417 
List.app priority 
f8292d3020db
use same hack as in "Async_Manager" to work around Proof General bug
blanchet
parents:
39366
diff
changeset

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

419 
(success, state) 
39318  420 
end 
421 
else 

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

423 
(false, state)) 

37584  424 
end 
28582  425 

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

426 
fun run_sledgehammer (params as {blocking, provers, full_types, 
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

427 
relevance_thresholds, max_relevant, timeout, 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

428 
...}) 
39366
f58fbb959826
handle relevance filter corner cases more gracefully;
blanchet
parents:
39364
diff
changeset

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

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

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

432 
error "No prover is set." 
39318  433 
else case subgoal_count state of 
434 
0 => (priority "No subgoal!"; (false, state)) 

435 
 n => 

436 
let 

39364  437 
val _ = Proof.assert_backward state 
39318  438 
val thy = Proof.theory_of state 
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

439 
val {context = ctxt, facts = chained_ths, goal} = Proof.goal state 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

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

441 
val _ = () > not blocking ? kill_provers 
39318  442 
val _ = if auto then () else priority "Sledgehammering..." 
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

443 
val (smts, atps) = 
40062  444 
provers > List.partition (member (op =) smt_prover_names) 
40065  445 
fun run_provers full_types maybe_prepare provers (res as (success, state)) = 
446 
if success orelse null provers then 

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

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

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

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

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

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

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

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

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

456 
> auto ? (fn n => n div auto_max_relevant_divisor) 
40065  457 
val axioms = 
458 
relevant_facts ctxt full_types relevance_thresholds 

459 
max_max_relevant relevance_override chained_ths 

460 
hyp_ts concl_t 

461 
> map maybe_prepare 

40062  462 
val problem = 
40065  463 
{state = state, goal = goal, subgoal = i, subgoal_count = n, 
464 
axioms = axioms, only = only} 

465 
val run_prover = run_prover params auto minimize_command 

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

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

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

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

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

471 
else 
40065  472 
provers > (if blocking then Par_List.map else map) 
473 
(run_prover problem) 

474 
> exists fst > rpair state 

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

475 
end 
40065  476 
val run_atps = run_provers full_types (Prepared o prepare_axiom ctxt) atps 
477 
val run_smts = run_provers true Unprepared smts 

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

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

480 
in 
40065  481 
(false, state) 
482 
> (if blocking then run_atps #> not auto ? run_smts 

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

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

484 
end 
38044  485 

38023  486 
val setup = 
487 
dest_dir_setup 

488 
#> problem_prefix_setup 

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

489 
#> measure_run_time_setup 
38023  490 

28582  491 
end; 