PolyBoRi
CCuddNavigator.h
Go to the documentation of this file.
1 // -*- c++ -*-
2 //*****************************************************************************
16 //*****************************************************************************
17 
18 #ifndef polybori_iterators_CCuddNavigator_h_
19 #define polybori_iterators_CCuddNavigator_h_
20 
21 #include <iterator>
22 
23 // include basic definitions
24 #include <polybori/pbori_defs.h>
25 #include <polybori/common/tags.h>
27 
29 
37 
38 public:
40  typedef DdNode* pointer_type;
41 
44 
47 
50 
53 
56 
59 
62 
64  typedef CCuddNavigator self;
65 
67 
69  typedef std::iterator_traits<pointer_type>::difference_type difference_type;
70  typedef void pointer;
73 
75  CCuddNavigator(): pNode(NULL) {}
76 
78  explicit CCuddNavigator(pointer_type ptr): pNode(ptr) {
79  PBORI_ASSERT(isValid());
80  }
81 
83  CCuddNavigator(const self& rhs): pNode(rhs.pNode) {}
84 
87 
89  self& incrementThen(); // inlined below
90 
92  self thenBranch() const { return self(*this).incrementThen(); }
93 
95  self& incrementElse(); // inlined below
96 
98  self elseBranch() const { return self(*this).incrementElse(); }
99 
101  reference operator*() const; // inlined below
102 
104  const_access_type operator->() const { return pNode; }
105 
107  const_access_type getNode() const { return pNode; }
108 
110  hash_type hash() const { return reinterpret_cast<hash_type>(pNode); }
111 
113  bool_type operator==(const self& rhs) const { return (pNode == rhs.pNode); }
114 
116  bool_type operator!=(const self& rhs) const { return (pNode != rhs.pNode); }
117 
119  bool_type isConstant() const; // inlined below
120 
122  bool_type terminalValue() const; // inlined below
123 
125  bool_type isValid() const { return (pNode != NULL); }
126 
128  bool_type isTerminated() const { return isConstant() && terminalValue(); }
129 
131  bool_type isEmpty() const { return isConstant() && !terminalValue(); }
132 
134 
135  bool_type operator<(const self& rhs) const { return (pNode < rhs.pNode); }
136  bool_type operator<=(const self& rhs) const { return (pNode <= rhs.pNode); }
137  bool_type operator>(const self& rhs) const { return (pNode > rhs.pNode); }
138  bool_type operator>=(const self& rhs) const { return (pNode >= rhs.pNode); }
140 
142  void incRef() const { PBORI_ASSERT(isValid()); PBORI_PREFIX(Cudd_Ref)(pNode); }
143 
145  void decRef() const { PBORI_ASSERT(isValid()); PBORI_PREFIX(Cudd_Deref)(pNode); }
146 
148  template <class MgrType>
149  void recursiveDecRef(const MgrType& mgr) const {
150  PBORI_ASSERT(isValid());
151  PBORI_PREFIX(Cudd_RecursiveDerefZdd)(mgr, pNode);
152  }
153 
154 private:
156  pointer_type pNode;
157 };
158 
159 // Inlined member functions
160 
161 // constant pointer access operator
162 inline CCuddNavigator::value_type
164 
165  PBORI_TRACE_FUNC( "CCuddNavigator::operator*() const" );
166  PBORI_ASSERT(isValid());
167  return Cudd_Regular(pNode)->index;
168 }
169 
170 // whether constant node was reached
172 CCuddNavigator::isConstant() const {
173 
174  PBORI_TRACE_FUNC( "CCuddNavigator::isConstant() const" );
175  PBORI_ASSERT(isValid());
176  return Cudd_IsConstant(pNode);
177 }
178 
179 // constant node value
181 CCuddNavigator::terminalValue() const {
182 
183  PBORI_TRACE_FUNC( "CCuddNavigator::terminalValue() const" );
184  PBORI_ASSERT(isConstant());
185  return Cudd_V(pNode);
186 }
187 
188 
189 // increment in then direction
190 inline CCuddNavigator&
191 CCuddNavigator::incrementThen() {
192 
193  PBORI_TRACE_FUNC( "CCuddNavigator::incrementThen()" );
194 
195  PBORI_ASSERT(isValid());
196  pNode = Cudd_T(pNode);
197 
198  return *this;
199 }
200 
201 // increment in else direction
202 inline CCuddNavigator&
203 CCuddNavigator::incrementElse() {
204 
205  PBORI_TRACE_FUNC( "CCuddNavigator::incrementElse()" );
206 
207  PBORI_ASSERT(isValid());
208  pNode = Cudd_E(pNode);
209 
210  return *this;
211 }
212 
213 inline CCuddNavigator
215 
216 #ifndef PBORI_NDEBUG
217  if (ptr == NULL)
218  return CCuddNavigator();
219  else
220 #endif
221  return CCuddNavigator(ptr);
222 }
223 
224 
226 
227 #endif