From adea39b92e19fe16b2c963167e50f464a3ea61b9 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Thu, 11 Apr 2024 11:12:49 +0200 Subject: [PATCH] dbg output --- src/sat/smt/polysat/assignment.cpp | 2 +- src/sat/smt/polysat/ule_constraint.cpp | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/sat/smt/polysat/assignment.cpp b/src/sat/smt/polysat/assignment.cpp index c1620891a..c67b681de 100644 --- a/src/sat/smt/polysat/assignment.cpp +++ b/src/sat/smt/polysat/assignment.cpp @@ -102,7 +102,7 @@ namespace polysat { std::ostream& assignment::display(std::ostream& out) const { char const* delim = ""; for (auto const& [var, value] : m_pairs) - out << delim << var << " == " << value, delim = " "; + out << delim << "v" << var << " == " << value, delim = " "; return out; } } diff --git a/src/sat/smt/polysat/ule_constraint.cpp b/src/sat/smt/polysat/ule_constraint.cpp index 0d9923836..35dc3f6f4 100644 --- a/src/sat/smt/polysat/ule_constraint.cpp +++ b/src/sat/smt/polysat/ule_constraint.cpp @@ -136,7 +136,7 @@ namespace polysat { } if (rhs.is_val() && !rhs.is_zero() && lhs.offset() == rhs.val()) { - TRACE("bv", tout << "- p + k <= k--> p <= k\n"); + TRACE("bv", tout << "- p + k <= k --> p <= k\n"); lhs = rhs - lhs; } @@ -148,7 +148,7 @@ namespace polysat { } if (lhs.is_val() && rhs.leading_coefficient().get_bit(N - 1) && !rhs.offset().is_zero()) { - TRACE("bv", tout << "k <= -p--> p - 1 <= -k - 1\n"); + TRACE("bv", tout << "k <= -p --> p - 1 <= -k - 1\n"); pdd k = lhs; lhs = -(rhs + 1); rhs = -k - 1;