From dade8178e52bd249ffed6044fffcf85f9a041925 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Mon, 6 Nov 2023 15:22:31 +0100 Subject: [PATCH] log solver-value --- src/math/polysat/slicing.cpp | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/src/math/polysat/slicing.cpp b/src/math/polysat/slicing.cpp index 96a4d2e63..a22126616 100644 --- a/src/math/polysat/slicing.cpp +++ b/src/math/polysat/slicing.cpp @@ -739,8 +739,16 @@ namespace polysat { swap(xlit, ylit); } - if (x != null_var) LOG("Variable v" << x << " with slice " << slice_pp(*this, sx) << " by literal " << lit_pp(m_solver, xlit)); - if (y != null_var) LOG("Variable v" << y << " with slice " << slice_pp(*this, sy) << " by literal " << lit_pp(m_solver, ylit)); + if (x != null_var) { + LOG("Variable v" << x << " with slice " << slice_pp(*this, sx) << " by literal " << lit_pp(m_solver, xlit)); + if (m_solver.is_assigned(x)) + LOG("solver-value " << assignment_pp(m_solver, x, m_solver.get_value(x))); + } + if (y != null_var) { + LOG("Variable v" << y << " with slice " << slice_pp(*this, sy) << " by literal " << lit_pp(m_solver, ylit)); + if (m_solver.is_assigned(y)) + LOG("solver-value " << assignment_pp(m_solver, y, m_solver.get_value(y))); + } // conflict has either 0 or 2 vars VERIFY(x != null_var || y == null_var);