author  blanchet 
Sat, 11 Sep 2010 10:21:52 +0200  
changeset 39318  ad9a1f9b0558 
parent 39263  e2a3c435334b 
child 39327  61547eda78b4 
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 
35969  16 
type params = 
38982
820b8221ed48
added "blocking" option to Sledgehammer to run in synchronous mode;
blanchet
parents:
38893
diff
changeset

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

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

20 
overlord: bool, 
35969  21 
atps: string list, 
22 
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

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

24 
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

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

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

29 
expect: string} 
35867  30 
type problem = 
39318  31 
{state: Proof.state, 
38998  32 
goal: thm, 
33 
subgoal: int, 

39005  34 
axioms: (term * ((string * locality) * fol_formula) option) list} 
35867  35 
type prover_result = 
36370
a4f601daa175
centralized ATPspecific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset

36 
{outcome: failure option, 
35969  37 
message: string, 
37926
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37627
diff
changeset

38 
pool: string Symtab.table, 
38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38748
diff
changeset

39 
used_thm_names: (string * locality) list, 
35969  40 
atp_run_time_in_msecs: int, 
36369
d2cd0d04b8e6
handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents:
36289
diff
changeset

41 
output: string, 
35969  42 
proof: string, 
38818
61cf050f8b2e
improve SPASS hack, when a clause comes from several facts
blanchet
parents:
38752
diff
changeset

43 
axiom_names: (string * locality) list vector, 
38083
c4b57f68ddb3
remove the "extra_clauses" business introduced in 19a5f1c8a844;
blanchet
parents:
38061
diff
changeset

44 
conjecture_shape: int list list} 
38100
e458a0dd3dc1
use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
blanchet
parents:
38098
diff
changeset

45 
type prover = params > minimize_command > problem > prover_result 
35867  46 

38023  47 
val dest_dir : string Config.T 
48 
val problem_prefix : string Config.T 

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

49 
val measure_run_time : bool Config.T 
35969  50 
val kill_atps: unit > unit 
51 
val running_atps: unit > unit 

29112
f2b45eea6dac
added 'atp_messages' command, which displays recent messages synchronously;
wenzelm
parents:
28835
diff
changeset

52 
val messages: int option > unit 
38023  53 
val get_prover_fun : theory > string > prover 
38044  54 
val run_sledgehammer : 
39318  55 
params > bool > int > relevance_override > (string > minimize_command) 
56 
> Proof.state > bool * Proof.state 

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

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

59 

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

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

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

62 

38028  63 
open ATP_Problem 
64 
open ATP_Systems 

37578
9367cb36b1c4
renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer
blanchet
parents:
37577
diff
changeset

65 
open Metis_Clauses 
38023  66 
open Sledgehammer_Util 
38988  67 
open Sledgehammer_Filter 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38277
diff
changeset

68 
open Sledgehammer_Translate 
38988  69 
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

70 

38023  71 

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

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

73 

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

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

75 
"Async_Manager". *) 
37585  76 
val das_Tool = "Sledgehammer" 
77 

78 
fun kill_atps () = Async_Manager.kill_threads das_Tool "ATPs" 

79 
fun running_atps () = Async_Manager.running_threads das_Tool "ATPs" 

80 
val messages = Async_Manager.thread_messages das_Tool "ATP" 

35969  81 

36281
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36235
diff
changeset

82 
(** problems, results, provers, etc. **) 
35969  83 

84 
type params = 

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

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

86 
debug: bool, 
35969  87 
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

88 
overlord: bool, 
35969  89 
atps: string list, 
90 
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

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

92 
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

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

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

97 
expect: string} 
35867  98 

99 
type problem = 

39318  100 
{state: Proof.state, 
38998  101 
goal: thm, 
102 
subgoal: int, 

39005  103 
axioms: (term * ((string * locality) * fol_formula) option) list} 
35867  104 

105 
type prover_result = 

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

