00001
00002
00003
00004
00005
00006
00007
00186 #ifndef __LAVABDD_H__
00187 #define __LAVABDD_H__
00188
00193 #define USING_DENSE_HASH_MAP
00194
00199 #define INITIAL_REFCOUNT 0
00200
00201 #include <list>
00202 #include <stdexcept>
00203 #include <iomanip>
00204 #include <iostream>
00205 #include <fstream>
00206 #include <map>
00207 #include <set>
00208 #include <vector>
00209
00210 #ifdef USING_DENSE_HASH_MAP
00211 #include <google/dense_hash_map>
00212 using google::dense_hash_map;
00213 #else
00214 #include <google/sparse_hash_map>
00215 using google::sparse_hash_map;
00216 #endif
00217
00218 using namespace std;
00219
00223 namespace lava {
00224
00228 const int UNF = 0;
00229
00234 const int SNF_MEET = 1;
00235
00240 const int SNF_JOIN = 2;
00241
00242
00243
00247 template<typename V>
00248 class Lattice {
00249
00250 public:
00251
00252 typedef V __V__;
00253
00258 static bool less(const V& x, const V& y) {
00259 throw logic_error("Lattice::less not implemented.");
00260 }
00261
00265 static bool equal(const V& x, const V& y) {
00266 throw logic_error("Lattice::equal not implemented.");
00267 }
00268
00272 static void join(const V& x, const V& y, V& z) {
00273 throw logic_error("Lattice::join not implemented.");
00274 }
00275
00279 static void meet(const V& x, const V& y, V& z) {
00280 throw logic_error("Lattice::meet not implemented.");
00281 }
00282
00287 static void rpc(const V& x, const V& y, V& z) {
00288 throw logic_error("Lattice::rpc not implemented.");
00289 }
00290
00295 static void drpc(const V& x, const V& y, V& z) {
00296 throw logic_error("Lattice::drpc not implemented.");
00297 }
00298
00302 static void top(V& x) {
00303 throw logic_error("Lattice::top not implemented.");
00304 }
00305
00309 static void bot(V& x) {
00310 throw logic_error("Lattice::bot not implemented.");
00311 }
00312
00321 static size_t hash(const V& x) {
00322 throw logic_error("Lattice::hash not implemented.");
00323 }
00324
00328 static void print(const V& x, ostream& out) {
00329 throw logic_error("Lattice::print not implemented.");
00330 }
00331
00337 static int size(const V& x) {
00338 throw logic_error("Lattice::size not implemented.");
00339 }
00340
00347 static int list_size(const list<V>& l) {
00348 throw logic_error("Lattice::list_size not implemented.");
00349 }
00350
00351 };
00352
00353
00354
00355 template<class L, int F> class Node;
00356
00363 template<class L, int F> class NodePtr {
00364
00365 private:
00366
00367 typedef typename L::__V__ V;
00368 typedef Node<L, F> Node;
00369
00370 Node* _node;
00371
00372 public:
00373
00374 NodePtr() {
00375 _node = NULL;
00376 }
00377
00382 NodePtr(Node* node) {
00383 _node = node;
00384 if (_node)
00385 _node->_ref();
00386 }
00387
00391 ~NodePtr() {
00392 if (_node)
00393 _node->_unref();
00394 }
00395
00399 NodePtr(const NodePtr& other) {
00400 _node = other._node;
00401 if (_node)
00402 _node->_ref();
00403 }
00404
00408 NodePtr& operator=(const NodePtr& other) {
00409 if (this != &other) {
00410 if (_node)
00411 _node->_unref();
00412 _node = other._node;
00413 if (_node)
00414 _node->_ref();
00415 }
00416 return *this;
00417 }
00418
00422 Node& operator*() const {
00423 if (_node == NULL)
00424 throw logic_error("NodePtr : NULL pointer access");
00425 return *_node;
00426 }
00427
00431 Node* operator->() const {
00432 if (_node == NULL)
00433 throw logic_error("NodePtr : NULL pointer access");
00434 return _node;
00435 }
00436
00442 Node* get_ptr() const {
00443 return _node;
00444 }
00445
00449 bool operator==(const NodePtr& other) const {
00450 return _node == other._node;
00451 }
00452
00456 bool operator!=(const NodePtr& other) const {
00457 return _node != other._node;
00458 }
00459
00463 operator bool() const {
00464 return _node ? true : false;
00465 }
00466
00470 void nullify() {
00471 if (_node)
00472 _node->_unref();
00473 _node = NULL;
00474 }
00475
00479 void grab(Node *node) {
00480 if (_node)
00481 _node->_unref();
00482 _node = node;
00483 if (_node)
00484 _node->_ref();
00485 }
00486
00487 };
00488
00489 template<class L, int F> class LVBDD;
00490
00497 template<class L, int F> class Node {
00498
00499 private:
00500
00501 typedef typename L::__V__ V;
00502
00503 friend class NodePtr<L, F> ;
00504 typedef NodePtr<L, F> NodePtr;
00505 typedef LVBDD<L, F> LVBDD;
00506
00507 int _refcount;
00508 int _index;
00509 V _value;
00510 size_t _hash;
00511
00512 NodePtr _lo;
00513 NodePtr _hi;
00514
00515 void _unref() {
00516 if (_refcount <= 0) {
00517 throw runtime_error("unref on orphan Node");
00518 }
00519 _refcount--;
00520 if (_refcount == 0) {
00521 LVBDD::_add_orphan(this);
00522 _lo.nullify();
00523 _hi.nullify();
00524 _index = -1;
00525 }
00526 }
00527
00528 void _ref() {
00529 _refcount++;
00530 }
00531
00532 void _descendants(set<Node*>& nodes) {
00533 nodes.clear();
00534 set<Node*> to_visit;
00535 typename set<Node*>::iterator it;
00536 to_visit.insert(this);
00537 Node* n;
00538 while (to_visit.size() > 0) {
00539 it = to_visit.begin();
00540 n = *it;
00541 to_visit.erase(it);
00542 if (nodes.find(n) == nodes.end()) {
00543 nodes.insert(n);
00544 if (n->index() > 0) {
00545 to_visit.insert(n->lo().get_ptr());
00546 to_visit.insert(n->hi().get_ptr());
00547 }
00548 }
00549 }
00550 }
00551
00552 public:
00553
00554
00555
00556
00557 Node() {
00558 }
00559
00572 Node(int index, const V& val, NodePtr lo, NodePtr hi) :
00573 _refcount(INITIAL_REFCOUNT), _index(index), _value(val), _lo(lo), _hi(hi) {
00574 _hash = L::hash(_value) ^ LVBDD::hash_int(_index);
00575 if (lo)
00576 _hash ^= LVBDD::hash_int(((size_t) lo.get_ptr()) * 17);
00577 if (hi)
00578 _hash ^= LVBDD::hash_int(((size_t) hi.get_ptr()));
00579 }
00580
00585 int index() const {
00586 return _index;
00587 }
00588
00593 size_t hash() const {
00594 return _hash;
00595 }
00596
00600 int refcount() const {
00601 return _refcount;
00602 }
00603
00607 const V& value() const {
00608 return _value;
00609 }
00610
00614 NodePtr lo() const {
00615 return _lo;
00616 }
00617
00621 NodePtr hi() const {
00622 return _hi;
00623 }
00624
00625
00626
00627
00628 NodePtr _lo_const_bypass() const {
00629 return _lo;
00630 }
00631
00632
00633
00634
00635 NodePtr _hi_const_bypass() const {
00636 return _hi;
00637 }
00638
00643 bool operator==(const Node& other) const {
00644 return _hash == other._hash && _index == other._index && _lo == other._lo
00645 && _hi == other._hi && L::equal(_value, other._value);
00646 }
00647
00651 bool operator!=(const Node& other) const {
00652 return not (*this == other);
00653 }
00654
00655
00656
00657
00658 void _new_refcount() {
00659 _refcount = 1;
00660 }
00661
00662
00663
00664
00665 static Node deleted_key() {
00666 Node key;
00667 key._refcount = -1;
00668 key._index = -1;
00669 key._hash = -1;
00670 return key;
00671 }
00672
00673
00674
00675
00676 static Node empty_key() {
00677 Node key;
00678 key._refcount = -2;
00679 key._index = -2;
00680 key._hash = -2;
00681 return key;
00682 }
00683
00690 static void print_graphviz(ostream& out = cout, NodePtr root = NULL) {
00691 set<Node*> my_nodes;
00692 if (not root) {
00693 typename LVBDD::HashMap::const_iterator it;
00694 for (it = LVBDD::_hash_map.begin(); it != LVBDD::_hash_map.end(); it++) {
00695 my_nodes.insert(it->second);
00696 }
00697 }
00698 else {
00699 root->_descendants(my_nodes);
00700 }
00701 typename set<Node*>::iterator it;
00702 out << "digraph G {" << endl;
00703 for (it = my_nodes.begin(); it != my_nodes.end(); it++) {
00704 if ((*it)->index() == 0) {
00705 out << "\"" << *it << "\" [label=\"";
00706 L::print((*it)->value(), out);
00707 if (*it == root.get_ptr())
00708 out << " (" << (*it)->refcount() - 1 << ")";
00709 else
00710 out << " (" << (*it)->refcount() << ")";
00711 out << "\", shape=box];" << endl;
00712 }
00713 else {
00714 out << "\"" << *it << "\" [label=\"" << (*it)->index() << " : ";
00715 L::print((*it)->value(), out);
00716 if (*it == root.get_ptr())
00717 out << " (" << (*it)->refcount() - 1 << ")";
00718 else
00719 out << " (" << (*it)->refcount() << ")";
00720 out << "\"];" << endl;
00721 }
00722 }
00723 for (it = my_nodes.begin(); it != my_nodes.end(); it++) {
00724 if ((*it)->lo()) {
00725 out << "\"" << *it << "\" -> " << "\"" << ((*it)->lo());
00726 out << "\" [style=dotted, arrowhead=none];" << endl;
00727 }
00728 if ((*it)->lo()) {
00729 out << "\"" << *it << "\" -> " << "\"" << ((*it)->hi());
00730 out << "\" [arrowhead=none];" << endl;
00731 }
00732 }
00733 out << "}" << endl;
00734 }
00735
00736 };
00737
00738
00739
00746 template<class L, int F>
00747 class LVBDD {
00748
00749 private:
00750
00751 typedef typename L::__V__ V;
00752
00753
00754
00755 struct NodeHashFunction {
00756 size_t operator()(Node<L, F>* const & n) const {
00757 return n->hash();
00758 }
00759 };
00760
00761 struct NodeEqualFunction {
00762 bool operator()(Node<L, F>* const & n1, Node<L, F>* const & n2) const {
00763 return (*n1) == (*n2);
00764 }
00765 };
00766
00767
00768
00769 struct Quadruple {
00770 NodePtr<L, F> n1, n2;
00771 V d1, d2;
00772 };
00773
00774 struct QuadrupleLT {
00775 bool operator()(const Quadruple& a, const Quadruple& b) const {
00776 if (a.n1->hash() != b.n1->hash())
00777 return a.n1->hash() < b.n1->hash();
00778 if (a.n2->hash() != b.n2->hash())
00779 return a.n2->hash() < b.n2->hash();
00780 if (L::hash(a.d1) != L::hash(b.d1))
00781 return L::hash(a.d1) < L::hash(b.d1);
00782 if (L::hash(a.d2) != L::hash(b.d2))
00783 return L::hash(a.d2) < L::hash(b.d2);
00784 return false;
00785 }
00786 };
00787
00788
00789
00790 class QuadrupleMemoizer {
00791
00792 typedef Node<L, F> Node;
00793 typedef NodePtr<L, F> NodePtr;
00794
00795 typedef map<const Quadruple, NodePtr, QuadrupleLT> MAP;
00796 MAP _map;
00797
00798 public:
00799
00800 NodePtr get(NodePtr n1, NodePtr n2, const V& d1, const V& d2) const {
00801 Quadruple q1, q2;
00802 q1.n1 = n1;
00803 q2.n1 = n2;
00804 q1.n2 = n2;
00805 q2.n2 = n1;
00806 q1.d1 = d1;
00807 q2.d1 = d2;
00808 q1.d2 = d2;
00809 q2.d2 = d1;
00810 typename MAP::const_iterator it;
00811 it = _map.find(q1);
00812 if (it != _map.end())
00813 return it->second;
00814 it = _map.find(q2);
00815 if (it != _map.end())
00816 return it->second;
00817 return NULL;
00818 }
00819
00820 void set(NodePtr n1, NodePtr n2, const V& d1, const V& d2, NodePtr memo) {
00821 Quadruple q;
00822 q.n1 = n1;
00823 q.n2 = n2;
00824 q.d1 = d1;
00825 q.d2 = d2;
00826 _map[q] = memo;
00827 }
00828
00829 void clear() {
00830 typename MAP::iterator it;
00831 for (it = _map.begin(); it != _map.end(); it++) {
00832 it->second.nullify();
00833 }
00834 _map.clear();
00835 }
00836
00837 };
00838
00839
00840
00841 class NodeNodeMemoizer {
00842
00843 typedef Node<L, F> Node;
00844 typedef NodePtr<L, F> NodePtr;
00845
00846 map<pair<NodePtr, NodePtr> , NodePtr> _map;
00847
00848 public:
00849
00850 NodePtr get(NodePtr n1, NodePtr n2) const {
00851 pair<NodePtr, NodePtr> p1(n1, n2);
00852 pair<NodePtr, NodePtr> p2(n2, n1);
00853 typename map<pair<NodePtr, NodePtr> , NodePtr>::const_iterator it;
00854 NodePtr result;
00855 it = _map.find(p1);
00856 if (it != _map.end()) {
00857 result = it->second;
00858 }
00859 else {
00860 it = _map.find(p2);
00861 if (it != _map.end())
00862 result = it->second;
00863 else
00864 result = NULL;
00865 }
00866 return result;
00867 }
00868
00869 void set(NodePtr n1, NodePtr n2, NodePtr memo) {
00870 pair<NodePtr, NodePtr> p(n1, n2);
00871 _map[p] = memo;
00872 }
00873
00874 void clear() {
00875 typename map<pair<NodePtr, NodePtr> , NodePtr>::iterator it;
00876 for (it = _map.begin(); it != _map.end(); it++) {
00877 it->second.nullify();
00878 }
00879 _map.clear();
00880 }
00881
00882 };
00883
00884
00885
00886 struct NodeValueLT {
00887 typedef Node<L, F> Node;
00888 typedef NodePtr<L, F> NodePtr;
00889
00890 bool operator()(const pair<NodePtr, V>& a, const pair<NodePtr, V>& b) const {
00891 if (a.first == b.first)
00892 return L::hash(a.second) < L::hash(b.second);
00893 else
00894 return a.first.get_ptr() < b.first.get_ptr();
00895 }
00896 };
00897
00898
00899
00900 class NodeValueMemoizer {
00901
00902 typedef Node<L, F> Node;
00903 typedef NodePtr<L, F> NodePtr;
00904 map<pair<NodePtr, V> , NodePtr, NodeValueLT> _map;
00905
00906 public:
00907
00908 NodePtr get(NodePtr n, const V& value) const {
00909 pair<NodePtr, V> p(n, value);
00910 typename map<pair<NodePtr, V> , NodePtr, NodeValueLT>::const_iterator
00911 it;
00912 it = _map.find(p);
00913 if (it != _map.end())
00914 return it->second;
00915 else
00916 return NULL;
00917 }
00918
00919 void set(NodePtr n, const V& value, NodePtr memo) {
00920 pair<NodePtr, V> p(n, value);
00921 _map[p] = memo;
00922 }
00923
00924 void clear() {
00925 typename map<pair<NodePtr, V> , NodePtr, NodeValueLT>::iterator it;
00926 for (it = _map.begin(); it != _map.end(); it++) {
00927 it->second.nullify();
00928 }
00929 _map.clear();
00930 }
00931
00932 };
00933
00934 friend class Node<L, F> ;
00935
00936 typedef Node<L, F> Node;
00937 typedef NodeHashFunction HashNode;
00938 typedef NodeEqualFunction EqualNode;
00939 typedef NodePtr<L, F> NodePtr;
00940
00941 #ifdef USING_DENSE_HASH_MAP
00942 typedef dense_hash_map<Node*, Node*, HashNode, EqualNode> HashMap;
00943 #else
00944 typedef sparse_hash_map<Node*, Node*, HashNode, EqualNode> HashMap;
00945 #endif
00946
00947 NodePtr _root;
00948
00949 static HashMap _hash_map;
00950 static list<Node*> _orphans;
00951
00952 static int _mk_call_count;
00953 static int _orphan_fetches;
00954 static int _node_allocations;
00955
00956 static NodeNodeMemoizer _memo_nn;
00957 static NodeValueMemoizer _memo_nv;
00958 static QuadrupleMemoizer _memo_quad;
00959
00960 static NodePtr _unf_apply_rec(NodePtr n1, NodePtr n2, bool meet) {
00961 if (not n1 or not n2)
00962 abort();
00963 NodePtr result = _memo_nn.get(n1, n2);
00964 V value;
00965 L::top(value);
00966 if (not result) {
00967 if (n1->index() == 0 and n2->index() == 0) {
00968 V value = n1->value();
00969 if (meet)
00970 L::meet(value, n2->value(), value);
00971 else
00972 L::join(value, n2->value(), value);
00973 result = _mk(0, value, NULL, NULL);
00974 }
00975 else if (n1->index() == n2->index()) {
00976 NodePtr lo = _unf_apply_rec(n1->lo(), n2->lo(), meet);
00977 NodePtr hi = _unf_apply_rec(n1->hi(), n2->hi(), meet);
00978 if (lo == hi) {
00979 result = lo;
00980 }
00981 else {
00982 result = _mk(n1->index(), value, lo, hi);
00983 }
00984 }
00985 else {
00986 if (n1->index() < n2->index())
00987 swap(n1, n2);
00988 NodePtr lo = _unf_apply_rec(n1->lo(), n2, meet);
00989 NodePtr hi = _unf_apply_rec(n1->hi(), n2, meet);
00990 if (lo == hi) {
00991 result = lo;
00992 }
00993 else {
00994 result = _mk(n1->index(), value, lo, hi);
00995 }
00996 }
00997 _memo_nn.set(n1, n2, result);
00998 }
00999 return result;
01000 }
01001
01002 static NodePtr _snf_rpc(NodePtr n, const V& d) {
01003 V value = n->value();
01004 if (F == SNF_MEET) {
01005 if (not L::less(value, d))
01006 throw logic_error("rpc order mismatch");
01007 L::rpc(d, value, value);
01008 }
01009 else {
01010 if (not L::less(d, value))
01011 throw logic_error("drpc order mismatch");
01012 L::drpc(d, value, value);
01013 }
01014 if (n->index() == 0)
01015 return _mk(0, value, NULL, NULL);
01016 V x = n->lo()->value();
01017 if (F == SNF_MEET) {
01018 L::join(x, n->hi()->value(), x);
01019 L::meet(value, x, value);
01020 }
01021 else {
01022 L::meet(x, n->hi()->value(), x);
01023 L::join(value, x, value);
01024 }
01025 return _mk(n->index(), value, n->_lo_const_bypass(), n->_hi_const_bypass());
01026 }
01027
01028 static NodePtr _snf_easy_cst(NodePtr n, const V& value) {
01029 NodePtr result = _memo_nv.get(n, value);
01030 if (result) {
01031 return result;
01032 }
01033 if ((F == SNF_MEET and L::less(n->value(), value)) or (F == SNF_JOIN
01034 and L::less(value, n->value()))) {
01035 NodePtr lo, hi;
01036 lo = n->_lo_const_bypass();
01037 hi = n->_hi_const_bypass();
01038 result = _mk(n->index(), n->value(), lo, hi);
01039 }
01040 else {
01041 V new_value = value;
01042 if (F == SNF_MEET)
01043 L::meet(new_value, n->value(), new_value);
01044 else
01045 L::join(new_value, n->value(), new_value);
01046 if (n->index() == 0) {
01047 result = _mk(0, new_value, NULL, NULL);
01048 }
01049 else {
01050 NodePtr lo, hi, new_lo, new_hi;
01051 lo = _snf_easy_cst(n->lo(), value);
01052 hi = _snf_easy_cst(n->hi(), value);
01053 if (lo == hi) {
01054 V label = lo->value();
01055 if (F == SNF_MEET)
01056 L::meet(label, value, label);
01057 else
01058 L::join(label, value, label);
01059 result = _mk(lo->index(), label, lo->_lo_const_bypass(),
01060 lo->_hi_const_bypass());
01061 }
01062 else {
01063 new_lo = _snf_rpc(lo, value);
01064 new_hi = _snf_rpc(hi, value);
01065 if (new_lo == new_hi)
01066 abort();
01067 result = _mk(n->index(), new_value, new_lo, new_hi);
01068 }
01069 }
01070 }
01071 _memo_nv.set(n, value, result);
01072 return result;
01073 }
01074
01075 static NodePtr _snf_easy_rec(NodePtr n1, NodePtr n2) {
01076 if (not n1 or not n2)
01077 abort();
01078 NodePtr result = _memo_nn.get(n1, n2);
01079 if (result) {
01080 return result;
01081 }
01082 if (n1->index() == 0)
01083 result = _snf_easy_cst(n2, n1->value());
01084 else if (n2->index() == 0)
01085 result = _snf_easy_cst(n1, n2->value());
01086 else if (n1->index() == n2->index()) {
01087 NodePtr lo = _snf_easy_rec(n1->lo(), n2->lo());
01088 NodePtr hi = _snf_easy_rec(n1->hi(), n2->hi());
01089 V cst_value = n1->value();
01090 if (F == SNF_MEET)
01091 L::meet(cst_value, n2->value(), cst_value);
01092 else
01093 L::join(cst_value, n2->value(), cst_value);
01094 NodePtr new_lo = _snf_easy_cst(lo, cst_value);
01095 NodePtr new_hi = _snf_easy_cst(hi, cst_value);
01096 if (new_lo == new_hi) {
01097 result = new_lo;
01098 }
01099 else {
01100 cst_value = new_lo->value();
01101 if (F == SNF_MEET) {
01102 L::join(cst_value, new_hi->value(), cst_value);
01103 L::meet(cst_value, n1->value(), cst_value);
01104 L::meet(cst_value, n2->value(), cst_value);
01105 }
01106 else {
01107 L::meet(cst_value, new_hi->value(), cst_value);
01108 L::join(cst_value, n1->value(), cst_value);
01109 L::join(cst_value, n2->value(), cst_value);
01110 }
01111 lo = _snf_rpc(new_lo, cst_value);
01112 hi = _snf_rpc(new_hi, cst_value);
01113 if (lo == hi) {
01114 result = lo;
01115 }
01116 else {
01117 result = _mk(n1->index(), cst_value, lo, hi);
01118 }
01119 }
01120 }
01121 else {
01122 if (n1->index() < n2->index())
01123 swap(n1, n2);
01124 NodePtr lo = _snf_easy_rec(n1->lo(), n2);
01125 NodePtr hi = _snf_easy_rec(n1->hi(), n2);
01126 V cst_value = n1->value();
01127 NodePtr new_lo = _snf_easy_cst(lo, cst_value);
01128 NodePtr new_hi = _snf_easy_cst(hi, cst_value);
01129 if (new_lo == new_hi) {
01130 result = new_lo;
01131 }
01132 else {
01133 cst_value = new_lo->value();
01134 if (F == SNF_MEET) {
01135 L::join(cst_value, new_hi->value(), cst_value);
01136 L::meet(cst_value, n1->value(), cst_value);
01137 }
01138 else {
01139 L::meet(cst_value, new_hi->value(), cst_value);
01140 L::join(cst_value, n1->value(), cst_value);
01141 }
01142 lo = _snf_rpc(new_lo, cst_value);
01143 hi = _snf_rpc(new_hi, cst_value);
01144 if (lo == hi) {
01145 result = lo;
01146 }
01147 else {
01148 result = _mk(n1->index(), cst_value, lo, hi);
01149 }
01150 }
01151 }
01152 _memo_nn.set(n1, n2, result);
01153 return result;
01154 }
01155
01156 static NodePtr _snf_hard_rec(NodePtr n1, NodePtr n2, const V& d1, const V& d2) {
01157 NodePtr result = _memo_quad.get(n1, n2, d1, d2);
01158 bool swapped = false;
01159 if (result) {
01160 return result;
01161 }
01162 V new_d1 = d1, new_d2 = d2;
01163 if (F == SNF_MEET) {
01164 L::meet(new_d1, n1->value(), new_d1);
01165 L::meet(new_d2, n2->value(), new_d2);
01166 }
01167 else {
01168 L::join(new_d1, n1->value(), new_d1);
01169 L::join(new_d2, n2->value(), new_d2);
01170 }
01171 if (n1->index() == 0 and n2->index() == 0) {
01172 V value = new_d1;
01173 if (F == SNF_MEET)
01174 L::join(value, new_d2, value);
01175 else
01176 L::meet(value, new_d2, value);
01177 result = _mk(0, value, NULL, NULL);
01178 }
01179 else if (n1->index() == n2->index()) {
01180 NodePtr lo = _snf_hard_rec(n1->_lo_const_bypass(),
01181 n2->_lo_const_bypass(), new_d1, new_d2);
01182 NodePtr hi = _snf_hard_rec(n1->_hi_const_bypass(),
01183 n2->_hi_const_bypass(), new_d1, new_d2);
01184 if (lo == hi) {
01185 result = lo;
01186 }
01187 else {
01188 V value = lo->value();
01189 if (F == SNF_MEET) {
01190 L::join(value, hi->value(), value);
01191 }
01192 else {
01193 L::meet(value, hi->value(), value);
01194 }
01195 NodePtr new_lo = _snf_rpc(lo, value);
01196 NodePtr new_hi = _snf_rpc(hi, value);
01197 result = _mk(n1->index(), value, new_lo, new_hi);
01198 }
01199 }
01200 else {
01201 if (n1->index() < n2->index()) {
01202 swap(n1, n2);
01203 swapped = true;
01204 swap(new_d1, new_d2);
01205 }
01206 NodePtr lo = _snf_hard_rec(n1->_lo_const_bypass(), n2, new_d1, new_d2);
01207 NodePtr hi = _snf_hard_rec(n1->_hi_const_bypass(), n2, new_d1, new_d2);
01208 if (lo == hi) {
01209 result = lo;
01210 }
01211 else {
01212 V value = lo->value();
01213 if (F == SNF_MEET) {
01214 L::join(value, hi->value(), value);
01215 }
01216 else {
01217 L::meet(value, hi->value(), value);
01218 }
01219 NodePtr new_lo = _snf_rpc(lo, value);
01220 NodePtr new_hi = _snf_rpc(hi, value);
01221 result = _mk(n1->index(), value, new_lo, new_hi);
01222 }
01223 }
01224 if (swapped)
01225 _memo_quad.set(n2, n1, d1, d2, result);
01226 else
01227 _memo_quad.set(n1, n2, d1, d2, result);
01228 return result;
01229 }
01230
01231 static NodePtr _fetch_orphan() {
01232 Node* result;
01233 typename list<Node*>::iterator it;
01234 for (it = _orphans.begin(); it != _orphans.end();) {
01235 if ((*it)->refcount() == 0)
01236 break;
01237 it = _orphans.erase(it);
01238 }
01239 if (it == _orphans.end()) {
01240 result = NULL;
01241 }
01242 else {
01243 Node* n = *it;
01244 _orphans.erase(it);
01245 _hash_map.erase(n);
01246 result = n;
01247 }
01248 return NodePtr(result);
01249 }
01250
01251 static NodePtr _mkbot() {
01252 V v;
01253 L::bot(v);
01254 return _mk(0, v, NULL, NULL);
01255 }
01256
01257 static NodePtr _mktop() {
01258 V v;
01259 L::top(v);
01260 return _mk(0, v, NULL, NULL);
01261 }
01262
01263 static void _add_orphan(Node* n) {
01264 if (n == NULL or n->refcount() != 0)
01265 throw runtime_error("invalid orphan node");
01266 _orphans.push_back(n);
01267 }
01268
01269 static NodePtr _mk(int index, const V& value, NodePtr lo, NodePtr hi) {
01270
01271 typename HashMap::const_iterator it;
01272
01273 _mk_call_count++;
01274
01275 NodePtr result;
01276 if (lo == hi and lo) {
01277 abort();
01278 }
01279 else {
01280 Node key(index, value, lo, hi);
01281 it = _hash_map.find(&key);
01282 if (it == _hash_map.end()) {
01283 result = _fetch_orphan();
01284 if (not result) {
01285 _node_allocations++;
01286 result.grab(new Node(index, value, lo, hi));
01287 }
01288 else {
01289 if (result->refcount() != 1)
01290 abort();
01291 _orphan_fetches++;
01292 *result = key;
01293 result->_new_refcount();
01294 }
01295 _hash_map[result.get_ptr()] = result.get_ptr();
01296 }
01297 else {
01298 result.grab(it->second);
01299 }
01300 }
01301
01302 return result;
01303 }
01304
01305 void _quantify_rec(NodePtr n, map<NodePtr, V>& memo, V& result, bool exists) const {
01306 typename map<NodePtr, V>::iterator it;
01307 it = memo.find(n);
01308 if (it != memo.end())
01309 result = it->second;
01310 else if (n->index() == 0) {
01311 result = n->value();
01312 memo[n] = result;
01313 }
01314 else {
01315 V tmp;
01316 _quantify_rec(n->lo(), memo, tmp, exists);
01317 _quantify_rec(n->hi(), memo, result, exists);
01318 if (exists) {
01319 L::join(result, tmp, result);
01320 }
01321 else {
01322 L::meet(result, tmp, result);
01323 }
01324 if (F == SNF_MEET) {
01325 L::meet(result, n->value(), result);
01326 }
01327 else {
01328 L::join(result, n->value(), result);
01329 }
01330 memo[n] = result;
01331 }
01332 }
01333
01334 static V _eval_rec(vector<bool> valuation, NodePtr node) {
01335 if (node->index() == 0) {
01336 return node->value();
01337 }
01338 if (node->index() > valuation.size()) {
01339 throw logic_error("eval : bad valuation");
01340 }
01341 NodePtr next = valuation[node->index() - 1] ? node->hi() : node->lo();
01342 V result = node->value();
01343 if (F == SNF_JOIN) {
01344 L::join(result, _eval_rec(valuation, next), result);
01345 }
01346 else {
01347 L::meet(result, _eval_rec(valuation, next), result);
01348 }
01349 return result;
01350 }
01351
01352 public:
01353
01357 LVBDD() {
01358 _root = _mkbot();
01359 }
01360
01364 ~LVBDD() {
01365
01366 }
01367
01371 LVBDD(const LVBDD& other) {
01372 _root = other._root;
01373 }
01374
01378 LVBDD& operator=(const LVBDD& other) {
01379 if (this != &other) {
01380 _root = other._root;
01381 }
01382 return *this;
01383 }
01384
01389 bool operator==(const LVBDD& other) const {
01390 return _root == other._root;
01391 }
01392
01396 bool operator!=(const LVBDD& other) const {
01397 return _root != other._root;
01398 }
01399
01404 static int hash_int(int key) {
01405 key = ~key + (key << 15);
01406 key = key ^ (key >> 12);
01407 key = key + (key << 2);
01408 key = key ^ (key >> 4);
01409 key = key * 2057;
01410 key = key ^ (key >> 16);
01411 return key;
01412 }
01413
01417 static LVBDD terminal(const V& value) {
01418 LVBDD res;
01419 res._root = _mk(0, value, NULL, NULL);
01420 return res;
01421 }
01422
01428 static LVBDD literal(int index, bool positive) {
01429 if (index <= 0)
01430 throw invalid_argument("bad index");
01431 LVBDD res;
01432 NodePtr lo = positive ? _mkbot() : _mktop();
01433 NodePtr hi = positive ? _mktop() : _mkbot();
01434 V value;
01435 if (F == SNF_JOIN)
01436 L::bot(value);
01437 else
01438 L::top(value);
01439 res._root = _mk(index, value, lo, hi);
01440 return res;
01441 }
01442
01446 static LVBDD top() {
01447 LVBDD result;
01448 V value;
01449 L::top(value);
01450 result._root = _mk(0, value, NULL, NULL);
01451 return result;
01452 }
01453
01457 static LVBDD bot() {
01458 LVBDD result;
01459 V value;
01460 L::bot(value);
01461 result._root = _mk(0, value, NULL, NULL);
01462 return result;
01463 }
01464
01475 static LVBDD _mk_unsafe(int index, V value, LVBDD lo, LVBDD hi) {
01476 if (index < 1)
01477 throw logic_error("bad index");
01478 if (lo == hi)
01479 throw logic_error("lo and hi are the same");
01480 LVBDD result;
01481 result._root = _mk(index, value, lo._root, hi._root);
01482 return result;
01483 }
01484
01488 static int orphan_count() {
01489 int count = 0;
01490 for (typename list<Node*>::iterator it = _orphans.begin(); it
01491 != _orphans.end(); it++) {
01492 if ((*it)->refcount() == 0)
01493 count++;
01494 }
01495 return count;
01496 }
01497
01501 static void print_hashmap_debug(ostream& out = cout) {
01502 out << endl;
01503 typename HashMap::iterator it;
01504 for (it = _hash_map.begin(); it != _hash_map.end(); it++) {
01505 Node* n = (*it).second;
01506 out << "@" << n << " index=" << n->index();
01507 out << " lo@" << setw(10) << n->lo();
01508 out << " hi@" << setw(10) << n->hi();
01509 out << " rc=" << n->refcount();
01510 out << " value=" << n->value();
01511 out << " hash=" << n->hash();
01512 out << endl;
01513 }
01514 print_hashmap_stats();
01515 out << endl;
01516 }
01517
01521 static void print_hashmap_stats(ostream& out = cout) {
01522 set<size_t, less<size_t> > hashes;
01523 map<int, int, less<int> > hash_count;
01524 for (typename HashMap::iterator it = _hash_map.begin(); it
01525 != _hash_map.end(); it++) {
01526 hashes.insert(it->second->hash());
01527 if (hash_count.find(it->second->hash()) == hash_count.end()) {
01528 hash_count[it->second->hash()] = 1;
01529 }
01530 else {
01531 hash_count[it->second->hash()] += 1;
01532 }
01533 }
01534 int max = -1;
01535 int max_hash = -1;
01536 map<int, int, less<int> >::const_iterator itt;
01537 for (itt = hash_count.begin(); itt != hash_count.end(); itt++) {
01538 if (itt->second > max) {
01539 max = itt->second;
01540 max_hash = itt->first;
01541 }
01542 }
01543 float lf = float(_hash_map.size()) / _hash_map.bucket_count();
01544 out << "HashMap size = " << _hash_map.size() << endl;
01545 out << "HashMap load factor = " << lf << endl;
01546 out << "HashMap bucket count = " << _hash_map.bucket_count() << endl;
01547 out << "# of different hashes = " << hashes.size() << endl;
01548 out << "Most usage of hash key = " << max << " (" << max_hash << ")";
01549 out << endl;
01550 out << "# of calls to MK = " << _mk_call_count << endl;
01551 float pct = (100.0 * _orphan_fetches) / _mk_call_count;
01552 out << "# of orphans reused = " << _orphan_fetches << " (";
01553 out << pct << "%)" << endl;
01554 pct = (100.0 * _node_allocations) / _mk_call_count;
01555 out << "# of node allocations = " << _node_allocations << " (";
01556 out << pct << "%)" << endl;
01557 out << "# of orphan nodes = " << orphan_count() << endl;
01558 }
01559
01563 static void free_orphaned_nodes() {
01564 typename list<NodePtr>::iterator it;
01565 NodePtr n;
01566 for (it = _orphans.begin(); it != _orphans.end(); it++) {
01567 if ((*it)->refcount())
01568 continue;
01569 n = *it;
01570 _hash_map.erase(*n);
01571 delete n;
01572 }
01573 _orphans.clear();
01574 }
01575
01580 static size_t total_node_count() {
01581 return _hash_map.size();
01582 }
01583
01587 static size_t node_count() {
01588 return total_node_count() - orphan_count();
01589 }
01590
01595 static void init() {
01596 Node *dk = new Node();
01597 *dk = Node::deleted_key();
01598 _hash_map.set_deleted_key(dk);
01599 #ifdef USING_DENSE_HASH_MAP
01600 Node *ek = new Node();
01601 *ek = Node::empty_key();
01602 _hash_map.set_empty_key(ek);
01603 #endif
01604 }
01605
01610 LVBDD join(const LVBDD& other) const {
01611 LVBDD result;
01612 if (F == SNF_MEET) {
01613 V value;
01614 L::top(value);
01615 result._root = _snf_hard_rec(_root, other._root, value, value);
01616 _memo_quad.clear();
01617 }
01618 else if (F == SNF_JOIN) {
01619 result._root = _snf_easy_rec(_root, other._root);
01620 _memo_nv.clear();
01621 _memo_nn.clear();
01622 }
01623 else {
01624 result._root = _unf_apply_rec(_root, other._root, false);
01625 _memo_nn.clear();
01626 }
01627 return result;
01628 }
01629
01633 LVBDD operator|(const LVBDD& other) const {
01634 return join(other);
01635 }
01636
01641 LVBDD meet(const LVBDD& other) const {
01642 LVBDD result;
01643 if (F == SNF_JOIN) {
01644 V value;
01645 L::bot(value);
01646 result._root = _snf_hard_rec(_root, other._root, value, value);
01647 _memo_quad.clear();
01648 }
01649 else if (F == SNF_MEET) {
01650 result._root = _snf_easy_rec(_root, other._root);
01651 _memo_nv.clear();
01652 _memo_nn.clear();
01653 }
01654 else {
01655 result._root = _unf_apply_rec(_root, other._root, true);
01656 _memo_nn.clear();
01657 }
01658 return result;
01659 }
01660
01664 LVBDD operator&(const LVBDD& other) const {
01665 return meet(other);
01666 }
01667
01671 int size() const {
01672 set<Node*> my_nodes;
01673 _root->descendants(my_nodes);
01674 return my_nodes.size();
01675 }
01676
01680 int nonterminal_size() const {
01681 set<Node*> my_nodes;
01682 _root->descendants(my_nodes);
01683 typename set<Node*>::iterator it;
01684 int count = 0;
01685 for (it = my_nodes.begin(); it != my_nodes.end(); it++) {
01686 if ((*it)->index() != 0) {
01687 count++;
01688 }
01689 }
01690 return count;
01691 }
01692
01696 int terminal_size() const {
01697 set<Node*> my_nodes;
01698 _root->descendants(my_nodes);
01699 typename set<Node*>::iterator it;
01700 int count = 0;
01701 for (it = my_nodes.begin(); it != my_nodes.end(); it++) {
01702 if ((*it)->index() == 0) {
01703 count++;
01704 }
01705 }
01706 return count;
01707 }
01708
01713 int values_size() const {
01714 set<Node*> my_nodes;
01715 _root->descendants(my_nodes);
01716 list<V> l;
01717 typename set<Node*>::iterator it;
01718 for (it = my_nodes.begin(); it != my_nodes.end(); it++) {
01719 V val = (*it)->value();
01720 l.push_back(val);
01721 }
01722 return L::list_size(l);
01723 }
01724
01728 void print_graphviz(ostream& out = cout) const {
01729 Node::print_graphviz(out, _root);
01730 }
01731
01735 static void print_graphviz_debug(ostream& out = cout) {
01736 Node::print_graphviz(out, NULL);
01737 }
01738
01742 void exists(V& result) const {
01743 if (F == SNF_MEET) {
01744 result = _root->value();
01745 }
01746 else {
01747 map<NodePtr, V> memo;
01748 _quantify_rec(_root, memo, result, true);
01749 }
01750 }
01751
01755 void forall(V& result) const {
01756 if (F == SNF_JOIN) {
01757 result = _root->value;
01758 }
01759 else {
01760 map<NodePtr, V> memo;
01761 _quantify_rec(_root, memo, result, false);
01762 }
01763 }
01764
01769 LVBDD lo() const {
01770 if (_root->index() == 0)
01771 throw logic_error("called lo() on terminal LVBDD");
01772 LVBDD result;
01773 result._root = _root->_lo_const_bypass();
01774 return result;
01775 }
01776
01781 LVBDD hi() const {
01782 if (_root->index() == 0)
01783 throw logic_error("called hi() on terminal LVBDD");
01784 LVBDD result;
01785 result._root = _root->_hi_const_bypass();
01786 return result;
01787 }
01788
01793 int index() const {
01794 return _root->index();
01795 }
01796
01800 void root_value(V& result) const {
01801 result = _root->value();
01802 }
01809 void evaluate(vector<bool> valuation, V& result) const {
01810 result = _eval_rec(valuation, _root);
01811 }
01812
01813 };
01814
01815 template<class L, int F>
01816 typename LVBDD<L, F>::HashMap LVBDD<L, F>::_hash_map;
01817
01818 template<class L, int F>
01819 list<Node<L, F>*> LVBDD<L, F>::_orphans;
01820
01821 template<class L, int F>
01822 int LVBDD<L, F>::_mk_call_count;
01823
01824 template<class L, int F>
01825 int LVBDD<L, F>::_orphan_fetches;
01826
01827 template<class L, int F>
01828 int LVBDD<L, F>::_node_allocations;
01829
01830 template<class L, int F>
01831 typename LVBDD<L, F>::NodeNodeMemoizer LVBDD<L, F>::_memo_nn;
01832
01833 template<class L, int F>
01834 typename LVBDD<L, F>::NodeValueMemoizer LVBDD<L, F>::_memo_nv;
01835
01836 template<class L, int F>
01837 typename LVBDD<L, F>::QuadrupleMemoizer LVBDD<L, F>::_memo_quad;
01838
01839 }
01840
01841
01842 #endif
