1 /*++ 2 Copyright (c) 2017 Arie Gurfinkel 3 4 Module Name: 5 6 spacer_proof_utils.cpp 7 8 Abstract: 9 Utilities to traverse and manipulate proofs 10 11 Author: 12 Bernhard Gleiss 13 Arie Gurfinkel 14 15 Revision History: 16 17 --*/ 18 19 #pragma once 20 #include "ast/ast.h" 21 22 namespace spacer { 23 24 bool is_arith_lemma(ast_manager& m, proof* pr); 25 bool is_farkas_lemma(ast_manager& m, proof* pr); 26 27 /// rewrites theory axioms into theory lemmas 28 class theory_axiom_reducer { 29 public: theory_axiom_reducer(ast_manager & m)30 theory_axiom_reducer(ast_manager& m) : m(m), m_pinned(m) {} 31 32 // reduce theory axioms and return transformed proof 33 proof_ref reduce(proof* pr); 34 35 private: 36 ast_manager &m; 37 38 // tracking all created expressions 39 expr_ref_vector m_pinned; 40 41 // maps each proof of a clause to the transformed subproof of 42 // that clause 43 obj_map<proof, proof*> m_cache; 44 45 void reset(); 46 }; 47 48 /// reduces the number of hypotheses in a proof 49 class hypothesis_reducer 50 { 51 public: hypothesis_reducer(ast_manager & m)52 hypothesis_reducer(ast_manager &m) : m(m), m_pinned(m) {} ~hypothesis_reducer()53 ~hypothesis_reducer() {reset();} 54 55 // reduce hypothesis and return transformed proof 56 proof_ref reduce(proof* pf); 57 58 private: 59 typedef ptr_vector<proof> proof_ptr_vector; 60 61 ast_manager &m; 62 63 proof_ptr_vector m_empty_vector; 64 65 // created expressions 66 expr_ref_vector m_pinned; 67 68 // created sets of active hypothesis 69 ptr_vector<proof_ptr_vector> m_pinned_active_hyps; 70 71 // maps a proof to the transformed proof 72 obj_map<proof, proof*> m_cache; 73 74 // maps a unit literal to its derivation 75 obj_map<expr, proof*> m_units; 76 77 // maps a proof node to the set of its active (i.e., in scope) hypotheses 78 obj_map<proof, proof_ptr_vector*> m_active_hyps; 79 80 /// marks if an expression is ever used as a hypothesis in a proof 81 expr_mark m_hyp_mark; 82 /// marks a proof as open, i.e., has a non-discharged hypothesis as ancestor 83 expr_mark m_open_mark; 84 expr_mark m_visited; 85 86 void reset(); 87 88 /// true if p is an ancestor of q 89 bool is_ancestor(proof *p, proof *q); 90 // compute active_hyps and parent_hyps for a given proof node and 91 // all its ancestors 92 void compute_hypsets(proof* pr); 93 // compute m_units 94 void collect_units(proof* pr); 95 96 // -- rewrite proof to reduce number of hypotheses used 97 proof* reduce_core(proof* pf); 98 99 proof* mk_lemma_core(proof *pf, expr *fact); 100 proof* mk_unit_resolution_core(proof* ures, ptr_buffer<proof>& args); 101 proof* mk_proof_core(proof* old, ptr_buffer<proof>& args); 102 }; 103 } 104