author  blanchet 
Fri, 22 Oct 2010 09:50:18 +0200  
changeset 40061  71cc5aac8b76 
parent 40060  5ef6747aa619 
child 40062  cfaebaa8588f 
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, 

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

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

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

42 

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

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

44 
{outcome: failure option, 
35969  45 
message: string, 
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, 
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

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

48 

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

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

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

51 
val smtN : string 
38023  52 
val dest_dir : string Config.T 
53 
val problem_prefix : string Config.T 

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

54 
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

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

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

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

58 
val messages : int option > unit 
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

59 
val run_atp : theory > string > prover 
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

60 
val is_smt_solver_installed : unit > bool 
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

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

62 
bool > params > minimize_command > prover_problem 
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

63 
> string * (string * locality) list 
38044  64 
val run_sledgehammer : 
39318  65 
params > bool > int > relevance_override > (string > minimize_command) 
66 
> Proof.state > bool * Proof.state 

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

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

69 

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

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

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

72 

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

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

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

79 
open Sledgehammer_Translate 
38988  80 
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

81 

38023  82 

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

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

84 

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

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

86 
"Async_Manager". *) 
37585  87 
val das_Tool = "Sledgehammer" 
88 

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

89 
val smtN = "smt" 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

90 
val smt_names = [smtN, remote_prefix ^ smtN] 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

91 

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

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

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

94 
val (remote_provers, local_provers) = 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

95 
sort_strings (available_atps thy) @ smt_names 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

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

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

98 
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

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

100 
end 
35969  101 

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

102 
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

103 
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

104 
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

105 

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

106 
(** problems, results, ATPs, etc. **) 
35969  107 

108 
type params = 

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

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

110 
debug: bool, 
35969  111 
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

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

113 
provers: string list, 
35969  114 
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

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

116 
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

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

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

121 
expect: string} 
35867  122 

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

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

124 
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

125 
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

126 

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

127 
type prover_problem = 
39318  128 
{state: Proof.state, 
38998  129 
goal: thm, 
130 
subgoal: int, 

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

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

132 
only: bool} 
35867  133 

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

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

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

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

138 
run_time_in_msecs: int} 
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 = params > minimize_command > prover_problem > prover_result 
35867  141 

38023  142 
(* configuration attributes *) 
143 

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

