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