LaVaBDD is a C++ template library for Lattice-Valued Binary Decision Diagrams. A formal description of this data structure is described in a paper recently submitted to ATVA 2010. The goal of this implementation is to be as simple as possible and reasonably efficient.
The LaVaBDD library is composed of a single C++ header file : lavabdd.h
The only dependency of the LaVaBDD library is Google's SparseHash. SparseHash is an efficient hash map implementation.
You can download it here : http://code.google.com/p/google-sparsehash/
The first step to use LaVaBDD is to define your own lattice class. This class must follow the lava::Lattice interface defined in the package.
The lava::Lattice class is a class template. To define your lattice class, you must subclass this template as in the following example:
#include <stdexcept> // for logic_error #include <bdd.h> // the BuDDy ROBDD library defines the "bdd" type #include "lavabdd.h" using namespace std; class BDDLattice : public lava::Lattice<bdd> { public: static bool less(const bdd& x, const bdd& y) { return (x & bdd_not(y)) == bddfalse; } static bool equal(const bdd& x, const bdd& y) { return x == y; } static void join(const bdd& x, const bdd& y, bdd& z) { z = x | y; } static void meet(const bdd& x, const bdd& y, bdd& z) { z = x & y; } static void rpc(const bdd& x, const bdd& y, bdd& z) { z = bdd_not(x) | y; } static void drpc(const bdd& x, const bdd& y, bdd& z) { z = y & bdd_not(x); } static void top(bdd& x) { x = bddtrue; } static void bot(bdd& x) { x = bddfalse; } static size_t hash(const bdd& x) { return lava::hash_int(x.id()); } static void print(const bdd& x, ostream& out) { out << x; } static int size(const bdd& x) { return bdd_nodecount(x); } // not implemented here for the sake of brevity static int list_size(const list<bdd>& dds) { throw logic_error("not implemented"); } };
Here is another, simpler example.
#include <algorithm> // for min() and max() #include "lavabdd.h" using namespace std; typedef unsigned char byte; class ByteLattice : public lava::Lattice<byte> { public: static bool less(const byte& x, const byte& y) { x < y; } static bool equal(const byte& x, const byte& y) { return x == y; } static void join(const byte& x, const byte& y, byte& z) { z = max(x, y); } static void meet(const byte& x, const byte& y, byte& z) { z = min(x, y); } static void rpc(const byte& x, const byte& y, byte& z) { z = y; } static void drpc(const byte& x, const byte& y, byte& z) { z = y; } static void top(byte& x) { x = 255; } static void bot(byte& x) { x = 0; } static size_t hash(const byte& x) { return lava::hash_int((int) x); } static void print(const byte& x, ostream& out) { out << x; } static int size(const byte& x) { return 1; } static int list_size(const list<byte>& xs) { return xs.size(); } };
There are three available normal forms for LVBDD defined in the package.
For a full comparison of each, see the paper. Here is a quick bottom line:
Since the LVBDD class template takes two parameters, it is convenient to define your own LVBDD type. This is done simply as follows :
class BDDLattice; // as defined above typedef lava::LVBDD<BDDLattice, lava::SNF_MEET> LVBDD;
Every LVBDD type must be initialized before use. See lava::LVBDD::init.
You can now use your LVBDD type. See lava::LVBDD for a complete reference on the available methods.
A good starting point is lava::LVBDD::terminal and lava::LVBDD::literal.
To help you, here is a short example.
#include <bdd.h> // BuDDy #include "lavabdd.h" using namespace std; class BDDLattice; // as defined above typedef lava::LVBDD<BDDLattice, lava::SNF_MEET> LVBDD; int main() { LVBDD::init(); // initialize the LVBDD type bdd_init(10000, 10000); // initialize the BuDDy library bdd_setvarnum(4); LVBDD p1 = LVBDD::literal(1, true); LVBDD p2 = LVBDD::literal(2, true); LVBDD p3 = LVBDD::literal(3, true); LVBDD c1 = LVBDD::terminal(bdd_ithvar(1)); LVBDD c2 = LVBDD::terminal(bdd_ithvar(2)); LVBDD c3 = LVBDD::terminal(bdd_ithvar(3)); LVBDD dd = (p1 | c1) & (p2 | c2) & (p3 | c3); dd.print_graphviz(); }
Initial version.
1.6.3