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

fix propagation when variables are assigned

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-04-07 13:27:36 +02:00
parent 704a41ee36
commit fde78f99c3
1 changed files with 7 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -292,8 +292,7 @@ namespace polysat {
if (!is_assigned(other_v)) { if (!is_assigned(other_v)) {
add_watch(c, other_v); add_watch(c, other_v);
std::swap(c->vars()[idx], c->vars()[i]); std::swap(c->vars()[idx], c->vars()[i]);
SASSERT(!is_assigned(c->var(0))); if (!is_assigned(c->var(1 - idx)))
SASSERT(!is_assigned(c->var(1)));
return true; return true;
} }
} }
@ -437,7 +436,11 @@ namespace polysat {
void solver::add_watch(signed_constraint c) { void solver::add_watch(signed_constraint c) {
SASSERT(c); SASSERT(c);
auto const& vars = c->vars(); auto& vars = c->vars();
unsigned i = 0, j = 0, sz = vars.size();
for (; i < sz && j < 2; ++i)
if (!is_assigned(vars[i]))
std::swap(vars[i], vars[j++]);
if (vars.size() > 0) if (vars.size() > 0)
add_watch(c, vars[0]); add_watch(c, vars[0]);
if (vars.size() > 1) if (vars.size() > 1)