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