2011CaoTme7: Bdd.h

File Bdd.h, 4.0 KB (added by jpc, 14 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__