author | blanchet |
Wed, 08 Dec 2010 22:17:52 +0100 | |
changeset 41088 | 54eb8e7c7f9b |
parent 41087 | d7b5fd465198 |
child 41089 | 2e69fb6331cb |
permissions | -rw-r--r-- |
41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
41066
diff
changeset
|
1 |
(* Title: HOL/Tools/Sledgehammer/sledgehammer_run.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 |
|
41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
41066
diff
changeset
|
9 |
signature SLEDGEHAMMER_RUN = |
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
10 |
sig |
38988 | 11 |
type relevance_override = Sledgehammer_Filter.relevance_override |
40068 | 12 |
type minimize_command = Sledgehammer_ATP_Reconstruct.minimize_command |
41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
41066
diff
changeset
|
13 |
type params = Sledgehammer_Provers.params |
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
14 |
|
38044 | 15 |
val run_sledgehammer : |
39318 | 16 |
params -> bool -> int -> relevance_override -> (string -> minimize_command) |
17 |
-> Proof.state -> bool * Proof.state |
|
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
18 |
end; |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
19 |
|
41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
41066
diff
changeset
|
20 |
structure Sledgehammer_Run : SLEDGEHAMMER_RUN = |
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
21 |
struct |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
22 |
|
38023 | 23 |
open Sledgehammer_Util |
38988 | 24 |
open Sledgehammer_Filter |
40068 | 25 |
open Sledgehammer_ATP_Translate |
41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
41066
diff
changeset
|
26 |
open Sledgehammer_Provers |
40072
27f2a45b0aab
more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents:
40071
diff
changeset
|
27 |
|
40698 | 28 |
(* FUDGE *) |
29 |
val auto_max_relevant_divisor = 2 |
|
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
30 |
|
40205
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset
|
31 |
fun fact_name (Untranslated ((name, _), _)) = SOME name |
41088 | 32 |
| fact_name (ATP_Translated (_, p)) = Option.map (fst o fst) p |
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
33 |
|
40205
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset
|
34 |
fun run_sledgehammer (params as {blocking, debug, provers, full_types, |
40069 | 35 |
relevance_thresholds, max_relevant, ...}) |
39366
f58fbb959826
handle relevance filter corner cases more gracefully;
blanchet
parents:
39364
diff
changeset
|
36 |
auto i (relevance_override as {only, ...}) minimize_command |
f58fbb959826
handle relevance filter corner cases more gracefully;
blanchet
parents:
39364
diff
changeset
|
37 |
state = |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
38 |
if null provers then |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
39 |
error "No prover is set." |
39318 | 40 |
else case subgoal_count state of |
40132
7ee65dbffa31
renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
wenzelm
parents:
40114
diff
changeset
|
41 |
0 => (Output.urgent_message "No subgoal!"; (false, state)) |
39318 | 42 |
| n => |
43 |
let |
|
39364 | 44 |
val _ = Proof.assert_backward state |
40200 | 45 |
val ctxt = Proof.context_of state |
46 |
val {facts = chained_ths, goal, ...} = Proof.goal state |
|
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
47 |
val (_, hyp_ts, concl_t) = strip_subgoal goal i |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
48 |
val _ = () |> not blocking ? kill_provers |
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
49 |
val _ = case find_first (not o is_prover_available ctxt) provers of |
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
50 |
SOME name => error ("No such prover: " ^ name ^ ".") |
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
51 |
| NONE => () |
40132
7ee65dbffa31
renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
wenzelm
parents:
40114
diff
changeset
|
52 |
val _ = if auto then () else Output.urgent_message "Sledgehammering..." |
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
53 |
val (smts, atps) = provers |> List.partition (is_smt_prover ctxt) |
40369
53dca3bd4250
use the SMT integration's official list of built-ins
blanchet
parents:
40341
diff
changeset
|
54 |
fun run_provers label full_types relevance_fudge maybe_translate provers |
53dca3bd4250
use the SMT integration's official list of built-ins
blanchet
parents:
40341
diff
changeset
|
55 |
(res as (success, state)) = |
40065 | 56 |
if success orelse null provers then |
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
57 |
res |
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
58 |
else |
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
59 |
let |
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
60 |
val max_max_relevant = |
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
61 |
case max_relevant of |
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
62 |
SOME n => n |
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
63 |
| NONE => |
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
64 |
0 |> fold (Integer.max o default_max_relevant_for_prover ctxt) |
40065 | 65 |
provers |
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
66 |
|> auto ? (fn n => n div auto_max_relevant_divisor) |
40369
53dca3bd4250
use the SMT integration's official list of built-ins
blanchet
parents:
40341
diff
changeset
|
67 |
val is_built_in_const = |
53dca3bd4250
use the SMT integration's official list of built-ins
blanchet
parents:
40341
diff
changeset
|
68 |
is_built_in_const_for_prover ctxt (hd provers) |
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents:
40202
diff
changeset
|
69 |
val facts = |
40065 | 70 |
relevant_facts ctxt full_types relevance_thresholds |
40369
53dca3bd4250
use the SMT integration's official list of built-ins
blanchet
parents:
40341
diff
changeset
|
71 |
max_max_relevant is_built_in_const relevance_fudge |
40071
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset
|
72 |
relevance_override chained_ths hyp_ts concl_t |
40114 | 73 |
|> map maybe_translate |
40062 | 74 |
val problem = |
40065 | 75 |
{state = state, goal = goal, subgoal = i, subgoal_count = n, |
40983 | 76 |
facts = facts} |
77 |
val run_prover = run_prover params auto minimize_command only |
|
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
78 |
in |
40205
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset
|
79 |
if debug then |
40370 | 80 |
Output.urgent_message (label ^ plural_s (length provers) ^ ": " ^ |
40205
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset
|
81 |
(if null facts then |
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset
|
82 |
"Found no relevant facts." |
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset
|
83 |
else |
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset
|
84 |
"Including (up to) " ^ string_of_int (length facts) ^ |
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset
|
85 |
" relevant fact" ^ plural_s (length facts) ^ ":\n" ^ |
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset
|
86 |
(facts |> map_filter fact_name |
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset
|
87 |
|> space_implode " ") ^ ".")) |
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset
|
88 |
else |
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset
|
89 |
(); |
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
90 |
if auto then |
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
91 |
fold (fn prover => fn (true, state) => (true, state) |
40064
db8413d82c3b
got rid of duplicate functionality ("run_smt_solver_somehow");
blanchet
parents:
40063
diff
changeset
|
92 |
| (false, _) => run_prover problem prover) |
40065 | 93 |
provers (false, state) |
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
94 |
else |
40065 | 95 |
provers |> (if blocking then Par_List.map else map) |
96 |
(run_prover problem) |
|
97 |
|> exists fst |> rpair state |
|
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
98 |
end |
40071
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset
|
99 |
val run_atps = |
40370 | 100 |
run_provers "ATP" full_types atp_relevance_fudge |
41088 | 101 |
(ATP_Translated o translate_atp_fact ctxt) atps |
40071
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset
|
102 |
val run_smts = |
40370 | 103 |
run_provers "SMT solver" true smt_relevance_fudge Untranslated smts |
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
104 |
fun run_atps_and_smt_solvers () = |
40065 | 105 |
[run_atps, run_smts] |> Par_List.map (fn f => f (false, state) |> K ()) |
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
106 |
in |
40065 | 107 |
(false, state) |
108 |
|> (if blocking then run_atps #> not auto ? run_smts |
|
109 |
else (fn p => Future.fork (tap run_atps_and_smt_solvers) |> K p)) |
|
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
110 |
end |
38044 | 111 |
|
28582 | 112 |
end; |