145 
Attrib.config_string "sledgehammer_dest_dir" (K "") 
38991  146 
(* Empty string means create files in Isabelle's temporary files directory. *) 
38023  147 

148 
val (problem_prefix, problem_prefix_setup) = 

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

149 
Attrib.config_string "sledgehammer_problem_prefix" (K "prob") 
38023  150 

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

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

152 
Attrib.config_bool "sledgehammer_measure_run_time" (K false) 
28484  153 

38023  154 
fun with_path cleanup after f path = 
155 
Exn.capture f path 

156 
> tap (fn _ => cleanup path) 

157 
> Exn.release 

158 
> tap (after path) 

159 

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

160 
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

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

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

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

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

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

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

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

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

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

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

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

172 

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

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

174 
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

175 

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

176 
(* generic TPTPbased ATPs *) 
38023  177 

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

178 
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

179 
 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

180 
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

181 
 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

182 

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

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

185 
val important_message_keep_factor = 0.1 
39492  186 

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

187 
fun atp_fun auto atp_name 
38645  188 
{exec, required_execs, arguments, has_incomplete_mode, proof_delims, 
38997  189 
known_failures, default_max_relevant, explicit_forall, 
190 
use_conjecture_for_hypotheses} 

38455  191 
({debug, verbose, overlord, full_types, explicit_apply, 
38998  192 
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

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

194 
({state, goal, subgoal, axioms, only} : prover_problem) = 
38023  195 
let 
39318  196 
val ctxt = Proof.context_of state 
38998  197 
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

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

199 
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

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

201 
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

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

203 
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

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

205 
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

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

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

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

209 
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

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

211 
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

212 
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

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

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

215 
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

216 
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

217 
(* write out problem file and call ATP *) 
38645  218 
fun command_line complete timeout probfile = 
38023  219 
let 
220 
val core = File.shell_path command ^ " " ^ arguments complete timeout ^ 

221 
" " ^ File.shell_path probfile 

222 
in 

39010  223 
(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

224 
else "exec " ^ core) ^ " 2>&1" 
38023  225 
end 
226 
fun split_time s = 

227 
let 

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

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

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

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

232 
val digit = Scan.one Symbol.is_ascii_digit; 

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

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

235 
val as_time = the_default 0 o Scan.read Symbol.stopper time o explode; 

236 
in (output, as_time t) end; 

237 
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

238 
case filter (curry (op =) "" o getenv o fst) (exec :: required_execs) of 
38032  239 
(home_var, _) :: _ => 
38023  240 
error ("The environment variable " ^ quote home_var ^ " is not set.") 
38032  241 
 [] => 
242 
if File.exists command then 

243 
let 

39318  244 
fun run complete timeout = 
38032  245 
let 
38645  246 
val command = command_line complete timeout probfile 
38032  247 
val ((output, msecs), res_code) = 
248 
bash_output command 

249 
>> (if overlord then 

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

251 
else 

252 
I) 

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

253 
>> (if measure_run_time then split_time else rpair 0) 
39452  254 
val (tstplike_proof, outcome) = 
255 
extract_tstplike_proof_and_outcome complete res_code 

256 
proof_delims known_failures output 

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

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

259 
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

260 
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

261 
explicit_apply hyp_ts concl_t axioms 
39452  262 
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

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

264 
val _ = File.write_list probfile ss 
38032  265 
val conjecture_shape = 
266 
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

267 
> map single 
39318  268 
val run_twice = has_incomplete_mode andalso not auto 
38645  269 
val timer = Timer.startRealTimer () 
38032  270 
val result = 
39318  271 
run false (if run_twice then 
272 
Time.fromMilliseconds 

38645  273 
(2 * Time.toMilliseconds timeout div 3) 
39318  274 
else 
275 
timeout) 

276 
> run_twice 

38645  277 
? (fn (_, msecs0, _, SOME _) => 
39318  278 
run true (Time. (timeout, Timer.checkRealTimer timer)) 
39452  279 
> (fn (output, msecs, tstplike_proof, outcome) => 
280 
(output, msecs0 + msecs, tstplike_proof, outcome)) 

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

282 
in ((pool, conjecture_shape, axiom_names), result) end 
38032  283 
else 
284 
error ("Bad executable: " ^ Path.implode command ^ ".") 

38023  285 

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

287 
the proof file too. *) 

288 
fun cleanup probfile = 

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

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

291 
if dest_dir = "" then 
38023  292 
() 
293 
else 

294 
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

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

297 
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

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

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

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

302 
if random () <= important_message_keep_factor then 
39492  303 
extract_important_message output 
304 
else 

305 
"" 

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

306 
val (message, used_axioms) = 
38023  307 
case outcome of 
308 
NONE => 

309 
proof_text isar_proof 

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

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

312 
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

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

314 
message ^ (if verbose then 
39371  315 
"\nATP real CPU time: " ^ string_of_int msecs ^ 
316 
" ms." 

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

317 
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

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

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

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

321 
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

322 
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

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

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

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

327 
run_time_in_msecs = msecs} 
38023  328 
end 
329 

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

330 
fun run_atp thy name = atp_fun false name (get_atp thy name) 
38023  331 

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

332 
fun run_atp_somehow (params as {blocking, debug, max_relevant, timeout, 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

333 
expect, ...}) 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

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

335 
(prover_problem as {state, goal, axioms, ...}) 
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

336 
(prover as {default_max_relevant, ...}, atp_name) = 
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

337 
let 
39318  338 
val ctxt = Proof.context_of state 
37584  339 
val birth_time = Time.now () 
340 
val death_time = Time.+ (birth_time, timeout) 

39110
a74bd9bfa880
show the number of facts for each prover in "verbose" mode
blanchet
parents:
39108
diff
changeset

341 
val max_relevant = the_default default_max_relevant max_relevant 
a74bd9bfa880
show the number of facts for each prover in "verbose" mode
blanchet
parents:
39108
diff
changeset

342 
val num_axioms = Int.min (length axioms, max_relevant) 
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

343 
val desc = prover_description ctxt params atp_name num_axioms i n goal 
39318  344 
fun go () = 
38982
820b8221ed48
added "blocking" option to Sledgehammer to run in synchronous mode;
blanchet
parents:
38893
diff
changeset

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

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

347 
atp_fun auto atp_name prover params (minimize_command atp_name) 
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

348 
prover_problem 
38985
162bbbea4e4d
added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents:
38982
diff
changeset

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

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

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

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

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

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

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

356 
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

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

358 
ML_Compiler.exn_message exn ^ "\n")) 
39318  359 
val _ = 
360 
if expect = "" orelse outcome_code = expect then 

361 
() 

362 
else if blocking then 

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

364 
else 

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

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

367 
in 

368 
if auto then 

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

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

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

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

373 
end 
39318  374 
else if blocking then 
375 
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

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

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

378 
(success, state) 
39318  379 
end 
380 
else 

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

382 
(false, state)) 

