(剛剛好像看到這個問題曇花一現???) Anyway... 避免有些人不敢問這些很重要的基本問題, 我還是稍微說一下好了... 1. A graph is connected by links of nodes. The links of nodes are best implemented as node pointers (why? (*)). 2. So a simple binary decision diagram can be implemented as: class BddNodeInt { BddNodeInt* _left; BddNodeInt* _right; }; 3. However, we also like to keep some information on the node, such as "level", "reference count", "visited flag", etc. So we use 4 Bytes to store them as: class BddNodeInt { BddNodeInt* _left; BddNodeInt* _right; unsigned _level : 16; unsigned _refCount : 15; unsigned _visited : 1; }; 4. Please note that the definition of reference count is --- Let this node be 'n'. Whoever pointing to this node (e.g. "k->_left = _n", k is some BddNodeInt*), or any variable associated to this node (e.g. _bddMap("a", n), will increase the reference count of 'n'. 5. But how do you maintain the correctness of the reference count? Whenver there is a BddNodeInt* assignment, or whenever there is a _bddMap insertion, you need to increase the count. And when to decrease the count? 6. Yes, it is quite complicated to "manually" maintain the reference count. This is the case as in CUDD, which is a very error prone feature. 7. Overload the operator or member functions to take care of the count? Look again on the assignment, "k->_left = n". Since both sides are "pointers", there is no way we can overload the pointer assignment. 8. That's the motivation of using an object variable to "wrap" the pointer class --- class BddNode { BddNodeInt* _node; }; 9. All the operations on BddNodeInt* need to go through BddNode --- * In the BddNode constructor, we increase the reference count of the BddNode::_node. So if a BddNode variable is declared, the reference count of its associated BddNodeInt* will be incremented by 1. * In the BddNode descructor, we decrease the reference count of the BddNode::_node. So if the program goes out of the scope of a certain BddNode variable, the reference count of its BddNodeInt* will be decremented by 1. * In the BddNode assignment '=' operator, for example, f = g, we first decrease the reference count of "f._node", and then increase the reference count of "g._node". Of course, we will asssign "f._node = g._node" 10. That's all the place we need to worry about the reference count. As all the operations are on BddNodes, the reference counts can be maintained automatically. 11. That's why we change the BddNodeInt as --- class BddNodeInt { BddNode _left; BddNode _right; unsigned _level : 16; unsigned _refCount : 15; unsigned _visited : 1; }; In other words, when there is a link between BddNodeInt, it is wrapped by a BddNode and therefore the reference count will be incremented by 1. 12. Then how about the "complement edge"? Try --- class BddNodeInt { BddNode _left; BddNode _right; unsigned _level : 15; unsigned _refCount : 14; unsigned _visited : 1; unsigned _leftPhase : 1; unsigned _rightPhase : 1; }; How to represent ~F, where the complement flag is on the node itself but not on its children? 13. So we will take the advanatage of the fact that the pointer addresses are multiplier of 4, and we can use the lowest two bits to record the edge information. We use the lowest 1 bit to record the INVERSION. 14. To use the lower bits of a pointer variable, we need to conver it to a size_t variable, such as: v = size_t(n); and then the edge information can be added to it by v = v + 1. 15. Combining the above, we redefine the classes BddNode and BddNodeInt as... class BddNode { size_t _nodeV; // to hold BddNodeInt* and 1-bit edge info }; class BddNodeInt { BddNode _left; BddNode _right; unsigned _level : 16; unsigned _refCount : 15; unsigned _visited : 1; }; 16. We also define functions like "BddNode::operator () const { return _nodeV; }", "bool isNegEdge() const { return (_nodeV & BDD_NEG_EDGE); }"... etc. (*) The reason of using "pointers" for the links of nodes are "to share the nodes pointed by different edges. (Remember the reason for using pointers is to "share"). ---- 不小心還是寫了一堆英文, 希望大家看得懂... --

※ 發信站: 批踢踢實業坊(ptt.cc) ◆ From: 59.121.129.139 ※ 編輯: ric2k1 來自: 59.121.129.139 (01/06 17:28)