diff --git a/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.cc b/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.cc index 2753c0950..d62328ff0 100644 --- a/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.cc +++ b/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.cc @@ -5277,14 +5277,14 @@ ABDD::FirstCube( int -NextCube( +ABDD::NextCube( DdGen * gen, int ** cube, - CUDD_VALUE_TYPE * value) + CUDD_VALUE_TYPE * value) const { return Cudd_NextCube(gen, cube, value); -} // NextCube +} // ABDD::NextCube BDD diff --git a/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.hh b/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.hh index 795a7a2ee..d8c2d0722 100644 --- a/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.hh +++ b/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.hh @@ -192,6 +192,7 @@ public: const; int CountLeaves() const; DdGen * FirstCube(int ** cube, CUDD_VALUE_TYPE * value) const; + int NextCube(DdGen * gen, int ** cube, CUDD_VALUE_TYPE * value) const; double Density(int nvars) const; }; // ABDD diff --git a/src/storage/dd/CuddDd.cpp b/src/storage/dd/CuddDd.cpp index c5fb92bbd..313a2b4d8 100644 --- a/src/storage/dd/CuddDd.cpp +++ b/src/storage/dd/CuddDd.cpp @@ -1,3 +1,4 @@ +#include #include #include "src/storage/dd/CuddDd.h" diff --git a/src/storage/dd/CuddDd.h b/src/storage/dd/CuddDd.h index 1942f6504..fa780f263 100644 --- a/src/storage/dd/CuddDd.h +++ b/src/storage/dd/CuddDd.h @@ -20,7 +20,7 @@ namespace storm { template<> class Dd { public: - // Declare the DdManager class as friend so it can access the internals of a DD. + // Declare the DdManager and DdIterator class as friend so it can access the internals of a DD. friend class DdManager; // Instantiate all copy/move constructors/assignments with the default implementation. diff --git a/src/storage/dd/CuddDdForwardIterator.cpp b/src/storage/dd/CuddDdForwardIterator.cpp new file mode 100644 index 000000000..fc66895dd --- /dev/null +++ b/src/storage/dd/CuddDdForwardIterator.cpp @@ -0,0 +1,33 @@ +#include "src/storage/dd/CuddDdForwardIterator.h" + +namespace storm { + namespace dd { + DdForwardIterator::DdForwardIterator(std::shared_ptr> ddManager, ADD cuddAdd) : ddManager(ddManager), value(0), cube(nullptr), cuddAdd(cuddAdd), isAtEnd(false), generator(nullptr) { + // Start by getting the first cube. + this->generator = this->cuddAdd.FirstCube(&cube, &value); + + // If the generator is already empty, we set the corresponding flag. + this->isAtEnd = Cudd_IsGenEmpty(generator); + } + + DdForwardIterator& DdForwardIterator::operator++() { + // TODO: eliminate current + } + + bool DdForwardIterator::operator==(DdForwardIterator const& other) const { + if (this->isAtEnd && other.isAtEnd) { + return true; + } else { + return this->cuddAdd == other.cuddAdd; + } + } + + bool DdForwardIterator::operator!=(DdForwardIterator const& other) const { + return !(*this == other); + } + + storm::expressions::SimpleValuation DdForwardIterator::operator*() const { + // FIXME: construct valuation and return it. + } + } +} \ No newline at end of file diff --git a/src/storage/dd/CuddDdForwardIterator.h b/src/storage/dd/CuddDdForwardIterator.h new file mode 100644 index 000000000..09c627b14 --- /dev/null +++ b/src/storage/dd/CuddDdForwardIterator.h @@ -0,0 +1,46 @@ +#ifndef STORM_STORAGE_DD_CUDDDDFORWARDITERATOR_H_ +#define STORM_STORAGE_DD_CUDDDDFORWARDITERATOR_H_ + +#include +#include + +#include "src/storage/dd/DdForwardIterator.h" +#include "src/storage/expressions/SimpleValuation.h" + +// Include the C++-interface of CUDD. +#include "cuddObj.hh" + +namespace storm { + namespace dd { + template<> + class DdForwardIterator { + public: + // Forward-declare the DdManager class. + template class DdManager; + + DdForwardIterator& operator++(); + storm::expressions::SimpleValuation operator*() const; + bool operator==(DdForwardIterator const& other) const; + bool operator!=(DdForwardIterator const& other) const; + + private: + DdForwardIterator(std::shared_ptr> ddManager, ADD cuddAdd, std::vector const& relevantDdVariables); + + std::shared_ptr> ddManager; + + double value; + + int* cube; + + uint_fast64_t positionInCube; + + ADD cuddAdd; + + bool isAtEnd; + + DdGen* generator; + }; + } +} + +#endif /* STORM_STORAGE_DD_CUDDDDFORWARDITERATOR_H_ */ \ No newline at end of file diff --git a/src/storage/dd/DdForwardIterator.h b/src/storage/dd/DdForwardIterator.h new file mode 100644 index 000000000..2eed23090 --- /dev/null +++ b/src/storage/dd/DdForwardIterator.h @@ -0,0 +1,13 @@ +#ifndef STORM_STORAGE_DD_DDFORWARDITERATOR_H_ +#define STORM_STORAGE_DD_DDFORWARDITERATOR_H_ + +#include "src/storage/dd/DdType.h" + +namespace storm { + namespace dd { + // Declare DdIterator class so we can then specialize it for the different DD types. + template class DdForwardIterator; + } +} + +#endif /* STORM_STORAGE_DD_DDFORWARDITERATOR_H_ */ \ No newline at end of file