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

Replay is needed for evaluated literals

Browse source
This commit is contained in:
Jakob Rath 2023-03-05 07:41:33 +01:00
parent 235c465ae2
commit 1b17fe79f8
1 changed files with 5 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -670,10 +670,12 @@ namespace polysat {
LOG_V(20, "Undo assign_bool_i: " << lit_pp(*this, lit)); LOG_V(20, "Undo assign_bool_i: " << lit_pp(*this, lit));
unsigned active_level = m_bvars.level(lit); unsigned active_level = m_bvars.level(lit);
if (false && active_level <= target_level) { if (active_level <= target_level && m_bvars.is_evaluation(lit)) {
SASSERT(!m_bvars.is_decision(lit)); // Replaying evaluations is fine since all dependencies (variable assignments) are left untouched.
// It is also necessary because repropagate will only restore boolean propagations.
replay.push_back(lit); replay.push_back(lit);
} else { }
else {
clause* reason = m_bvars.reason(lit); clause* reason = m_bvars.reason(lit);
if (reason && reason->size() == 1) { if (reason && reason->size() == 1) {
VERIFY(m_bvars.is_bool_propagation(lit)); VERIFY(m_bvars.is_bool_propagation(lit));