2011CaoTme7: Bdd.h

File Bdd.h, 4.0 KB (added by jpc, 15 years ago)

C++ Header: Classe Bdd

Line 
1
2#ifndef __BDD_H__
3#define __BDD_H__
4
5#include <string>
6#include <iostream>
7#include <map>
8
9
10class Ebm;
11
12
13class Bdd {
14 public:
15 class Key {
16 private:
17 unsigned int _index;
18 unsigned int _highIdent;
19 unsigned int _lowIdent;
20 public:
21 inline Key ( unsigned int index, unsigned int high, unsigned int low );
22 friend bool operator< ( const Key& lhs, const Key& rhs );
23 };
24 private:
25 static unsigned int _maxIdent;
26 static unsigned int _maxStamp;
27 static std::map<Key,Bdd*> _bdds;
28 private:
29 unsigned int _ident; // Unicity identifier.
30 unsigned int _index; // Decomposition variable index.
31 Bdd* _high; // Low cofactor pointer.
32 Bdd* _low; // High cofactor pointer.
33 unsigned _stamp; // Used to flag already reached nodes in the DAG recursive walktrhough.
34 public:
35 static Bdd* One;
36 static Bdd* Zero;
37 private:
38 Bdd ( unsigned index, Bdd* high, Bdd* low );
39 ~Bdd ();
40 public :
41 static Bdd* create ( unsigned index, Bdd* high, Bdd* low );
42 static Bdd* apply ( Ebm::OperatorType, Bdd*, Bdd* );
43 static Bdd* Not ( Bdd* );
44 static Bdd* And ( Bdd*, Bdd* );
45 static Bdd* And ( Bdd*, Bdd*, Bdd* );
46 static Bdd* And ( Bdd*, Bdd*, Bdd*, Bdd* );
47 static Bdd* Xor ( Bdd*, Bdd* );
48 static Bdd* Xor ( Bdd*, Bdd*, Bdd* );
49 static Bdd* Xor ( Bdd*, Bdd*, Bdd*, Bdd* );
50 static Bdd* Or ( Bdd*, Bdd* );
51 static Bdd* Or ( Bdd*, Bdd*, Bdd* );
52 static Bdd* Or ( Bdd*, Bdd*, Bdd*, Bdd* );
53 public:
54 inline unsigned getIdent ();
55 inline unsigned getIndex ();
56 inline Bdd* getHigh ();
57 inline Bdd* getLow ();
58 Bdd* neg ();
59 unsigned int depth ();
60 Bdd* satisfy ();
61 void display ( std::ostream& );
62 void toDot ( const string& filename );
63 void toDot ( std::ostream& );
64 BoolValue eval ();
65 Ebm* toEbm ();
66 static Bdd* fromEbm ( Ebm* );
67 private:
68 inline Key _getKey ();
69 void _display ( std::ostream& );
70 void _toDot ( std::ostream& );
71 friend std::ostream& operator<< ( std::ostream&, const Bdd* );
72};
73
74
75// Bdd inline methods.
76inline unsigned int Bdd::getIdent () { return _ident; }
77inline unsigned int Bdd::getIndex () { return _index; }
78inline Bdd* Bdd::getHigh () { return _high; }
79inline Bdd* Bdd::getLow () { return _low; }
80
81inline Bdd::Key Bdd::_getKey ()
82{
83 return Key ( _index
84 , (_high == NULL) ? 0 : _high->_index
85 , (_low == NULL) ? 0 : _low ->_index );
86}
87
88
89// Bdd::Key inline method.
90inline Bdd::Key::Key ( unsigned int index, unsigned int high, unsigned int low )
91 : _index (index)
92 , _highIdent(high)
93 , _lowIdent (low)
94{ }
95
96
97inline bool operator< ( const Bdd::Key& lhs, const Bdd::Key& rhs )
98{
99// Uses lexicographical order (_index,_lowId,_highId).
100 if ( lhs._index != rhs._index )
101 return ( lhs._index < rhs._index );
102
103 if ( lhs._lowIdent != rhs._lowIdent )
104 return ( lhs._lowIdent < rhs._lowIdent );
105
106 return ( lhs._highIdent < rhs._highIdent );
107}
108
109
110#endif // __BDD_H__