From 1de51da67ee0a46d5d93cad2a2b50a4bea60cb42 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Fri, 11 Mar 2022 18:03:39 +0100
Subject: [PATCH] get univariate coefficients

---
 src/math/dd/dd_pdd.cpp | 26 ++++++++++++++++++++++++++
 src/math/dd/dd_pdd.h   |  5 +++++
 src/test/pdd.cpp       | 23 +++++++++++++++++++++++
 3 files changed, 54 insertions(+)

diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp
index ca0f22abf..fb9854c50 100644
--- a/src/math/dd/dd_pdd.cpp
+++ b/src/math/dd/dd_pdd.cpp
@@ -1141,6 +1141,32 @@ namespace dd {
         }
     }
 
+    /** Determine whether p contains at most one variable. */
+    bool pdd_manager::is_univariate(PDD p) {
+        unsigned const lvl = level(p);
+        while (!is_val(p)) {
+            if (!is_val(lo(p)))
+                return false;
+            if (level(p) != lvl)
+                return false;
+            p = hi(p);
+        }
+        return true;
+    }
+
+    /**
+     * Push coefficients of univariate polynomial in order of ascending degree.
+     * Example:     a*x^2 + b*x + c    ==>    [ c, b, a ]
+     */
+    void pdd_manager::get_univariate_coefficients(PDD p, vector<rational>& coeff) {
+        SASSERT(is_univariate(p));
+        while (!is_val(p)) {
+            coeff.push_back(val(lo(p)));
+            p = hi(p);
+        }
+        coeff.push_back(val(p));
+    }
+
     /*
       \brief determine if v occurs as a leaf variable.
      */
diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h
index 421790e7f..51e3813c0 100644
--- a/src/math/dd/dd_pdd.h
+++ b/src/math/dd/dd_pdd.h
@@ -356,6 +356,9 @@ namespace dd {
 
         bool is_monomial(PDD p);
 
+        bool is_univariate(PDD p);
+        void get_univariate_coefficients(PDD p, vector<rational>& coeff);
+
         // create an spoly r if leading monomials of a and b overlap
         bool try_spoly(pdd const& a, pdd const& b, pdd& r);
 
@@ -413,6 +416,8 @@ namespace dd {
         bool is_unary() const { return !is_val() && lo().is_zero() && hi().is_val(); } 
         bool is_binary() const { return m.is_binary(root); }
         bool is_monomial() const { return m.is_monomial(root); }
+        bool is_univariate() const { return m.is_univariate(root); }
+        void get_univariate_coefficients(vector<rational>& coeff) const { m.get_univariate_coefficients(root, coeff); }
         bool is_never_zero() const { return m.is_never_zero(root); }
         bool var_is_leaf(unsigned v) const { return m.var_is_leaf(root, v); }
 
diff --git a/src/test/pdd.cpp b/src/test/pdd.cpp
index 0a5126807..b327e92db 100644
--- a/src/test/pdd.cpp
+++ b/src/test/pdd.cpp
@@ -570,6 +570,28 @@ public :
         }
     }
 
+    static void univariate() {
+        std::cout << "univariate\n";
+        pdd_manager m(4, pdd_manager::mod2N_e, 4);
+
+        unsigned const va = 0;
+        unsigned const vb = 1;
+        pdd const a = m.mk_var(va);
+        pdd const b = m.mk_var(vb);
+
+        pdd p = a*a*b - a*a;
+        SASSERT(!p.is_univariate());
+
+        pdd q = 3*a*a*a + 1*a + 2;
+        SASSERT(q.is_univariate());
+        vector<rational> coeff;
+        q.get_univariate_coefficients(coeff);
+        SASSERT_EQ(coeff.size(), 4);
+        SASSERT_EQ(coeff[0], 2);
+        SASSERT_EQ(coeff[1], 1);
+        SASSERT_EQ(coeff[2], 0);
+        SASSERT_EQ(coeff[3], 3);
+    }
 };
 
 }
@@ -591,4 +613,5 @@ void tst_pdd() {
     dd::test::binary_resolve();
     dd::test::pow();
     dd::test::subst_val();
+    dd::test::univariate();
 }