mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-04 10:20:23 +00:00
Code Activity

track assertions

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-01-09 15:18:33 -08:00
parent 64ec8acd30
commit a4d4e2e483
2 changed files with 13 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/sat/smt/q_mbi.cpp
View file

@ -107,7 +107,7 @@ namespace q {
if (ctx.values2root().find(e, n) && n->class_generation() <= generation_min) if (ctx.values2root().find(e, n) && n->class_generation() <= generation_min)
eqs.push_back(m.mk_eq(sk, e)); eqs.push_back(m.mk_eq(sk, e));
} }
m_solver->assert_expr(mk_or(eqs)); assert_expr(mk_or(eqs));
} }
expr_ref mbqi::replace_model_value(expr* e) { expr_ref mbqi::replace_model_value(expr* e) {
@ -168,7 +168,7 @@ namespace q {
while (true) { while (true) {
::solver::scoped_push _sp(*m_solver); ::solver::scoped_push _sp(*m_solver);
add_universe_restriction(*qb); add_universe_restriction(*qb);
m_solver->assert_expr(qb->mbody); assert_expr(qb->mbody);
++m_stats.m_num_checks; ++m_stats.m_num_checks;
lbool r = m_solver->check_sat(0, nullptr); lbool r = m_solver->check_sat(0, nullptr);
if (r == l_undef) if (r == l_undef)
@ -219,7 +219,7 @@ namespace q {
if (!proj) if (!proj)
break; break;
add_instantiation(q, proj); add_instantiation(q, proj);
m_solver->assert_expr(m.mk_not(mk_and(eqs))); assert_expr(m.mk_not(mk_and(eqs)));
} }
return i > 0; return i > 0;
} }
@ -392,7 +392,7 @@ namespace q {
if (!m_model->eval_expr(bounds, mbounds, true)) if (!m_model->eval_expr(bounds, mbounds, true))
return; return;
mbounds = subst(mbounds, qb.vars); mbounds = subst(mbounds, qb.vars);
m_solver->assert_expr(mbounds); assert_expr(mbounds);
qb.domain_eqs.push_back(vbounds); qb.domain_eqs.push_back(vbounds);
} }
@ -425,11 +425,18 @@ namespace q {
continue; continue;
expr_ref meq = mk_or(meqs); expr_ref meq = mk_or(meqs);
expr_ref veq = mk_or(veqs); expr_ref veq = mk_or(veqs);
m_solver->assert_expr(meq); assert_expr(meq);
qb.domain_eqs.push_back(veq); qb.domain_eqs.push_back(veq);
} }
} }
void mbqi::assert_expr(expr* e) {
expr_ref _e(e, m);
TRACE("q", tout << _e << "\n");
m_solver->assert_expr(e);
}
/* /*
* Add bounds to sub-terms under uninterpreted functions for projection. * Add bounds to sub-terms under uninterpreted functions for projection.
*/ */

1
src/sat/smt/q_mbi.h
View file

@ -93,6 +93,7 @@ namespace q {
void extract_free_vars(quantifier* q, q_body& qb); void extract_free_vars(quantifier* q, q_body& qb);
void init_model(); void init_model();
void init_solver(); void init_solver();
void assert_expr(expr* e);
mbp::project_plugin* get_plugin(app* var); mbp::project_plugin* get_plugin(app* var);
void add_plugin(mbp::project_plugin* p); void add_plugin(mbp::project_plugin* p);
void add_instantiation(quantifier* q, expr_ref& proj); void add_instantiation(quantifier* q, expr_ref& proj);