Using CUDD library to manipulate algebraic decision diagrams (ADDs)

add.txt

4 

0 X
1 Y
2 Z
3 W

2

3 X Y Z
8 0.1 0.9 0.1 0.9 0.9 0.1 0.5 0.5

2 Z W
4 0 1 1 0

CUDD-ADD

CC=g++
CCFLAGS=-Wall -Wextra -ansi -pedantic -std=c++11

CUDD=/usr/local/CUDD/cudd-3.0.0

INCLUDE=-I$(CUDD)/cudd -I$(CUDD)/cplusplus
LIBS=$(CUDD)/cudd/.libs/libcudd.a

cudd: main.o
	$(CC) -o $@ $^ $(LIBS)

main.o: main.cpp
	$(CC) $(CCFLAGS) $(INCLUDE) -g -c $<

check: clean cudd
	./cudd add.txt && dot -Tpdf add1.dot -O && open add1.dot.pdf && \
					  dot -Tpdf add2.dot -O && open add2.dot.pdf && \
					  dot -Tpdf add3.dot -O && open add3.dot.pdf && \
					  dot -Tpdf add4.dot -O && open add4.dot.pdf

.PHONY: clean
clean:
	rm -rf cudd *.o *.dot *.dot.pdf

main.cpp

#include <iostream>
#include <fstream>
#include <vector>
#include <unordered_map>
using namespace std;

#include "cuddObj.hh"

static Cudd mgr(0,0);
static void Cudd_init_manager();

void usage(const char *program);
int  input(const char *filename, unordered_map<unsigned,string> &id2var, unordered_map<string,unsigned> &var2id, vector<ADD> &adds);

ADD  build_add(const unordered_map<string,unsigned> &symbols, const vector<string> &domain, const vector<double> &values);
void print_add(const ADD &dd, size_t width);
int  dump_dot(string filename, const ADD &dd, unordered_map<unsigned,string> &id2var);

int
main(int argc, char *argv[])
{
	if (argc < 2) {
		usage(argv[0]);
		return -1;
	}

	Cudd_init_manager();

	unordered_map<string,unsigned> var2id;
	unordered_map<unsigned,string> id2var;
	vector<ADD> adds;
	if (input(argv[1], id2var, var2id, adds)) return -2;

	// input ADDs
	size_t P = adds.size();
	for (size_t i = 1; i <= P; ++i) {
		ADD dd = adds[i-1];
		cout << ">> ADD" << i << endl;
		print_add(dd, 3);
		string filename = "add" + to_string(i);
		dump_dot(filename, dd, id2var);
	}

	// multiplication
	ADD product = adds[0] * adds[1];
	cout << ">> ADD product" << endl;
	print_add(product, 3);
	string filename = "add3";
	dump_dot(filename, product, id2var);

	// summing out variable Z from ADD product
	ADD dd = product;
	int index = var2id["Z"];
	ADD positive = mgr.addVar(index);
	ADD negated  = ~positive;
	ADD summed_out = dd.Restrict(positive) + dd.Restrict(negated);
	cout << ">> ADD Summing Out Z" << endl;
	print_add(summed_out, 3);
	filename = "add4";
	dump_dot(filename, summed_out, id2var);

	return 0;
}

static void Cudd_init_manager()
{
	mgr.AutodynDisable();
}

void
usage(const char *program)
{
	cout << "usage: " << program << " <filename>" << endl;
}

int
input(const char *filename, unordered_map<unsigned,string> &id2var, unordered_map<string,unsigned> &var2id, vector<ADD> &adds)
{
	ifstream input_file(filename, ios::in);

	// read symbols
	size_t nvars;
	input_file >> nvars;
	for (size_t i = 0; i < nvars; ++i) {
		unsigned id;
		string var;
		input_file >> id;
		input_file >> var;
		var2id[var] = id;
		id2var[id] = var;
	}

	// read adds
	size_t nadds;
	input_file >> nadds;

	for (size_t i = 0; i < nadds; ++i) {

		size_t domain_width;
		input_file >> domain_width;

		vector<string> domain;
		for (size_t j = 0; j < domain_width; ++j) {
			string var;
			input_file >> var;
			domain.push_back(var);
		}

		size_t add_size;
		input_file >> add_size;

		vector<double> values;
		for (size_t j = 0; j < add_size; ++j) {
			double val;
			input_file >> val;
			values.push_back(val);
		}

		adds.push_back(build_add(var2id, domain, values));
	}

	input_file.close();

	return 0;
}

ADD
build_add(const unordered_map<string,unsigned> &symbols, const vector<string> &domain, const vector<double> &values)
{
	ADD dd = mgr.addZero();

	size_t add_width = domain.size();
	vector<unsigned> instantiation(add_width, 0);

	size_t add_size = values.size();
	for (size_t pos = 0; pos < add_size; ++pos) {

		double val = values[pos];
		ADD line = mgr.constant(val);

		for (size_t i = 0; i < add_width; ++i) {
			string var = domain[i];
			ADD v = mgr.addVar(symbols.at(var));
			line *= (instantiation[i] ? v : ~v);
		}

		dd += line;

		for (int i = add_width-1; i >= 0; --i) {
			if (instantiation[i] == 0) {
				instantiation[i] = 1;
				break;
			}
			instantiation[i] = 0;
		}
	}

	return dd;
}

void
print_add(const ADD &dd, size_t width)
{
	dd.print(width,3);
}

int
dump_dot(string filename, const ADD &dd, unordered_map<unsigned,string> &id2var) {
	int result;

	const char *fname = (filename + ".dot").c_str();
	FILE *f = fopen(fname, "w");
	if (!f) return -1;

	DdNode *outputs[1];
	outputs[0] = dd.getNode();

	const char *outputNames[1];
	outputNames[0] = filename.c_str();

	size_t N = id2var.size();
	const char **inputNames = new const char*[N];
	for (size_t i = 0; i < N; ++i) {
		inputNames[i] = id2var[i].c_str();
	}

	result = Cudd_DumpDot(mgr.getManager(), 1, outputs, inputNames, outputNames, f);

	delete[] inputNames;
	fclose(f);

	return !result;
}

Download

ftp://vlsi.colorado.edu/pub/cudd-3.0.0.tar.gz

How to install & test

$ ./configure --enable-obj --enable-shared --enable-dddmp
$ make
$ make check

Documentation

• http://vlsi.colorado.edu/~fabio/CUDD/cudd.pdf
• http://vlsi.colorado.edu/~fabio/CUDD/html/

CU Decision Diagram Package (CUDD, unofficial mirror)

• https://github.com/blambeau/cudd

Tutorials (not necessarily up-to-date)

• http://www.di.univr.it/documenti/OccorrenzaIns/matdid/matdid866162.pdf
• https://www.ece.cmu.edu/~ee760/760docs/cuddv1.pdf
• http://www.cs.uleth.ca/~rice/cudd.html
• http://davidkebo.com/cudd