From f18789257e2d042d85a4a44440d9aad88eb61a28 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 12 Apr 2021 10:39:48 -0700
Subject: [PATCH] Print polynomials with power

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/dd/dd_pdd.cpp | 21 +++++++++++++++++----
 1 file changed, 17 insertions(+), 4 deletions(-)

diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp
index fe3eb0b02..05581f7cb 100644
--- a/src/math/dd/dd_pdd.cpp
+++ b/src/math/dd/dd_pdd.cpp
@@ -1350,12 +1350,25 @@ namespace dd {
                 out << c;
                 if (!m.second.empty()) out << "*";
             }
-            bool f = true;
+            unsigned v_prev = UINT_MAX;
+            unsigned pow = 0;
             for (unsigned v : m.second) {
-                if (!f) out << "*";
-                f = false;
-                out << "v" << v;
+                if (v == v_prev) {
+                    pow++;
+                    continue;
+                }
+                if (v_prev != UINT_MAX) {
+                    out << "v" << v_prev;
+                    if (pow > 1)
+                        out << "^" << pow;
+                    out << "*";
+                }
+                pow = 1;
+                v_prev = v;
             }
+            out << "v" << v_prev;
+            if (pow > 1)
+                out << "^" << pow;
         }
         if (first) out << "0";
         return out;