mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 22:23:22 +00:00
Code Activity

Should we really prefer bit constraints?

Browse source
This commit is contained in:
Jakob Rath 2023-11-06 10:41:12 +01:00
parent 625ec18b0f
commit ec64b93edb
1 changed files with 6 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1065,9 +1065,14 @@ namespace {
return false; return false;
} }
// just override; we prefer bit constraints over parity as those are easier for subsumption to remove // just override; we prefer bit constraints over parity as those are easier for subsumption to remove
// do we just introduce a new justification here that subsumption will remove anyway?
// the only way it will not is if all bits are overwritten like this.
// but in that case we basically replace one parity constraint by multiple bit constraints?
// verbose_stream() << "Adding bit constraint: " << e->src[0] << " (" << bit.position << ")\n"; // verbose_stream() << "Adding bit constraint: " << e->src[0] << " (" << bit.position << ")\n";
if (prev == l_undef) {
out_fbi.set_just(bit.position, e1); out_fbi.set_just(bit.position, e1);
} }
}
else if (src->is_eq() && else if (src->is_eq() &&
simplify_clause::get_lsb(s.subst(src->to_ule().lhs()), s.subst(src->to_ule().rhs()), p, lsb, src.is_positive()) && p.is_var()) { simplify_clause::get_lsb(s.subst(src->to_ule().lhs()), s.subst(src->to_ule().rhs()), p, lsb, src.is_positive()) && p.is_var()) {
if (src.is_positive()) { if (src.is_positive()) {