add the pdd evaluator and a unit test for it

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

src/math/dd/pdd_eval.h

@@ -0,0 +1,42 @@
+/*++
+Copyright (c) 2019 Microsoft Corporation
+
+Module Name:
+
+    dd_pdd.cpp
+
+Abstract:
+
+    Poly DD package 
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2019-12-23
+    Lev Nachmanson (levnach) 2019-12-23
+
+Revision History:
+
+--*/
+#include "math/dd/dd_pdd.h"
+
+namespace dd {
+// calculates the value of a pdd expression based on the given values of the variables
+class pdd_eval {
+    pdd_manager& m;
+    
+    std::function<rational (unsigned)> m_var2val;
+    
+public:
+    
+    pdd_eval(pdd_manager& m): m(m) {}
+    
+    void operator=(std::function<rational (unsigned)>& i2v) { m_var2val = i2v; }
+
+    rational operator()(pdd const& p) {
+        if (p.is_val()) {
+            return p.val();
+        }
+        return (*this)(p.hi()) * m_var2val(p.var()) + (*this)(p.lo());
+    }
+};
+}

src/test/pdd.cpp

@@ -1,91 +1,92 @@
 #include "math/dd/dd_pdd.h"
+#include "math/dd/pdd_eval.h"
 
 namespace dd {
-    static void test1() {
-        pdd_manager m(3);
-        pdd v0 = m.mk_var(0);
-        pdd v1 = m.mk_var(1);
-        pdd v2 = m.mk_var(2);
-        std::cout << v0 << "\n";
-        std::cout << v1 << "\n";
-        std::cout << v2 << "\n";
-        pdd c1 = v0 * v1 * v2;
-        pdd c2 = v2 * v0 * v1;
-        std::cout << c1 << "\n";
-        SASSERT(c1 == c2);
+static void test1() {
+    pdd_manager m(3);
+    pdd v0 = m.mk_var(0);
+    pdd v1 = m.mk_var(1);
+    pdd v2 = m.mk_var(2);
+    std::cout << v0 << "\n";
+    std::cout << v1 << "\n";
+    std::cout << v2 << "\n";
+    pdd c1 = v0 * v1 * v2;
+    pdd c2 = v2 * v0 * v1;
+    std::cout << c1 << "\n";
+    SASSERT(c1 == c2);
 
-        c1 = v0 + v1 + v2;
-        c2 = v2 + v1 + v0;
-        std::cout << c1 << "\n";
-        SASSERT(c1 == c2);
+    c1 = v0 + v1 + v2;
+    c2 = v2 + v1 + v0;
+    std::cout << c1 << "\n";
+    SASSERT(c1 == c2);
 
-        c1 = (v0+v1) * v2;
-        c2 = (v0*v2) + (v1*v2);
-        std::cout << c1 << "\n";
-        SASSERT(c1 == c2);
-        c1 = (c1 + 3) + 1;
-        c2 = (c2 + 1) + 3;
-        std::cout << c1 << "\n";
-        SASSERT(c1 == c2);
-        c1 = v0 - v1;
-        c2 = v1 - v0;
-        std::cout << c1 << " " << c2 << "\n";
+    c1 = (v0+v1) * v2;
+    c2 = (v0*v2) + (v1*v2);
+    std::cout << c1 << "\n";
+    SASSERT(c1 == c2);
+    c1 = (c1 + 3) + 1;
+    c2 = (c2 + 1) + 3;
+    std::cout << c1 << "\n";
+    SASSERT(c1 == c2);
+    c1 = v0 - v1;
+    c2 = v1 - v0;
+    std::cout << c1 << " " << c2 << "\n";
 
-        c1 = v1*v2;
-        c2 = (v0*v2) + (v2*v2);
-        pdd c3 = m.zero();
-        VERIFY(m.try_spoly(c1, c2, c3));
-        std::cout << c1 << " " << c2 << " spoly: " << c3 << "\n";
+    c1 = v1*v2;
+    c2 = (v0*v2) + (v2*v2);
+    pdd c3 = m.zero();
+    VERIFY(m.try_spoly(c1, c2, c3));
+    std::cout << c1 << " " << c2 << " spoly: " << c3 << "\n";
 
-        c1 = v1*v2;
-        c2 = (v0*v2) + (v1*v1);
-        VERIFY(m.try_spoly(c1, c2, c3));
-        std::cout << c1 << " " << c2 << " spoly: " << c3 << "\n";
+    c1 = v1*v2;
+    c2 = (v0*v2) + (v1*v1);
+    VERIFY(m.try_spoly(c1, c2, c3));
+    std::cout << c1 << " " << c2 << " spoly: " << c3 << "\n";
 
-        c1 = (v0*v1) - (v0*v0);
-        c2 = (v0*v1*(v2 + v0)) + v2;
-        c3 = c2.reduce(c1);
-        std::cout << c1 << " " << c2 << " reduce: " << c3 << "\n";
-    }
+    c1 = (v0*v1) - (v0*v0);
+    c2 = (v0*v1*(v2 + v0)) + v2;
+    c3 = c2.reduce(c1);
+    std::cout << c1 << " " << c2 << " reduce: " << c3 << "\n";
+}
 
-    static void test2() {
-        std::cout << "\ntest2\n";
-        // a(b^2)cd + abc + bcd + bc + cd + 3 reduce by  bc
-        pdd_manager m(4);
-        pdd a = m.mk_var(0);
-        pdd b = m.mk_var(1);
-        pdd c = m.mk_var(2);
-        pdd d = m.mk_var(3);
-        pdd e = (a * b * b * c * d) + (2*a*b*c) + (b*c*d) + (b*c) + (c*d) + 3;
-        std::cout << e << "\n";
-        pdd f = b * c;
-        pdd r_ef = m.reduce(e, f);
-        m.display(std::cout);
-        std::cout << "result of reduce " << e << " by " << f << " is " << r_ef <<  "\n";
-        pdd r_fe = m.reduce(f, e);
-        std::cout << "result of reduce " << f << " by " << e << " is " << r_fe << "\n" ;
-        VERIFY(r_fe == f);
-    }
+static void test2() {
+    std::cout << "\ntest2\n";
+    // a(b^2)cd + abc + bcd + bc + cd + 3 reduce by  bc
+    pdd_manager m(4);
+    pdd a = m.mk_var(0);
+    pdd b = m.mk_var(1);
+    pdd c = m.mk_var(2);
+    pdd d = m.mk_var(3);
+    pdd e = (a * b * b * c * d) + (2*a*b*c) + (b*c*d) + (b*c) + (c*d) + 3;
+    std::cout << e << "\n";
+    pdd f = b * c;
+    pdd r_ef = m.reduce(e, f);
+    m.display(std::cout);
+    std::cout << "result of reduce " << e << " by " << f << " is " << r_ef <<  "\n";
+    pdd r_fe = m.reduce(f, e);
+    std::cout << "result of reduce " << f << " by " << e << " is " << r_fe << "\n" ;
+    VERIFY(r_fe == f);
+}
 
-    static void test3() {
-        std::cout << "\ntest3\n";
-        pdd_manager m(4);
-        pdd a = m.mk_var(0);
-        pdd b = m.mk_var(1);
-        pdd c = m.mk_var(2);
-        pdd d = m.mk_var(3);
+static void test3() {
+    std::cout << "\ntest3\n";
+    pdd_manager m(4);
+    pdd a = m.mk_var(0);
+    pdd b = m.mk_var(1);
+    pdd c = m.mk_var(2);
+    pdd d = m.mk_var(3);
         
-        pdd e = a + c;
-        for (unsigned i = 0; i < 5; i++) {
-            e = e * e;
-        }
-        e = e * b;
-        std::cout << e << "\n";
+    pdd e = a + c;
+    for (unsigned i = 0; i < 5; i++) {
+        e = e * e;
     }
+    e = e * b;
+    std::cout << e << "\n";
+}
 
-    static void test_reset() {
-        std::cout << "\ntest reset\n";
-        pdd_manager m(4);
+static void test_reset() {
+    std::cout << "\ntest reset\n";
+    pdd_manager m(4);
         pdd a = m.mk_var(0);
         pdd b = m.mk_var(1);
         pdd c = m.mk_var(2);