Skip to content

Instantly share code, notes, and snippets.

@cocomoff cocomoff/dp_zdd.cpp
Created Aug 12, 2019

Embed
What would you like to do?
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;
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.