59015
|
1 |
(* Title: HOL/Tools/SMT/cvc4_proof_parse.ML
|
|
2 |
Author: Jasmin Blanchette, TU Muenchen
|
|
3 |
|
|
4 |
CVC4 proof (actually, unsat core) parsing.
|
|
5 |
*)
|
|
6 |
|
|
7 |
signature CVC4_PROOF_PARSE =
|
|
8 |
sig
|
|
9 |
val parse_proof: SMT_Translate.replay_data ->
|
|
10 |
((string * ATP_Problem_Generate.stature) * thm) list -> term list -> term -> string list ->
|
|
11 |
SMT_Solver.parsed_proof
|
|
12 |
end;
|
|
13 |
|
|
14 |
structure CVC4_Proof_Parse: CVC4_PROOF_PARSE =
|
|
15 |
struct
|
|
16 |
|
|
17 |
fun parse_proof ({ll_defs, assms, ...} : SMT_Translate.replay_data) xfacts prems _ output =
|
|
18 |
let
|
|
19 |
val num_ll_defs = length ll_defs
|
|
20 |
|
|
21 |
val id_of_index = Integer.add num_ll_defs
|
|
22 |
val index_of_id = Integer.add (~ num_ll_defs)
|
|
23 |
|
|
24 |
val used_assert_ids = map_filter (try SMTLIB_Interface.assert_index_of_name) output
|
|
25 |
val used_assm_js =
|
|
26 |
map_filter (fn id => let val i = index_of_id id in if i >= 0 then SOME i else NONE end)
|
|
27 |
used_assert_ids
|
|
28 |
|
|
29 |
val conjecture_i = 0
|
|
30 |
val prems_i = conjecture_i + 1
|
|
31 |
val num_prems = length prems
|
|
32 |
val facts_i = prems_i + num_prems
|
|
33 |
|
|
34 |
val fact_ids' =
|
|
35 |
map_filter (fn j =>
|
|
36 |
let val (i, _) = nth assms j in
|
|
37 |
try (apsnd (nth xfacts)) (id_of_index j, i - facts_i)
|
|
38 |
end) used_assm_js
|
|
39 |
in
|
|
40 |
{outcome = NONE, fact_ids = fact_ids', atp_proof = fn () => []}
|
|
41 |
end
|
|
42 |
|
|
43 |
end;
|