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