/Users/nmaquet/Documents/Workspace/lavabdd/src/lavabdd.h

/*
 * lavabdd.h
 *
 *  Created on: 25 janv. 2010
 *      Author: nmaquet
 */

#ifndef __LAVABDD_H__
#define __LAVABDD_H__

#define USING_DENSE_HASH_MAP

#define INITIAL_REFCOUNT 0

#include <list>
#include <stdexcept>
#include <iomanip>
#include <iostream>
#include <fstream>
#include <map>
#include <set>
#include <vector>

#ifdef USING_DENSE_HASH_MAP
#include <google/dense_hash_map>
using google::dense_hash_map;
#else
#include <google/sparse_hash_map>
using google::sparse_hash_map;
#endif

using namespace std;

namespace lava {

const int UNF = 0;

const int SNF_MEET = 1;

const int SNF_JOIN = 2;

/* =====================================================================================*/

inline int hash_int(int key) {
    key = ~key + (key << 15);
    key = key ^ (key >> 12);
    key = key + (key << 2);
    key = key ^ (key >> 4);
    key = key * 2057;
    key = key ^ (key >> 16);
    return key;
}

/* =====================================================================================*/

template<typename V>
class Lattice {

public:

    typedef V ValueType; // This type is propagated as V in Node, NodePtr, and LVBDD.

    static bool less(const V& x, const V& y) {
        throw logic_error("Lattice::less not implemented.");
    }

    static bool equal(const V& x, const V& y) {
        throw logic_error("Lattice::equal not implemented.");
    }

    static void join(const V& x, const V& y, V& z) {
        throw logic_error("Lattice::join not implemented.");
    }

    static void meet(const V& x, const V& y, V& z) {
        throw logic_error("Lattice::meet not implemented.");
    }

    static void rpc(const V& x, const V& y, V& z) {
        throw logic_error("Lattice::rpc not implemented.");
    }

    static void drpc(const V& x, const V& y, V& z) {
        throw logic_error("Lattice::drpc not implemented.");
    }

    static void top(V& x) {
        throw logic_error("Lattice::top not implemented.");
    }

    static void bot(V& x) {
        throw logic_error("Lattice::bot not implemented.");
    }

    static size_t hash(const V& x) {
        throw logic_error("Lattice::hash not implemented.");
    }

    static void print(const V& x, ostream& out) {
        throw logic_error("Lattice::print not implemented.");
    }

    static int size(const V& x) {
        throw logic_error("Lattice::size not implemented.");
    }

