Add substitution routine to pdd

For Grobner we want to preserve directions of intervals for finding sign conflicts. This means that it makes sense to have external control over linear solutions.

src/math/dd/dd_pdd.cpp

@@ -1291,6 +1291,27 @@ namespace dd {
         return *this; 
     }
 
+
+    /**
+     * \brief substitute variable v by r.
+     * This base line implementation is simplistic and does not use operator caching.
+     */
+    pdd pdd::subst_pdd(unsigned v, pdd const& r) const {
+        if (is_val())
+            return *this;
+        if (m.m_var2level[var()] < m.m_var2level[v])
+            return *this;
+        pdd l = lo().subst_pdd(v, r);
+        pdd h = hi().subst_pdd(v, r);
+        if (var() == v) 
+            return r*h + l;
+        else if (l == lo() && h == hi())
+            return *this;
+        else
+            return m.mk_var(v)*h + l;
+    }
+
+
     std::ostream& operator<<(std::ostream& out, pdd const& b) { return b.display(out); }
 
     void pdd_iterator::next() {

src/math/dd/dd_pdd.h

@@ -367,6 +367,12 @@ namespace dd {
         pdd subst_val(vector<std::pair<unsigned, rational>> const& s) const { return m.subst_val(*this, s); }
         pdd subst_val(unsigned v, rational const& val) const { return m.subst_val(*this, v, val); }
 
+        
+        /**
+         * \brief substitute variable v by r.
+         */
+        pdd subst_pdd(unsigned v, pdd const& r) const;
+
         std::ostream& display(std::ostream& out) const { return m.display(out, *this); }
         bool operator==(pdd const& other) const { return root == other.root; }
         bool operator!=(pdd const& other) const { return root != other.root; }