13 |
13 |
14 structure CVC4_Proof_Parse: CVC4_PROOF_PARSE = |
14 structure CVC4_Proof_Parse: CVC4_PROOF_PARSE = |
15 struct |
15 struct |
16 |
16 |
17 fun parse_proof ({ll_defs, assms, ...} : SMT_Translate.replay_data) xfacts prems _ output = |
17 fun parse_proof ({ll_defs, assms, ...} : SMT_Translate.replay_data) xfacts prems _ output = |
18 let |
18 if exists (String.isPrefix "(error \"This build of CVC4 doesn't have proof support") output then |
19 val num_ll_defs = length ll_defs |
19 {outcome = NONE, fact_ids = NONE, atp_proof = K []} |
|
20 else |
|
21 let |
|
22 val num_ll_defs = length ll_defs |
20 |
23 |
21 val id_of_index = Integer.add num_ll_defs |
24 val id_of_index = Integer.add num_ll_defs |
22 val index_of_id = Integer.add (~ num_ll_defs) |
25 val index_of_id = Integer.add (~ num_ll_defs) |
23 |
26 |
24 val used_assert_ids = map_filter (try SMTLIB_Interface.assert_index_of_name) output |
27 val used_assert_ids = map_filter (try SMTLIB_Interface.assert_index_of_name) output |
25 val used_assm_js = |
28 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) |
29 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 |
30 used_assert_ids |
28 |
31 |
29 val conjecture_i = 0 |
32 val conjecture_i = 0 |
30 val prems_i = conjecture_i + 1 |
33 val prems_i = conjecture_i + 1 |
31 val num_prems = length prems |
34 val num_prems = length prems |
32 val facts_i = prems_i + num_prems |
35 val facts_i = prems_i + num_prems |
33 |
36 |
34 val fact_ids' = |
37 val fact_ids' = |
35 map_filter (fn j => |
38 map_filter (fn j => |
36 let val (i, _) = nth assms j in |
39 let val (i, _) = nth assms j in |
37 try (apsnd (nth xfacts)) (id_of_index j, i - facts_i) |
40 try (apsnd (nth xfacts)) (id_of_index j, i - facts_i) |
38 end) used_assm_js |
41 end) used_assm_js |
39 in |
42 in |
40 {outcome = NONE, fact_ids = fact_ids', atp_proof = fn () => []} |
43 {outcome = NONE, fact_ids = SOME fact_ids', atp_proof = K []} |
41 end |
44 end |
42 |
45 |
43 end; |
46 end; |