• Main Page
  • Related Pages
  • Namespaces
  • Classes
  • Files
  • File List
  • File Members

CCuddNavigator.h

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

Generated on Wed Sep 29 2010 for PolyBoRi by  doxygen 1.7.1