mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 04:13:38 +00:00
Code Activity

factor out inherit_properties

Browse source
This commit is contained in:
Arie Gurfinkel 2018-05-21 09:24:57 -07:00
parent 23272f0d2f
commit aeb2f3c4bb
2 changed files with 33 additions and 33 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1749,50 +1749,51 @@ app* pred_transformer::extend_initial (expr *e)
/// pred_transformer::frames /// pred_transformer::frames
bool pred_transformer::frames::add_lemma(lemma *lem) bool pred_transformer::frames::add_lemma(lemma *new_lemma)
{ {
TRACE("spacer", tout << "add-lemma: " << pp_level(lem->level()) << " " TRACE("spacer", tout << "add-lemma: " << pp_level(new_lemma->level()) << " "
<< m_pt.head()->get_name() << " " << m_pt.head()->get_name() << " "
<< mk_pp(lem->get_expr(), m_pt.get_ast_manager()) << "\n";); << mk_pp(new_lemma->get_expr(), m_pt.get_ast_manager()) << "\n";);
for (unsigned i = 0, sz = m_lemmas.size(); i < sz; ++i) { for (unsigned i = 0, sz = m_lemmas.size(); i < sz; ++i) {
if (m_lemmas [i]->get_expr() == lem->get_expr()) { if (m_lemmas[i]->get_expr() == new_lemma->get_expr()) {
m_pt.get_context().new_lemma_eh(m_pt, lem); m_pt.get_context().new_lemma_eh(m_pt, new_lemma);
// extend bindings if needed // extend bindings if needed
if (!lem->get_bindings().empty()) { if (!new_lemma->get_bindings().empty()) {
m_lemmas [i]->add_binding(lem->get_bindings()); m_lemmas[i]->add_binding(new_lemma->get_bindings());
} }
// if the lemma is at a higher level, skip it, // if the lemma is at a higher level, skip it,
// but still assert any new instances if (m_lemmas[i]->level() >= new_lemma->level()) {
if (m_lemmas [i]->level() >= lem->level()) {
TRACE("spacer", tout << "Already at a higher level: " TRACE("spacer", tout << "Already at a higher level: "
<< pp_level(m_lemmas [i]->level()) << "\n";); << pp_level(m_lemmas[i]->level()) << "\n";);
if (!lem->get_bindings().empty()) { // but, since the instances might be new, assert the
// instances that have been copied into m_lemmas[i]
if (!new_lemma->get_bindings().empty()) {
m_pt.add_lemma_core(m_lemmas[i], true); m_pt.add_lemma_core(m_lemmas[i], true);
} }
// no new lemma added
return false; return false;
} }
// update level of the existing lemma // update level of the existing lemma
m_lemmas [i]->set_level(lem->level()); m_lemmas[i]->set_level(new_lemma->level());
// assert lemma in the solver // assert lemma in the solver
m_pt.add_lemma_core(m_lemmas[i], false); m_pt.add_lemma_core(m_lemmas[i], false);
// move the lemma to its new place to maintain sortedness // move the lemma to its new place to maintain sortedness
for (unsigned j = i; (j + 1) < sz && m_lt(m_lemmas [j + 1], m_lemmas[j]); ++j) { for (unsigned j = i; (j + 1) < sz && m_lt(m_lemmas[j + 1], m_lemmas[j]); ++j) {
m_lemmas.swap (j, j+1); m_lemmas.swap (j, j+1);
} }
return true; return true;
} }
} }
// did not find, create new lemma // new_lemma is really new
m_lemmas.push_back(lem); m_lemmas.push_back(new_lemma);
m_sorted = false; m_sorted = false;
m_pt.add_lemma_core(lem); m_pt.add_lemma_core(new_lemma);
if (!lem->external()) { if (!new_lemma->external()) {
m_pt.get_context().new_lemma_eh(m_pt, lem); m_pt.get_context().new_lemma_eh(m_pt, new_lemma);
} }
return true; return true;
} }
@ -2029,10 +2030,7 @@ void context::reset()
{ {
TRACE("spacer", tout << "\n";); TRACE("spacer", tout << "\n";);
m_pob_queue.reset(); m_pob_queue.reset();
decl2rel::iterator it = m_rels.begin(), end = m_rels.end(); for (auto &entry: m_rels) {dealloc(entry.m_value);}
for (; it != end; ++it) {
dealloc(it->m_value);
}
m_rels.reset(); m_rels.reset();
m_query = nullptr; m_query = nullptr;
m_last_result = l_undef; m_last_result = l_undef;
@ -2093,22 +2091,23 @@ void context::init_rules(datalog::rule_set& rules, decl2rel& rels)
for (auto &entry : rels) {entry.m_value->init_reach_facts();} for (auto &entry : rels) {entry.m_value->init_reach_facts();}
} }
void context::inherit_properties(const decl2rel &rels) {
for (auto &entry : rels) {
pred_transformer *pt = nullptr;
if (m_rels.find(entry.m_key, pt)) {
entry.m_value->inherit_properties(*pt);
}
}
}
void context::update_rules(datalog::rule_set& rules) void context::update_rules(datalog::rule_set& rules)
{ {
decl2rel rels; decl2rel rels;
init_lemma_generalizers(rules); init_lemma_generalizers(rules);
init_rules(rules, rels); init_rules(rules, rels);
decl2rel::iterator it = rels.begin(), end = rels.end(); inherit_properties(rels);
for (; it != end; ++it) {
pred_transformer* pt = nullptr;
if (m_rels.find(it->m_key, pt)) {
it->m_value->inherit_properties(*pt);
}
}
reset(); reset();
it = rels.begin(), end = rels.end(); for (auto &entry : rels) {
for (; it != end; ++it) { m_rels.insert(entry.m_key, entry.m_value);
m_rels.insert(it->m_key, it->m_value);
} }
} }

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

@ -812,6 +812,7 @@ class context {
// Initialization // Initialization
void init_lemma_generalizers(datalog::rule_set& rules); void init_lemma_generalizers(datalog::rule_set& rules);
void inherit_properties(const decl2rel& rels);
bool check_invariant(unsigned lvl); bool check_invariant(unsigned lvl);
bool check_invariant(unsigned lvl, func_decl* fn); bool check_invariant(unsigned lvl, func_decl* fn);