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

fix #4795

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-11-27 18:00:36 -08:00
parent df09cb7c95
commit 6e14d3fbd3
2 changed files with 35 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

40
src/smt/theory_bv.cpp
View file

@ -49,7 +49,6 @@ namespace smt {
unsigned bv_size = get_bv_size(n);
bool is_relevant = ctx.is_relevant(n);
literal_vector & bits = m_bits[v];
TRACE("bv", tout << "v" << v << "\n";);
bits.reset();
m_bits_expr.reset();
@ -65,6 +64,12 @@ namespace smt {
ctx.mark_as_relevant(b);
}
}
TRACE("bv", tout << "v" << v << " #" << owner->get_id() << "\n";
for (unsigned i = 0; i < bv_size; i++)
tout << mk_bounded_pp(m_bits_expr[i], m) << "\n";
);
}
class mk_atom_trail : public trail<theory_bv> {
@ -217,12 +222,17 @@ namespace smt {
}
};
void theory_bv::add_new_diseq_axiom(theory_var v1, theory_var v2, unsigned idx) {
if (!params().m_bv_eq_axioms)
return;
m_prop_diseqs.push_back(bv_diseq(v1, v2, idx));
ctx.push_trail(push_back_vector<context, svector<bv_diseq>>(m_prop_diseqs));
}
/**
\brief v1[idx] = ~v2[idx], then v1 /= v2 is a theory axiom.
*/
void theory_bv::mk_new_diseq_axiom(theory_var v1, theory_var v2, unsigned idx) {
if (!params().m_bv_eq_axioms)
return;
void theory_bv::assert_new_diseq_axiom(theory_var v1, theory_var v2, unsigned idx) {
SASSERT(m_bits[v1][idx] == ~m_bits[v2][idx]);
TRACE("bv_diseq_axiom", tout << "found new diseq axiom\n"; display_var(tout, v1); display_var(tout, v2););
// found new disequality
@ -260,7 +270,7 @@ namespace smt {
theory_var v2 = occs->m_var;
unsigned idx2 = occs->m_idx;
if (idx == idx2 && m_bits[v2][idx2] == l && get_bv_size(v2) == get_bv_size(v))
mk_new_diseq_axiom(v, v2, idx);
add_new_diseq_axiom(v, v2, idx);
occs = occs->m_next;
}
}
@ -1160,7 +1170,6 @@ namespace smt {
m_diseq_watch[watch_var].push_back(std::make_pair(v1, v2));
m_diseq_watch_trail.push_back(watch_var);
return;
//m_replay_diseq.push_back(std::make_pair(v1, v2));
}
}
@ -1329,7 +1338,7 @@ namespace smt {
}
void theory_bv::relevant_eh(app * n) {
TRACE("bv", tout << "relevant: " << ctx.e_internalized(n) << ": " << mk_pp(n, m) << "\n";);
TRACE("bv", tout << "relevant: #" << n->get_id() << " " << ctx.e_internalized(n) << ": " << mk_pp(n, m) << "\n";);
if (m.is_bool(n)) {
bool_var v = ctx.get_bool_var(n);
atom * a = get_bv2a(v);
@ -1355,6 +1364,8 @@ namespace smt {
theory_var v = e->get_th_var(get_id());
if (v != null_theory_var) {
literal_vector & bits = m_bits[v];
TRACE("bv", tout << "mark bits relevant: " << bits.size() << ": " << bits << "\n";);
SASSERT(!is_bv(v) || bits.size() == get_bv_size(v));
for (literal lit : bits) {
ctx.mark_as_relevant(lit);
}
@ -1543,7 +1554,7 @@ namespace smt {
// conflict was detected ... v1 and v2 have complementary bits
SASSERT(m_bits[v1][zo.m_idx] == ~(m_bits[v2][zo.m_idx]));
SASSERT(m_bits[v1].size() == m_bits[v2].size());
mk_new_diseq_axiom(v1, v2, zo.m_idx);
add_new_diseq_axiom(v1, v2, zo.m_idx);
reset_merge_aux();
return false;
}
@ -1559,13 +1570,12 @@ namespace smt {
}
void theory_bv::propagate() {
unsigned sz = m_replay_diseq.size();
if (sz > 0) {
for (unsigned i = 0; i < sz; ++i) {
auto const& p = m_replay_diseq[i];
expand_diseq(p.first, p.second);
}
m_replay_diseq.reset();
if (!can_propagate())
return;
ctx.push_trail(value_trail<context, unsigned>(m_prop_diseqs_qhead));
for (; m_prop_diseqs_qhead < m_prop_diseqs.size() && !ctx.inconsistent(); ++m_prop_diseqs_qhead) {
auto p = m_prop_diseqs[m_prop_diseqs_qhead];
assert_new_diseq_axiom(p.v1, p.v2, p.idx);
}
}

13
src/smt/theory_bv.h
View file

@ -125,7 +125,13 @@ namespace smt {
mutable vector<rational> m_power2;
unsigned char m_eq_activity[256];
svector<std::pair<theory_var, theory_var>> m_replay_diseq;
struct bv_diseq {
theory_var v1, v2;
unsigned idx;
bv_diseq(theory_var v1, theory_var v2, unsigned idx):v1(v1), v2(v2), idx(idx) {}
};
svector<bv_diseq> m_prop_diseqs;
unsigned m_prop_diseqs_qhead { 0 };
vector<vector<std::pair<theory_var, theory_var>>> m_diseq_watch;
unsigned char m_diseq_activity[256];
svector<bool_var> m_diseq_watch_trail;
@ -162,7 +168,8 @@ namespace smt {
void get_arg_bits(app * n, unsigned idx, expr_ref_vector & r);
friend class add_var_pos_trail;
void simplify_bit(expr * s, expr_ref & r);
void mk_new_diseq_axiom(theory_var v1, theory_var v2, unsigned idx);
void add_new_diseq_axiom(theory_var v1, theory_var v2, unsigned idx);
void assert_new_diseq_axiom(theory_var v1, theory_var v2, unsigned idx);
friend class register_true_false_bit_trail;
void register_true_false_bit(theory_var v, unsigned idx);
void find_new_diseq_axioms(var_pos_occ * occs, theory_var v, unsigned idx);
@ -240,7 +247,7 @@ namespace smt {
bool include_func_interp(func_decl* f) override;
svector<theory_var> m_merge_aux[2]; //!< auxiliary vector used in merge_zero_one_bits
bool merge_zero_one_bits(theory_var r1, theory_var r2);
bool can_propagate() override { return !m_replay_diseq.empty(); }
bool can_propagate() override { return m_prop_diseqs_qhead < m_prop_diseqs.size(); }
void propagate() override;
// -----------------------------------