From b019477378d93935f3d39c1cfa65b6b415d1270e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 30 Jun 2021 09:11:42 -0700
Subject: [PATCH] add cofactoring functionality

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/dd/dd_bdd.cpp | 48 ++++++++++++++++++++++++++++++++++++++++++
 src/math/dd/dd_bdd.h   |  6 +++++-
 src/test/bdd.cpp       | 14 ++++++++++++
 3 files changed, 67 insertions(+), 1 deletion(-)

diff --git a/src/math/dd/dd_bdd.cpp b/src/math/dd/dd_bdd.cpp
index bdf23c78a..85e632db7 100644
--- a/src/math/dd/dd_bdd.cpp
+++ b/src/math/dd/dd_bdd.cpp
@@ -145,6 +145,13 @@ namespace dd {
             if (is_true(a)) return mk_not_rec(b);
             if (is_true(b)) return mk_not_rec(a);
             break;
+	case bdd_cofactor_op:
+	    if (a == b) return a;
+	    if (is_const(a)) return a;
+	    if (level(a) == level(b))
+		
+	    SASSERT(!is_const(b));
+	    break;
         default:
             UNREACHABLE();
             break;
@@ -573,7 +580,47 @@ namespace dd {
         e1->m_result = r;
         return r;
     }
+
+    /**
+     * co-factor a using b. 
+     * b must be a variable bdd (it can be generalized to a cube)
+     */
+
+    bdd bdd_manager::mk_cofactor(bdd const& a, bdd const& b) {
+	bool first = true;
+        scoped_push _sp(*this);
+	    SASSERT(!is_const(b) && is_const(lo(b)) && is_const(hi(b)));
+        while (true) {
+            try {
+                return bdd(mk_cofactor_rec(a.root, b.root), this); 
+            }
+            catch (const mem_out &) {
+                if (!first) throw;
+                try_reorder();
+                first = false;
+            }
+        }
+    }
+
+    bdd_manager::BDD bdd_manager::mk_cofactor_rec(BDD a, BDD b) {
+        if (is_const(a)) return a;
+        unsigned la = level(a), lb = level(b);
+        if (la < lb) return a;
+        if (la == lb) return is_true(hi(b)) ? hi(a) : lo(a);
+        op_entry* e1 = pop_entry(a, b, bdd_cofactor_op);
+        op_entry const* e2 = m_op_cache.insert_if_not_there(e1);
+        if (check_result(e1, e2, a, b, bdd_cofactor_op))
+            return e2->m_result;
+        SASSERT(la > lb);
+        push(mk_cofactor_rec(lo(a), b));
+        push(mk_cofactor_rec(hi(a), b));
+        BDD r = make_node(la, read(2), read(1));
+        pop(2);
+        e1->m_result = r;
+        return r;
+    }
     
+
     bdd bdd_manager::mk_ite(bdd const& c, bdd const& t, bdd const& e) {         
         bool first = true;
         scoped_push _sp(*this);
@@ -589,6 +636,7 @@ namespace dd {
         }
     }
 
+
     bdd_manager::BDD bdd_manager::mk_ite_rec(BDD a, BDD b, BDD c) {
         if (is_true(a)) return b;
         if (is_false(a)) return c;
diff --git a/src/math/dd/dd_bdd.h b/src/math/dd/dd_bdd.h
index ae23e6256..acaa6175a 100644
--- a/src/math/dd/dd_bdd.h
+++ b/src/math/dd/dd_bdd.h
@@ -45,7 +45,8 @@ namespace dd {
             bdd_not_op = 5,
             bdd_and_proj_op = 6,
             bdd_or_proj_op = 7,
-            bdd_no_op = 8,
+	    bdd_cofactor_op = 8,
+            bdd_no_op = 9,
         };
 
         struct bdd_node {
@@ -146,6 +147,7 @@ namespace dd {
         BDD mk_not_rec(BDD b);
         BDD mk_ite_rec(BDD a, BDD b, BDD c);
         BDD mk_quant_rec(unsigned lvl, BDD b, bdd_op op);
+	BDD mk_cofactor_rec(BDD a, BDD b);
 
         void push(BDD b);
         void pop(unsigned num_scopes);
@@ -193,6 +195,7 @@ namespace dd {
         bdd mk_and(bdd const& a, bdd const& b);
         bdd mk_or(bdd const& a, bdd const& b);
         bdd mk_xor(bdd const& a, bdd const& b);
+	bdd mk_cofactor(bdd const& a, bdd const& b);
 
         void reserve_var(unsigned v);
         bool well_formed();
@@ -292,6 +295,7 @@ namespace dd {
         bdd operator^(bdd const& other) const { return m->mk_xor(*this, other); }
         bdd operator|=(bdd const& other) { return *this = *this || other; }
         bdd operator&=(bdd const& other) { return *this = *this && other; }
+	bdd cofactor(bdd const& cube) { return m->mk_cofactor(*this, cube); }
         std::ostream& display(std::ostream& out) const { return m->display(out, *this); }
         bool operator==(bdd const& other) const { return root == other.root; }
         bool operator!=(bdd const& other) const { return root != other.root; }
diff --git a/src/test/bdd.cpp b/src/test/bdd.cpp
index d66acc960..c20e2364e 100644
--- a/src/test/bdd.cpp
+++ b/src/test/bdd.cpp
@@ -425,6 +425,19 @@ public:
         SASSERT_EQ(x_dom.find_hint(s358 && (x == rational(4)), rational(5), r), find_t::empty);
     }
 
+    static void test_cofactor() {
+	std::cout << "test_cofactor\n";
+	bdd_manager m(20);
+        bdd v0 = m.mk_var(0);
+        bdd v1 = m.mk_var(1);
+        bdd v2 = m.mk_var(2);
+        bdd c1 = v0 && v1 && v2;
+	SASSERT(c1.cofactor(v0) == (v1 && v2));
+	SASSERT(c1.cofactor(v1) == (v0 && v2));
+	SASSERT(c1.cofactor(v2) == (v0 && v1));
+	SASSERT(c1.cofactor(!v1) == m.mk_false());
+    }
+
 };
 
 }
@@ -446,4 +459,5 @@ void tst_bdd() {
     dd::test_bdd::test_fdd_reorder();
     dd::test_bdd::test_fdd_twovars();
     dd::test_bdd::test_fdd_find_hint();
+    dd::test_bdd::test_cofactor();
 }