mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 18:05:21 +00:00
Code Activity

Cleaning up unsat_core_learner

Browse source
This commit is contained in:
Arie Gurfinkel 2018-06-23 00:05:14 -04:00
parent 7b2ca769ef
commit 1764bb8785
3 changed files with 10 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/muz/spacer/spacer_unsat_core_learner.cpp
View file

@ -54,7 +54,7 @@ void unsat_core_learner::compute_unsat_core(expr_ref_vector& unsat_core) {
// if the node mixes A-reasoning and B-reasoning
// and contains non-closed premises
if (!done) {
if (m_pr.is_a_marked(curr) && m_pr.is_b_marked(curr)) {
if (is_a(curr) && is_b(curr)) {
compute_partial_core(curr);
}
}
@ -92,9 +92,6 @@ void unsat_core_learner::set_closed(proof* p, bool value) {
m_closed.mark(p, value);
}
bool unsat_core_learner::is_b_open(proof *p) {
return m_pr.is_b_marked(p) && !is_closed (p);
}
void unsat_core_learner::add_lemma_to_core(expr* lemma) {
m_unsat_core.push_back(lemma);

10
src/muz/spacer/spacer_unsat_core_learner.h
View file

@ -47,10 +47,17 @@ namespace spacer {
ast_manager& get_manager() {return m;}
bool is_a(proof *pr) {return m_pr.is_a_marked(pr);}
bool is_a(proof *pr) {
// AG: treat hypotheses as A
// AG: assume that all B-hyp have been eliminated
// AG: this is not yet true in case of arithmetic eq_prop
return m_pr.is_a_marked(pr) || is_h(pr);
}
bool is_b(proof *pr) {return m_pr.is_b_marked(pr);}
bool is_h(proof *pr) {return m_pr.is_h_marked(pr);}
bool is_b_pure(proof *pr) { return m_pr.is_b_pure(pr);}
bool is_b_open(proof *p) {return m_pr.is_b_marked(p) && !is_closed (p);}
/*
* register a plugin for computation of partial unsat cores
@ -72,7 +79,6 @@ namespace spacer {
bool is_closed(proof* p);
void set_closed(proof* p, bool value);
bool is_b_open (proof *p);
/*
* adds a lemma to the unsat core

1
src/muz/spacer/spacer_unsat_core_plugin.cpp
View file

@ -210,6 +210,7 @@ namespace spacer {
// AG: it will go into the core. However, it does not mean that this literal should/could not be added.
m_ctx.set_closed(step, done);
expr_ref res = compute_linear_combination(coeff_lits);
TRACE("spacer.farkas", tout << "Farkas core: " << res << "\n";);
m_ctx.add_lemma_to_core(res);
}
}