From d25bd3a32f966cb56e6758124210ccd6a621d31f Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 20 Nov 2015 20:14:41 +0100 Subject: [PATCH] added 'empty' framework for sylvan-based implementation of DD abstraction layer Former-commit-id: c0f781a515574602a67bbac3a9cadf76590ea91a --- src/CMakeLists.txt | 2 + src/storage/dd/Add.cpp | 5 +- src/storage/dd/Add.h | 5 +- src/storage/dd/Bdd.cpp | 12 + src/storage/dd/Bdd.h | 1 + src/storage/dd/Dd.cpp | 1 + src/storage/dd/DdManager.cpp | 27 +- src/storage/dd/DdManager.h | 1 + src/storage/dd/DdMetaVariable.cpp | 1 + src/storage/dd/DdMetaVariable.h | 4 +- src/storage/dd/cudd/CuddAddIterator.h | 6 +- src/storage/dd/cudd/InternalCuddAdd.cpp | 2 +- src/storage/dd/sylvan/InternalSylvanAdd.cpp | 317 ++++++++++ src/storage/dd/sylvan/InternalSylvanAdd.h | 581 ++++++++++++++++++ src/storage/dd/sylvan/InternalSylvanBdd.cpp | 150 +++++ src/storage/dd/sylvan/InternalSylvanBdd.h | 301 +++++++++ .../dd/sylvan/InternalSylvanDdManager.cpp | 61 ++ .../dd/sylvan/InternalSylvanDdManager.h | 101 +++ src/storage/dd/sylvan/SylvanAddIterator.cpp | 36 ++ src/storage/dd/sylvan/SylvanAddIterator.h | 69 +++ 20 files changed, 1669 insertions(+), 14 deletions(-) create mode 100644 src/storage/dd/sylvan/InternalSylvanAdd.cpp create mode 100644 src/storage/dd/sylvan/InternalSylvanAdd.h create mode 100644 src/storage/dd/sylvan/InternalSylvanBdd.cpp create mode 100644 src/storage/dd/sylvan/InternalSylvanBdd.h create mode 100644 src/storage/dd/sylvan/InternalSylvanDdManager.cpp create mode 100644 src/storage/dd/sylvan/InternalSylvanDdManager.h create mode 100644 src/storage/dd/sylvan/SylvanAddIterator.cpp create mode 100644 src/storage/dd/sylvan/SylvanAddIterator.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 496a32f9b..be3b825a0 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -36,6 +36,7 @@ file(GLOB STORM_STORAGE_FILES ${PROJECT_SOURCE_DIR}/src/storage/*.h ${PROJECT_SO file(GLOB STORM_STORAGE_BISIMULATION_FILES ${PROJECT_SOURCE_DIR}/src/storage/bisimulation/*.h ${PROJECT_SOURCE_DIR}/src/storage/bisimulation/*.cpp) file(GLOB STORM_STORAGE_DD_FILES ${PROJECT_SOURCE_DIR}/src/storage/dd/*.h ${PROJECT_SOURCE_DIR}/src/storage/dd/*.cpp) file(GLOB_RECURSE STORM_STORAGE_DD_CUDD_FILES ${PROJECT_SOURCE_DIR}/src/storage/dd/cudd/*.h ${PROJECT_SOURCE_DIR}/src/storage/dd/cudd/*.cpp) +file(GLOB_RECURSE STORM_STORAGE_DD_SYLVAN_FILES ${PROJECT_SOURCE_DIR}/src/storage/dd/sylvan/*.h ${PROJECT_SOURCE_DIR}/src/storage/dd/sylvan/*.cpp) file(GLOB_RECURSE STORM_STORAGE_EXPRESSIONS_FILES ${PROJECT_SOURCE_DIR}/src/storage/expressions/*.h ${PROJECT_SOURCE_DIR}/src/storage/expressions/*.cpp) file(GLOB_RECURSE STORM_STORAGE_PRISM_FILES ${PROJECT_SOURCE_DIR}/src/storage/prism/*.h ${PROJECT_SOURCE_DIR}/src/storage/prism/*.cpp) file(GLOB_RECURSE STORM_STORAGE_SPARSE_FILES ${PROJECT_SOURCE_DIR}/src/storage/sparse/*.h ${PROJECT_SOURCE_DIR}/src/storage/sparse/*.cpp) @@ -82,6 +83,7 @@ source_group(storage FILES ${STORM_STORAGE_FILES}) source_group(storage\\bisimulation FILES ${STORM_STORAGE_BISIMULATION_FILES}) source_group(storage\\dd FILES ${STORM_STORAGE_DD_FILES}) source_group(storage\\dd\\cudd FILES ${STORM_STORAGE_DD_CUDD_FILES}) +source_group(storage\\dd\\sylvan FILES ${STORM_STORAGE_DD_SYLVAN_FILES}) source_group(storage\\expressions FILES ${STORM_STORAGE_EXPRESSIONS_FILES}) source_group(storage\\prism FILES ${STORM_STORAGE_PRISM_FILES}) source_group(storage\\sparse FILES ${STORM_STORAGE_SPARSE_FILES}) diff --git a/src/storage/dd/Add.cpp b/src/storage/dd/Add.cpp index b51aab46c..021ca1bd6 100644 --- a/src/storage/dd/Add.cpp +++ b/src/storage/dd/Add.cpp @@ -768,7 +768,7 @@ namespace storm { template Bdd Add::toBdd() const { - return Bdd(this->getDdManager(), internalAdd.toBdd(), this->getContainedMetaVariables()); + return Bdd(this->getDdManager(), internalAdd.toBdd(), this->getContainedMetaVariables()); } template @@ -783,5 +783,8 @@ namespace storm { template class Add; template class Add; + + template class Add; + template class Add; } } \ No newline at end of file diff --git a/src/storage/dd/Add.h b/src/storage/dd/Add.h index 3aedb86a4..d4e3553b6 100644 --- a/src/storage/dd/Add.h +++ b/src/storage/dd/Add.h @@ -5,10 +5,13 @@ #include "src/storage/dd/Dd.h" #include "src/storage/dd/DdType.h" +#include "src/storage/dd/Odd.h" #include "src/storage/dd/cudd/InternalCuddAdd.h" +#include "src/storage/dd/sylvan/InternalSylvanAdd.h" + #include "src/storage/dd/cudd/CuddAddIterator.h" -#include "src/storage/dd/Odd.h" +#include "src/storage/dd/sylvan/SylvanAddIterator.h" namespace storm { namespace dd { diff --git a/src/storage/dd/Bdd.cpp b/src/storage/dd/Bdd.cpp index 49c736e08..882471d8c 100644 --- a/src/storage/dd/Bdd.cpp +++ b/src/storage/dd/Bdd.cpp @@ -261,5 +261,17 @@ namespace storm { template std::vector Bdd::filterExplicitVector(Odd const& odd, std::vector const& values) const; template std::vector Bdd::filterExplicitVector(Odd const& odd, std::vector const& values) const; + + + template class Bdd; + + template Bdd Bdd::fromVector(std::shared_ptr const> ddManager, std::vector const& values, Odd const& odd, std::set const& metaVariables, std::function const& filter); + template Bdd Bdd::fromVector(std::shared_ptr const> ddManager, std::vector const& values, Odd const& odd, std::set const& metaVariables, std::function const& filter); + + template Add Bdd::toAdd() const; + template Add Bdd::toAdd() const; + + template std::vector Bdd::filterExplicitVector(Odd const& odd, std::vector const& values) const; + template std::vector Bdd::filterExplicitVector(Odd const& odd, std::vector const& values) const; } } \ No newline at end of file diff --git a/src/storage/dd/Bdd.h b/src/storage/dd/Bdd.h index 65cf35f55..85504708c 100644 --- a/src/storage/dd/Bdd.h +++ b/src/storage/dd/Bdd.h @@ -5,6 +5,7 @@ #include "src/storage/dd/DdType.h" #include "src/storage/dd/cudd/InternalCuddBdd.h" +#include "src/storage/dd/sylvan/InternalSylvanBdd.h" namespace storm { namespace logic { diff --git a/src/storage/dd/Dd.cpp b/src/storage/dd/Dd.cpp index 2a806156c..ce477be7d 100644 --- a/src/storage/dd/Dd.cpp +++ b/src/storage/dd/Dd.cpp @@ -85,5 +85,6 @@ namespace storm { } template class Dd; + template class Dd; } } \ No newline at end of file diff --git a/src/storage/dd/DdManager.cpp b/src/storage/dd/DdManager.cpp index 687496629..41295db4b 100644 --- a/src/storage/dd/DdManager.cpp +++ b/src/storage/dd/DdManager.cpp @@ -51,7 +51,7 @@ namespace storm { std::vector> const& ddVariables = metaVariable.getDdVariables(); - Bdd result; + Bdd result; if (value & (1ull << (ddVariables.size() - 1))) { result = ddVariables[0]; } else { @@ -114,8 +114,8 @@ namespace storm { std::vector> variablesPrime; for (std::size_t i = 0; i < numberOfBits; ++i) { auto ddVariablePair = internalDdManager.createNewDdVariablePair(); - variables.emplace_back(Bdd(this->shared_from_this(), ddVariablePair.first, {unprimed})); - variablesPrime.emplace_back(Bdd(this->shared_from_this(), ddVariablePair.second, {primed})); + variables.emplace_back(Bdd(this->shared_from_this(), ddVariablePair.first, {unprimed})); + variablesPrime.emplace_back(Bdd(this->shared_from_this(), ddVariablePair.second, {primed})); } metaVariableMap.emplace(unprimed, DdMetaVariable(name, low, high, variables)); @@ -138,8 +138,8 @@ namespace storm { std::vector> variables; std::vector> variablesPrime; auto ddVariablePair = internalDdManager.createNewDdVariablePair(); - variables.emplace_back(Bdd(this->shared_from_this(), ddVariablePair.first, {unprimed})); - variablesPrime.emplace_back(Bdd(this->shared_from_this(), ddVariablePair.second, {primed})); + variables.emplace_back(Bdd(this->shared_from_this(), ddVariablePair.first, {unprimed})); + variablesPrime.emplace_back(Bdd(this->shared_from_this(), ddVariablePair.second, {primed})); metaVariableMap.emplace(unprimed, DdMetaVariable(name, variables)); metaVariableMap.emplace(primed, DdMetaVariable(name + "'", variablesPrime)); @@ -220,7 +220,7 @@ namespace storm { // First, we initialize a list DD variables and their names. std::vector> variablePairs; for (auto const& variablePair : this->metaVariableMap) { - DdMetaVariable const& metaVariable = variablePair.second; + DdMetaVariable const& metaVariable = variablePair.second; // If the meta variable is of type bool, we don't need to suffix it with the bit number. if (metaVariable.getType() == MetaVariableType::Bool) { variablePairs.emplace_back(metaVariable.getDdVariables().front().getIndex(), variablePair.first); @@ -325,5 +325,20 @@ namespace storm { template Add DdManager::getIdentity(storm::expressions::Variable const& variable) const; template Add DdManager::getIdentity(storm::expressions::Variable const& variable) const; + + + template class DdManager; + + template Add DdManager::getAddZero() const; + template Add DdManager::getAddZero() const; + + template Add DdManager::getAddOne() const; + template Add DdManager::getAddOne() const; + + template Add DdManager::getConstant(double const& value) const; + template Add DdManager::getConstant(uint_fast64_t const& value) const; + + template Add DdManager::getIdentity(storm::expressions::Variable const& variable) const; + template Add DdManager::getIdentity(storm::expressions::Variable const& variable) const; } } \ No newline at end of file diff --git a/src/storage/dd/DdManager.h b/src/storage/dd/DdManager.h index 1c068684e..f882ea57e 100644 --- a/src/storage/dd/DdManager.h +++ b/src/storage/dd/DdManager.h @@ -13,6 +13,7 @@ #include "src/storage/expressions/Variable.h" #include "src/storage/dd/cudd/InternalCuddDdManager.h" +#include "src/storage/dd/sylvan/InternalSylvanDdManager.h" namespace storm { namespace dd { diff --git a/src/storage/dd/DdMetaVariable.cpp b/src/storage/dd/DdMetaVariable.cpp index bffdb480d..16373578d 100644 --- a/src/storage/dd/DdMetaVariable.cpp +++ b/src/storage/dd/DdMetaVariable.cpp @@ -61,5 +61,6 @@ namespace storm { } template class DdMetaVariable; + template class DdMetaVariable; } } \ No newline at end of file diff --git a/src/storage/dd/DdMetaVariable.h b/src/storage/dd/DdMetaVariable.h index c9f426f38..05b037fe3 100644 --- a/src/storage/dd/DdMetaVariable.h +++ b/src/storage/dd/DdMetaVariable.h @@ -118,10 +118,10 @@ namespace storm { int_fast64_t high; // The vector of variables that are used to encode the meta variable. - std::vector> ddVariables; + std::vector> ddVariables; // The cube consisting of all variables that encode the meta variable. - Bdd cube; + Bdd cube; }; } } diff --git a/src/storage/dd/cudd/CuddAddIterator.h b/src/storage/dd/cudd/CuddAddIterator.h index 12b506b8f..615056505 100644 --- a/src/storage/dd/cudd/CuddAddIterator.h +++ b/src/storage/dd/cudd/CuddAddIterator.h @@ -1,5 +1,5 @@ -#ifndef STORM_STORAGE_DD_CUDDAddIterator_H_ -#define STORM_STORAGE_DD_CUDDAddIterator_H_ +#ifndef STORM_STORAGE_DD_CUDDADDITERATOR_H_ +#define STORM_STORAGE_DD_CUDDADDITERATOR_H_ #include #include @@ -136,4 +136,4 @@ namespace storm { } } -#endif /* STORM_STORAGE_DD_CUDDAddIterator_H_ */ \ No newline at end of file +#endif /* STORM_STORAGE_DD_CUDDADDITERATOR_H_ */ \ No newline at end of file diff --git a/src/storage/dd/cudd/InternalCuddAdd.cpp b/src/storage/dd/cudd/InternalCuddAdd.cpp index 15a1706d8..f9bc567b5 100644 --- a/src/storage/dd/cudd/InternalCuddAdd.cpp +++ b/src/storage/dd/cudd/InternalCuddAdd.cpp @@ -179,7 +179,7 @@ namespace storm { } else { return this->getCuddAdd().EqualSupNorm(other.getCuddAdd(), precision); } - }; + } template InternalAdd InternalAdd::swapVariables(std::vector> const& from, std::vector> const& to) const { diff --git a/src/storage/dd/sylvan/InternalSylvanAdd.cpp b/src/storage/dd/sylvan/InternalSylvanAdd.cpp new file mode 100644 index 000000000..e1ec4dcbd --- /dev/null +++ b/src/storage/dd/sylvan/InternalSylvanAdd.cpp @@ -0,0 +1,317 @@ +#include "src/storage/dd/sylvan/InternalSylvanAdd.h" + +#include "src/utility/macros.h" +#include "src/exceptions/NotImplementedException.h" + +namespace storm { + namespace dd { + template + bool InternalAdd::operator==(InternalAdd const& other) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template + bool InternalAdd::operator!=(InternalAdd const& other) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template + InternalAdd InternalAdd::ite(InternalAdd const& thenDd, InternalAdd const& elseDd) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template + InternalAdd InternalAdd::operator!() const { + 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."); + } + + 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."); + } + + 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."); + } + + 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."); + } + + 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."); + } + + template + InternalAdd& InternalAdd::operator/=(InternalAdd const& other) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template + InternalAdd InternalAdd::equals(InternalAdd const& other) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template + InternalAdd InternalAdd::notEquals(InternalAdd const& other) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template + InternalAdd InternalAdd::less(InternalAdd const& other) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template + InternalAdd InternalAdd::lessOrEqual(InternalAdd const& other) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template + InternalAdd InternalAdd::greater(InternalAdd const& other) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template + InternalAdd InternalAdd::greaterOrEqual(InternalAdd const& other) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template + InternalAdd InternalAdd::pow(InternalAdd const& other) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template + InternalAdd InternalAdd::mod(InternalAdd const& other) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template + InternalAdd InternalAdd::logxy(InternalAdd const& other) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template + InternalAdd InternalAdd::floor() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template + InternalAdd InternalAdd::ceil() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template + InternalAdd InternalAdd::minimum(InternalAdd const& other) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template + InternalAdd InternalAdd::maximum(InternalAdd const& other) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template + InternalAdd InternalAdd::sumAbstract(InternalBdd const& cube) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template + InternalAdd InternalAdd::minAbstract(InternalBdd const& cube) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template + InternalAdd InternalAdd::maxAbstract(InternalBdd const& cube) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template + bool InternalAdd::equalModuloPrecision(InternalAdd const& other, double precision, bool relative) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template + InternalAdd InternalAdd::swapVariables(std::vector> const& from, std::vector> const& to) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template + InternalAdd InternalAdd::multiplyMatrix(InternalAdd const& otherMatrix, std::vector> const& summationDdVariables) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template + InternalBdd InternalAdd::greater(ValueType const& value) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template + InternalBdd InternalAdd::greaterOrEqual(ValueType const& value) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template + InternalBdd InternalAdd::less(ValueType const& value) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template + InternalBdd InternalAdd::lessOrEqual(ValueType const& value) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template + InternalBdd InternalAdd::notZero() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template + InternalAdd InternalAdd::constrain(InternalAdd const& constraint) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template + InternalAdd InternalAdd::restrict(InternalAdd const& constraint) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template + InternalBdd InternalAdd::getSupport() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template + uint_fast64_t InternalAdd::getNonZeroCount(uint_fast64_t numberOfDdVariables) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template + uint_fast64_t InternalAdd::getLeafCount() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template + uint_fast64_t InternalAdd::getNodeCount() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template + ValueType InternalAdd::getMin() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template + ValueType InternalAdd::getMax() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template + InternalBdd InternalAdd::toBdd() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template + bool InternalAdd::isOne() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template + bool InternalAdd::isZero() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template + bool InternalAdd::isConstant() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template + uint_fast64_t InternalAdd::getIndex() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template + void InternalAdd::exportToDot(std::string const& filename, std::vector const& ddVariableNamesAsStrings) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template + AddIterator InternalAdd::begin(std::shared_ptr const> fullDdManager, std::set const& metaVariables, bool enumerateDontCareMetaVariables) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template + AddIterator InternalAdd::end(std::shared_ptr const> fullDdManager, bool enumerateDontCareMetaVariables) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template + Odd InternalAdd::createOdd(std::vector const& ddVariableIndices) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template + void InternalAdd::composeWithExplicitVector(storm::dd::Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector, std::function const& function) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template + void InternalAdd::composeWithExplicitVector(storm::dd::Odd const& odd, std::vector const& ddVariableIndices, std::vector const& offsets, std::vector& targetVector, std::function const& function) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template + std::vector> InternalAdd::splitIntoGroups(std::vector const& ddGroupVariableIndices) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template + std::vector, InternalAdd>> InternalAdd::splitIntoGroups(InternalAdd vector, std::vector const& ddGroupVariableIndices) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template + void InternalAdd::toMatrixComponents(std::vector const& rowGroupIndices, std::vector& rowIndications, std::vector>& columnsAndValues, Odd const& rowOdd, Odd const& columnOdd, std::vector const& ddRowVariableIndices, std::vector const& ddColumnVariableIndices, bool writeValues) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template + InternalAdd InternalAdd::fromVector(InternalDdManager const* ddManager, std::vector const& values, storm::dd::Odd const& odd, std::vector const& ddVariableIndices) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template class InternalAdd; + template class InternalAdd; + } +} \ No newline at end of file diff --git a/src/storage/dd/sylvan/InternalSylvanAdd.h b/src/storage/dd/sylvan/InternalSylvanAdd.h new file mode 100644 index 000000000..1889cf6e3 --- /dev/null +++ b/src/storage/dd/sylvan/InternalSylvanAdd.h @@ -0,0 +1,581 @@ +#ifndef STORM_STORAGE_DD_CUDD_INTERNALSYLVANADD_H_ +#define STORM_STORAGE_DD_CUDD_INTERNALSYLVANADD_H_ + +#include +#include + +#include "src/storage/dd/DdType.h" +#include "src/storage/dd/InternalAdd.h" +#include "src/storage/dd/Odd.h" + +#include "src/storage/dd/sylvan/InternalSylvanBdd.h" +#include "src/storage/dd/sylvan/SylvanAddIterator.h" + +#include "src/storage/expressions/Variable.h" + +namespace storm { + namespace storage { + template + class SparseMatrix; + + class BitVector; + + template + class MatrixEntry; + } + + namespace dd { + template + class DdManager; + + template + class InternalDdManager; + + template + class InternalBdd; + + template + class AddIterator; + + template + class InternalAdd { + public: + // 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. + * + * @param other The DD that is to be compared with the current one. + * @return True if the DDs represent the same function. + */ + bool operator==(InternalAdd const& other) const; + + /*! + * Retrieves whether the two DDs represent different functions. + * + * @param other The DD that is to be compared with the current one. + * @return True if the DDs represent the different functions. + */ + bool operator!=(InternalAdd const& other) const; + + /*! + * Performs an if-then-else with the given operands, i.e. maps all valuations that are mapped to a non-zero + * function value to the function values specified by the first DD and all others to the function values + * specified by the second DD. + * + * @param thenDd The ADD specifying the 'then' part. + * @param elseDd The ADD specifying the 'else' part. + * @return The ADD corresponding to the if-then-else of the operands. + */ + InternalAdd ite(InternalAdd const& thenAdd, InternalAdd const& elseAdd) const; + + /*! + * Logically inverts the current ADD. That is, all inputs yielding non-zero values will be mapped to zero in + * the result and vice versa. + * + * @return The resulting ADD. + */ + InternalAdd operator!() const; + + /*! + * Performs a logical or of the current and the given ADD. As a prerequisite, the operand ADDs need to be + * 0/1 ADDs. + * + * @param other The second ADD used for the operation. + * @return The logical or of the operands. + */ + InternalAdd operator||(InternalAdd const& other) const; + + /*! + * Performs a logical or of the current and the given ADD and assigns it to the current ADD. As a + * prerequisite, the operand ADDs need to be 0/1 ADDs. + * + * @param other The second ADD used for the operation. + * @return A reference to the current ADD after the operation + */ + InternalAdd& operator|=(InternalAdd const& other); + + /*! + * Adds the two ADDs. + * + * @param other The ADD to add to the current one. + * @return The result of the addition. + */ + InternalAdd operator+(InternalAdd const& other) const; + + /*! + * Adds the given ADD to the current one. + * + * @param other The ADD to add to the current one. + * @return A reference to the current ADD after the operation. + */ + InternalAdd& operator+=(InternalAdd const& other); + + /*! + * Multiplies the two ADDs. + * + * @param other The ADD to multiply with the current one. + * @return The result of the multiplication. + */ + InternalAdd operator*(InternalAdd const& other) const; + + /*! + * Multiplies the given ADD with the current one and assigns the result to the current ADD. + * + * @param other The ADD to multiply with the current one. + * @return A reference to the current ADD after the operation. + */ + InternalAdd& operator*=(InternalAdd const& other); + + /*! + * Subtracts the given ADD from the current one. + * + * @param other The ADD to subtract from the current one. + * @return The result of the subtraction. + */ + InternalAdd operator-(InternalAdd const& other) const; + + /*! + * Subtracts the given ADD from the current one and assigns the result to the current ADD. + * + * @param other The ADD to subtract from the current one. + * @return A reference to the current ADD after the operation. + */ + InternalAdd& operator-=(InternalAdd const& other); + + /*! + * Divides the current ADD by the given one. + * + * @param other The ADD by which to divide the current one. + * @return The result of the division. + */ + InternalAdd operator/(InternalAdd const& other) const; + + /*! + * Divides the current ADD by the given one and assigns the result to the current ADD. + * + * @param other The ADD by which to divide the current one. + * @return A reference to the current ADD after the operation. + */ + InternalAdd& operator/=(InternalAdd const& other); + + /*! + * Retrieves the function that maps all evaluations to one that have identical function values. + * + * @param other The ADD with which to perform the operation. + * @return The resulting function represented as an ADD. + */ + InternalAdd equals(InternalAdd const& other) const; + + /*! + * Retrieves the function that maps all evaluations to one that have distinct function values. + * + * @param other The ADD with which to perform the operation. + * @return The resulting function represented as an ADD. + */ + InternalAdd notEquals(InternalAdd const& other) const; + + /*! + * Retrieves the function that maps all evaluations to one whose function value in the first ADD are less + * than the one in the given ADD. + * + * @param other The ADD with which to perform the operation. + * @return The resulting function represented as an ADD. + */ + InternalAdd less(InternalAdd const& other) const; + + /*! + * Retrieves the function that maps all evaluations to one whose function value in the first ADD are less or + * equal than the one in the given ADD. + * + * @param other The DD with which to perform the operation. + * @return The resulting function represented as an ADD. + */ + InternalAdd lessOrEqual(InternalAdd const& other) const; + + /*! + * Retrieves the function that maps all evaluations to one whose function value in the first ADD are greater + * than the one in the given ADD. + * + * @param other The ADD with which to perform the operation. + * @return The resulting function represented as an ADD. + */ + InternalAdd greater(InternalAdd const& other) const; + + /*! + * Retrieves the function that maps all evaluations to one whose function value in the first ADD are greater + * or equal than the one in the given ADD. + * + * @param other The ADD with which to perform the operation. + * @return The resulting function represented as an ADD. + */ + InternalAdd greaterOrEqual(InternalAdd const& other) const; + + /*! + * Retrieves the function that represents the current ADD to the power of the given ADD. + * + * @other The exponent function (given as an ADD). + * @retur The resulting ADD. + */ + InternalAdd pow(InternalAdd const& other) const; + + /*! + * Retrieves the function that represents the current ADD modulo the given ADD. + * + * @other The modul function (given as an ADD). + * @retur The resulting ADD. + */ + InternalAdd mod(InternalAdd const& other) const; + + /*! + * Retrieves the function that represents the logarithm of the current ADD to the bases given by the second + * ADD. + * + * @other The base function (given as an ADD). + * @retur The resulting ADD. + */ + InternalAdd logxy(InternalAdd const& other) const; + + /*! + * Retrieves the function that floors all values in the current ADD. + * + * @retur The resulting ADD. + */ + InternalAdd floor() const; + + /*! + * Retrieves the function that ceils all values in the current ADD. + * + * @retur The resulting ADD. + */ + InternalAdd ceil() const; + + /*! + * Retrieves the function that maps all evaluations to the minimum of the function values of the two ADDs. + * + * @param other The ADD with which to perform the operation. + * @return The resulting function represented as an ADD. + */ + InternalAdd minimum(InternalAdd const& other) const; + + /*! + * Retrieves the function that maps all evaluations to the maximum of the function values of the two ADDs. + * + * @param other The ADD with which to perform the operation. + * @return The resulting function represented as an ADD. + */ + InternalAdd maximum(InternalAdd const& other) const; + + /*! + * Sum-abstracts from the given cube. + * + * @param cube The cube from which to abstract. + */ + InternalAdd sumAbstract(InternalBdd const& cube) const; + + /*! + * Min-abstracts from the given cube. + * + * @param cube The cube from which to abstract. + */ + InternalAdd minAbstract(InternalBdd const& cube) const; + + /*! + * Max-abstracts from the given cube. + * + * @param cube The cube from which to abstract. + */ + InternalAdd maxAbstract(InternalBdd const& cube) const; + + /*! + * Checks whether the current and the given ADD represent the same function modulo some given precision. + * + * @param other The ADD with which to compare. + * @param precision An upper bound on the maximal difference between any two function values that is to be + * tolerated. + * @param relative If set to true, not the absolute values have to be within the precision, but the relative + * values. + */ + bool equalModuloPrecision(InternalAdd const& other, double precision, bool relative = true) const; + + /*! + * Swaps the given pairs of DD variables in the ADD. The pairs of meta variables have to be represented by + * ADDs must have equal length. + * + * @param from The vector that specifies the 'from' part of the variable renaming. + * @param to The vector that specifies the 'to' part of the variable renaming. + * @return The resulting ADD. + */ + InternalAdd swapVariables(std::vector> const& from, std::vector> const& to) const; + + /*! + * Multiplies the current ADD (representing a matrix) with the given matrix by summing over the given meta + * variables. + * + * @param otherMatrix The matrix with which to multiply. + * @param summationDdVariables The DD variables (represented as ADDs) over which to sum. + * @return An ADD representing the result of the matrix-matrix multiplication. + */ + InternalAdd multiplyMatrix(InternalAdd const& otherMatrix, std::vector> const& summationDdVariables) const; + + /*! + * Computes a BDD that represents the function in which all assignments with a function value strictly + * larger than the given value are mapped to one and all others to zero. + * + * @param value The value used for the comparison. + * @return The resulting BDD. + */ + InternalBdd greater(ValueType const& value) const; + + /*! + * Computes a BDD that represents the function in which all assignments with a function value larger or equal + * to the given value are mapped to one and all others to zero. + * + * @param value The value used for the comparison. + * @return The resulting BDD. + */ + InternalBdd greaterOrEqual(ValueType const& value) const; + + /*! + * Computes a BDD that represents the function in which all assignments with a function value strictly + * lower than the given value are mapped to one and all others to zero. + * + * @param value The value used for the comparison. + * @return The resulting BDD. + */ + InternalBdd less(ValueType const& value) const; + + /*! + * Computes a BDD that represents the function in which all assignments with a function value less or equal + * to the given value are mapped to one and all others to zero. + * + * @param value The value used for the comparison. + * @return The resulting BDD. + */ + InternalBdd lessOrEqual(ValueType const& value) const; + + /*! + * Computes a BDD that represents the function in which all assignments with a function value unequal to + * zero are mapped to one and all others to zero. + * + * @return The resulting DD. + */ + InternalBdd notZero() const; + + /*! + * Computes the constraint of the current ADD with the given constraint. That is, the function value of the + * resulting ADD will be the same as the current ones for all assignments mapping to one in the constraint + * and may be different otherwise. + * + * @param constraint The constraint to use for the operation. + * @return The resulting ADD. + */ + InternalAdd constrain(InternalAdd const& constraint) const; + + /*! + * Computes the restriction of the current ADD with the given constraint. That is, the function value of the + * resulting DD will be the same as the current ones for all assignments mapping to one in the constraint + * and may be different otherwise. + * + * @param constraint The constraint to use for the operation. + * @return The resulting ADD. + */ + InternalAdd restrict(InternalAdd const& constraint) const; + + /*! + * Retrieves the support of the current ADD. + * + * @return The support represented as a BDD. + */ + InternalBdd getSupport() const; + + /*! + * Retrieves the number of encodings that are mapped to a non-zero value. + * + * @param The number of DD variables contained in this ADD. + * @return The number of encodings that are mapped to a non-zero value. + */ + virtual uint_fast64_t getNonZeroCount(uint_fast64_t numberOfDdVariables) const; + + /*! + * Retrieves the number of leaves of the ADD. + * + * @return The number of leaves of the ADD. + */ + virtual uint_fast64_t getLeafCount() const; + + /*! + * Retrieves the number of nodes necessary to represent the DD. + * + * @return The number of nodes in this DD. + */ + virtual uint_fast64_t getNodeCount() const; + + /*! + * Retrieves the lowest function value of any encoding. + * + * @return The lowest function value of any encoding. + */ + ValueType getMin() const; + + /*! + * Retrieves the highest function value of any encoding. + * + * @return The highest function value of any encoding. + */ + ValueType getMax() const; + + /*! + * Converts the ADD to a BDD by mapping all values unequal to zero to 1. This effectively does the same as + * a call to notZero(). + * + * @return The corresponding BDD. + */ + InternalBdd toBdd() const; + + /*! + * Retrieves whether this ADD represents the constant one function. + * + * @return True if this ADD represents the constant one function. + */ + bool isOne() const; + + /*! + * Retrieves whether this ADD represents the constant zero function. + * + * @return True if this ADD represents the constant zero function. + */ + bool isZero() const; + + /*! + * Retrieves whether this ADD represents a constant function. + * + * @return True if this ADD represents a constants function. + */ + bool isConstant() const; + + /*! + * Retrieves the index of the topmost variable in the DD. + * + * @return The index of the topmost variable in DD. + */ + virtual uint_fast64_t getIndex() const; + + /*! + * Exports the DD to the given file in the dot format. + * + * @param filename The name of the file to which the DD is to be exported. + * @param ddVariableNamesAsString The names of the DD variables to display in the dot file. + */ + void exportToDot(std::string const& filename, std::vector const& ddVariableNamesAsStrings) const; + + /*! + * Retrieves an iterator that points to the first meta variable assignment with a non-zero function value. + * + * @param fullDdManager The DD manager responsible for this ADD. + * @param metaVariables The meta variables contained in the ADD. + * @param enumerateDontCareMetaVariables If set to true, all meta variable assignments are enumerated, even + * if a meta variable does not at all influence the the function value. + * @return An iterator that points to the first meta variable assignment with a non-zero function value. + */ + AddIterator begin(std::shared_ptr const> fullDdManager, std::set const& metaVariables, bool enumerateDontCareMetaVariables = true) const; + + /*! + * Retrieves an iterator that points past the end of the container. + * + * @param fullDdManager The DD manager responsible for this ADD. + * @param enumerateDontCareMetaVariables If set to true, all meta variable assignments are enumerated, even + * if a meta variable does not at all influence the the function value. + * @return An iterator that points past the end of the container. + */ + AddIterator end(std::shared_ptr const> fullDdManager, bool enumerateDontCareMetaVariables = true) const; + + /*! + * Composes the ADD with an explicit vector by performing a specified function between the entries of this + * ADD and the explicit vector. + * + * @param odd The ODD to use for the translation from symbolic to explicit positions. + * @param ddVariableIndices The indices of the DD variables present in this ADD. + * @param targetVector The explicit vector that is to be composed with the ADD. The results are written to + * this vector again. + * @param function The function to perform in the composition. + */ + void composeWithExplicitVector(Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector, std::function const& function) const; + + /*! + * Composes the (row-grouped) ADD with an explicit vector by performing a specified function between the + * entries of this ADD and the explicit vector. + * + * @param odd The ODD to use for the translation from symbolic to explicit positions. + * @param ddVariableIndices The indices of the DD variables present in this ADD. + * @param offsets The offsets + * @param targetVector The explicit vector that is to be composed with the ADD. The results are written to + * this vector again. + * @param function The function to perform in the composition. + */ + void composeWithExplicitVector(Odd const& odd, std::vector const& ddVariableIndices, std::vector const& offsets, std::vector& targetVector, std::function const& function) const; + + /*! + * Splits the ADD into several ADDs that differ in the encoding of the given group variables (given via indices). + * + * @param ddGroupVariableIndices The indices of the variables that are used to distinguish the groups. + * @return A vector of ADDs that are the separate groups (wrt. to the encoding of the given variables). + */ + std::vector> splitIntoGroups(std::vector const& ddGroupVariableIndices) const; + + /*! + * Simultaneously splits the ADD and the given vector ADD into several ADDs that differ in the encoding of + * the given group variables (given via indices). + * + * @param vector The vector to split (in addition to the current ADD). + * @param ddGroupVariableIndices The indices of the variables that are used to distinguish the groups. + * @return A vector of pairs of ADDs that are the separate groups of the current ADD and the vector, + * respectively (wrt. to the encoding of the given variables). + */ + std::vector, InternalAdd>> splitIntoGroups(InternalAdd vector, std::vector const& ddGroupVariableIndices) const; + + /*! + * Translates the ADD into the components needed for constructing a matrix. + * + * @param rowGroupIndices The row group indices. + * @param rowIndications The vector that is to be filled with the row indications. + * @param columnsAndValues The vector that is to be filled with the non-zero entries of the matrix. + * @param rowOdd The ODD used for translating the rows. + * @param columnOdd The ODD used for translating the columns. + * @param ddRowVariableIndices The variable indices of the row variables. + * @param ddColumnVariableIndices The variable indices of the column variables. + * @param writeValues A flag that indicates whether or not to write to the entry vector. If this is not set, + * only the row indications are modified. + */ + void toMatrixComponents(std::vector const& rowGroupIndices, std::vector& rowIndications, std::vector>& columnsAndValues, Odd const& rowOdd, Odd const& columnOdd, std::vector const& ddRowVariableIndices, std::vector const& ddColumnVariableIndices, bool writeValues) const; + + /*! + * Creates an ADD from the given explicit vector. + * + * @param ddManager The manager to use to built the ADD. + * @param values The explicit vector to encode. + * @param odd The ODD to use for the translation. + * @param ddVariableIndices The indices of the variables to use in the ADD. + */ + static InternalAdd fromVector(InternalDdManager const* ddManager, std::vector const& values, storm::dd::Odd const& odd, std::vector const& ddVariableIndices); + + /*! + * Creates an ODD based on the current ADD. + * + * @return The corresponding ODD. + */ + Odd createOdd(std::vector const& ddVariableIndices) const; + + private: + InternalDdManager const* ddManager; + + }; + } +} + +#endif /* STORM_STORAGE_DD_CUDD_INTERNALSYLVANADD_H_ */ \ No newline at end of file diff --git a/src/storage/dd/sylvan/InternalSylvanBdd.cpp b/src/storage/dd/sylvan/InternalSylvanBdd.cpp new file mode 100644 index 000000000..bc2444273 --- /dev/null +++ b/src/storage/dd/sylvan/InternalSylvanBdd.cpp @@ -0,0 +1,150 @@ +#include "src/storage/dd/sylvan/InternalSylvanBdd.h" + +#include "src/storage/dd/sylvan/InternalSylvanAdd.h" +#include "src/storage/dd/sylvan/SylvanAddIterator.h" +# + +#include "src/storage/BitVector.h" + +#include "src/utility/macros.h" +#include "src/exceptions/NotImplementedException.h" + +namespace storm { + namespace dd { + template + InternalBdd InternalBdd::fromVector(InternalDdManager const* ddManager, std::vector const& values, Odd const& odd, std::vector const& sortedDdVariableIndices, std::function const& filter) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + bool InternalBdd::operator==(InternalBdd const& other) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + bool InternalBdd::operator!=(InternalBdd const& other) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + InternalBdd InternalBdd::ite(InternalBdd const& thenDd, InternalBdd const& elseDd) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + InternalBdd InternalBdd::operator||(InternalBdd const& other) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + InternalBdd& InternalBdd::operator|=(InternalBdd const& other) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + InternalBdd InternalBdd::operator&&(InternalBdd const& other) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + InternalBdd& InternalBdd::operator&=(InternalBdd const& other) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + InternalBdd InternalBdd::iff(InternalBdd const& other) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + InternalBdd InternalBdd::exclusiveOr(InternalBdd const& other) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + InternalBdd InternalBdd::implies(InternalBdd const& other) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + InternalBdd InternalBdd::operator!() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + InternalBdd& InternalBdd::complement() { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + InternalBdd InternalBdd::existsAbstract(InternalBdd const& cube) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + InternalBdd InternalBdd::universalAbstract(InternalBdd const& cube) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + InternalBdd InternalBdd::andExists(InternalBdd const& other, InternalBdd const& cube) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + InternalBdd InternalBdd::constrain(InternalBdd const& constraint) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + InternalBdd InternalBdd::restrict(InternalBdd const& constraint) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + InternalBdd InternalBdd::swapVariables(std::vector> const& from, std::vector> const& to) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + InternalBdd InternalBdd::getSupport() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + uint_fast64_t InternalBdd::getNonZeroCount(uint_fast64_t numberOfDdVariables) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + uint_fast64_t InternalBdd::getLeafCount() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + uint_fast64_t InternalBdd::getNodeCount() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + bool InternalBdd::isOne() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + bool InternalBdd::isZero() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + uint_fast64_t InternalBdd::getIndex() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + void InternalBdd::exportToDot(std::string const& filename, std::vector const& ddVariableNamesAsStrings) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template + InternalAdd InternalBdd::toAdd() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + storm::storage::BitVector InternalBdd::toVector(storm::dd::Odd const& rowOdd, std::vector const& ddVariableIndices) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + Odd InternalBdd::createOdd(std::vector const& ddVariableIndices) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template + void InternalBdd::filterExplicitVector(Odd const& odd, std::vector const& ddVariableIndices, std::vector const& sourceValues, std::vector& targetValues) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template InternalBdd InternalBdd::fromVector(InternalDdManager const* ddManager, std::vector const& values, Odd const& odd, std::vector const& sortedDdVariableIndices, std::function const& filter); + template InternalBdd InternalBdd::fromVector(InternalDdManager const* ddManager, std::vector const& values, Odd const& odd, std::vector const& sortedDdVariableIndices, std::function const& filter); + + template InternalAdd InternalBdd::toAdd() const; + template InternalAdd InternalBdd::toAdd() const; + + template void InternalBdd::filterExplicitVector(Odd const& odd, std::vector const& ddVariableIndices, std::vector const& sourceValues, std::vector& targetValues) const; + template void InternalBdd::filterExplicitVector(Odd const& odd, std::vector const& ddVariableIndices, std::vector const& sourceValues, std::vector& targetValues) const; + } +} \ No newline at end of file diff --git a/src/storage/dd/sylvan/InternalSylvanBdd.h b/src/storage/dd/sylvan/InternalSylvanBdd.h new file mode 100644 index 000000000..bacc4efca --- /dev/null +++ b/src/storage/dd/sylvan/InternalSylvanBdd.h @@ -0,0 +1,301 @@ +#ifndef STORM_STORAGE_DD_CUDD_INTERNALSYLVANBDD_H_ +#define STORM_STORAGE_DD_CUDD_INTERNALSYLVANBDD_H_ + +#include +#include + +#include "src/storage/dd/DdType.h" +#include "src/storage/dd/InternalBdd.h" +#include "src/storage/dd/InternalAdd.h" + +namespace storm { + namespace storage { + class BitVector; + } + + namespace dd { + template + class InternalDdManager; + + template + class InternalAdd; + + class Odd; + + template<> + class InternalBdd { + public: + friend class InternalAdd; + + // Instantiate all copy/move constructors/assignments with the default implementation. + InternalBdd() = default; + InternalBdd(InternalBdd const& other) = default; + InternalBdd& operator=(InternalBdd const& other) = default; + InternalBdd(InternalBdd&& other) = default; + InternalBdd& operator=(InternalBdd&& other) = default; + + /*! + * Builds a BDD representing the values that make the given filter function evaluate to true. + * + * @param ddManager The manager responsible for the BDD. + * @param values The values that are to be checked against the filter function. + * @param odd The ODD used for the translation. + * @param metaVariables The meta variables used for the translation. + * @param filter The filter that evaluates whether an encoding is to be mapped to 0 or 1. + * @return The resulting BDD. + */ + template + static InternalBdd fromVector(InternalDdManager const* ddManager, std::vector const& values, Odd const& odd, std::vector const& sortedDdVariableIndices, std::function const& filter); + + /*! + * Retrieves whether the two BDDs represent the same function. + * + * @param other The BDD that is to be compared with the current one. + * @return True if the BDDs represent the same function. + */ + bool operator==(InternalBdd const& other) const; + + /*! + * Retrieves whether the two BDDs represent different functions. + * + * @param other The BDD that is to be compared with the current one. + * @return True if the BDDs represent the different functions. + */ + bool operator!=(InternalBdd const& other) const; + + /*! + * Performs an if-then-else with the given operands, i.e. maps all valuations that are mapped to a non-zero + * function value to the function values specified by the first DD and all others to the function values + * specified by the second DD. + * + * @param thenBdd The BDD defining the 'then' part. + * @param elseBdd The BDD defining the 'else' part. + * @return The resulting BDD. + */ + InternalBdd ite(InternalBdd const& thenBdd, InternalBdd const& elseBdd) const; + + /*! + * Performs a logical or of the current and the given BDD. + * + * @param other The second BDD used for the operation. + * @return The logical or of the operands. + */ + InternalBdd operator||(InternalBdd const& other) const; + + /*! + * Performs a logical or of the current and the given BDD and assigns it to the current BDD. + * + * @param other The second BDD used for the operation. + * @return A reference to the current BDD after the operation + */ + InternalBdd& operator|=(InternalBdd const& other); + + /*! + * Performs a logical and of the current and the given BDD. + * + * @param other The second BDD used for the operation. + * @return The logical and of the operands. + */ + InternalBdd operator&&(InternalBdd const& other) const; + + /*! + * Performs a logical and of the current and the given BDD and assigns it to the current BDD. + * + * @param other The second BDD used for the operation. + * @return A reference to the current BDD after the operation + */ + InternalBdd& operator&=(InternalBdd const& other); + + /*! + * Performs a logical iff of the current and the given BDD. + * + * @param other The second BDD used for the operation. + * @return The logical iff of the operands. + */ + InternalBdd iff(InternalBdd const& other) const; + + /*! + * Performs a logical exclusive-or of the current and the given BDD. + * + * @param other The second BDD used for the operation. + * @return The logical exclusive-or of the operands. + */ + InternalBdd exclusiveOr(InternalBdd const& other) const; + + /*! + * Performs a logical implication of the current and the given BDD. + * + * @param other The second BDD used for the operation. + * @return The logical implication of the operands. + */ + InternalBdd implies(InternalBdd const& other) const; + + /*! + * Logically inverts the current BDD. + * + * @return The resulting BDD. + */ + InternalBdd operator!() const; + + /*! + * Logically complements the current BDD. + * + * @return A reference to the current BDD after the operation. + */ + InternalBdd& complement(); + + /*! + * Existentially abstracts from the given cube. + * + * @param cube The cube from which to abstract. + */ + InternalBdd existsAbstract(InternalBdd const& cube) const; + + /*! + * Universally abstracts from the given cube. + * + * @param cube The cube from which to abstract. + */ + InternalBdd universalAbstract(InternalBdd const& cube) const; + + /*! + * Swaps the given pairs of DD variables in the BDD. The pairs of meta variables have to be represented by + * BDDs must have equal length. + * + * @param from The vector that specifies the 'from' part of the variable renaming. + * @param to The vector that specifies the 'to' part of the variable renaming. + * @return The resulting BDD. + */ + InternalBdd swapVariables(std::vector> const& from, std::vector> const& to) const; + + /*! + * Computes the logical and of the current and the given BDD and existentially abstracts from the given cube. + * + * @param other The second BDD for the logical and. + * @param cube The cube to existentially abstract. + * @return A BDD representing the result. + */ + InternalBdd andExists(InternalBdd const& other, InternalBdd const& cube) const; + + /*! + * Computes the constraint of the current BDD with the given constraint. That is, the function value of the + * resulting BDD will be the same as the current ones for all assignments mapping to one in the constraint + * and may be different otherwise. + * + * @param constraint The constraint to use for the operation. + * @return The resulting BDD. + */ + InternalBdd constrain(InternalBdd const& constraint) const; + + /*! + * Computes the restriction of the current BDD with the given constraint. That is, the function value of the + * resulting DD will be the same as the current ones for all assignments mapping to one in the constraint + * and may be different otherwise. + * + * @param constraint The constraint to use for the operation. + * @return The resulting BDD. + */ + InternalBdd restrict(InternalBdd const& constraint) const; + + /*! + * Retrieves the support of the current BDD. + * + * @return The support represented as a BDD. + */ + InternalBdd getSupport() const; + + /*! + * Retrieves the number of encodings that are mapped to a non-zero value. + * + * @param The number of DD variables contained in this BDD. + * @return The number of encodings that are mapped to a non-zero value. + */ + uint_fast64_t getNonZeroCount(uint_fast64_t numberOfDdVariables) const; + + /*! + * Retrieves the number of leaves of the DD. + * + * @return The number of leaves of the DD. + */ + uint_fast64_t getLeafCount() const; + + /*! + * Retrieves the number of nodes necessary to represent the DD. + * + * @return The number of nodes in this DD. + */ + uint_fast64_t getNodeCount() const; + + /*! + * Retrieves whether this DD represents the constant one function. + * + * @return True if this DD represents the constant one function. + */ + bool isOne() const; + + /*! + * Retrieves whether this DD represents the constant zero function. + * + * @return True if this DD represents the constant zero function. + */ + bool isZero() const; + + /*! + * Retrieves the index of the topmost variable in the BDD. + * + * @return The index of the topmost variable in BDD. + */ + uint_fast64_t getIndex() const; + + /*! + * Exports the BDD to the given file in the dot format. + * + * @param filename The name of the file to which the BDD is to be exported. + * @param ddVariableNamesAsStrings The names of the variables to display in the dot file. + */ + void exportToDot(std::string const& filename, std::vector const& ddVariableNamesAsStrings) const; + + /*! + * Converts a BDD to an equivalent ADD. + * + * @return The corresponding ADD. + */ + template + InternalAdd toAdd() const; + + /*! + * Converts the BDD to a bit vector. The given offset-labeled DD is used to determine the correct row of + * each entry. + * + * @param rowOdd The ODD used for determining the correct row. + * @param ddVariableIndices The indices of the DD variables contained in this BDD. + * @return The bit vector that is represented by this BDD. + */ + storm::storage::BitVector toVector(storm::dd::Odd const& rowOdd, std::vector const& ddVariableIndices) const; + + /*! + * Creates an ODD based on the current BDD. + * + * @param ddVariableIndices The indices of the DD variables contained in this BDD. + * @return The corresponding ODD. + */ + Odd createOdd(std::vector const& ddVariableIndices) const; + + /*! + * Uses the current BDD to filter values from the explicit vector. + * + * @param odd The ODD used to determine which entries to select. + * @param ddVariableIndices The indices of the DD variables contained in this BDD. + * @param sourceValues The source vector. + * @param targetValues The vector to which to write the selected values. + */ + template + void filterExplicitVector(Odd const& odd, std::vector const& ddVariableIndices, std::vector const& sourceValues, std::vector& targetValues) const; + + private: + InternalDdManager const* ddManager; + }; + } +} + +#endif /* STORM_STORAGE_DD_CUDD_INTERNALSYLVANBDD_H_ */ \ No newline at end of file diff --git a/src/storage/dd/sylvan/InternalSylvanDdManager.cpp b/src/storage/dd/sylvan/InternalSylvanDdManager.cpp new file mode 100644 index 000000000..322c6c540 --- /dev/null +++ b/src/storage/dd/sylvan/InternalSylvanDdManager.cpp @@ -0,0 +1,61 @@ +#include "src/storage/dd/sylvan/InternalSylvanDdManager.h" + +#include "src/utility/macros.h" +#include "src/exceptions/NotImplementedException.h" + +namespace storm { + namespace dd { + + InternalDdManager::InternalDdManager() { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + InternalBdd InternalDdManager::getBddOne() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template + InternalAdd InternalDdManager::getAddOne() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + InternalBdd InternalDdManager::getBddZero() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template + InternalAdd InternalDdManager::getAddZero() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template + InternalAdd InternalDdManager::getConstant(ValueType const& value) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + std::pair, InternalBdd> InternalDdManager::createNewDdVariablePair() { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + void InternalDdManager::allowDynamicReordering(bool value) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + bool InternalDdManager::isDynamicReorderingAllowed() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + void InternalDdManager::triggerReordering() { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + 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; + } +} \ No newline at end of file diff --git a/src/storage/dd/sylvan/InternalSylvanDdManager.h b/src/storage/dd/sylvan/InternalSylvanDdManager.h new file mode 100644 index 000000000..3dc203b2e --- /dev/null +++ b/src/storage/dd/sylvan/InternalSylvanDdManager.h @@ -0,0 +1,101 @@ +#ifndef STORM_STORAGE_DD_INTERNALSYLVANDDMANAGER_H_ +#define STORM_STORAGE_DD_INTERNALSYLVANDDMANAGER_H_ + +#include "src/storage/dd/DdType.h" +#include "src/storage/dd/InternalDdManager.h" + +#include "src/storage/dd/sylvan/InternalSylvanBdd.h" +#include "src/storage/dd/sylvan/InternalSylvanAdd.h" + +namespace storm { + namespace dd { + template + class InternalAdd; + + template + class InternalBdd; + + template<> + class InternalDdManager { + public: + friend class InternalBdd; + + template + friend class InternalAdd; + + /*! + * Creates a new internal manager for CUDD DDs. + */ + InternalDdManager(); + + /*! + * Retrieves a BDD representing the constant one function. + * + * @return A BDD representing the constant one function. + */ + InternalBdd getBddOne() const; + + /*! + * Retrieves an ADD representing the constant one function. + * + * @return An ADD representing the constant one function. + */ + template + InternalAdd getAddOne() const; + + /*! + * Retrieves a BDD representing the constant zero function. + * + * @return A BDD representing the constant zero function. + */ + InternalBdd getBddZero() const; + + /*! + * Retrieves an ADD representing the constant zero function. + * + * @return An ADD representing the constant zero function. + */ + template + InternalAdd getAddZero() const; + + /*! + * Retrieves an ADD representing the constant function with the given value. + * + * @return An ADD representing the constant function with the given value. + */ + template + InternalAdd getConstant(ValueType const& value) const; + + /*! + * Creates a new pair of DD variables and returns the two cubes as a result. + * + * @return The two cubes belonging to the DD variables. + */ + std::pair, InternalBdd> createNewDdVariablePair(); + + /*! + * Sets whether or not dynamic reordering is allowed for the DDs managed by this manager. + * + * @param value If set to true, dynamic reordering is allowed and forbidden otherwise. + */ + void allowDynamicReordering(bool value); + + /*! + * Retrieves whether dynamic reordering is currently allowed. + * + * @return True iff dynamic reordering is currently allowed. + */ + bool isDynamicReorderingAllowed() const; + + /*! + * Triggers a reordering of the DDs managed by this manager. + */ + void triggerReordering(); + + private: + + }; + } +} + +#endif /* STORM_STORAGE_DD_INTERNALSYLVANDDMANAGER_H_ */ \ No newline at end of file diff --git a/src/storage/dd/sylvan/SylvanAddIterator.cpp b/src/storage/dd/sylvan/SylvanAddIterator.cpp new file mode 100644 index 000000000..f6d067b63 --- /dev/null +++ b/src/storage/dd/sylvan/SylvanAddIterator.cpp @@ -0,0 +1,36 @@ +#include "src/storage/dd/sylvan/SylvanAddIterator.h" + +#include "src/utility/macros.h" +#include "src/exceptions/NotImplementedException.h" + +namespace storm { + namespace dd { + template + AddIterator::AddIterator() { + // Intentionally left empty. + } + + template + AddIterator& AddIterator::operator++() { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template + bool AddIterator::operator==(AddIterator const& other) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template + bool AddIterator::operator!=(AddIterator const& other) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template + std::pair AddIterator::operator*() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + + template class AddIterator; + template class AddIterator; + } +} \ No newline at end of file diff --git a/src/storage/dd/sylvan/SylvanAddIterator.h b/src/storage/dd/sylvan/SylvanAddIterator.h new file mode 100644 index 000000000..9a79c0384 --- /dev/null +++ b/src/storage/dd/sylvan/SylvanAddIterator.h @@ -0,0 +1,69 @@ +#ifndef STORM_STORAGE_DD_SYLVANADDITERATOR_H_ +#define STORM_STORAGE_DD_SYLVANADDITERATOR_H_ + +#include "src/storage/dd/AddIterator.h" +#include "src/storage/expressions/SimpleValuation.h" + +namespace storm { + namespace dd { + // Forward-declare the DdManager class. + template + class DdManager; + + template + class InternalAdd; + + template + class AddIterator { + public: + friend class InternalAdd; + + // Default-instantiate the constructor. + AddIterator(); + + // Forbid copy-construction and copy assignment, because ownership of the internal pointer is unclear then. + AddIterator(AddIterator const& other) = delete; + AddIterator& operator=(AddIterator const& other) = delete; + + // Provide move-construction and move-assignment, though. + AddIterator(AddIterator&& other) = default; + AddIterator& operator=(AddIterator&& other) = default; + + /*! + * Moves the iterator one position forward. + */ + AddIterator& operator++(); + + /*! + * Returns a pair consisting of a valuation of meta variables and the value to which this valuation is + * mapped. Note that the result is returned by value. + * + * @return A pair of a valuation and the function value. + */ + std::pair operator*() const; + + /*! + * Compares the iterator with the given one. Two iterators are considered equal when all their underlying + * data members are the same or they both are at their end. + * + * @param other The iterator with which to compare. + * @return True if the two iterators are considered equal. + */ + bool operator==(AddIterator const& other) const; + + /*! + * Compares the iterator with the given one. Two iterators are considered unequal iff they are not + * considered equal. + * + * @param other The iterator with which to compare. + * @return True if the two iterators are considered unequal. + */ + bool operator!=(AddIterator const& other) const; + + private: + + }; + } +} + +#endif /* STORM_STORAGE_DD_SYLVANADDITERATOR_H_ */ \ No newline at end of file