From 81944546216678138216fde8af61c10b97d7e656 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 24 Nov 2015 17:55:30 +0100 Subject: [PATCH] more work on making sylvan mtbdds work Former-commit-id: 98454b0ff49e3bdcf02f2759beacdc14c7a015c8 --- resources/3rdparty/sylvan/src/sylvan_mtbdd.c | 83 +++++++++++++++++++ resources/3rdparty/sylvan/src/sylvan_mtbdd.h | 13 +++ resources/3rdparty/sylvan/src/sylvan_obj.cpp | 15 ++++ resources/3rdparty/sylvan/src/sylvan_obj.hpp | 10 +++ src/storage/dd/Add.cpp | 13 ++- src/storage/dd/cudd/InternalCuddAdd.cpp | 2 +- src/storage/dd/cudd/InternalCuddAdd.h | 6 +- src/storage/dd/cudd/InternalCuddBdd.h | 3 +- src/storage/dd/sylvan/InternalSylvanAdd.cpp | 72 +++++++++------- src/storage/dd/sylvan/InternalSylvanAdd.h | 16 +++- src/storage/dd/sylvan/InternalSylvanBdd.h | 9 +- .../dd/sylvan/InternalSylvanDdManager.cpp | 34 ++++++-- .../dd/sylvan/InternalSylvanDdManager.h | 25 +++++- src/storage/dd/sylvan/SylvanAddIterator.h | 6 +- test/functional/storage/SylvanDdTest.cpp | 68 +++++++-------- 15 files changed, 283 insertions(+), 92 deletions(-) diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd.c b/resources/3rdparty/sylvan/src/sylvan_mtbdd.c index ef0c54ba2..9db5da54c 100644 --- a/resources/3rdparty/sylvan/src/sylvan_mtbdd.c +++ b/resources/3rdparty/sylvan/src/sylvan_mtbdd.c @@ -1191,6 +1191,89 @@ TASK_IMPL_2(MTBDD, mtbdd_op_times, MTBDD*, pa, MTBDD*, pb) return mtbdd_invalid; } +/** + * Binary operation Times (for MTBDDs of same type) + * Only for MTBDDs where either all leaves are Double. + * For Integer/Double MTBDD, if either operand is mtbdd_false (not defined), + * then the result is mtbdd_false (i.e. not defined). + */ +TASK_IMPL_2(MTBDD, mtbdd_op_divide, MTBDD*, pa, MTBDD*, pb) +{ + MTBDD a = *pa, b = *pb; +// if (a == mtbdd_false || b == mtbdd_false) return mtbdd_false; + + // Handle Boolean MTBDDs: interpret as And +// if (a == mtbdd_true) return b; +// if (b == mtbdd_true) return a; + + mtbddnode_t na = GETNODE(a); + mtbddnode_t nb = GETNODE(b); + + if (mtbddnode_isleaf(na) && mtbddnode_isleaf(nb)) { +// uint64_t val_a = mtbddnode_getvalue(na); +// uint64_t val_b = mtbddnode_getvalue(nb); +// if (mtbddnode_gettype(na) == 0 && mtbddnode_gettype(nb) == 0) { +// // both uint64_t +// if (val_a == 0) return a; +// else if (val_b == 0) return b; +// else { +// MTBDD result; +// if (val_a == 1) result = b; +// else if (val_b == 1) result = a; +// else result = mtbdd_uint64(val_a*val_b); +// int nega = mtbdd_isnegated(a); +// int negb = mtbdd_isnegated(b); +// if (nega ^ negb) return mtbdd_negate(result); +// else return result; +// } +// } else if (mtbddnode_gettype(na) == 1 && mtbddnode_gettype(nb) == 1) { + if (mtbddnode_gettype(na) == 1 && mtbddnode_gettype(nb) == 1) { + // both double + double vval_a = *(double*)&val_a; + double vval_b = *(double*)&val_b; + if (vval_a == 0.0) return a; + else if (vval_b == 0.0) return b; + else { + MTBDD result; + if (vval_a == 0.0 || vval_b == 1.0) result = a; + + int nega = mtbdd_isnegated(a); + int negb = mtbdd_isnegated(b); + result = mtbdd_double(a / b); + if (nega ^ negb) return mtbdd_negate(result); + else return result; + } + } +// else if (mtbddnode_gettype(na) == 2 && mtbddnode_gettype(nb) == 2) { +// // both fraction +// uint64_t nom_a = val_a>>32; +// uint64_t nom_b = val_b>>32; +// uint64_t denom_a = val_a&0xffffffff; +// uint64_t denom_b = val_b&0xffffffff; +// // multiply! +// uint32_t c = gcd(nom_b, denom_a); +// uint32_t d = gcd(nom_a, denom_b); +// nom_a /= d; +// denom_a /= c; +// nom_a *= (nom_b/c); +// denom_a *= (denom_b/d); +// // compute result +// int nega = mtbdd_isnegated(a); +// int negb = mtbdd_isnegated(b); +// MTBDD result = mtbdd_fraction(nom_a, denom_a); +// if (nega ^ negb) return mtbdd_negate(result); +// else return result; +// } + } + +// if (a < b) { +// *pa = b; +// *pb = a; +// } + + return mtbdd_invalid; +} + /** * Binary operation Minimum (for MTBDDs of same type) * Only for MTBDDs where either all leaves are Boolean, or Integer, or Double. diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd.h b/resources/3rdparty/sylvan/src/sylvan_mtbdd.h index d791d66fb..c0b1a36a5 100644 --- a/resources/3rdparty/sylvan/src/sylvan_mtbdd.h +++ b/resources/3rdparty/sylvan/src/sylvan_mtbdd.h @@ -224,6 +224,14 @@ TASK_DECL_3(MTBDD, mtbdd_abstract_op_plus, MTBDD, MTBDD, int); TASK_DECL_2(MTBDD, mtbdd_op_times, MTBDD*, MTBDD*); TASK_DECL_3(MTBDD, mtbdd_abstract_op_times, MTBDD, MTBDD, int); +/** + * Binary operation Divide (for MTBDDs of same type) + * Only for MTBDDs where all leaves are Double. + * If either operand is mtbdd_false (not defined), + * then the result is mtbdd_false (i.e. not defined). + */ +TASK_DECL_2(MTBDD, mtbdd_op_divide, MTBDD*, MTBDD*); + /** * Binary operation Minimum (for MTBDDs of same type) * Only for MTBDDs where either all leaves are Boolean, or Integer, or Double. @@ -257,6 +265,11 @@ TASK_DECL_3(MTBDD, mtbdd_abstract_op_max, MTBDD, MTBDD, int); */ #define mtbdd_times(a, b) mtbdd_apply(a, b, TASK(mtbdd_op_times)) +/** + * Compute a / b + */ +#define mtbdd_divide(a, b) mtbdd_apply(a, b, TASK(mtbdd_op_divide)) + /** * Compute min(a, b) */ diff --git a/resources/3rdparty/sylvan/src/sylvan_obj.cpp b/resources/3rdparty/sylvan/src/sylvan_obj.cpp index a39edbd56..819882679 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj.cpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj.cpp @@ -724,6 +724,14 @@ Mtbdd::Plus(const Mtbdd &other) const return mtbdd_plus(mtbdd, other.mtbdd); } +Mtbdd +Mtbdd::Minus(const Mtbdd &other) const +{ + LACE_ME; + return mtbdd_minus(mtbdd, other.mtbdd); +} + + Mtbdd Mtbdd::Times(const Mtbdd &other) const { @@ -731,6 +739,13 @@ Mtbdd::Times(const Mtbdd &other) const return mtbdd_times(mtbdd, other.mtbdd); } +Mtbdd +Mtbdd::Divide(const Mtbdd &other) const +{ + LACE_ME; + return mtbdd_divide(mtbdd, other.mtbdd); +} + Mtbdd Mtbdd::Min(const Mtbdd &other) const { diff --git a/resources/3rdparty/sylvan/src/sylvan_obj.hpp b/resources/3rdparty/sylvan/src/sylvan_obj.hpp index 47d12be4f..f0ee1add5 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj.hpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj.hpp @@ -516,11 +516,21 @@ public: */ Mtbdd Plus(const Mtbdd &other) const; + /** + * @brief Computes f - g + */ + Mtbdd Minus(const Mtbdd &other) const; + /** * @brief Computes f * g */ Mtbdd Times(const Mtbdd &other) const; + /** + * @brief Computes f / g + */ + Mtbdd Divide(const Mtbdd &other) const; + /** * @brief Computes min(f, g) */ diff --git a/src/storage/dd/Add.cpp b/src/storage/dd/Add.cpp index 021ca1bd6..3f4841a99 100644 --- a/src/storage/dd/Add.cpp +++ b/src/storage/dd/Add.cpp @@ -287,10 +287,17 @@ namespace storm { template uint_fast64_t Add::getNonZeroCount() const { std::size_t numberOfDdVariables = 0; - for (auto const& metaVariable : this->getContainedMetaVariables()) { - numberOfDdVariables += this->getDdManager()->getMetaVariable(metaVariable).getNumberOfDdVariables(); + if (LibraryType == DdType::CUDD) { + std::size_t numberOfDdVariables = 0; + for (auto const& metaVariable : this->getContainedMetaVariables()) { + numberOfDdVariables += this->getDdManager()->getMetaVariable(metaVariable).getNumberOfDdVariables(); + } + } + Bdd cube; + if (LibraryType == DdType::Sylvan) { + cube = Bdd::getCube(*this->getDdManager(), this->getContainedMetaVariables()); } - return internalAdd.getNonZeroCount(numberOfDdVariables); + return internalAdd.getNonZeroCount(cube, numberOfDdVariables); } template diff --git a/src/storage/dd/cudd/InternalCuddAdd.cpp b/src/storage/dd/cudd/InternalCuddAdd.cpp index aac311481..1a6a65ebc 100644 --- a/src/storage/dd/cudd/InternalCuddAdd.cpp +++ b/src/storage/dd/cudd/InternalCuddAdd.cpp @@ -245,7 +245,7 @@ namespace storm { } template - uint_fast64_t InternalAdd::getNonZeroCount(uint_fast64_t numberOfDdVariables) const { + uint_fast64_t InternalAdd::getNonZeroCount(InternalBdd const& cube, uint_fast64_t numberOfDdVariables) const { return static_cast(this->getCuddAdd().CountMinterm(static_cast(numberOfDdVariables))); } diff --git a/src/storage/dd/cudd/InternalCuddAdd.h b/src/storage/dd/cudd/InternalCuddAdd.h index c62dbe04d..8cd8aa068 100644 --- a/src/storage/dd/cudd/InternalCuddAdd.h +++ b/src/storage/dd/cudd/InternalCuddAdd.h @@ -45,7 +45,6 @@ namespace storm { * * @param ddManager The manager responsible for this DD. * @param cuddAdd The CUDD ADD to store. - * @param containedMetaVariables The meta variables that appear in the DD. */ InternalAdd(InternalDdManager const* ddManager, cudd::ADD cuddAdd); @@ -406,10 +405,11 @@ namespace storm { /*! * Retrieves the number of encodings that are mapped to a non-zero value. * - * @param The number of DD variables contained in this ADD. + * @param cube A cube of variables that is ignored. + * @param numberOfDdVariables The number of DD variables contained in this BDD. * @return The number of encodings that are mapped to a non-zero value. */ - virtual uint_fast64_t getNonZeroCount(uint_fast64_t numberOfDdVariables) const; + uint_fast64_t getNonZeroCount(InternalBdd const& cube, uint_fast64_t numberOfDdVariables) const; /*! * Retrieves the number of leaves of the ADD. diff --git a/src/storage/dd/cudd/InternalCuddBdd.h b/src/storage/dd/cudd/InternalCuddBdd.h index 1bec0aa09..99b78808c 100644 --- a/src/storage/dd/cudd/InternalCuddBdd.h +++ b/src/storage/dd/cudd/InternalCuddBdd.h @@ -28,7 +28,8 @@ namespace storm { template<> class InternalBdd { public: - friend class InternalAdd; + template + friend class InternalAdd; /*! * Creates a DD that encapsulates the given CUDD ADD. diff --git a/src/storage/dd/sylvan/InternalSylvanAdd.cpp b/src/storage/dd/sylvan/InternalSylvanAdd.cpp index e1ec4dcbd..0345be183 100644 --- a/src/storage/dd/sylvan/InternalSylvanAdd.cpp +++ b/src/storage/dd/sylvan/InternalSylvanAdd.cpp @@ -1,18 +1,25 @@ #include "src/storage/dd/sylvan/InternalSylvanAdd.h" +#include "src/storage/dd/sylvan/InternalSylvanDdManager.h" + #include "src/utility/macros.h" #include "src/exceptions/NotImplementedException.h" namespace storm { namespace dd { + template + InternalAdd::InternalAdd(InternalDdManager const* ddManager, sylvan::Mtbdd const& sylvanMtbdd) : ddManager(ddManager), sylvanMtbdd(sylvanMtbdd) { + // Intentionally left empty. + } + template bool InternalAdd::operator==(InternalAdd const& other) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + return this->sylvanMtbdd == other.sylvanMtbdd; } template bool InternalAdd::operator!=(InternalAdd const& other) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + return this->sylvanMtbdd != other.sylvanMtbdd; } template @@ -33,37 +40,39 @@ namespace storm { template InternalAdd& InternalAdd::operator|=(InternalAdd const& other) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); - } template InternalAdd InternalAdd::operator+(InternalAdd const& other) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + return InternalAdd(ddManager, this->sylvanMtbdd.Plus(other.sylvanMtbdd)); } template InternalAdd& InternalAdd::operator+=(InternalAdd const& other) { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + this->sylvanMtbdd = this->sylvanMtbdd.Plus(other.sylvanMtbdd); + return *this; } template InternalAdd InternalAdd::operator*(InternalAdd const& other) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + return InternalAdd(ddManager, this->sylvanMtbdd.Times(other.sylvanMtbdd)); } template InternalAdd& InternalAdd::operator*=(InternalAdd const& other) { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + this->sylvanMtbdd = this->sylvanMtbdd.Times(other.sylvanMtbdd); + return *this; } template InternalAdd InternalAdd::operator-(InternalAdd const& other) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + return InternalAdd(ddManager, this->sylvanMtbdd.Minus(other.sylvanMtbdd)); } template InternalAdd& InternalAdd::operator-=(InternalAdd const& other) { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + this->sylvanMtbdd = this->sylvanMtbdd.Plus(other.sylvanMtbdd.Negate()); + return *this; } template @@ -133,27 +142,27 @@ namespace storm { template InternalAdd InternalAdd::minimum(InternalAdd const& other) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + return InternalAdd(ddManager, this->sylvanMtbdd.Min(other.sylvanMtbdd)); } template InternalAdd InternalAdd::maximum(InternalAdd const& other) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + return InternalAdd(ddManager, this->sylvanMtbdd.Max(other.sylvanMtbdd)); } template InternalAdd InternalAdd::sumAbstract(InternalBdd const& cube) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + return InternalAdd(ddManager, this->sylvanMtbdd.AbstractPlus(static_cast(cube.sylvanBdd.GetBDD()))); } template InternalAdd InternalAdd::minAbstract(InternalBdd const& cube) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + return InternalAdd(ddManager, this->sylvanMtbdd.AbstractMin(static_cast(cube.sylvanBdd.GetBDD()))); } template InternalAdd InternalAdd::maxAbstract(InternalBdd const& cube) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + return InternalAdd(ddManager, this->sylvanMtbdd.AbstractMax(static_cast(cube.sylvanBdd.GetBDD()))); } template @@ -168,27 +177,31 @@ namespace storm { template InternalAdd InternalAdd::multiplyMatrix(InternalAdd const& otherMatrix, std::vector> const& summationDdVariables) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + sylvan::Mtbdd summationVariables = sylvan::Mtbdd::mtbddOne(); + for (auto const& ddVariable : summationDdVariables) { + summationVariables *= ddVariable.sylvanMtbdd; + } + return InternalAdd(ddManager, this->sylvanMtbdd.AndExists(otherMatrix.sylvanMtbdd, summationVariables)); } template InternalBdd InternalAdd::greater(ValueType const& value) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + return InternalBdd(ddManager, this->sylvanMtbdd.BddStrictThreshold(value)); } template InternalBdd InternalAdd::greaterOrEqual(ValueType const& value) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + return InternalBdd(ddManager, this->sylvanMtbdd.BddThreshold(value)); } template InternalBdd InternalAdd::less(ValueType const& value) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + return !this->greaterOrEqual(value); } template InternalBdd InternalAdd::lessOrEqual(ValueType const& value) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + return !this->greater(value); } template @@ -208,12 +221,12 @@ namespace storm { template InternalBdd InternalAdd::getSupport() const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + return InternalBdd(ddManager, sylvan::Bdd(static_cast(this->sylvanMtbdd.Support().GetMTBDD()))); } template - uint_fast64_t InternalAdd::getNonZeroCount(uint_fast64_t numberOfDdVariables) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + uint_fast64_t InternalAdd::getNonZeroCount(InternalBdd const& cube, uint_fast64_t numberOfDdVariables) const { + return static_cast(this->sylvanMtbdd.SatCount(cube.sylvanBdd)); } template @@ -223,7 +236,7 @@ namespace storm { template uint_fast64_t InternalAdd::getNodeCount() const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + return static_cast(this->sylvanMtbdd.NodeCount()) + this->getLeafCount(); } template @@ -243,27 +256,30 @@ namespace storm { template bool InternalAdd::isOne() const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + return *this == ddManager->getAddOne(); } template bool InternalAdd::isZero() const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + return *this == ddManager->getAddZero(); } template bool InternalAdd::isConstant() const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + return this->sylvanMtbdd.isTerminal(); } template uint_fast64_t InternalAdd::getIndex() const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + return static_cast(this->sylvanMtbdd.TopVar()); } template void InternalAdd::exportToDot(std::string const& filename, std::vector const& ddVariableNamesAsStrings) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + // Open the file, dump the DD and close it again. + FILE* filePointer = fopen(filename.c_str() , "w"); + mtbdd_fprintdot(filePointer, this->sylvanMtbdd.GetMTBDD(), nullptr); + fclose(filePointer); } template diff --git a/src/storage/dd/sylvan/InternalSylvanAdd.h b/src/storage/dd/sylvan/InternalSylvanAdd.h index 1889cf6e3..960ee1f01 100644 --- a/src/storage/dd/sylvan/InternalSylvanAdd.h +++ b/src/storage/dd/sylvan/InternalSylvanAdd.h @@ -40,13 +40,21 @@ namespace storm { template class InternalAdd { public: + /*! + * Creates an ADD that encapsulates the given Sylvan MTBDD. + * + * @param ddManager The manager responsible for this DD. + * @param sylvanMtbdd The sylvan MTBDD to store. + */ + InternalAdd(InternalDdManager const* ddManager, sylvan::Mtbdd const& sylvanMtbdd); + // Instantiate all copy/move constructors/assignments with the default implementation. InternalAdd() = default; InternalAdd(InternalAdd const& other) = default; InternalAdd& operator=(InternalAdd const& other) = default; InternalAdd(InternalAdd&& other) = default; InternalAdd& operator=(InternalAdd&& other) = default; - + /*! * Retrieves whether the two DDs represent the same function. * @@ -397,10 +405,11 @@ namespace storm { /*! * Retrieves the number of encodings that are mapped to a non-zero value. * - * @param The number of DD variables contained in this ADD. + * @param cube The cube of variables contained in this BDD. + * @param numberOfDdVariables The number of DD variables contained in this BDD. This is ignored. * @return The number of encodings that are mapped to a non-zero value. */ - virtual uint_fast64_t getNonZeroCount(uint_fast64_t numberOfDdVariables) const; + virtual uint_fast64_t getNonZeroCount(InternalBdd const& cube, uint_fast64_t numberOfDdVariables) const; /*! * Retrieves the number of leaves of the ADD. @@ -574,6 +583,7 @@ namespace storm { private: InternalDdManager const* ddManager; + sylvan::Mtbdd sylvanMtbdd; }; } } diff --git a/src/storage/dd/sylvan/InternalSylvanBdd.h b/src/storage/dd/sylvan/InternalSylvanBdd.h index 4fd653253..9b8a4c28e 100644 --- a/src/storage/dd/sylvan/InternalSylvanBdd.h +++ b/src/storage/dd/sylvan/InternalSylvanBdd.h @@ -1,5 +1,5 @@ -#ifndef STORM_STORAGE_DD_CUDD_INTERNALSYLVANBDD_H_ -#define STORM_STORAGE_DD_CUDD_INTERNALSYLVANBDD_H_ +#ifndef STORM_STORAGE_DD_SYLVAN_INTERNALSYLVANBDD_H_ +#define STORM_STORAGE_DD_SYLVAN_INTERNALSYLVANBDD_H_ #include #include @@ -24,7 +24,8 @@ namespace storm { template<> class InternalBdd { public: - friend class InternalAdd; + template + friend class InternalAdd; InternalBdd(InternalDdManager const* ddManager, sylvan::Bdd const& sylvanBdd); @@ -305,4 +306,4 @@ namespace storm { } } -#endif /* STORM_STORAGE_DD_CUDD_INTERNALSYLVANBDD_H_ */ \ No newline at end of file +#endif /* STORM_STORAGE_DD_SYLVAN_INTERNALSYLVANBDD_H_ */ \ No newline at end of file diff --git a/src/storage/dd/sylvan/InternalSylvanDdManager.cpp b/src/storage/dd/sylvan/InternalSylvanDdManager.cpp index b4da41d8f..93e7511b8 100644 --- a/src/storage/dd/sylvan/InternalSylvanDdManager.cpp +++ b/src/storage/dd/sylvan/InternalSylvanDdManager.cpp @@ -1,5 +1,6 @@ #include "src/storage/dd/sylvan/InternalSylvanDdManager.h" +#include "src/utility/constants.h" #include "src/utility/macros.h" #include "src/exceptions/NotImplementedException.h" #include "src/exceptions/NotSupportedException.h" @@ -33,23 +34,38 @@ namespace storm { return InternalBdd(this, sylvan::Bdd::bddOne()); } - template - InternalAdd InternalDdManager::getAddOne() const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + template<> + InternalAdd InternalDdManager::getAddOne() const { + return InternalAdd(this, sylvan::Mtbdd::doubleTerminal(storm::utility::one())); + } + + template<> + InternalAdd InternalDdManager::getAddOne() const { + return InternalAdd(this, sylvan::Mtbdd::uint64Terminal(storm::utility::one())); } InternalBdd InternalDdManager::getBddZero() const { return InternalBdd(this, sylvan::Bdd::bddZero()); } - template - InternalAdd InternalDdManager::getAddZero() const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + template<> + InternalAdd InternalDdManager::getAddZero() const { + return InternalAdd(this, sylvan::Mtbdd::doubleTerminal(storm::utility::zero())); + } + + template<> + InternalAdd InternalDdManager::getAddZero() const { + return InternalAdd(this, sylvan::Mtbdd::uint64Terminal(storm::utility::zero())); } - template - InternalAdd InternalDdManager::getConstant(ValueType const& value) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + template<> + InternalAdd InternalDdManager::getConstant(double const& value) const { + return InternalAdd(this, sylvan::Mtbdd::doubleTerminal(value)); + } + + template<> + InternalAdd InternalDdManager::getConstant(uint_fast64_t const& value) const { + return InternalAdd(this, sylvan::Mtbdd::uint64Terminal(value)); } std::pair, InternalBdd> InternalDdManager::createNewDdVariablePair() { diff --git a/src/storage/dd/sylvan/InternalSylvanDdManager.h b/src/storage/dd/sylvan/InternalSylvanDdManager.h index 1c2941bf2..55be0581f 100644 --- a/src/storage/dd/sylvan/InternalSylvanDdManager.h +++ b/src/storage/dd/sylvan/InternalSylvanDdManager.h @@ -1,5 +1,5 @@ -#ifndef STORM_STORAGE_DD_INTERNALSYLVANDDMANAGER_H_ -#define STORM_STORAGE_DD_INTERNALSYLVANDDMANAGER_H_ +#ifndef STORM_STORAGE_DD_SYLVAN_INTERNALSYLVANDDMANAGER_H_ +#define STORM_STORAGE_DD_SYLVAN_INTERNALSYLVANDDMANAGER_H_ #include "src/storage/dd/DdType.h" #include "src/storage/dd/InternalDdManager.h" @@ -107,7 +107,26 @@ namespace storm { // manager is implicitly 'global'. static uint_fast64_t nextFreeVariableIndex; }; + + template<> + InternalAdd InternalDdManager::getAddOne() const; + + template<> + InternalAdd InternalDdManager::getAddOne() const; + + template<> + InternalAdd InternalDdManager::getAddZero() const; + + template<> + InternalAdd InternalDdManager::getAddZero() const; + + template<> + InternalAdd InternalDdManager::getConstant(double const& value) const; + + template<> + InternalAdd InternalDdManager::getConstant(uint_fast64_t const& value) const; + } } -#endif /* STORM_STORAGE_DD_INTERNALSYLVANDDMANAGER_H_ */ \ No newline at end of file +#endif /* STORM_STORAGE_DD_SYLVAN_INTERNALSYLVANDDMANAGER_H_ */ \ No newline at end of file diff --git a/src/storage/dd/sylvan/SylvanAddIterator.h b/src/storage/dd/sylvan/SylvanAddIterator.h index 9a79c0384..cbf75076c 100644 --- a/src/storage/dd/sylvan/SylvanAddIterator.h +++ b/src/storage/dd/sylvan/SylvanAddIterator.h @@ -1,5 +1,5 @@ -#ifndef STORM_STORAGE_DD_SYLVANADDITERATOR_H_ -#define STORM_STORAGE_DD_SYLVANADDITERATOR_H_ +#ifndef STORM_STORAGE_DD_SYLVAN_SYLVANADDITERATOR_H_ +#define STORM_STORAGE_DD_SYLVAN_SYLVANADDITERATOR_H_ #include "src/storage/dd/AddIterator.h" #include "src/storage/expressions/SimpleValuation.h" @@ -66,4 +66,4 @@ namespace storm { } } -#endif /* STORM_STORAGE_DD_SYLVANADDITERATOR_H_ */ \ No newline at end of file +#endif /* STORM_STORAGE_DD_SYLVAN_SYLVANADDITERATOR_H_ */ \ No newline at end of file diff --git a/test/functional/storage/SylvanDdTest.cpp b/test/functional/storage/SylvanDdTest.cpp index dc595dbac..4898dbc47 100644 --- a/test/functional/storage/SylvanDdTest.cpp +++ b/test/functional/storage/SylvanDdTest.cpp @@ -102,38 +102,38 @@ TEST(SylvanDd, RangeTest) { // EXPECT_EQ(21ul, identity.getNodeCount()); //} // -//TEST(SylvanDd, OperatorTest) { -// std::shared_ptr> manager(new storm::dd::DdManager()); -// std::pair x = manager->addMetaVariable("x", 1, 9); -// EXPECT_TRUE(manager->template getAddZero() == manager->template getAddZero()); -// EXPECT_FALSE(manager->template getAddZero() == manager->template getAddOne()); -// -// EXPECT_FALSE(manager->template getAddZero() != manager->template getAddZero()); -// EXPECT_TRUE(manager->template getAddZero() != manager->template getAddOne()); -// -// storm::dd::Add dd1 = manager->template getAddOne(); -// storm::dd::Add dd2 = manager->template getAddOne(); -// storm::dd::Add dd3 = dd1 + dd2; -// EXPECT_TRUE(dd3 == manager->template getConstant(2)); -// -// dd3 += manager->template getAddZero(); -// EXPECT_TRUE(dd3 == manager->template getConstant(2)); -// -// dd3 = dd1 * manager->template getConstant(3); -// EXPECT_TRUE(dd3 == manager->template getConstant(3)); -// -// dd3 *= manager->template getConstant(2); -// EXPECT_TRUE(dd3 == manager->template getConstant(6)); -// -// dd3 = dd1 - dd2; -// EXPECT_TRUE(dd3.isZero()); -// -// dd3 -= manager->template getConstant(-2); -// EXPECT_TRUE(dd3 == manager->template getConstant(2)); -// -// dd3 /= manager->template getConstant(2); -// EXPECT_TRUE(dd3.isOne()); -// +TEST(SylvanDd, OperatorTest) { + std::shared_ptr> manager(new storm::dd::DdManager()); + std::pair x = manager->addMetaVariable("x", 1, 9); + EXPECT_TRUE(manager->template getAddZero() == manager->template getAddZero()); + EXPECT_FALSE(manager->template getAddZero() == manager->template getAddOne()); + + EXPECT_FALSE(manager->template getAddZero() != manager->template getAddZero()); + EXPECT_TRUE(manager->template getAddZero() != manager->template getAddOne()); + + storm::dd::Add dd1 = manager->template getAddOne(); + storm::dd::Add dd2 = manager->template getAddOne(); + storm::dd::Add dd3 = dd1 + dd2; + EXPECT_TRUE(dd3 == manager->template getConstant(2)); + + dd3 += manager->template getAddZero(); + EXPECT_TRUE(dd3 == manager->template getConstant(2)); + + dd3 = dd1 * manager->template getConstant(3); + EXPECT_TRUE(dd3 == manager->template getConstant(3)); + + dd3 *= manager->template getConstant(2); + EXPECT_TRUE(dd3 == manager->template getConstant(6)); + + dd3 = dd1 - dd2; + EXPECT_TRUE(dd3.isZero()); + + dd3 -= manager->template getConstant(-2); + EXPECT_TRUE(dd3 == manager->template getConstant(2)); + + dd3 /= manager->template getConstant(2); + EXPECT_TRUE(dd3.isOne()); + // dd3 = !dd3; // EXPECT_TRUE(dd3.isZero()); // @@ -182,8 +182,8 @@ TEST(SylvanDd, RangeTest) { // dd2 = manager->template getConstant(0.01 + 1e-6); // EXPECT_TRUE(dd1.equalModuloPrecision(dd2, 1e-6, false)); // EXPECT_FALSE(dd1.equalModuloPrecision(dd2, 1e-6)); -//} -// +} + //TEST(SylvanDd, AbstractionTest) { // std::shared_ptr> manager(new storm::dd::DdManager()); // std::pair x = manager->addMetaVariable("x", 1, 9);