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