106 
{outcome: failure option, 
35969  107 
message: string, 
37926
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37627
diff
changeset

108 
pool: string Symtab.table, 
38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38748
diff
changeset

109 
used_thm_names: (string * locality) list, 
35969  110 
atp_run_time_in_msecs: int, 
36369
d2cd0d04b8e6
handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents:
36289
diff
changeset

111 
output: string, 
35969  112 
proof: string, 
38818
61cf050f8b2e
improve SPASS hack, when a clause comes from several facts
blanchet
parents:
38752
diff
changeset

113 
axiom_names: (string * locality) list vector, 
38083
c4b57f68ddb3
remove the "extra_clauses" business introduced in 19a5f1c8a844;
blanchet
parents:
38061
diff
changeset

114 
conjecture_shape: int list list} 
35867  115 

38100
e458a0dd3dc1
use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
blanchet
parents:
38098
diff
changeset

116 
type prover = params > minimize_command > problem > prover_result 
35867  117 

38023  118 
(* configuration attributes *) 
119 

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

121 
Attrib.config_string "sledgehammer_dest_dir" (K "") 
38991  122 
(* Empty string means create files in Isabelle's temporary files directory. *) 
38023  123 

124 
val (problem_prefix, problem_prefix_setup) = 

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

125 
Attrib.config_string "sledgehammer_problem_prefix" (K "prob") 
38023  126 

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

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

128 
Attrib.config_bool "sledgehammer_measure_run_time" (K false) 
28484  129 

38023  130 
fun with_path cleanup after f path = 
131 
Exn.capture f path 

132 
> tap (fn _ => cleanup path) 

133 
> Exn.release 

134 
> tap (after path) 

135 

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

136 
fun extract_delimited (begin_delim, end_delim) output = 
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

137 
output > first_field begin_delim > the > snd 
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

138 
> first_field end_delim > the > fst 
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

139 
> first_field "\n" > the > snd 
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

140 
handle Option.Option => "" 
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

141 

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

142 
val tstp_important_message_delims = 
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

143 
("% SZS start RequiredInformation", "% SZS end RequiredInformation") 
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

144 

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

145 
fun extract_important_message output = 
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

146 
case extract_delimited tstp_important_message_delims output of 
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

147 
"" => "" 
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

148 
 s => s > space_explode "\n" > filter_out (curry (op =) "") 
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

149 
> map (perhaps (try (unprefix "%"))) 
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

150 
> map (perhaps (try (unprefix " "))) 
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

151 
> space_implode "\n " > quote 
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

152 

38023  153 
(* Splits by the first possible of a list of delimiters. *) 
154 
fun extract_proof delims output = 

155 
case pairself (find_first (fn s => String.isSubstring s output)) 

156 
(ListPair.unzip delims) of 

157 
(SOME begin_delim, SOME end_delim) => 

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

158 
extract_delimited (begin_delim, end_delim) output 
38023  159 
 _ => "" 
28484  160 

38023  161 
fun extract_proof_and_outcome complete res_code proof_delims known_failures 
162 
output = 

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

163 
case known_failure_in_output output known_failures of 
685d1f0f75b3
handle Perl and "libwwwperl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents:
38044
diff
changeset

164 
NONE => (case extract_proof proof_delims output of 
39262
bdfcf2434601
better error reporting when the Sledgehammer minimizer is interrupted
blanchet
parents:
39223
diff
changeset

165 
"" => ("", SOME (if res_code = 0 andalso output = "" then 
bdfcf2434601
better error reporting when the Sledgehammer minimizer is interrupted
blanchet
parents:
39223
diff
changeset

166 
Interrupted 
bdfcf2434601
better error reporting when the Sledgehammer minimizer is interrupted
blanchet
parents:
39223
diff
changeset

167 
else 
39263
e2a3c435334b
more precise error messages when Vampire is interrupted or SPASS runs into an internal bug
blanchet
parents:
39262
diff
changeset

168 
UnknownError)) 
38023  169 
 proof => if res_code = 0 then (proof, NONE) 
170 
else ("", SOME UnknownError)) 

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

171 
 SOME failure => 
38023  172 
("", SOME (if failure = IncompleteUnprovable andalso complete then 
173 
Unprovable 

174 
else 

175 
failure)) 

28582  176 

38023  177 
fun extract_clause_sequence output = 
178 
let 

179 
val tokens_of = String.tokens (not o Char.isAlphaNum) 

180 
fun extract_num ("clause" :: (ss as _ :: _)) = 

181 
Int.fromString (List.last ss) 

182 
 extract_num _ = NONE 

183 
in output > split_lines > map_filter (extract_num o tokens_of) end 

184 

185 
val set_ClauseFormulaRelationN = "set_ClauseFormulaRelation" 

186 

187 
val parse_clause_formula_pair = 

38515  188 
$$ "("  scan_integer  $$ "," 
189 
 (Symbol.scan_id ::: Scan.repeat ($$ ","  Symbol.scan_id))  $$ ")" 

38023  190 
 Scan.option ($$ ",") 
191 
val parse_clause_formula_relation = 

192 
Scan.this_string set_ClauseFormulaRelationN  $$ "(" 

193 
 Scan.repeat parse_clause_formula_pair 

194 
val extract_clause_formula_relation = 

38738
0ce517c1970f
make sure that "undo_ascii_of" is the inverse of "ascii_of", also for nonprintable characters  and avoid those in ``style facts
blanchet
parents:
38698
diff
changeset

195 
Substring.full #> Substring.position set_ClauseFormulaRelationN 
39007
aae6a0d33c66
speed up SPASS hack + output time information in "blocking" mode
blanchet
parents:
39005
diff
changeset

196 
#> snd #> Substring.position "." #> fst #> Substring.string 
39008  197 
#> explode #> filter_out Symbol.is_blank #> parse_clause_formula_relation 
39007
aae6a0d33c66
speed up SPASS hack + output time information in "blocking" mode
blanchet
parents:
39005
diff
changeset

198 
#> fst 
38023  199 

38988  200 
(* TODO: move to "Sledgehammer_Reconstruct" *) 
38023  201 
fun repair_conjecture_shape_and_theorem_names output conjecture_shape 
38698
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38682
diff
changeset

202 
axiom_names = 
38023  203 
if String.isSubstring set_ClauseFormulaRelationN output then 
204 
(* This is a hack required for keeping track of axioms after they have been 

38698
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38682
diff
changeset

205 
clausified by SPASS's Flotter tool. The "ATP/scripts/spass" script is 
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38682
diff
changeset

206 
also part of this hack. *) 
38023  207 
let 
38040
174568533593
fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
blanchet
parents:
38039
diff
changeset

208 
val j0 = hd (hd conjecture_shape) 
38023  209 
val seq = extract_clause_sequence output 
210 
val name_map = extract_clause_formula_relation output 

211 
fun renumber_conjecture j = 

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

212 
conjecture_prefix ^ string_of_int (j  j0) 
38515  213 
> AList.find (fn (s, ss) => member (op =) ss s) name_map 
38040
174568533593
fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
blanchet
parents:
38039
diff
changeset

214 
> map (fn s => find_index (curry (op =) s) seq + 1) 
38818
61cf050f8b2e
improve SPASS hack, when a clause comes from several facts
blanchet
parents:
38752
diff
changeset

215 
fun names_for_number j = 
61cf050f8b2e
improve SPASS hack, when a clause comes from several facts
blanchet
parents:
38752
diff
changeset

216 
j > AList.lookup (op =) name_map > these 
61cf050f8b2e
improve SPASS hack, when a clause comes from several facts
blanchet
parents:
38752
diff
changeset

217 
> map_filter (try (unprefix axiom_prefix)) > map unascii_of 
61cf050f8b2e
improve SPASS hack, when a clause comes from several facts
blanchet
parents:
38752
diff
changeset

218 
> map (fn name => 
61cf050f8b2e
improve SPASS hack, when a clause comes from several facts
blanchet
parents:
38752
diff
changeset

219 
(name, name > find_first_in_list_vector axiom_names 
61cf050f8b2e
improve SPASS hack, when a clause comes from several facts
blanchet
parents:
38752
diff
changeset

220 
> the) 
61cf050f8b2e
improve SPASS hack, when a clause comes from several facts
blanchet
parents:
38752
diff
changeset

221 
handle Option.Option => 
61cf050f8b2e
improve SPASS hack, when a clause comes from several facts
blanchet
parents:
38752
diff
changeset

222 
error ("No such fact: " ^ quote name ^ ".")) 
38023  223 
in 
38040
174568533593
fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
blanchet
parents:
38039
diff
changeset

224 
(conjecture_shape > map (maps renumber_conjecture), 
38818
61cf050f8b2e
improve SPASS hack, when a clause comes from several facts
blanchet
parents:
38752
diff
changeset

225 
seq > map names_for_number > Vector.fromList) 
38023  226 
end 
227 
else 

38698
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38682
diff
changeset

228 
(conjecture_shape, axiom_names) 
38023  229 

230 

231 
(* generic TPTPbased provers *) 

232 

39318  233 
fun prover_fun auto atp_name 
38645  234 
{exec, required_execs, arguments, has_incomplete_mode, proof_delims, 
38997  235 
known_failures, default_max_relevant, explicit_forall, 
236 
use_conjecture_for_hypotheses} 

38455  237 
({debug, verbose, overlord, full_types, explicit_apply, 
38998  238 
max_relevant, isar_proof, isar_shrink_factor, timeout, ...} : params) 
39318  239 
minimize_command ({state, goal, subgoal, axioms} : problem) = 
38023  240 
let 
39318  241 
val ctxt = Proof.context_of state 
38998  242 
val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal 
243 
val max_relevant = the_default default_max_relevant max_relevant 

39005  244 
val axioms = take max_relevant axioms 
38023  245 
val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER" 
38998  246 
else Config.get ctxt dest_dir 
247 
val the_problem_prefix = Config.get ctxt problem_prefix 

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

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

249 
Path.basic ((if overlord then "prob_" ^ atp_name 
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset

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

251 
^ "_" ^ string_of_int subgoal) 
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset

252 
val problem_path_name = 
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset

253 
if the_dest_dir = "" then 
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset

254 
File.tmp_path problem_file_name 
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset

255 
else if File.exists (Path.explode the_dest_dir) then 
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset

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

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

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

259 
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

260 
val command = Path.explode (getenv (fst exec) ^ "/" ^ snd exec) 
38023  261 
(* write out problem file and call prover *) 
38645  262 
fun command_line complete timeout probfile = 
38023  263 
let 
264 
val core = File.shell_path command ^ " " ^ arguments complete timeout ^ 

265 
" " ^ File.shell_path probfile 

266 
in 

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

268 
else "exec " ^ core) ^ " 2>&1" 
38023  269 
end 
270 
fun split_time s = 

271 
let 

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

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

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

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

276 
val digit = Scan.one Symbol.is_ascii_digit; 

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

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

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

280 
in (output, as_time t) end; 

281 
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

282 
case filter (curry (op =) "" o getenv o fst) (exec :: required_execs) of 
38032  283 
(home_var, _) :: _ => 
38023  284 
error ("The environment variable " ^ quote home_var ^ " is not set.") 
38032  285 
 [] => 
286 
if File.exists command then 

287 
let 

39318  288 
fun run complete timeout = 
38032  289 
let 
38645  290 
val command = command_line complete timeout probfile 
38032  291 
val ((output, msecs), res_code) = 
292 
bash_output command 

293 
>> (if overlord then 

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

295 
else 

296 
I) 

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

297 
>> (if measure_run_time then split_time else rpair 0) 
38032  298 
val (proof, outcome) = 
299 
extract_proof_and_outcome complete res_code proof_delims 

300 
known_failures output 

301 
in (output, msecs, proof, outcome) end 

302 
val readable_names = debug andalso overlord 

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

303 
val (problem, pool, conjecture_offset, axiom_names) = 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38277
diff
changeset

304 
prepare_problem ctxt readable_names explicit_forall full_types 
39005  305 
explicit_apply hyp_ts concl_t axioms 
38631
979a0b37f981
prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible;
blanchet
parents:
38600
diff
changeset

306 
val ss = strings_for_tptp_problem use_conjecture_for_hypotheses 
979a0b37f981
prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible;
blanchet
parents:
38600
diff
changeset

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

308 
val _ = File.write_list probfile ss 
38032  309 
val conjecture_shape = 
310 
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

311 
> map single 
39318  312 
val run_twice = has_incomplete_mode andalso not auto 
38645  313 
val timer = Timer.startRealTimer () 
38032  314 
val result = 
39318  315 
run false (if run_twice then 
316 
Time.fromMilliseconds 

38645  317 
(2 * Time.toMilliseconds timeout div 3) 
39318  318 
else 
319 
timeout) 

320 
> run_twice 

38645  321 
? (fn (_, msecs0, _, SOME _) => 
39318  322 
run true (Time. (timeout, Timer.checkRealTimer timer)) 
38645  323 
> (fn (output, msecs, proof, outcome) => 
324 
(output, msecs0 + msecs, proof, outcome)) 

325 
 result => result) 

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

326 
in ((pool, conjecture_shape, axiom_names), result) end 
38032  327 
else 
328 
error ("Bad executable: " ^ Path.implode command ^ ".") 

38023  329 

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

331 
the proof file too. *) 

