diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index c621757f3..55f5fa2a6 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -864,7 +864,7 @@ void pred_transformer::simplify_formulas() {m_frames.simplify_formulas ();} -expr_ref pred_transformer::get_formulas(unsigned level) +expr_ref pred_transformer::get_formulas(unsigned level) const { expr_ref_vector res(m); m_frames.get_frame_geq_lemmas (level, res); @@ -1791,6 +1791,83 @@ app* pred_transformer::extend_initial (expr *e) } +/// \brief Update a given solver with all constraints representing +/// this pred_transformer +void pred_transformer::updt_solver(prop_solver *solver) { + + m_solver->assert_expr(m_transition); + m_solver->assert_expr(m_init, 0); + + // -- facts derivable at the head + expr_ref last_tag(m); + last_tag = m_extend_lit0; + for (auto *rf : m_reach_facts) { + if (rf->is_init()) continue; + m_solver->assert_expr(m.mk_or(last_tag, rf->get(), rf->tag())); + last_tag = m.mk_not(rf->tag()); + } + + + for (auto &entry : m_tag2rule) { + const datalog::rule *r = entry.m_value; + if (!r) continue; + 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); + // assert rfs of pt + update_solver_with_rfs(solver, pt, to_app(entry.m_key), i); + } + } +} + +void pred_transformer::updt_solver_with_lemmas(prop_solver *solver, + const pred_transformer &pt, + app* rule_tag, unsigned pos) { + expr_ref not_rule_tag(m); + not_rule_tag = m.mk_not(rule_tag); + + // XXX deal with quantified instantiations + // XXX perhaps expose lemmas, which gives better idea of what is active + expr_ref_vector fmls(m); + for (unsigned i = 0, sz = pt.get_num_levels(); i <= sz; ++i) { + expr_ref tmp(m); + if (i == sz) i = infty_level(); + tmp = pt.get_formulas(i); + flatten_and(tmp, fmls); + + for (expr *f : fmls) { + tmp = m.mk_or(not_rule_tag, f); + pm.formula_n2o(tmp, tmp, pos, !is_quantifier(f)); + m_solver->assert_expr(tmp, i); + } + } +} + +void pred_transformer::update_solver_with_rfs(prop_solver *solver, + const pred_transformer &pt, + app *rule_tag, unsigned pos) { + expr_ref last_tag(m); + expr_ref not_rule_tag(m); + not_rule_tag = m.mk_not(rule_tag); + + for (auto *rf : pt.m_reach_facts) { + expr_ref e(m); + if (last_tag) { + expr *args[4] = { m.mk_not(rule_tag), last_tag, rf->get(), rf->tag() }; + e = m.mk_or(4, args); + } + else + e = m.mk_or(m.mk_not(rule_tag), rf->get(), rf->tag()); + last_tag = m.mk_not(rf->tag()); + pm.formula_n2o(e.get(), e, pos); + solver->assert_expr(e); + } +} + /// pred_transformer::frames diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h index 924c5f9cc..d95f1185d 100644 --- a/src/muz/spacer/spacer_context.h +++ b/src/muz/spacer/spacer_context.h @@ -226,14 +226,14 @@ class pred_transformer { pred_transformer& pt () {return m_pt;} - void get_frame_lemmas (unsigned level, expr_ref_vector &out) { + void get_frame_lemmas (unsigned level, expr_ref_vector &out) const { for (auto &lemma : m_lemmas) { if (lemma->level() == level) { out.push_back(lemma->get_expr()); } } } - void get_frame_geq_lemmas (unsigned level, expr_ref_vector &out) { + void get_frame_geq_lemmas (unsigned level, expr_ref_vector &out) const { for (auto &lemma : m_lemmas) { if(lemma->level() >= level) { out.push_back(lemma->get_expr()); @@ -366,7 +366,7 @@ public: expr* transition() const {return m_transition;} expr* init() const {return m_init;} expr* rule2tag(datalog::rule const* r) {return m_rule2tag.find(r);} - unsigned get_num_levels() {return m_frames.size ();} + 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); expr_ref get_reachable(); @@ -438,7 +438,7 @@ public: bool check_inductive(unsigned level, expr_ref_vector& state, unsigned& assumes_level, unsigned weakness = UINT_MAX); - expr_ref get_formulas(unsigned level); + expr_ref get_formulas(unsigned level) const; void simplify_formulas(); @@ -465,6 +465,15 @@ public: void mbp(app_ref_vector &vars, expr_ref &fml, const model_ref &mdl, bool reduce_all_selects = true); + void updt_solver(prop_solver *solver); + + void updt_solver_with_lemmas(prop_solver *solver, + const pred_transformer &pt, + app *rule_tag, unsigned pos); + void update_solver_with_rfs(prop_solver *solver, + const pred_transformer &pt, + app *rule_tag, unsigned pos); + }; @@ -566,8 +575,8 @@ public: const ptr_vector &lemmas() {return m_lemmas;} void add_lemma(lemma* new_lemma) {m_lemmas.push_back(new_lemma);} - bool is_ground () { return m_binding.empty (); } - unsigned get_free_vars_size() { return m_binding.size(); } + bool is_ground () const { return m_binding.empty (); } + unsigned get_free_vars_size() const { return m_binding.size(); } app_ref_vector const &get_binding() const {return m_binding;} /* * Returns a map from variable id to skolems that implicitly @@ -718,9 +727,9 @@ public: void set_root(pob& n); bool is_root (pob& n) const {return m_root.get () == &n;} - unsigned max_level() {return m_max_level;} - unsigned min_depth() {return m_min_depth;} - size_t size() {return m_obligations.size();} + unsigned max_level() const {return m_max_level;} + unsigned min_depth() const {return m_min_depth;} + size_t size() const {return m_obligations.size();} };