mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-26 07:43:41 +00:00
Code Activity

Cleanup iuc_proof

Browse source
This commit is contained in:
Arie Gurfinkel 2018-05-16 12:57:35 -07:00
parent abe67705d3
commit 45500ff7d3
2 changed files with 24 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

25
src/muz/spacer/spacer_iuc_proof.cpp
View file

@ -11,13 +11,21 @@ namespace spacer {
* init * init
* ==================================== * ====================================
*/ */
iuc_proof::iuc_proof(ast_manager& m, proof* pr, expr_set& core_lits) : iuc_proof::iuc_proof(ast_manager& m, proof* pr, const expr_set& core_lits) :
m(m), m_pr(pr,m) { m(m), m_pr(pr,m) {
for (auto lit : core_lits) m_core_lits.insert(lit);
// init A-marks and B-marks // init A-marks and B-marks
collect_core_symbols(core_lits); collect_core_symbols();
compute_marks(core_lits); compute_marks();
} }
iuc_proof::iuc_proof(ast_manager& m, proof* pr, const expr_ref_vector& core_lits) :
m(m), m_pr(pr,m) {
for (auto lit : core_lits) m_core_lits.insert(lit);
// init A-marks and B-marks
collect_core_symbols();
compute_marks();
}
/* /*
* ==================================== * ====================================
* methods for computing symbol colors * methods for computing symbol colors
@ -37,13 +45,12 @@ public:
void operator()(quantifier*) {} void operator()(quantifier*) {}
}; };
void iuc_proof::collect_core_symbols(expr_set& core_lits) void iuc_proof::collect_core_symbols()
{ {
expr_mark visited; expr_mark visited;
collect_pure_proc proc(m_core_symbols); collect_pure_proc proc(m_core_symbols);
for (expr_set::iterator it = core_lits.begin(); it != core_lits.end(); ++it) { for (auto lit : m_core_lits)
for_each_expr(proc, visited, *it); for_each_expr(proc, visited, lit);
}
} }
class is_pure_expr_proc { class is_pure_expr_proc {
@ -84,7 +91,7 @@ bool iuc_proof::is_core_pure(expr* e) const
return true; return true;
} }
void iuc_proof::compute_marks(expr_set& core_lits) void iuc_proof::compute_marks()
{ {
proof_post_order it(m_pr, m); proof_post_order it(m_pr, m);
while (it.hasNext()) while (it.hasNext())
@ -95,7 +102,7 @@ void iuc_proof::compute_marks(expr_set& core_lits)
switch(cur->get_decl_kind()) switch(cur->get_decl_kind())
{ {
case PR_ASSERTED: case PR_ASSERTED:
if (core_lits.contains(m.get_fact(cur))) if (m_core_lits.contains(m.get_fact(cur)))
m_b_mark.mark(cur, true); m_b_mark.mark(cur, true);
else else
m_a_mark.mark(cur, true); m_a_mark.mark(cur, true);

12
src/muz/spacer/spacer_iuc_proof.h
View file

@ -17,7 +17,8 @@ public:
// Constructs an iuc_proof given an ast_manager, a proof, and a set of // 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 // literals core_lits that might be included in the unsat core
iuc_proof(ast_manager& m, proof* pr, expr_set& core_lits); 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 // returns the proof object
proof* get() {return m_pr.get();} proof* get() {return m_pr.get();}
@ -44,15 +45,18 @@ private:
ast_mark m_b_mark; ast_mark m_b_mark;
ast_mark m_h_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 // symbols that occur in any literals in the core
func_decl_set m_core_symbols; func_decl_set m_core_symbols;
// collect symbols occuring in B (the core) // collect symbols occurring in B (the core)
void collect_core_symbols(expr_set& core_lits); void collect_core_symbols();
// compute for each formula of the proof whether it derives // compute for each formula of the proof whether it derives
// from A or from B // from A or from B
void compute_marks(expr_set& core_lits); void compute_marks();
}; };