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;
     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   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 
    46 end;