author | blanchet |
Thu, 16 Sep 2010 11:59:45 +0200 | |
changeset 39453 | 1740a2d6bef9 |
parent 39452 | 70a57e40f795 |
child 39491 | 2416666e6f94 |
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 |
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, |
|
39366
f58fbb959826
handle relevance filter corner cases more gracefully;
blanchet
parents:
39364
diff
changeset
|
34 |
axioms: (term * ((string * locality) * fol_formula) option) list, |
f58fbb959826
handle relevance filter corner cases more gracefully;
blanchet
parents:
39364
diff
changeset
|
35 |
only: bool} |
35867 | 36 |
type prover_result = |
36370
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
37 |
{outcome: failure option, |
35969 | 38 |
message: string, |
37926
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37627
diff
changeset
|
39 |
pool: string Symtab.table, |
38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38748
diff
changeset
|
40 |
used_thm_names: (string * locality) list, |
35969 | 41 |
atp_run_time_in_msecs: int, |
36369
d2cd0d04b8e6
handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents:
36289
diff
changeset
|
42 |
output: string, |
39452 | 43 |
tstplike_proof: string, |
38818
61cf050f8b2e
improve SPASS hack, when a clause comes from several facts
blanchet
parents:
38752
diff
changeset
|
44 |
axiom_names: (string * locality) list vector, |
38083
c4b57f68ddb3
remove the "extra_clauses" business introduced in 19a5f1c8a844;
blanchet
parents:
38061
diff
changeset
|
45 |
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
|
46 |
type prover = params -> minimize_command -> problem -> prover_result |
35867 | 47 |
|
38023 | 48 |
val dest_dir : string Config.T |
49 |
val problem_prefix : string Config.T |
|
39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset
|
50 |
val measure_run_time : bool Config.T |
35969 | 51 |
val kill_atps: unit -> unit |
52 |
val running_atps: unit -> unit |
|
29112
f2b45eea6dac
added 'atp_messages' command, which displays recent messages synchronously;
wenzelm
parents:
28835
diff
changeset
|
53 |
val messages: int option -> unit |
38023 | 54 |
val get_prover_fun : theory -> string -> prover |
38044 | 55 |
val run_sledgehammer : |
39318 | 56 |
params -> bool -> int -> relevance_override -> (string -> minimize_command) |
57 |
-> Proof.state -> bool * Proof.state |
|
38023 | 58 |
val setup : theory -> theory |
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
59 |
end; |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
60 |
|
38021
e024504943d1
rename "ATP_Manager" ML module to "Sledgehammer";
blanchet
parents:
38020
diff
changeset
|
61 |
structure Sledgehammer : SLEDGEHAMMER = |
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
62 |
struct |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
63 |
|
38028 | 64 |
open ATP_Problem |
65 |
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
|
66 |
open Metis_Clauses |
38023 | 67 |
open Sledgehammer_Util |
38988 | 68 |
open Sledgehammer_Filter |
38282
319c59682c51
move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38277
diff
changeset
|
69 |
open Sledgehammer_Translate |
38988 | 70 |
open Sledgehammer_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
|
71 |
|
38023 | 72 |
|
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
|
73 |
(** 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
|
74 |
|
38102
019a49759829
fix bug in the newly introduced "bound concealing" code
blanchet
parents:
38100
diff
changeset
|
75 |
(* Identifier to distinguish Sledgehammer from other tools using |
019a49759829
fix bug in the newly introduced "bound concealing" code
blanchet
parents:
38100
diff
changeset
|
76 |
"Async_Manager". *) |
37585 | 77 |
val das_Tool = "Sledgehammer" |
78 |
||
79 |
fun kill_atps () = Async_Manager.kill_threads das_Tool "ATPs" |
|
80 |
fun running_atps () = Async_Manager.running_threads das_Tool "ATPs" |
|
81 |
val messages = Async_Manager.thread_messages das_Tool "ATP" |
|
35969 | 82 |
|
36281
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36235
diff
changeset
|
83 |
(** problems, results, provers, etc. **) |
35969 | 84 |
|
85 |
type params = |
|
38982
820b8221ed48
added "blocking" option to Sledgehammer to run in synchronous mode;
blanchet
parents:
38893
diff
changeset
|
86 |
{blocking: bool, |
820b8221ed48
added "blocking" option to Sledgehammer to run in synchronous mode;
blanchet
parents:
38893
diff
changeset
|
87 |
debug: bool, |
35969 | 88 |
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
|
89 |
overlord: bool, |
35969 | 90 |
atps: string list, |
91 |
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
|
92 |
explicit_apply: bool, |
38745
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset
|
93 |
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
|
94 |
max_relevant: int option, |
35969 | 95 |
isar_proof: bool, |
36924 | 96 |
isar_shrink_factor: int, |
38985
162bbbea4e4d
added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents:
38982
diff
changeset
|
97 |
timeout: Time.time, |
162bbbea4e4d
added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents:
38982
diff
changeset
|
98 |
expect: string} |
35867 | 99 |
|
100 |
type problem = |
|
39318 | 101 |
{state: Proof.state, |
38998 | 102 |
goal: thm, |
103 |
subgoal: int, |
|
39366
f58fbb959826
handle relevance filter corner cases more gracefully;
blanchet
parents:
39364
diff
changeset
|
104 |
axioms: (term * ((string * locality) * fol_formula) option) list, |
f58fbb959826
handle relevance filter corner cases more gracefully;
blanchet
parents:
39364
diff
changeset
|
105 |
only: bool} |
35867 | 106 |
|
107 |
type prover_result = |
|
36370
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
108 |
{outcome: failure option, |
35969 | 109 |
message: string, |
37926
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37627
diff
changeset
|
110 |
pool: string Symtab.table, |
38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38748
diff
changeset
|
111 |
used_thm_names: (string * locality) list, |
35969 | 112 |
atp_run_time_in_msecs: int, |
36369
d2cd0d04b8e6
handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents:
36289
diff
changeset
|
113 |
output: string, |
39452 | 114 |
tstplike_proof: string, |
38818
61cf050f8b2e
improve SPASS hack, when a clause comes from several facts
blanchet
parents:
38752
diff
changeset
|
115 |
axiom_names: (string * locality) list vector, |
38083
c4b57f68ddb3
remove the "extra_clauses" business introduced in 19a5f1c8a844;
blanchet
parents:
38061
diff
changeset
|
116 |
conjecture_shape: int list list} |
35867 | 117 |
|
38100
e458a0dd3dc1
use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
blanchet
parents:
38098
diff
changeset
|
118 |
type prover = params -> minimize_command -> problem -> prover_result |
35867 | 119 |
|
38023 | 120 |
(* configuration attributes *) |
121 |
||
38991 | 122 |
val (dest_dir, dest_dir_setup) = |
39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset
|
123 |
Attrib.config_string "sledgehammer_dest_dir" (K "") |
38991 | 124 |
(* Empty string means create files in Isabelle's temporary files directory. *) |
38023 | 125 |
|
126 |
val (problem_prefix, problem_prefix_setup) = |
|
39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset
|
127 |
Attrib.config_string "sledgehammer_problem_prefix" (K "prob") |
38023 | 128 |
|
39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset
|
129 |
val (measure_run_time, measure_run_time_setup) = |
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset
|
130 |
Attrib.config_bool "sledgehammer_measure_run_time" (K false) |
28484 | 131 |
|
38023 | 132 |
fun with_path cleanup after f path = |
133 |
Exn.capture f path |
|
134 |
|> tap (fn _ => cleanup path) |
|
135 |
|> Exn.release |
|
136 |
|> tap (after path) |
|
137 |
||
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
|
138 |
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
|
139 |
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
|
140 |
|> 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
|
141 |
|> 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
|
142 |
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
|
143 |
|
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 |
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
|
145 |
("% 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
|
146 |
|
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 |
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
|
148 |
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
|
149 |
"" => "" |
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 |
| 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
|
151 |
|> 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
|
152 |
|> 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
|
153 |
|> 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
|
154 |
|
38023 | 155 |
(* Splits by the first possible of a list of delimiters. *) |
39452 | 156 |
fun extract_tstplike_proof delims output = |
38023 | 157 |
case pairself (find_first (fn s => String.isSubstring s output)) |
158 |
(ListPair.unzip delims) of |
|
159 |
(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
|
160 |
extract_delimited (begin_delim, end_delim) output |
38023 | 161 |
| _ => "" |
28484 | 162 |
|
39452 | 163 |
fun extract_tstplike_proof_and_outcome complete res_code proof_delims |
164 |
known_failures 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
|
165 |
case known_failure_in_output output known_failures of |
39452 | 166 |
NONE => (case extract_tstplike_proof proof_delims output of |
39262
bdfcf2434601
better error reporting when the Sledgehammer minimizer is interrupted
blanchet
parents:
39223
diff
changeset
|
167 |
"" => ("", SOME (if res_code = 0 andalso output = "" then |
bdfcf2434601
better error reporting when the Sledgehammer minimizer is interrupted
blanchet
parents:
39223
diff
changeset
|
168 |
Interrupted |
bdfcf2434601
better error reporting when the Sledgehammer minimizer is interrupted
blanchet
parents:
39223
diff
changeset
|
169 |
else |
39263
e2a3c435334b
more precise error messages when Vampire is interrupted or SPASS runs into an internal bug
blanchet
parents:
39262
diff
changeset
|
170 |
UnknownError)) |
39452 | 171 |
| tstplike_proof => if res_code = 0 then (tstplike_proof, NONE) |
172 |
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
|
173 |
| SOME failure => |
38023 | 174 |
("", SOME (if failure = IncompleteUnprovable andalso complete then |
175 |
Unprovable |
|
176 |
else |
|
177 |
failure)) |
|
28582 | 178 |
|
38023 | 179 |
fun extract_clause_sequence output = |
180 |
let |
|
181 |
val tokens_of = String.tokens (not o Char.isAlphaNum) |
|
182 |
fun extract_num ("clause" :: (ss as _ :: _)) = |
|
183 |
Int.fromString (List.last ss) |
|
184 |
| extract_num _ = NONE |
|
185 |
in output |> split_lines |> map_filter (extract_num o tokens_of) end |
|
186 |
||
187 |
val set_ClauseFormulaRelationN = "set_ClauseFormulaRelation" |
|
188 |
||
189 |
val parse_clause_formula_pair = |
|
38515 | 190 |
$$ "(" |-- scan_integer --| $$ "," |
191 |
-- (Symbol.scan_id ::: Scan.repeat ($$ "," |-- Symbol.scan_id)) --| $$ ")" |
|
38023 | 192 |
--| Scan.option ($$ ",") |
193 |
val parse_clause_formula_relation = |
|
194 |
Scan.this_string set_ClauseFormulaRelationN |-- $$ "(" |
|
195 |
|-- Scan.repeat parse_clause_formula_pair |
|
196 |
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
|
197 |
Substring.full #> Substring.position set_ClauseFormulaRelationN |
39007
aae6a0d33c66
speed up SPASS hack + output time information in "blocking" mode
blanchet
parents:
39005
diff
changeset
|
198 |
#> snd #> Substring.position "." #> fst #> Substring.string |
39008 | 199 |
#> 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
|
200 |
#> fst |
38023 | 201 |
|
38988 | 202 |
(* TODO: move to "Sledgehammer_Reconstruct" *) |
38023 | 203 |
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
|
204 |
axiom_names = |
38023 | 205 |
if String.isSubstring set_ClauseFormulaRelationN output then |
206 |
(* 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
|
207 |
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
|
208 |
also part of this hack. *) |
38023 | 209 |
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
|
210 |
val j0 = hd (hd conjecture_shape) |
38023 | 211 |
val seq = extract_clause_sequence output |
212 |
val name_map = extract_clause_formula_relation output |
|
213 |
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
|
214 |
conjecture_prefix ^ string_of_int (j - j0) |
38515 | 215 |
|> 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
|
216 |
|> 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
|
217 |
fun names_for_number j = |
61cf050f8b2e
improve SPASS hack, when a clause comes from several facts
blanchet
parents:
38752
diff
changeset
|
218 |
j |> AList.lookup (op =) name_map |> these |
61cf050f8b2e
improve SPASS hack, when a clause comes from several facts
blanchet
parents:
38752
diff
changeset
|
219 |
|> 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
|
220 |
|> map (fn name => |
61cf050f8b2e
improve SPASS hack, when a clause comes from several facts
blanchet
parents:
38752
diff
changeset
|
221 |
(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
|
222 |
|> the) |
61cf050f8b2e
improve SPASS hack, when a clause comes from several facts
blanchet
parents:
38752
diff
changeset
|
223 |
handle Option.Option => |
61cf050f8b2e
improve SPASS hack, when a clause comes from several facts
blanchet
parents:
38752
diff
changeset
|
224 |
error ("No such fact: " ^ quote name ^ ".")) |
38023 | 225 |
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
|
226 |
(conjecture_shape |> map (maps renumber_conjecture), |
38818
61cf050f8b2e
improve SPASS hack, when a clause comes from several facts
blanchet
parents:
38752
diff
changeset
|
227 |
seq |> map names_for_number |> Vector.fromList) |
38023 | 228 |
end |
229 |
else |
|
38698
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38682
diff
changeset
|
230 |
(conjecture_shape, axiom_names) |
38023 | 231 |
|
232 |
||
233 |
(* generic TPTP-based provers *) |
|
234 |
||
39318 | 235 |
fun prover_fun auto atp_name |
38645 | 236 |
{exec, required_execs, arguments, has_incomplete_mode, proof_delims, |
38997 | 237 |
known_failures, default_max_relevant, explicit_forall, |
238 |
use_conjecture_for_hypotheses} |
|
38455 | 239 |
({debug, verbose, overlord, full_types, explicit_apply, |
38998 | 240 |
max_relevant, isar_proof, isar_shrink_factor, timeout, ...} : params) |
39366
f58fbb959826
handle relevance filter corner cases more gracefully;
blanchet
parents:
39364
diff
changeset
|
241 |
minimize_command ({state, goal, subgoal, axioms, only} : problem) = |
38023 | 242 |
let |
39318 | 243 |
val ctxt = Proof.context_of state |
38998 | 244 |
val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal |
39366
f58fbb959826
handle relevance filter corner cases more gracefully;
blanchet
parents:
39364
diff
changeset
|
245 |
val axioms = axioms |> not only |
f58fbb959826
handle relevance filter corner cases more gracefully;
blanchet
parents:
39364
diff
changeset
|
246 |
? take (the_default default_max_relevant max_relevant) |
38023 | 247 |
val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER" |
38998 | 248 |
else Config.get ctxt dest_dir |
249 |
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
|
250 |
val problem_file_name = |
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset
|
251 |
Path.basic ((if overlord then "prob_" ^ atp_name |
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset
|
252 |
else the_problem_prefix ^ serial_string ()) |
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset
|
253 |
^ "_" ^ string_of_int subgoal) |
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset
|
254 |
val problem_path_name = |
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset
|
255 |
if the_dest_dir = "" then |
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset
|
256 |
File.tmp_path problem_file_name |
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset
|
257 |
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
|
258 |
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
|
259 |
else |
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset
|
260 |
error ("No such directory: " ^ quote the_dest_dir ^ ".") |
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset
|
261 |
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
|
262 |
val command = Path.explode (getenv (fst exec) ^ "/" ^ snd exec) |
38023 | 263 |
(* write out problem file and call prover *) |
38645 | 264 |
fun command_line complete timeout probfile = |
38023 | 265 |
let |
266 |
val core = File.shell_path command ^ " " ^ arguments complete timeout ^ |
|
267 |
" " ^ File.shell_path probfile |
|
268 |
in |
|
39010 | 269 |
(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
|
270 |
else "exec " ^ core) ^ " 2>&1" |
38023 | 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 |
|
39318 | 290 |
fun 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) |
|
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38741
diff
changeset
|
299 |
|>> (if measure_run_time then split_time else rpair 0) |
39452 | 300 |
val (tstplike_proof, outcome) = |
301 |
extract_tstplike_proof_and_outcome complete res_code |
|
302 |
proof_delims known_failures output |
|
303 |
in (output, msecs, tstplike_proof, outcome) end |
|
38032 | 304 |
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
|
305 |
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
|
306 |
prepare_problem ctxt readable_names explicit_forall full_types |
39005 | 307 |
explicit_apply hyp_ts concl_t axioms |
39452 | 308 |
val ss = tptp_strings_for_atp_problem use_conjecture_for_hypotheses |
309 |
problem |
|
38631
979a0b37f981
prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible;
blanchet
parents:
38600
diff
changeset
|
310 |
val _ = File.write_list probfile ss |
38032 | 311 |
val conjecture_shape = |
312 |
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
|
313 |
|> map single |
39318 | 314 |
val run_twice = has_incomplete_mode andalso not auto |
38645 | 315 |
val timer = Timer.startRealTimer () |
38032 | 316 |
val result = |
39318 | 317 |
run false (if run_twice then |
318 |
Time.fromMilliseconds |
|
38645 | 319 |
(2 * Time.toMilliseconds timeout div 3) |
39318 | 320 |
else |
321 |
timeout) |
|
322 |
|> run_twice |
|
38645 | 323 |
? (fn (_, msecs0, _, SOME _) => |
39318 | 324 |
run true (Time.- (timeout, Timer.checkRealTimer timer)) |
39452 | 325 |
|> (fn (output, msecs, tstplike_proof, outcome) => |
326 |
(output, msecs0 + msecs, tstplike_proof, outcome)) |
|
38645 | 327 |
| result => result) |
38282
319c59682c51
move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38277
diff
changeset
|
328 |
in ((pool, conjecture_shape, axiom_names), result) end |
38032 | 329 |
else |
330 |
error ("Bad executable: " ^ Path.implode command ^ ".") |
|
38023 | 331 |
|
332 |
(* If the problem file has not been exported, remove it; otherwise, export |
|
333 |
the proof file too. *) |
|
334 |
fun cleanup probfile = |
|
335 |
if the_dest_dir = "" then try File.rm probfile else NONE |
|
336 |
fun export probfile (_, (output, _, _, _)) = |
|
337 |
if the_dest_dir = "" then |
|
338 |
() |
|
339 |
else |
|
340 |
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
|
341 |
val ((pool, conjecture_shape, axiom_names), |
39452 | 342 |
(output, msecs, tstplike_proof, outcome)) = |
39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset
|
343 |
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
|
344 |
val (conjecture_shape, axiom_names) = |
38023 | 345 |
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
|
346 |
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
|
347 |
val important_message = extract_important_message output |
39327 | 348 |
val banner = if auto then "Sledgehammer found a proof" |
349 |
else "Try this command" |
|
38023 | 350 |
val (message, used_thm_names) = |
351 |
case outcome of |
|
352 |
NONE => |
|
353 |
proof_text isar_proof |
|
354 |
(pool, debug, isar_shrink_factor, ctxt, conjecture_shape) |
|
39452 | 355 |
(banner, full_types, minimize_command, tstplike_proof, axiom_names, |
356 |
goal, subgoal) |
|
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38741
diff
changeset
|
357 |
|>> (fn message => |
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38741
diff
changeset
|
358 |
message ^ (if verbose then |
39371 | 359 |
"\nATP real CPU time: " ^ string_of_int msecs ^ |
360 |
" ms." |
|
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38741
diff
changeset
|
361 |
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
|
362 |
"") ^ |
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
|
363 |
(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
|
364 |
"\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
|
365 |
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
|
366 |
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
|
367 |
"")) |
38597
db482afec7f0
no spurious trailing "\n" at the end of Sledgehammer's output
blanchet
parents:
38590
diff
changeset
|
368 |
| SOME failure => (string_for_failure failure, []) |
38023 | 369 |
in |
370 |
{outcome = outcome, message = message, pool = pool, |
|
371 |
used_thm_names = used_thm_names, atp_run_time_in_msecs = msecs, |
|
39452 | 372 |
output = output, tstplike_proof = tstplike_proof, |
373 |
axiom_names = axiom_names, conjecture_shape = conjecture_shape} |
|
38023 | 374 |
end |
375 |
||
39318 | 376 |
fun get_prover_fun thy name = prover_fun false name (get_prover thy name) |
38023 | 377 |
|
39453
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for one-liners as for Isar proofs
blanchet
parents:
39452
diff
changeset
|
378 |
fun run_prover (params as {blocking, debug, verbose, max_relevant, timeout, |
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for one-liners as for Isar proofs
blanchet
parents:
39452
diff
changeset
|
379 |
expect, ...}) |
39338 | 380 |
auto i n minimize_command (problem as {state, goal, axioms, ...}) |
39110
a74bd9bfa880
show the number of facts for each prover in "verbose" mode
blanchet
parents:
39108
diff
changeset
|
381 |
(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
|
382 |
let |
39318 | 383 |
val ctxt = Proof.context_of state |
37584 | 384 |
val birth_time = Time.now () |
385 |
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
|
386 |
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
|
387 |
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
|
388 |
val desc = |
39110
a74bd9bfa880
show the number of facts for each prover in "verbose" mode
blanchet
parents:
39108
diff
changeset
|
389 |
"ATP " ^ quote atp_name ^ |
a74bd9bfa880
show the number of facts for each prover in "verbose" mode
blanchet
parents:
39108
diff
changeset
|
390 |
(if verbose then |
a74bd9bfa880
show the number of facts for each prover in "verbose" mode
blanchet
parents:
39108
diff
changeset
|
391 |
" 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
|
392 |
else |
a74bd9bfa880
show the number of facts for each prover in "verbose" mode
blanchet
parents:
39108
diff
changeset
|
393 |
"") ^ |
a74bd9bfa880
show the number of facts for each prover in "verbose" mode
blanchet
parents:
39108
diff
changeset
|
394 |
" 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
|
395 |
(if blocking then |
162bbbea4e4d
added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents:
38982
diff
changeset
|
396 |
"" |
162bbbea4e4d
added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents:
38982
diff
changeset
|
397 |
else |
162bbbea4e4d
added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents:
38982
diff
changeset
|
398 |
"\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i))) |
39318 | 399 |
fun go () = |
38982
820b8221ed48
added "blocking" option to Sledgehammer to run in synchronous mode;
blanchet
parents:
38893
diff
changeset
|
400 |
let |
39453
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for one-liners as for Isar proofs
blanchet
parents:
39452
diff
changeset
|
401 |
fun really_go () = |
39318 | 402 |
prover_fun auto atp_name prover params (minimize_command atp_name) |
403 |
problem |
|
38985
162bbbea4e4d
added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents:
38982
diff
changeset
|
404 |
|> (fn {outcome, message, ...} => |
162bbbea4e4d
added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents:
38982
diff
changeset
|
405 |
(if is_some outcome then "none" else "some", message)) |
39453
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for one-liners as for Isar proofs
blanchet
parents:
39452
diff
changeset
|
406 |
val (outcome_code, message) = |
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for one-liners as for Isar proofs
blanchet
parents:
39452
diff
changeset
|
407 |
if debug then |
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for one-liners as for Isar proofs
blanchet
parents:
39452
diff
changeset
|
408 |
really_go () |
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for one-liners as for Isar proofs
blanchet
parents:
39452
diff
changeset
|
409 |
else |
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for one-liners as for Isar proofs
blanchet
parents:
39452
diff
changeset
|
410 |
(really_go () |
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for one-liners as for Isar proofs
blanchet
parents:
39452
diff
changeset
|
411 |
handle ERROR message => ("unknown", "Error: " ^ message ^ "\n") |
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for one-liners as for Isar proofs
blanchet
parents:
39452
diff
changeset
|
412 |
| exn => ("unknown", "Internal error:\n" ^ |
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for one-liners as for Isar proofs
blanchet
parents:
39452
diff
changeset
|
413 |
ML_Compiler.exn_message exn ^ "\n")) |
39318 | 414 |
val _ = |
415 |
if expect = "" orelse outcome_code = expect then |
|
416 |
() |
|
417 |
else if blocking then |
|
418 |
error ("Unexpected outcome: " ^ quote outcome_code ^ ".") |
|
419 |
else |
|
420 |
warning ("Unexpected outcome: " ^ quote outcome_code ^ "."); |
|
421 |
in (outcome_code = "some", message) end |
|
422 |
in |
|
423 |
if auto then |
|
424 |
let val (success, message) = TimeLimit.timeLimit timeout go () in |
|
425 |
(success, state |> success ? Proof.goal_message (fn () => |
|
426 |
Pretty.chunks [Pretty.str "", Pretty.mark Markup.hilite |
|
39327 | 427 |
(Pretty.str message)])) |
38982
820b8221ed48
added "blocking" option to Sledgehammer to run in synchronous mode;
blanchet
parents:
38893
diff
changeset
|
428 |
end |
39318 | 429 |
else if blocking then |
430 |
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
|
431 |
List.app priority |
f8292d3020db
use same hack as in "Async_Manager" to work around Proof General bug
blanchet
parents:
39366
diff
changeset
|
432 |
(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
|
433 |
(success, state) |
39318 | 434 |
end |
435 |
else |
|
436 |
(Async_Manager.launch das_Tool birth_time death_time desc (snd o go); |
|
437 |
(false, state)) |
|
37584 | 438 |
end |
28582 | 439 |
|
39318 | 440 |
val auto_max_relevant_divisor = 2 |
441 |
||
39373 | 442 |
fun run_sledgehammer (params as {blocking, atps, full_types, |
38998 | 443 |
relevance_thresholds, max_relevant, ...}) |
39366
f58fbb959826
handle relevance filter corner cases more gracefully;
blanchet
parents:
39364
diff
changeset
|
444 |
auto i (relevance_override as {only, ...}) minimize_command |
f58fbb959826
handle relevance filter corner cases more gracefully;
blanchet
parents:
39364
diff
changeset
|
445 |
state = |
39318 | 446 |
if null atps then |
447 |
error "No ATP is set." |
|
448 |
else case subgoal_count state of |
|
449 |
0 => (priority "No subgoal!"; (false, state)) |
|
450 |
| n => |
|
451 |
let |
|
39364 | 452 |
val _ = Proof.assert_backward state |
39318 | 453 |
val thy = Proof.theory_of state |
454 |
val _ = () |> not blocking ? kill_atps |
|
455 |
val _ = if auto then () else priority "Sledgehammering..." |
|
456 |
val provers = map (`(get_prover thy)) atps |
|
457 |
fun go () = |
|
458 |
let |
|
459 |
val {context = ctxt, facts = chained_ths, goal} = Proof.goal state |
|
460 |
val (_, hyp_ts, concl_t) = strip_subgoal goal i |
|
461 |
val max_max_relevant = |
|
462 |
case max_relevant of |
|
463 |
SOME n => n |
|
464 |
| NONE => |
|
465 |
0 |> fold (Integer.max o #default_max_relevant o fst) provers |
|
466 |
|> auto ? (fn n => n div auto_max_relevant_divisor) |
|
467 |
val axioms = |
|
468 |
relevant_facts ctxt full_types relevance_thresholds |
|
469 |
max_max_relevant relevance_override chained_ths |
|
470 |
hyp_ts concl_t |
|
471 |
val problem = |
|
472 |
{state = state, goal = goal, subgoal = i, |
|
39366
f58fbb959826
handle relevance filter corner cases more gracefully;
blanchet
parents:
39364
diff
changeset
|
473 |
axioms = map (prepare_axiom ctxt) axioms, only = only} |
39338 | 474 |
val run_prover = run_prover params auto i n minimize_command problem |
39318 | 475 |
in |
476 |
if auto then |
|
477 |
fold (fn prover => fn (true, state) => (true, state) |
|
478 |
| (false, _) => run_prover prover) |
|
479 |
provers (false, state) |
|
480 |
else |
|
481 |
(if blocking then Par_List.map else map) run_prover provers |
|
482 |
|> exists fst |> rpair state |
|
483 |
end |
|
484 |
in if blocking then go () else Future.fork (tap go) |> K (false, state) end |
|
38044 | 485 |
|
38023 | 486 |
val setup = |
487 |
dest_dir_setup |
|
488 |
#> problem_prefix_setup |
|
39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset
|
489 |
#> measure_run_time_setup |
38023 | 490 |
|
28582 | 491 |
end; |