mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-05 19:00:25 +00:00
Code Activity

val_pp

Browse source
This commit is contained in:
Jakob Rath 2022-12-08 15:25:36 +01:00
parent 28fb67219e
commit 85818612fb
2 changed files with 11 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1719,15 +1719,15 @@ namespace dd {
unsigned pow; unsigned pow;
if (val.is_power_of_two(pow) && pow > 10) if (val.is_power_of_two(pow) && pow > 10)
return out << "2^" << pow; return out << "2^" << pow;
else if (val < m.max_value() && (val + 1).is_power_of_two(pow) && pow > 10) { for (int offset : {-1, 1})
if (require_parens) if (val < m.max_value() && (val - offset).is_power_of_two(pow) && pow > 10)
out << "("; return out << lparen() << "2^" << pow << (offset >= 0 ? "+" : "") << offset << rparen();
out << "2^" << pow << "-1"; rational neg_val = mod(-val, m.two_to_N());
if (require_parens) if (neg_val < val) { // keep this condition so we don't suddenly print negative values where we wouldn't otherwise
out << ")"; if (neg_val.is_power_of_two(pow) && pow > 10)
return out; return out << "-2^" << pow;
} else }
return out << m.normalize(val); return out << m.normalize(val);
} }
bool pdd_manager::well_formed() { bool pdd_manager::well_formed() {

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

@ -556,6 +556,8 @@ namespace dd {
pdd_manager const& m; pdd_manager const& m;
rational const& val; rational const& val;
bool require_parens; bool require_parens;
char const* lparen() const { return require_parens ? "(" : ""; }
char const* rparen() const { return require_parens ? ")" : ""; }
public: public:
val_pp(pdd_manager const& m, rational const& val, bool require_parens): m(m), val(val), require_parens(require_parens) {} 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; std::ostream& display(std::ostream& out) const;