From adebd2fd9428607e2fc8f06f89391ae9cc916092 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 1 Jan 2024 19:10:11 -0800 Subject: [PATCH] debugging Signed-off-by: Nikolaj Bjorner --- src/sat/smt/polysat/monomials.cpp | 2 +- src/sat/smt/polysat/saturation.cpp | 4 +--- src/sat/smt/polysat/umul_ovfl_constraint.cpp | 4 +++- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/sat/smt/polysat/monomials.cpp b/src/sat/smt/polysat/monomials.cpp index 9e2920a99..a3974e9b1 100644 --- a/src/sat/smt/polysat/monomials.cpp +++ b/src/sat/smt/polysat/monomials.cpp @@ -98,7 +98,7 @@ namespace polysat { return l_false; if (any_of(m_to_refine, [&](auto i) { return non_overflow_monotone(m_monomials[i]); })) return l_false; - if (any_of(m_to_refine, [&](auto i) { return mulp2(m_monomials[i]); })) + if (false && any_of(m_to_refine, [&](auto i) { return mulp2(m_monomials[i]); })) return l_false; return l_undef; diff --git a/src/sat/smt/polysat/saturation.cpp b/src/sat/smt/polysat/saturation.cpp index 66e35728c..0d3c547c3 100644 --- a/src/sat/smt/polysat/saturation.cpp +++ b/src/sat/smt/polysat/saturation.cpp @@ -44,10 +44,8 @@ namespace polysat { } bool saturation::resolve(pvar v, constraint_id id) { - if (c.eval_unfold(id) == l_true) - return false; auto sc = c.get_constraint(id); - if (!sc.vars().contains(v)) + if (!sc.unfold_vars().contains(v)) return false; if (sc.is_ule()) resolve(v, inequality::from_ule(c, id)); diff --git a/src/sat/smt/polysat/umul_ovfl_constraint.cpp b/src/sat/smt/polysat/umul_ovfl_constraint.cpp index e7991952f..f612b2ab4 100644 --- a/src/sat/smt/polysat/umul_ovfl_constraint.cpp +++ b/src/sat/smt/polysat/umul_ovfl_constraint.cpp @@ -69,7 +69,9 @@ namespace polysat { } lbool umul_ovfl_constraint::eval(assignment const& a) const { - return eval(a.apply_to(p()), a.apply_to(q())); + auto r = eval(a.apply_to(p()), a.apply_to(q())); + CTRACE("bv", r != l_undef, tout << "eval: " << *this << " := " << r << "\n";); + return r; } void umul_ovfl_constraint::activate(core& c, bool sign, dependency const& dep) {