From d9100437ce377bf185cb0b3f9b2da8e79ca9ce60 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Tue, 26 Jun 2018 11:33:54 -0400 Subject: [PATCH 01/32] 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/32] 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/32] 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/32] 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/32] 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/32] 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/32] 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/32] 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/32] 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/32] 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/32] 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/32] 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/32] 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/32] 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/32] 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); From 5de6628a5d72a0600222b66cedc4ae908d40d1dc Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Thu, 28 Jun 2018 10:31:38 +0100 Subject: [PATCH 16/32] remove spurious copies and inc_refs around ref_vector --- src/ackermannization/ackermannize_bv_tactic.cpp | 2 +- src/ackermannization/ackr_model_converter.cpp | 2 +- src/ackermannization/lackr.cpp | 17 ++++++----------- src/ackermannization/lackr.h | 6 +++--- src/api/api_context.cpp | 5 ++--- src/ast/ast_smt2_pp.cpp | 2 +- src/ast/fpa/fpa2bv_converter.cpp | 4 ++-- src/ast/rewriter/bv_trailing.cpp | 6 +++--- src/ast/substitution/substitution.cpp | 6 +++--- src/qe/qe_lite.cpp | 10 +++++----- src/smt/smt_context.cpp | 4 ++-- src/smt/smt_context.h | 6 ------ src/smt/smt_context_pp.cpp | 4 ++-- src/smt/smt_justification.cpp | 9 ++------- src/tactic/smtlogics/qfufbv_tactic.cpp | 2 +- src/util/ref_vector.h | 17 +++++++++++++++-- 16 files changed, 49 insertions(+), 53 deletions(-) diff --git a/src/ackermannization/ackermannize_bv_tactic.cpp b/src/ackermannization/ackermannize_bv_tactic.cpp index 3ffee518e..98417cc7b 100644 --- a/src/ackermannization/ackermannize_bv_tactic.cpp +++ b/src/ackermannization/ackermannize_bv_tactic.cpp @@ -35,7 +35,7 @@ public: fail_if_proof_generation("ackermannize", g); TRACE("ackermannize", g->display(tout << "in\n");); - expr_ref_vector flas(m); + ptr_vector flas; const unsigned sz = g->size(); for (unsigned i = 0; i < sz; i++) flas.push_back(g->form(i)); lackr lackr(m, m_p, m_st, flas, nullptr); diff --git a/src/ackermannization/ackr_model_converter.cpp b/src/ackermannization/ackr_model_converter.cpp index 9e87a1a69..c5e04ab23 100644 --- a/src/ackermannization/ackr_model_converter.cpp +++ b/src/ackermannization/ackr_model_converter.cpp @@ -134,7 +134,7 @@ void ackr_model_converter::add_entry(model_evaluator & evaluator, info->abstract(arg, aarg); expr_ref arg_value(m); evaluator(aarg, arg_value); - args.push_back(arg_value); + args.push_back(std::move(arg_value)); } if (fi->get_entry(args.c_ptr()) == nullptr) { TRACE("ackr_model", diff --git a/src/ackermannization/lackr.cpp b/src/ackermannization/lackr.cpp index b739af9d3..8c18df7b2 100644 --- a/src/ackermannization/lackr.cpp +++ b/src/ackermannization/lackr.cpp @@ -23,8 +23,8 @@ #include "ast/for_each_expr.h" #include "model/model_smt2_pp.h" -lackr::lackr(ast_manager& m, params_ref p, lackr_stats& st, expr_ref_vector& formulas, - solver * uffree_solver) +lackr::lackr(ast_manager& m, const params_ref& p, lackr_stats& st, + const ptr_vector& formulas, solver * uffree_solver) : m_m(m) , m_p(p) , m_formulas(formulas) @@ -173,11 +173,10 @@ void lackr::abstract() { } m_info->seal(); // perform abstraction of the formulas - const unsigned sz = m_formulas.size(); - for (unsigned i = 0; i < sz; ++i) { + for (expr * f : m_formulas) { expr_ref a(m_m); - m_info->abstract(m_formulas.get(i), a); - m_abstr.push_back(a); + m_info->abstract(f, a); + m_abstr.push_back(std::move(a)); } } @@ -249,13 +248,9 @@ lbool lackr::lazy() { // Collect all uninterpreted terms, skipping 0-arity. // bool lackr::collect_terms() { - ptr_vector stack; + ptr_vector stack = m_formulas; expr * curr; expr_mark visited; - for(unsigned i = 0; i < m_formulas.size(); ++i) { - stack.push_back(m_formulas.get(i)); - TRACE("lackr", tout << "infla: " <& formulas, solver * uffree_solver); ~lackr(); void updt_params(params_ref const & _p); @@ -82,7 +82,7 @@ class lackr { typedef ackr_helper::app_set app_set; ast_manager& m_m; params_ref m_p; - expr_ref_vector m_formulas; + const ptr_vector& m_formulas; expr_ref_vector m_abstr; fun2terms_map m_fun2terms; ackr_info_ref m_info; diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 5993e9fdd..295977a06 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -218,10 +218,9 @@ namespace api { // Corner case bug: n may be in m_last_result, and this is the only reference to n. // When, we execute reset() it is deleted // To avoid this bug, I bump the reference counter before reseting m_last_result - m().inc_ref(n); + ast_ref node(n, m()); m_last_result.reset(); - m_last_result.push_back(n); - m().dec_ref(n); + m_last_result.push_back(std::move(node)); } else { m_ast_trail.push_back(n); diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp index 5cd09263d..3a55bbb0b 100644 --- a/src/ast/ast_smt2_pp.cpp +++ b/src/ast/ast_smt2_pp.cpp @@ -1199,7 +1199,7 @@ void mk_smt2_format(unsigned sz, expr * const* es, smt2_pp_environment & env, pa for (unsigned i = 0; i < sz; ++i) { format_ref fr(fm(m)); pr(es[i], num_vars, var_prefix, fr, var_names); - fmts.push_back(fr); + fmts.push_back(std::move(fr)); } r = mk_seq(m, fmts.c_ptr(), fmts.c_ptr() + fmts.size(), f2f()); } diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index b079fc2ca..dd3f35a2a 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -3108,12 +3108,12 @@ void fpa2bv_converter::mk_to_ieee_bv_unspecified(func_decl * f, unsigned num, ex expr_ref exp_bv(m), exp_all_ones(m); exp_bv = m_bv_util.mk_extract(ebits+sbits-2, sbits-1, result); exp_all_ones = m.mk_eq(exp_bv, m_bv_util.mk_bv_neg(m_bv_util.mk_numeral(1, ebits))); - m_extra_assertions.push_back(exp_all_ones); + m_extra_assertions.push_back(std::move(exp_all_ones)); expr_ref sig_bv(m), sig_is_non_zero(m); sig_bv = m_bv_util.mk_extract(sbits-2, 0, result); sig_is_non_zero = m.mk_not(m.mk_eq(sig_bv, m_bv_util.mk_numeral(0, sbits-1))); - m_extra_assertions.push_back(sig_is_non_zero); + m_extra_assertions.push_back(std::move(sig_is_non_zero)); } TRACE("fpa2bv_to_ieee_bv_unspecified", tout << "result=" << mk_ismt2_pp(result, m) << std::endl;); diff --git a/src/ast/rewriter/bv_trailing.cpp b/src/ast/rewriter/bv_trailing.cpp index ad9350eca..433ef6f66 100644 --- a/src/ast/rewriter/bv_trailing.cpp +++ b/src/ast/rewriter/bv_trailing.cpp @@ -125,7 +125,7 @@ struct bv_trailing::imp { for (unsigned i = 0; i < num; ++i) { expr * const curr = a->get_arg(i); VERIFY(to_rm == remove_trailing(curr, to_rm, tmp, depth - 1)); - new_args.push_back(tmp); + new_args.push_back(std::move(tmp)); } result = m.mk_app(m_util.get_fid(), OP_BADD, new_args.size(), new_args.c_ptr()); return to_rm; @@ -150,7 +150,7 @@ struct bv_trailing::imp { numeral c_val; unsigned c_sz; if (!m_util.is_numeral(tmp, c_val, c_sz) || !c_val.is_one()) - new_args.push_back(tmp); + new_args.push_back(std::move(tmp)); const unsigned sz = m_util.get_bv_size(coefficient); const unsigned new_sz = sz - retv; @@ -204,7 +204,7 @@ struct bv_trailing::imp { expr_ref_vector new_args(m); for (unsigned j = 0; j < i; ++j) new_args.push_back(a->get_arg(j)); - if (new_last) new_args.push_back(new_last); + if (new_last) new_args.push_back(std::move(new_last)); result = new_args.size() == 1 ? new_args.get(0) : m_util.mk_concat(new_args.size(), new_args.c_ptr()); return retv; diff --git a/src/ast/substitution/substitution.cpp b/src/ast/substitution/substitution.cpp index 39e9e07a2..7e981aab8 100644 --- a/src/ast/substitution/substitution.cpp +++ b/src/ast/substitution/substitution.cpp @@ -196,16 +196,16 @@ void substitution::apply(unsigned num_actual_offsets, unsigned const * deltas, e expr_ref_vector pats(m_manager), no_pats(m_manager); for (unsigned i = 0; i < q->get_num_patterns(); ++i) { subst.apply(num_actual_offsets, deltas, expr_offset(q->get_pattern(i), off), s1, t1, er); - pats.push_back(er); + pats.push_back(std::move(er)); } for (unsigned i = 0; i < q->get_num_no_patterns(); ++i) { subst.apply(num_actual_offsets, deltas, expr_offset(q->get_no_pattern(i), off), s1, t1, er); - no_pats.push_back(er); + no_pats.push_back(std::move(er)); } subst.apply(num_actual_offsets, deltas, body, s1, t1, er); er = m_manager.update_quantifier(q, pats.size(), pats.c_ptr(), no_pats.size(), no_pats.c_ptr(), er); m_todo.pop_back(); - m_new_exprs.push_back(er); + m_new_exprs.push_back(std::move(er)); m_apply_cache.insert(n, er); break; } diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp index 3223706d4..da45d17ca 100644 --- a/src/qe/qe_lite.cpp +++ b/src/qe/qe_lite.cpp @@ -320,8 +320,8 @@ namespace eq { << "sz is " << sz << "\n" << "subst_map[inx]: " << mk_pp(m_subst_map.get(inx), m) << "\n";); SASSERT(m_subst_map.get(inx) == nullptr); - m_subst_map[inx] = r; m_subst.update_inv_binding_at(inx, r); + m_subst_map[inx] = std::move(r); } } @@ -470,7 +470,7 @@ namespace eq { m_var2pos[idx] = i; def_count++; largest_vinx = std::max(idx, largest_vinx); - m_new_exprs.push_back(t); + m_new_exprs.push_back(std::move(t)); } else if (!m.is_value(m_map[idx])) { // check if the new definition is simpler @@ -482,7 +482,7 @@ namespace eq { m_pos2var[i] = idx; m_var2pos[idx] = i; m_map[idx] = t; - m_new_exprs.push_back(t); + m_new_exprs.push_back(std::move(t)); } // -- prefer ground else if (is_app(t) && to_app(t)->is_ground() && @@ -492,7 +492,7 @@ namespace eq { m_pos2var[i] = idx; m_var2pos[idx] = i; m_map[idx] = t; - m_new_exprs.push_back(t); + m_new_exprs.push_back(std::move(t)); } // -- prefer constants else if (is_uninterp_const(t) @@ -501,7 +501,7 @@ namespace eq { m_pos2var[i] = idx; m_var2pos[idx] = i; m_map[idx] = t; - m_new_exprs.push_back(t); + m_new_exprs.push_back(std::move(t)); } TRACE ("qe_def", tout << "Replacing definition of VAR " << idx << " from " diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index fd9b27069..73a3c27bd 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -1594,7 +1594,7 @@ namespace smt { for (literal lit : m_assigned_literals) { expr_ref e(m_manager); literal2expr(lit, e); - assignments.push_back(e); + assignments.push_back(std::move(e)); } } @@ -4180,7 +4180,7 @@ namespace smt { SASSERT(get_justification(guess.var()).get_kind() == b_justification::AXIOM); expr_ref lit(m_manager); literal2expr(guess, lit); - result.push_back(lit); + result.push_back(std::move(lit)); } } diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 48b689bd7..4f7c8073e 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1115,8 +1115,6 @@ namespace smt { void internalize_assertions(); - void assert_assumption(expr * a); - bool validate_assumptions(expr_ref_vector const& asms); void init_assumptions(expr_ref_vector const& asms); @@ -1129,8 +1127,6 @@ namespace smt { void reset_assumptions(); - void reset_clause(); - void add_theory_assumptions(expr_ref_vector & theory_assumptions); lbool mk_unsat_core(lbool result); @@ -1585,8 +1581,6 @@ namespace smt { //proof * const * get_asserted_formula_proofs() const { return m_asserted_formulas.get_formula_proofs(); } - void get_assumptions_core(ptr_vector & result); - void get_assertions(ptr_vector & result) { m_asserted_formulas.get_assertions(result); } void display(std::ostream & out) const; diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp index 19247c1d9..29c624bb2 100644 --- a/src/smt/smt_context_pp.cpp +++ b/src/smt/smt_context_pp.cpp @@ -409,11 +409,11 @@ namespace smt { for (unsigned i = 0; i < num_antecedents; i++) { literal l = antecedents[i]; literal2expr(l, n); - fmls.push_back(n); + fmls.push_back(std::move(n)); } if (consequent != false_literal) { literal2expr(~consequent, n); - fmls.push_back(n); + fmls.push_back(std::move(n)); } if (logic != symbol::null) out << "(set-logic " << logic << ")\n"; visitor.collect(fmls); diff --git a/src/smt/smt_justification.cpp b/src/smt/smt_justification.cpp index 4ac176a2b..fc9307792 100644 --- a/src/smt/smt_justification.cpp +++ b/src/smt/smt_justification.cpp @@ -281,7 +281,7 @@ namespace smt { for (unsigned i = 0; i < m_num_literals; i++) { expr_ref l(m); ctx.literal2expr(m_literals[i], l); - lits.push_back(l); + lits.push_back(std::move(l)); } if (lits.size() == 1) return m.mk_th_lemma(m_th_id, lits.get(0), 0, nullptr, m_params.size(), m_params.c_ptr()); @@ -407,12 +407,7 @@ namespace smt { for (unsigned i = 0; i < m_num_literals; i++) { bool sign = GET_TAG(m_literals[i]) != 0; expr * v = UNTAG(expr*, m_literals[i]); - expr_ref l(m); - if (sign) - l = m.mk_not(v); - else - l = v; - lits.push_back(l); + lits.push_back(sign ? m.mk_not(v) : v); } if (lits.size() == 1) return m.mk_th_lemma(m_th_id, lits.get(0), 0, nullptr, m_params.size(), m_params.c_ptr()); diff --git a/src/tactic/smtlogics/qfufbv_tactic.cpp b/src/tactic/smtlogics/qfufbv_tactic.cpp index 3bd28ad6d..a4e169856 100644 --- a/src/tactic/smtlogics/qfufbv_tactic.cpp +++ b/src/tactic/smtlogics/qfufbv_tactic.cpp @@ -62,7 +62,7 @@ public: TRACE("qfufbv_ackr_tactic", g->display(tout << "goal:\n");); // running implementation - expr_ref_vector flas(m); + ptr_vector flas; const unsigned sz = g->size(); for (unsigned i = 0; i < sz; i++) flas.push_back(g->form(i)); scoped_ptr uffree_solver = setup_sat(); diff --git a/src/util/ref_vector.h b/src/util/ref_vector.h index f340d8886..1e6525a06 100644 --- a/src/util/ref_vector.h +++ b/src/util/ref_vector.h @@ -99,6 +99,13 @@ public: return *this; } + template + ref_vector_core& push_back(obj_ref && n) { + m_nodes.push_back(n.get()); + n.steal(); + return *this; + } + void pop_back() { SASSERT(!m_nodes.empty()); T * n = m_nodes.back(); @@ -253,6 +260,13 @@ public: return *this; } + template + element_ref & operator=(obj_ref && n) { + m_manager.dec_ref(m_ref); + m_ref = n.steal(); + return *this; + } + T * get() const { return m_ref; } @@ -288,9 +302,8 @@ public: return *this; } -private: // prevent abuse: - ref_vector & operator=(ref_vector const & other); + ref_vector & operator=(ref_vector const & other) = delete; }; template From 46799cb3f067a3aff3df66f524b034daf388d0f2 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Thu, 28 Jun 2018 18:25:22 +0100 Subject: [PATCH 17/32] MAM: check soft limits before calling the interpreter --- src/smt/mam.cpp | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp index e2a9cbed4..978a1a8e1 100644 --- a/src/smt/mam.cpp +++ b/src/smt/mam.cpp @@ -2000,7 +2000,8 @@ namespace smt { if (t->filter_candidates()) { for (enode* app : t->get_candidates()) { if (!app->is_marked() && app->is_cgr()) { - execute_core(t, app); + if (m_context.resource_limits_exceeded() || !execute_core(t, app)) + return; app->set_mark(); } } @@ -2014,14 +2015,15 @@ namespace smt { TRACE("trigger_bug", tout << "candidate\n" << mk_ismt2_pp(app->get_owner(), m_ast_manager) << "\n";); if (app->is_cgr()) { TRACE("trigger_bug", tout << "is_cgr\n";); - execute_core(t, app); + if (m_context.resource_limits_exceeded() || !execute_core(t, app)) + return; } } } } // init(t) must be invoked before execute_core - void execute_core(code_tree * t, enode * n); + bool execute_core(code_tree * t, enode * n); // Return the min, max generation of the enodes in m_pattern_instances. @@ -2250,7 +2252,7 @@ namespace smt { display_instr_input_reg(out, m_pc); } - void interpreter::execute_core(code_tree * t, enode * n) { + bool interpreter::execute_core(code_tree * t, enode * n) { TRACE("trigger_bug", tout << "interpreter::execute_core\n"; t->display(tout); tout << "\nenode\n" << mk_ismt2_pp(n->get_owner(), m_ast_manager) << "\n";); unsigned since_last_check = 0; @@ -2494,7 +2496,7 @@ namespace smt { #define ON_MATCH(NUM) \ m_max_generation = std::max(m_max_generation, get_max_generation(NUM, m_bindings.begin())); \ if (m_context.get_cancel_flag()) { \ - return; \ + return false; \ } \ m_mam.on_match(static_cast(m_pc)->m_qa, \ static_cast(m_pc)->m_pat, \ @@ -2647,7 +2649,7 @@ namespace smt { #ifdef _PROFILE_MAM t->get_watch().stop(); #endif - return; // no more alternatives + return true; // no more alternatives } backtrack_point & bp = m_backtrack_stack[m_top - 1]; m_max_generation = bp.m_old_max_generation; @@ -2675,7 +2677,7 @@ namespace smt { #ifdef _PROFILE_MAM t->get_watch().stop(); #endif - return; + return false; } } From e8e27f0daf572f8e6f7d9bb4bd3a2b5c76117888 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Thu, 28 Jun 2018 10:59:28 -0400 Subject: [PATCH 18/32] Don't simplify bounds when normalizing a lemma --- src/muz/spacer/spacer_context.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index b034a8fd5..b6d9f810d 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -538,7 +538,8 @@ void lemma::mk_expr_core() { SASSERT(!m_cube.empty()); m_body = ::mk_and(m_cube); // normalize works better with a cube - normalize(m_body, m_body); + normalize(m_body, m_body, false /* no simplify bounds */, false /* term_graph */); + m_body = ::push_not(m_body); if (!m_zks.empty() && has_zk_const(m_body)) { From a8c9e3a837fccf687de01babdccad2b234f25683 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Thu, 28 Jun 2018 11:13:25 -0400 Subject: [PATCH 19/32] Bug fix in qgen --- src/muz/spacer/spacer_quant_generalizer.cpp | 26 ++++++++++----------- 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/src/muz/spacer/spacer_quant_generalizer.cpp b/src/muz/spacer/spacer_quant_generalizer.cpp index 95e884d42..834f0d8ae 100644 --- a/src/muz/spacer/spacer_quant_generalizer.cpp +++ b/src/muz/spacer/spacer_quant_generalizer.cpp @@ -473,7 +473,7 @@ bool lemma_quantifier_generalizer::generalize (lemma_ref &lemma, app *term) { lb = abs_cube.back(); } if (!ub) { - abs_cube.push_back (m_arith.mk_lt(var, term)); + abs_cube.push_back (m_arith.mk_le(var, term)); ub = abs_cube.back(); } @@ -489,10 +489,10 @@ bool lemma_quantifier_generalizer::generalize (lemma_ref &lemma, app *term) { TRACE("spacer_qgen", tout << "mod=" << mod << " init=" << init << " stride=" << stride << "\n"; tout.flush();); - abs_cube.push_back(m.mk_eq( - m_arith.mk_mod(var, m_arith.mk_numeral(rational(stride), true)), - m_arith.mk_numeral(rational(mod), true))); - } + abs_cube.push_back + (m.mk_eq(m_arith.mk_mod(var, + m_arith.mk_numeral(rational(stride), true)), + m_arith.mk_numeral(rational(mod), true)));} // skolemize expr_ref gnd(m); @@ -512,21 +512,21 @@ bool lemma_quantifier_generalizer::generalize (lemma_ref &lemma, app *term) { << "New CUBE is: " << gnd_cube << "\n";); SASSERT(zks.size() >= static_cast(m_offset)); - // lift quantified variables to top of select + // lift quantified variables to top of select expr_ref ext_bind(m); ext_bind = term; cleanup(gnd_cube, zks, ext_bind); - // XXX better do that check before changing bind in cleanup() - // XXX Or not because substitution might introduce _n variable into bind + // XXX better do that check before changing bind in cleanup() + // XXX Or not because substitution might introduce _n variable into bind if (m_ctx.get_manager().is_n_formula(ext_bind)) { - // XXX this creates an instance, but not necessarily the needed one + // XXX this creates an instance, but not necessarily the needed one - // XXX This is sound because any instance of - // XXX universal quantifier is sound + // XXX This is sound because any instance of + // XXX universal quantifier is sound - // XXX needs better long term solution. leave - // comment here for the future + // XXX needs better long term solution. leave + // comment here for the future m_ctx.get_manager().formula_n2o(ext_bind, ext_bind, 0); } From a63e4b48cae1a98c967cace1aa0f79a3d63575e2 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Thu, 28 Jun 2018 14:21:32 -0400 Subject: [PATCH 20/32] Fix order of arguments when normalizing a conjunction --- src/muz/spacer/spacer_util.cpp | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/muz/spacer/spacer_util.cpp b/src/muz/spacer/spacer_util.cpp index 3ea0917b7..ec01218f1 100644 --- a/src/muz/spacer/spacer_util.cpp +++ b/src/muz/spacer/spacer_util.cpp @@ -666,9 +666,6 @@ namespace { flatten_and(out, v); if (v.size() > 1) { - // sort arguments of the top-level and - std::stable_sort(v.c_ptr(), v.c_ptr() + v.size(), ast_lt_proc()); - if (use_simplify_bounds) { // remove redundant inequalities simplify_bounds(v); @@ -680,6 +677,8 @@ namespace { v.reset(); egraph.to_lits(v); } + // sort arguments of the top-level and + std::stable_sort(v.c_ptr(), v.c_ptr() + v.size(), ast_lt_proc()); TRACE("spacer_normalize", tout << "Normalized:\n" From 41a05e9d587b31c9b342b46a8636e38da05511e7 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Thu, 28 Jun 2018 14:23:14 -0400 Subject: [PATCH 21/32] Add methods to print pob --- src/muz/spacer/spacer_context.cpp | 14 ++++++++++---- src/muz/spacer/spacer_context.h | 4 ++++ 2 files changed, 14 insertions(+), 4 deletions(-) diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index b6d9f810d..07dc1a372 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -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 @@ -2174,9 +2182,7 @@ pob* pred_transformer::pob_manager::mk_pob(pob *parent, p.set_post(post, b); if (m_pobs.contains(p.post())) { - auto &buf = m_pobs[p.post()]; - for (unsigned i = 0, sz = buf.size(); i < sz; ++i) { - pob *f = buf.get(i); + for (auto *f : m_pobs[p.post()]) { if (f->parent() == parent && !f->is_in_queue()) { f->inherit(p); return f; diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h index 93c2337e6..36f898ed1 100644 --- a/src/muz/spacer/spacer_context.h +++ b/src/muz/spacer/spacer_context.h @@ -693,6 +693,7 @@ public: if (m_ref_count == 0) {dealloc(this);} } + std::ostream &display(std::ostream &out, bool full = false) const; class on_expand_event { 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 { bool operator() (const pob *pn1, const pob *pn2) const; From 6422fa37392f2904bd3c5cba07b8ea4ef4a47bcf Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Thu, 28 Jun 2018 15:35:02 -0400 Subject: [PATCH 22/32] Fix arithmetic equality solver in qgen --- src/muz/spacer/spacer_quant_generalizer.cpp | 17 ++++++++++++----- 1 file changed, 12 insertions(+), 5 deletions(-) diff --git a/src/muz/spacer/spacer_quant_generalizer.cpp b/src/muz/spacer/spacer_quant_generalizer.cpp index 834f0d8ae..23344fd6f 100644 --- a/src/muz/spacer/spacer_quant_generalizer.cpp +++ b/src/muz/spacer/spacer_quant_generalizer.cpp @@ -191,9 +191,15 @@ expr* times_minus_one(expr *e, arith_util &arith) { Find sub-expression of the form (select A (+ sk!0 t)) and replaces (+ sk!0 t) --> sk!0 and sk!0 --> (+ sk!0 (* (- 1) t)) - Current implementation is an ugly hack for one special case + + rewrites bind to (+ bsk!0 t) where bsk!0 is the original binding for sk!0 + + Current implementation is an ugly hack for one special + case. Should be rewritten based on an equality solver from qe */ -void lemma_quantifier_generalizer::cleanup(expr_ref_vector &cube, app_ref_vector const &zks, expr_ref &bind) { +void lemma_quantifier_generalizer::cleanup(expr_ref_vector &cube, + app_ref_vector const &zks, + expr_ref &bind) { if (zks.size() != 1) return; arith_util arith(m); @@ -219,8 +225,8 @@ void lemma_quantifier_generalizer::cleanup(expr_ref_vector &cube, app_ref_vector kids_bind.push_back(bind); } else { - kids.push_back (times_minus_one(arg, arith)); - kids_bind.push_back (times_minus_one(arg, arith)); + kids.push_back(times_minus_one(arg, arith)); + kids_bind.push_back(arg); } } if (!found) continue; @@ -228,7 +234,8 @@ void lemma_quantifier_generalizer::cleanup(expr_ref_vector &cube, app_ref_vector rep = arith.mk_add(kids.size(), kids.c_ptr()); bind = arith.mk_add(kids_bind.size(), kids_bind.c_ptr()); TRACE("spacer_qgen", - tout << "replace " << mk_pp(idx, m) << " with " << mk_pp(rep, m) << "\n";); + tout << "replace " << mk_pp(idx, m) << " with " << mk_pp(rep, m) << "\n" + << "bind is: " << bind << "\n";); break; } } From bd63458778d020fb037ff11af2e2d597a865a00d Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Thu, 28 Jun 2018 15:35:49 -0400 Subject: [PATCH 23/32] Shuffle assumptions on every call Order of assumptions appears to make a huge difference on what lemmas are discovered. Shuffling the assumptions ensures that the solver is never stuck with any bad order. --- src/muz/spacer/spacer_prop_solver.cpp | 3 +++ src/muz/spacer/spacer_prop_solver.h | 2 ++ 2 files changed, 5 insertions(+) diff --git a/src/muz/spacer/spacer_prop_solver.cpp b/src/muz/spacer/spacer_prop_solver.cpp index 7bd21a1b5..004ea6754 100644 --- a/src/muz/spacer/spacer_prop_solver.cpp +++ b/src/muz/spacer/spacer_prop_solver.cpp @@ -56,6 +56,7 @@ prop_solver::prop_solver(ast_manager &m, m_use_push_bg(p.spacer_keep_proxy()) { + m_random.set_seed(p.spacer_random_seed()); m_solvers[0] = solver0; m_solvers[1] = solver1; @@ -363,6 +364,8 @@ lbool prop_solver::check_assumptions(const expr_ref_vector & _hard, hard.append(_hard.size(), _hard.c_ptr()); flatten_and(hard); + shuffle(hard.size(), hard.c_ptr(), m_random); + m_ctx = m_contexts [solver_id == 0 ? 0 : 0 /* 1 */].get(); // can be disabled if use_push_bg == true diff --git a/src/muz/spacer/spacer_prop_solver.h b/src/muz/spacer/spacer_prop_solver.h index 1db65dc3e..0eed969bd 100644 --- a/src/muz/spacer/spacer_prop_solver.h +++ b/src/muz/spacer/spacer_prop_solver.h @@ -61,6 +61,8 @@ private: bool m_use_push_bg; unsigned m_current_level; // set when m_in_level + random_gen m_random; + void assert_level_atoms(unsigned level); void ensure_level(unsigned lvl); From 5e87d7c4a3f9ac6553e13a687cda509d1e9c7bdf Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Thu, 28 Jun 2018 15:37:18 -0400 Subject: [PATCH 24/32] Formatting: move q3 parameters closer together --- src/muz/base/fp_params.pyg | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/muz/base/fp_params.pyg b/src/muz/base/fp_params.pyg index 31ab3a358..981b99de7 100644 --- a/src/muz/base/fp_params.pyg +++ b/src/muz/base/fp_params.pyg @@ -150,6 +150,8 @@ def_module_params('fp', ('spacer.keep_proxy', BOOL, True, 'keep proxy variables (internal parameter)'), ('spacer.q3', BOOL, True, 'Allow quantified lemmas in frames'), ('spacer.q3.instantiate', BOOL, True, 'Instantiate quantified lemmas'), + ('spacer.q3.use_qgen', BOOL, False, 'use quantified lemma generalizer'), + ('spacer.q3.qgen.normalize', BOOL, True, 'normalize cube before quantified generalization'), ('spacer.iuc', UINT, 1, '0 = use old implementation of unsat-core-generation, ' + '1 = use new implementation of IUC generation, ' + @@ -164,8 +166,6 @@ def_module_params('fp', ('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)'), ('spacer.simplify_pob', BOOL, False, 'simplify pobs by removing redundant constraints'), - ('spacer.q3.use_qgen', BOOL, False, 'use quantified lemma generalizer'), - ('spacer.q3.qgen.normalize', BOOL, True, 'normalize cube before quantified generalization'), ('spacer.p3.share_lemmas', BOOL, False, 'Share frame lemmas'), ('spacer.p3.share_invariants', BOOL, False, "Share invariants lemmas"), ('spacer.min_level', UINT, 0, 'Minimal level to explore'), From 9b578083f546436d8ace536141a5b6e8077c325c Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Thu, 28 Jun 2018 16:50:43 -0400 Subject: [PATCH 25/32] Avoid non-linear arithmetic in qgen --- src/muz/spacer/spacer_quant_generalizer.cpp | 51 +++++++++++++++++++++ 1 file changed, 51 insertions(+) diff --git a/src/muz/spacer/spacer_quant_generalizer.cpp b/src/muz/spacer/spacer_quant_generalizer.cpp index 23344fd6f..dd40d8546 100644 --- a/src/muz/spacer/spacer_quant_generalizer.cpp +++ b/src/muz/spacer/spacer_quant_generalizer.cpp @@ -80,6 +80,51 @@ struct index_lt_proc : public std::binary_function { } }; + + struct has_nlira_functor { + struct found{}; + + ast_manager &m; + arith_util u; + + has_nlira_functor(ast_manager &_m) : m(_m), u(m) {} + + void operator()(var *) {} + void operator()(quantifier *) {} + void operator()(app *n) { + family_id fid = n->get_family_id(); + if (fid != u.get_family_id()) return; + + switch(n->get_decl_kind()) { + case OP_MUL: + if (n->get_num_args() != 2) + throw found(); + if (!u.is_numeral(n->get_arg(0)) && !u.is_numeral(n->get_arg(1))) + throw found(); + return; + case OP_IDIV: case OP_DIV: case OP_REM: case OP_MOD: + if (!u.is_numeral(n->get_arg(1))) + throw found(); + return; + default: + return; + } + return; + } + }; + + bool has_nlira(expr_ref_vector &v) { + has_nlira_functor fn(v.m()); + expr_fast_mark1 visited; + try { + for (expr *e : v) + quick_for_each_expr(fn, visited, e); + } + catch (has_nlira_functor::found e) { + return true; + } + return false; + } } namespace spacer { @@ -461,9 +506,15 @@ bool lemma_quantifier_generalizer::generalize (lemma_ref &lemma, app *term) { mk_abs_cube(lemma, term, var, gnd_cube, abs_cube, lb, ub, stride); if (abs_cube.empty()) {return false;} + if (has_nlira(abs_cube)) { + TRACE("spacer_qgen", + tout << "non-linear expression: " << abs_cube << "\n";); + return false; + } TRACE("spacer_qgen", tout << "abs_cube is: " << mk_and(abs_cube) << "\n"; + tout << "term: " << mk_pp(term, m) << "\n"; tout << "lb = "; if (lb) tout << mk_pp(lb, m); else tout << "none"; tout << "\n"; From c429455f10e5b7019918045e20c793d92db57607 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 29 Jun 2018 08:52:25 -0700 Subject: [PATCH 26/32] visit parameters during occurs count Signed-off-by: Nikolaj Bjorner --- src/model/model.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/model/model.cpp b/src/model/model.cpp index 97a2917b7..83adfc87e 100644 --- a/src/model/model.cpp +++ b/src/model/model.cpp @@ -260,7 +260,7 @@ struct model::occs_collector { void operator()(func_decl* f) { ts.add_occurs(f); } - void operator()(ast* ) {} + void operator()(ast*) {} }; @@ -319,7 +319,7 @@ void model::collect_occs(top_sort& ts, func_decl* f) { void model::collect_occs(top_sort& ts, expr* e) { occs_collector collector(ts); - for_each_ast(collector, e); + for_each_ast(collector, e, true); } bool model::can_inline_def(top_sort& ts, func_decl* f) { From 1e67717d7556cbc3da7a40d77953a26aebbd6bf4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 29 Jun 2018 09:11:44 -0700 Subject: [PATCH 27/32] log with unsigned characters to avoid malformed strings as in #1712 Signed-off-by: Nikolaj Bjorner --- src/api/z3_logger.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/api/z3_logger.h b/src/api/z3_logger.h index 357d79bcb..211601713 100644 --- a/src/api/z3_logger.h +++ b/src/api/z3_logger.h @@ -49,7 +49,7 @@ void __declspec(noinline) _Z3_append_log(char const * msg) { *g_z3_log << "M \"" static std::ostream & operator<<(std::ostream & out, ll_escaped const & d) { char const * s = d.m_str; while (*s) { - char c = *s; + unsigned char c = *s; if (('0' <= c && c <= '9') || ('a' <= c && c <= 'z') || ('A' <= c && c <= 'Z') || c == '~' || c == '!' || c == '@' || c == '#' || c == '$' || c == '%' || c == '^' || c == '&' || c == '*' || c == '-' || c == '_' || c == '+' || c == '.' || c == '?' || c == '/' || c == ' ' || @@ -57,7 +57,7 @@ static std::ostream & operator<<(std::ostream & out, ll_escaped const & d) { out << c; } else { - char str[4] = {'0', '0', '0', 0}; + unsigned char str[4] = {'0', '0', '0', 0}; str[2] = '0' + (c % 10); c /= 10; str[1] = '0' + (c % 10); From cbc5aaad2c804f2b53cca2800f4afa274a19e6c5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 29 Jun 2018 09:44:54 -0700 Subject: [PATCH 28/32] strengthen simplification of to_int such that #1608 is handled during pre-processing Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/arith_rewriter.cpp | 65 +++++++++++++---------------- 1 file changed, 30 insertions(+), 35 deletions(-) diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index 379020331..7451795f3 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -1159,49 +1159,44 @@ br_status arith_rewriter::mk_to_int_core(expr * arg, expr_ref & result) { result = m_util.mk_numeral(floor(a), true); return BR_DONE; } - else if (m_util.is_to_real(arg, x)) { + + if (m_util.is_to_real(arg, x)) { result = x; return BR_DONE; } - else { - if (m_util.is_add(arg) || m_util.is_mul(arg) || m_util.is_power(arg)) { - // Try to apply simplifications such as: - // (to_int (+ 1.0 (to_real x))) --> (+ 1 x) - // if all arguments of arg are - // - integer numerals, OR - // - to_real applications - // then, to_int can be eliminated - unsigned num_args = to_app(arg)->get_num_args(); - unsigned i = 0; - for (; i < num_args; i++) { - expr * c = to_app(arg)->get_arg(i); - if (m_util.is_numeral(c, a) && a.is_int()) - continue; - if (m_util.is_to_real(c)) - continue; - break; // failed + if (m_util.is_add(arg) || m_util.is_mul(arg) || m_util.is_power(arg)) { + // Try to apply simplifications such as: + // (to_int (+ 1.0 (to_real x)) y) --> (+ 1 x (to_int y)) + + expr_ref_buffer int_args(m()), real_args(m()); + for (expr* c : *to_app(arg)) { + if (m_util.is_numeral(c, a) && a.is_int()) { + int_args.push_back(m_util.mk_numeral(a, true)); } - if (i == num_args) { - // simplification can be applied - expr_ref_buffer new_args(m()); - for (i = 0; i < num_args; i++) { - expr * c = to_app(arg)->get_arg(i); - if (m_util.is_numeral(c, a) && a.is_int()) { - new_args.push_back(m_util.mk_numeral(a, true)); - } - else { - VERIFY (m_util.is_to_real(c, x)); - new_args.push_back(x); - } - } - SASSERT(num_args == new_args.size()); - result = m().mk_app(get_fid(), to_app(arg)->get_decl()->get_decl_kind(), new_args.size(), new_args.c_ptr()); - return BR_REWRITE1; + else if (m_util.is_to_real(c, x)) { + int_args.push_back(x); + } + else { + real_args.push_back(c); } } - return BR_FAILED; + if (real_args.empty()) { + result = m().mk_app(get_fid(), to_app(arg)->get_decl()->get_decl_kind(), int_args.size(), int_args.c_ptr()); + return BR_REWRITE1; + } + if (!int_args.empty() && (m_util.is_add(arg) || m_util.is_mul(arg))) { + decl_kind k = to_app(arg)->get_decl()->get_decl_kind(); + expr_ref t1(m().mk_app(get_fid(), k, int_args.size(), int_args.c_ptr()), m()); + expr_ref t2(m().mk_app(get_fid(), k, real_args.size(), real_args.c_ptr()), m()); + int_args.reset(); + int_args.push_back(t1); + int_args.push_back(m_util.mk_to_int(t2)); + result = m().mk_app(get_fid(), k, int_args.size(), int_args.c_ptr()); + return BR_REWRITE3; + } } + return BR_FAILED; } br_status arith_rewriter::mk_to_real_core(expr * arg, expr_ref & result) { From bc8cd7ff551886576d35b1b1a56711a39e8003d8 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Fri, 29 Jun 2018 18:34:17 +0100 Subject: [PATCH 29/32] remove a few random mem allocs --- src/ast/rewriter/bv_rewriter.cpp | 14 +++++--------- src/ast/rewriter/th_rewriter.cpp | 18 ++++++++++-------- 2 files changed, 15 insertions(+), 17 deletions(-) diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp index a0adb6398..c81c7385a 100644 --- a/src/ast/rewriter/bv_rewriter.cpp +++ b/src/ast/rewriter/bv_rewriter.cpp @@ -1383,7 +1383,7 @@ br_status bv_rewriter::mk_bv2int(expr * arg, expr_ref & result) { --i; tmp = args[i].get(); tmp = m_autil.mk_mul(m_autil.mk_numeral(power(numeral(2), sz), true), tmp); - args[i] = tmp; + args[i] = std::move(tmp); sz += get_bv_size(to_app(arg)->get_arg(i)); } result = m_autil.mk_add(args.size(), args.c_ptr()); @@ -2400,8 +2400,8 @@ bool bv_rewriter::isolate_term(expr* lhs, expr* rhs, expr_ref& result) { return false; } unsigned sz = to_app(rhs)->get_num_args(); - expr_ref t1(m()), t2(m()); - t1 = to_app(rhs)->get_arg(0); + expr * t1 = to_app(rhs)->get_arg(0); + expr_ref t2(m()); if (sz > 2) { t2 = m().mk_app(get_fid(), OP_BADD, sz-1, to_app(rhs)->get_args()+1); } @@ -2597,14 +2597,10 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) { result = m().mk_bool_val(new_lhs == new_rhs); return BR_DONE; } - } - else { - new_lhs = lhs; - new_rhs = rhs; + lhs = new_lhs; + rhs = new_rhs; } - lhs = new_lhs; - rhs = new_rhs; // Try to rewrite t1 + t2 = c --> t1 = c - t2 // Reason: it is much cheaper to bit-blast. if (isolate_term(lhs, rhs, result)) { diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index 4fbf77ec9..eb819c988 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -35,6 +35,7 @@ Notes: #include "ast/ast_util.h" #include "ast/well_sorted.h" +namespace { struct th_rewriter_cfg : public default_rewriter_cfg { bool_rewriter m_b_rw; arith_rewriter m_a_rw; @@ -337,16 +338,16 @@ struct th_rewriter_cfg : public default_rewriter_cfg { family_id fid = t->get_family_id(); if (fid == m_a_rw.get_fid()) { switch (t->get_decl_kind()) { - case OP_ADD: n = m_a_util.mk_numeral(rational(0), m().get_sort(t)); return true; - case OP_MUL: n = m_a_util.mk_numeral(rational(1), m().get_sort(t)); return true; + case OP_ADD: n = m_a_util.mk_numeral(rational::zero(), m().get_sort(t)); return true; + case OP_MUL: n = m_a_util.mk_numeral(rational::one(), m().get_sort(t)); return true; default: return false; } } if (fid == m_bv_rw.get_fid()) { switch (t->get_decl_kind()) { - case OP_BADD: n = m_bv_util.mk_numeral(rational(0), m().get_sort(t)); return true; - case OP_BMUL: n = m_bv_util.mk_numeral(rational(1), m().get_sort(t)); return true; + case OP_BADD: n = m_bv_util.mk_numeral(rational::zero(), m().get_sort(t)); return true; + case OP_BMUL: n = m_bv_util.mk_numeral(rational::one(), m().get_sort(t)); return true; default: return false; } @@ -468,9 +469,9 @@ struct th_rewriter_cfg : public default_rewriter_cfg { // terms matched... bool is_int = m_a_util.is_int(t1); if (!new_t1) - new_t1 = m_a_util.mk_numeral(rational(0), is_int); + new_t1 = m_a_util.mk_numeral(rational::zero(), is_int); if (!new_t2) - new_t2 = m_a_util.mk_numeral(rational(0), is_int); + new_t2 = m_a_util.mk_numeral(rational::zero(), is_int); // mk common part ptr_buffer args; for (unsigned i = 0; i < num1; i++) { @@ -709,6 +710,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg { }; +} template class rewriter_tpl; @@ -764,8 +766,8 @@ unsigned th_rewriter::get_num_steps() const { void th_rewriter::cleanup() { ast_manager & m = m_imp->m(); - dealloc(m_imp); - m_imp = alloc(imp, m, m_params); + m_imp->~imp(); + new (m_imp) imp(m, m_params); } void th_rewriter::reset() { From c0694ae33a002dcf768f36779040bb6534c12b32 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 29 Jun 2018 10:39:07 -0700 Subject: [PATCH 30/32] deal with memory leak during shutdown Signed-off-by: Nikolaj Bjorner --- src/cmd_context/cmd_context.cpp | 1 + src/cmd_context/pdecl.cpp | 35 ++++++++++++++++++++++----------- 2 files changed, 24 insertions(+), 12 deletions(-) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 1950e35f9..0b4c5cd3d 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -493,6 +493,7 @@ cmd_context::~cmd_context() { if (m_main_ctx) { set_verbose_stream(std::cerr); } + pop(m_scopes.size()); finalize_cmds(); finalize_tactic_cmds(); finalize_probes(); diff --git a/src/cmd_context/pdecl.cpp b/src/cmd_context/pdecl.cpp index 5a0f6468b..8c88b1680 100644 --- a/src/cmd_context/pdecl.cpp +++ b/src/cmd_context/pdecl.cpp @@ -18,6 +18,7 @@ Revision History: --*/ #include "cmd_context/pdecl.h" #include "ast/datatype_decl_plugin.h" +#include "ast/ast_pp.h" #include using namespace format_ns; @@ -768,9 +769,8 @@ struct pdecl_manager::app_sort_info : public pdecl_manager::sort_info { } else { out << "(" << m_decl->get_name(); - for (unsigned i = 0; i < m_args.size(); i++) { - out << " "; - m.display(out, m_args[i]); + for (auto arg : m_args) { + m.display(out << " ", arg); } out << ")"; } @@ -782,8 +782,8 @@ struct pdecl_manager::app_sort_info : public pdecl_manager::sort_info { } else { ptr_buffer b; - for (unsigned i = 0; i < m_args.size(); i++) - b.push_back(m.pp(m_args[i])); + for (auto arg : m_args) + b.push_back(m.pp(arg)); return mk_seq1(m.m(), b.begin(), b.end(), f2f(), m_decl->get_name().str().c_str()); } } @@ -807,8 +807,8 @@ struct pdecl_manager::indexed_sort_info : public pdecl_manager::sort_info { } else { out << "(_ " << m_decl->get_name(); - for (unsigned i = 0; i < m_indices.size(); i++) { - out << " " << m_indices[i]; + for (auto idx : m_indices) { + out << " " << idx; } out << ")"; } @@ -821,8 +821,8 @@ struct pdecl_manager::indexed_sort_info : public pdecl_manager::sort_info { else { ptr_buffer b; b.push_back(mk_string(m.m(), m_decl->get_name().str().c_str())); - for (unsigned i = 0; i < m_indices.size(); i++) - b.push_back(mk_unsigned(m.m(), m_indices[i])); + for (auto idx : m_indices) + b.push_back(mk_unsigned(m.m(), idx)); return mk_seq1(m.m(), b.begin(), b.end(), f2f(), "_"); } } @@ -853,6 +853,15 @@ pdecl_manager::pdecl_manager(ast_manager & m): pdecl_manager::~pdecl_manager() { dec_ref(m_list); reset_sort_info(); + for (auto const& kv : m_sort2psort) { + del_decl_core(kv.m_value); + TRACE("pdecl_manager", tout << "orphan: " << mk_pp(kv.m_key, m()) << "\n";); + } + for (auto* p : m_table) { + del_decl_core(p); + } + m_sort2psort.reset(); + m_table.reset(); SASSERT(m_sort2psort.empty()); SASSERT(m_table.empty()); } @@ -946,13 +955,15 @@ void pdecl_manager::del_decl_core(pdecl * p) { } void pdecl_manager::del_decl(pdecl * p) { - TRACE("register_psort", tout << "del psort "; p->display(tout); tout << "\n";); + TRACE("pdecl_manager", tout << "del psort "; p->display(tout); tout << "\n";); if (p->is_psort()) { psort * _p = static_cast(p); - if (_p->is_sort_wrapper()) + if (_p->is_sort_wrapper()) { m_sort2psort.erase(static_cast(_p)->get_sort()); - else + } + else { m_table.erase(_p); + } } del_decl_core(p); } From f1d27cd487ca4469f5e1ff1925bf7867fdede5e9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 29 Jun 2018 18:16:32 -0700 Subject: [PATCH 31/32] workaround non-deterministic behavior of is_irrational_numeral test Signed-off-by: Nikolaj Bjorner --- scripts/update_api.py | 2 +- src/api/api_arith.cpp | 6 +----- src/api/dotnet/AST.cs | 2 +- src/api/dotnet/ASTMap.cs | 2 +- src/api/dotnet/BitVecNum.cs | 8 ++++---- src/api/dotnet/Context.cs | 20 +++++++++----------- src/api/dotnet/Expr.cs | 22 ++++++++++++---------- src/api/dotnet/FPNum.cs | 24 ++++++++++++------------ src/api/dotnet/FiniteDomainNum.cs | 8 ++++---- src/api/dotnet/FuncDecl.cs | 2 +- src/api/dotnet/Global.cs | 4 ++-- src/api/dotnet/Goal.cs | 8 ++++---- src/api/dotnet/IntNum.cs | 8 ++++---- src/api/dotnet/Model.cs | 4 ++-- src/api/dotnet/Params.cs | 4 ++-- src/api/dotnet/Quantifier.cs | 12 ++++++------ src/api/dotnet/Sort.cs | 2 +- src/api/dotnet/Statistics.cs | 4 ++-- src/ast/arith_decl_plugin.cpp | 7 ++++++- src/ast/arith_decl_plugin.h | 5 ++--- 20 files changed, 77 insertions(+), 77 deletions(-) diff --git a/scripts/update_api.py b/scripts/update_api.py index 78fad45be..4452ae613 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -73,7 +73,7 @@ Type2PyStr = { VOID_PTR : 'ctypes.c_void_p', INT : 'ctypes.c_int', UINT : 'ctype # Mapping to .NET types Type2Dotnet = { VOID : 'void', VOID_PTR : 'IntPtr', INT : 'int', UINT : 'uint', INT64 : 'Int64', UINT64 : 'UInt64', DOUBLE : 'double', - FLOAT : 'float', STRING : 'string', STRING_PTR : 'byte**', BOOL : 'int', SYMBOL : 'IntPtr', + FLOAT : 'float', STRING : 'string', STRING_PTR : 'byte**', BOOL : 'bool', SYMBOL : 'IntPtr', PRINT_MODE : 'uint', ERROR_CODE : 'uint' } # Mapping to Java types diff --git a/src/api/api_arith.cpp b/src/api/api_arith.cpp index 9bb236fe2..a79f55855 100644 --- a/src/api/api_arith.cpp +++ b/src/api/api_arith.cpp @@ -120,12 +120,8 @@ extern "C" { } Z3_bool Z3_API Z3_is_algebraic_number(Z3_context c, Z3_ast a) { - Z3_TRY; LOG_Z3_is_algebraic_number(c, a); - RESET_ERROR_CODE(); - expr * e = to_expr(a); - return mk_c(c)->autil().is_irrational_algebraic_numeral(e); - Z3_CATCH_RETURN(Z3_FALSE); + return mk_c(c)->autil().is_irrational_algebraic_numeral(to_expr(a)); } Z3_ast Z3_API Z3_get_algebraic_number_lower(Z3_context c, Z3_ast a, unsigned precision) { diff --git a/src/api/dotnet/AST.cs b/src/api/dotnet/AST.cs index c7ca1851e..64ec88d09 100644 --- a/src/api/dotnet/AST.cs +++ b/src/api/dotnet/AST.cs @@ -43,7 +43,7 @@ namespace Microsoft.Z3 (!Object.ReferenceEquals(a, null) && !Object.ReferenceEquals(b, null) && a.Context.nCtx == b.Context.nCtx && - Native.Z3_is_eq_ast(a.Context.nCtx, a.NativeObject, b.NativeObject) != 0); + Native.Z3_is_eq_ast(a.Context.nCtx, a.NativeObject, b.NativeObject)); } /// diff --git a/src/api/dotnet/ASTMap.cs b/src/api/dotnet/ASTMap.cs index 596b2943f..9dcb3ef82 100644 --- a/src/api/dotnet/ASTMap.cs +++ b/src/api/dotnet/ASTMap.cs @@ -37,7 +37,7 @@ namespace Microsoft.Z3 { Contract.Requires(k != null); - return Native.Z3_ast_map_contains(Context.nCtx, NativeObject, k.NativeObject) != 0; + return Native.Z3_ast_map_contains(Context.nCtx, NativeObject, k.NativeObject); } /// diff --git a/src/api/dotnet/BitVecNum.cs b/src/api/dotnet/BitVecNum.cs index 66054761a..c6055db14 100644 --- a/src/api/dotnet/BitVecNum.cs +++ b/src/api/dotnet/BitVecNum.cs @@ -39,7 +39,7 @@ namespace Microsoft.Z3 get { UInt64 res = 0; - if (Native.Z3_get_numeral_uint64(Context.nCtx, NativeObject, ref res) == 0) + if (Native.Z3_get_numeral_uint64(Context.nCtx, NativeObject, ref res) == false) throw new Z3Exception("Numeral is not a 64 bit unsigned"); return res; } @@ -53,7 +53,7 @@ namespace Microsoft.Z3 get { int res = 0; - if (Native.Z3_get_numeral_int(Context.nCtx, NativeObject, ref res) == 0) + if (Native.Z3_get_numeral_int(Context.nCtx, NativeObject, ref res) == false) throw new Z3Exception("Numeral is not an int"); return res; } @@ -67,7 +67,7 @@ namespace Microsoft.Z3 get { Int64 res = 0; - if (Native.Z3_get_numeral_int64(Context.nCtx, NativeObject, ref res) == 0) + if (Native.Z3_get_numeral_int64(Context.nCtx, NativeObject, ref res) == false) throw new Z3Exception("Numeral is not an int64"); return res; } @@ -81,7 +81,7 @@ namespace Microsoft.Z3 get { uint res = 0; - if (Native.Z3_get_numeral_uint(Context.nCtx, NativeObject, ref res) == 0) + if (Native.Z3_get_numeral_uint(Context.nCtx, NativeObject, ref res) == false) throw new Z3Exception("Numeral is not a uint"); return res; } diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index 890d86619..ba76ae7eb 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -1963,7 +1963,7 @@ namespace Microsoft.Z3 Contract.Ensures(Contract.Result() != null); CheckContextMatch(t); - return new IntExpr(this, Native.Z3_mk_bv2int(nCtx, t.NativeObject, (signed) ? 1 : 0)); + return new IntExpr(this, Native.Z3_mk_bv2int(nCtx, t.NativeObject, (signed))); } /// @@ -1980,7 +1980,7 @@ namespace Microsoft.Z3 CheckContextMatch(t1); CheckContextMatch(t2); - return new BoolExpr(this, Native.Z3_mk_bvadd_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned) ? 1 : 0)); + return new BoolExpr(this, Native.Z3_mk_bvadd_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned))); } /// @@ -2031,7 +2031,7 @@ namespace Microsoft.Z3 CheckContextMatch(t1); CheckContextMatch(t2); - return new BoolExpr(this, Native.Z3_mk_bvsub_no_underflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned) ? 1 : 0)); + return new BoolExpr(this, Native.Z3_mk_bvsub_no_underflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned))); } /// @@ -2080,7 +2080,7 @@ namespace Microsoft.Z3 CheckContextMatch(t1); CheckContextMatch(t2); - return new BoolExpr(this, Native.Z3_mk_bvmul_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned) ? 1 : 0)); + return new BoolExpr(this, Native.Z3_mk_bvmul_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned))); } /// @@ -3135,9 +3135,7 @@ namespace Microsoft.Z3 public BitVecNum MkBV(bool[] bits) { Contract.Ensures(Contract.Result() != null); - int[] _bits = new int[bits.Length]; - for (int i = 0; i < bits.Length; ++i) _bits[i] = bits[i] ? 1 : 0; - return (BitVecNum)Expr.Create(this, Native.Z3_mk_bv_numeral(nCtx, (uint)bits.Length, _bits)); + return (BitVecNum)Expr.Create(this, Native.Z3_mk_bv_numeral(nCtx, (uint)bits.Length, bits)); } @@ -4186,7 +4184,7 @@ namespace Microsoft.Z3 public FPNum MkFPInf(FPSort s, bool negative) { Contract.Ensures(Contract.Result() != null); - return new FPNum(this, Native.Z3_mk_fpa_inf(nCtx, s.NativeObject, negative ? 1 : 0)); + return new FPNum(this, Native.Z3_mk_fpa_inf(nCtx, s.NativeObject, negative)); } /// @@ -4197,7 +4195,7 @@ namespace Microsoft.Z3 public FPNum MkFPZero(FPSort s, bool negative) { Contract.Ensures(Contract.Result() != null); - return new FPNum(this, Native.Z3_mk_fpa_zero(nCtx, s.NativeObject, negative ? 1 : 0)); + return new FPNum(this, Native.Z3_mk_fpa_zero(nCtx, s.NativeObject, negative)); } /// @@ -4243,7 +4241,7 @@ namespace Microsoft.Z3 public FPNum MkFPNumeral(bool sgn, uint sig, int exp, FPSort s) { Contract.Ensures(Contract.Result() != null); - return new FPNum(this, Native.Z3_mk_fpa_numeral_int_uint(nCtx, sgn ? 1 : 0, exp, sig, s.NativeObject)); + return new FPNum(this, Native.Z3_mk_fpa_numeral_int_uint(nCtx, sgn, exp, sig, s.NativeObject)); } /// @@ -4256,7 +4254,7 @@ namespace Microsoft.Z3 public FPNum MkFPNumeral(bool sgn, Int64 exp, UInt64 sig, FPSort s) { Contract.Ensures(Contract.Result() != null); - return new FPNum(this, Native.Z3_mk_fpa_numeral_int64_uint64(nCtx, sgn ? 1 : 0, exp, sig, s.NativeObject)); + return new FPNum(this, Native.Z3_mk_fpa_numeral_int64_uint64(nCtx, sgn, exp, sig, s.NativeObject)); } /// diff --git a/src/api/dotnet/Expr.cs b/src/api/dotnet/Expr.cs index f09eecbdd..677ea7f7c 100644 --- a/src/api/dotnet/Expr.cs +++ b/src/api/dotnet/Expr.cs @@ -179,7 +179,7 @@ namespace Microsoft.Z3 /// public bool IsNumeral { - get { return Native.Z3_is_numeral_ast(Context.nCtx, NativeObject) != 0; } + get { return Native.Z3_is_numeral_ast(Context.nCtx, NativeObject) ; } } /// @@ -188,7 +188,7 @@ namespace Microsoft.Z3 /// True if the term is well-sorted, false otherwise. public bool IsWellSorted { - get { return Native.Z3_is_well_sorted(Context.nCtx, NativeObject) != 0; } + get { return Native.Z3_is_well_sorted(Context.nCtx, NativeObject) ; } } /// @@ -239,7 +239,7 @@ namespace Microsoft.Z3 /// public bool IsAlgebraicNumber { - get { return Native.Z3_is_algebraic_number(Context.nCtx, NativeObject) != 0; } + get { return Native.Z3_is_algebraic_number(Context.nCtx, NativeObject); } } #endregion @@ -256,7 +256,7 @@ namespace Microsoft.Z3 return (IsExpr && Native.Z3_is_eq_sort(Context.nCtx, Native.Z3_mk_bool_sort(Context.nCtx), - Native.Z3_get_sort(Context.nCtx, NativeObject)) != 0); + Native.Z3_get_sort(Context.nCtx, NativeObject)) ); } } @@ -423,7 +423,7 @@ namespace Microsoft.Z3 { get { - return (Native.Z3_is_app(Context.nCtx, NativeObject) != 0 && + return (Native.Z3_is_app(Context.nCtx, NativeObject) && (Z3_sort_kind)Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == Z3_sort_kind.Z3_ARRAY_SORT); } @@ -789,7 +789,7 @@ namespace Microsoft.Z3 /// Check whether expression is a string constant. /// /// a Boolean - public bool IsString { get { return IsApp && 0 != Native.Z3_is_string(Context.nCtx, NativeObject); } } + public bool IsString { get { return IsApp && Native.Z3_is_string(Context.nCtx, NativeObject); } } /// /// Retrieve string corresponding to string constant. @@ -1336,7 +1336,7 @@ namespace Microsoft.Z3 { get { - return (Native.Z3_is_app(Context.nCtx, NativeObject) != 0 && + return (Native.Z3_is_app(Context.nCtx, NativeObject) && Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == (uint)Z3_sort_kind.Z3_RELATION_SORT); } @@ -1458,7 +1458,7 @@ namespace Microsoft.Z3 { get { - return (Native.Z3_is_app(Context.nCtx, NativeObject) != 0 && + return (Native.Z3_is_app(Context.nCtx, NativeObject) && Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == (uint)Z3_sort_kind.Z3_FINITE_DOMAIN_SORT); } } @@ -1822,11 +1822,13 @@ namespace Microsoft.Z3 IntPtr s = Native.Z3_get_sort(ctx.nCtx, obj); Z3_sort_kind sk = (Z3_sort_kind)Native.Z3_get_sort_kind(ctx.nCtx, s); - if (Native.Z3_is_algebraic_number(ctx.nCtx, obj) != 0) // is this a numeral ast? + if (Z3_sort_kind.Z3_REAL_SORT == sk && + Native.Z3_is_algebraic_number(ctx.nCtx, obj)) // is this a numeral ast? return new AlgebraicNum(ctx, obj); - if (Native.Z3_is_numeral_ast(ctx.nCtx, obj) != 0) + if (Native.Z3_is_numeral_ast(ctx.nCtx, obj)) { + switch (sk) { case Z3_sort_kind.Z3_INT_SORT: return new IntNum(ctx, obj); diff --git a/src/api/dotnet/FPNum.cs b/src/api/dotnet/FPNum.cs index 808752eaa..4a2575fe4 100644 --- a/src/api/dotnet/FPNum.cs +++ b/src/api/dotnet/FPNum.cs @@ -52,7 +52,7 @@ namespace Microsoft.Z3 get { int res = 0; - if (Native.Z3_fpa_get_numeral_sign(Context.nCtx, NativeObject, ref res) == 0) + if (Native.Z3_fpa_get_numeral_sign(Context.nCtx, NativeObject, ref res) == false) throw new Z3Exception("Sign is not a Boolean value"); return res != 0; } @@ -86,7 +86,7 @@ namespace Microsoft.Z3 get { UInt64 result = 0; - if (Native.Z3_fpa_get_numeral_significand_uint64(Context.nCtx, NativeObject, ref result) == 0) + if (Native.Z3_fpa_get_numeral_significand_uint64(Context.nCtx, NativeObject, ref result) == false) throw new Z3Exception("Significand is not a 64 bit unsigned integer"); return result; } @@ -111,7 +111,7 @@ namespace Microsoft.Z3 /// public string Exponent(bool biased = true) { - return Native.Z3_fpa_get_numeral_exponent_string(Context.nCtx, NativeObject, biased ? 1 : 0); + return Native.Z3_fpa_get_numeral_exponent_string(Context.nCtx, NativeObject, biased); } /// @@ -120,7 +120,7 @@ namespace Microsoft.Z3 public Int64 ExponentInt64(bool biased = true) { Int64 result = 0; - if (Native.Z3_fpa_get_numeral_exponent_int64(Context.nCtx, NativeObject, ref result, biased ? 1 : 0) == 0) + if (Native.Z3_fpa_get_numeral_exponent_int64(Context.nCtx, NativeObject, ref result, biased) == false) throw new Z3Exception("Exponent is not a 64 bit integer"); return result; } @@ -133,43 +133,43 @@ namespace Microsoft.Z3 /// public BitVecExpr ExponentBV(bool biased = true) { - return new BitVecExpr(Context, Native.Z3_fpa_get_numeral_exponent_bv(Context.nCtx, NativeObject, biased ? 1 : 0)); + return new BitVecExpr(Context, Native.Z3_fpa_get_numeral_exponent_bv(Context.nCtx, NativeObject, biased)); } /// /// Indicates whether the numeral is a NaN. /// - public bool IsNaN { get { return Native.Z3_fpa_is_numeral_nan(Context.nCtx, NativeObject) != 0; } } + public bool IsNaN { get { return Native.Z3_fpa_is_numeral_nan(Context.nCtx, NativeObject) ; } } /// /// Indicates whether the numeral is a +oo or -oo. /// - public bool IsInf { get { return Native.Z3_fpa_is_numeral_inf(Context.nCtx, NativeObject) != 0; } } + public bool IsInf { get { return Native.Z3_fpa_is_numeral_inf(Context.nCtx, NativeObject) ; } } /// /// Indicates whether the numeral is +zero or -zero. /// - public bool IsZero{ get { return Native.Z3_fpa_is_numeral_zero(Context.nCtx, NativeObject) != 0; } } + public bool IsZero{ get { return Native.Z3_fpa_is_numeral_zero(Context.nCtx, NativeObject) ; } } /// /// Indicates whether the numeral is normal. /// - public bool IsNormal { get { return Native.Z3_fpa_is_numeral_normal(Context.nCtx, NativeObject) != 0; } } + public bool IsNormal { get { return Native.Z3_fpa_is_numeral_normal(Context.nCtx, NativeObject) ; } } /// /// Indicates whether the numeral is subnormal. /// - public bool IsSubnormal { get { return Native.Z3_fpa_is_numeral_subnormal(Context.nCtx, NativeObject) != 0; } } + public bool IsSubnormal { get { return Native.Z3_fpa_is_numeral_subnormal(Context.nCtx, NativeObject) ; } } /// /// Indicates whether the numeral is positive. /// - public bool IsPositive { get { return Native.Z3_fpa_is_numeral_positive(Context.nCtx, NativeObject) != 0; } } + public bool IsPositive { get { return Native.Z3_fpa_is_numeral_positive(Context.nCtx, NativeObject) ; } } /// /// Indicates whether the numeral is negative. /// - public bool IsNegative { get { return Native.Z3_fpa_is_numeral_negative(Context.nCtx, NativeObject) != 0; } } + public bool IsNegative { get { return Native.Z3_fpa_is_numeral_negative(Context.nCtx, NativeObject) ; } } #region Internal internal FPNum(Context ctx, IntPtr obj) diff --git a/src/api/dotnet/FiniteDomainNum.cs b/src/api/dotnet/FiniteDomainNum.cs index 52c0af8bd..fb51e1014 100644 --- a/src/api/dotnet/FiniteDomainNum.cs +++ b/src/api/dotnet/FiniteDomainNum.cs @@ -39,7 +39,7 @@ namespace Microsoft.Z3 get { UInt64 res = 0; - if (Native.Z3_get_numeral_uint64(Context.nCtx, NativeObject, ref res) == 0) + if (Native.Z3_get_numeral_uint64(Context.nCtx, NativeObject, ref res) == false) throw new Z3Exception("Numeral is not a 64 bit unsigned"); return res; } @@ -53,7 +53,7 @@ namespace Microsoft.Z3 get { int res = 0; - if (Native.Z3_get_numeral_int(Context.nCtx, NativeObject, ref res) == 0) + if (Native.Z3_get_numeral_int(Context.nCtx, NativeObject, ref res) == false) throw new Z3Exception("Numeral is not an int"); return res; } @@ -67,7 +67,7 @@ namespace Microsoft.Z3 get { Int64 res = 0; - if (Native.Z3_get_numeral_int64(Context.nCtx, NativeObject, ref res) == 0) + if (Native.Z3_get_numeral_int64(Context.nCtx, NativeObject, ref res) == false) throw new Z3Exception("Numeral is not an int64"); return res; } @@ -81,7 +81,7 @@ namespace Microsoft.Z3 get { uint res = 0; - if (Native.Z3_get_numeral_uint(Context.nCtx, NativeObject, ref res) == 0) + if (Native.Z3_get_numeral_uint(Context.nCtx, NativeObject, ref res) == false) throw new Z3Exception("Numeral is not a uint"); return res; } diff --git a/src/api/dotnet/FuncDecl.cs b/src/api/dotnet/FuncDecl.cs index 0587a2276..39ddfad83 100644 --- a/src/api/dotnet/FuncDecl.cs +++ b/src/api/dotnet/FuncDecl.cs @@ -38,7 +38,7 @@ namespace Microsoft.Z3 (!Object.ReferenceEquals(a, null) && !Object.ReferenceEquals(b, null) && a.Context.nCtx == b.Context.nCtx && - Native.Z3_is_eq_func_decl(a.Context.nCtx, a.NativeObject, b.NativeObject) != 0); + Native.Z3_is_eq_func_decl(a.Context.nCtx, a.NativeObject, b.NativeObject)); } /// diff --git a/src/api/dotnet/Global.cs b/src/api/dotnet/Global.cs index acf3fab32..f242003a8 100644 --- a/src/api/dotnet/Global.cs +++ b/src/api/dotnet/Global.cs @@ -65,7 +65,7 @@ namespace Microsoft.Z3 public static string GetParameter(string id) { IntPtr t; - if (Native.Z3_global_param_get(id, out t) == 0) + if (Native.Z3_global_param_get(id, out t) == false) return null; else return Marshal.PtrToStringAnsi(t); @@ -91,7 +91,7 @@ namespace Microsoft.Z3 /// all contexts globally. public static void ToggleWarningMessages(bool enabled) { - Native.Z3_toggle_warning_messages((enabled) ? 1 : 0); + Native.Z3_toggle_warning_messages(enabled); } /// diff --git a/src/api/dotnet/Goal.cs b/src/api/dotnet/Goal.cs index 03e573538..a5e35fcd5 100644 --- a/src/api/dotnet/Goal.cs +++ b/src/api/dotnet/Goal.cs @@ -103,7 +103,7 @@ namespace Microsoft.Z3 /// public bool Inconsistent { - get { return Native.Z3_goal_inconsistent(Context.nCtx, NativeObject) != 0; } + get { return Native.Z3_goal_inconsistent(Context.nCtx, NativeObject) ; } } /// @@ -163,7 +163,7 @@ namespace Microsoft.Z3 /// public bool IsDecidedSat { - get { return Native.Z3_goal_is_decided_sat(Context.nCtx, NativeObject) != 0; } + get { return Native.Z3_goal_is_decided_sat(Context.nCtx, NativeObject) ; } } /// @@ -171,7 +171,7 @@ namespace Microsoft.Z3 /// public bool IsDecidedUnsat { - get { return Native.Z3_goal_is_decided_unsat(Context.nCtx, NativeObject) != 0; } + get { return Native.Z3_goal_is_decided_unsat(Context.nCtx, NativeObject) ; } } /// @@ -251,7 +251,7 @@ namespace Microsoft.Z3 internal Goal(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); } internal Goal(Context ctx, bool models, bool unsatCores, bool proofs) - : base(ctx, Native.Z3_mk_goal(ctx.nCtx, (models) ? 1 : 0, (unsatCores) ? 1 : 0, (proofs) ? 1 : 0)) + : base(ctx, Native.Z3_mk_goal(ctx.nCtx, (models), (unsatCores), (proofs))) { Contract.Requires(ctx != null); } diff --git a/src/api/dotnet/IntNum.cs b/src/api/dotnet/IntNum.cs index 64fd78ad2..78fee44f4 100644 --- a/src/api/dotnet/IntNum.cs +++ b/src/api/dotnet/IntNum.cs @@ -49,7 +49,7 @@ namespace Microsoft.Z3 get { UInt64 res = 0; - if (Native.Z3_get_numeral_uint64(Context.nCtx, NativeObject, ref res) == 0) + if (Native.Z3_get_numeral_uint64(Context.nCtx, NativeObject, ref res) == false) throw new Z3Exception("Numeral is not a 64 bit unsigned"); return res; } @@ -63,7 +63,7 @@ namespace Microsoft.Z3 get { int res = 0; - if (Native.Z3_get_numeral_int(Context.nCtx, NativeObject, ref res) == 0) + if (Native.Z3_get_numeral_int(Context.nCtx, NativeObject, ref res) == false) throw new Z3Exception("Numeral is not an int"); return res; } @@ -77,7 +77,7 @@ namespace Microsoft.Z3 get { Int64 res = 0; - if (Native.Z3_get_numeral_int64(Context.nCtx, NativeObject, ref res) == 0) + if (Native.Z3_get_numeral_int64(Context.nCtx, NativeObject, ref res) == false) throw new Z3Exception("Numeral is not an int64"); return res; } @@ -91,7 +91,7 @@ namespace Microsoft.Z3 get { uint res = 0; - if (Native.Z3_get_numeral_uint(Context.nCtx, NativeObject, ref res) == 0) + if (Native.Z3_get_numeral_uint(Context.nCtx, NativeObject, ref res) == false) throw new Z3Exception("Numeral is not a uint"); return res; } diff --git a/src/api/dotnet/Model.cs b/src/api/dotnet/Model.cs index d11a57052..2c6d12dc0 100644 --- a/src/api/dotnet/Model.cs +++ b/src/api/dotnet/Model.cs @@ -86,7 +86,7 @@ namespace Microsoft.Z3 return null; else { - if (Native.Z3_is_as_array(Context.nCtx, n) == 0) + if (Native.Z3_is_as_array(Context.nCtx, n) == false) throw new Z3Exception("Argument was not an array constant"); IntPtr fd = Native.Z3_get_as_array_func_decl(Context.nCtx, n); return FuncInterp(new FuncDecl(Context, fd)); @@ -227,7 +227,7 @@ namespace Microsoft.Z3 Contract.Ensures(Contract.Result() != null); IntPtr v = IntPtr.Zero; - if (Native.Z3_model_eval(Context.nCtx, NativeObject, t.NativeObject, (completion) ? 1 : 0, ref v) == 0) + if (Native.Z3_model_eval(Context.nCtx, NativeObject, t.NativeObject, (completion), ref v) == false) throw new ModelEvaluationFailedException(); else return Expr.Create(Context, v); diff --git a/src/api/dotnet/Params.cs b/src/api/dotnet/Params.cs index 5b143d525..eeda55755 100644 --- a/src/api/dotnet/Params.cs +++ b/src/api/dotnet/Params.cs @@ -35,7 +35,7 @@ namespace Microsoft.Z3 { Contract.Requires(name != null); - Native.Z3_params_set_bool(Context.nCtx, NativeObject, name.NativeObject, (value) ? 1 : 0); + Native.Z3_params_set_bool(Context.nCtx, NativeObject, name.NativeObject, (value)); return this; } @@ -90,7 +90,7 @@ namespace Microsoft.Z3 /// public Params Add(string name, bool value) { - Native.Z3_params_set_bool(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, (value) ? 1 : 0); + Native.Z3_params_set_bool(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, (value)); return this; } diff --git a/src/api/dotnet/Quantifier.cs b/src/api/dotnet/Quantifier.cs index e34b4ef97..d729f7424 100644 --- a/src/api/dotnet/Quantifier.cs +++ b/src/api/dotnet/Quantifier.cs @@ -33,7 +33,7 @@ namespace Microsoft.Z3 /// public bool IsUniversal { - get { return Native.Z3_is_quantifier_forall(Context.nCtx, NativeObject) != 0; } + get { return Native.Z3_is_quantifier_forall(Context.nCtx, NativeObject); } } /// @@ -41,7 +41,7 @@ namespace Microsoft.Z3 /// public bool IsExistential { - get { return Native.Z3_is_quantifier_exists(Context.nCtx, NativeObject) != 0; } + get { return Native.Z3_is_quantifier_exists(Context.nCtx, NativeObject); } } /// @@ -193,7 +193,7 @@ namespace Microsoft.Z3 if (noPatterns == null && quantifierID == null && skolemID == null) { - NativeObject = Native.Z3_mk_quantifier(ctx.nCtx, (isForall) ? 1 : 0, weight, + NativeObject = Native.Z3_mk_quantifier(ctx.nCtx, (isForall) , weight, AST.ArrayLength(patterns), AST.ArrayToNative(patterns), AST.ArrayLength(sorts), AST.ArrayToNative(sorts), Symbol.ArrayToNative(names), @@ -201,7 +201,7 @@ namespace Microsoft.Z3 } else { - NativeObject = Native.Z3_mk_quantifier_ex(ctx.nCtx, (isForall) ? 1 : 0, weight, + NativeObject = Native.Z3_mk_quantifier_ex(ctx.nCtx, (isForall), weight, AST.GetNativeObject(quantifierID), AST.GetNativeObject(skolemID), AST.ArrayLength(patterns), AST.ArrayToNative(patterns), AST.ArrayLength(noPatterns), AST.ArrayToNative(noPatterns), @@ -229,14 +229,14 @@ namespace Microsoft.Z3 if (noPatterns == null && quantifierID == null && skolemID == null) { - NativeObject = Native.Z3_mk_quantifier_const(ctx.nCtx, (isForall) ? 1 : 0, weight, + NativeObject = Native.Z3_mk_quantifier_const(ctx.nCtx, (isForall) , weight, AST.ArrayLength(bound), AST.ArrayToNative(bound), AST.ArrayLength(patterns), AST.ArrayToNative(patterns), body.NativeObject); } else { - NativeObject = Native.Z3_mk_quantifier_const_ex(ctx.nCtx, (isForall) ? 1 : 0, weight, + NativeObject = Native.Z3_mk_quantifier_const_ex(ctx.nCtx, (isForall), weight, AST.GetNativeObject(quantifierID), AST.GetNativeObject(skolemID), AST.ArrayLength(bound), AST.ArrayToNative(bound), AST.ArrayLength(patterns), AST.ArrayToNative(patterns), diff --git a/src/api/dotnet/Sort.cs b/src/api/dotnet/Sort.cs index e6f195434..66acc5c0f 100644 --- a/src/api/dotnet/Sort.cs +++ b/src/api/dotnet/Sort.cs @@ -41,7 +41,7 @@ namespace Microsoft.Z3 (!Object.ReferenceEquals(a, null) && !Object.ReferenceEquals(b, null) && a.Context == b.Context && - Native.Z3_is_eq_sort(a.Context.nCtx, a.NativeObject, b.NativeObject) != 0); + Native.Z3_is_eq_sort(a.Context.nCtx, a.NativeObject, b.NativeObject)); } /// diff --git a/src/api/dotnet/Statistics.cs b/src/api/dotnet/Statistics.cs index c94af625c..6708035bc 100644 --- a/src/api/dotnet/Statistics.cs +++ b/src/api/dotnet/Statistics.cs @@ -134,9 +134,9 @@ namespace Microsoft.Z3 { Entry e; string k = Native.Z3_stats_get_key(Context.nCtx, NativeObject, i); - if (Native.Z3_stats_is_uint(Context.nCtx, NativeObject, i) != 0) + if (Native.Z3_stats_is_uint(Context.nCtx, NativeObject, i) ) e = new Entry(k, Native.Z3_stats_get_uint_value(Context.nCtx, NativeObject, i)); - else if (Native.Z3_stats_is_double(Context.nCtx, NativeObject, i) != 0) + else if (Native.Z3_stats_is_double(Context.nCtx, NativeObject, i) ) e = new Entry(k, Native.Z3_stats_get_double_value(Context.nCtx, NativeObject, i)); else throw new Z3Exception("Unknown data entry value"); diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp index fe5bc3af5..be3a02019 100644 --- a/src/ast/arith_decl_plugin.cpp +++ b/src/ast/arith_decl_plugin.cpp @@ -638,6 +638,11 @@ bool arith_recognizers::is_numeral(expr const * n, rational & val, bool & is_int return true; } +bool arith_recognizers::is_irrational_algebraic_numeral(expr const * n) const { + return is_app(n) && to_app(n)->is_app_of(m_afid, OP_IRRATIONAL_ALGEBRAIC_NUM); +} + + #define IS_INT_EXPR_DEPTH_LIMIT 100 bool arith_recognizers::is_int_expr(expr const *e) const { if (is_int(e)) return true; @@ -678,7 +683,7 @@ void arith_util::init_plugin() { m_plugin = static_cast(m_manager.get_plugin(m_afid)); } -bool arith_util::is_irrational_algebraic_numeral(expr const * n, algebraic_numbers::anum & val) { +bool arith_util::is_irrational_algebraic_numeral2(expr const * n, algebraic_numbers::anum & val) { if (!is_app_of(n, m_afid, OP_IRRATIONAL_ALGEBRAIC_NUM)) return false; am().set(val, to_irrational_algebraic_numeral(n)); diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h index d7340297b..17b8fa1d0 100644 --- a/src/ast/arith_decl_plugin.h +++ b/src/ast/arith_decl_plugin.h @@ -229,7 +229,7 @@ public: family_id get_family_id() const { return m_afid; } bool is_arith_expr(expr const * n) const { return is_app(n) && to_app(n)->get_family_id() == m_afid; } - bool is_irrational_algebraic_numeral(expr const * n) const { return is_app_of(n, m_afid, OP_IRRATIONAL_ALGEBRAIC_NUM); } + bool is_irrational_algebraic_numeral(expr const * n) const; bool is_numeral(expr const * n, rational & val, bool & is_int) const; bool is_numeral(expr const * n, rational & val) const { bool is_int; return is_numeral(n, val, is_int); } bool is_numeral(expr const * n) const { return is_app_of(n, m_afid, OP_NUM); } @@ -338,8 +338,7 @@ public: return plugin().am(); } - bool is_irrational_algebraic_numeral(expr const * n) const { return is_app_of(n, m_afid, OP_IRRATIONAL_ALGEBRAIC_NUM); } - bool is_irrational_algebraic_numeral(expr const * n, algebraic_numbers::anum & val); + bool is_irrational_algebraic_numeral2(expr const * n, algebraic_numbers::anum & val); algebraic_numbers::anum const & to_irrational_algebraic_numeral(expr const * n); sort * mk_int() { return m_manager.mk_sort(m_afid, INT_SORT); } From 33fc56f686ff5ff536d809f3a35ec5612febc82d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 29 Jun 2018 18:36:43 -0700 Subject: [PATCH 32/32] fix debug Signed-off-by: Nikolaj Bjorner --- src/api/dotnet/Expr.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/dotnet/Expr.cs b/src/api/dotnet/Expr.cs index 677ea7f7c..99745ffff 100644 --- a/src/api/dotnet/Expr.cs +++ b/src/api/dotnet/Expr.cs @@ -1789,7 +1789,7 @@ namespace Microsoft.Z3 [Pure] internal override void CheckNativeObject(IntPtr obj) { - if (Native.Z3_is_app(Context.nCtx, obj) == 0 && + if (Native.Z3_is_app(Context.nCtx, obj) == false && Native.Z3_get_ast_kind(Context.nCtx, obj) != (uint)Z3_ast_kind.Z3_VAR_AST && Native.Z3_get_ast_kind(Context.nCtx, obj) != (uint)Z3_ast_kind.Z3_QUANTIFIER_AST) throw new Z3Exception("Underlying object is not a term");