1 #pragma once 2 3 #include <ostream> 4 #include "ast/ast.h" 5 6 namespace spacer { 7 typedef obj_hashtable<expr> expr_set; 8 typedef obj_hashtable<func_decl> func_decl_set; 9 10 /* 11 * An iuc_proof is a proof together with information of the 12 * coloring of the axioms. 13 */ 14 class iuc_proof 15 { 16 public: 17 18 // Constructs an iuc_proof given an ast_manager, a proof, and a set of 19 // literals core_lits that might be included in the unsat core 20 iuc_proof(ast_manager& m, proof* pr, const expr_set& core_lits); 21 iuc_proof(ast_manager& m, proof* pr, const expr_ref_vector &core_lits); 22 23 // returns the proof object get()24 proof* get() {return m_pr.get();} 25 26 // returns true if all uninterpreted symbols of e are from the core literals 27 // requires that m_core_symbols has already been computed 28 bool is_core_pure(expr* e) const; 29 is_a_marked(proof * p)30 bool is_a_marked(proof* p) {return m_a_mark.is_marked(p);} is_b_marked(proof * p)31 bool is_b_marked(proof* p) {return m_b_mark.is_marked(p);} is_h_marked(proof * p)32 bool is_h_marked(proof* p) {return m_h_mark.is_marked(p);} 33 is_b_pure(proof * p)34 bool is_b_pure (proof *p) { 35 return !is_h_marked (p) && !this->is_a_marked(p) && is_core_pure(m.get_fact (p)); 36 } 37 38 void display_dot(std::ostream &out); 39 // debug method 40 void dump_farkas_stats(); 41 private: 42 ast_manager& m; 43 proof_ref m_pr; 44 45 ast_mark m_a_mark; 46 ast_mark m_b_mark; 47 ast_mark m_h_mark; 48 49 // -- literals that are part of the core 50 expr_set m_core_lits; 51 52 // symbols that occur in any literals in the core 53 func_decl_set m_core_symbols; 54 55 // collect symbols occurring in B (the core) 56 void collect_core_symbols(); 57 58 // compute for each formula of the proof whether it derives 59 // from A or from B 60 void compute_marks(); 61 }; 62 63 64 } 65 66