From df0cd3075415cffefa3cfe8b7c0e177cce244de6 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Thu, 21 Dec 2023 14:37:13 +0100 Subject: [PATCH] fix viable propagation reason (part 1) --- src/math/polysat/viable.cpp | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp index 4106679be..7922895a9 100644 --- a/src/math/polysat/viable.cpp +++ b/src/math/polysat/viable.cpp @@ -199,6 +199,8 @@ namespace polysat { } void viable::propagate(pvar v, rational const& val, ptr_vector const& reason) { + LOG_H2("viable::propagate: v" << v << " := " << val); + SASSERT(!s.is_assigned(v)); SASSERT(m_propagation_reasons[v].begin == 0); SASSERT(m_propagation_reasons[v].len == 0); unsigned const begin = m_propagation_reason_storage.size(); @@ -223,8 +225,9 @@ namespace polysat { for (signed_constraint c : e->src) add_reason(c); auto const& i = e->interval; - add_reason(s.eq(i.lo(), i.lo_val())); - add_reason(s.eq(i.hi(), i.hi_val())); + // NOTE: use s.eval(i.lo()) instead of i.lo_val() because when reducing interval bit-width, we adapt the values but not the PDDs + add_reason(s.eq(i.lo(), s.eval(i.lo()))); + add_reason(s.eq(i.hi(), s.eval(i.hi()))); } unsigned const len = m_propagation_reason_storage.size() - begin; @@ -240,11 +243,13 @@ namespace polysat { void viable::pop_propagation_reason() { pvar const v = m_propagation_trail.back(); m_propagation_trail.pop_back(); - unsigned begin = m_propagation_reasons[v].begin; - unsigned len = m_propagation_reasons[v].len; + unsigned const begin = m_propagation_reasons[v].begin; + unsigned const len = m_propagation_reasons[v].len; SASSERT(len > 0); SASSERT(begin + len == m_propagation_reason_storage.size()); m_propagation_reason_storage.shrink(begin); + m_propagation_reasons[v].begin = 0; + m_propagation_reasons[v].len = 0; } bool viable::intersect(pvar v, signed_constraint const& c) {