From f9f61249e1584ed9d7d8540e22877a8fe825c7b5 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Thu, 19 Jan 2023 13:42:33 +0100 Subject: [PATCH] debug output --- src/math/polysat/ule_constraint.cpp | 1 + src/math/polysat/viable.cpp | 60 ++++++++++++++++++++++------- src/math/polysat/viable.h | 6 +-- 3 files changed, 50 insertions(+), 17 deletions(-) diff --git a/src/math/polysat/ule_constraint.cpp b/src/math/polysat/ule_constraint.cpp index f198e289b..5fe9f42ea 100644 --- a/src/math/polysat/ule_constraint.cpp +++ b/src/math/polysat/ule_constraint.cpp @@ -397,6 +397,7 @@ namespace polysat { pdd q = s.subst(rhs()); bool p_ok = p.is_univariate_in(v); bool q_ok = q.is_univariate_in(v); + IF_VERBOSE(10, display(verbose_stream() << ";; ", to_lbool(is_positive), p, q) << "\n"); if (!is_positive && !q_ok) // add p > 0 us.add_ugt(p.get_univariate_coefficients(), rational::zero(), false, dep); if (!is_positive && !p_ok) // add -1 > q <==> q+1 > 0 diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp index a5304e0fc..62458db29 100644 --- a/src/math/polysat/viable.cpp +++ b/src/math/polysat/viable.cpp @@ -883,6 +883,9 @@ namespace { } bool viable::has_max_forbidden(pvar v, signed_constraint const& c, rational& out_lo, rational& out_hi, vector& out_c) { + // verbose_stream() << "has-max-forbidden with c = " << lit_pp(s, c) << "\n"; + // display(verbose_stream(), v, "\n"); + out_c.reset(); entry const* first = m_units[v]; entry const* e = first; @@ -899,6 +902,7 @@ namespace { if (e->src != c) return false; entry const* e0 = e; + // display_one(verbose_stream() << "selected e0 = ", v, e0) << "\n"; do { entry const* n = e->next(); @@ -911,19 +915,24 @@ namespace { break; n = n1; } + // display_one(verbose_stream() << "e is ", v, e) << "\n"; if (e == n) { SASSERT_EQ(e, e0); return false; } if (e == e0) { out_lo = n->interval.lo_val(); - if (!n->interval.lo().is_val()) + if (!n->interval.lo().is_val()) { + // verbose_stream() << "A: " << lit_pp(s, s.eq(n->interval.lo(), out_lo)) << "\n"; out_c.push_back(s.eq(n->interval.lo(), out_lo)); + } } else if (n == e0) { out_hi = e->interval.hi_val(); - if (!e->interval.hi().is_val()) + if (!e->interval.hi().is_val()) { + // verbose_stream() << "B: " << lit_pp(s, s.eq(e->interval.hi(), out_hi)) << "\n"; out_c.push_back(s.eq(e->interval.hi(), out_hi)); + } } else if (!e->interval.is_full()) { auto const& hi = e->interval.hi(); @@ -933,10 +942,14 @@ namespace { auto rhs = next_hi - next_lo; signed_constraint c = s.m_constraints.ult(lhs, rhs); out_c.push_back(c); + // verbose_stream() << "C: " << lhs << " < " << rhs << " -> " << lit_pp(s, c) << "\n"; } if (e != e0) { - for (auto sc : e->side_cond) + for (auto sc : e->side_cond) { + // verbose_stream() << "D: " << lit_pp(s, sc) << "\n"; out_c.push_back(sc); + } + // verbose_stream() << "E: " << lit_pp(s, e->src) << "\n"; out_c.push_back(e->src); } e = n; @@ -1322,33 +1335,52 @@ namespace { } std::ostream& viable::display_one(std::ostream& out, pvar v, entry const* e) const { - if (e->coeff != 1) - out << e->coeff << " * v" << v << " "; - out << e->interval << " " << e->side_cond << " " << e->src << "; "; + auto& m = s.var2pdd(v); + if (e->coeff == -1) { + // p*val + q > r*val + s if e->src.is_positive() + // p*val + q >= r*val + s if e->src.is_negative() + // Note that e->interval is meaningless in this case, + // we just use it to transport the values p,q,r,s + rational const& p = e->interval.lo_val(); + rational const& q_ = e->interval.lo().val(); + rational const& r = e->interval.hi_val(); + rational const& s_ = e->interval.hi().val(); + out << "[ "; + out << val_pp(m, p, true) << "*v" << v << " + " << val_pp(m, q_); + out << (e->src.is_positive() ? " > " : " >= "); + out << val_pp(m, r, true) << "*v" << v << " + " << val_pp(m, s_); + out << " ] "; + } + else if (e->coeff != 1) + out << e->coeff << " * v" << v << " " << e->interval << " "; + else + out << e->interval << " "; + out << e->side_cond << " " << e->src << "; "; return out; } - std::ostream& viable::display_all(std::ostream& out, pvar v, entry const* e) const { + + std::ostream& viable::display_all(std::ostream& out, pvar v, entry const* e, char const* delimiter) const { if (!e) return out; entry const* first = e; do { - display_one(out, v, e); + display_one(out, v, e) << delimiter; e = e->next(); } while (e != first); return out; } - std::ostream& viable::display(std::ostream& out, pvar v) const { - display_all(out, v, m_units[v]); - display_all(out, v, m_equal_lin[v]); - display_all(out, v, m_diseq_lin[v]); + std::ostream& viable::display(std::ostream& out, pvar v, char const* delimiter) const { + display_all(out, v, m_units[v], delimiter); + display_all(out, v, m_equal_lin[v], delimiter); + display_all(out, v, m_diseq_lin[v], delimiter); return out; } - std::ostream& viable::display(std::ostream& out) const { + std::ostream& viable::display(std::ostream& out, char const* delimiter) const { for (pvar v = 0; v < m_units.size(); ++v) - display(out << "v" << v << ": ", v) << "\n"; + display(out << "v" << v << ": ", v, delimiter) << "\n"; return out; } diff --git a/src/math/polysat/viable.h b/src/math/polysat/viable.h index 475df101a..f698bf4a0 100644 --- a/src/math/polysat/viable.h +++ b/src/math/polysat/viable.h @@ -100,7 +100,7 @@ namespace polysat { bool refine_disequal_lin(pvar v, rational const& val); std::ostream& display_one(std::ostream& out, pvar v, entry const* e) const; - std::ostream& display_all(std::ostream& out, pvar v, entry const* e) const; + std::ostream& display_all(std::ostream& out, pvar v, entry const* e, char const* delimiter = "") const; void insert(entry* e, pvar v, ptr_vector& entries, entry_kind k); @@ -236,7 +236,7 @@ namespace polysat { /** Like log(v) but for all variables */ void log(); - std::ostream& display(std::ostream& out) const; + std::ostream& display(std::ostream& out, char const* delimiter = "") const; class iterator { entry* curr = nullptr; @@ -320,7 +320,7 @@ namespace polysat { intervals units(pvar v) { return intervals(*this, v); } - std::ostream& display(std::ostream& out, pvar v) const; + std::ostream& display(std::ostream& out, pvar v, char const* delimiter = "") const; struct var_pp { viable const& v;