diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index 5806c08fb..a8a904aa1 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -659,10 +659,18 @@ void lemma::mk_insts(expr_ref_vector &out, expr* e) } } - - // ---------------- // pred_tansformer +pred_transformer::pt_rule &pred_transformer::pt_rules::mk_rule(const pred_transformer::pt_rule &v) { + pt_rule *p = nullptr; + if (find_by_rule(v.rule(), p)) + return *p; + + p = alloc(pt_rule, v); + m_rules.insert(&p->rule(), p); + if (p->tag()) m_tags.insert(p->tag(), p); + return *p; +} pred_transformer::pred_transformer(context& ctx, manager& pm, func_decl* head): pm(pm), m(pm.get_manager()), @@ -692,9 +700,6 @@ app_ref pred_transformer::mk_extend_lit() { return app_ref(m.mk_not (m.mk_const (pm.get_n_pred (v->get_decl ()))), m); } -pred_transformer::~pred_transformer() { - for (auto &entry : m_rule2transition) {m.dec_ref(entry.m_value);} -} std::ostream& pred_transformer::display(std::ostream& out) const { @@ -819,10 +824,10 @@ reach_fact *pred_transformer::get_used_origin_rf (model_evaluator_util& mev, const datalog::rule *pred_transformer::find_rule(model &model) { expr_ref val(m); - for (auto &entry : m_tag2rule) { - app *tag = to_app(entry.m_key); + for (auto &kv : m_pt_rules) { + app *tag = kv.m_value->tag(); if (model.eval(tag->get_decl(), val) && m.is_true(val)) { - return entry.m_value; + return &kv.m_value->rule(); } } return nullptr; @@ -833,26 +838,16 @@ const datalog::rule *pred_transformer::find_rule(model &model, vector& reach_pred_used, unsigned& num_reuse_reach) { - TRACE ("spacer_verbose", - datalog::rule_manager& rm = ctx.get_datalog_context().get_rule_manager(); - for (auto &entry : m_tag2rule) { - expr* pred = entry.m_key; - tout << mk_pp(pred, m) << ":\n"; - if (entry.m_value) { - rm.display_smt2(*(entry.m_value), tout) << "\n"; - } - } - ); - // find a rule whose tag is true in the model; // prefer a rule where the model intersects with reach facts of all predecessors; // also find how many predecessors' reach facts are true in the model expr_ref vl(m); const datalog::rule *r = ((datalog::rule*)nullptr); - for (auto &entry : m_tag2rule) { - expr* tag = entry.m_key; - if (model.eval(to_app(tag)->get_decl(), vl) && m.is_true(vl)) { - r = entry.m_value; + //for (auto &entry : m_tag2rule) { + for (auto &kv : m_pt_rules) { + app* tag = kv.m_value->tag(); + if (model.eval(tag->get_decl(), vl) && m.is_true(vl)) { + r = &kv.m_value->rule(); is_concrete = true; num_reuse_reach = 0; reach_pred_used.reset(); @@ -1309,9 +1304,8 @@ lbool pred_transformer::is_reachable(pob& n, expr_ref_vector* core, // populate reach_assumps if (n.level () > 0 && !m_all_init) { - for (auto &entry : m_tag2rule) { - datalog::rule const* r = entry.m_value; - if (!r) {continue;} + for (auto &kv : m_pt_rules) { + datalog::rule const* r = &kv.m_value->rule(); find_predecessors(*r, m_predicates); if (m_predicates.empty()) {continue;} for (unsigned i = 0; i < m_predicates.size(); i++) { @@ -1322,7 +1316,7 @@ lbool pred_transformer::is_reachable(pob& n, expr_ref_vector* core, pm.formula_n2o(pt.get_last_rf_tag(), a, i); reach_assumps.push_back(m.mk_not (a)); } else { - reach_assumps.push_back(m.mk_not (entry.m_key)); + reach_assumps.push_back(m.mk_not (kv.m_value->tag())); break; } } @@ -1504,11 +1498,10 @@ void pred_transformer::mk_assumptions(func_decl* head, expr* fml, expr_ref_vector& result) { expr_ref tmp1(m), tmp2(m); - for (auto& kv : m_tag2rule) { - expr* tag = kv.m_key; - datalog::rule const* r = kv.m_value; - if (!r) { continue; } - find_predecessors(*r, m_predicates); + for (auto& kv : m_pt_rules) { + expr* tag = kv.m_value->tag(); + datalog::rule const& r = kv.m_value->rule(); + find_predecessors(r, m_predicates); for (unsigned i = 0; i < m_predicates.size(); i++) { func_decl* d = m_predicates[i]; if (d == head) { @@ -1545,79 +1538,52 @@ void pred_transformer::init_rfs () expr_ref_vector v(m); reach_fact_ref fact; - for (auto &entry : m_rule2tag) { - const datalog::rule* r = entry.m_key; - if (r->get_uninterpreted_tail_size() == 0) { - fact = alloc (reach_fact, m, *r, m_rule2transition.find(r), - get_aux_vars(*r), true); - add_rf(fact.get ()); + for (auto &kv : m_pt_rules) { + pt_rule &ptr = *kv.m_value; + const datalog::rule& r = ptr.rule(); + if (ptr.is_init()) { + fact = alloc(reach_fact, m, r, ptr.trans(), ptr.auxs(), true); + add_rf(fact.get()); } } } void pred_transformer::init_rules(decl2rel const& pts) { - expr_ref_vector transitions(m); - ptr_vector tr_rules; - datalog::rule const* rule; - expr_ref_vector init_conds (m); + expr_ref_vector transitions(m), not_inits(m); app_ref tag(m); - vector is_init; - for (auto r : m_rules) {init_rule(pts, *r, is_init, tr_rules, transitions);} - SASSERT (is_init.size () == transitions.size ()); + for (auto r : m_rules) { + init_rule(pts, *r); + } - std::string name; - switch(transitions.size()) { - case 0: + if (m_pt_rules.empty()) { m_transition = m.mk_false(); m_transition_clause.reset(); - break; - case 1: - // create a dummy tag. - name = head()->get_name().str() + "_dummy"; - tag = m.mk_const(symbol(name.c_str()), m.mk_bool_sort()); - - rule = tr_rules[0]; - m_tag2rule.insert(tag, rule); - m_rule2tag.insert(rule, tag); - transitions[0] = m.mk_implies (tag, transitions.get(0)); - - m_transition_clause.push_back(m_extend_lit->get_arg(0)); - m_transition_clause.push_back(tag); - - if (!ctx.use_inc_clause()) { - transitions.push_back(mk_or(m_transition_clause)); - m_transition_clause.reset(); - } - - if (!is_init[0]) {init_conds.push_back(m.mk_not(tag));} - - m_transition = mk_and(transitions); - break; - default: - m_transition_clause.push_back (m_extend_lit->get_arg(0)); - for (unsigned i = 0; i < transitions.size(); ++i) { - name = head()->get_name().str() + "__tr" + std::to_string(i); - tag = m.mk_const(symbol(name.c_str()), m.mk_bool_sort()); - rule = tr_rules[i]; - m_tag2rule.insert(tag, rule); - m_rule2tag.insert(rule, tag); - m_transition_clause.push_back(tag); - transitions[i] = m.mk_implies(tag, transitions.get(i)); - // update init conds - if (!is_init[i]) {init_conds.push_back (m.mk_not (tag));} - } - - if (!ctx.use_inc_clause()) { - transitions.push_back(mk_or(m_transition_clause)); - m_transition_clause.reset(); - } - m_transition = mk_and(transitions); - break; } - // mk init condition - m_init = mk_and(init_conds); + else { + unsigned i = 0; + expr_ref_vector transitions(m); + m_transition_clause.push_back (m_extend_lit->get_arg(0)); + for (auto &kv : m_pt_rules) { + pt_rule &r = *kv.m_value; + std::string name = head()->get_name().str() + "__tr" + std::to_string(i); + tag = m.mk_const(symbol(name.c_str()), m.mk_bool_sort()); + m_pt_rules.set_tag(tag, r); + m_transition_clause.push_back(tag); + transitions.push_back(m.mk_implies(r.tag(), r.trans())); + if (!r.is_init()) {not_inits.push_back(m.mk_not(tag));} + ++i; + } + + if (!ctx.use_inc_clause()) { + transitions.push_back(mk_or(m_transition_clause)); + m_transition_clause.reset(); + } + m_transition = mk_and(transitions); + } + // mk init condition -- disables all non-initial transitions + m_init = mk_and(not_inits); // no rule has uninterpreted tail - if (init_conds.empty ()) {m_all_init = true;} + if (not_inits.empty ()) {m_all_init = true;} } static bool is_all_non_null(app_ref_vector const& v) @@ -1628,10 +1594,7 @@ static bool is_all_non_null(app_ref_vector const& v) return true; } -void pred_transformer::init_rule(decl2rel const& pts, datalog::rule const& rule, - vector& is_init, - ptr_vector& rules, - expr_ref_vector& transitions) { +void pred_transformer::init_rule(decl2rel const& pts, datalog::rule const& rule) { scoped_watch _t_(m_initialize_watch); // Predicates that are variable representatives. Other predicates at @@ -1652,46 +1615,42 @@ void pred_transformer::init_rule(decl2rel const& pts, datalog::rule const& rule, init_atom(pts, rule.get_tail(i), var_reprs, side, i); } // -- substitute free variables - expr_ref fml(m); + expr_ref trans(m); { expr_ref_vector tail(m); for (unsigned i = ut_size; i < t_size; ++i) - {tail.push_back(rule.get_tail(i));} - fml = mk_and (tail); + tail.push_back(rule.get_tail(i)); + trans= mk_and (tail); - ground_free_vars(fml, var_reprs, aux_vars, ut_size == 0); + ground_free_vars(trans, var_reprs, aux_vars, ut_size == 0); SASSERT(is_all_non_null(var_reprs)); expr_ref tmp(m); - var_subst(m, false)(fml, var_reprs.size (), + var_subst(m, false)(trans, var_reprs.size (), (expr*const*)var_reprs.c_ptr(), tmp); flatten_and (tmp, side); - fml = mk_and(side); + trans = mk_and(side); side.reset (); } // rewrite and simplify th_rewriter rw(m); - rw(fml); - if (ctx.blast_term_ite()) {blast_term_ite(fml, 3); rw(fml);} - TRACE("spacer", tout << mk_pp(fml, m) << "\n";); + rw(trans); + if (ctx.blast_term_ite()) {blast_term_ite(trans, 3); rw(trans);} + TRACE("spacer_init_rule", tout << mk_pp(trans, m) << "\n";); // allow quantifiers in init rule - SASSERT(ut_size == 0 || is_ground(fml)); - if (!m.is_false(fml)) { - is_init.push_back (ut_size == 0); - transitions.push_back(fml); - rules.push_back(&rule); - - m.inc_ref(fml); - m_rule2transition.insert(&rule, fml); + SASSERT(ut_size == 0 || is_ground(trans)); + if (!m.is_false(trans)) { + pt_rule &ptr = m_pt_rules.mk_rule(m, rule); + ptr.set_trans(trans); + ptr.set_auxs(aux_vars); + ptr.set_reps(var_reprs); } - // AG: shouldn't this be under the if-statement above? - m_rule2vars.insert(&rule, aux_vars); - TRACE("spacer", - tout << rule.get_decl()->get_name() << "\n"; - tout << var_reprs << "\n";); + // TRACE("spacer", + // tout << rule.get_decl()->get_name() << "\n"; + // tout << var_reprs << "\n";); } @@ -1857,18 +1816,17 @@ void pred_transformer::updt_solver(prop_solver *solver) { } // -- lemmas and rfs from other predicates - for (auto &entry : m_tag2rule) { - const datalog::rule *r = entry.m_value; - if (!r) continue; - find_predecessors(*r, m_predicates); + for (auto &kv : m_pt_rules) { + const datalog::rule &r = kv.m_value->rule(); + find_predecessors(r, m_predicates); if (m_predicates.empty()) continue; for (unsigned i = 0, sz = m_predicates.size(); i < sz; ++i) { const pred_transformer &pt = ctx.get_pred_transformer(m_predicates[i]); // assert lemmas of pt - updt_solver_with_lemmas(solver, pt, to_app(entry.m_key), i); + updt_solver_with_lemmas(solver, pt, to_app(kv.m_value->tag()), i); // assert rfs of pt - update_solver_with_rfs(solver, pt, to_app(entry.m_key), i); + update_solver_with_rfs(solver, pt, to_app(kv.m_value->tag()), i); } } } @@ -2447,6 +2405,7 @@ bool context::validate() switch(m_last_result) { case l_true: { +#if 0 expr_ref cex(m); cex = get_ground_sat_answer(); if (!cex.get()) { @@ -2454,6 +2413,14 @@ bool context::validate() throw default_exception("Cex validation failed\n"); return false; } +#endif + proof_ref cex(m); + cex = get_ground_refutation(); + if (!cex.get()) { + IF_VERBOSE(0, verbose_stream() << "Cex validation failed\n";); + throw default_exception("Cex validation failed\n"); + return false; + } break; } case l_false: { diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h index e95ddc8ec..402cb63cc 100644 --- a/src/muz/spacer/spacer_context.h +++ b/src/muz/spacer/spacer_context.h @@ -292,6 +292,64 @@ class pred_transformer { }; + class pt_rule { + const datalog::rule &m_rule; + expr_ref m_trans; // ground version of m_rule + ptr_vector m_auxs; // auxiliary variables in m_trans + app_ref_vector m_reps; // map from fv in m_rule to ground constants + app_ref m_tag; // a unique tag for the rule + + public: + pt_rule(ast_manager &m, const datalog::rule &r) : + m_rule(r), m_trans(m), m_reps(m), m_tag(m) {} + + const datalog::rule &rule() const {return m_rule;} + + void set_tag(expr *tag) {SASSERT(is_app(tag)); set_tag(to_app(tag));} + void set_tag(app* tag) {m_tag = tag;} + app* tag() const {return m_tag;} + ptr_vector &auxs() {return m_auxs;} + void set_auxs(ptr_vector &v) {m_auxs.reset(); m_auxs.append(v);} + void set_reps(app_ref_vector &v) {m_reps.reset(); m_reps.append(v);} + + void set_trans(expr_ref &v) {m_trans=v;} + expr* trans() const {return m_trans;} + bool is_init() const {return m_rule.get_uninterpreted_tail_size() == 0;} + }; + + class pt_rules { + typedef obj_map rule2ptrule; + typedef obj_map tag2ptrule; + typedef rule2ptrule::iterator iterator; + rule2ptrule m_rules; + tag2ptrule m_tags; + public: + pt_rules() {} + ~pt_rules() {for (auto &kv : m_rules) {dealloc(kv.m_value);}} + + bool find_by_rule(const datalog::rule &r, pt_rule* &ptr) { + return m_rules.find(&r, ptr); + } + bool find_by_tag(const expr* tag, pt_rule* &ptr) { + return m_tags.find(tag, ptr); + } + pt_rule &mk_rule(ast_manager &m, const datalog::rule &r) { + return mk_rule(pt_rule(m, r)); + } + pt_rule &mk_rule(const pt_rule &v); + void set_tag(expr* tag, pt_rule &v) { + pt_rule *p; + VERIFY(find_by_rule(v.rule(), p)); + p->set_tag(tag); + m_tags.insert(tag, p); + } + + bool empty() {return m_rules.empty();} + iterator begin() {return m_rules.begin();} + iterator end() {return m_rules.end();} + + }; + typedef obj_map rule2expr; typedef obj_map > rule2apps; typedef obj_map expr2rule; @@ -302,6 +360,7 @@ class pred_transformer { func_decl_ref m_head; // predicate func_decl_ref_vector m_sig; // signature ptr_vector m_use; // places where 'this' is referenced. + pt_rules m_pt_rules; // pt rules used to derive transformer ptr_vector m_rules; // rules used to derive transformer scoped_ptr m_solver; // solver context ref m_reach_solver; // context for reachability facts @@ -309,10 +368,6 @@ class pred_transformer { 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 - expr2rule m_tag2rule; // map tag predicate to rule. - rule2expr m_rule2tag; // map rule to predicate tag. - rule2expr m_rule2transition; // map rules to transition - rule2apps m_rule2vars; // map rule to auxiliary variables expr_ref_vector m_transition_clause; // extra clause for trans expr_ref m_transition; // transition relation expr_ref m_init; // initial condition @@ -337,8 +392,7 @@ class pred_transformer { // Initialization void init_rules(decl2rel const& pts); - void init_rule(decl2rel const& pts, datalog::rule const& rule, vector& is_init, - ptr_vector& rules, expr_ref_vector& transition); + void init_rule(decl2rel const& pts, datalog::rule const& rule); void init_atom(decl2rel const& pts, app * atom, app_ref_vector& var_reprs, expr_ref_vector& side, unsigned tail_idx); @@ -350,7 +404,7 @@ class pred_transformer { public: pred_transformer(context& ctx, manager& pm, func_decl* head); - ~pred_transformer(); + ~pred_transformer() {} inline bool use_native_mbp (); reach_fact *get_rf (expr *v) { @@ -372,7 +426,10 @@ public: unsigned sig_size() const {return m_sig.size();} expr* transition() const {return m_transition;} expr* init() const {return m_init;} - expr* rule2tag(datalog::rule const* r) {return m_rule2tag.find(r);} + expr* rule2tag(datalog::rule const* r) { + pt_rule *p; + return m_pt_rules.find_by_rule(*r, p) ? p->tag() : nullptr; + } unsigned get_num_levels() const {return m_frames.size ();} expr_ref get_cover_delta(func_decl* p_orig, int level); void add_cover(unsigned level, expr* property); @@ -398,8 +455,15 @@ public: const datalog::rule *find_rule(model &mev, bool& is_concrete, vector& reach_pred_used, unsigned& num_reuse_reach); - expr* get_transition(datalog::rule const& r) { return m_rule2transition.find(&r); } - ptr_vector& get_aux_vars(datalog::rule const& r) { return m_rule2vars.find(&r); } + expr* get_transition(datalog::rule const& r) { + pt_rule *p; + return m_pt_rules.find_by_rule(r, p) ? p->trans() : nullptr; + } + ptr_vector& get_aux_vars(datalog::rule const& r) { + pt_rule *p = nullptr; + VERIFY(m_pt_rules.find_by_rule(r, p)); + return p->auxs(); + } bool propagate_to_next_level(unsigned level); void propagate_to_infinity(unsigned level);