PolyBoRi
|
00001 // -*- c++ -*- 00002 //***************************************************************************** 00093 //***************************************************************************** 00094 00095 #include <iterator> 00096 00097 // include basic definitions 00098 #include "pbori_defs.h" 00099 #include "pbori_tags.h" 00100 00101 #include "CCuddInterface.h" 00102 00103 00104 #ifndef CCuddNavigator_h_ 00105 #define CCuddNavigator_h_ 00106 00107 BEGIN_NAMESPACE_PBORI 00108 00115 class CCuddNavigator { 00116 00117 public: 00119 typedef DdNode* pointer_type; 00120 00122 typedef CTypes::dd_base dd_base; 00123 00125 typedef const pointer_type const_access_type; 00126 00128 typedef CTypes::idx_type idx_type; 00129 00131 typedef CTypes::size_type size_type; 00132 00134 typedef CTypes::hash_type hash_type; 00135 00137 typedef CTypes::bool_type bool_type; 00138 00140 typedef idx_type value_type; 00141 00143 typedef CCuddNavigator self; 00144 00146 00147 typedef navigator_tag iterator_category; 00148 typedef std::iterator_traits<pointer_type>::difference_type difference_type; 00149 typedef void pointer; 00150 typedef value_type reference; 00152 00154 CCuddNavigator(): pNode(NULL) {} 00155 00157 explicit CCuddNavigator(pointer_type ptr): pNode(ptr) { 00158 assert(isValid()); 00159 } 00160 00162 explicit CCuddNavigator(const dd_base& rhs): pNode(rhs.getNode()) {} 00163 00165 CCuddNavigator(const self& rhs): pNode(rhs.pNode) {} 00166 00168 ~CCuddNavigator() {} 00169 00171 self& incrementThen(); // inlined below 00172 00174 self thenBranch() const { return self(*this).incrementThen(); } 00175 00177 self& incrementElse(); // inlined below 00178 00180 self elseBranch() const { return self(*this).incrementElse(); } 00181 00183 reference operator*() const; // inlined below 00184 00186 const_access_type operator->() const { return pNode; } 00187 00189 const_access_type getNode() const { return pNode; } 00190 00192 hash_type hash() const { return reinterpret_cast<long>(pNode); } 00193 00195 bool_type operator==(const self& rhs) const { return (pNode == rhs.pNode); } 00196 00198 bool_type operator!=(const self& rhs) const { return (pNode != rhs.pNode); } 00199 00201 bool_type isConstant() const; // inlined below 00202 00204 bool_type terminalValue() const; // inlined below 00205 00207 bool_type isValid() const { return (pNode != NULL); } 00208 00210 bool_type isTerminated() const { return isConstant() && terminalValue(); } 00211 00213 bool_type isEmpty() const { return isConstant() && !terminalValue(); } 00214 00216 00217 bool_type operator<(const self& rhs) const { return (pNode < rhs.pNode); } 00218 bool_type operator<=(const self& rhs) const { return (pNode <= rhs.pNode); } 00219 bool_type operator>(const self& rhs) const { return (pNode > rhs.pNode); } 00220 bool_type operator>=(const self& rhs) const { return (pNode >= rhs.pNode); } 00222 00224 void incRef() const { assert(isValid()); Cudd_Ref(pNode); } 00225 00227 void decRef() const { assert(isValid()); Cudd_Deref(pNode); } 00228 00230 template <class MgrType> 00231 void recursiveDecRef(const MgrType& mgr) const { 00232 assert(isValid()); 00233 Cudd_RecursiveDerefZdd(mgr, pNode); 00234 } 00235 00236 private: 00238 pointer_type pNode; 00239 }; 00240 00241 // Inlined member functions 00242 00243 // constant pointer access operator 00244 inline CCuddNavigator::value_type 00245 CCuddNavigator::operator*() const { 00246 00247 PBORI_TRACE_FUNC( "CCuddNavigator::operator*() const" ); 00248 assert(isValid()); 00249 return Cudd_Regular(pNode)->index; 00250 } 00251 00252 // whether constant node was reached 00253 inline CCuddNavigator::bool_type 00254 CCuddNavigator::isConstant() const { 00255 00256 PBORI_TRACE_FUNC( "CCuddNavigator::isConstant() const" ); 00257 assert(isValid()); 00258 return Cudd_IsConstant(pNode); 00259 } 00260 00261 // constant node value 00262 inline CCuddNavigator::bool_type 00263 CCuddNavigator::terminalValue() const { 00264 00265 PBORI_TRACE_FUNC( "CCuddNavigator::terminalValue() const" ); 00266 assert(isConstant()); 00267 return Cudd_V(pNode); 00268 } 00269 00270 00271 // increment in then direction 00272 inline CCuddNavigator& 00273 CCuddNavigator::incrementThen() { 00274 00275 PBORI_TRACE_FUNC( "CCuddNavigator::incrementThen()" ); 00276 00277 assert(isValid()); 00278 pNode = Cudd_T(pNode); 00279 00280 return *this; 00281 } 00282 00283 // increment in else direction 00284 inline CCuddNavigator& 00285 CCuddNavigator::incrementElse() { 00286 00287 PBORI_TRACE_FUNC( "CCuddNavigator::incrementElse()" ); 00288 00289 assert(isValid()); 00290 pNode = Cudd_E(pNode); 00291 00292 return *this; 00293 } 00294 00295 inline CCuddNavigator 00296 explicit_navigator_cast(CCuddNavigator::pointer_type ptr) { 00297 00298 #ifndef NDEBUG 00299 if (ptr == NULL) 00300 return CCuddNavigator(); 00301 else 00302 #endif 00303 return CCuddNavigator(ptr); 00304 } 00305 00306 00307 END_NAMESPACE_PBORI 00308 00309 #endif