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