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

skip unassigned variables when computing level

Browse source
This commit is contained in:
Jakob Rath 2022-01-20 17:46:23 +01:00
parent 0a59387d05
commit 543ad2f205
1 changed files with 3 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -750,7 +750,9 @@ namespace polysat {
void solver::assign_eval(sat::literal lit) { void solver::assign_eval(sat::literal lit) {
unsigned level = 0; unsigned level = 0;
// NOTE: constraint may be evaluated even if some variables are still unassigned (e.g., 0*x doesn't depend on x).
for (auto v : lit2cnstr(lit)->vars()) for (auto v : lit2cnstr(lit)->vars())
if (is_assigned(v))
level = std::max(get_level(v), level); level = std::max(get_level(v), level);
m_bvars.eval(lit, level); m_bvars.eval(lit, level);
m_trail.push_back(trail_instr_t::assign_bool_i); m_trail.push_back(trail_instr_t::assign_bool_i);