From f33c933241640396065087a5485aa42240f2e36b Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 11 Jul 2022 12:10:28 -0700
Subject: [PATCH] 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 | 21 +++++++++++++++++++++
 src/math/dd/dd_pdd.h   |  6 ++++++
 2 files changed, 27 insertions(+)

diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp
index 0dbf3c6f9..857665583 100644
--- a/src/math/dd/dd_pdd.cpp
+++ b/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() {
diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h
index 78c447494..13c6c0605 100644
--- a/src/math/dd/dd_pdd.h
+++ b/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; }