    static int list_size(const list<V>& l) {
        throw logic_error("Lattice::list_size not implemented.");
    }

};

/* ==================================================================================== */

template<class L, int F> class LVBDD;

namespace {

template<class L, int F> class Node;

template<class L, int F> class NodePtr {

private:

    typedef typename L::ValueType V;
    typedef lava::Node<L, F> Node;

    Node* _node;

public:

    NodePtr() {
        _node = NULL;
    }

    NodePtr(Node* node) {
        _node = node;
        if (_node)
            _node->_ref();
    }

    ~NodePtr() {
        if (_node)
            _node->_unref();
    }

    NodePtr(const NodePtr& other) {
        _node = other._node;
        if (_node)
            _node->_ref();
    }

    NodePtr& operator=(const NodePtr& other) {
        if (this != &other) {
            if (_node)
                _node->_unref();
            _node = other._node;
            if (_node)
                _node->_ref();
        }
        return *this;
    }

    Node& operator*() const {
        if (_node == NULL)
            throw logic_error("NodePtr : NULL pointer access");
        return *_node;
    }

    Node* operator->() const {
        if (_node == NULL)
            throw logic_error("NodePtr : NULL pointer access");
        return _node;
    }

    Node* get_ptr() const {
        return _node;
    }

    bool operator==(const NodePtr& other) const {
        return _node == other._node;
    }

    bool operator!=(const NodePtr& other) const {
        return _node != other._node;
    }

    bool operator<(const NodePtr& other) const {
        return _node < other._node;
    }

    operator bool() const {
        return _node ? true : false;
    }

    void nullify() {
        if (_node)
            _node->_unref();
        _node = NULL;
    }

    void grab(Node *node) {
        if (_node)
            _node->_unref();
        _node = node;
        if (_node)
            _node->_ref();
    }

};

template<class L, int F> class Node {

private:

    typedef typename L::ValueType V;

    friend class NodePtr<L, F> ;
    typedef lava::NodePtr<L, F> NodePtr;
    typedef lava::LVBDD<L, F> LVBDD;

    mutable int _refcount; /* you can change the RC of const Node references */
    int _index;
    V _value;
    size_t _hash;

    NodePtr _lo;
    NodePtr _hi;

    void _unref() {
        if (_refcount <= 0) {
            throw runtime_error("unref on orphan Node");
        }
        _refcount--;
        if (_refcount == 0) {
            LVBDD::_add_orphan(this);
            _lo.nullify();
            _hi.nullify();
            _index = -1;
        }
    }

    void _ref() {
        _refcount++;
    }

public:

    /*
     *  Default constructor. Do not use.
     */
    Node() {
    }

    Node(int index, const V& val, const NodePtr& lo, const NodePtr& hi) :
        _refcount(INITIAL_REFCOUNT), _index(index), _value(val), _lo(lo), _hi(hi) {
        _hash = L::hash(_value) ^ hash_int(_index);
        if (lo)
            _hash ^= hash_int(((size_t) lo.get_ptr()) * 17);
        if (hi)
            _hash ^= hash_int(((size_t) hi.get_ptr()));
    }

    int index() const {
        return _index;
    }

    size_t hash() const {
        return _hash;
    }

    int refcount() const {
        return _refcount;
    }

    const V& value() const {
        return _value;
    }

    void value(V& value) const {
        value = _value;
    }

    NodePtr lo() const {
        return _lo;
    }

    NodePtr hi() const {
        return _hi;
    }

    bool operator==(const Node& other) const {
        return _hash == other._hash && _index == other._index && _lo == other._lo && _hi
                == other._hi && L::equal(_value, other._value);
    }

    bool operator!=(const Node& other) const {
        return not (*this == other);
    }

    /*
     * Needless to say, be careful with this one ;-)
     */
    void set_refcount(int refcount) {
        _refcount = refcount;
    }

    /*
     *  Do not use. This is used as a hashmap sentinel key.
     */
    static Node deleted_key() {
        Node key;
        key._refcount = -1;
        key._index = -1;
        key._hash = -1;
        return key;
    }

    /*
     * Do not use. This is used as a hashmap sentinel key.
     */
    static Node empty_key() {
        Node key;
        key._refcount = -2;
        key._index = -2;
        key._hash = -2;
        return key;
    }

    static void print_graphviz(ostream& out = cout, NodePtr root = NULL) {
        set<Node*> my_nodes;
        if (not root) {
            typename LVBDD::HashMap::const_iterator it;
            for (it = LVBDD::_hash_map.begin(); it != LVBDD::_hash_map.end(); it++) {
                my_nodes.insert(it->second);
            }
        }
        else {
            root->_descendants(my_nodes);
        }
        typename set<Node*>::iterator it;
        out << "digraph G {" << endl;
        for (it = my_nodes.begin(); it != my_nodes.end(); it++) {
            if ((*it)->index() == 0) {
                out << "\"" << *it << "\" [label=\"";
                L::print((*it)->value(), out);
                if (*it == root.get_ptr())
                    out << " (" << (*it)->refcount() - 1 << ")";
                else
                    out << " (" << (*it)->refcount() << ")";
                out << "\", shape=box];" << endl;
            }
            else {
                out << "\"" << *it << "\" [label=\"" << (*it)->index() << " : ";
                L::print((*it)->value(), out);
                if (*it == root.get_ptr())
                    out << " (" << (*it)->refcount() - 1 << ")";
                else
                    out << " (" << (*it)->refcount() << ")";
                out << "\"];" << endl;
            }
        }
        for (it = my_nodes.begin(); it != my_nodes.end(); it++) {
            if ((*it)->lo()) {
                out << "\"" << *it << "\" -> " << "\"" << ((*it)->lo().get_ptr());
                out << "\" [style=dotted, arrowhead=none];" << endl;
            }
            if ((*it)->lo()) {
                out << "\"" << *it << "\" -> " << "\"" << ((*it)->hi().get_ptr());
                out << "\" [arrowhead=none];" << endl;
            }
        }
        out << "}" << endl;
    }

    void _descendants(set<Node*>& nodes) {
        nodes.clear();
        set<Node*> to_visit;
        typename set<Node*>::iterator it;
        to_visit.insert(this);
        Node* n;
        while (to_visit.size() > 0) {
            it = to_visit.begin();
            n = *it;
            to_visit.erase(it);
            if (nodes.find(n) == nodes.end()) {
                nodes.insert(n);
                if (n->index() > 0) {
                    to_visit.insert(n->lo().get_ptr());
                    to_visit.insert(n->hi().get_ptr());
                }
            }
        }
    }

};

} // namespace (anonymous)

/* ==================================================================================== */

template<class L, int F>
class LVBDD {

private:

    typedef typename L::ValueType V;

    /* ================================================================================ */

