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

for Clemens: ensure fixed values are propagated after registration

Browse source 
Also allow to register expressions that the rewriter changes to ensure they get picked up.
This commit is contained in:
Nikolaj Bjorner 2022-01-19 14:38:11 +01:00
parent 5b0389615b
commit 0f03ef4ab0
7 changed files with 129 additions and 45 deletions

24
src/smt/smt_context.cpp
View file

@ -2906,6 +2906,30 @@ namespace smt {
m_user_propagator->new_fixed_eh(v, val, sz, explain);
}
bool context::is_fixed(enode* n, expr_ref& val, literal_vector& explain) {
if (m.is_bool(n->get_expr())) {
literal lit = get_literal(n->get_expr());
switch (get_assignment(lit)) {
case l_true:
val = m.mk_true(); explain.push_back(lit); return true;
case l_false:
val = m.mk_false(); explain.push_back(~lit); return true;
default:
return false;
}
}
theory_var_list * l = n->get_th_var_list();
while (l) {
theory_id tid = l->get_id();
auto* p = m_theories.get_plugin(tid);
if (p && p->is_fixed(l->get_var(), val, explain))
return true;
l = l->get_next();
}
return false;
}
void context::push() {
pop_to_base_lvl();
setup_context(false);

2
src/smt/smt_context.h
View file

@ -1747,6 +1747,8 @@ namespace smt {
assign_fixed(n, val, 1, &explain);
}
bool is_fixed(enode* n, expr_ref& val, literal_vector& explain);
void display(std::ostream & out) const;
void display_unsat_core(std::ostream & out) const;

6
src/smt/smt_theory.h
View file

@ -615,6 +615,12 @@ namespace smt {
bool is_relevant_and_shared(enode * n) const;
bool assume_eq(enode * n1, enode * n2);
/**
* \brief theory plugin for fixed values.
*/
virtual bool is_fixed(theory_var v, expr_ref& val, literal_vector & explain) { return false; }
};
};

15
src/smt/theory_bv.cpp
View file

