PolyBoRi
CCuddNavigator.h
Go to the documentation of this file.
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