From adc531391645bbd78be3aa55de5e97961f933a69 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Tue, 19 Mar 2024 10:11:06 +0100 Subject: [PATCH] remove debug output --- src/sat/smt/polysat/ule_constraint.cpp | 11 ----------- 1 file changed, 11 deletions(-) diff --git a/src/sat/smt/polysat/ule_constraint.cpp b/src/sat/smt/polysat/ule_constraint.cpp index 410a37dea..0d9923836 100644 --- a/src/sat/smt/polysat/ule_constraint.cpp +++ b/src/sat/smt/polysat/ule_constraint.cpp @@ -82,12 +82,9 @@ namespace polysat { // NOTE: the result should not depend on the initial value of is_positive; // the purpose of is_positive is to allow flipping the sign as part of a rewrite rule. static void simplify_impl(bool& is_positive, pdd& lhs, pdd& rhs) { - SASSERT_EQ(lhs.power_of_2(), rhs.power_of_2()); unsigned const N = lhs.power_of_2(); - // verbose_stream() << "simplify " << lhs << " <= " << rhs << "\n"; - // 0 <= p --> 0 <= 0 if (lhs.is_zero()) { rhs = 0; @@ -235,7 +232,6 @@ namespace polysat { SASSERT(parity < N); // since at least one side is a non-constant if (parity > lhs.offset().parity(N) || parity > rhs.offset().parity(N)) { - verbose_stream() << "lhs = " << lhs << " rhs = " << rhs << " parity = " << parity << "\n"; // 2^k p + a <= 2^k q + b with 0 <= a < 2^k and 0 <= b < 2^k // --> 2^k p <= 2^k q if a <= b // --> 2^k p < 2^k q if a > b @@ -250,14 +246,8 @@ namespace polysat { } // one more round to detect trivial constraints return simplify_impl(is_positive, lhs, rhs); - verbose_stream() << "lhs' = " << lhs << " rhs' = " << rhs << "\n"; } - } // simplify_impl -} - - -namespace polysat { ule_constraint::ule_constraint(pdd const& l, pdd const& r, pdd const& ul, pdd const& ur) : m_lhs(l), m_rhs(r), m_unfold_lhs(ul), m_unfold_rhs(ur) { @@ -403,5 +393,4 @@ namespace polysat { */ } - }