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