From 85818612fbf2681d47c23101e9835ae0638ba4d9 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Thu, 8 Dec 2022 15:25:36 +0100
Subject: [PATCH] val_pp

---
 src/math/dd/dd_pdd.cpp | 18 +++++++++---------
 src/math/dd/dd_pdd.h   |  2 ++
 2 files changed, 11 insertions(+), 9 deletions(-)

diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp
index 3886bbb0f..42d473657 100644
--- a/src/math/dd/dd_pdd.cpp
+++ b/src/math/dd/dd_pdd.cpp
@@ -1719,15 +1719,15 @@ namespace dd {
         unsigned pow;
         if (val.is_power_of_two(pow) && pow > 10)
             return out << "2^" << pow;
-        else if (val < m.max_value() && (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);
+        for (int offset : {-1, 1})
+            if (val < m.max_value() && (val - offset).is_power_of_two(pow) && pow > 10)
+                return out << lparen() << "2^" << pow << (offset >= 0 ? "+" : "") << offset << rparen();
+        rational neg_val = mod(-val, m.two_to_N());
+        if (neg_val < val) {  // keep this condition so we don't suddenly print negative values where we wouldn't otherwise
+            if (neg_val.is_power_of_two(pow) && pow > 10)
+                return out << "-2^" << pow;
+        }
+        return out << m.normalize(val);
     }
 
     bool pdd_manager::well_formed() {
diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h
index 4851626b2..de29ed600 100644
--- a/src/math/dd/dd_pdd.h
+++ b/src/math/dd/dd_pdd.h
@@ -556,6 +556,8 @@ namespace dd {
         pdd_manager const& m;
         rational const& val;
         bool require_parens;
+        char const* lparen() const { return require_parens ? "(" : ""; }
+        char const* rparen() const { return 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;