author | blanchet |
Fri, 17 Dec 2010 18:23:56 +0100 | |
changeset 41255 | a80024d7b71b |
parent 41245 | cddc7db22bc9 |
child 41256 | 0e7d45cc005f |
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 |
|
41245 | 15 |
(* for experimentation purposes -- do not use in production code *) |
41255
a80024d7b71b
added debugging option to find out how good the relevance filter was at identifying relevant facts
blanchet
parents:
41245
diff
changeset
|
16 |
val show_facts_in_proofs : bool Unsynchronized.ref |
41245 | 17 |
val smt_weights : bool Unsynchronized.ref |
18 |
val smt_weight_min_facts : int Unsynchronized.ref |
|
19 |
val smt_min_weight : int Unsynchronized.ref |
|
20 |
val smt_max_weight : int Unsynchronized.ref |
|
21 |
val smt_max_weight_index : int Unsynchronized.ref |
|
22 |
val smt_weight_curve : (int -> int) Unsynchronized.ref |
|
23 |
||
38044 | 24 |
val run_sledgehammer : |
39318 | 25 |
params -> bool -> int -> relevance_override -> (string -> minimize_command) |
26 |
-> Proof.state -> bool * Proof.state |
|
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
27 |
end; |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
28 |
|
41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
41066
diff
changeset
|
29 |
structure Sledgehammer_Run : SLEDGEHAMMER_RUN = |
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
30 |
struct |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
31 |
|
38023 | 32 |
open Sledgehammer_Util |
38988 | 33 |
open Sledgehammer_Filter |
40068 | 34 |
open Sledgehammer_ATP_Translate |
41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
41066
diff
changeset
|
35 |
open Sledgehammer_Provers |
41091
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41090
diff
changeset
|
36 |
open Sledgehammer_Minimize |
40072
27f2a45b0aab
more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents:
40071
diff
changeset
|
37 |
|
41208
1b28c43a7074
make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive
blanchet
parents:
41180
diff
changeset
|
38 |
fun prover_description ctxt ({verbose, blocking, ...} : params) name num_facts i |
41089 | 39 |
n goal = |
40 |
quote name ^ |
|
41 |
(if verbose then |
|
42 |
" with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts |
|
43 |
else |
|
44 |
"") ^ |
|
45 |
" on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^ ":" ^ |
|
46 |
(if blocking then |
|
47 |
"" |
|
48 |
else |
|
49 |
"\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i))) |
|
50 |
||
41255
a80024d7b71b
added debugging option to find out how good the relevance filter was at identifying relevant facts
blanchet
parents:
41245
diff
changeset
|
51 |
val show_facts_in_proofs = Unsynchronized.ref false |
a80024d7b71b
added debugging option to find out how good the relevance filter was at identifying relevant facts
blanchet
parents:
41245
diff
changeset
|
52 |
|
41091
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41090
diff
changeset
|
53 |
val implicit_minimization_threshold = 50 |
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41090
diff
changeset
|
54 |
|
41208
1b28c43a7074
make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive
blanchet
parents:
41180
diff
changeset
|
55 |
fun run_prover (params as {debug, blocking, max_relevant, timeout, expect, ...}) |
41089 | 56 |
auto minimize_command only |
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
57 |
{state, goal, subgoal, subgoal_count, facts, smt_head} name = |
41089 | 58 |
let |
59 |
val ctxt = Proof.context_of state |
|
60 |
val birth_time = Time.now () |
|
61 |
val death_time = Time.+ (birth_time, timeout) |
|
62 |
val max_relevant = |
|
63 |
the_default (default_max_relevant_for_prover ctxt name) max_relevant |
|
64 |
val num_facts = length facts |> not only ? Integer.min max_relevant |
|
65 |
val desc = |
|
66 |
prover_description ctxt params name num_facts subgoal subgoal_count goal |
|
67 |
val prover = get_prover ctxt auto name |
|
68 |
val problem = |
|
69 |
{state = state, goal = goal, subgoal = subgoal, |
|
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
70 |
subgoal_count = subgoal_count, facts = take num_facts facts, |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
71 |
smt_head = smt_head} |
41255
a80024d7b71b
added debugging option to find out how good the relevance filter was at identifying relevant facts
blanchet
parents:
41245
diff
changeset
|
72 |
fun really_go () = |
a80024d7b71b
added debugging option to find out how good the relevance filter was at identifying relevant facts
blanchet
parents:
41245
diff
changeset
|
73 |
prover params (minimize_command name) problem |
a80024d7b71b
added debugging option to find out how good the relevance filter was at identifying relevant facts
blanchet
parents:
41245
diff
changeset
|
74 |
|> (fn {outcome, used_facts, message, ...} => |
a80024d7b71b
added debugging option to find out how good the relevance filter was at identifying relevant facts
blanchet
parents:
41245
diff
changeset
|
75 |
if is_some outcome then |
a80024d7b71b
added debugging option to find out how good the relevance filter was at identifying relevant facts
blanchet
parents:
41245
diff
changeset
|
76 |
("none", message) |
a80024d7b71b
added debugging option to find out how good the relevance filter was at identifying relevant facts
blanchet
parents:
41245
diff
changeset
|
77 |
else |
a80024d7b71b
added debugging option to find out how good the relevance filter was at identifying relevant facts
blanchet
parents:
41245
diff
changeset
|
78 |
let |
a80024d7b71b
added debugging option to find out how good the relevance filter was at identifying relevant facts
blanchet
parents:
41245
diff
changeset
|
79 |
val (used_facts, message) = |
a80024d7b71b
added debugging option to find out how good the relevance filter was at identifying relevant facts
blanchet
parents:
41245
diff
changeset
|
80 |
if length used_facts >= implicit_minimization_threshold then |
a80024d7b71b
added debugging option to find out how good the relevance filter was at identifying relevant facts
blanchet
parents:
41245
diff
changeset
|
81 |
minimize_facts params true subgoal subgoal_count state |
a80024d7b71b
added debugging option to find out how good the relevance filter was at identifying relevant facts
blanchet
parents:
41245
diff
changeset
|
82 |
(filter_used_facts used_facts |
a80024d7b71b
added debugging option to find out how good the relevance filter was at identifying relevant facts
blanchet
parents:
41245
diff
changeset
|
83 |
(map (apsnd single o untranslated_fact) facts)) |
a80024d7b71b
added debugging option to find out how good the relevance filter was at identifying relevant facts
blanchet
parents:
41245
diff
changeset
|
84 |
|>> Option.map (map fst) |
a80024d7b71b
added debugging option to find out how good the relevance filter was at identifying relevant facts
blanchet
parents:
41245
diff
changeset
|
85 |
else |
a80024d7b71b
added debugging option to find out how good the relevance filter was at identifying relevant facts
blanchet
parents:
41245
diff
changeset
|
86 |
(SOME used_facts, message) |
a80024d7b71b
added debugging option to find out how good the relevance filter was at identifying relevant facts
blanchet
parents:
41245
diff
changeset
|
87 |
val _ = |
a80024d7b71b
added debugging option to find out how good the relevance filter was at identifying relevant facts
blanchet
parents:
41245
diff
changeset
|
88 |
case (debug orelse !show_facts_in_proofs, used_facts) of |
a80024d7b71b
added debugging option to find out how good the relevance filter was at identifying relevant facts
blanchet
parents:
41245
diff
changeset
|
89 |
(true, SOME (used_facts as _ :: _)) => |
a80024d7b71b
added debugging option to find out how good the relevance filter was at identifying relevant facts
blanchet
parents:
41245
diff
changeset
|
90 |
facts ~~ (0 upto length facts - 1) |
a80024d7b71b
added debugging option to find out how good the relevance filter was at identifying relevant facts
blanchet
parents:
41245
diff
changeset
|
91 |
|> map (fn (fact, j) => |
a80024d7b71b
added debugging option to find out how good the relevance filter was at identifying relevant facts
blanchet
parents:
41245
diff
changeset
|
92 |
fact |> untranslated_fact |> apsnd (K j)) |
a80024d7b71b
added debugging option to find out how good the relevance filter was at identifying relevant facts
blanchet
parents:
41245
diff
changeset
|
93 |
|> filter_used_facts used_facts |
a80024d7b71b
added debugging option to find out how good the relevance filter was at identifying relevant facts
blanchet
parents:
41245
diff
changeset
|
94 |
|> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j) |
a80024d7b71b
added debugging option to find out how good the relevance filter was at identifying relevant facts
blanchet
parents:
41245
diff
changeset
|
95 |
|> commas |
a80024d7b71b
added debugging option to find out how good the relevance filter was at identifying relevant facts
blanchet
parents:
41245
diff
changeset
|
96 |
|> enclose ("Fact" ^ plural_s num_facts ^ " in " ^ |
a80024d7b71b
added debugging option to find out how good the relevance filter was at identifying relevant facts
blanchet
parents:
41245
diff
changeset
|
97 |
quote name ^ " proof (of " ^ |
a80024d7b71b
added debugging option to find out how good the relevance filter was at identifying relevant facts
blanchet
parents:
41245
diff
changeset
|
98 |
string_of_int num_facts ^ "): ") "." |
a80024d7b71b
added debugging option to find out how good the relevance filter was at identifying relevant facts
blanchet
parents:
41245
diff
changeset
|
99 |
|> Output.urgent_message |
a80024d7b71b
added debugging option to find out how good the relevance filter was at identifying relevant facts
blanchet
parents:
41245
diff
changeset
|
100 |
| _ => () |
a80024d7b71b
added debugging option to find out how good the relevance filter was at identifying relevant facts
blanchet
parents:
41245
diff
changeset
|
101 |
in ("some", message) end) |
41089 | 102 |
fun go () = |
103 |
let |
|
104 |
val (outcome_code, message) = |
|
105 |
if debug then |
|
106 |
really_go () |
|
107 |
else |
|
108 |
(really_go () |
|
109 |
handle ERROR message => ("unknown", "Error: " ^ message ^ "\n") |
|
110 |
| exn => |
|
111 |
if Exn.is_interrupt exn then |
|
112 |
reraise exn |
|
113 |
else |
|
114 |
("unknown", "Internal error:\n" ^ |
|
115 |
ML_Compiler.exn_message exn ^ "\n")) |
|
116 |
val _ = |
|
41142
43e2b051339c
weaken the "expect" flag so that it doesn't trigger errors if a prover is not installed
blanchet
parents:
41138
diff
changeset
|
117 |
(* The "expect" argument is deliberately ignored if the prover is |
43e2b051339c
weaken the "expect" flag so that it doesn't trigger errors if a prover is not installed
blanchet
parents:
41138
diff
changeset
|
118 |
missing so that the "Metis_Examples" can be processed on any |
43e2b051339c
weaken the "expect" flag so that it doesn't trigger errors if a prover is not installed
blanchet
parents:
41138
diff
changeset
|
119 |
machine. *) |
43e2b051339c
weaken the "expect" flag so that it doesn't trigger errors if a prover is not installed
blanchet
parents:
41138
diff
changeset
|
120 |
if expect = "" orelse outcome_code = expect orelse |
43e2b051339c
weaken the "expect" flag so that it doesn't trigger errors if a prover is not installed
blanchet
parents:
41138
diff
changeset
|
121 |
not (is_prover_installed ctxt name) then |
41089 | 122 |
() |
123 |
else if blocking then |
|
124 |
error ("Unexpected outcome: " ^ quote outcome_code ^ ".") |
|
125 |
else |
|
126 |
warning ("Unexpected outcome: " ^ quote outcome_code ^ "."); |
|
127 |
in (outcome_code = "some", message) end |
|
128 |
in |
|
129 |
if auto then |
|
130 |
let val (success, message) = TimeLimit.timeLimit timeout go () in |
|
131 |
(success, state |> success ? Proof.goal_message (fn () => |
|
41091
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41090
diff
changeset
|
132 |
Pretty.chunks [Pretty.str "", |
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41090
diff
changeset
|
133 |
Pretty.mark Markup.hilite (Pretty.str message)])) |
41089 | 134 |
end |
135 |
else if blocking then |
|
136 |
let val (success, message) = TimeLimit.timeLimit timeout go () in |
|
137 |
List.app Output.urgent_message |
|
138 |
(Async_Manager.break_into_chunks [desc ^ "\n" ^ message]); |
|
139 |
(success, state) |
|
140 |
end |
|
141 |
else |
|
142 |
(Async_Manager.launch das_Tool birth_time death_time desc (snd o go); |
|
143 |
(false, state)) |
|
144 |
end |
|
145 |
||
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
146 |
val smt_weights = Unsynchronized.ref true |
41245 | 147 |
val smt_weight_min_facts = Unsynchronized.ref 20 |
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
148 |
|
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
149 |
(* FUDGE *) |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
150 |
val smt_min_weight = Unsynchronized.ref 0 |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
151 |
val smt_max_weight = Unsynchronized.ref 10 |
41245 | 152 |
val smt_max_weight_index = Unsynchronized.ref 200 |
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
153 |
val smt_weight_curve = Unsynchronized.ref (fn x : int => x * x) |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
154 |
|
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
155 |
fun smt_fact_weight j num_facts = |
41245 | 156 |
if !smt_weights andalso num_facts >= !smt_weight_min_facts then |
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
157 |
SOME (!smt_max_weight |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
158 |
- (!smt_max_weight - !smt_min_weight + 1) |
41245 | 159 |
* !smt_weight_curve (Int.max (0, !smt_max_weight_index - j - 1)) |
160 |
div !smt_weight_curve (!smt_max_weight_index)) |
|
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
161 |
else |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
162 |
NONE |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
163 |
|
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
164 |
fun weight_smt_fact thy num_facts (fact, j) = |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
165 |
fact |> apsnd (pair (smt_fact_weight j num_facts) o Thm.transfer thy) |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
166 |
|
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
167 |
fun class_of_smt_solver ctxt name = |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
168 |
ctxt |> select_smt_solver name |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
169 |
|> SMT_Config.solver_class_of |> SMT_Utils.string_of_class |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
170 |
|
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
171 |
(* Makes backtraces more transparent and might be more efficient as well. *) |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
172 |
fun smart_par_list_map _ [] = [] |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
173 |
| smart_par_list_map f [x] = [f x] |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
174 |
| smart_par_list_map f xs = Par_List.map f xs |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
175 |
|
40698 | 176 |
(* FUDGE *) |
177 |
val auto_max_relevant_divisor = 2 |
|
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
178 |
|
41208
1b28c43a7074
make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive
blanchet
parents:
41180
diff
changeset
|
179 |
fun run_sledgehammer (params as {debug, blocking, provers, type_sys, |
40069 | 180 |
relevance_thresholds, max_relevant, ...}) |
39366
f58fbb959826
handle relevance filter corner cases more gracefully;
blanchet
parents:
39364
diff
changeset
|
181 |
auto i (relevance_override as {only, ...}) minimize_command |
f58fbb959826
handle relevance filter corner cases more gracefully;
blanchet
parents:
39364
diff
changeset
|
182 |
state = |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
183 |
if null provers then |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
184 |
error "No prover is set." |
39318 | 185 |
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
|
186 |
0 => (Output.urgent_message "No subgoal!"; (false, state)) |
39318 | 187 |
| n => |
188 |
let |
|
39364 | 189 |
val _ = Proof.assert_backward state |
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
190 |
val state = |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
191 |
state |> Proof.map_context (Config.put SMT_Config.verbose debug) |
40200 | 192 |
val ctxt = Proof.context_of state |
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
193 |
val thy = ProofContext.theory_of ctxt |
40200 | 194 |
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
|
195 |
val (_, hyp_ts, concl_t) = strip_subgoal goal i |
41138
eb80538166b6
implemented partially-typed "tags" type encoding
blanchet
parents:
41091
diff
changeset
|
196 |
val no_dangerous_types = types_dangerous_types type_sys |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
197 |
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
|
198 |
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
|
199 |
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
|
200 |
| NONE => () |
40132
7ee65dbffa31
renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
wenzelm
parents:
40114
diff
changeset
|
201 |
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
|
202 |
val (smts, atps) = provers |> List.partition (is_smt_prover ctxt) |
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
203 |
fun run_provers get_facts translate maybe_smt_head provers |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
204 |
(res as (success, state)) = |
40065 | 205 |
if success orelse null provers then |
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
206 |
res |
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
207 |
else |
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
208 |
let |
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
209 |
val facts = get_facts () |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
210 |
val num_facts = length facts |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
211 |
val facts = facts ~~ (0 upto num_facts - 1) |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
212 |
|> map (translate num_facts) |
40062 | 213 |
val problem = |
40065 | 214 |
{state = state, goal = goal, subgoal = i, subgoal_count = n, |
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
215 |
facts = facts, |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
216 |
smt_head = maybe_smt_head (map smt_weighted_fact facts) i} |
40983 | 217 |
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
|
218 |
in |
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
219 |
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
|
220 |
fold (fn prover => fn (true, state) => (true, state) |
40064
db8413d82c3b
got rid of duplicate functionality ("run_smt_solver_somehow");
blanchet
parents:
40063
diff
changeset
|
221 |
| (false, _) => run_prover problem prover) |
40065 | 222 |
provers (false, state) |
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
223 |
else |
41171 | 224 |
provers |
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
225 |
|> (if blocking then smart_par_list_map else map) |
41171 | 226 |
(run_prover problem) |
227 |
|> exists fst |> rpair state |
|
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
228 |
end |
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
229 |
fun get_facts label no_dangerous_types relevance_fudge provers = |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
230 |
let |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
231 |
val max_max_relevant = |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
232 |
case max_relevant of |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
233 |
SOME n => n |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
234 |
| NONE => |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
235 |
0 |> fold (Integer.max o default_max_relevant_for_prover ctxt) |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
236 |
provers |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
237 |
|> auto ? (fn n => n div auto_max_relevant_divisor) |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
238 |
val is_built_in_const = |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
239 |
is_built_in_const_for_prover ctxt (hd provers) |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
240 |
in |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
241 |
relevant_facts ctxt no_dangerous_types relevance_thresholds |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
242 |
max_max_relevant is_built_in_const relevance_fudge |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
243 |
relevance_override chained_ths hyp_ts concl_t |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
244 |
|> tap (fn facts => |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
245 |
if debug then |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
246 |
label ^ plural_s (length provers) ^ ": " ^ |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
247 |
(if null facts then |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
248 |
"Found no relevant facts." |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
249 |
else |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
250 |
"Including (up to) " ^ string_of_int (length facts) ^ |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
251 |
" relevant fact" ^ plural_s (length facts) ^ ":\n" ^ |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
252 |
(facts |> map (fst o fst) |> space_implode " ") ^ ".") |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
253 |
|> Output.urgent_message |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
254 |
else |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
255 |
()) |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
256 |
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
|
257 |
val run_atps = |
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
258 |
run_provers |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
259 |
(get_facts "ATP" no_dangerous_types atp_relevance_fudge o K atps) |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
260 |
(ATP_Translated_Fact oo K (translate_atp_fact ctxt o fst)) |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
261 |
(K (K NONE)) atps |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
262 |
fun run_smts (accum as (success, _)) = |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
263 |
if success orelse null smts then |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
264 |
accum |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
265 |
else |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
266 |
let |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
267 |
val facts = get_facts "SMT solver" true smt_relevance_fudge smts |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
268 |
val translate = SMT_Weighted_Fact oo weight_smt_fact thy |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
269 |
val maybe_smt_head = try o SMT_Solver.smt_filter_head state |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
270 |
in |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
271 |
smts |> map (`(class_of_smt_solver ctxt)) |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
272 |
|> AList.group (op =) |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
273 |
|> map (fn (_, smts) => run_provers (K facts) translate |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
274 |
maybe_smt_head smts accum) |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
275 |
|> exists fst |> rpair state |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
276 |
end |
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
277 |
fun run_atps_and_smt_solvers () = |
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
278 |
[run_atps, run_smts] |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
279 |
|> smart_par_list_map (fn f => f (false, state) |> K ()) |
41180
a99bc6f3664b
make sure errors generated in a thread don't vanish in cyberspace (e.g., when invoking Sledgehammer with unknown facts)
blanchet
parents:
41171
diff
changeset
|
280 |
handle ERROR msg => (Output.urgent_message ("Error: " ^ msg); error msg) |
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
281 |
in |
40065 | 282 |
(false, state) |
283 |
|> (if blocking then run_atps #> not auto ? run_smts |
|
284 |
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
|
285 |
end |
38044 | 286 |
|
28582 | 287 |
end; |