332 
fun cleanup probfile = 

333 
if the_dest_dir = "" then try File.rm probfile else NONE 

334 
fun export probfile (_, (output, _, _, _)) = 

335 
if the_dest_dir = "" then 

336 
() 

337 
else 

338 
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

339 
val ((pool, conjecture_shape, axiom_names), 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38277
diff
changeset

340 
(output, msecs, proof, outcome)) = 
39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset

341 
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

342 
val (conjecture_shape, axiom_names) = 
38023  343 
repair_conjecture_shape_and_theorem_names output conjecture_shape 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38277
diff
changeset

344 
axiom_names 
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

345 
val important_message = extract_important_message output 
38023  346 
val (message, used_thm_names) = 
347 
case outcome of 

348 
NONE => 

349 
proof_text isar_proof 

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

38998  351 
(full_types, minimize_command, proof, 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

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

353 
message ^ (if verbose then 
39010  354 
"\nReal CPU time: " ^ string_of_int msecs ^ " ms." 
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38741
diff
changeset

355 
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

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

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

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

359 
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

360 
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

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

362 
 SOME failure => (string_for_failure failure, []) 
38023  363 
in 
364 
{outcome = outcome, message = message, pool = pool, 

365 
used_thm_names = used_thm_names, atp_run_time_in_msecs = msecs, 

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

366 
output = output, proof = proof, axiom_names = axiom_names, 
38083
c4b57f68ddb3
remove the "extra_clauses" business introduced in 19a5f1c8a844;
blanchet
parents:
38061
diff
changeset

367 
conjecture_shape = conjecture_shape} 
38023  368 
end 
369 

39318  370 
fun get_prover_fun thy name = prover_fun false name (get_prover thy name) 
38023  371 

39318  372 
fun run_prover (params as {blocking, verbose, max_relevant, timeout, expect, 
373 
...}) 

374 
auto i n relevance_override minimize_command 

375 
(problem as {state, goal, axioms, ...}) 

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

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

377 
let 
39318  378 
val ctxt = Proof.context_of state 
37584  379 
val birth_time = Time.now () 
380 
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

381 
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

382 
val num_axioms = Int.min (length axioms, max_relevant) 
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

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

384 
"ATP " ^ quote atp_name ^ 
a74bd9bfa880
show the number of facts for each prover in "verbose" mode
blanchet
parents:
39108
diff
changeset

385 
(if verbose then 
a74bd9bfa880
show the number of facts for each prover in "verbose" mode
blanchet
parents:
39108
diff
changeset

386 
" with " ^ string_of_int num_axioms ^ " fact" ^ plural_s num_axioms 
a74bd9bfa880
show the number of facts for each prover in "verbose" mode
blanchet
parents:
39108
diff
changeset

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

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

389 
" on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^ ":" ^ 
38985
162bbbea4e4d
added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents:
38982
diff
changeset

390 
(if blocking then 
162bbbea4e4d
added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents:
38982
diff
changeset

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

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

393 
"\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i))) 
39318  394 
fun go () = 
38982
820b8221ed48
added "blocking" option to Sledgehammer to run in synchronous mode;
blanchet
parents:
38893
diff
changeset

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

396 
val (outcome_code, message) = 
39318  397 
prover_fun auto atp_name prover params (minimize_command atp_name) 
398 
problem 

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

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

400 
(if is_some outcome then "none" else "some", message)) 
162bbbea4e4d
added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents:
38982
diff
changeset

401 
handle ERROR message => ("unknown", "Error: " ^ message ^ "\n") 
162bbbea4e4d
added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents:
38982
diff
changeset

402 
 exn => ("unknown", "Internal error:\n" ^ 
162bbbea4e4d
added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents:
38982
diff
changeset

403 
ML_Compiler.exn_message exn ^ "\n") 
39318  404 
val _ = 
405 
if expect = "" orelse outcome_code = expect then 

406 
() 

407 
else if blocking then 

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

409 
else 

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

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

412 
in 

413 
if auto then 

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

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

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

417 
(Pretty.str ("Sledgehammer found a proof! " ^ message))])) 

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

