dp_zdd.cpp

dp_zdd.cpp

#include <bits/stdc++.h>
#include "cuddObj.hh"

using namespace std;
const string red = "\033[0;31m";
const string green = "\033[0;32m";
const string reset = "\033[0m";

// Global manager
Cudd mgr;

bool isZero(DdNode* n) {
    return n == Cudd_ReadZero(mgr.getManager());
}

bool isOne(DdNode* n) {
    return n == Cudd_ReadOne(mgr.getManager());
}


// BDD
vector<int> buildZDD(DdNode* n, const int maxdepth, int indent = 0) {
    vector<int> ans;

    if (isZero(n)) {
        // ans = {}
    } else if (isOne(n)) {
        // ans = {{}}
        ans.push_back(0);
    } else {
        // ans = ans0 ∪ (ans1 ⊔ sᵢ)
        const int rn = Cudd_NodeReadIndex(n);
        vector<int> setl = buildZDD(Cudd_E(n), maxdepth, indent + 1);
        vector<int> setr = buildZDD(Cudd_T(n), maxdepth, indent + 1);
        for (auto v : setl)
            ans.push_back(v);
        for (auto v : setr)
            ans.push_back(v | (1 <<rn));
    }
    sort(begin(ans), end(ans));
    unique(begin(ans), end(ans));
    ans.erase(unique(begin(ans), end(ans)), end(ans));
    return ans;
}


int main() {
    vector<BDD> X(3);
    for (int i = 0; i < 3; i++)
        X[i] = mgr.bddVar();

    BDD f1 = X[0] & X[1] & X[2];
    BDD f2 = X[0] & !X[1] & X[2];
    BDD f3 = !X[0] & !X[1] & X[2];
    ZDD zf1 = f1.PortToZdd();
    ZDD zf2 = f2.PortToZdd();
    ZDD zf3 = f3.PortToZdd();
    ZDD zf123 = zf1 | zf2 | zf3;

    // ZDD traverse
    cout << red << "Zero: " << Cudd_ReadZero(mgr.getManager()) << reset << endl;
    cout << red << "One : " << Cudd_ReadOne(mgr.getManager()) << reset << endl;
    cout << endl;

    // build parent-child map
    unordered_map<DdNode*, pair<DdNode*, DdNode*>> nodemap;
    queue<DdNode*> q;
    q.push(zf123.getNode());
    while (!q.empty()) {
        DdNode* n = q.front(); q.pop();
        if (nodemap.find(n) != nodemap.end())
            continue;
        if (!isZero(n) && !isOne(n)) {
            DdNode* nl = Cudd_E(n);
            DdNode* nr = Cudd_T(n);
            nodemap[n] = make_pair(nl, nr);
            q.push(nl);
            q.push(nr);
        }
    }

    // build BDD
    // see; https://qiita.com/tsukasa_diary/items/9c897de26d4a7e1fffbf
    const int maxdepth = 3;
    DdNode* root = zf123.getNode();
    vector<int> zddset = buildZDD(root, maxdepth, 0);
    cout << "Z(r)={";
    for (auto v : zddset) {
        cout << "{";
        for (int i = 0; i < maxdepth; i++) {
            if ((v & (1 << i)) == (1 << i))
                cout << i << " ";
        }
        cout << "} ";
    }
    cout << "}" << endl;
}