From d9100437ce377bf185cb0b3f9b2da8e79ca9ce60 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Tue, 26 Jun 2018 11:33:54 -0400 Subject: [PATCH 01/15] Weakness of the lemma independent of the pob Lemma inherits its weakness score from the pob. However, pob's weakness might be reset or changed for some other reason. To avoid affecting the lemma, the weakness is copied on construction. --- src/muz/spacer/spacer_context.cpp | 9 ++++++--- src/muz/spacer/spacer_context.h | 4 ++-- 2 files changed, 8 insertions(+), 5 deletions(-) diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index 40569295b..172aff40f 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -463,7 +463,8 @@ lemma::lemma (ast_manager &manager, expr * body, unsigned lvl) : m_ref_count(0), m(manager), m_body(body, m), m_cube(m), m_zks(m), m_bindings(m), m_lvl(lvl), m_init_lvl(m_lvl), - m_pob(nullptr), m_ctp(nullptr), m_external(false), m_bumped(0) { + m_pob(nullptr), m_ctp(nullptr), m_external(false), + m_bumped(0), m_weakness(UINT_MAX) { SASSERT(m_body); normalize(m_body, m_body); } @@ -472,7 +473,8 @@ lemma::lemma(pob_ref const &p) : m_ref_count(0), m(p->get_ast_manager()), m_body(m), m_cube(m), m_zks(m), m_bindings(m), m_lvl(p->level()), m_init_lvl(m_lvl), - m_pob(p), m_ctp(nullptr), m_external(false), m_bumped(0) { + m_pob(p), m_ctp(nullptr), m_external(false), m_bumped(0), + m_weakness(p->weakness()) { SASSERT(m_pob); m_pob->get_skolems(m_zks); add_binding(m_pob->get_binding()); @@ -483,7 +485,8 @@ lemma::lemma(pob_ref const &p, expr_ref_vector &cube, unsigned lvl) : m(p->get_ast_manager()), m_body(m), m_cube(m), m_zks(m), m_bindings(m), m_lvl(p->level()), m_init_lvl(m_lvl), - m_pob(p), m_ctp(nullptr), m_external(false), m_bumped(0) + m_pob(p), m_ctp(nullptr), m_external(false), m_bumped(0), + m_weakness(p->weakness()) { if (m_pob) { m_pob->get_skolems(m_zks); diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h index 37b035b98..87beb472e 100644 --- a/src/muz/spacer/spacer_context.h +++ b/src/muz/spacer/spacer_context.h @@ -128,6 +128,7 @@ class lemma { model_ref m_ctp; // counter-example to pushing bool m_external; unsigned m_bumped; + unsigned m_weakness; void mk_expr_core(); void mk_cube_core(); @@ -154,7 +155,7 @@ public: bool has_pob() {return m_pob;} pob_ref &get_pob() {return m_pob;} - inline unsigned weakness(); + unsigned weakness() {return m_weakness;} void add_skolem(app *zk, app* b); @@ -690,7 +691,6 @@ struct pob_ref_gt : {return gt (n1.get (), n2.get ());} }; -inline unsigned lemma::weakness() {return m_pob ? m_pob->weakness() : UINT_MAX;} /** */ class derivation { From 176c0a97f762aefcd9bfefe704ec7c21677e0257 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Tue, 26 Jun 2018 21:18:10 -0400 Subject: [PATCH 02/15] Gracefully handle absence of a proof --- src/solver/solver_pool.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/solver/solver_pool.cpp b/src/solver/solver_pool.cpp index 9dacfb5ce..598bb6c02 100644 --- a/src/solver/solver_pool.cpp +++ b/src/solver/solver_pool.cpp @@ -101,9 +101,11 @@ public: proof * get_proof() override { scoped_watch _t_(m_pool.m_proof_watch); if (!m_proof.get()) { - elim_aux_assertions pc(m_pred); m_proof = m_base->get_proof(); - pc(m, m_proof, m_proof); + if (m_proof) { + elim_aux_assertions pc(m_pred); + pc(m, m_proof, m_proof); + } } return m_proof; } From 1910b4c87c5fea35f801ec57fb0185f9e5f378a5 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Tue, 26 Jun 2018 21:20:54 -0400 Subject: [PATCH 03/15] Rename pobs into pob_manager --- src/muz/spacer/spacer_context.cpp | 7 ++++--- src/muz/spacer/spacer_context.h | 8 ++++---- 2 files changed, 8 insertions(+), 7 deletions(-) diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index 172aff40f..bf7743bae 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -2123,9 +2123,10 @@ void pred_transformer::frames::simplify_formulas () /// pred_transformer::pobs -pob* pred_transformer::pobs::mk_pob(pob *parent, - unsigned level, unsigned depth, - expr *post, app_ref_vector const &b) { +pob* pred_transformer::pob_manager::mk_pob(pob *parent, + unsigned level, unsigned depth, + expr *post, + app_ref_vector const &b) { if (!m_pt.ctx.reuse_pobs()) { pob* n = alloc(pob, parent, m_pt, level, depth); diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h index 87beb472e..6823f0406 100644 --- a/src/muz/spacer/spacer_context.h +++ b/src/muz/spacer/spacer_context.h @@ -269,9 +269,9 @@ class pred_transformer { }; /** - manager of proof-obligations (pobs) + manager of proof-obligations (pob_manager) */ - class pobs { + class pob_manager { typedef ptr_buffer pob_buffer; typedef obj_map expr2pob_buffer; @@ -280,7 +280,7 @@ class pred_transformer { expr2pob_buffer m_pobs; pob_ref_vector m_pinned; public: - pobs(pred_transformer &pt) : m_pt(pt) {} + pob_manager(pred_transformer &pt) : m_pt(pt) {} pob* mk_pob(pob *parent, unsigned level, unsigned depth, expr *post, app_ref_vector const &b); @@ -362,7 +362,7 @@ class pred_transformer { ptr_vector m_rules; // rules used to derive transformer scoped_ptr m_solver; // solver context ref m_reach_solver; // context for reachability facts - pobs m_pobs; // proof obligations created so far + pob_manager m_pobs; // proof obligations created so far frames m_frames; // frames with lemmas reach_fact_ref_vector m_reach_facts; // reach facts unsigned m_rf_init_sz; // number of reach fact from INIT From c00c6b4285a2b901141d49a229e24ceb61e01de3 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Tue, 26 Jun 2018 21:36:18 -0400 Subject: [PATCH 04/15] Pobs are always managed Removed options to allow unmanaged pobs. Other minor cleanups. --- src/muz/base/fp_params.pyg | 1 - src/muz/spacer/spacer_context.cpp | 26 ++++++---------- src/muz/spacer/spacer_context.h | 52 +++++++++++++++++-------------- 3 files changed, 37 insertions(+), 42 deletions(-) diff --git a/src/muz/base/fp_params.pyg b/src/muz/base/fp_params.pyg index c96a12ca2..31ab3a358 100644 --- a/src/muz/base/fp_params.pyg +++ b/src/muz/base/fp_params.pyg @@ -160,7 +160,6 @@ def_module_params('fp', '2 = use Gaussian elimination optimization (broken), 3 = use additive IUC plugin'), ('spacer.iuc.old_hyp_reducer', BOOL, False, 'use old hyp reducer instead of new implementation, for debugging only'), ('spacer.validate_lemmas', BOOL, False, 'Validate each lemma after generalization'), - ('spacer.reuse_pobs', BOOL, True, 'Reuse pobs'), ('spacer.ground_pobs', BOOL, True, 'Ground pobs by using values from a model'), ('spacer.iuc.print_farkas_stats', BOOL, False, 'prints for each proof how many Farkas lemmas it contains and how many of these participate in the cut (for debugging)'), ('spacer.iuc.debug_proof', BOOL, False, 'prints proof used by unsat-core-learner for debugging purposes (debugging)'), diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index bf7743bae..48550df12 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -137,15 +137,15 @@ void pob::get_skolems(app_ref_vector &v) { pob* pob_queue::top () { /// nothing in the queue - if (m_obligations.empty()) { return nullptr; } + if (m_data.empty()) { return nullptr; } /// top queue element is above max level - if (m_obligations.top()->level() > m_max_level) { return nullptr; } + if (m_data.top()->level() > m_max_level) { return nullptr; } /// top queue element is at the max level, but at a higher than base depth - if (m_obligations.top ()->level () == m_max_level && - m_obligations.top()->depth() > m_min_depth) { return nullptr; } + if (m_data.top ()->level () == m_max_level && + m_data.top()->depth() > m_min_depth) { return nullptr; } /// there is something good in the queue - return m_obligations.top ().get (); + return m_data.top (); } void pob_queue::set_root(pob& root) @@ -160,14 +160,14 @@ pob_queue::~pob_queue() {} void pob_queue::reset() { - while (!m_obligations.empty()) { m_obligations.pop(); } - if (m_root) { m_obligations.push(m_root); } + while (!m_data.empty()) { m_data.pop(); } + if (m_root) { 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_obligations.push (&n); + m_data.push (&n); n.get_context().new_pob_eh(&n); } @@ -2127,13 +2127,6 @@ pob* pred_transformer::pob_manager::mk_pob(pob *parent, unsigned level, unsigned depth, expr *post, app_ref_vector const &b) { - - if (!m_pt.ctx.reuse_pobs()) { - pob* n = alloc(pob, parent, m_pt, level, depth); - n->set_post(post, b); - return n; - } - // create a new pob and set its post to normalize it pob p(parent, m_pt, level, depth, false); p.set_post(post, b); @@ -2211,7 +2204,6 @@ void context::updt_params() { m_use_ctp = m_params.spacer_ctp(); m_use_inc_clause = m_params.spacer_use_inc_clause(); m_blast_term_ite = m_params.spacer_blast_term_ite(); - m_reuse_pobs = m_params.spacer_reuse_pobs(); m_use_ind_gen = m_params.spacer_use_inductive_generalizer(); m_use_array_eq_gen = m_params.spacer_use_array_eq_generalizer(); m_validate_lemmas = m_params.spacer_validate_lemmas(); @@ -3936,7 +3928,7 @@ bool context::is_inductive() { } /// pob_lt operator -inline bool pob_lt::operator() (const pob *pn1, const pob *pn2) const +inline bool pob_lt_proc::operator() (const pob *pn1, const pob *pn2) const { SASSERT (pn1); SASSERT (pn2); diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h index 6823f0406..480b8ecf5 100644 --- a/src/muz/spacer/spacer_context.h +++ b/src/muz/spacer/spacer_context.h @@ -270,14 +270,27 @@ class pred_transformer { /** manager of proof-obligations (pob_manager) + + Pobs are determined uniquely by their post-condition and a parent pob. + They are managed by pob_manager and remain live through the + life of the manager */ class pob_manager { + // a buffer that contains space for one pob and allocates more + // space if needed typedef ptr_buffer pob_buffer; + // Type for the map from post-conditions to pobs. The common + // case is that each post-condition corresponds to a single + // pob. Other cases are handled by expanding the buffer typedef obj_map expr2pob_buffer; + // parent predicate transformer pred_transformer &m_pt; + // map from post-conditions to pobs expr2pob_buffer m_pobs; + + // a store pob_ref_vector m_pinned; public: pob_manager(pred_transformer &pt) : m_pt(pt) {} @@ -673,22 +686,14 @@ public: }; -struct pob_lt : - public std::binary_function -{bool operator() (const pob *pn1, const pob *pn2) const;}; - -struct pob_gt : - public std::binary_function { - pob_lt lt; - bool operator() (const pob *n1, const pob *n2) const - {return lt(n2, n1);} +struct pob_lt_proc : public std::binary_function { + bool operator() (const pob *pn1, const pob *pn2) const; }; -struct pob_ref_gt : - public std::binary_function { - pob_gt gt; - bool operator() (const pob_ref &n1, const pob_ref &n2) const - {return gt (n1.get (), n2.get ());} +struct pob_gt_proc : public std::binary_function { + bool operator() (const pob *n1, const pob *n2) const { + return pob_lt_proc()(n2, n1); + } }; /** @@ -767,36 +772,37 @@ public: class pob_queue { + + typedef std::priority_queue, pob_gt_proc> pob_queue_ty; pob_ref m_root; unsigned m_max_level; unsigned m_min_depth; - std::priority_queue, - pob_ref_gt> m_obligations; + pob_queue_ty m_data; public: pob_queue(): m_root(nullptr), m_max_level(0), m_min_depth(0) {} ~pob_queue(); void reset(); - pob * top (); - void pop () {m_obligations.pop ();} + pob* top(); + void pop() {m_data.pop ();} void push (pob &n); void inc_level () { - SASSERT (!m_obligations.empty () || m_root); + SASSERT (!m_data.empty () || m_root); m_max_level++; m_min_depth++; - if (m_root && m_obligations.empty()) { m_obligations.push(m_root); } + if (m_root && m_data.empty()) { m_data.push(m_root.get()); } } pob& get_root() const {return *m_root.get ();} void set_root(pob& n); - bool is_root (pob& n) const {return m_root.get () == &n;} + bool is_root(pob& n) const {return m_root.get () == &n;} unsigned max_level() const {return m_max_level;} unsigned min_depth() const {return m_min_depth;} - size_t size() const {return m_obligations.size();} + size_t size() const {return m_data.size();} }; @@ -910,7 +916,6 @@ class context { bool m_use_ctp; bool m_use_inc_clause; bool m_blast_term_ite; - bool m_reuse_pobs; bool m_use_ind_gen; bool m_use_array_eq_gen; bool m_validate_lemmas; @@ -1007,7 +1012,6 @@ public: bool use_ctp() {return m_use_ctp;} bool use_inc_clause() {return m_use_inc_clause;} bool blast_term_ite() {return m_blast_term_ite;} - bool reuse_pobs() {return m_reuse_pobs;} bool elim_aux() {return m_elim_aux;} bool reach_dnf() {return m_reach_dnf;} From 5bc57238a69dba4197b3113c2f21830a99957523 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Tue, 26 Jun 2018 22:06:19 -0400 Subject: [PATCH 05/15] Track whether pob is in pob_queue 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. --- src/muz/spacer/spacer_context.cpp | 89 ++++++++++++++++--------------- src/muz/spacer/spacer_context.h | 63 +++++++++++++--------- 2 files changed, 85 insertions(+), 67 deletions(-) diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index 48550df12..ff63ae2ef 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -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 diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h index 480b8ecf5..f2242f0ad 100644 --- a/src/muz/spacer/spacer_context.h +++ b/src/muz/spacer/spacer_context.h @@ -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 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 &children() {return m_kids;} + const ptr_vector &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 &lemmas() {return m_lemmas;} + const ptr_vector &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 ();} From f6dcc6fc7202392d9f467702189267c280fb817b Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Tue, 26 Jun 2018 22:18:45 -0400 Subject: [PATCH 06/15] API to find pob in pob_manager --- src/muz/spacer/spacer_context.cpp | 16 +++++++++++++++- src/muz/spacer/spacer_context.h | 3 ++- 2 files changed, 17 insertions(+), 2 deletions(-) diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index ff63ae2ef..7b0fd8b57 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -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; +} // ---------------- diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h index f2242f0ad..07bea0538 100644 --- a/src/muz/spacer/spacer_context.h +++ b/src/muz/spacer/spacer_context.h @@ -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 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++;} From 2b4d92821a1c333a79f652ba93d607308b5b82ae Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Wed, 27 Jun 2018 09:16:51 -0400 Subject: [PATCH 07/15] Avoid crashing on cancel --- src/muz/spacer/spacer_context.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index 7b0fd8b57..3a20dc8ce 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -1361,7 +1361,7 @@ lbool pred_transformer::is_reachable(pob& n, expr_ref_vector* core, if (is_sat == l_true || is_sat == l_undef) { if (core) { core->reset(); } - if (model) { + if (model && model->get()) { r = find_rule(**model, is_concrete, reach_pred_used, num_reuse_reach); TRACE ("spacer", tout << "reachable " << "is_concrete " << is_concrete << " rused: "; From d7234dc039fc1c477d0efd7446a9e794af013f20 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Wed, 27 Jun 2018 09:17:10 -0400 Subject: [PATCH 08/15] Inactive debug code --- src/muz/spacer/spacer_iuc_solver.cpp | 34 ++++++++++++++++++++++++++++ 1 file changed, 34 insertions(+) diff --git a/src/muz/spacer/spacer_iuc_solver.cpp b/src/muz/spacer/spacer_iuc_solver.cpp index a68db4c0a..27b8ee357 100644 --- a/src/muz/spacer/spacer_iuc_solver.cpp +++ b/src/muz/spacer/spacer_iuc_solver.cpp @@ -322,6 +322,24 @@ void iuc_solver::get_iuc(expr_ref_vector &core) // -- new hypothesis reducer else { +#if 0 + static unsigned bcnt = 0; + { + bcnt++; + TRACE("spacer", tout << "Dumping pf bcnt: " << bcnt << "\n";); + if (bcnt == 123) { + std::ofstream ofs; + ofs.open("/tmp/bpf_" + std::to_string(bcnt) + ".dot"); + iuc_proof iuc_pf_before(m, res.get(), core_lits); + iuc_pf_before.display_dot(ofs); + ofs.close(); + + proof_checker pc(m); + expr_ref_vector side(m); + ENSURE(pc.check(res, side)); + } + } +#endif scoped_watch _t_ (m_hyp_reduce2_sw); // pre-process proof for better iuc extraction @@ -356,6 +374,22 @@ void iuc_solver::get_iuc(expr_ref_vector &core) iuc_proof iuc_pf(m, res, core_lits); +#if 0 + static unsigned cnt = 0; + { + cnt++; + TRACE("spacer", tout << "Dumping pf cnt: " << cnt << "\n";); + if (cnt == 123) { + std::ofstream ofs; + ofs.open("/tmp/pf_" + std::to_string(cnt) + ".dot"); + iuc_pf.display_dot(ofs); + ofs.close(); + proof_checker pc(m); + expr_ref_vector side(m); + ENSURE(pc.check(res, side)); + } + } +#endif unsat_core_learner learner(m, iuc_pf); unsat_core_plugin* plugin; From bc6604441b7af1c138a9e5cd3f2c2ac09955b4f2 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Wed, 27 Jun 2018 14:32:43 -0400 Subject: [PATCH 09/15] Helpers in model_core --- src/model/model_core.h | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/model/model_core.h b/src/model/model_core.h index d705e432d..7f5051386 100644 --- a/src/model/model_core.h +++ b/src/model/model_core.h @@ -48,6 +48,14 @@ public: func_interp * get_func_interp(func_decl * d) const { func_interp * fi; return m_finterp.find(d, fi) ? fi : nullptr; } bool eval(func_decl * f, expr_ref & r) const; + bool is_true_decl(func_decl *f) const { + expr_ref r(m); + return eval(f, r) && m.is_true(r); + } + bool is_false_decl(func_decl *f) const { + expr_ref r(m); + return eval(f, r) && m.is_false(r); + } unsigned get_num_constants() const { return m_const_decls.size(); } unsigned get_num_functions() const { return m_func_decls.size(); } From 49e94809282eee4dff22d39887724112dd6472a1 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Wed, 27 Jun 2018 14:34:29 -0400 Subject: [PATCH 10/15] Fix lemma_as_cti option Use negation of a lemma as a proof obligation. This speeds up discovering bad lemmas that do not contain some reachable states. --- src/muz/spacer/spacer_context.cpp | 59 ++++++++++++++++++++++--------- src/muz/spacer/spacer_context.h | 21 +++++++---- 2 files changed, 56 insertions(+), 24 deletions(-) diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index 3a20dc8ce..142cfa898 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -55,6 +55,8 @@ Notes: #include "muz/spacer/spacer_sat_answer.h" +#define WEAKNESS_MAX 65535 + namespace spacer { /// pob -- proof obligation @@ -473,9 +475,11 @@ void derivation::premise::set_summary (expr * summary, bool must, lemma::lemma (ast_manager &manager, expr * body, unsigned lvl) : m_ref_count(0), m(manager), m_body(body, m), m_cube(m), - m_zks(m), m_bindings(m), m_lvl(lvl), m_init_lvl(m_lvl), - m_pob(nullptr), m_ctp(nullptr), m_external(false), - m_bumped(0), m_weakness(UINT_MAX) { + m_zks(m), m_bindings(m), + m_pob(nullptr), m_ctp(nullptr), + m_lvl(lvl), m_init_lvl(m_lvl), + m_bumped(0), m_weakness(WEAKNESS_MAX), + m_external(false), m_blocked(false) { SASSERT(m_body); normalize(m_body, m_body); } @@ -483,9 +487,11 @@ lemma::lemma (ast_manager &manager, expr * body, unsigned lvl) : lemma::lemma(pob_ref const &p) : m_ref_count(0), m(p->get_ast_manager()), m_body(m), m_cube(m), - m_zks(m), m_bindings(m), m_lvl(p->level()), m_init_lvl(m_lvl), - m_pob(p), m_ctp(nullptr), m_external(false), m_bumped(0), - m_weakness(p->weakness()) { + m_zks(m), m_bindings(m), + m_pob(p), m_ctp(nullptr), + m_lvl(p->level()), m_init_lvl(m_lvl), + m_bumped(0), m_weakness(p->weakness()), + m_external(false), m_blocked(false) { SASSERT(m_pob); m_pob->get_skolems(m_zks); add_binding(m_pob->get_binding()); @@ -495,9 +501,11 @@ lemma::lemma(pob_ref const &p, expr_ref_vector &cube, unsigned lvl) : m_ref_count(0), m(p->get_ast_manager()), m_body(m), m_cube(m), - m_zks(m), m_bindings(m), m_lvl(p->level()), m_init_lvl(m_lvl), - m_pob(p), m_ctp(nullptr), m_external(false), m_bumped(0), - m_weakness(p->weakness()) + m_zks(m), m_bindings(m), + m_pob(p), m_ctp(nullptr), + m_lvl(p->level()), m_init_lvl(m_lvl), + m_bumped(0), m_weakness(p->weakness()), + m_external(false), m_blocked(false) { if (m_pob) { m_pob->get_skolems(m_zks); @@ -834,7 +842,7 @@ const datalog::rule *pred_transformer::find_rule(model &model) { for (auto &kv : m_pt_rules) { app *tag = kv.m_value->tag(); - if (model.eval(tag->get_decl(), val) && m.is_true(val)) { + if (model.is_true_decl(tag->get_decl())) { return &kv.m_value->rule(); } } @@ -1401,7 +1409,12 @@ bool pred_transformer::is_ctp_blocked(lemma *lem) { // -- find rule of the ctp const datalog::rule *r; r = find_rule(*ctp); - if (r == nullptr) {return false;} + if (r == nullptr) { + // no rules means lemma is blocked forever because + // it does not satisfy some derived facts + lem->set_blocked(true); + return true; + } // -- find predicates along the rule find_predecessors(*r, m_predicates); @@ -1424,6 +1437,8 @@ bool pred_transformer::is_invariant(unsigned level, lemma* lem, unsigned& solver_level, expr_ref_vector* core) { + if (lem->is_blocked()) return false; + m_stats.m_num_is_invariant++; if (is_ctp_blocked(lem)) { m_stats.m_num_ctp_blocked++; @@ -1465,7 +1480,7 @@ bool pred_transformer::is_invariant(unsigned level, lemma* lem, SASSERT (level <= solver_level); } else if (r == l_true) { - // optionally remove unused symbols from the model + // TBD: optionally remove unused symbols from the model if (mdl_ref_ptr) {lem->set_ctp(*mdl_ref_ptr);} } else {lem->reset_ctp();} @@ -3427,11 +3442,21 @@ 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) { - 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(); + expr_ref c(m); + c = mk_and(lemma->get_cube()); + // check that the post condition is different + if (c != n.post()) { + pob *f = n.pt().find_pob(n.parent(), c); + // skip if a similar pob is already in the queue + if (f != &n && (!f || !f->is_in_queue())) { + f = n.pt().mk_pob(n.parent(), n.level(), + n.depth(), c, n.get_binding()); + SASSERT(!f->is_in_queue()); + f->inc_level(); + //f->set_farkas_generalizer(false); + out.push_back(f); + } + } } // schedule the node to be placed back in the queue diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h index 07bea0538..93c2337e6 100644 --- a/src/muz/spacer/spacer_context.h +++ b/src/muz/spacer/spacer_context.h @@ -122,13 +122,14 @@ class lemma { expr_ref_vector m_cube; app_ref_vector m_zks; app_ref_vector m_bindings; + pob_ref m_pob; + model_ref m_ctp; // counter-example to pushing unsigned m_lvl; // current level of the lemma unsigned m_init_lvl; // level at which lemma was created - pob_ref m_pob; - model_ref m_ctp; // counter-example to pushing - bool m_external; - unsigned m_bumped; - unsigned m_weakness; + unsigned m_bumped:16; + unsigned m_weakness:16; + unsigned m_external:1; + unsigned m_blocked:1; void mk_expr_core(); void mk_cube_core(); @@ -159,8 +160,11 @@ public: void add_skolem(app *zk, app* b); - inline void set_external(bool ext){m_external = ext;} - inline bool external() { return m_external;} + void set_external(bool ext){m_external = ext;} + bool external() { return m_external;} + + bool is_blocked() {return m_blocked;} + void set_blocked(bool v) {m_blocked=v;} bool is_inductive() const {return is_infty_level(m_lvl);} unsigned level () const {return m_lvl;} @@ -496,6 +500,9 @@ public: expr *post, app_ref_vector const &b){ return m_pobs.mk_pob(parent, level, depth, post, b); } + pob* find_pob(pob *parent, expr *post) { + return m_pobs.find_pob(parent, post); + } pob* mk_pob(pob *parent, unsigned level, unsigned depth, expr *post) { From 4339722e98d809730351d71cd60e1c35c4856105 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Wed, 27 Jun 2018 14:36:59 -0400 Subject: [PATCH 11/15] Fix segfaults in qgen --- src/muz/spacer/spacer_quant_generalizer.cpp | 64 +++++++++++---------- src/muz/spacer/spacer_util.cpp | 17 ++++-- src/muz/spacer/spacer_util.h | 2 +- 3 files changed, 46 insertions(+), 37 deletions(-) diff --git a/src/muz/spacer/spacer_quant_generalizer.cpp b/src/muz/spacer/spacer_quant_generalizer.cpp index f66fe7b29..95e884d42 100644 --- a/src/muz/spacer/spacer_quant_generalizer.cpp +++ b/src/muz/spacer/spacer_quant_generalizer.cpp @@ -114,7 +114,7 @@ void lemma_quantifier_generalizer::find_candidates(expr *e, if (!contains_selects(e, m)) return; app_ref_vector indices(m); - get_select_indices(e, indices, m); + get_select_indices(e, indices); app_ref_vector extra(m); expr_sparse_mark marked_args; @@ -155,7 +155,7 @@ bool lemma_quantifier_generalizer::match_sk_idx(expr *e, app_ref_vector const &z if (!contains_selects(e, m)) return false; app_ref_vector indicies(m); - get_select_indices(e, indicies, m); + get_select_indices(e, indicies); if (indicies.size() > 2) return false; unsigned i=0; @@ -255,15 +255,17 @@ void lemma_quantifier_generalizer::cleanup(expr_ref_vector &cube, app_ref_vector lb and ub are null if no bound was found */ -void lemma_quantifier_generalizer::mk_abs_cube(lemma_ref &lemma, app *term, var *var, +void lemma_quantifier_generalizer::mk_abs_cube(lemma_ref &lemma, app *term, + var *var, expr_ref_vector &gnd_cube, expr_ref_vector &abs_cube, - expr *&lb, expr *&ub, unsigned &stride) { + expr *&lb, expr *&ub, + unsigned &stride) { // create an abstraction function that maps candidate term to variables expr_safe_replace sub(m); // term -> var - sub.insert(term , var); + sub.insert(term, var); rational val; if (m_arith.is_numeral(term, val)) { bool is_int = val.is_int(); @@ -285,19 +287,17 @@ void lemma_quantifier_generalizer::mk_abs_cube(lemma_ref &lemma, app *term, var for (expr *lit : m_cube) { expr_ref abs_lit(m); - sub (lit, abs_lit); - if (lit == abs_lit) { - gnd_cube.push_back(lit); - } + sub(lit, abs_lit); + if (lit == abs_lit) {gnd_cube.push_back(lit);} else { expr *e1, *e2; // generalize v=num into v>=num if (m.is_eq(abs_lit, e1, e2) && (e1 == var || e2 == var)) { - if (m_arith.is_numeral(e1)) { - abs_lit = m_arith.mk_ge (var, e1); + if (m_arith.is_numeral(e1)) { + abs_lit = m_arith.mk_ge(var, e1); } else if (m_arith.is_numeral(e2)) { abs_lit = m_arith.mk_ge(var, e2); - } + } } abs_cube.push_back(abs_lit); if (contains_selects(abs_lit, m)) { @@ -464,7 +464,7 @@ bool lemma_quantifier_generalizer::generalize (lemma_ref &lemma, app *term) { if (ub) tout << mk_pp(ub, m); else tout << "none"; tout << "\n";); - if (!lb && !ub) + if (!lb && !ub) return false; // -- guess lower or upper bound if missing @@ -542,46 +542,50 @@ bool lemma_quantifier_generalizer::generalize (lemma_ref &lemma, app *term) { return false; } -bool lemma_quantifier_generalizer::find_stride(expr_ref_vector &c, expr_ref &pattern, unsigned &stride) { +bool lemma_quantifier_generalizer::find_stride(expr_ref_vector &cube, + expr_ref &pattern, + unsigned &stride) { expr_ref tmp(m); - tmp = mk_and(c); + tmp = mk_and(cube); normalize(tmp, tmp, false, true); - c.reset(); - flatten_and(tmp, c); + cube.reset(); + flatten_and(tmp, cube); app_ref_vector indices(m); - get_select_indices(pattern, indices, m); + get_select_indices(pattern, indices); - // TODO - if (indices.size() > 1) - return false; + CTRACE("spacer_qgen", indices.empty(), + tout << "Found no select indices in: " << pattern << "\n";); + + // TBD: handle multi-dimensional arrays and literals with multiple + // select terms + if (indices.size() != 1) return false; app *p_index = indices.get(0); - if (is_var(p_index)) return false; - std::vector instances; - for (expr* lit : c) { + unsigned_vector instances; + for (expr* lit : cube) { if (!contains_selects(lit, m)) continue; indices.reset(); - get_select_indices(lit, indices, m); + get_select_indices(lit, indices); - // TODO: - if (indices.size() > 1) + // TBD: handle multi-dimensional arrays + if (indices.size() != 1) continue; app *candidate = indices.get(0); unsigned size = p_index->get_num_args(); unsigned matched = 0; - for (unsigned p=0; p < size; p++) { + for (unsigned p = 0; p < size; p++) { expr *arg = p_index->get_arg(p); if (is_var(arg)) { rational val; - if (p < candidate->get_num_args() && - m_arith.is_numeral(candidate->get_arg(p), val) && + if (p < candidate->get_num_args() && + m_arith.is_numeral(candidate->get_arg(p), val) && val.is_unsigned()) { instances.push_back(val.get_unsigned()); } diff --git a/src/muz/spacer/spacer_util.cpp b/src/muz/spacer/spacer_util.cpp index 42b40c665..3ea0917b7 100644 --- a/src/muz/spacer/spacer_util.cpp +++ b/src/muz/spacer/spacer_util.cpp @@ -900,17 +900,22 @@ namespace { struct collect_indices { app_ref_vector& m_indices; array_util a; - collect_indices(app_ref_vector& indices): m_indices(indices), a(indices.get_manager()) {} + collect_indices(app_ref_vector& indices): m_indices(indices), + a(indices.get_manager()) {} void operator()(expr* n) {} void operator()(app* n) { - if (a.is_select(n)) - for (unsigned i = 1; i < n->get_num_args(); ++i) - if (is_app(n->get_arg(i))) - m_indices.push_back(to_app(n->get_arg(i))); + if (a.is_select(n)) { + // for all but first argument + for (unsigned i = 1; i < n->get_num_args(); ++i) { + expr *arg = n->get_arg(i); + if (is_app(arg)) + m_indices.push_back(to_app(arg)); + } + } } }; - void get_select_indices(expr* fml, app_ref_vector &indices, ast_manager& m) { + void get_select_indices(expr* fml, app_ref_vector &indices) { collect_indices ci(indices); for_each_expr(ci, fml); } diff --git a/src/muz/spacer/spacer_util.h b/src/muz/spacer/spacer_util.h index 9912769c5..8da574d0e 100644 --- a/src/muz/spacer/spacer_util.h +++ b/src/muz/spacer/spacer_util.h @@ -121,7 +121,7 @@ namespace spacer { void mbqi_project(model &mdl, app_ref_vector &vars, expr_ref &fml); bool contains_selects (expr* fml, ast_manager& m); - void get_select_indices (expr* fml, app_ref_vector& indices, ast_manager& m); + void get_select_indices (expr* fml, app_ref_vector& indices); void find_decls (expr* fml, app_ref_vector& decls, std::string& prefix); From 704c19920d7f15f58ae1d7433c5df4d14b2d1b2e Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Wed, 27 Jun 2018 16:40:07 -0400 Subject: [PATCH 12/15] Only 10 levels of weakness --- src/muz/spacer/spacer_context.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index 142cfa898..575c9993b 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -3474,7 +3474,7 @@ lbool context::expand_pob(pob& n, pob_ref_buffer &out) } case l_undef: // something went wrong - if (n.weakness() < 100 /* MAX_WEAKENSS */) { + if (n.weakness() < 10 /* MAX_WEAKENSS */) { bool has_new_child = false; SASSERT(m_weak_abs); m_stats.m_expand_pob_undef++; From 7c924c49f679605f062b15bd92005e550cbc48f6 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Wed, 27 Jun 2018 16:40:49 -0400 Subject: [PATCH 13/15] Do not evaluate quantified formulas in a model --- src/muz/spacer/spacer_context.cpp | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index 575c9993b..8eee087e6 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -1184,7 +1184,16 @@ expr_ref pred_transformer::get_origin_summary (model &mdl, } // bail out of if the model is insufficient - if (!mdl.is_true(summary)) return expr_ref(m); + // (skip quantified lemmas cause we can't validate them in the model) + // TBD: for quantified lemmas use current instances + flatten_and(summary); + for (auto *s : summary) { + if (!is_quantifier(s) && !mdl.is_true(s)) { + TRACE("spacer", tout << "Summary not true in the model: " + << mk_pp(s, m) << "\n";); + return expr_ref(m); + } + } // -- pick an implicant expr_ref_vector lits(m); From 0e5434ce0cd74afe61f268393c51812a2318dcc7 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Wed, 27 Jun 2018 22:42:19 -0400 Subject: [PATCH 14/15] Debug prints --- src/muz/spacer/spacer_context.cpp | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index 8eee087e6..b034a8fd5 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -279,6 +279,8 @@ pob *derivation::create_next_child(model &mdl) m_evars.reset(); pt().mbp(vars, m_trans, mdl, true, pt().get_context().use_ground_pob()); + CTRACE("spacer", !vars.empty(), + tout << "Failed to eliminate: " << vars << "\n";); m_evars.append (vars); vars.reset(); } @@ -308,6 +310,8 @@ pob *derivation::create_next_child(model &mdl) vars.append(m_evars); pt().mbp(vars, post, mdl, true, pt().get_context().use_ground_pob()); + CTRACE("spacer", !vars.empty(), + tout << "Failed to eliminate: " << vars << "\n";); //qe::reduce_array_selects (*mev.get_model (), post); } else { @@ -411,6 +415,8 @@ pob *derivation::create_next_child () this->pt().mbp(vars, m_trans, *mdl, true, this->pt().get_context().use_ground_pob()); // keep track of implicitly quantified variables + CTRACE("spacer", !vars.empty(), + tout << "Failed to eliminate: " << vars << "\n";); m_evars.append (vars); vars.reset(); } From 4abab8aaf535ed6c7cac04d37893fd57390facd6 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Wed, 27 Jun 2018 22:45:38 -0400 Subject: [PATCH 15/15] Fix bug in qe_term_graph In merge, parents of A instead of parents of B were traversed. Among other things, it created stale marks that caused an infinite loop in to_lits() --- src/qe/qe_term_graph.cpp | 27 ++++++++++++++++++--------- src/qe/qe_term_graph.h | 1 + 2 files changed, 19 insertions(+), 9 deletions(-) diff --git a/src/qe/qe_term_graph.cpp b/src/qe/qe_term_graph.cpp index 5cf1206a3..e9ec3d4b7 100644 --- a/src/qe/qe_term_graph.cpp +++ b/src/qe/qe_term_graph.cpp @@ -200,7 +200,8 @@ namespace qe { } std::ostream& display(std::ostream& out) const { - out << get_id() << ": " << m_expr << " - "; + out << get_id() << ": " << m_expr + << (is_root() ? " R" : "") << " - "; term const* r = &this->get_next(); while (r != this) { out << r->get_id() << " "; @@ -371,20 +372,20 @@ namespace qe { } void term_graph::merge(term &t1, term &t2) { - // -- merge might invalidate term2app cache - m_term2app.reset(); - m_pinned.reset(); - term *a = &t1.get_root(); term *b = &t2.get_root(); if (a == b) return; + // -- merge might invalidate term2app cache + m_term2app.reset(); + m_pinned.reset(); + if (a->get_class_size() > b->get_class_size()) { std::swap(a, b); } - // Remove parents of it from the cg table. + // Remove parents of b from the cg table. for (term* p : term::parents(b)) { if (!p->is_marked()) { p->set_mark(true); @@ -401,7 +402,7 @@ namespace qe { a->merge_eq_class(*b); // Insert parents of b's old equilvalence class into the cg table - for (term* p : term::parents(a)) { + for (term* p : term::parents(b)) { if (p->is_marked()) { term* p_old = m_cg_table.insert_if_not_there(p); p->set_mark(false); @@ -412,6 +413,7 @@ namespace qe { } } } + SASSERT(marks_are_clear()); } expr* term_graph::mk_app_core (expr *e) { @@ -484,10 +486,16 @@ namespace qe { } } + bool term_graph::marks_are_clear() { + for (term * t : m_terms) { + if (t->is_marked()) return false; + } + return true; + } + /// Order of preference for roots of equivalence classes /// XXX This should be factored out to let clients control the preference bool term_graph::term_lt(term const &t1, term const &t2) { - // prefer constants over applications // prefer uninterpreted constants over values // prefer smaller expressions over larger ones @@ -521,6 +529,7 @@ namespace qe { /// Choose better roots for equivalence classes void term_graph::pick_roots() { + SASSERT(marks_are_clear()); for (term* t : m_terms) { if (!t->is_marked() && t->is_root()) pick_root(*t); @@ -589,7 +598,7 @@ namespace qe { // prefer a node that resembles current child, // otherwise, pick a root representative, if present. if (m_term2app.find(ch->get_id(), e)) - kids.push_back(e); + kids.push_back(e); else if (m_root2rep.find(ch->get_root().get_id(), e)) kids.push_back(e); else diff --git a/src/qe/qe_term_graph.h b/src/qe/qe_term_graph.h index 2ab234a96..0c66f4193 100644 --- a/src/qe/qe_term_graph.h +++ b/src/qe/qe_term_graph.h @@ -75,6 +75,7 @@ namespace qe { void pick_roots(); void reset_marks(); + bool marks_are_clear(); expr* mk_app_core(expr* a); expr_ref mk_app(term const &t);