mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 12:53:38 +00:00
Code Activity

no more unassigned constraints in value propagation

Browse source
This commit is contained in:
Jakob Rath 2023-03-29 15:49:31 +02:00
parent d7930b3997
commit 1f58a906ed
1 changed files with 1 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/math/polysat/solver.cpp
View file

@ -937,9 +937,7 @@ namespace polysat {
unsigned lvl = 0; unsigned lvl = 0;
for (signed_constraint c : m_viable.get_constraints(v)) { for (signed_constraint c : m_viable.get_constraints(v)) {
LOG("due to: " << lit_pp(*this, c)); LOG("due to: " << lit_pp(*this, c));
if (!m_bvars.is_assigned(c.blit())) // side condition, irrelevant because all vars are already in the main condition VERIFY(m_bvars.is_assigned(c.blit()));
continue;
SASSERT(m_bvars.is_assigned(c.blit()));
lvl = std::max(lvl, m_bvars.level(c.blit())); lvl = std::max(lvl, m_bvars.level(c.blit()));
for (pvar w : c->vars()) for (pvar w : c->vars())
if (is_assigned(w)) // TODO: question of which variables are relevant. e.g., v1 > v0 implies v1 > 0 without dependency on v0. maybe add a lemma v1 > v0 --> v1 > 0 on the top level to reduce false variable dependencies? instead of handling such special cases separately everywhere. if (is_assigned(w)) // TODO: question of which variables are relevant. e.g., v1 > v0 implies v1 > 0 without dependency on v0. maybe add a lemma v1 > v0 --> v1 > 0 on the top level to reduce false variable dependencies? instead of handling such special cases separately everywhere.