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
PBORI_PREFIX
#define PBORI_PREFIX(name)
Definition: prefix.h:27
polybori::CCuddNavigator::size_type
CTypes::size_type size_type
Type for indices.
Definition: CCuddNavigator.h:49
END_NAMESPACE_PBORI
#define END_NAMESPACE_PBORI
Finish project's namespace.
Definition: pbori_defs.h:77
polybori::CCuddNavigator::iterator_category
navigator_tag iterator_category
Definition: CCuddNavigator.h:68
BEGIN_NAMESPACE_PBORI
#define BEGIN_NAMESPACE_PBORI
Start project's namespace.
Definition: pbori_defs.h:74
polybori::CCuddNavigator::reference
value_type reference
Definition: CCuddNavigator.h:71
Cudd_RecursiveDerefZdd
#define Cudd_RecursiveDerefZdd
Definition: prefix_internal.h:149
polybori::CAuxTypes::deg_type
int deg_type
Type for polynomial degrees (ranges from -1 to maxint)
Definition: pbori_defs.h:222
polybori::CCuddNavigator::incRef
void incRef() const
Force incrementation of reference count.
Definition: CCuddNavigator.h:142
polybori::explicit_navigator_cast
CCuddNavigator explicit_navigator_cast(CCuddNavigator::pointer_type ptr)
Definition: CCuddNavigator.h:214
polybori::CCuddNavigator::bool_type
CTypes::bool_type bool_type
Type for boolean results.
Definition: CCuddNavigator.h:58
polybori::CCuddNavigator::operator!=
bool_type operator!=(const self &rhs) const
Nonequality test.
Definition: CCuddNavigator.h:116
polybori::CCuddNavigator::decRef
void decRef() const
Force decrementation of reference count.
Definition: CCuddNavigator.h:145
polybori::CCuddNavigator::elseBranch
self elseBranch() const
Increment in else direction.
Definition: CCuddNavigator.h:98
polybori::CCuddNavigator::isEmpty
bool_type isEmpty() const
Check whether dead end was reached.
Definition: CCuddNavigator.h:131
polybori::CAuxTypes::hash_type
std::size_t hash_type
Type for hashing.
Definition: pbori_defs.h:231
polybori::CCuddNavigator::idx_type
CTypes::idx_type idx_type
Type for indices.
Definition: CCuddNavigator.h:46
polybori::CCuddNavigator::CCuddNavigator
CCuddNavigator(const self &rhs)
Copy Constructor.
Definition: CCuddNavigator.h:83
polybori::CCuddNavigator::operator->
const_access_type operator->() const
Constant pointer access operator.
Definition: CCuddNavigator.h:104
pbori_defs.h
polybori::CCuddNavigator::operator==
bool_type operator==(const self &rhs) const
Equality test.
Definition: CCuddNavigator.h:113
polybori::CCuddNavigator::isTerminated
bool_type isTerminated() const
Check whether end of path was reached.
Definition: CCuddNavigator.h:128
polybori::CCuddNavigator::pointer
void pointer
Definition: CCuddNavigator.h:70
polybori::CCuddNavigator::thenBranch
self thenBranch() const
Increment in then direction.
Definition: CCuddNavigator.h:92
PBORI_ASSERT
#define PBORI_ASSERT(arg)
Definition: pbori_defs.h:118
polybori::CCuddNavigator::operator<
bool_type operator<(const self &rhs) const
Definition: CCuddNavigator.h:135
polybori::CCuddNavigator::value_type
idx_type value_type
Return type of dereferencing operator.
Definition: CCuddNavigator.h:61
polybori::CAuxTypes::idx_type
int idx_type
Type for indices.
Definition: pbori_defs.h:228
polybori::CCuddNavigator::hash_type
CTypes::hash_type hash_type
Type for hashing.
Definition: CCuddNavigator.h:55
polybori::CCuddNavigator::operator>
bool_type operator>(const self &rhs) const
Definition: CCuddNavigator.h:137
polybori::CCuddNavigator::getNode
const_access_type getNode() const
Constant pointer access operator.
Definition: CCuddNavigator.h:107
polybori::CCuddNavigator::~CCuddNavigator
~CCuddNavigator()
Destructor.
Definition: CCuddNavigator.h:86
polybori::CCuddNavigator::recursiveDecRef
void recursiveDecRef(const MgrType &mgr) const
Force recursive decrementation of reference count.
Definition: CCuddNavigator.h:149
polybori::CCuddNavigator::hash
hash_type hash() const
Constant pointer access operator.
Definition: CCuddNavigator.h:110
polybori::CCuddNavigator::operator>=
bool_type operator>=(const self &rhs) const
Definition: CCuddNavigator.h:138
polybori::CCuddNavigator::incrementThen
self & incrementThen()
Increment in then direction.
Definition: CCuddNavigator.h:191
polybori::CCuddNavigator::const_access_type
const pointer_type const_access_type
Type for constantly accessing node pointer.
Definition: CCuddNavigator.h:43
polybori::CCuddNavigator::deg_type
CTypes::deg_type deg_type
Type for degrees.
Definition: CCuddNavigator.h:52
CCuddInterface.h
Cudd_Deref
#define Cudd_Deref
Definition: prefix_internal.h:160
tags.h
polybori::CCuddNavigator::CCuddNavigator
CCuddNavigator()
Default constructor.
Definition: CCuddNavigator.h:75
polybori::CAuxTypes::size_type
std::size_t size_type
Type for lengths, dimensions, etc.
Definition: pbori_defs.h:219
polybori::CCuddNavigator::isValid
bool_type isValid() const
Check whether *this is not the default iterator self() (NULL pointer)
Definition: CCuddNavigator.h:125
polybori::operator*
BooleConstant operator*(const BooleConstant &lhs, const BooleConstant &rhs)
Definition: BooleConstant.h:124
polybori::CCuddNavigator
This class defines an iterator for navigating through then and else branches of ZDDs.
Definition: CCuddNavigator.h:36
polybori::CCuddNavigator::incrementElse
self & incrementElse()
Increment in else direction.
Definition: CCuddNavigator.h:203
polybori::CCuddNavigator::operator<=
bool_type operator<=(const self &rhs) const
Definition: CCuddNavigator.h:136
polybori::CCuddNavigator::pointer_type
DdNode * pointer_type
Cudd's node pointer.
Definition: CCuddNavigator.h:40
polybori::navigator_tag
for iterator_category
Definition: tags.h:60
PBORI_TRACE_FUNC
#define PBORI_TRACE_FUNC(text)
Generate trace function if debugging.
Definition: pbori_defs.h:111
polybori::CAuxTypes::bool_type
bool bool_type
Type for standard true/false statements.
Definition: pbori_defs.h:216
polybori::CCuddNavigator::CCuddNavigator
CCuddNavigator(pointer_type ptr)
Construct from node pointer.
Definition: CCuddNavigator.h:78
polybori::CCuddNavigator::difference_type
std::iterator_traits< pointer_type >::difference_type difference_type
Definition: CCuddNavigator.h:69
Cudd_Ref
#define Cudd_Ref
Definition: prefix_internal.h:157