mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity

API to find pob in pob_manager

Browse source
This commit is contained in:
Arie Gurfinkel 2018-06-26 22:18:45 -04:00
parent 5bc57238a6
commit f6dcc6fc72
2 changed files with 17 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -2168,7 +2168,21 @@ pob* pred_transformer::pob_manager::mk_pob(pob *parent,
return n;
}
pob* pred_transformer::pob_manager::find_pob(pob* parent, expr *post) {
pob p(parent, m_pt, 0, 0, false);
p.set_post(post);
pob *res = nullptr;
if (m_pobs.contains(p.post())) {
for (auto *f : m_pobs[p.post()]) {
if (f->parent() == parent) {
// try to find pob not already in queue
if (!f->is_in_queue()) return f;
res = f;
}
}
}
return res;
}
// ----------------

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

@ -304,6 +304,7 @@ class pred_transformer {
}
unsigned size() const {return m_pinned.size();}
pob* find_pob(pob* parent, expr *post);
};
class pt_rule {
@ -601,7 +602,6 @@ class pob {
std::map<unsigned, stopwatch> m_expand_watches;
unsigned m_blocked_lvl;
void set_post(expr *post);
public:
pob (pob* parent, pred_transformer& pt,
unsigned level, unsigned depth=0, bool add_to_parent=true);
@ -610,6 +610,7 @@ public:
// TBD: move into constructor and make private
void set_post(expr *post, app_ref_vector const &binding);
void set_post(expr *post);
unsigned weakness() {return m_weakness;}
void bump_weakness() {m_weakness++;}