mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

Code to update solver with all constraints of a pred_transformer

Browse source
This commit is contained in:
Arie Gurfinkel 2018-05-31 18:25:18 -07:00
parent cfcc084688
commit 70f4674b3a
2 changed files with 96 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

79
src/muz/spacer/spacer_context.cpp
View file

@ -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

27
src/muz/spacer/spacer_context.h
View file

@ -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<lemma> &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();}
};