    struct NodeHashFunction {
        size_t operator()(Node<L, F>* const & n) const {
            return n->hash();
        }
    };

    struct NodeEqualFunction {
        bool operator()(Node<L, F>* const & n1, Node<L, F>* const & n2) const {
            return (*n1) == (*n2);
        }
    };

    /* ================================================================================ */

    struct Quadruple {
        NodePtr<L, F> n1, n2;
        V d1, d2;
    };

    struct QuadrupleLT {
        bool operator()(const Quadruple& a, const Quadruple& b) const {
            if (a.n1->hash() != b.n1->hash())
                return a.n1->hash() < b.n1->hash();
            if (a.n2->hash() != b.n2->hash())
                return a.n2->hash() < b.n2->hash();
            if (L::hash(a.d1) != L::hash(b.d1))
                return L::hash(a.d1) < L::hash(b.d1);
            if (L::hash(a.d2) != L::hash(b.d2))
                return L::hash(a.d2) < L::hash(b.d2);
            return false;
        }
    };

    /* ================================================================================ */

    class QuadrupleMemoizer {

        typedef lava::Node<L, F> Node;
        typedef lava::NodePtr<L, F> NodePtr;

        typedef map<const Quadruple, NodePtr, QuadrupleLT> MAP;
        MAP _map;

    public:

        NodePtr get(const NodePtr& n1, const NodePtr& n2, const V& d1, const V& d2) const {
            Quadruple q1, q2;
            q1.n1 = n1;
            q2.n1 = n2;
            q1.n2 = n2;
            q2.n2 = n1;
            q1.d1 = d1;
            q2.d1 = d2;
            q1.d2 = d2;
            q2.d2 = d1;
            typename MAP::const_iterator it;
            it = _map.find(q1);
            if (it != _map.end())
                return it->second;
            it = _map.find(q2);
            if (it != _map.end())
                return it->second;
            return NULL;
        }

        void set(const NodePtr& n1, const NodePtr& n2, const V& d1, const V& d2,
                const NodePtr& memo) {
            Quadruple q;
            q.n1 = n1;
            q.n2 = n2;
            q.d1 = d1;
            q.d2 = d2;
            _map[q] = memo;
        }

        void clear() {
            _map.clear();
        }

    };

    /* ================================================================================ */

    class NodeNodeMemoizer {

        typedef lava::Node<L, F> Node;
        typedef lava::NodePtr<L, F> NodePtr;

        map<pair<NodePtr, NodePtr> , NodePtr> _map;

    public:

        NodePtr get(const NodePtr& n1, const NodePtr& n2) const {
            pair<NodePtr, NodePtr> p1(n1, n2);
            pair<NodePtr, NodePtr> p2(n2, n1);
            typename map<pair<NodePtr, NodePtr> , NodePtr>::const_iterator it;
            NodePtr result;
            it = _map.find(p1);
            if (it != _map.end()) {
                result = it->second;
            }
            else {
                it = _map.find(p2);
                if (it != _map.end())
                    result = it->second;
                else
                    result = NULL;
            }
            return result;
        }

        void set(const NodePtr& n1, const NodePtr& n2, const NodePtr& memo) {
            pair<NodePtr, NodePtr> p(n1, n2);
            _map[p] = memo;
        }

        void clear() {
            _map.clear();
        }

    };

    /* ================================================================================ */

    struct NodeValueLT {
        typedef lava::Node<L, F> Node;
        typedef lava::NodePtr<L, F> NodePtr;

        bool operator()(const pair<NodePtr, V>& a, const pair<NodePtr, V>& b) const {
            if (a.first == b.first)
                return L::hash(a.second) < L::hash(b.second);
            else
                return a.first.get_ptr() < b.first.get_ptr();
        }
    };

    /* ================================================================================ */

    class NodeValueMemoizer {

        typedef lava::Node<L, F> Node;
        typedef lava::NodePtr<L, F> NodePtr;
        map<pair<NodePtr, V> , NodePtr, NodeValueLT> _map;

    public:

        NodePtr get(const NodePtr& n, const V& value) const {
            pair<NodePtr, V> p(n, value);
            typename map<pair<NodePtr, V> , NodePtr, NodeValueLT>::const_iterator it;
            it = _map.find(p);
            if (it != _map.end())
                return it->second;
            else
                return NULL;
        }

        void set(const NodePtr& n, const V& value, const NodePtr& memo) {
            pair<NodePtr, V> p(n, value);
            _map[p] = memo;
        }

        void clear() {
            _map.clear();
        }

    };

    friend class Node<L, F> ;

