mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-16 02:46:16 +00:00
Code Activity

dealing with quantifier reference counts

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-05-14 23:05:07 +03:00
parent f989e4eb38
commit e0c3b4a77d
1 changed files with 19 additions and 23 deletions
Download patch file Download diff file Expand all files Collapse all files

42
src/smt/smt_model_finder.cpp
View file

@ -598,7 +598,7 @@ namespace smt {
for (expr* e : exceptions) { for (expr* e : exceptions) {
expr * val = eval(e, true); expr * val = eval(e, true);
SASSERT(val != 0); SASSERT(val != nullptr);
r.push_back(val); r.push_back(val);
} }
@ -606,7 +606,7 @@ namespace smt {
node * n = a->get_root(); node * n = a->get_root();
if (!n->is_mono_proj() && n->get_else() != nullptr) { if (!n->is_mono_proj() && n->get_else() != nullptr) {
expr * val = eval(n->get_else(), true); expr * val = eval(n->get_else(), true);
SASSERT(val != 0); SASSERT(val != nullptr);
r.push_back(val); r.push_back(val);
} }
} }
@ -629,7 +629,7 @@ namespace smt {
expr * t = kv.m_key; expr * t = kv.m_key;
unsigned gen = kv.m_value; unsigned gen = kv.m_value;
expr * t_val = eval(t, true); expr * t_val = eval(t, true);
SASSERT(t_val != 0); SASSERT(t_val != nullptr);
bool found = false; bool found = false;
for (expr* v : ex_vals) { for (expr* v : ex_vals) {
if (!m.are_distinct(t_val, v)) { if (!m.are_distinct(t_val, v)) {
@ -1203,7 +1203,7 @@ namespace smt {
if (uvar_inst_sets[m_var_j] == 0) if (uvar_inst_sets[m_var_j] == 0)
uvar_inst_sets[m_var_j] = alloc(instantiation_set, ctx->get_manager()); uvar_inst_sets[m_var_j] = alloc(instantiation_set, ctx->get_manager());
instantiation_set * s = uvar_inst_sets[m_var_j]; instantiation_set * s = uvar_inst_sets[m_var_j];
SASSERT(s != 0); SASSERT(s != nullptr);
for (enode * n : ctx->enodes_of(m_f)) { for (enode * n : ctx->enodes_of(m_f)) {
if (ctx->is_relevant(n)) { if (ctx->is_relevant(n)) {
@ -1689,6 +1689,7 @@ namespace smt {
*/ */
class quantifier_info { class quantifier_info {
model_finder& m_mf; model_finder& m_mf;
quantifier_ref m_q; // original quantifier
quantifier_ref m_flat_q; // flat version of the quantifier quantifier_ref m_flat_q; // flat version of the quantifier
bool m_is_auf; bool m_is_auf;
bool m_has_x_eq_y; bool m_has_x_eq_y;
@ -1728,6 +1729,7 @@ namespace smt {
quantifier_info(model_finder& mf, ast_manager & m, quantifier * q): quantifier_info(model_finder& mf, ast_manager & m, quantifier * q):
m_mf(mf), m_mf(mf),
m_q(q, m),
m_flat_q(m), m_flat_q(m),
m_is_auf(true), m_is_auf(true),
m_has_x_eq_y(false), m_has_x_eq_y(false),
@ -2418,14 +2420,11 @@ namespace smt {
proto_model * m_model; proto_model * m_model;
quantifier_info * get_qinfo(quantifier * q) const { quantifier_info * get_qinfo(quantifier * q) const {
quantifier_info * qi = nullptr; return m_q2info[q];
m_q2info.find(q, qi);
SASSERT(qi != 0);
return qi;
} }
void set_else_interp(func_decl * f, expr * f_else) { void set_else_interp(func_decl * f, expr * f_else) {
SASSERT(f_else != 0); SASSERT(f_else != nullptr);
func_interp * fi = m_model->get_func_interp(f); func_interp * fi = m_model->get_func_interp(f);
if (fi == nullptr) { if (fi == nullptr) {
fi = alloc(func_interp, m, f->get_arity()); fi = alloc(func_interp, m, f->get_arity());
@ -2494,7 +2493,7 @@ namespace smt {
if (!contains(f, qs, q)) { if (!contains(f, qs, q)) {
qi->set_the_one(f); qi->set_the_one(f);
expr * f_else = m->get_def(); expr * f_else = m->get_def();
SASSERT(f_else != 0); SASSERT(f_else != nullptr);
// Remark: I can ignore the conditions of m because // Remark: I can ignore the conditions of m because
// I know the (partial) interpretation of f satisfied the ground part. // I know the (partial) interpretation of f satisfied the ground part.
// MBQI will force extra instantiations if the (partial) interpretation of f // MBQI will force extra instantiations if the (partial) interpretation of f
@ -2587,7 +2586,7 @@ namespace smt {
m_q_f.insert(f, s); m_q_f.insert(f, s);
m_qsets.push_back(s); m_qsets.push_back(s);
} }
SASSERT(s != 0); SASSERT(s != nullptr);
s->insert(q); s->insert(q);
} }
@ -2598,7 +2597,7 @@ namespace smt {
m_f2defs.insert(f, s); m_f2defs.insert(f, s);
m_esets.push_back(s); m_esets.push_back(s);
} }
SASSERT(s != 0); SASSERT(s != nullptr);
s->insert(def); s->insert(def);
} }
@ -2611,7 +2610,7 @@ namespace smt {
insert_f2def(f, def); insert_f2def(f, def);
m_qsets.push_back(s); m_qsets.push_back(s);
} }
SASSERT(s != 0); SASSERT(s != nullptr);
s->insert(q); s->insert(q);
} }
@ -2620,7 +2619,7 @@ namespace smt {
quantifier_set * get_q_f_def(func_decl * f, expr * def) { quantifier_set * get_q_f_def(func_decl * f, expr * def) {
quantifier_set * s = nullptr; quantifier_set * s = nullptr;
m_q_f_def.find(f, def, s); m_q_f_def.find(f, def, s);
SASSERT(s != 0); SASSERT(s != nullptr);
return s; return s;
} }
@ -2771,8 +2770,8 @@ namespace smt {
for (quantifier * q : m_satisfied) { for (quantifier * q : m_satisfied) {
SASSERT(!m_residue.contains(q)); SASSERT(!m_residue.contains(q));
quantifier_info * qi = get_qinfo(q); quantifier_info * qi = get_qinfo(q);
SASSERT(qi != 0); SASSERT(qi != nullptr);
SASSERT(qi->get_the_one() != 0); SASSERT(qi->get_the_one() != nullptr);
}); });
return true; return true;
} }
@ -3060,7 +3059,7 @@ namespace smt {
func_decl * f = m->get_f(); func_decl * f = m->get_f();
TRACE("model_finder", tout << "considering macro for: " << f->get_name() << "\n"; TRACE("model_finder", tout << "considering macro for: " << f->get_name() << "\n";
m->display(tout); tout << "\n";); m->display(tout); tout << "\n";);
SASSERT(m_qi_params != 0); SASSERT(m_qi_params != nullptr);
if (m->is_unconditional() && (!qi->is_auf() || m->get_weight() >= m_qi_params->m_mbqi_force_template)) { if (m->is_unconditional() && (!qi->is_auf() || m->get_weight() >= m_qi_params->m_mbqi_force_template)) {
full_macros.insert(f, std::make_pair(m, q)); full_macros.insert(f, std::make_pair(m, q));
cond_macros.erase(f); cond_macros.erase(f);
@ -3186,10 +3185,7 @@ namespace smt {
} }
mf::quantifier_info * model_finder::get_quantifier_info(quantifier * q) const { mf::quantifier_info * model_finder::get_quantifier_info(quantifier * q) const {
quantifier_info * info = nullptr; return m_q2info[q];
m_q2info.find(q, info);
SASSERT(info != 0);
return info;
} }
void model_finder::set_context(context * ctx) { void model_finder::set_context(context * ctx) {
@ -3221,8 +3217,8 @@ namespace smt {
quantifier * q = m_quantifiers[i]; quantifier * q = m_quantifiers[i];
SASSERT(m_q2info.contains(q)); SASSERT(m_q2info.contains(q));
quantifier_info * info = get_quantifier_info(q); quantifier_info * info = get_quantifier_info(q);
dealloc(info);
m_q2info.erase(q); m_q2info.erase(q);
dealloc(info);
} }
m_quantifiers.shrink(old_size); m_quantifiers.shrink(old_size);
} }
@ -3355,7 +3351,7 @@ namespace smt {
// it must have been satisfied by "macro"/"hint". // it must have been satisfied by "macro"/"hint".
quantifier_info * qinfo = get_quantifier_info(q); quantifier_info * qinfo = get_quantifier_info(q);
SASSERT(qinfo); SASSERT(qinfo);
SASSERT(qinfo->get_the_one() != 0); SASSERT(qinfo->get_the_one() != nullptr);
return qinfo->get_macro_based_inst_set(i, m_context, *(m_auf_solver.get())); return qinfo->get_macro_based_inst_set(i, m_context, *(m_auf_solver.get()));
} }