37584  383 
end 
28582  384 

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

385 
(* FIXME: dummy *) 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

386 
fun is_smt_solver_installed () = true 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

387 

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

388 
(* FIXME: dummy *) 
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

389 
fun raw_run_smt_solver remote timeout state axioms i = 
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

390 
("", axioms > take 5 > map fst) 
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

391 

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

392 
fun run_smt_solver remote ({timeout, ...} : params) minimize_command 
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

393 
({state, subgoal, axioms, ...} : prover_problem) = 
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

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

395 
(map_filter (try dest_Unprepared) axioms) subgoal 
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

396 

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

397 
fun run_smt_solver_somehow state (params as {timeout, ...}) i n goal axioms 
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

398 
(remote, name) = 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

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

400 
val ctxt = Proof.context_of state 
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

401 
val desc = prover_description ctxt params name (length axioms) i n goal 
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

402 
val (failure, used_axioms) = 
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

403 
raw_run_smt_solver remote timeout state axioms i 
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

404 
val success = (failure = "") 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

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

406 
das_Tool ^ ": " ^ desc ^ "\n" ^ 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

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

408 
sendback_line (proof_banner false) 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

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

410 
command_call "smt" (map fst used_axioms)) 
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

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

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

413 
in priority message; success end 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

414 

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

415 
val smt_default_max_relevant = 300 (* FUDGE *) 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

416 
val auto_max_relevant_divisor = 2 (* FUDGE *) 
39318  417 

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

418 
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

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

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

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

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

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

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

427 
 n => 

428 
let 

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

431 
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

432 
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

433 
val _ = () > not blocking ? kill_provers 
39318  434 
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

435 
val (smts, atps) = 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

436 
provers > List.partition (member (op =) smt_names) 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

437 
>> (take 1 #> map (`(String.isPrefix remote_prefix))) 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

438 
> map (`(get_atp thy)) 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

439 
fun run_atps (res as (success, state)) = 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

440 
if success orelse null atps then 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

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

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

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

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

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

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

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

448 
0 > fold (Integer.max o #default_max_relevant o fst) atps 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

449 
> auto ? (fn n => n div auto_max_relevant_divisor) 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

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

451 
relevant_facts ctxt full_types relevance_thresholds 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

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

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

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

455 
{state = state, goal = goal, subgoal = i, 
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

456 
axioms = axioms > map (Prepared o prepare_axiom ctxt), 
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

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

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

459 
run_atp_somehow params auto i n minimize_command prover_problem 
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

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

461 
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

462 
fold (fn prover => fn (true, state) => (true, state) 
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

463 
 (false, _) => run_atp_somehow prover) 
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

464 
atps (false, state) 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

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

466 
atps > (if blocking then Par_List.map else map) run_atp_somehow 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

467 
> exists fst > rpair state 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

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

469 
fun run_smt_solvers (res as (success, state)) = 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

470 
if success orelse null smts then 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

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

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

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

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

475 
max_relevant > the_default smt_default_max_relevant 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

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

477 
relevant_facts ctxt full_types relevance_thresholds 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

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

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

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

481 
smts > map (run_smt_solver_somehow state params i n goal axioms) 
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

482 
> exists I > rpair state 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

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

484 
fun run_atps_and_smt_solvers () = 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

485 
[run_atps, run_smt_solvers] 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

486 
> Par_List.map (fn f => f (false, state) > K ()) 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

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

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

489 
(false, state) > run_atps > not auto ? run_smt_solvers 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

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

491 
Future.fork (tap run_atps_and_smt_solvers) > K (false, state) 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

492 
end 
38044  493 

38023  494 
val setup = 
495 
dest_dir_setup 

496 
#> problem_prefix_setup 

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

497 
#> measure_run_time_setup 
38023  498 

28582  499 
end; 