From 49e94809282eee4dff22d39887724112dd6472a1 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Wed, 27 Jun 2018 14:34:29 -0400 Subject: [PATCH] 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) {