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

CCuddNavigator.h

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

Generated on Thu Oct 21 2010 02:56:31 for PolyBoRi by  doxygen 1.7.1