From 31ffe894806504f619d11976046819e9ec5181db Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 17 Aug 2022 08:24:41 -0700
Subject: [PATCH] normalize more pretty printing

---
 src/math/dd/dd_pdd.cpp      | 6 +++---
 src/math/dd/dd_pdd.h        | 2 ++
 src/math/polysat/interval.h | 3 ++-
 3 files changed, 7 insertions(+), 4 deletions(-)

diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp
index 66113204c..ffc7c1b0d 100644
--- a/src/math/dd/dd_pdd.cpp
+++ b/src/math/dd/dd_pdd.cpp
@@ -1627,9 +1627,9 @@ namespace dd {
             rational c = abs(m.first);
             m.second.reverse();
             if (!c.is_one() || m.second.empty()) {
-                if (m_semantics == mod2N_e && mod(-c, m_mod2N) < c)
-                    out << -mod(-c, m_mod2N);
-                else 
+                if (m_semantics == mod2N_e)
+                    out << normalize(c);
+                else
                     out << c;
                 if (!m.second.empty()) out << "*";
             }
diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h
index f5ed9e790..d225bf2fd 100644
--- a/src/math/dd/dd_pdd.h
+++ b/src/math/dd/dd_pdd.h
@@ -374,6 +374,8 @@ namespace dd {
         unsigned power_of_2() const { return m_power_of_2; }
         rational const& max_value() const { return m_max_value; }
         rational const& two_to_N() const { return m_mod2N; }
+        rational normalize(rational const& n) const { return mod(-n, m_mod2N) < n ? -mod(-n, m_mod2N) : n; }
+
 
         unsigned_vector const& free_vars(pdd const& p);
 
diff --git a/src/math/polysat/interval.h b/src/math/polysat/interval.h
index 4397e147f..952d53a1b 100644
--- a/src/math/polysat/interval.h
+++ b/src/math/polysat/interval.h
@@ -118,10 +118,11 @@ namespace polysat {
     };
 
     inline std::ostream& operator<<(std::ostream& os, eval_interval const& i) {
+        auto& m = i.hi().manager();
         if (i.is_full())
             return os << "full";
         else
-            return os << i.symbolic() << " := [" << i.lo_val() << ";" << i.hi_val() << "[";
+            return os << i.symbolic() << " := [" << m.normalize(i.lo_val()) << ";" << m.normalize(i.hi_val()) << "[";
     }