get univariate coefficients

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.
      */

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); }
 

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();
 }