00001 // -*- c++ -*- 00002 //***************************************************************************** 00016 //***************************************************************************** 00017 00018 #ifndef polybori_iterators_CCuddNavigator_h_ 00019 #define polybori_iterators_CCuddNavigator_h_ 00020 00021 #include <iterator> 00022 00023 // include basic definitions 00024 #include <polybori/pbori_defs.h> 00025 #include <polybori/common/tags.h> 00026 #include <polybori/ring/CCuddInterface.h> 00027 00028 BEGIN_NAMESPACE_PBORI 00029 00036 class CCuddNavigator { 00037 00038 public: 00040 typedef DdNode* pointer_type; 00041 00043 typedef const pointer_type const_access_type; 00044 00046 typedef CTypes::idx_type idx_type; 00047 00049 typedef CTypes::size_type size_type; 00050 00052 typedef CTypes::deg_type deg_type; 00053 00055 typedef CTypes::hash_type hash_type; 00056 00058 typedef CTypes::bool_type bool_type; 00059 00061 typedef idx_type value_type; 00062 00064 typedef CCuddNavigator self; 00065 00067 00068 typedef navigator_tag iterator_category; 00069 typedef std::iterator_traits<pointer_type>::difference_type difference_type; 00070 typedef void pointer; 00071 typedef value_type reference; 00073 00075 CCuddNavigator(): pNode(NULL) {} 00076 00078 explicit CCuddNavigator(pointer_type ptr): pNode(ptr) { 00079 PBORI_ASSERT(isValid()); 00080 } 00081 00083 CCuddNavigator(const self& rhs): pNode(rhs.pNode) {} 00084 00086 ~CCuddNavigator() {} 00087 00089 self& incrementThen(); // inlined below 00090 00092 self thenBranch() const { return self(*this).incrementThen(); } 00093 00095 self& incrementElse(); // inlined below 00096 00098 self elseBranch() const { return self(*this).incrementElse(); } 00099 00101 reference operator*() const; // inlined below 00102 00104 const_access_type operator->() const { return pNode; } 00105 00107 const_access_type getNode() const { return pNode; } 00108 00110 hash_type hash() const { return reinterpret_cast<hash_type>(pNode); } 00111 00113 bool_type operator==(const self& rhs) const { return (pNode == rhs.pNode); } 00114 00116 bool_type operator!=(const self& rhs) const { return (pNode != rhs.pNode); } 00117 00119 bool_type isConstant() const; // inlined below 00120 00122 bool_type terminalValue() const; // inlined below 00123 00125 bool_type isValid() const { return (pNode != NULL); } 00126 00128 bool_type isTerminated() const { return isConstant() && terminalValue(); } 00129 00131 bool_type isEmpty() const { return isConstant() && !terminalValue(); } 00132 00134 00135 bool_type operator<(const self& rhs) const { return (pNode < rhs.pNode); } 00136 bool_type operator<=(const self& rhs) const { return (pNode <= rhs.pNode); } 00137 bool_type operator>(const self& rhs) const { return (pNode > rhs.pNode); } 00138 bool_type operator>=(const self& rhs) const { return (pNode >= rhs.pNode); } 00140 00142 void incRef() const { PBORI_ASSERT(isValid()); PBORI_PREFIX(Cudd_Ref)(pNode); } 00143 00145 void decRef() const { PBORI_ASSERT(isValid()); PBORI_PREFIX(Cudd_Deref)(pNode); } 00146 00148 template <class MgrType> 00149 void recursiveDecRef(const MgrType& mgr) const { 00150 PBORI_ASSERT(isValid()); 00151 PBORI_PREFIX(Cudd_RecursiveDerefZdd)(mgr, pNode); 00152 } 00153 00154 private: 00156 pointer_type pNode; 00157 }; 00158 00159 // Inlined member functions 00160 00161 // constant pointer access operator 00162 inline CCuddNavigator::value_type 00163 CCuddNavigator::operator*() const { 00164 00165 PBORI_TRACE_FUNC( "CCuddNavigator::operator*() const" ); 00166 PBORI_ASSERT(isValid()); 00167 return Cudd_Regular(pNode)->index; 00168 } 00169 00170 // whether constant node was reached 00171 inline CCuddNavigator::bool_type 00172 CCuddNavigator::isConstant() const { 00173 00174 PBORI_TRACE_FUNC( "CCuddNavigator::isConstant() const" ); 00175 PBORI_ASSERT(isValid()); 00176 return Cudd_IsConstant(pNode); 00177 } 00178 00179 // constant node value 00180 inline CCuddNavigator::bool_type 00181 CCuddNavigator::terminalValue() const { 00182 00183 PBORI_TRACE_FUNC( "CCuddNavigator::terminalValue() const" ); 00184 PBORI_ASSERT(isConstant()); 00185 return Cudd_V(pNode); 00186 } 00187 00188 00189 // increment in then direction 00190 inline CCuddNavigator& 00191 CCuddNavigator::incrementThen() { 00192 00193 PBORI_TRACE_FUNC( "CCuddNavigator::incrementThen()" ); 00194 00195 PBORI_ASSERT(isValid()); 00196 pNode = Cudd_T(pNode); 00197 00198 return *this; 00199 } 00200 00201 // increment in else direction 00202 inline CCuddNavigator& 00203 CCuddNavigator::incrementElse() { 00204 00205 PBORI_TRACE_FUNC( "CCuddNavigator::incrementElse()" ); 00206 00207 PBORI_ASSERT(isValid()); 00208 pNode = Cudd_E(pNode); 00209 00210 return *this; 00211 } 00212 00213 inline CCuddNavigator 00214 explicit_navigator_cast(CCuddNavigator::pointer_type ptr) { 00215 00216 #ifndef PBORI_NDEBUG 00217 if (ptr == NULL) 00218 return CCuddNavigator(); 00219 else 00220 #endif 00221 return CCuddNavigator(ptr); 00222 } 00223 00224 00225 END_NAMESPACE_PBORI 00226 00227 #endif
1.5.6