PolyBoRi
|
00001 // -*- c++ -*- 00002 //***************************************************************************** 00016 //***************************************************************************** 00017 00018 #include <iterator> 00019 00020 // include basic definitions 00021 #include "pbori_defs.h" 00022 #include "pbori_tags.h" 00023 00024 #include "CCuddInterface.h" 00025 00026 #ifndef CCuddNavigator_h_ 00027 #define CCuddNavigator_h_ 00028 00029 BEGIN_NAMESPACE_PBORI 00030 00037 class CCuddNavigator { 00038 00039 public: 00041 typedef DdNode* pointer_type; 00042 00044 typedef const pointer_type const_access_type; 00045 00047 typedef CTypes::idx_type idx_type; 00048 00050 typedef CTypes::size_type size_type; 00051 00053 typedef CTypes::deg_type deg_type; 00054 00056 typedef CTypes::hash_type hash_type; 00057 00059 typedef CTypes::bool_type bool_type; 00060 00062 typedef idx_type value_type; 00063 00065 typedef CCuddNavigator self; 00066 00068 00069 typedef navigator_tag iterator_category; 00070 typedef std::iterator_traits<pointer_type>::difference_type difference_type; 00071 typedef void pointer; 00072 typedef value_type reference; 00074 00076 CCuddNavigator(): pNode(NULL) {} 00077 00079 explicit CCuddNavigator(pointer_type ptr): pNode(ptr) { 00080 assert(isValid()); 00081 } 00082 00084 CCuddNavigator(const self& rhs): pNode(rhs.pNode) {} 00085 00087 ~CCuddNavigator() {} 00088 00090 self& incrementThen(); // inlined below 00091 00093 self thenBranch() const { return self(*this).incrementThen(); } 00094 00096 self& incrementElse(); // inlined below 00097 00099 self elseBranch() const { return self(*this).incrementElse(); } 00100 00102 reference operator*() const; // inlined below 00103 00105 const_access_type operator->() const { return pNode; } 00106 00108 const_access_type getNode() const { return pNode; } 00109 00111 hash_type hash() const { return reinterpret_cast<hash_type>(pNode); } 00112 00114 bool_type operator==(const self& rhs) const { return (pNode == rhs.pNode); } 00115 00117 bool_type operator!=(const self& rhs) const { return (pNode != rhs.pNode); } 00118 00120 bool_type isConstant() const; // inlined below 00121 00123 bool_type terminalValue() const; // inlined below 00124 00126 bool_type isValid() const { return (pNode != NULL); } 00127 00129 bool_type isTerminated() const { return isConstant() && terminalValue(); } 00130 00132 bool_type isEmpty() const { return isConstant() && !terminalValue(); } 00133 00135 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); } 00139 bool_type operator>=(const self& rhs) const { return (pNode >= rhs.pNode); } 00141 00143 void incRef() const { assert(isValid()); Cudd_Ref(pNode); } 00144 00146 void decRef() const { assert(isValid()); Cudd_Deref(pNode); } 00147 00149 template <class MgrType> 00150 void recursiveDecRef(const MgrType& mgr) const { 00151 assert(isValid()); 00152 Cudd_RecursiveDerefZdd(mgr, pNode); 00153 } 00154 00155 private: 00157 pointer_type pNode; 00158 }; 00159 00160 // Inlined member functions 00161 00162 // constant pointer access operator 00163 inline CCuddNavigator::value_type 00164 CCuddNavigator::operator*() const { 00165 00166 PBORI_TRACE_FUNC( "CCuddNavigator::operator*() const" ); 00167 assert(isValid()); 00168 return Cudd_Regular(pNode)->index; 00169 } 00170 00171 // whether constant node was reached 00172 inline CCuddNavigator::bool_type 00173 CCuddNavigator::isConstant() const { 00174 00175 PBORI_TRACE_FUNC( "CCuddNavigator::isConstant() const" ); 00176 assert(isValid()); 00177 return Cudd_IsConstant(pNode); 00178 } 00179 00180 // constant node value 00181 inline CCuddNavigator::bool_type 00182 CCuddNavigator::terminalValue() const { 00183 00184 PBORI_TRACE_FUNC( "CCuddNavigator::terminalValue() const" ); 00185 assert(isConstant()); 00186 return Cudd_V(pNode); 00187 } 00188 00189 00190 // increment in then direction 00191 inline CCuddNavigator& 00192 CCuddNavigator::incrementThen() { 00193 00194 PBORI_TRACE_FUNC( "CCuddNavigator::incrementThen()" ); 00195 00196 assert(isValid()); 00197 pNode = Cudd_T(pNode); 00198 00199 return *this; 00200 } 00201 00202 // increment in else direction 00203 inline CCuddNavigator& 00204 CCuddNavigator::incrementElse() { 00205 00206 PBORI_TRACE_FUNC( "CCuddNavigator::incrementElse()" ); 00207 00208 assert(isValid()); 00209 pNode = Cudd_E(pNode); 00210 00211 return *this; 00212 } 00213 00214 inline CCuddNavigator 00215 explicit_navigator_cast(CCuddNavigator::pointer_type ptr) { 00216 00217 #ifndef NDEBUG 00218 if (ptr == NULL) 00219 return CCuddNavigator(); 00220 else 00221 #endif 00222 return CCuddNavigator(ptr); 00223 } 00224 00225 00226 END_NAMESPACE_PBORI 00227 00228 #endif