418 
end 
39318  419 
else if blocking then 
420 
let val (success, message) = TimeLimit.timeLimit timeout go () in 

421 
priority (desc ^ "\n" ^ message); (success, state) 

422 
end 

423 
else 

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

425 
(false, state)) 

37584  426 
end 
28582  427 

39318  428 
val auto_max_relevant_divisor = 2 
429 

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

430 
fun run_sledgehammer (params as {blocking, verbose, atps, full_types, 
38998  431 
relevance_thresholds, max_relevant, ...}) 
39318  432 
auto i relevance_override minimize_command state = 
433 
if null atps then 

434 
error "No ATP is set." 

435 
else case subgoal_count state of 

436 
0 => (priority "No subgoal!"; (false, state)) 

437 
 n => 

438 
let 

439 
val thy = Proof.theory_of state 

440 
val timer = Timer.startRealTimer () 

441 
val _ = () > not blocking ? kill_atps 

442 
val _ = if auto then () else priority "Sledgehammering..." 

443 
val provers = map (`(get_prover thy)) atps 

444 
fun go () = 

445 
let 

446 
val {context = ctxt, facts = chained_ths, goal} = Proof.goal state 

447 
val (_, hyp_ts, concl_t) = strip_subgoal goal i 

448 
val max_max_relevant = 

449 
case max_relevant of 

450 
SOME n => n 

451 
 NONE => 

452 
0 > fold (Integer.max o #default_max_relevant o fst) provers 

453 
> auto ? (fn n => n div auto_max_relevant_divisor) 

454 
val axioms = 

455 
relevant_facts ctxt full_types relevance_thresholds 

456 
max_max_relevant relevance_override chained_ths 

457 
hyp_ts concl_t 

458 
val problem = 

459 
{state = state, goal = goal, subgoal = i, 

460 
axioms = map (prepare_axiom ctxt) axioms} 

461 
val run_prover = 

462 
run_prover params auto i n relevance_override minimize_command 

463 
problem 

464 
val num_axioms = length axioms 

465 
in 

466 
if auto then 

467 
fold (fn prover => fn (true, state) => (true, state) 

468 
 (false, _) => run_prover prover) 

469 
provers (false, state) 

470 
else 

471 
(if blocking then Par_List.map else map) run_prover provers 

472 
> tap (fn _ => 

473 
if verbose then 

474 
priority ("Total time: " ^ 

475 
signed_string_of_int (Time.toMilliseconds 

476 
(Timer.checkRealTimer timer)) ^ " ms.") 

477 
else 

478 
()) 

479 
> exists fst > rpair state 

480 
end 

481 
in if blocking then go () else Future.fork (tap go) > K (false, state) end 

38044  482 

38023  483 
val setup = 
484 
dest_dir_setup 

485 
#> problem_prefix_setup 

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

486 
#> measure_run_time_setup 
38023  487 

28582  488 
end; 