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