equal
deleted
inserted
replaced
255 TFree (_, []) => true |
255 TFree (_, []) => true |
256 | TVar (_, []) => true |
256 | TVar (_, []) => true |
257 | _ => false)) |
257 | _ => false)) |
258 |
258 |
259 (* without this test, we would run into problems when atomizing the rules: *) |
259 (* without this test, we would run into problems when atomizing the rules: *) |
260 fun check_topsort iwthms = |
260 fun check_topsort ctxt thm = |
261 if exists (has_topsort o Thm.prop_of o snd o snd) iwthms then |
261 if has_topsort (Thm.prop_of thm) then |
262 raise SMT_Failure.SMT (SMT_Failure.Other_Failure ("proof state " ^ |
262 (SMT_Normalize.drop_fact_warning ctxt thm; TrueI) |
263 "contains the universal sort {}")) |
263 else |
264 else () |
264 thm |
|
265 |
|
266 fun check_topsorts ctxt iwthms = map (apsnd (apsnd (check_topsort ctxt))) iwthms |
265 |
267 |
266 |
268 |
267 (* filter *) |
269 (* filter *) |
268 |
270 |
269 val cnot = Thm.cterm_of @{theory} @{const Not} |
271 val cnot = Thm.cterm_of @{theory} @{const Not} |
275 fun smt_filter_preprocess ctxt facts goal xwthms i = |
277 fun smt_filter_preprocess ctxt facts goal xwthms i = |
276 let |
278 let |
277 val ctxt = |
279 val ctxt = |
278 ctxt |
280 ctxt |
279 |> Config.put SMT_Config.oracle false |
281 |> Config.put SMT_Config.oracle false |
280 |> Config.put SMT_Config.drop_bad_facts true |
|
281 |> Config.put SMT_Config.filter_only_facts true |
282 |> Config.put SMT_Config.filter_only_facts true |
282 |
283 |
283 val ({context=ctxt', prems, concl, ...}, _) = Subgoal.focus ctxt i goal |
284 val ({context=ctxt', prems, concl, ...}, _) = Subgoal.focus ctxt i goal |
284 fun negate ct = Thm.dest_comb ct ||> Thm.apply cnot |-> Thm.apply |
285 fun negate ct = Thm.dest_comb ct ||> Thm.apply cnot |-> Thm.apply |
285 val cprop = |
286 val cprop = |
289 "goal is not a HOL term"))) |
290 "goal is not a HOL term"))) |
290 in |
291 in |
291 map snd xwthms |
292 map snd xwthms |
292 |> map_index I |
293 |> map_index I |
293 |> append (map (pair ~1 o pair NONE) (Thm.assume cprop :: prems @ facts)) |
294 |> append (map (pair ~1 o pair NONE) (Thm.assume cprop :: prems @ facts)) |
294 |> tap check_topsort |
295 |> check_topsorts ctxt' |
295 |> gen_preprocess ctxt' |
296 |> gen_preprocess ctxt' |
296 |> pair (map (apsnd snd) xwthms) |
297 |> pair (map (apsnd snd) xwthms) |
297 end |
298 end |
298 |
299 |
299 fun smt_filter_apply time_limit (xthms, (ithms, ctxt)) = |
300 fun smt_filter_apply time_limit (xthms, (ithms, ctxt)) = |
330 else () |
331 else () |
331 end |
332 end |
332 |
333 |
333 fun solve ctxt iwthms = |
334 fun solve ctxt iwthms = |
334 iwthms |
335 iwthms |
335 |> tap check_topsort |
336 |> check_topsorts ctxt |
336 |> apply_solver ctxt |
337 |> apply_solver ctxt |
337 |>> trace_assumptions ctxt iwthms |
338 |>> trace_assumptions ctxt iwthms |
338 |> snd |
339 |> snd |
339 |
340 |
340 fun str_of ctxt fail = |
341 fun str_of ctxt fail = |