    typedef lava::Node<L, F> Node;
    typedef NodeHashFunction HashNode;
    typedef NodeEqualFunction EqualNode;
    typedef lava::NodePtr<L, F> NodePtr;

#ifdef USING_DENSE_HASH_MAP
    typedef dense_hash_map<Node*, Node*, HashNode, EqualNode> HashMap;
#else
    typedef sparse_hash_map<Node*, Node*, HashNode, EqualNode> HashMap;
#endif

    NodePtr _root;

    static HashMap _hash_map;
    static list<Node*> _orphans;

    static int _mk_call_count;
    static int _orphan_fetches;
    static int _node_allocations;

    static NodeNodeMemoizer _memo_nn;
    static NodeValueMemoizer _memo_nv;
    static QuadrupleMemoizer _memo_quad;

    static NodePtr _unf_apply_rec(const NodePtr& n1, const NodePtr& n2, bool meet) {
        if (not n1 or not n2)
            abort();
        NodePtr result = _memo_nn.get(n1, n2);
        V value;
        L::top(value);
        if (not result) {
            if (n1->index() == 0 and n2->index() == 0) {
                V value = n1->value();
                if (meet)
                    L::meet(value, n2->value(), value);
                else
                    L::join(value, n2->value(), value);
                result = _mk(0, value, NULL, NULL);
            }
            else if (n1->index() == n2->index()) {
                NodePtr lo = _unf_apply_rec(n1->lo(), n2->lo(), meet);
                NodePtr hi = _unf_apply_rec(n1->hi(), n2->hi(), meet);
                if (lo == hi) {
                    result = lo;
                }
                else {
                    result = _mk(n1->index(), value, lo, hi);
                }
            }
            else {
                const NodePtr *new_n1 = &n1, *new_n2 = &n2;
                if (n1->index() < n2->index()) {
                    new_n1 = &n2;
                    new_n2 = &n1;
                }
                NodePtr lo = _unf_apply_rec((*new_n1)->lo(), *new_n2, meet);
                NodePtr hi = _unf_apply_rec((*new_n1)->hi(), *new_n2, meet);
                if (lo == hi) {
                    result = lo;
                }
                else {
                    result = _mk((*new_n1)->index(), value, lo, hi);
                }
            }
            _memo_nn.set(n1, n2, result);
        }
        return result;
    }

    static NodePtr _snf_rpc(const NodePtr& n, const V& d) {
        V value = n->value();
        if (F == SNF_MEET) {
            L::rpc(d, value, value);
        }
        else {
            L::drpc(d, value, value);
        }
        if (n->index() == 0)
            return _mk(0, value, NULL, NULL);
        V x = n->lo()->value();
        if (F == SNF_MEET) {
            L::join(x, n->hi()->value(), x);
            L::meet(value, x, value);
        }
        else {
            L::meet(x, n->hi()->value(), x);
            L::join(value, x, value);
        }
        return _mk(n->index(), value, n->lo(), n->hi());
    }

    static NodePtr _snf_easy_cst(const NodePtr& n, const V& value) {
        NodePtr result = _memo_nv.get(n, value);
        if (result) {
            return result;
        }
        if ((F == SNF_MEET and L::less(n->value(), value)) or (F == SNF_JOIN and L::less(value,
                n->value()))) {
            result = n;
        }
        else {
            V new_value = value;
            if (F == SNF_MEET)
                L::meet(new_value, n->value(), new_value);
            else
                L::join(new_value, n->value(), new_value);
            if (n->index() == 0) {
                result = _mk(0, new_value, NULL, NULL);
            }
            else {
                NodePtr lo, hi, new_lo, new_hi;
                lo = _snf_easy_cst(n->lo(), value);
                hi = _snf_easy_cst(n->hi(), value);
                if (lo == hi) {
                    V label = lo->value();
                    if (F == SNF_MEET)
                        L::meet(label, n->value(), label);
                    else
                        L::join(label, n->value(), label);
                    result = _mk(lo->index(), label, lo->lo(), lo->hi());
                }
                else {
                    new_lo = _snf_rpc(lo, value);
                    new_hi = _snf_rpc(hi, value);
                    if (new_lo == new_hi)
                        abort();
                    result = _mk(n->index(), new_value, new_lo, new_hi);
                }
            }
        }
        _memo_nv.set(n, value, result);
        return result;
    }

