mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

spacer: pobs keep track of their lemmas

Browse source
This commit is contained in:
Arie Gurfinkel 2018-05-29 21:23:32 -07:00
parent 61cd74818f
commit 5072a2a869
2 changed files with 31 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

33
src/muz/spacer/spacer_context.cpp
View file

@ -70,7 +70,6 @@ pob::pob (pob* parent, pred_transformer& pt,
}
}
void pob::set_post(expr* post) {
app_ref_vector empty_binding(get_ast_manager());
set_post(post, empty_binding);
@ -1800,36 +1799,48 @@ bool pred_transformer::frames::add_lemma(lemma *new_lemma)
<< m_pt.head()->get_name() << " "
<< mk_pp(new_lemma->get_expr(), m_pt.get_ast_manager()) << "\n";);
for (unsigned i = 0, sz = m_lemmas.size(); i < sz; ++i) {
if (m_lemmas[i]->get_expr() == new_lemma->get_expr()) {
unsigned i = 0;
for (auto *old_lemma : m_lemmas) {
if (old_lemma->get_expr() == new_lemma->get_expr()) {
m_pt.get_context().new_lemma_eh(m_pt, new_lemma);
// register existing lemma with the pob
if (new_lemma->has_pob()) {
pob_ref &pob = new_lemma->get_pob();
if (!pob->lemmas().contains(old_lemma))
pob->add_lemma(old_lemma);
}
// extend bindings if needed
if (!new_lemma->get_bindings().empty()) {
m_lemmas[i]->add_binding(new_lemma->get_bindings());
old_lemma->add_binding(new_lemma->get_bindings());
}
// if the lemma is at a higher level, skip it,
if (m_lemmas[i]->level() >= new_lemma->level()) {
if (old_lemma->level() >= new_lemma->level()) {
TRACE("spacer", tout << "Already at a higher level: "
<< pp_level(m_lemmas[i]->level()) << "\n";);
<< pp_level(old_lemma->level()) << "\n";);
// but, since the instances might be new, assert the
// instances that have been copied into m_lemmas[i]
if (!new_lemma->get_bindings().empty()) {
m_pt.add_lemma_core(m_lemmas[i], true);
m_pt.add_lemma_core(old_lemma, true);
}
// no new lemma added
return false;
}
// update level of the existing lemma
m_lemmas[i]->set_level(new_lemma->level());
old_lemma->set_level(new_lemma->level());
// assert lemma in the solver
m_pt.add_lemma_core(m_lemmas[i], false);
m_pt.add_lemma_core(old_lemma, false);
// move the lemma to its new place to maintain sortedness
for (unsigned j = i; (j + 1) < sz && m_lt(m_lemmas[j + 1], m_lemmas[j]); ++j) {
unsigned sz = m_lemmas.size();
for (unsigned j = i;
(j + 1) < sz && m_lt(m_lemmas[j + 1], m_lemmas[j]); ++j) {
m_lemmas.swap (j, j+1);
}
return true;
}
i++;
}
// new_lemma is really new
@ -1840,6 +1851,8 @@ bool pred_transformer::frames::add_lemma(lemma *new_lemma)
m_sorted = false;
m_pt.add_lemma_core(new_lemma);
if (new_lemma->has_pob()) {new_lemma->get_pob()->add_lemma(new_lemma);}
if (!new_lemma->external()) {
m_pt.get_context().new_lemma_eh(m_pt, new_lemma);
}

8
src/muz/spacer/spacer_context.h
View file

@ -486,7 +486,11 @@ class pob {
/// derivation representing the position of this node in the parent's rule
scoped_ptr<derivation> m_derivation;
/// pobs created as children of this pob (at any time, not
/// necessarily currently active)
ptr_vector<pob> m_kids;
// lemmas created to block this pob (at any time, not necessarily active)
ptr_vector<lemma> m_lemmas;
// depth -> watch
std::map<unsigned, stopwatch> m_expand_watches;
@ -542,9 +546,13 @@ public:
bool is_closed () const { return !m_open; }
void close();
const ptr_vector<pob> &children() {return m_kids;}
void add_child (pob &v) {m_kids.push_back (&v);}
void erase_child (pob &v) {m_kids.erase (&v);}
const ptr_vector<lemma> &lemmas() {return m_lemmas;}
void add_lemma(lemma* new_lemma) {m_lemmas.push_back(new_lemma);}
bool is_ground () { return m_binding.empty (); }
unsigned get_free_vars_size() { return m_binding.size(); }
app_ref_vector const &get_binding() const {return m_binding;}