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

Track whether pob is in pob_queue

Browse source 
pob_queue is a priority queue. Changing a pob while it is in the queue might change
the priority. This is a source of subtle bugs. The flag is ment to help defend
against this issues in the future.

As a side-effect, a pob that is already in the queue will be silently not added
to it, and a new version of a pob might be created if a version being looked
for is already in the queue.
This commit is contained in:
Arie Gurfinkel 2018-06-26 22:06:19 -04:00
parent c00c6b4285
commit 5bc57238a6
2 changed files with 85 additions and 67 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -66,8 +66,8 @@ pob::pob (pob* parent, pred_transformer& pt,
m_binding(m_pt.get_ast_manager()),
m_new_post (m_pt.get_ast_manager ()),
m_level (level), m_depth (depth),
m_open (true), m_use_farkas (true), m_weakness(0),
m_blocked_lvl(0) {
m_open (true), m_use_farkas (true), m_in_queue(false),
m_weakness(0), m_blocked_lvl(0) {
if (add_to_parent && m_parent) {
m_parent->add_child(*this);
}
@ -79,6 +79,7 @@ void pob::set_post(expr* post) {
}
void pob::set_post(expr* post, app_ref_vector const &binding) {
SASSERT(!is_in_queue());
normalize(post, m_post,
m_pt.get_context().simplify_pob(),
m_pt.get_context().use_euf_gen());
@ -88,6 +89,7 @@ void pob::set_post(expr* post, app_ref_vector const &binding) {
}
void pob::inherit(pob const &p) {
SASSERT(!is_in_queue());
SASSERT(m_parent == p.m_parent);
SASSERT(&m_pt == &p.m_pt);
SASSERT(m_post == p.m_post);
@ -105,17 +107,10 @@ void pob::inherit(pob const &p) {
m_derivation = nullptr;
}
void pob::clean () {
if (m_new_post) {
m_post = m_new_post;
m_new_post.reset();
}
}
void pob::close () {
if (!m_open) { return; }
reset ();
m_derivation = nullptr;
m_open = false;
for (unsigned i = 0, sz = m_kids.size (); i < sz; ++i)
{ m_kids [i]->close(); }
@ -148,6 +143,13 @@ pob* pob_queue::top ()
return m_data.top ();
}
void pob_queue::pop() {
pob *p = m_data.top();
p->set_in_queue(false);
m_data.pop();
}
void pob_queue::set_root(pob& root)
{
m_root = &root;
@ -156,19 +158,28 @@ void pob_queue::set_root(pob& root)
reset();
}
pob_queue::~pob_queue() {}
void pob_queue::reset()
{
while (!m_data.empty()) { m_data.pop(); }
if (m_root) { m_data.push(m_root.get()); }
while (!m_data.empty()) {
pob *p = m_data.top();
m_data.pop();
p->set_in_queue(false);
}
if (m_root) {
SASSERT(!m_root->is_in_queue());
m_root->set_in_queue(true);
m_data.push(m_root.get());
}
}
void pob_queue::push(pob &n) {
TRACE("pob_queue",
tout << "pob_queue::push(" << n.post()->get_id() << ")\n";);
m_data.push (&n);
n.get_context().new_pob_eh(&n);
if (!n.is_in_queue()) {
TRACE("pob_queue",
tout << "pob_queue::push(" << n.post()->get_id() << ")\n";);
n.set_in_queue(true);
m_data.push (&n);
n.get_context().new_pob_eh(&n);
}
}
// ----------------
@ -2135,7 +2146,7 @@ pob* pred_transformer::pob_manager::mk_pob(pob *parent,
auto &buf = m_pobs[p.post()];
for (unsigned i = 0, sz = buf.size(); i < sz; ++i) {
pob *f = buf.get(i);
if (f->parent() == parent) {
if (f->parent() == parent && !f->is_in_queue()) {
f->inherit(p);
return f;
}
@ -3051,27 +3062,19 @@ bool context::check_reachability ()
}
SASSERT (m_pob_queue.top ());
// -- remove all closed nodes and updated all dirty nodes
// -- remove all closed nodes
// -- this is necessary because there is no easy way to
// -- remove nodes from the priority queue.
while (m_pob_queue.top ()->is_closed () ||
m_pob_queue.top()->is_dirty()) {
pob_ref n = m_pob_queue.top ();
m_pob_queue.pop ();
if (n->is_closed()) {
IF_VERBOSE (1,
verbose_stream () << "Deleting closed node: "
<< n->pt ().head ()->get_name ()
<< "(" << n->level () << ", " << n->depth () << ")"
<< " " << n->post ()->get_id () << "\n";);
if (m_pob_queue.is_root(*n)) { return true; }
SASSERT (m_pob_queue.top ());
} else if (n->is_dirty()) {
n->clean ();
// -- the node n might not be at the top after it is cleaned
m_pob_queue.push (*n);
} else
{ UNREACHABLE(); }
while (m_pob_queue.top ()->is_closed ()) {
pob_ref n = m_pob_queue.top();
m_pob_queue.pop();
IF_VERBOSE (1,
verbose_stream () << "Deleting closed node: "
<< n->pt ().head ()->get_name ()
<< "(" << n->level () << ", " << n->depth () << ")"
<< " " << n->post ()->get_id () << "\n";);
if (m_pob_queue.is_root(*n)) {return true;}
SASSERT (m_pob_queue.top ());
}
SASSERT (m_pob_queue.top ());
@ -3165,6 +3168,7 @@ bool context::is_reachable(pob &n)
unsigned num_reuse_reach = 0;
unsigned saved = n.level ();
// TBD: don't expose private field
n.m_level = infty_level ();
lbool res = n.pt().is_reachable(n, nullptr, &mdl,
uses_level, is_concrete, r,
@ -3409,10 +3413,11 @@ lbool context::expand_pob(pob& n, pob_ref_buffer &out)
// Optionally update the node to be the negation of the lemma
if (v && m_use_lemma_as_pob) {
n.new_post (mk_and(lemma->get_cube()));
n.set_farkas_generalizer (false);
// XXX hack while refactoring is in progress
n.clean();
NOT_IMPLEMENTED_YET();
// n.new_post (mk_and(lemma->get_cube()));
// n.set_farkas_generalizer (false);
// // XXX hack while refactoring is in progress
// n.clean();
}
// schedule the node to be placed back in the queue

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

@ -562,6 +562,7 @@ public:
* A proof obligation.
*/
class pob {
// TBD: remove this
friend class context;
unsigned m_ref_count;
/// parent node
@ -576,14 +577,15 @@ class pob {
/// new post to be swapped in for m_post
expr_ref m_new_post;
/// level at which to decide the post
unsigned m_level;
unsigned m_depth;
unsigned m_level:16;
unsigned m_depth:16;
/// whether a concrete answer to the post is found
bool m_open;
unsigned m_open:1;
/// whether to use farkas generalizer to construct a lemma blocking this node
bool m_use_farkas;
unsigned m_use_farkas:1;
/// true if this pob is in pob_queue
unsigned m_in_queue:1;
unsigned m_weakness;
/// derivation representing the position of this node in the parent's rule
@ -598,17 +600,25 @@ class pob {
// depth -> watch
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);
~pob() {if (m_parent) { m_parent->erase_child(*this); }}
// TBD: move into constructor and make private
void set_post(expr *post, app_ref_vector const &binding);
unsigned weakness() {return m_weakness;}
void bump_weakness() {m_weakness++;}
void reset_weakness() {m_weakness=0;}
void inc_level () {m_level++; m_depth++;reset_weakness();}
void inc_level () {
SASSERT(!is_in_queue());
m_level++; m_depth++;reset_weakness();
}
void inherit(pob const &p);
void set_derivation (derivation *d) {m_derivation = d;}
@ -628,32 +638,25 @@ public:
unsigned level () const { return m_level; }
unsigned depth () const {return m_depth;}
unsigned width () const {return m_kids.size();}
unsigned blocked_at(unsigned lvl=0){return (m_blocked_lvl = std::max(lvl, m_blocked_lvl)); }
unsigned blocked_at(unsigned lvl=0){
return (m_blocked_lvl = std::max(lvl, m_blocked_lvl));
}
bool is_in_queue() const {return m_in_queue;}
void set_in_queue(bool v) {m_in_queue = v;}
bool use_farkas_generalizer () const {return m_use_farkas;}
void set_farkas_generalizer (bool v) {m_use_farkas = v;}
expr* post() const { return m_post.get (); }
void set_post(expr *post);
void set_post(expr *post, app_ref_vector const &binding);
/// indicate that a new post should be set for the node
void new_post(expr *post) {if (post != m_post) {m_new_post = post;}}
/// true if the node needs to be updated outside of the priority queue
bool is_dirty () {return m_new_post;}
/// clean a dirty node
void clean();
void reset () {clean (); m_derivation = nullptr; m_open = true;}
bool is_closed () const { return !m_open; }
void close();
const ptr_vector<pob> &children() {return m_kids;}
const ptr_vector<pob> &children() const {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;}
const ptr_vector<lemma> &lemmas() const {return m_lemmas;}
void add_lemma(lemma* new_lemma) {m_lemmas.push_back(new_lemma);}
bool is_ground () const { return m_binding.empty (); }
@ -666,8 +669,14 @@ public:
*/
void get_skolems(app_ref_vector& v);
void on_expand() { m_expand_watches[m_depth].start(); if (m_parent.get()){m_parent.get()->on_expand();} }
void off_expand() { m_expand_watches[m_depth].stop(); if (m_parent.get()){m_parent.get()->off_expand();} };
void on_expand() {
m_expand_watches[m_depth].start();
if (m_parent.get()){m_parent.get()->on_expand();}
}
void off_expand() {
m_expand_watches[m_depth].stop();
if (m_parent.get()){m_parent.get()->off_expand();}
}
double get_expand_time(unsigned depth) { return m_expand_watches[depth].get_seconds();}
void inc_ref () {++m_ref_count;}
@ -782,18 +791,22 @@ class pob_queue {
public:
pob_queue(): m_root(nullptr), m_max_level(0), m_min_depth(0) {}
~pob_queue();
~pob_queue() {}
void reset();
pob* top();
void pop() {m_data.pop ();}
void pop();
void push (pob &n);
void inc_level () {
SASSERT (!m_data.empty () || m_root);
m_max_level++;
m_min_depth++;
if (m_root && m_data.empty()) { m_data.push(m_root.get()); }
if (m_root && m_data.empty()) {
SASSERT(!m_root->is_in_queue());
m_root->set_in_queue(true);
m_data.push(m_root.get());
}
}
pob& get_root() const {return *m_root.get ();}