    static NodePtr _snf_easy_rec(const NodePtr& n1, const NodePtr& n2) {
        if (not n1 or not n2)
            abort();
        NodePtr result = _memo_nn.get(n1, n2);
        if (result) {
            return result;
        }
        if (n1->index() == 0)
            result = _snf_easy_cst(n2, n1->value());
        else if (n2->index() == 0)
            result = _snf_easy_cst(n1, n2->value());
        else if (n1->index() == n2->index()) {
            NodePtr lo = _snf_easy_rec(n1->lo(), n2->lo());
            NodePtr hi = _snf_easy_rec(n1->hi(), n2->hi());
            V cst_value = n1->value();
            if (F == SNF_MEET)
                L::meet(cst_value, n2->value(), cst_value);
            else
                L::join(cst_value, n2->value(), cst_value);
            NodePtr new_lo = _snf_easy_cst(lo, cst_value);
            NodePtr new_hi = _snf_easy_cst(hi, cst_value);
            if (new_lo == new_hi) {
                result = new_lo;
            }
            else {
                cst_value = new_lo->value();
                if (F == SNF_MEET) {
                    L::join(cst_value, new_hi->value(), cst_value);
                }
                else {
                    L::meet(cst_value, new_hi->value(), cst_value);
                }
                lo = _snf_rpc(new_lo, cst_value);
                hi = _snf_rpc(new_hi, cst_value);
                if (lo == hi) {
                    result = lo;
                }
                else {
                    result = _mk(n1->index(), cst_value, lo, hi);
                }
            }
        }
        else {
            const NodePtr *new_n1 = &n1, *new_n2 = &n2;
            if (n1->index() < n2->index()) {
                new_n1 = &n2;
                new_n2 = &n1;
            }
            NodePtr lo = _snf_easy_rec((*new_n1)->lo(), *new_n2);
            NodePtr hi = _snf_easy_rec((*new_n1)->hi(), *new_n2);
            V cst_value = (*new_n1)->value();
            NodePtr new_lo = _snf_easy_cst(lo, cst_value);
            NodePtr new_hi = _snf_easy_cst(hi, cst_value);
            if (new_lo == new_hi) {
                result = new_lo;
            }
            else {
                cst_value = new_lo->value();
                if (F == SNF_MEET) {
                    L::join(cst_value, new_hi->value(), cst_value);
                }
                else {
                    L::meet(cst_value, new_hi->value(), cst_value);
                }
                lo = _snf_rpc(new_lo, cst_value);
                hi = _snf_rpc(new_hi, cst_value);
                if (lo == hi) {
                    result = lo;
                }
                else {
                    result = _mk((*new_n1)->index(), cst_value, lo, hi);
                }
            }
        }
        _memo_nn.set(n1, n2, result);
        return result;
    }

    static NodePtr _snf_hard_rec(const NodePtr& n1, const NodePtr& n2, const V& d1, const V& d2) {
        NodePtr result = _memo_quad.get(n1, n2, d1, d2);
        if (result) {
            return result;
        }
        V new_d1 = d1, new_d2 = d2;
        if (F == SNF_MEET) {
            L::meet(new_d1, n1->value(), new_d1);
            L::meet(new_d2, n2->value(), new_d2);
        }
        else {
            L::join(new_d1, n1->value(), new_d1);
            L::join(new_d2, n2->value(), new_d2);
        }
        if (n1->index() == 0 and n2->index() == 0) {
            V value = new_d1;
            if (F == SNF_MEET)
                L::join(value, new_d2, value);
            else
                L::meet(value, new_d2, value);
            result = _mk(0, value, NULL, NULL);
            _memo_quad.set(n1, n2, d1, d2, result);
            return result;
        }
        else if (n1->index() == n2->index()) {
            NodePtr lo = _snf_hard_rec(n1->lo(), n2->lo(), new_d1, new_d2);
            NodePtr hi = _snf_hard_rec(n1->hi(), n2->hi(), new_d1, new_d2);
            if (lo == hi) {
                result = lo;
            }
            else {
                V value = lo->value();
                if (F == SNF_MEET) {
                    L::join(value, hi->value(), value);
                }
                else {
                    L::meet(value, hi->value(), value);
                }
                NodePtr new_lo = _snf_rpc(lo, value);
                NodePtr new_hi = _snf_rpc(hi, value);
                result = _mk(n1->index(), value, new_lo, new_hi);
            }
            _memo_quad.set(n1, n2, d1, d2, result);
            return result;
        }
        else {
            const NodePtr *new_n1 = &n1, *new_n2 = &n2;
            bool swapped = false;
            if (n1->index() < n2->index()) {
                new_n1 = &n2;
                new_n2 = &n1;
                swapped = true;
                swap(new_d1, new_d2);
            }
            NodePtr lo = _snf_hard_rec((*new_n1)->lo(), *new_n2, new_d1, new_d2);
            NodePtr hi = _snf_hard_rec((*new_n1)->hi(), *new_n2, new_d1, new_d2);
            if (lo == hi) {
                result = lo;
            }
            else {
                V value = lo->value();
                if (F == SNF_MEET) {
                    L::join(value, hi->value(), value);
                }
                else {
                    L::meet(value, hi->value(), value);
                }
                NodePtr new_lo = _snf_rpc(lo, value);
                NodePtr new_hi = _snf_rpc(hi, value);
                result = _mk((*new_n1)->index(), value, new_lo, new_hi);
            }
            if (swapped)
                _memo_quad.set(n2, n1, d1, d2, result);
            else
                _memo_quad.set(n1, n2, d1, d2, result);
            return result;
        }
    }

