mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

user propagator fixes

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-08-19 19:32:23 -07:00
parent de65c61ebc
commit ba4a218fc0
4 changed files with 22 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/smt/smt_context.cpp
View file

@ -2880,6 +2880,7 @@ namespace smt {
std::function<void(void*)>& push_eh,
std::function<void(void*, unsigned)>& pop_eh,
std::function<void*(void*)>& fresh_eh) {
setup_context(m_fparams.m_auto_config);
m_user_propagator = alloc(user_propagator, *this);
m_user_propagator->add(ctx, fixed_eh, push_eh, pop_eh, fresh_eh);
for (unsigned i = m_scopes.size(); i-- > 0; )

2
src/smt/smt_internalizer.cpp
View file

@ -795,7 +795,7 @@ namespace smt {
// and a theory variable must be created for it.
enode * e = get_enode(n);
if (!th->is_attached_to_var(e))
internalize_theory_term(n);
th->internalize_term(n);
}
return;
}

19
src/smt/user_propagator.cpp
View file

@ -49,6 +49,17 @@ unsigned user_propagator::add_expr(expr* e) {
return v;
}
void user_propagator::add_propagation(unsigned sz, unsigned const* ids, expr* conseq) {
m_prop.push_back(prop_info(sz, ids, expr_ref(conseq, m)));
}
theory * user_propagator::mk_fresh(context * new_ctx) {
auto* th = alloc(user_propagator, *new_ctx);
void* ctx = m_fresh_eh(m_user_context);
th->add(ctx, m_fixed_eh, m_push_eh, m_pop_eh, m_fresh_eh);
return th;
}
void user_propagator::new_fixed_eh(theory_var v, expr* value, unsigned num_lits, literal const* jlits) {
force_push();
m_id2justification.setx(v, literal_vector(num_lits, jlits), literal_vector());
@ -77,6 +88,8 @@ bool user_propagator::can_propagate() {
}
void user_propagator::propagate() {
if (m_qhead == m_prop.size())
return;
force_push();
unsigned qhead = m_qhead;
literal_vector lits;
@ -86,7 +99,11 @@ void user_propagator::propagate() {
auto const& prop = m_prop[qhead];
lits.reset();
for (unsigned id : prop.m_ids)
lits.append(m_id2justification[id]);
for (literal lit : m_id2justification[id]) {
if (ctx.get_assignment(lit) == l_false)
lit.neg();
lits.push_back(lit);
}
if (m.is_false(prop.m_conseq)) {
js = ctx.mk_justification(
ext_theory_conflict_justification(

11
src/smt/user_propagator.h
View file

@ -72,18 +72,11 @@ namespace smt {
unsigned add_expr(expr* e);
void add_propagation(unsigned sz, unsigned const* ids, expr* conseq) {
m_prop.push_back(prop_info(sz, ids, expr_ref(conseq, m)));
}
void add_propagation(unsigned sz, unsigned const* ids, expr* conseq);
void new_fixed_eh(theory_var v, expr* value, unsigned num_lits, literal const* jlits);
theory * mk_fresh(context * new_ctx) override {
auto* th = alloc(user_propagator, *new_ctx);
void* ctx = m_fresh_eh(m_user_context);
th->add(ctx, m_fixed_eh, m_push_eh, m_pop_eh, m_fresh_eh);
return th;
}
theory * mk_fresh(context * new_ctx) override;
bool internalize_atom(app * atom, bool gate_ctx) override { UNREACHABLE(); return false; }
bool internalize_term(app * term) override { UNREACHABLE(); return false; }
void new_eq_eh(theory_var v1, theory_var v2) override { }