mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 21:03:39 +00:00
Code Activity

Add methods to print pob

Browse source
This commit is contained in:
Arie Gurfinkel 2018-06-28 14:23:14 -04:00
parent a63e4b48ca
commit 41a05e9d58
2 changed files with 14 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -126,7 +126,15 @@ void pob::get_skolems(app_ref_vector &v) {
} }
} }
std::ostream &pob::display(std::ostream &out, bool full) const {
out << pt().head()->get_name ()
<< " level: " << level()
<< " depth: " << depth()
<< " post_id: " << post()->get_id()
<< (is_in_queue() ? " in_queue" : "");
if (full) out << "\n" << m_post;
return out;
}
// ---------------- // ----------------
// pob_queue // pob_queue
@ -2174,9 +2182,7 @@ pob* pred_transformer::pob_manager::mk_pob(pob *parent,
p.set_post(post, b); p.set_post(post, b);
if (m_pobs.contains(p.post())) { if (m_pobs.contains(p.post())) {
auto &buf = m_pobs[p.post()]; for (auto *f : m_pobs[p.post()]) {
for (unsigned i = 0, sz = buf.size(); i < sz; ++i) {
pob *f = buf.get(i);
if (f->parent() == parent && !f->is_in_queue()) { if (f->parent() == parent && !f->is_in_queue()) {
f->inherit(p); f->inherit(p);
return f; return f;

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

@ -693,6 +693,7 @@ public:
if (m_ref_count == 0) {dealloc(this);} if (m_ref_count == 0) {dealloc(this);}
} }
std::ostream &display(std::ostream &out, bool full = false) const;
class on_expand_event class on_expand_event
{ {
pob &m_p; pob &m_p;
@ -702,6 +703,9 @@ public:
}; };
}; };
inline std::ostream &operator<<(std::ostream &out, pob const &p) {
return p.display(out);
}
struct pob_lt_proc : public std::binary_function<const pob*, const pob*, bool> { struct pob_lt_proc : public std::binary_function<const pob*, const pob*, bool> {
bool operator() (const pob *pn1, const pob *pn2) const; bool operator() (const pob *pn1, const pob *pn2) const;