@ -519,6 +519,21 @@ namespace smt {
}
}
bool theory_bv::is_fixed(theory_var v, expr_ref& val, literal_vector& lits) {
numeral r;
enode* n = get_enode(v);
if (!get_fixed_value(v, r))
return false;
val = m_util.mk_numeral(r, n->get_sort());
for (literal b : m_bits[v]) {
if (ctx.get_assignment(b) == l_false)
b.neg();
lits.push_back(b);
}
return true;
}
bool theory_bv::get_fixed_value(theory_var v, numeral & result) const {
result.reset();
unsigned i = 0;

1
src/smt/theory_bv.h
View file

@ -282,6 +282,7 @@ namespace smt {
void collect_statistics(::statistics & st) const override;
bool get_fixed_value(app* x, numeral & result) const;
bool is_fixed(theory_var v, expr_ref& val, literal_vector& explain) override;
bool check_assignment(theory_var v);
bool check_invariant();

105
src/smt/theory_user_propagator.cpp
View file

@ -40,11 +40,24 @@ void theory_user_propagator::force_push() {
unsigned theory_user_propagator::add_expr(expr* e) {
force_push();
expr_ref r(m);
ctx.get_rewriter()(e, r);
if (r != e) {
r = m.mk_fresh_const("aux-expr", e->get_sort());
expr_ref eq(m.mk_eq(r, e), m);
ctx.assert_expr(eq);
ctx.internalize_assertions();
e = r;
ctx.mark_as_relevant(eq);
}
enode* n = ensure_enode(e);
if (is_attached_to_var(n))
return n->get_th_var(get_id());
theory_var v = mk_var(n);
ctx.attach_th_var(n, this, v);
literal_vector explain;
if (ctx.is_fixed(n, r, explain))
m_prop.push_back(prop_info(explain, v, r));
return v;
}
@ -118,54 +131,66 @@ bool theory_user_propagator::can_propagate() {
return m_qhead < m_prop.size();
}
void theory_user_propagator::propagate_consequence(prop_info const& prop) {
justification* js;
m_lits.reset();
m_eqs.reset();
for (unsigned id : prop.m_ids)
m_lits.append(m_id2justification[id]);
for (auto const& p : prop.m_eqs)
m_eqs.push_back(enode_pair(get_enode(p.first), get_enode(p.second)));
DEBUG_CODE(for (auto const& p : m_eqs) VERIFY(p.first->get_root() == p.second->get_root()););
DEBUG_CODE(for (unsigned id : prop.m_ids) VERIFY(m_fixed.contains(id)););
DEBUG_CODE(for (literal lit : m_lits) VERIFY(ctx.get_assignment(lit) == l_true););
TRACE("user_propagate", tout << "propagating #" << prop.m_conseq->get_id() << ": " << prop.m_conseq << "\n");
if (m.is_false(prop.m_conseq)) {
js = ctx.mk_justification(
ext_theory_conflict_justification(
get_id(), ctx.get_region(), m_lits.size(), m_lits.data(), m_eqs.size(), m_eqs.data(), 0, nullptr));
ctx.set_conflict(js);
}
else {
for (auto& lit : m_lits)
lit.neg();
for (auto const& [a,b] : m_eqs)
m_lits.push_back(~mk_eq(a->get_expr(), b->get_expr(), false));
literal lit;
if (has_quantifiers(prop.m_conseq)) {
expr_ref fn(m.mk_fresh_const("aux-literal", m.mk_bool_sort()), m);
expr_ref eq(m.mk_eq(fn, prop.m_conseq), m);
ctx.assert_expr(eq);
ctx.internalize_assertions();
lit = mk_literal(fn);
}
else
lit = mk_literal(prop.m_conseq);
ctx.mark_as_relevant(lit);
m_lits.push_back(lit);
ctx.mk_th_lemma(get_id(), m_lits);
TRACE("user_propagate", ctx.display(tout););
}
}
void theory_user_propagator::propagate_new_fixed(prop_info const& prop) {
new_fixed_eh(prop.m_var, prop.m_conseq, prop.m_lits.size(), prop.m_lits.data());
}
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())
return;
force_push();
unsigned qhead = m_qhead;
justification* js;
while (qhead < m_prop.size() && !ctx.inconsistent()) {
auto const& prop = m_prop[qhead];
m_lits.reset();
m_eqs.reset();
for (unsigned id : prop.m_ids)
m_lits.append(m_id2justification[id]);
for (auto const& p : prop.m_eqs)
m_eqs.push_back(enode_pair(get_enode(p.first), get_enode(p.second)));
DEBUG_CODE(for (auto const& p : m_eqs) VERIFY(p.first->get_root() == p.second->get_root()););
DEBUG_CODE(for (unsigned id : prop.m_ids) VERIFY(m_fixed.contains(id)););
DEBUG_CODE(for (literal lit : m_lits) VERIFY(ctx.get_assignment(lit) == l_true););
TRACE("user_propagate", tout << "propagating #" << prop.m_conseq->get_id() << ": " << prop.m_conseq << "\n");
if (m.is_false(prop.m_conseq)) {
js = ctx.mk_justification(
ext_theory_conflict_justification(
get_id(), ctx.get_region(), m_lits.size(), m_lits.data(), m_eqs.size(), m_eqs.data(), 0, nullptr));
ctx.set_conflict(js);
}
else {
for (auto& lit : m_lits)
lit.neg();
for (auto const& [a,b] : m_eqs)
m_lits.push_back(~mk_eq(a->get_expr(), b->get_expr(), false));
literal lit;
if (has_quantifiers(prop.m_conseq)) {
expr_ref fn(m.mk_fresh_const("aux-literal", m.mk_bool_sort()), m);
expr_ref eq(m.mk_eq(fn, prop.m_conseq), m);
ctx.assert_expr(eq);
ctx.internalize_assertions();
lit = mk_literal(fn);
}
else
lit = mk_literal(prop.m_conseq);
ctx.mark_as_relevant(lit);
m_lits.push_back(lit);
ctx.mk_th_lemma(get_id(), m_lits);
TRACE("user_propagate", ctx.display(tout););
}
if (prop.m_var == null_theory_var)
propagate_consequence(prop);
else
propagate_new_fixed(prop);
++m_stats.m_num_propagations;
++qhead;
}

21
src/smt/theory_user_propagator.h
View file

@ -30,16 +30,24 @@ namespace smt {
class theory_user_propagator : public theory, public user_propagator::callback {
struct prop_info {
unsigned_vector m_ids;
expr_ref m_conseq;
unsigned_vector m_ids;
expr_ref m_conseq;
svector<std::pair<unsigned, unsigned>> m_eqs;
prop_info(unsigned num_fixed, unsigned const* fixed_ids, unsigned num_eqs, unsigned const* eq_lhs, unsigned const* eq_rhs, expr_ref const& c):
literal_vector m_lits;
theory_var m_var = null_theory_var;
prop_info(unsigned num_fixed, unsigned const* fixed_ids,
unsigned num_eqs, unsigned const* eq_lhs, unsigned const* eq_rhs, expr_ref const& c):
m_ids(num_fixed, fixed_ids),
m_conseq(c)
{
m_conseq(c) {
for (unsigned i = 0; i < num_eqs; ++i)
m_eqs.push_back(std::make_pair(eq_lhs[i], eq_rhs[i]));
}
prop_info(literal_vector const& lits, theory_var v, expr_ref const& val):
m_conseq(val),
m_lits(lits),
m_var(v) {}
};
struct stats {
@ -71,6 +79,9 @@ namespace smt {
void force_push();
void propagate_consequence(prop_info const& prop);
void propagate_new_fixed(prop_info const& prop);
public:
theory_user_propagator(context& ctx);