mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

Skip propagation on bits that have not (yet) been fixed by the SAT core: congruence closure for bits has not necessarily propagated to all bit positions when a bit in a congruence class gets fixed.

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-01-08 08:17:18 -08:00
parent 7e3676e24a
commit 3d01246f71
1 changed files with 12 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/smt/theory_bv.cpp
View file

@ -1176,31 +1176,37 @@ namespace smt {
unsigned idx = entry.second;
if (m_wpos[v] == idx)
find_wpos(v);
find_wpos(v);
literal_vector & bits = m_bits[v];
literal bit = bits[idx];
lbool val = ctx.get_assignment(bit);
lbool val = ctx.get_assignment(bit);
if (val == l_undef) {
continue;
}
theory_var v2 = next(v);
TRACE("bv_bit_prop", tout << "propagating #" << get_enode(v)->get_owner_id() << "[" << idx << "] = " << val << "\n";);
literal antecedent = bit;
if (val == l_false) {
antecedent.neg();
}
while (v2 != v) {
literal_vector & bits2 = m_bits[v2];
literal bit2 = bits2[idx];
SASSERT(bit != ~bit2);
lbool val2 = ctx.get_assignment(bit2);
TRACE("bv_bit_prop", tout << "propagating #" << get_enode(v2)->get_owner_id() << "[" << idx << "] = " << val2 << "\n";);
if (val != val2) {
literal antecedent = bit;
literal consequent = bit2;
if (val == l_false) {
antecedent.neg();
consequent.neg();
}
SASSERT(ctx.get_assignment(antecedent) == l_true);
assign_bit(consequent, v, v2, idx, antecedent, false);
if (ctx.inconsistent()) {
TRACE("bv_bit_prop", tout << "inconsistent " << bit << " " << bit2 << "\n";);
m_prop_queue.reset();
return;
}
}