author | blanchet |
Wed, 25 Aug 2010 09:32:43 +0200 | |
changeset 38741 | 7635bf8918a1 |
parent 38739 | 8b8ed80b5699 |
child 38744 | 2b6333f78a9e |
permissions | -rw-r--r-- |
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 |
35969 | 12 |
type relevance_override = Sledgehammer_Fact_Filter.relevance_override |
36281
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36235
diff
changeset
|
13 |
type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command |
35969 | 14 |
type params = |
15 |
{debug: bool, |
|
16 |
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
|
17 |
overlord: bool, |
35969 | 18 |
atps: string list, |
19 |
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
|
20 |
explicit_apply: bool, |
35969 | 21 |
relevance_threshold: real, |
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset
|
22 |
relevance_decay: real, |
38589
b03f8fe043ec
added "max_relevant_per_iter" option to Sledgehammer
blanchet
parents:
38515
diff
changeset
|
23 |
max_relevant_per_iter: int option, |
36220
f3655a3ae1ab
rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does
blanchet
parents:
36184
diff
changeset
|
24 |
theory_relevant: bool option, |
35969 | 25 |
isar_proof: bool, |
36924 | 26 |
isar_shrink_factor: int, |
38590
bd443b426d56
get rid of "minimize_timeout", now that there's an automatic adaptive timeout mechanism in "minimize"
blanchet
parents:
38589
diff
changeset
|
27 |
timeout: Time.time} |
35867 | 28 |
type problem = |
35969 | 29 |
{subgoal: int, |
30 |
goal: Proof.context * (thm list * thm), |
|
31 |
relevance_override: relevance_override, |
|
38698
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38682
diff
changeset
|
32 |
axioms: ((string * bool) * thm) list option} |
35867 | 33 |
type prover_result = |
36370
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
34 |
{outcome: failure option, |
35969 | 35 |
message: string, |
37926
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37627
diff
changeset
|
36 |
pool: string Symtab.table, |
38698
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38682
diff
changeset
|
37 |
used_thm_names: (string * bool) list, |
35969 | 38 |
atp_run_time_in_msecs: int, |
36369
d2cd0d04b8e6
handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents:
36289
diff
changeset
|
39 |
output: string, |
35969 | 40 |
proof: string, |
38698
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38682
diff
changeset
|
41 |
axiom_names: (string * bool) vector, |
38083
c4b57f68ddb3
remove the "extra_clauses" business introduced in 19a5f1c8a844;
blanchet
parents:
38061
diff
changeset
|
42 |
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
|
43 |
type prover = params -> minimize_command -> problem -> prover_result |
35867 | 44 |
|
38023 | 45 |
val dest_dir : string Config.T |
46 |
val problem_prefix : string Config.T |
|
47 |
val measure_runtime : bool Config.T |
|
35969 | 48 |
val kill_atps: unit -> unit |
49 |
val running_atps: unit -> unit |
|
29112
f2b45eea6dac
added 'atp_messages' command, which displays recent messages synchronously;
wenzelm
parents:
28835
diff
changeset
|
50 |
val messages: int option -> unit |
38023 | 51 |
val get_prover_fun : theory -> string -> prover |
38044 | 52 |
val run_sledgehammer : |
53 |
params -> int -> relevance_override -> (string -> minimize_command) |
|
54 |
-> Proof.state -> unit |
|
38023 | 55 |
val setup : theory -> theory |
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
56 |
end; |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
57 |
|
38021
e024504943d1
rename "ATP_Manager" ML module to "Sledgehammer";
blanchet
parents:
38020
diff
changeset
|
58 |
structure Sledgehammer : SLEDGEHAMMER = |
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
59 |
struct |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
60 |
|
38028 | 61 |
open ATP_Problem |
62 |
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
|
63 |
open Metis_Clauses |
38023 | 64 |
open Sledgehammer_Util |
36063
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36059
diff
changeset
|
65 |
open Sledgehammer_Fact_Filter |
38282
319c59682c51
move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38277
diff
changeset
|
66 |
open Sledgehammer_Translate |
36063
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36059
diff
changeset
|
67 |
open Sledgehammer_Proof_Reconstruct |
37583
9ce2451647d5
factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
37581
diff
changeset
|
68 |
|
38023 | 69 |
|
37583
9ce2451647d5
factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
37581
diff
changeset
|
70 |
(** The Sledgehammer **) |
9ce2451647d5
factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
37581
diff
changeset
|
71 |
|
38102
019a49759829
fix bug in the newly introduced "bound concealing" code
blanchet
parents:
38100
diff
changeset
|
72 |
(* Identifier to distinguish Sledgehammer from other tools using |
019a49759829
fix bug in the newly introduced "bound concealing" code
blanchet
parents:
38100
diff
changeset
|
73 |
"Async_Manager". *) |
37585 | 74 |
val das_Tool = "Sledgehammer" |
75 |
||
76 |
fun kill_atps () = Async_Manager.kill_threads das_Tool "ATPs" |
|
77 |
fun running_atps () = Async_Manager.running_threads das_Tool "ATPs" |
|
78 |
val messages = Async_Manager.thread_messages das_Tool "ATP" |
|
35969 | 79 |
|
36281
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36235
diff
changeset
|
80 |
(** problems, results, provers, etc. **) |
35969 | 81 |
|
82 |
type params = |
|
83 |
{debug: bool, |
|
84 |
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
|
85 |
overlord: bool, |
35969 | 86 |
atps: string list, |
87 |
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
|
88 |
explicit_apply: bool, |
35969 | 89 |
relevance_threshold: real, |
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset
|
90 |
relevance_decay: real, |
38589
b03f8fe043ec
added "max_relevant_per_iter" option to Sledgehammer
blanchet
parents:
38515
diff
changeset
|
91 |
max_relevant_per_iter: int option, |
36220
f3655a3ae1ab
rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does
blanchet
parents:
36184
diff
changeset
|
92 |
theory_relevant: bool option, |
35969 | 93 |
isar_proof: bool, |
36924 | 94 |
isar_shrink_factor: int, |
38590
bd443b426d56
get rid of "minimize_timeout", now that there's an automatic adaptive timeout mechanism in "minimize"
blanchet
parents:
38589
diff
changeset
|
95 |
timeout: Time.time} |
35867 | 96 |
|
97 |
type problem = |
|
35969 | 98 |
{subgoal: int, |
99 |
goal: Proof.context * (thm list * thm), |
|
100 |
relevance_override: relevance_override, |
|
38698
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38682
diff
changeset
|
101 |
axioms: ((string * bool) * thm) list option} |
35867 | 102 |
|
103 |
type prover_result = |
|
36370
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
104 |
{outcome: failure option, |
35969 | 105 |
message: string, |
37926
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37627
diff
changeset
|
106 |
pool: string Symtab.table, |
38698
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38682
diff
changeset
|
107 |
used_thm_names: (string * bool) list, |
35969 | 108 |
atp_run_time_in_msecs: int, |
36369
d2cd0d04b8e6
handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents:
36289
diff
changeset
|
109 |
output: string, |
35969 | 110 |
proof: string, |
38698
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38682
diff
changeset
|
111 |
axiom_names: (string * bool) vector, |
38083
c4b57f68ddb3
remove the "extra_clauses" business introduced in 19a5f1c8a844;
blanchet
parents:
38061
diff
changeset
|
112 |
conjecture_shape: int list list} |
35867 | 113 |
|
38100
e458a0dd3dc1
use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
blanchet
parents:
38098
diff
changeset
|
114 |
type prover = params -> minimize_command -> problem -> prover_result |
35867 | 115 |
|
38023 | 116 |
(* configuration attributes *) |
117 |
||
118 |
val (dest_dir, dest_dir_setup) = Attrib.config_string "atp_dest_dir" (K ""); |
|
119 |
(*Empty string means create files in Isabelle's temporary files directory.*) |
|
120 |
||
121 |
val (problem_prefix, problem_prefix_setup) = |
|
122 |
Attrib.config_string "atp_problem_prefix" (K "prob"); |
|
123 |
||
124 |
val (measure_runtime, measure_runtime_setup) = |
|
125 |
Attrib.config_bool "atp_measure_runtime" (K false); |
|
28484 | 126 |
|
38023 | 127 |
fun with_path cleanup after f path = |
128 |
Exn.capture f path |
|
129 |
|> tap (fn _ => cleanup path) |
|
130 |
|> Exn.release |
|
131 |
|> tap (after path) |
|
132 |
||
133 |
(* Splits by the first possible of a list of delimiters. *) |
|
134 |
fun extract_proof delims output = |
|
135 |
case pairself (find_first (fn s => String.isSubstring s output)) |
|
136 |
(ListPair.unzip delims) of |
|
137 |
(SOME begin_delim, SOME end_delim) => |
|
138 |
(output |> first_field begin_delim |> the |> snd |
|
139 |
|> first_field end_delim |> the |> fst |
|
140 |
|> first_field "\n" |> the |> snd |
|
141 |
handle Option.Option => "") |
|
142 |
| _ => "" |
|
28484 | 143 |
|
38023 | 144 |
fun extract_proof_and_outcome complete res_code proof_delims known_failures |
145 |
output = |
|
38061
685d1f0f75b3
handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents:
38044
diff
changeset
|
146 |
case known_failure_in_output output known_failures of |
685d1f0f75b3
handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents:
38044
diff
changeset
|
147 |
NONE => (case extract_proof proof_delims output of |
685d1f0f75b3
handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents:
38044
diff
changeset
|
148 |
"" => ("", SOME MalformedOutput) |
38023 | 149 |
| proof => if res_code = 0 then (proof, NONE) |
150 |
else ("", SOME UnknownError)) |
|
38061
685d1f0f75b3
handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents:
38044
diff
changeset
|
151 |
| SOME failure => |
38023 | 152 |
("", SOME (if failure = IncompleteUnprovable andalso complete then |
153 |
Unprovable |
|
154 |
else |
|
155 |
failure)) |
|
28582 | 156 |
|
38023 | 157 |
fun extract_clause_sequence output = |
158 |
let |
|
159 |
val tokens_of = String.tokens (not o Char.isAlphaNum) |
|
160 |
fun extract_num ("clause" :: (ss as _ :: _)) = |
|
161 |
Int.fromString (List.last ss) |
|
162 |
| extract_num _ = NONE |
|
163 |
in output |> split_lines |> map_filter (extract_num o tokens_of) end |
|
164 |
||
165 |
val set_ClauseFormulaRelationN = "set_ClauseFormulaRelation" |
|
166 |
||
167 |
val parse_clause_formula_pair = |
|
38515 | 168 |
$$ "(" |-- scan_integer --| $$ "," |
169 |
-- (Symbol.scan_id ::: Scan.repeat ($$ "," |-- Symbol.scan_id)) --| $$ ")" |
|
38023 | 170 |
--| Scan.option ($$ ",") |
171 |
val parse_clause_formula_relation = |
|
172 |
Scan.this_string set_ClauseFormulaRelationN |-- $$ "(" |
|
173 |
|-- Scan.repeat parse_clause_formula_pair |
|
174 |
val extract_clause_formula_relation = |
|
38738
0ce517c1970f
make sure that "undo_ascii_of" is the inverse of "ascii_of", also for non-printable characters -- and avoid those in ``-style facts
blanchet
parents:
38698
diff
changeset
|
175 |
Substring.full #> Substring.position set_ClauseFormulaRelationN |
0ce517c1970f
make sure that "undo_ascii_of" is the inverse of "ascii_of", also for non-printable characters -- and avoid those in ``-style facts
blanchet
parents:
38698
diff
changeset
|
176 |
#> snd #> Substring.string #> strip_spaces_except_between_ident_chars |
0ce517c1970f
make sure that "undo_ascii_of" is the inverse of "ascii_of", also for non-printable characters -- and avoid those in ``-style facts
blanchet
parents:
38698
diff
changeset
|
177 |
#> explode #> parse_clause_formula_relation #> fst |
38023 | 178 |
|
179 |
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
|
180 |
axiom_names = |
38023 | 181 |
if String.isSubstring set_ClauseFormulaRelationN output then |
182 |
(* 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
|
183 |
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
|
184 |
also part of this hack. *) |
38023 | 185 |
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
|
186 |
val j0 = hd (hd conjecture_shape) |
38023 | 187 |
val seq = extract_clause_sequence output |
188 |
val name_map = extract_clause_formula_relation output |
|
189 |
fun renumber_conjecture j = |
|
38515 | 190 |
conjecture_prefix ^ Int.toString (j - j0) |
191 |
|> 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
|
192 |
|> map (fn s => find_index (curry (op =) s) seq + 1) |
38698
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38682
diff
changeset
|
193 |
fun name_for_number j = |
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38682
diff
changeset
|
194 |
let |
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38682
diff
changeset
|
195 |
val axioms = |
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38682
diff
changeset
|
196 |
j |> AList.lookup (op =) name_map |
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38682
diff
changeset
|
197 |
|> these |> map_filter (try (unprefix axiom_prefix)) |
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38682
diff
changeset
|
198 |
|> map undo_ascii_of |
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38682
diff
changeset
|
199 |
val chained = forall (is_true_for axiom_names) axioms |
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38682
diff
changeset
|
200 |
in (axioms |> space_implode " ", chained) end |
38023 | 201 |
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
|
202 |
(conjecture_shape |> map (maps renumber_conjecture), |
38698
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38682
diff
changeset
|
203 |
seq |> map name_for_number |> Vector.fromList) |
38023 | 204 |
end |
205 |
else |
|
38698
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38682
diff
changeset
|
206 |
(conjecture_shape, axiom_names) |
38023 | 207 |
|
208 |
||
209 |
(* generic TPTP-based provers *) |
|
210 |
||
38455 | 211 |
fun prover_fun atp_name |
38645 | 212 |
{exec, required_execs, arguments, has_incomplete_mode, proof_delims, |
213 |
known_failures, default_max_relevant_per_iter, default_theory_relevant, |
|
38631
979a0b37f981
prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible;
blanchet
parents:
38600
diff
changeset
|
214 |
explicit_forall, use_conjecture_for_hypotheses} |
38455 | 215 |
({debug, verbose, overlord, full_types, explicit_apply, |
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset
|
216 |
relevance_threshold, relevance_decay, |
38741 | 217 |
max_relevant_per_iter, theory_relevant, isar_proof, |
218 |
isar_shrink_factor, timeout, ...} : params) |
|
38100
e458a0dd3dc1
use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
blanchet
parents:
38098
diff
changeset
|
219 |
minimize_command |
38084
e2aac207d13b
"axiom_clauses" -> "axioms" (these are no longer clauses)
blanchet
parents:
38083
diff
changeset
|
220 |
({subgoal, goal, relevance_override, axioms} : problem) = |
38023 | 221 |
let |
222 |
val (ctxt, (_, th)) = goal; |
|
223 |
val thy = ProofContext.theory_of ctxt |
|
224 |
val (params, hyp_ts, concl_t) = strip_subgoal th subgoal |
|
38455 | 225 |
|
226 |
fun print s = (priority s; if debug then tracing s else ()) |
|
227 |
fun print_v f = () |> verbose ? print o f |
|
228 |
fun print_d f = () |> debug ? print o f |
|
229 |
||
38084
e2aac207d13b
"axiom_clauses" -> "axioms" (these are no longer clauses)
blanchet
parents:
38083
diff
changeset
|
230 |
val the_axioms = |
e2aac207d13b
"axiom_clauses" -> "axioms" (these are no longer clauses)
blanchet
parents:
38083
diff
changeset
|
231 |
case axioms of |
38083
c4b57f68ddb3
remove the "extra_clauses" business introduced in 19a5f1c8a844;
blanchet
parents:
38061
diff
changeset
|
232 |
SOME axioms => axioms |
38455 | 233 |
| NONE => |
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset
|
234 |
(relevant_facts full_types relevance_threshold relevance_decay |
38589
b03f8fe043ec
added "max_relevant_per_iter" option to Sledgehammer
blanchet
parents:
38515
diff
changeset
|
235 |
(the_default default_max_relevant_per_iter |
b03f8fe043ec
added "max_relevant_per_iter" option to Sledgehammer
blanchet
parents:
38515
diff
changeset
|
236 |
max_relevant_per_iter) |
b03f8fe043ec
added "max_relevant_per_iter" option to Sledgehammer
blanchet
parents:
38515
diff
changeset
|
237 |
(the_default default_theory_relevant theory_relevant) |
38455 | 238 |
relevance_override goal hyp_ts concl_t |
239 |
|> tap ((fn n => print_v (fn () => |
|
240 |
"Selected " ^ string_of_int n ^ " fact" ^ plural_s n ^ |
|
241 |
" for " ^ quote atp_name ^ ".")) o length)) |
|
38023 | 242 |
|
243 |
(* path to unique problem file *) |
|
244 |
val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER" |
|
245 |
else Config.get ctxt dest_dir; |
|
246 |
val the_problem_prefix = Config.get ctxt problem_prefix; |
|
247 |
fun prob_pathname nr = |
|
248 |
let |
|
249 |
val probfile = |
|
38455 | 250 |
Path.basic ((if overlord then "prob_" ^ atp_name |
38023 | 251 |
else the_problem_prefix ^ serial_string ()) |
252 |
^ "_" ^ string_of_int nr) |
|
253 |
in |
|
254 |
if the_dest_dir = "" then File.tmp_path probfile |
|
255 |
else if File.exists (Path.explode the_dest_dir) |
|
256 |
then Path.append (Path.explode the_dest_dir) probfile |
|
257 |
else error ("No such directory: " ^ the_dest_dir ^ ".") |
|
258 |
end; |
|
259 |
||
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 |
|
267 |
(if Config.get ctxt measure_runtime then |
|
268 |
"TIMEFORMAT='%3U'; { time " ^ core ^ " ; }" |
|
269 |
else |
|
270 |
"exec " ^ core) ^ " 2>&1" |
|
271 |
end |
|
272 |
fun split_time s = |
|
273 |
let |
|
274 |
val split = String.tokens (fn c => str c = "\n"); |
|
275 |
val (output, t) = s |> split |> split_last |> apfst cat_lines; |
|
276 |
fun as_num f = f >> (fst o read_int); |
|
277 |
val num = as_num (Scan.many1 Symbol.is_ascii_digit); |
|
278 |
val digit = Scan.one Symbol.is_ascii_digit; |
|
279 |
val num3 = as_num (digit ::: digit ::: (digit >> single)); |
|
280 |
val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b); |
|
281 |
val as_time = the_default 0 o Scan.read Symbol.stopper time o explode; |
|
282 |
in (output, as_time t) end; |
|
283 |
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
|
284 |
case filter (curry (op =) "" o getenv o fst) (exec :: required_execs) of |
38032 | 285 |
(home_var, _) :: _ => |
38023 | 286 |
error ("The environment variable " ^ quote home_var ^ " is not set.") |
38032 | 287 |
| [] => |
288 |
if File.exists command then |
|
289 |
let |
|
38645 | 290 |
fun do_run complete timeout = |
38032 | 291 |
let |
38645 | 292 |
val command = command_line complete timeout probfile |
38032 | 293 |
val ((output, msecs), res_code) = |
294 |
bash_output command |
|
295 |
|>> (if overlord then |
|
296 |
prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") |
|
297 |
else |
|
298 |
I) |
|
299 |
|>> (if Config.get ctxt measure_runtime then split_time |
|
300 |
else rpair 0) |
|
301 |
val (proof, outcome) = |
|
302 |
extract_proof_and_outcome complete res_code proof_delims |
|
303 |
known_failures output |
|
304 |
in (output, msecs, proof, outcome) end |
|
38455 | 305 |
val _ = print_d (fn () => "Preparing problem for " ^ |
306 |
quote atp_name ^ "...") |
|
38032 | 307 |
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
|
308 |
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
|
309 |
prepare_problem ctxt readable_names explicit_forall full_types |
319c59682c51
move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38277
diff
changeset
|
310 |
explicit_apply hyp_ts concl_t the_axioms |
38631
979a0b37f981
prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible;
blanchet
parents:
38600
diff
changeset
|
311 |
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
|
312 |
problem |
979a0b37f981
prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible;
blanchet
parents:
38600
diff
changeset
|
313 |
val _ = File.write_list probfile ss |
38032 | 314 |
val conjecture_shape = |
315 |
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
|
316 |
|> map single |
38455 | 317 |
val _ = print_d (fn () => "Running " ^ quote atp_name ^ "...") |
38645 | 318 |
val timer = Timer.startRealTimer () |
38032 | 319 |
val result = |
38645 | 320 |
do_run false (if has_incomplete_mode then |
321 |
Time.fromMilliseconds |
|
322 |
(2 * Time.toMilliseconds timeout div 3) |
|
323 |
else |
|
324 |
timeout) |
|
325 |
|> has_incomplete_mode |
|
326 |
? (fn (_, msecs0, _, SOME _) => |
|
327 |
do_run true |
|
328 |
(Time.- (timeout, Timer.checkRealTimer timer)) |
|
329 |
|> (fn (output, msecs, proof, outcome) => |
|
330 |
(output, msecs0 + msecs, proof, outcome)) |
|
331 |
| result => result) |
|
38282
319c59682c51
move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38277
diff
changeset
|
332 |
in ((pool, conjecture_shape, axiom_names), result) end |
38032 | 333 |
else |
334 |
error ("Bad executable: " ^ Path.implode command ^ ".") |
|
38023 | 335 |
|
336 |
(* If the problem file has not been exported, remove it; otherwise, export |
|
337 |
the proof file too. *) |
|
338 |
fun cleanup probfile = |
|
339 |
if the_dest_dir = "" then try File.rm probfile else NONE |
|
340 |
fun export probfile (_, (output, _, _, _)) = |
|
341 |
if the_dest_dir = "" then |
|
342 |
() |
|
343 |
else |
|
344 |
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
|
345 |
val ((pool, conjecture_shape, axiom_names), |
319c59682c51
move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38277
diff
changeset
|
346 |
(output, msecs, proof, outcome)) = |
38023 | 347 |
with_path cleanup export run_on (prob_pathname subgoal) |
38282
319c59682c51
move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38277
diff
changeset
|
348 |
val (conjecture_shape, axiom_names) = |
38023 | 349 |
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
|
350 |
axiom_names |
38023 | 351 |
val (message, used_thm_names) = |
352 |
case outcome of |
|
353 |
NONE => |
|
354 |
proof_text isar_proof |
|
355 |
(pool, debug, isar_shrink_factor, ctxt, conjecture_shape) |
|
38282
319c59682c51
move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38277
diff
changeset
|
356 |
(full_types, minimize_command, proof, axiom_names, th, subgoal) |
38597
db482afec7f0
no spurious trailing "\n" at the end of Sledgehammer's output
blanchet
parents:
38590
diff
changeset
|
357 |
| SOME failure => (string_for_failure failure, []) |
38023 | 358 |
in |
359 |
{outcome = outcome, message = message, pool = pool, |
|
360 |
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
|
361 |
output = output, proof = proof, axiom_names = axiom_names, |
38083
c4b57f68ddb3
remove the "extra_clauses" business introduced in 19a5f1c8a844;
blanchet
parents:
38061
diff
changeset
|
362 |
conjecture_shape = conjecture_shape} |
38023 | 363 |
end |
364 |
||
365 |
fun get_prover_fun thy name = prover_fun name (get_prover thy name) |
|
366 |
||
37584 | 367 |
fun start_prover_thread (params as {verbose, full_types, timeout, ...}) i n |
38455 | 368 |
relevance_override minimize_command proof_state |
369 |
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
|
370 |
let |
38023 | 371 |
val thy = Proof.theory_of proof_state |
37584 | 372 |
val birth_time = Time.now () |
373 |
val death_time = Time.+ (birth_time, timeout) |
|
38455 | 374 |
val prover = get_prover_fun thy 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
|
375 |
val {context = ctxt, facts, goal} = Proof.goal proof_state; |
20ef039bccff
make "ATP_Manager.get_prover" a total function, since we always want to show the same error text
blanchet
parents:
36373
diff
changeset
|
376 |
val desc = |
38455 | 377 |
"ATP " ^ quote atp_name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^ |
36392 | 378 |
Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)); |
37584 | 379 |
in |
37585 | 380 |
Async_Manager.launch das_Tool verbose birth_time death_time desc |
37584 | 381 |
(fn () => |
382 |
let |
|
383 |
val problem = |
|
384 |
{subgoal = i, goal = (ctxt, (facts, goal)), |
|
38084
e2aac207d13b
"axiom_clauses" -> "axioms" (these are no longer clauses)
blanchet
parents:
38083
diff
changeset
|
385 |
relevance_override = relevance_override, axioms = NONE} |
37584 | 386 |
in |
38455 | 387 |
prover params (minimize_command atp_name) problem |> #message |
37994
b04307085a09
make TPTP generator accept full first-order formulas
blanchet
parents:
37926
diff
changeset
|
388 |
handle ERROR message => "Error: " ^ message ^ "\n" |
38290
581a402a80f0
prevent ATP thread for staying around for 1 minute if an exception occurred earlier;
blanchet
parents:
38282
diff
changeset
|
389 |
| exn => "Internal error: \n" ^ ML_Compiler.exn_message exn ^ |
581a402a80f0
prevent ATP thread for staying around for 1 minute if an exception occurred earlier;
blanchet
parents:
38282
diff
changeset
|
390 |
"\n" |
37584 | 391 |
end) |
392 |
end |
|
28582 | 393 |
|
38044 | 394 |
fun run_sledgehammer {atps = [], ...} _ _ _ _ = error "No ATP is set." |
395 |
| run_sledgehammer (params as {atps, ...}) i relevance_override |
|
396 |
minimize_command state = |
|
397 |
case subgoal_count state of |
|
398 |
0 => priority "No subgoal!" |
|
399 |
| n => |
|
400 |
let |
|
401 |
val _ = kill_atps () |
|
402 |
val _ = priority "Sledgehammering..." |
|
403 |
val _ = app (start_prover_thread params i n relevance_override |
|
404 |
minimize_command state) atps |
|
405 |
in () end |
|
406 |
||
38023 | 407 |
val setup = |
408 |
dest_dir_setup |
|
409 |
#> problem_prefix_setup |
|
410 |
#> measure_runtime_setup |
|
411 |
||
28582 | 412 |
end; |