pdd::subst_get

src/math/dd/dd_pdd.cpp

@@ -186,6 +186,19 @@ namespace dd {
         return pdd(apply(s.root, v_val.root, pdd_subst_add_op), this);
     }
 
+    bool pdd_manager::subst_get(pdd const& s, unsigned v, rational& out_val) {
+        unsigned level_v = m_var2level[v];
+        PDD p = s.root;
+        while (/* !is_val(p) && */ level(p) > level_v) {
+            SASSERT(is_val(lo(p)));
+            p = hi(p);
+        }
+        if (!is_val(p) && level(p) == level_v) {
+            out_val = val(lo(p));
+            return true;
+        }
+        return false;
+    }
 
     pdd_manager::PDD pdd_manager::apply(PDD arg1, PDD arg2, pdd_op op) {
         bool first = true;

src/math/dd/dd_pdd.h

@@ -10,7 +10,7 @@ Abstract:
     Poly DD package
 
     It is a mild variant of ZDDs. 
-    In PDDs arithmetic is either standard or using mod 2 (over GF2).
+    In PDDs arithmetic is either standard or using mod 2^n.
 
     Non-leaf nodes are of the form x*hi + lo
     where 
@@ -343,6 +343,7 @@ namespace dd {
         pdd subst_val(pdd const& a, unsigned v, rational const& val);
         pdd subst_val(pdd const& a, pdd const& s);
         pdd subst_add(pdd const& s, unsigned v, rational const& val);
+        bool subst_get(pdd const& s, unsigned v, rational& out_val);
         bool resolve(unsigned v, pdd const& p, pdd const& q, pdd& r);
         pdd reduce(unsigned v, pdd const& a, pdd const& b);
         void quot_rem(pdd const& a, pdd const& b, pdd& q, pdd& r);
@@ -459,7 +460,8 @@ namespace dd {
         pdd subst_val0(vector<std::pair<unsigned, rational>> const& s) const { return m.subst_val0(*this, s); }
         pdd subst_val(pdd 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); }
-        pdd subst_add(unsigned var, rational const& val) { return m.subst_add(*this, var, val); }
+        pdd subst_add(unsigned var, rational const& val) const { return m.subst_add(*this, var, val); }
+        bool subst_get(unsigned var, rational& out_val) const { return m.subst_get(*this, var, out_val); }
 
         /**
          * \brief substitute variable v by r.

src/test/pdd.cpp

@@ -571,6 +571,38 @@ public:
         }
     }
 
+    static void subst_get() {
+        std::cout << "subst_get\n";
+        pdd_manager m(4, pdd_manager::mod2N_e, 32);
+
+        unsigned const va = 0;
+        unsigned const vb = 1;
+        unsigned const vc = 2;
+        unsigned const vd = 3;
+
+        rational val;
+        pdd s = m.one();
+        std::cout << s << "\n";
+        VERIFY(!s.subst_get(va, val));
+        VERIFY(!s.subst_get(vb, val));
+        VERIFY(!s.subst_get(vc, val));
+        VERIFY(!s.subst_get(vd, val));
+
+        s = s.subst_add(va, rational(5));
+        std::cout << s << "\n";
+        VERIFY(s.subst_get(va, val) && val == 5);
+        VERIFY(!s.subst_get(vb, val));
+        VERIFY(!s.subst_get(vc, val));
+        VERIFY(!s.subst_get(vd, val));
+
+        s = s.subst_add(vc, rational(7));
+        std::cout << s << "\n";
+        VERIFY(s.subst_get(va, val) && val == 5);
+        VERIFY(!s.subst_get(vb, val));
+        VERIFY(s.subst_get(vc, val) && val == 7);
+        VERIFY(!s.subst_get(vd, val));
+    }
+
     static void univariate() {
         std::cout << "univariate\n";
         pdd_manager m(4, pdd_manager::mod2N_e, 4);
@@ -671,6 +703,7 @@ void tst_pdd() {
     dd::test::binary_resolve();
     dd::test::pow();
     dd::test::subst_val();
+    dd::test::subst_get();
     dd::test::univariate();
     dd::test::factors();
 }