    static NodePtr _fetch_orphan() {
        Node* result;
        typename list<Node*>::iterator it;
        for (it = _orphans.begin(); it != _orphans.end();) {
            if ((*it)->refcount() == 0)
                break;
            it = _orphans.erase(it);
        }
        if (it == _orphans.end()) {
            result = NULL;
        }
        else {
            Node* n = *it;
            _orphans.erase(it);
            _hash_map.erase(n);
            result = n;
        }
        return NodePtr(result);
    }

    static NodePtr _mkbot() {
        V v;
        L::bot(v);
        return _mk(0, v, NULL, NULL);
    }

    static NodePtr _mktop() {
        V v;
        L::top(v);
        return _mk(0, v, NULL, NULL);
    }

    static void _add_orphan(Node* n) {
        if (n == NULL or n->refcount() != 0)
            throw runtime_error("invalid orphan node");
        _hash_map.erase(n);
        _orphans.push_back(n);
    }

    static NodePtr _mk(int index, const V& value, const NodePtr& lo, const NodePtr& hi) {

        typename HashMap::const_iterator it;

        _mk_call_count++;

        NodePtr result;
        Node key(index, value, lo, hi);
        it = _hash_map.find(&key);
        if (it == _hash_map.end()) {
            result = _fetch_orphan();
            if (not result) {
                _node_allocations++;
                result.grab(new Node(index, value, lo, hi));
            }
            else {
                if (result->refcount() != 1)
                    abort();
                _orphan_fetches++;
                *result = key;
                result->set_refcount(1);
            }
            _hash_map[result.get_ptr()] = result.get_ptr();
        }
        else {
            result.grab(it->second);
        }

        return result;
    }

    void _quantify_rec(const NodePtr& n, map<NodePtr, V>& memo, V& result, bool exists) const {
        typename map<NodePtr, V>::iterator it;
        it = memo.find(n);
        if (it != memo.end())
            result = it->second;
        else if (n->index() == 0) {
            result = n->value();
            memo[n] = result;
        }
        else {
            V tmp;
            _quantify_rec(n->lo(), memo, tmp, exists);
            _quantify_rec(n->hi(), memo, result, exists);
            if (exists) {
                L::join(result, tmp, result);
            }
            else {
                L::meet(result, tmp, result);
            }
            if (F == SNF_MEET) {
                L::meet(result, n->value(), result);
            }
            else {
                L::join(result, n->value(), result);
            }
            memo[n] = result;
        }
    }

    static void _eval_rec(const vector<bool>& valuation, const NodePtr& node, V& result) {
        if (node->index() == 0) {
            node->value(result);
            return;
        }
        if (node->index() > (int) valuation.size()) {
            throw logic_error("eval : bad valuation");
        }
        NodePtr next = valuation[node->index() - 1] ? node->hi() : node->lo();
        if (F == SNF_JOIN) {
            V tmp;
            _eval_rec(valuation, next, tmp);
            L::join(tmp, node->value(), result);
        }
        else {
            V tmp;
            _eval_rec(valuation, next, tmp);
            L::meet(tmp, node->value(), result);
        }
    }

public:

    LVBDD() {
        _root = _mkbot();
    }

    ~LVBDD() {
        // nothing to do (NodePtr's destructor is called automatically).
    }

    LVBDD(const LVBDD& other) {
        _root = other._root;
    }

    LVBDD& operator=(const LVBDD& other) {
        if (this != &other) {
            _root = other._root;
        }
        return *this;
    }

    bool operator==(const LVBDD& other) const {
        return _root == other._root;
    }

    bool operator!=(const LVBDD& other) const {
        return _root != other._root;
    }

    static LVBDD terminal(const V& value) {
        LVBDD res;
        res._root = _mk(0, value, NULL, NULL);
        return res;
    }

    static LVBDD literal(int index, bool positive) {
        if (index <= 0)
            throw invalid_argument("LVBDD::literal : bad index");
        LVBDD res;
        NodePtr lo = positive ? _mkbot() : _mktop();
        NodePtr hi = positive ? _mktop() : _mkbot();
        V value;
        if (F == SNF_JOIN)
            L::bot(value);
        else
            L::top(value);
        res._root = _mk(index, value, lo, hi);
        return res;
    }

