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

less nesting

Browse source
This commit is contained in:
Jakob Rath 2023-10-23 11:46:25 +02:00
parent 38b0976adc
commit 64ac3596bd
1 changed files with 15 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

33
src/math/polysat/viable.cpp
View file

@ -1082,27 +1082,24 @@ namespace {
for (unsigned i = 0; i < lsb.length; i++) {
lbool prev = fixed[i];
fixed[i] = to_lbool(lsb.bits.get_bit(i));
if (prev != l_undef) {
if (fixed[i] != prev) {
// LOG("Positive parity conflicting " << e1->src << " with " << just_src[i][0]); // NOTE: just_src may be empty if the justification is by slicing
if (add_conflict) {
add_bit_justification(out_fbi, i);
add_entry(e1);
s.set_conflict(*builder.build());
}
return false;
}
else {
// Prefer justifications from larger masks (less premises)
// TODO: Check that we don't override justifications comming from bit constraints
if (largest_lsb < lsb.length)
out_fbi.set_just(i, e1);
}
}
else {
if (prev == l_undef) {
SASSERT(just_src[i].empty());
out_fbi.set_just(i, e1);
continue;
}
if (fixed[i] != prev) {
// LOG("Positive parity conflicting " << e1->src << " with " << just_src[i][0]); // NOTE: just_src may be empty if the justification is by slicing
if (add_conflict) {
add_bit_justification(out_fbi, i);
add_entry(e1);
s.set_conflict(*builder.build());
}
return false;
}
// Prefer justifications from larger masks (less premises)
// TODO: Check that we don't override justifications coming from bit constraints
if (largest_lsb < lsb.length)
out_fbi.set_just(i, e1);
}
largest_lsb = std::max(largest_lsb, lsb.length);
}