55205
|
1 |
(* Title: HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
|
|
2 |
Author: Fabian Immler, TU Muenchen
|
|
3 |
Author: Makarius
|
|
4 |
Author: Jasmin Blanchette, TU Muenchen
|
|
5 |
|
|
6 |
SMT solvers as Sledgehammer provers.
|
|
7 |
*)
|
|
8 |
|
|
9 |
signature SLEDGEHAMMER_PROVER_SMT =
|
|
10 |
sig
|
|
11 |
type stature = ATP_Problem_Generate.stature
|
|
12 |
type mode = Sledgehammer_Prover.mode
|
|
13 |
type prover = Sledgehammer_Prover.prover
|
|
14 |
|
|
15 |
val smt_builtins : bool Config.T
|
|
16 |
val smt_triggers : bool Config.T
|
|
17 |
val smt_weights : bool Config.T
|
|
18 |
val smt_weight_min_facts : int Config.T
|
|
19 |
val smt_min_weight : int Config.T
|
|
20 |
val smt_max_weight : int Config.T
|
|
21 |
val smt_max_weight_index : int Config.T
|
|
22 |
val smt_weight_curve : (int -> int) Unsynchronized.ref
|
|
23 |
val smt_max_slices : int Config.T
|
|
24 |
val smt_slice_fact_frac : real Config.T
|
|
25 |
val smt_slice_time_frac : real Config.T
|
|
26 |
val smt_slice_min_secs : int Config.T
|
|
27 |
|
|
28 |
val is_smt_prover : Proof.context -> string -> bool
|
|
29 |
val run_smt_solver : mode -> string -> prover
|
|
30 |
end;
|
|
31 |
|
|
32 |
structure Sledgehammer_Prover_SMT : SLEDGEHAMMER_PROVER_SMT =
|
|
33 |
struct
|
|
34 |
|
55212
|
35 |
open ATP_Util
|
55205
|
36 |
open ATP_Proof
|
|
37 |
open ATP_Systems
|
|
38 |
open ATP_Problem_Generate
|
|
39 |
open ATP_Proof_Reconstruct
|
|
40 |
open Sledgehammer_Util
|
|
41 |
open Sledgehammer_Reconstructor
|
|
42 |
open Sledgehammer_Prover
|
|
43 |
|
|
44 |
val smt_builtins = Attrib.setup_config_bool @{binding sledgehammer_smt_builtins} (K true)
|
|
45 |
val smt_triggers = Attrib.setup_config_bool @{binding sledgehammer_smt_triggers} (K true)
|
|
46 |
val smt_weights = Attrib.setup_config_bool @{binding sledgehammer_smt_weights} (K true)
|
|
47 |
val smt_weight_min_facts =
|
|
48 |
Attrib.setup_config_int @{binding sledgehammer_smt_weight_min_facts} (K 20)
|
|
49 |
|
|
50 |
fun is_smt_prover ctxt = member (op =) (SMT_Solver.available_solvers_of ctxt)
|
|
51 |
|
|
52 |
(* FUDGE *)
|
55212
|
53 |
val smt_min_weight = Attrib.setup_config_int @{binding sledgehammer_smt_min_weight} (K 0)
|
|
54 |
val smt_max_weight = Attrib.setup_config_int @{binding sledgehammer_smt_max_weight} (K 10)
|
55205
|
55 |
val smt_max_weight_index =
|
|
56 |
Attrib.setup_config_int @{binding sledgehammer_smt_max_weight_index} (K 200)
|
|
57 |
val smt_weight_curve = Unsynchronized.ref (fn x : int => x * x)
|
|
58 |
|
|
59 |
fun smt_fact_weight ctxt j num_facts =
|
55212
|
60 |
if Config.get ctxt smt_weights andalso num_facts >= Config.get ctxt smt_weight_min_facts then
|
55205
|
61 |
let
|
|
62 |
val min = Config.get ctxt smt_min_weight
|
|
63 |
val max = Config.get ctxt smt_max_weight
|
|
64 |
val max_index = Config.get ctxt smt_max_weight_index
|
|
65 |
val curve = !smt_weight_curve
|
|
66 |
in
|
55212
|
67 |
SOME (max - (max - min + 1) * curve (Int.max (0, max_index - j - 1)) div curve max_index)
|
55205
|
68 |
end
|
|
69 |
else
|
|
70 |
NONE
|
|
71 |
|
|
72 |
fun weight_smt_fact ctxt num_facts ((info, th), j) =
|
|
73 |
let val thy = Proof_Context.theory_of ctxt in
|
|
74 |
(info, (smt_fact_weight ctxt j num_facts, th |> Thm.transfer thy))
|
|
75 |
end
|
|
76 |
|
|
77 |
(* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until these are sorted out
|
|
78 |
properly in the SMT module, we must interpret these here. *)
|
|
79 |
val z3_failures =
|
|
80 |
[(101, OutOfResources),
|
|
81 |
(103, MalformedInput),
|
|
82 |
(110, MalformedInput),
|
|
83 |
(112, TimedOut)]
|
|
84 |
val unix_failures =
|
|
85 |
[(138, Crashed),
|
|
86 |
(139, Crashed)]
|
|
87 |
val smt_failures = z3_failures @ unix_failures
|
|
88 |
|
|
89 |
fun failure_of_smt_failure (SMT_Failure.Counterexample {is_real_cex, ...}) =
|
|
90 |
if is_real_cex then Unprovable else GaveUp
|
|
91 |
| failure_of_smt_failure SMT_Failure.Time_Out = TimedOut
|
|
92 |
| failure_of_smt_failure (SMT_Failure.Abnormal_Termination code) =
|
|
93 |
(case AList.lookup (op =) smt_failures code of
|
|
94 |
SOME failure => failure
|
|
95 |
| NONE => UnknownError ("Abnormal termination with exit code " ^ string_of_int code ^ "."))
|
|
96 |
| failure_of_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources
|
|
97 |
| failure_of_smt_failure (SMT_Failure.Other_Failure s) = UnknownError s
|
|
98 |
|
|
99 |
(* FUDGE *)
|
|
100 |
val smt_max_slices = Attrib.setup_config_int @{binding sledgehammer_smt_max_slices} (K 8)
|
|
101 |
val smt_slice_fact_frac =
|
|
102 |
Attrib.setup_config_real @{binding sledgehammer_smt_slice_fact_frac} (K 0.667)
|
|
103 |
val smt_slice_time_frac =
|
|
104 |
Attrib.setup_config_real @{binding sledgehammer_smt_slice_time_frac} (K 0.333)
|
|
105 |
val smt_slice_min_secs = Attrib.setup_config_int @{binding sledgehammer_smt_slice_min_secs} (K 3)
|
|
106 |
|
|
107 |
val is_boring_builtin_typ =
|
|
108 |
not o exists_subtype (member (op =) [@{typ nat}, @{typ int}, HOLogic.realT])
|
|
109 |
|
|
110 |
fun smt_filter_loop name ({debug, overlord, max_mono_iters, max_new_mono_instances, timeout, slice,
|
|
111 |
...} : params) state goal i =
|
|
112 |
let
|
|
113 |
fun repair_context ctxt =
|
55212
|
114 |
ctxt |> Context.proof_map (SMT_Config.select_solver name)
|
55205
|
115 |
|> Config.put SMT_Config.verbose debug
|
|
116 |
|> (if overlord then
|
|
117 |
Config.put SMT_Config.debug_files
|
|
118 |
(overlord_file_location_of_prover name |> (fn (path, name) => path ^ "/" ^ name))
|
|
119 |
else
|
|
120 |
I)
|
|
121 |
|> Config.put SMT_Config.infer_triggers (Config.get ctxt smt_triggers)
|
|
122 |
|> not (Config.get ctxt smt_builtins)
|
|
123 |
? (SMT_Builtin.filter_builtins is_boring_builtin_typ
|
|
124 |
#> Config.put SMT_Config.datatypes false)
|
|
125 |
|> repair_monomorph_context max_mono_iters default_max_mono_iters max_new_mono_instances
|
|
126 |
default_max_new_mono_instances
|
|
127 |
|
|
128 |
val state = Proof.map_context (repair_context) state
|
|
129 |
val ctxt = Proof.context_of state
|
|
130 |
val max_slices = if slice then Config.get ctxt smt_max_slices else 1
|
|
131 |
|
|
132 |
fun do_slice timeout slice outcome0 time_so_far
|
55212
|
133 |
(weighted_factss as (fact_filter, weighted_facts) :: _) =
|
55205
|
134 |
let
|
|
135 |
val timer = Timer.startRealTimer ()
|
|
136 |
val slice_timeout =
|
|
137 |
if slice < max_slices then
|
|
138 |
let val ms = Time.toMilliseconds timeout in
|
|
139 |
Int.min (ms, Int.max (1000 * Config.get ctxt smt_slice_min_secs,
|
|
140 |
Real.ceil (Config.get ctxt smt_slice_time_frac * Real.fromInt ms)))
|
|
141 |
|> Time.fromMilliseconds
|
|
142 |
end
|
|
143 |
else
|
|
144 |
timeout
|
|
145 |
val num_facts = length weighted_facts
|
|
146 |
val _ =
|
|
147 |
if debug then
|
|
148 |
quote name ^ " slice " ^ string_of_int slice ^ " with " ^ string_of_int num_facts ^
|
|
149 |
" fact" ^ plural_s num_facts ^ " for " ^ string_of_time slice_timeout
|
|
150 |
|> Output.urgent_message
|
|
151 |
else
|
|
152 |
()
|
|
153 |
val birth = Timer.checkRealTimer timer
|
|
154 |
val _ = if debug then Output.urgent_message "Invoking SMT solver..." else ()
|
|
155 |
|
|
156 |
val (outcome, used_facts) =
|
|
157 |
SMT_Solver.smt_filter_preprocess ctxt [] goal weighted_facts i
|
|
158 |
|> SMT_Solver.smt_filter_apply slice_timeout
|
|
159 |
|> (fn {outcome, used_facts} => (outcome, used_facts))
|
|
160 |
handle exn =>
|
|
161 |
if Exn.is_interrupt exn then reraise exn
|
|
162 |
else (ML_Compiler.exn_message exn |> SMT_Failure.Other_Failure |> SOME, [])
|
|
163 |
|
|
164 |
val death = Timer.checkRealTimer timer
|
|
165 |
val outcome0 = if is_none outcome0 then SOME outcome else outcome0
|
|
166 |
val time_so_far = Time.+ (time_so_far, Time.- (death, birth))
|
|
167 |
|
|
168 |
val too_many_facts_perhaps =
|
|
169 |
(case outcome of
|
|
170 |
NONE => false
|
|
171 |
| SOME (SMT_Failure.Counterexample _) => false
|
|
172 |
| SOME SMT_Failure.Time_Out => slice_timeout <> timeout
|
|
173 |
| SOME (SMT_Failure.Abnormal_Termination _) => true (* kind of *)
|
|
174 |
| SOME SMT_Failure.Out_Of_Memory => true
|
|
175 |
| SOME (SMT_Failure.Other_Failure _) => true)
|
|
176 |
|
|
177 |
val timeout = Time.- (timeout, Timer.checkRealTimer timer)
|
|
178 |
in
|
|
179 |
if too_many_facts_perhaps andalso slice < max_slices andalso num_facts > 0 andalso
|
|
180 |
Time.> (timeout, Time.zeroTime) then
|
|
181 |
let
|
|
182 |
val new_num_facts =
|
|
183 |
Real.ceil (Config.get ctxt smt_slice_fact_frac * Real.fromInt num_facts)
|
|
184 |
val weighted_factss as (new_fact_filter, _) :: _ =
|
|
185 |
weighted_factss
|
|
186 |
|> (fn (x :: xs) => xs @ [x])
|
|
187 |
|> app_hd (apsnd (take new_num_facts))
|
|
188 |
val show_filter = fact_filter <> new_fact_filter
|
|
189 |
|
|
190 |
fun num_of_facts fact_filter num_facts =
|
|
191 |
string_of_int num_facts ^ (if show_filter then " " ^ quote fact_filter else "") ^
|
|
192 |
" fact" ^ plural_s num_facts
|
|
193 |
|
|
194 |
val _ =
|
|
195 |
if debug then
|
|
196 |
quote name ^ " invoked with " ^
|
|
197 |
num_of_facts fact_filter num_facts ^ ": " ^
|
|
198 |
string_of_atp_failure (failure_of_smt_failure (the outcome)) ^
|
|
199 |
" Retrying with " ^ num_of_facts new_fact_filter new_num_facts ^
|
|
200 |
"..."
|
|
201 |
|> Output.urgent_message
|
|
202 |
else
|
|
203 |
()
|
|
204 |
in
|
|
205 |
do_slice timeout (slice + 1) outcome0 time_so_far weighted_factss
|
|
206 |
end
|
|
207 |
else
|
|
208 |
{outcome = if is_none outcome then NONE else the outcome0, used_facts = used_facts,
|
|
209 |
used_from = map (apsnd snd) weighted_facts, run_time = time_so_far}
|
|
210 |
end
|
|
211 |
in
|
|
212 |
do_slice timeout 1 NONE Time.zeroTime
|
|
213 |
end
|
|
214 |
|
|
215 |
fun run_smt_solver mode name (params as {debug, verbose, preplay_timeout, ...}) minimize_command
|
|
216 |
({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
|
|
217 |
let
|
|
218 |
val thy = Proof.theory_of state
|
|
219 |
val ctxt = Proof.context_of state
|
|
220 |
|
|
221 |
fun weight_facts facts =
|
|
222 |
let val num_facts = length facts in
|
|
223 |
map (weight_smt_fact ctxt num_facts) (facts ~~ (0 upto num_facts - 1))
|
|
224 |
end
|
|
225 |
|
|
226 |
val weighted_factss = factss |> map (apsnd weight_facts)
|
|
227 |
val {outcome, used_facts = used_pairs, used_from, run_time} =
|
|
228 |
smt_filter_loop name params state goal subgoal weighted_factss
|
|
229 |
val used_facts = used_pairs |> map fst
|
|
230 |
val outcome = outcome |> Option.map failure_of_smt_failure
|
|
231 |
|
|
232 |
val (preplay, message, message_tail) =
|
|
233 |
(case outcome of
|
|
234 |
NONE =>
|
|
235 |
(Lazy.lazy (fn () =>
|
55285
|
236 |
play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal
|
|
237 |
SMT_Method (bunch_of_proof_methods false liftingN)),
|
55205
|
238 |
fn preplay =>
|
|
239 |
let
|
|
240 |
val one_line_params =
|
|
241 |
(preplay, proof_banner mode name, used_facts,
|
|
242 |
choose_minimize_command thy params minimize_command name preplay, subgoal,
|
|
243 |
subgoal_count)
|
|
244 |
val num_chained = length (#facts (Proof.goal state))
|
|
245 |
in
|
|
246 |
one_line_proof_text num_chained one_line_params
|
|
247 |
end,
|
|
248 |
if verbose then "\nSMT solver real CPU time: " ^ string_of_time run_time ^ "." else "")
|
|
249 |
| SOME failure =>
|
55285
|
250 |
(Lazy.value (Metis_Method (NONE, NONE), Play_Failed),
|
|
251 |
fn _ => string_of_atp_failure failure, ""))
|
55205
|
252 |
in
|
55212
|
253 |
{outcome = outcome, used_facts = used_facts, used_from = used_from, run_time = run_time,
|
|
254 |
preplay = preplay, message = message, message_tail = message_tail}
|
55205
|
255 |
end
|
|
256 |
|
|
257 |
end;
|