PolyBoRi
CCuddNavigator.h
Go to the documentation of this file.
1 // -*- c++ -*-
2 //*****************************************************************************
93 //*****************************************************************************
94 
95 #include <iterator>
96 
97 // include basic definitions
98 #include "pbori_defs.h"
99 #include "pbori_tags.h"
100 
101 #include "CCuddInterface.h"
102 
103 
104 #ifndef CCuddNavigator_h_
105 #define CCuddNavigator_h_
106 
108 
116 
117 public:
119  typedef DdNode* pointer_type;
120 
123 
126 
129 
132 
135 
138 
141 
143  typedef CCuddNavigator self;
144 
146 
148  typedef std::iterator_traits<pointer_type>::difference_type difference_type;
149  typedef void pointer;
152 
154  CCuddNavigator(): pNode(NULL) {}
155 
157  explicit CCuddNavigator(pointer_type ptr): pNode(ptr) {
158  assert(isValid());
159  }
160 
162  explicit CCuddNavigator(const dd_base& rhs): pNode(rhs.getNode()) {}
163 
165  CCuddNavigator(const self& rhs): pNode(rhs.pNode) {}
166 
169 
171  self& incrementThen(); // inlined below
172 
174  self thenBranch() const { return self(*this).incrementThen(); }
175 
177  self& incrementElse(); // inlined below
178 
180  self elseBranch() const { return self(*this).incrementElse(); }
181 
183  reference operator*() const; // inlined below
184 
186  const_access_type operator->() const { return pNode; }
187 
189  const_access_type getNode() const { return pNode; }
190 
192  hash_type hash() const { return reinterpret_cast<long>(pNode); }
193 
195  bool_type operator==(const self& rhs) const { return (pNode == rhs.pNode); }
196 
198  bool_type operator!=(const self& rhs) const { return (pNode != rhs.pNode); }
199 
201  bool_type isConstant() const; // inlined below
202 
204  bool_type terminalValue() const; // inlined below
205 
207  bool_type isValid() const { return (pNode != NULL); }
208 
210  bool_type isTerminated() const { return isConstant() && terminalValue(); }
211 
213  bool_type isEmpty() const { return isConstant() && !terminalValue(); }
214 
216 
217  bool_type operator<(const self& rhs) const { return (pNode < rhs.pNode); }
218  bool_type operator<=(const self& rhs) const { return (pNode <= rhs.pNode); }
219  bool_type operator>(const self& rhs) const { return (pNode > rhs.pNode); }
220  bool_type operator>=(const self& rhs) const { return (pNode >= rhs.pNode); }
222 
224  void incRef() const { assert(isValid()); Cudd_Ref(pNode); }
225 
227  void decRef() const { assert(isValid()); Cudd_Deref(pNode); }
228 
230  template <class MgrType>
231  void recursiveDecRef(const MgrType& mgr) const {
232  assert(isValid());
233  Cudd_RecursiveDerefZdd(mgr, pNode);
234  }
235 
236 private:
238  pointer_type pNode;
239 };
240 
241 // Inlined member functions
242 
243 // constant pointer access operator
244 inline CCuddNavigator::value_type
246 
247  PBORI_TRACE_FUNC( "CCuddNavigator::operator*() const" );
248  assert(isValid());
249  return Cudd_Regular(pNode)->index;
250 }
251 
252 // whether constant node was reached
254 CCuddNavigator::isConstant() const {
255 
256  PBORI_TRACE_FUNC( "CCuddNavigator::isConstant() const" );
257  assert(isValid());
258  return Cudd_IsConstant(pNode);
259 }
260 
261 // constant node value
263 CCuddNavigator::terminalValue() const {
264 
265  PBORI_TRACE_FUNC( "CCuddNavigator::terminalValue() const" );
266  assert(isConstant());
267  return Cudd_V(pNode);
268 }
269 
270 
271 // increment in then direction
272 inline CCuddNavigator&
273 CCuddNavigator::incrementThen() {
274 
275  PBORI_TRACE_FUNC( "CCuddNavigator::incrementThen()" );
276 
277  assert(isValid());
278  pNode = Cudd_T(pNode);
279 
280  return *this;
281 }
282 
283 // increment in else direction
284 inline CCuddNavigator&
285 CCuddNavigator::incrementElse() {
286 
287  PBORI_TRACE_FUNC( "CCuddNavigator::incrementElse()" );
288 
289  assert(isValid());
290  pNode = Cudd_E(pNode);
291 
292  return *this;
293 }
294 
295 inline CCuddNavigator
297 
298 #ifndef NDEBUG
299  if (ptr == NULL)
300  return CCuddNavigator();
301  else
302 #endif
303  return CCuddNavigator(ptr);
304 }
305 
306 
308 
309 #endif