    static LVBDD top() {
        LVBDD result;
        V value;
        L::top(value);
        result._root = _mk(0, value, NULL, NULL);
        return result;
    }

    static LVBDD bot() {
        LVBDD result;
        V value;
        L::bot(value);
        result._root = _mk(0, value, NULL, NULL);
        return result;
    }

    static LVBDD _mk_unsafe(int index, V value, LVBDD lo, LVBDD hi) {
        if (index < 1)
            throw logic_error("LVBDD::_mk_unsafe : bad index");
        if (lo == hi)
            throw logic_error("lo and hi are the same");
        LVBDD result;
        result._root = _mk(index, value, lo._root, hi._root);
        return result;
    }

    static int orphan_count() {
        int count = 0;
        for (typename list<Node*>::iterator it = _orphans.begin(); it != _orphans.end(); it++) {
            if ((*it)->refcount() == 0)
                count++;
        }
        return count;
    }

    static void print_hashmap_debug(ostream& out = cout) {
        out << endl;
        typename HashMap::iterator it;
        for (it = _hash_map.begin(); it != _hash_map.end(); it++) {
            Node* n = (*it).second;
            out << "@" << n << "  index=" << n->index();
            out << "  lo@" << setw(10) << n->lo();
            out << "  hi@" << setw(10) << n->hi();
            out << "  rc=" << n->refcount();
            out << "  value=" << n->value();
            out << "  hash=" << n->hash();
            out << endl;
        }
        print_hashmap_stats();
        out << endl;
    }

    static void print_hashmap_stats(ostream& out = cout) {
        set<size_t, less<size_t> > hashes;
        map<int, int, less<int> > hash_count;
        for (typename HashMap::iterator it = _hash_map.begin(); it != _hash_map.end(); it++) {
            hashes.insert(it->second->hash());
            if (hash_count.find(it->second->hash()) == hash_count.end()) {
                hash_count[it->second->hash()] = 1;
            }
            else {
                hash_count[it->second->hash()] += 1;
            }
        }
        int max = -1;
        int max_hash = -1;
        map<int, int, less<int> >::const_iterator itt;
        for (itt = hash_count.begin(); itt != hash_count.end(); itt++) {
            if (itt->second > max) {
                max = itt->second;
                max_hash = itt->first;
            }
        }
        float lf = float(_hash_map.size()) / _hash_map.bucket_count();
        out << "HashMap size           = " << _hash_map.size() << endl;
        out << "HashMap load factor    = " << lf << endl;
        out << "HashMap bucket count   = " << _hash_map.bucket_count() << endl;
        out << "# of different hashes  = " << hashes.size() << endl;
        out << "Most usage of hash key = " << max << " (" << max_hash << ")";
        out << endl;
        out << "# of calls to MK       = " << _mk_call_count << endl;
        float pct = 100.0 - ((100.0 * (_orphan_fetches + _node_allocations)) / _mk_call_count);
        out << "# of MK cache hits     = " << _mk_call_count - _orphan_fetches - _node_allocations;
        out << " (" << pct << "%)" << endl;
        pct = (100.0 * _orphan_fetches) / _mk_call_count;
        out << "# of orphans reused    = " << _orphan_fetches << " (";
        out << pct << "%)" << endl;
        pct = (100.0 * _node_allocations) / _mk_call_count;
        out << "# of node allocations  = " << _node_allocations << " (";
        out << pct << "%)" << endl;
        out << "# of orphan nodes      = " << orphan_count() << endl;
    }

    static void free_orphaned_nodes() {
        typename list<Node*>::iterator it;
        Node* n;
        for (it = _orphans.begin(); it != _orphans.end(); it++) {
            if ((*it)->refcount())
                continue;
            n = *it;
            delete n;
        }
        _orphans.clear();
    }

    static void clear_memoization_tables() {
        _memo_quad.clear();
        _memo_nn.clear();
        _memo_nv.clear();
    }

    static int memoization_tables_size() {
        return _memo_quad.size() + _memo_nn.size() + _memo_nv.size();
    }

    static size_t total_node_count() {
        return _hash_map.size();
    }

    static size_t node_count() {
        return total_node_count() - orphan_count();
    }

    static void init() {
        Node *dk = new Node();
        *dk = Node::deleted_key();
        _hash_map.set_deleted_key(dk);
#ifdef USING_DENSE_HASH_MAP
        Node *ek = new Node();
        *ek = Node::empty_key();
        _hash_map.set_empty_key(ek);
#endif
    }

