CCuddNavigator.h
Go to the documentation of this file.
// -*- c++ -*-
//*****************************************************************************
//*****************************************************************************
#ifndef polybori_iterators_CCuddNavigator_h_
#define polybori_iterators_CCuddNavigator_h_
#include <iterator>
// include basic definitions
#include <polybori/pbori_defs.h>
#include <polybori/common/tags.h>
#include <polybori/ring/CCuddInterface.h>
BEGIN_NAMESPACE_PBORI
class CCuddNavigator {
public:
typedef DdNode* pointer_type;
typedef const pointer_type const_access_type;
typedef CTypes::idx_type idx_type;
typedef CTypes::size_type size_type;
typedef CTypes::deg_type deg_type;
typedef CTypes::hash_type hash_type;
typedef CTypes::bool_type bool_type;
typedef idx_type value_type;
typedef CCuddNavigator self;
typedef navigator_tag iterator_category;
typedef std::iterator_traits<pointer_type>::difference_type difference_type;
typedef void pointer;
typedef value_type reference;
CCuddNavigator(): pNode(NULL) {}
explicit CCuddNavigator(pointer_type ptr): pNode(ptr) {
PBORI_ASSERT(isValid());
}
CCuddNavigator(const self& rhs): pNode(rhs.pNode) {}
~CCuddNavigator() {}
self& incrementThen(); // inlined below
self thenBranch() const { return self(*this).incrementThen(); }
self& incrementElse(); // inlined below
self elseBranch() const { return self(*this).incrementElse(); }
reference operator*() const; // inlined below
const_access_type operator->() const { return pNode; }
const_access_type getNode() const { return pNode; }
hash_type hash() const { return reinterpret_cast<hash_type>(pNode); }
bool_type operator==(const self& rhs) const { return (pNode == rhs.pNode); }
bool_type operator!=(const self& rhs) const { return (pNode != rhs.pNode); }
bool_type isConstant() const; // inlined below
bool_type terminalValue() const; // inlined below
bool_type isValid() const { return (pNode != NULL); }
bool_type isTerminated() const { return isConstant() && terminalValue(); }
bool_type isEmpty() const { return isConstant() && !terminalValue(); }
bool_type operator<(const self& rhs) const { return (pNode < rhs.pNode); }
bool_type operator<=(const self& rhs) const { return (pNode <= rhs.pNode); }
bool_type operator>(const self& rhs) const { return (pNode > rhs.pNode); }
bool_type operator>=(const self& rhs) const { return (pNode >= rhs.pNode); }
void incRef() const { PBORI_ASSERT(isValid()); PBORI_PREFIX(Cudd_Ref)(pNode); }
void decRef() const { PBORI_ASSERT(isValid()); PBORI_PREFIX(Cudd_Deref)(pNode); }
template <class MgrType>
void recursiveDecRef(const MgrType& mgr) const {
PBORI_ASSERT(isValid());
PBORI_PREFIX(Cudd_RecursiveDerefZdd)(mgr, pNode);
}
private:
pointer_type pNode;
};
// Inlined member functions
// constant pointer access operator
inline CCuddNavigator::value_type
CCuddNavigator::operator*() const {
PBORI_TRACE_FUNC( "CCuddNavigator::operator*() const" );
PBORI_ASSERT(isValid());
return Cudd_Regular(pNode)->index;
}
// whether constant node was reached
inline CCuddNavigator::bool_type
CCuddNavigator::isConstant() const {
PBORI_TRACE_FUNC( "CCuddNavigator::isConstant() const" );
PBORI_ASSERT(isValid());
return Cudd_IsConstant(pNode);
}
// constant node value
inline CCuddNavigator::bool_type
CCuddNavigator::terminalValue() const {
PBORI_TRACE_FUNC( "CCuddNavigator::terminalValue() const" );
PBORI_ASSERT(isConstant());
return Cudd_V(pNode);
}
// increment in then direction
inline CCuddNavigator&
CCuddNavigator::incrementThen() {
PBORI_TRACE_FUNC( "CCuddNavigator::incrementThen()" );
PBORI_ASSERT(isValid());
pNode = Cudd_T(pNode);
return *this;
}
// increment in else direction
inline CCuddNavigator&
CCuddNavigator::incrementElse() {
PBORI_TRACE_FUNC( "CCuddNavigator::incrementElse()" );
PBORI_ASSERT(isValid());
pNode = Cudd_E(pNode);
return *this;
}
inline CCuddNavigator
explicit_navigator_cast(CCuddNavigator::pointer_type ptr) {
#ifndef PBORI_NDEBUG
if (ptr == NULL)
return CCuddNavigator();
else
#endif
return CCuddNavigator(ptr);
}
END_NAMESPACE_PBORI
#endif