# LaVaBDD : Lattice-Valued Binary Decision Diagrams Template Library

Version:
0.2
Date:
February 26th, 2010

## Introduction

LaVaBDD is C++ template library for Lattice-Valued Binary Decision Diagrams. 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

## Installation

The only dependency of the LaVaBDD library is Google's SparseHash. SparseHash is an efficient hash map implementation.

## How to use the library

Lattice-Valued Binary Decision Diagrams (LVBDD for short) encode functions of the form V(p1,...,pn) → L where:
• p1,...,pn is a finite set of propositional variables
• V(p1,...,pn) is the set of valuations over p1,...,pn
• L is a finite distributive lattice
• ### Step 1 : define your lattice class

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 : 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 : 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(); }

};
```

### Step 2 : Choose an LVBDD normal form

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:

• both SNF are potentially exponentially more compact than UNF
• the meet and join are both quadratic-time for UNF
• the meet for meet-semantics SNF is polynomial, join is exponential
• the join for join-semantics SNF is polynomial, meet is exponential

### Step 3 : Define your LVBDD type

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;
```

### Step 4 : Initialize your LVBDD type

Every LVBDD type must be initialized before use. See lava::LVBDD::init.

### Step 5 : You're good to go !

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.

``` #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();
}
```

## Changelog

### Version 0.1 (Released February 23rd 2010)

Initial version.

### Version 0.2 (Released February 26th 2010)

• Added a changelog to the documentation ;-)
• Lots of bugfixes / typos
• lava::hash_int is now a global function and not a static member of lava:LVBDD
• Added a definition for operator<< for writing LVBDD on output streams
• Added a definition for operator< in lava::NodePtr to allow std::set<NodePtr>
Generated on Sat Feb 27 01:22:15 2010 for LaVaBDD by  1.6.3