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

enable fixed bits in slicing

Browse source
This commit is contained in:
Jakob Rath 2023-08-17 17:37:11 +02:00
parent 996012adb1
commit 6593754cd6
1 changed files with 4 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1233,7 +1233,7 @@ namespace polysat {
void slicing::add_constraint(signed_constraint c) {
LOG(c);
SASSERT(!is_conflict());
#if 0
#if 1
if (!add_fixed_bits(c))
return;
#endif
@ -1246,6 +1246,8 @@ namespace polysat {
// - we don't prioritize constraints that set larger bit ranges
// e.g., c1 sets 3 lower bits, and c2 sets 5 lower bits.
// slicing may have both {c1,c2} in justifications while previously we always prefer c2.
// - instead of prioritizing constraints (which is annoying to do incrementally), let subsumption take care of this issue.
// if constraint C subsumes constraint D, then we might even want to completely deactivate D in the solver? (not easy if D is on higher level than C).
// - (we could wait until propagate() to add fixed bits to the egraph. but that would only work on a single decision level.)
if (c->vars().size() != 1)
return true;
@ -1257,6 +1259,7 @@ namespace polysat {
}
bool slicing::add_fixed_bits(pvar x, unsigned hi, unsigned lo, rational const& value, sat::literal lit) {
LOG("add_fixed_bits: v" << x << "[" << hi << ":" << lo << "] = " << value << " by " << lit_pp(m_solver, lit));
enode_vector& xs = m_tmp3;
SASSERT(xs.empty());
mk_slice(var2slice(x), hi, lo, xs, false, false);