src/HOL/Tools/SMT/cvc4_proof_parse.ML
author wenzelm
Sun Nov 26 21:08:32 2017 +0100 (18 months ago)
changeset 67091 1393c2340eec
parent 60201 90e88e521e0e
permissions -rw-r--r--
more symbols;
blanchet@59015
     1
(*  Title:      HOL/Tools/SMT/cvc4_proof_parse.ML
blanchet@59015
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@59015
     3
blanchet@59015
     4
CVC4 proof (actually, unsat core) parsing.
blanchet@59015
     5
*)
blanchet@59015
     6
blanchet@59015
     7
signature CVC4_PROOF_PARSE =
blanchet@59015
     8
sig
blanchet@59015
     9
  val parse_proof: SMT_Translate.replay_data ->
blanchet@59015
    10
    ((string * ATP_Problem_Generate.stature) * thm) list -> term list -> term -> string list ->
blanchet@59015
    11
    SMT_Solver.parsed_proof
blanchet@59015
    12
end;
blanchet@59015
    13
blanchet@59015
    14
structure CVC4_Proof_Parse: CVC4_PROOF_PARSE =
blanchet@59015
    15
struct
blanchet@59015
    16
blanchet@59015
    17
fun parse_proof ({ll_defs, assms, ...} : SMT_Translate.replay_data) xfacts prems _ output =
blanchet@60201
    18
  if exists (String.isPrefix "(error \"This build of CVC4 doesn't have proof support") output then
blanchet@60201
    19
    {outcome = NONE, fact_ids = NONE, atp_proof = K []}
blanchet@60201
    20
  else
blanchet@60201
    21
    let
blanchet@60201
    22
      val num_ll_defs = length ll_defs
blanchet@59015
    23
blanchet@60201
    24
      val id_of_index = Integer.add num_ll_defs
blanchet@60201
    25
      val index_of_id = Integer.add (~ num_ll_defs)
blanchet@59015
    26
blanchet@60201
    27
      val used_assert_ids = map_filter (try SMTLIB_Interface.assert_index_of_name) output
blanchet@60201
    28
      val used_assm_js =
blanchet@60201
    29
        map_filter (fn id => let val i = index_of_id id in if i >= 0 then SOME i else NONE end)
blanchet@60201
    30
          used_assert_ids
blanchet@59015
    31
blanchet@60201
    32
      val conjecture_i = 0
blanchet@60201
    33
      val prems_i = conjecture_i + 1
blanchet@60201
    34
      val num_prems = length prems
blanchet@60201
    35
      val facts_i = prems_i + num_prems
blanchet@59015
    36
blanchet@60201
    37
      val fact_ids' =
blanchet@60201
    38
        map_filter (fn j =>
blanchet@60201
    39
          let val (i, _) = nth assms j in
blanchet@60201
    40
            try (apsnd (nth xfacts)) (id_of_index j, i - facts_i)
blanchet@60201
    41
          end) used_assm_js
blanchet@60201
    42
    in
blanchet@60201
    43
      {outcome = NONE, fact_ids = SOME fact_ids', atp_proof = K []}
blanchet@60201
    44
    end
blanchet@59015
    45
blanchet@59015
    46
end;