mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-23 20:58:54 +00:00
Code Activity

dbg output

Browse source
This commit is contained in:
Jakob Rath 2024-04-11 11:12:49 +02:00
parent 020a4d5d04
commit adea39b92e
2 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/sat/smt/polysat/assignment.cpp
View file

@ -102,7 +102,7 @@ namespace polysat {
std::ostream& assignment::display(std::ostream& out) const { std::ostream& assignment::display(std::ostream& out) const {
char const* delim = ""; char const* delim = "";
for (auto const& [var, value] : m_pairs) for (auto const& [var, value] : m_pairs)
out << delim << var << " == " << value, delim = " "; out << delim << "v" << var << " == " << value, delim = " ";
return out; return out;
} }
} }

4
src/sat/smt/polysat/ule_constraint.cpp
View file

@ -136,7 +136,7 @@ namespace polysat {
} }
if (rhs.is_val() && !rhs.is_zero() && lhs.offset() == rhs.val()) { 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; lhs = rhs - lhs;
} }
@ -148,7 +148,7 @@ namespace polysat {
} }
if (lhs.is_val() && rhs.leading_coefficient().get_bit(N - 1) && !rhs.offset().is_zero()) { 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; pdd k = lhs;
lhs = -(rhs + 1); lhs = -(rhs + 1);
rhs = -k - 1; rhs = -k - 1;