/*
* lavabdd.h
*
* Created on: 25 janv. 2010
* Author: nmaquet
*/
/*!
* \mainpage LaVaBDD : Lattice-Valued Binary Decision Diagrams Template Library
* \version 0.2
* \date February 26th, 2010
* \author Nicolas Maquet
* \section intro_sec 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
*
* \section install_sec Installation
*
* 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/
*
* \section howto_sec How to use the library
*
* \htmlonly
*
* 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
*
* \endhtmlonly
*
* \subsection define_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:
*
*
* \code
#include // for logic_error
#include // the BuDDy ROBDD library defines the "bdd" type
#include "lavabdd.h"
using namespace std;
class BDDLattice : lava::Lattice {
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& dds) { throw logic_error("not implemented"); }
};
* \endcode
*
* Here is another, simpler example.
*
* \code
#include // for min() and max()
#include "lavabdd.h"
using namespace std;
typedef unsigned char byte;
class ByteLattice : lava::Lattice {
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& xs) { return xs.size(); }
};
* \endcode
*
* \subsection chose_normal_form Step 2 : Choose an LVBDD normal form
*
* There are three available normal forms for LVBDD defined in the package.
* \li the Unshared Normal Form (lava::UNF)
* \li the \e meet-semantics Shared Normal Form (lava::SNF_MEET)
* \li the \e join-semantics Shared Normal Form (lava::SNF_JOIN)
*
* For a full comparison of each, see the paper. Here is a quick bottom line:
* \li both SNF are potentially exponentially more compact than UNF
* \li the meet and join are both quadratic-time for UNF
* \li the meet for \e meet-semantics SNF is polynomial, join is exponential
* \li the join for \e join-semantics SNF is polynomial, meet is exponential
*
* \subsection define_lvbdd_type 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 :
*
* \code
*
* class BDDLattice; // as defined above
*
* typedef lava::LVBDD LVBDD;
*
* \endcode
*
* \subsection init_LVBDD Step 4 : Initialize your LVBDD type
*
* Every LVBDD type \b must be initialized before use. See lava::LVBDD::init.
*
* \subsection use_LVBDD 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.
*
* To help you, here is a short example.
*
* \code
#include // BuDDy
#include "lavabdd.h"
using namespace std;
class BDDLattice; // as defined above
typedef lava::LVBDD 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();
}
* \endcode
*
* \section sect_changelog Changelog
*
* \subsection version_0_dot_1 Version 0.1 (Released February 23rd 2010)
*
* Initial version.
*
* \subsection version_0_dot_2 Version 0.2 (Released February 26th 2010)
*
* \li Added a changelog to the documentation ;-)
* \li Lots of bugfixes / typos
* \li lava::hash_int is now a global function and not a static member of lava:LVBDD
* \li Added a definition for operator<< for writing LVBDD on output streams
* \li Added a definition for operator< in lava::NodePtr to allow std::set
*/
#ifndef __LAVABDD_H__
#define __LAVABDD_H__
/*!
* \brief Define this to use Google's *dense* hashmap (fast but memory hungry).
* Don't define it if you want to use the *sparse* hashmap (slower but memory-efficient).
*/
#define USING_DENSE_HASH_MAP
/*!
* \brief Initial reference count for LVBDD nodes. Should be zero.
* Increase the value to track reference counting leaks.
*/
#define INITIAL_REFCOUNT 0
#include
#include
#include
#include
#include
#include