From ec64b93edb085ea051cf62cbe9af2d693e6affdb Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Mon, 6 Nov 2023 10:41:12 +0100 Subject: [PATCH] Should we really prefer bit constraints? --- src/math/polysat/viable.cpp | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp index c18843d70..78113e661 100644 --- a/src/math/polysat/viable.cpp +++ b/src/math/polysat/viable.cpp @@ -1065,8 +1065,13 @@ namespace { return false; } // 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"; - out_fbi.set_just(bit.position, e1); + if (prev == l_undef) { + out_fbi.set_just(bit.position, e1); + } } 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()) {