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

debug output

Browse source
This commit is contained in:
Jakob Rath 2023-01-19 13:42:33 +01:00
parent a7ad1f0bfb
commit f9f61249e1
3 changed files with 50 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/math/polysat/ule_constraint.cpp
View file

@ -397,6 +397,7 @@ namespace polysat {
pdd q = s.subst(rhs()); pdd q = s.subst(rhs());
bool p_ok = p.is_univariate_in(v); bool p_ok = p.is_univariate_in(v);
bool q_ok = q.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 if (!is_positive && !q_ok) // add p > 0
us.add_ugt(p.get_univariate_coefficients(), rational::zero(), false, dep); us.add_ugt(p.get_univariate_coefficients(), rational::zero(), false, dep);
if (!is_positive && !p_ok) // add -1 > q <==> q+1 > 0 if (!is_positive && !p_ok) // add -1 > q <==> q+1 > 0

60
src/math/polysat/viable.cpp
View file

@ -883,6 +883,9 @@ namespace {
} }
bool viable::has_max_forbidden(pvar v, signed_constraint const& c, rational& out_lo, rational& out_hi, vector<signed_constraint>& out_c) { bool viable::has_max_forbidden(pvar v, signed_constraint const& c, rational& out_lo, rational& out_hi, vector<signed_constraint>& out_c) {
// verbose_stream() << "has-max-forbidden with c = " << lit_pp(s, c) << "\n";
// display(verbose_stream(), v, "\n");
out_c.reset(); out_c.reset();
entry const* first = m_units[v]; entry const* first = m_units[v];
entry const* e = first; entry const* e = first;
@ -899,6 +902,7 @@ namespace {
if (e->src != c) if (e->src != c)
return false; return false;
entry const* e0 = e; entry const* e0 = e;
// display_one(verbose_stream() << "selected e0 = ", v, e0) << "\n";
do { do {
entry const* n = e->next(); entry const* n = e->next();
@ -911,20 +915,25 @@ namespace {
break; break;
n = n1; n = n1;
} }
// display_one(verbose_stream() << "e is ", v, e) << "\n";
if (e == n) { if (e == n) {
SASSERT_EQ(e, e0); SASSERT_EQ(e, e0);
return false; return false;
} }
if (e == e0) { if (e == e0) {
out_lo = n->interval.lo_val(); 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)); out_c.push_back(s.eq(n->interval.lo(), out_lo));
} }
}
else if (n == e0) { else if (n == e0) {
out_hi = e->interval.hi_val(); 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)); out_c.push_back(s.eq(e->interval.hi(), out_hi));
} }
}
else if (!e->interval.is_full()) { else if (!e->interval.is_full()) {
auto const& hi = e->interval.hi(); auto const& hi = e->interval.hi();
auto const& next_lo = n->interval.lo(); auto const& next_lo = n->interval.lo();
@ -933,10 +942,14 @@ namespace {
auto rhs = next_hi - next_lo; auto rhs = next_hi - next_lo;
signed_constraint c = s.m_constraints.ult(lhs, rhs); signed_constraint c = s.m_constraints.ult(lhs, rhs);
out_c.push_back(c); out_c.push_back(c);
// verbose_stream() << "C: " << lhs << " < " << rhs << " -> " << lit_pp(s, c) << "\n";
} }
if (e != e0) { 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); out_c.push_back(sc);
}
// verbose_stream() << "E: " << lit_pp(s, e->src) << "\n";
out_c.push_back(e->src); out_c.push_back(e->src);
} }
e = n; e = n;
@ -1322,33 +1335,52 @@ namespace {
} }
std::ostream& viable::display_one(std::ostream& out, pvar v, entry const* e) const { std::ostream& viable::display_one(std::ostream& out, pvar v, entry const* e) const {
if (e->coeff != 1) auto& m = s.var2pdd(v);
out << e->coeff << " * v" << v << " "; if (e->coeff == -1) {
out << e->interval << " " << e->side_cond << " " << e->src << "; "; // 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; 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) if (!e)
return out; return out;
entry const* first = e; entry const* first = e;
do { do {
display_one(out, v, e); display_one(out, v, e) << delimiter;
e = e->next(); e = e->next();
} }
while (e != first); while (e != first);
return out; return out;
} }
std::ostream& viable::display(std::ostream& out, pvar v) const { std::ostream& viable::display(std::ostream& out, pvar v, char const* delimiter) const {
display_all(out, v, m_units[v]); display_all(out, v, m_units[v], delimiter);
display_all(out, v, m_equal_lin[v]); display_all(out, v, m_equal_lin[v], delimiter);
display_all(out, v, m_diseq_lin[v]); display_all(out, v, m_diseq_lin[v], delimiter);
return out; 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) for (pvar v = 0; v < m_units.size(); ++v)
display(out << "v" << v << ": ", v) << "\n"; display(out << "v" << v << ": ", v, delimiter) << "\n";
return out; return out;
} }

6
src/math/polysat/viable.h
View file

@ -100,7 +100,7 @@ namespace polysat {
bool refine_disequal_lin(pvar v, rational const& val); 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_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<entry>& entries, entry_kind k); void insert(entry* e, pvar v, ptr_vector<entry>& entries, entry_kind k);
@ -236,7 +236,7 @@ namespace polysat {
/** Like log(v) but for all variables */ /** Like log(v) but for all variables */
void log(); void log();
std::ostream& display(std::ostream& out) const; std::ostream& display(std::ostream& out, char const* delimiter = "") const;
class iterator { class iterator {
entry* curr = nullptr; entry* curr = nullptr;
@ -320,7 +320,7 @@ namespace polysat {
intervals units(pvar v) { return intervals(*this, v); } 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 { struct var_pp {
viable const& v; viable const& v;