    LVBDD join(const LVBDD& other) const {
        LVBDD result;
        if (F == SNF_MEET) {
            V value;
            L::top(value);
            result._root = _snf_hard_rec(_root, other._root, value, value);
        }
        else if (F == SNF_JOIN) {
            result._root = _snf_easy_rec(_root, other._root);
        }
        else { // UNF
            result._root = _unf_apply_rec(_root, other._root, false);
        }
        return result;
    }

    LVBDD operator|(const LVBDD& other) const {
        return join(other);
    }

    LVBDD meet(const LVBDD& other) const {
        LVBDD result;
        if (F == SNF_JOIN) {
            V value;
            L::bot(value);
            result._root = _snf_hard_rec(_root, other._root, value, value);
        }
        else if (F == SNF_MEET) {
            result._root = _snf_easy_rec(_root, other._root);
        }
        else { // UNF
            result._root = _unf_apply_rec(_root, other._root, true);
        }
        return result;
    }

    LVBDD operator&(const LVBDD& other) const {
        return meet(other);
    }

    int size() const {
        set<Node*> my_nodes;
        _root->_descendants(my_nodes);
        return my_nodes.size();
    }

    int nonterminal_size() const {
        set<Node*> my_nodes;
        _root->_descendants(my_nodes);
        typename set<Node*>::iterator it;
        int count = 0;
        for (it = my_nodes.begin(); it != my_nodes.end(); it++) {
            if ((*it)->index() != 0) {
                count++;
            }
        }
        return count;
    }

    int terminal_size() const {
        set<Node*> my_nodes;
        _root->_descendants(my_nodes);
        typename set<Node*>::iterator it;
        int count = 0;
        for (it = my_nodes.begin(); it != my_nodes.end(); it++) {
            if ((*it)->index() == 0) {
                count++;
            }
        }
        return count;
    }

    int values_size() const {
        set<Node*> my_nodes;
        _root->_descendants(my_nodes);
        list<V> l;
        typename set<Node*>::iterator it;
        for (it = my_nodes.begin(); it != my_nodes.end(); it++) {
            V val = (*it)->value();
            l.push_back(val);
        }
        return L::list_size(l);
    }

    void print_graphviz(ostream& out = cout) const {
        Node::print_graphviz(out, _root);
    }

    static void print_graphviz_debug(ostream& out = cout) {
        Node::print_graphviz(out, NULL);
    }

    void exists(V& result) const {
        if (F == SNF_MEET) {
            result = _root->value();
        }
        else {
            map<NodePtr, V> memo;
            _quantify_rec(_root, memo, result, true);
        }
    }

    V exists() const {
        V result;
        exists(result);
        return result;
    }

    void forall(V& result) const {
        if (F == SNF_JOIN) {
            result = _root->value();
        }
        else {
            map<NodePtr, V> memo;
            _quantify_rec(_root, memo, result, false);
        }
    }

    V forall() const {
        V result;
        forall(result);
        return result;
    }

    LVBDD lo() const {
        if (_root->index() == 0)
            throw logic_error("called lo() on terminal LVBDD");
        LVBDD result;
        result._root = _root->lo();
        return result;
    }

    LVBDD hi() const {
        if (_root->index() == 0)
            throw logic_error("called hi() on terminal LVBDD");
        LVBDD result;
        result._root = _root->hi();
        return result;
    }

    int index() const {
        return _root->index();
    }

    void root_value(V& result) const {
        _root->value(result);
    }

    V root_value() const {
        return _root->value();
    }

    void evaluate(const vector<bool>& valuation, V& result) const {
        result = _eval_rec(valuation, _root, result);
    }

    V evaluate(const vector<bool>& valuation) const {
        V result;
        _eval_rec(valuation, _root, result);
        return result;
    }

    friend ostream& operator<<(ostream& out, const LVBDD& dd) {
        out << dd._root.get_ptr();
        return out;
    }

};

template<class L, int F>
typename LVBDD<L, F>::HashMap LVBDD<L, F>::_hash_map;

template<class L, int F>
list<Node<L, F>*> LVBDD<L, F>::_orphans;

template<class L, int F>
int LVBDD<L, F>::_mk_call_count;

template<class L, int F>
int LVBDD<L, F>::_orphan_fetches;

template<class L, int F>
int LVBDD<L, F>::_node_allocations;

template<class L, int F>
typename LVBDD<L, F>::NodeNodeMemoizer LVBDD<L, F>::_memo_nn;

template<class L, int F>
typename LVBDD<L, F>::NodeValueMemoizer LVBDD<L, F>::_memo_nv;

template<class L, int F>
typename LVBDD<L, F>::QuadrupleMemoizer LVBDD<L, F>::_memo_quad;

} // namespace lava


#endif /* __LAVABDD_H__ */

---