mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

Pretty-print powers of two

Browse source
This commit is contained in:
Jakob Rath 2022-11-29 15:49:58 +01:00
parent 630276dbad
commit 5b6e383c88
2 changed files with 35 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

33
src/math/dd/dd_pdd.cpp
View file

@ -1629,26 +1629,26 @@ namespace dd {
std::ostream& pdd_manager::display(std::ostream& out, pdd const& b) { std::ostream& pdd_manager::display(std::ostream& out, pdd const& b) {
auto mons = to_monomials(b); auto mons = to_monomials(b);
bool first = true; bool first = true;
for (auto& m : mons) { for (auto& [a, vs] : mons) {
if (!first) if (!first)
out << " "; out << " ";
if (m.first.is_neg()) if (a.is_neg())
out << "- "; out << "- ";
else if (!first) else if (!first)
out << "+ "; out << "+ ";
first = false; first = false;
rational c = abs(m.first); rational c = abs(a);
m.second.reverse(); vs.reverse();
if (!c.is_one() || m.second.empty()) { if (!c.is_one() || vs.empty()) {
if (m_semantics == mod2N_e) if (m_semantics == mod2N_e)
out << normalize(c); out << val_pp(*this, c, !vs.empty());
else else
out << c; out << c;
if (!m.second.empty()) out << "*"; if (!vs.empty()) out << "*";
} }
unsigned v_prev = UINT_MAX; unsigned v_prev = UINT_MAX;
unsigned pow = 0; unsigned pow = 0;
for (unsigned v : m.second) { for (unsigned v : vs) {
if (v == v_prev) { if (v == v_prev) {
pow++; pow++;
continue; continue;
@ -1672,6 +1672,23 @@ namespace dd {
return out; return out;
} }
std::ostream& val_pp::display(std::ostream& out) const {
if (m.get_semantics() != pdd_manager::mod2N_e)
return out << val;
unsigned pow;
if (val.is_power_of_two(pow) && pow > 10)
return out << "2^" << pow;
else if ((val + 1).is_power_of_two(pow) && pow > 10) {
if (require_parens)
out << "(";
out << "2^" << pow << "-1";
if (require_parens)
out << ")";
return out;
} else
return out << m.normalize(val);
}
bool pdd_manager::well_formed() { bool pdd_manager::well_formed() {
bool ok = true; bool ok = true;
for (unsigned n : m_free_nodes) { for (unsigned n : m_free_nodes) {

10
src/math/dd/dd_pdd.h
View file

@ -550,6 +550,16 @@ namespace dd {
bool operator!=(pdd_iterator const& other) const { return m_nodes != other.m_nodes; } bool operator!=(pdd_iterator const& other) const { return m_nodes != other.m_nodes; }
}; };
class val_pp {
pdd_manager const& m;
rational const& val;
bool require_parens;
public:
val_pp(pdd_manager const& m, rational const& val, bool require_parens): m(m), val(val), require_parens(require_parens) {}
std::ostream& display(std::ostream& out) const;
};
inline std::ostream& operator<<(std::ostream& out, val_pp const& v) { return v.display(out); }
} }