mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity

allow add_expr during pop

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-04-06 16:27:10 +02:00
parent b0dce5b27d
commit 0fa0feb979
2 changed files with 32 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

36
src/smt/theory_user_propagator.cpp
View file

@ -24,7 +24,8 @@ using namespace smt;
theory_user_propagator::theory_user_propagator(context& ctx):
theory(ctx, ctx.get_manager().mk_family_id(user_propagator::plugin::name())),
m_var2expr(ctx.get_manager())
m_var2expr(ctx.get_manager()),
m_to_add(ctx.get_manager())
{}
theory_user_propagator::~theory_user_propagator() {
@ -33,9 +34,11 @@ theory_user_propagator::~theory_user_propagator() {
void theory_user_propagator::force_push() {
for (; m_num_scopes > 0; --m_num_scopes) {
flet<bool> _pushing(m_push_popping, true);
theory::push_scope_eh();
m_push_eh(m_user_context);
m_prop_lim.push_back(m_prop.size());
m_to_add_lim.push_back(m_to_add.size());
m_push_eh(m_user_context);
}
}
@ -82,6 +85,7 @@ void theory_user_propagator::propagate_cb(
expr* conseq) {
CTRACE("user_propagate", ctx.lit_internalized(conseq) && ctx.get_assignment(ctx.get_literal(conseq)) == l_true,
ctx.display(tout << "redundant consequence: " << mk_pp(conseq, m) << "\n"));
expr_ref _conseq(conseq, m);
ctx.get_rewriter()(conseq, _conseq);
if (ctx.lit_internalized(_conseq) && ctx.get_assignment(ctx.get_literal(_conseq)) == l_true)
@ -90,7 +94,10 @@ void theory_user_propagator::propagate_cb(
}
void theory_user_propagator::register_cb(expr* e) {
add_expr(e, true);
if (m_push_popping)
m_to_add.push_back(e);
else
add_expr(e, true);
}
theory * theory_user_propagator::mk_fresh(context * new_ctx) {
@ -144,25 +151,29 @@ void theory_user_propagator::new_fixed_eh(theory_var v, expr* value, unsigned nu
}
}
void theory_user_propagator::push_scope_eh() {
void theory_user_propagator::push_scope_eh() {
++m_num_scopes;
}
void theory_user_propagator::pop_scope_eh(unsigned num_scopes) {
flet<bool> _popping(m_push_popping, true);
unsigned n = std::min(num_scopes, m_num_scopes);
m_num_scopes -= n;
num_scopes -= n;
if (num_scopes == 0)
return;
m_pop_eh(m_user_context, num_scopes);
theory::pop_scope_eh(num_scopes);
unsigned old_sz = m_prop_lim.size() - num_scopes;
m_prop.shrink(m_prop_lim[old_sz]);
m_prop_lim.shrink(old_sz);
old_sz = m_to_add_lim.size() - num_scopes;
m_to_add.shrink(m_to_add_lim[old_sz]);
m_to_add_lim.shrink(old_sz);
m_pop_eh(m_user_context, num_scopes);
}
bool theory_user_propagator::can_propagate() {
return m_qhead < m_prop.size();
return m_qhead < m_prop.size() || !m_to_add.empty();
}
void theory_user_propagator::propagate_consequence(prop_info const& prop) {
@ -215,10 +226,19 @@ void theory_user_propagator::propagate_new_fixed(prop_info const& prop) {
void theory_user_propagator::propagate() {
TRACE("user_propagate", tout << "propagating queue head: " << m_qhead << " prop queue: " << m_prop.size() << "\n");
if (m_qhead == m_prop.size())
if (m_qhead == m_prop.size() && m_to_add_qhead == m_to_add.size())
return;
force_push();
unsigned qhead = m_qhead;
unsigned qhead = m_to_add_qhead;
if (qhead < m_to_add.size()) {
for (; qhead < m_to_add.size(); ++qhead)
add_expr(m_to_add.get(qhead), true);
ctx.push_trail(value_trail<unsigned>(m_to_add_qhead));
m_to_add_qhead = qhead;
}
qhead = m_qhead;
while (qhead < m_prop.size() && !ctx.inconsistent()) {
auto const& prop = m_prop[qhead];
if (prop.m_var == null_theory_var)

4
src/smt/theory_user_propagator.h
View file

@ -78,6 +78,10 @@ namespace smt {
stats m_stats;
expr_ref_vector m_var2expr;
unsigned_vector m_expr2var;
bool m_push_popping;
expr_ref_vector m_to_add;
unsigned_vector m_to_add_lim;
unsigned m_to_add_qhead = 0;
expr* var2expr(theory_var v) { return m_var2expr.get(v); }
theory_var expr2var(expr* e) { check_defined(e); return m_expr2var[e->get_id()]; }