Browse Source
trying to get the new infrastructure of the DD abstraction layer integrated into the other parts of storm
trying to get the new infrastructure of the DD abstraction layer integrated into the other parts of storm
Former-commit-id: 80a6634565
main
dehnert
10 years ago
34 changed files with 2941 additions and 2187 deletions
-
73src/adapters/AddExpressionAdapter.cpp
-
2src/adapters/AddExpressionAdapter.h
-
12src/modelchecker/csl/HybridCtmcCslModelChecker.cpp
-
8src/modelchecker/csl/HybridCtmcCslModelChecker.h
-
50src/modelchecker/csl/helper/HybridCtmcCslHelper.cpp
-
20src/modelchecker/csl/helper/HybridCtmcCslHelper.h
-
2src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp
-
4src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h
-
13src/modelchecker/propositional/SymbolicPropositionalModelChecker.h
-
32src/modelchecker/results/CheckResult.h
-
18src/modelchecker/results/HybridQuantitativeCheckResult.h
-
2src/modelchecker/results/SymbolicQualitativeCheckResult.h
-
12src/modelchecker/results/SymbolicQuantitativeCheckResult.h
-
24src/models/symbolic/Ctmc.h
-
20src/models/symbolic/DeterministicModel.h
-
20src/models/symbolic/Dtmc.h
-
20src/models/symbolic/Mdp.h
-
42src/models/symbolic/Model.h
-
38src/models/symbolic/StandardRewardModel.h
-
626src/storage/dd/Add.cpp
-
671src/storage/dd/Add.h
-
3src/storage/dd/AddIterator.h
-
4src/storage/dd/Bdd.cpp
-
2src/storage/dd/Bdd.h
-
1084src/storage/dd/cudd/CuddAdd.cpp
-
828src/storage/dd/cudd/CuddAdd.h
-
37src/storage/dd/cudd/CuddAddIterator.cpp
-
32src/storage/dd/cudd/CuddAddIterator.h
-
2src/storage/dd/cudd/CuddOdd.h
-
757src/storage/dd/cudd/InternalCuddAdd.cpp
-
598src/storage/dd/cudd/InternalCuddAdd.h
-
7src/storage/dd/cudd/InternalCuddBdd.h
-
50src/utility/graph.h
-
15src/utility/solver.h
@ -1,8 +1,634 @@ |
|||
#include "src/storage/dd/Add.h"
|
|||
|
|||
#include <boost/algorithm/string/join.hpp>
|
|||
|
|||
#include "src/storage/dd/DdMetaVariable.h"
|
|||
#include "src/storage/dd/DdManager.h"
|
|||
|
|||
#include "src/storage/SparseMatrix.h"
|
|||
|
|||
#include "src/utility/constants.h"
|
|||
#include "src/utility/macros.h"
|
|||
#include "src/exceptions/InvalidArgumentException.h"
|
|||
|
|||
namespace storm { |
|||
namespace dd { |
|||
template<DdType LibraryType, typename ValueType> |
|||
Add<LibraryType, ValueType>::Add(std::shared_ptr<DdManager<LibraryType> const> ddManager, InternalAdd<LibraryType, ValueType> const& internalAdd, std::set<storm::expressions::Variable> const& containedMetaVariables) : Dd<LibraryType>(ddManager, containedMetaVariables), internalAdd(internalAdd) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
bool Add<LibraryType, ValueType>::operator==(Add<LibraryType, ValueType> const& other) const { |
|||
return internalAdd == other.internalAdd; |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
bool Add<LibraryType, ValueType>::operator!=(Add<LibraryType, ValueType> const& other) const { |
|||
return internalAdd != other.internalAdd; |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
Add<LibraryType, ValueType> Add<LibraryType, ValueType>::ite(Add<LibraryType, ValueType> const& thenAdd, Add<LibraryType, ValueType> const& elseAdd) const { |
|||
std::set<storm::expressions::Variable> metaVariables = Dd<LibraryType>::joinMetaVariables(thenAdd, elseAdd); |
|||
metaVariables.insert(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end()); |
|||
return Add<LibraryType, ValueType>(this->getDdManager(), internalAdd.ite(thenAdd.internalAdd, elseAdd.internalAdd), metaVariables); |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
Add<LibraryType, ValueType> Add<LibraryType, ValueType>::operator!() const { |
|||
return Add<LibraryType, ValueType>(this->getDdManager(), !internalAdd, this->getContainedMetaVariables()); |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
Add<LibraryType, ValueType> Add<LibraryType, ValueType>::operator||(Add<LibraryType, ValueType> const& other) const { |
|||
return Add<LibraryType, ValueType>(this->getDdManager(), internalAdd || other.internalAdd, Dd<LibraryType>::joinMetaVariables(*this, other)); |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
Add<LibraryType, ValueType>& Add<LibraryType, ValueType>::operator|=(Add<LibraryType, ValueType> const& other) { |
|||
this->addMetaVariables(other.getContainedMetaVariables()); |
|||
internalAdd |= other.internalAdd; |
|||
return *this; |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
Add<LibraryType, ValueType> Add<LibraryType, ValueType>::operator+(Add<LibraryType, ValueType> const& other) const { |
|||
return Add<LibraryType, ValueType>(this->getDdManager(), internalAdd + other.internalAdd, Dd<LibraryType>::joinMetaVariables(*this, other)); |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
Add<LibraryType, ValueType>& Add<LibraryType, ValueType>::operator+=(Add<LibraryType, ValueType> const& other) { |
|||
this->addMetaVariables(other.getContainedMetaVariables()); |
|||
internalAdd += other.internalAdd; |
|||
return *this; |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
Add<LibraryType, ValueType> Add<LibraryType, ValueType>::operator*(Add<LibraryType, ValueType> const& other) const { |
|||
return Add<LibraryType, ValueType>(this->getDdManager(), internalAdd * other.internalAdd, Dd<LibraryType>::joinMetaVariables(*this, other)); |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
Add<LibraryType, ValueType>& Add<LibraryType, ValueType>::operator*=(Add<LibraryType, ValueType> const& other) { |
|||
this->addMetaVariables(other.getContainedMetaVariables()); |
|||
internalAdd *= other.internalAdd; |
|||
return *this; |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
Add<LibraryType, ValueType> Add<LibraryType, ValueType>::operator-(Add<LibraryType, ValueType> const& other) const { |
|||
return Add<LibraryType, ValueType>(this->getDdManager(), internalAdd - other.internalAdd, Dd<LibraryType>::joinMetaVariables(*this, other)); |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
Add<LibraryType, ValueType> Add<LibraryType, ValueType>::operator-() const { |
|||
return this->getDdManager()->getAddZero() - *this; |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
Add<LibraryType, ValueType>& Add<LibraryType, ValueType>::operator-=(Add<LibraryType, ValueType> const& other) { |
|||
this->addMetaVariables(other.getContainedMetaVariables()); |
|||
internalAdd -= other.internalAdd; |
|||
return *this; |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
Add<LibraryType, ValueType> Add<LibraryType, ValueType>::operator/(Add<LibraryType, ValueType> const& other) const { |
|||
return Add<LibraryType, ValueType>(this->getDdManager(), internalAdd / other.internalAdd, Dd<LibraryType>::joinMetaVariables(*this, other)); |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
Add<LibraryType, ValueType>& Add<LibraryType, ValueType>::operator/=(Add<LibraryType, ValueType> const& other) { |
|||
this->addMetaVariables(other.getContainedMetaVariables()); |
|||
internalAdd /= other.internalAdd; |
|||
return *this; |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
Add<LibraryType, ValueType> Add<LibraryType, ValueType>::equals(Add<LibraryType, ValueType> const& other) const { |
|||
return Add<LibraryType, ValueType>(this->getDdManager(), internalAdd.equals(other), Dd<LibraryType>::joinMetaVariables(*this, other)); |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
Add<LibraryType, ValueType> Add<LibraryType, ValueType>::notEquals(Add<LibraryType, ValueType> const& other) const { |
|||
return Add<LibraryType, ValueType>(this->getDdManager(), internalAdd.notEquals(other), Dd<LibraryType>::joinMetaVariables(*this, other)); |
|||
|
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
Add<LibraryType, ValueType> Add<LibraryType, ValueType>::less(Add<LibraryType, ValueType> const& other) const { |
|||
return Add<LibraryType, ValueType>(this->getDdManager(), internalAdd.less(other), Dd<LibraryType>::joinMetaVariables(*this, other)); |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
Add<LibraryType, ValueType> Add<LibraryType, ValueType>::lessOrEqual(Add<LibraryType, ValueType> const& other) const { |
|||
return Add<LibraryType, ValueType>(this->getDdManager(), internalAdd.lessOrEqual(other), Dd<LibraryType>::joinMetaVariables(*this, other)); |
|||
|
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
Add<LibraryType, ValueType> Add<LibraryType, ValueType>::greater(Add<LibraryType, ValueType> const& other) const { |
|||
return Add<LibraryType, ValueType>(this->getDdManager(), internalAdd.greater(other), Dd<LibraryType>::joinMetaVariables(*this, other)); |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
Add<LibraryType, ValueType> Add<LibraryType, ValueType>::greaterOrEqual(Add<LibraryType, ValueType> const& other) const { |
|||
return Add<LibraryType, ValueType>(this->getDdManager(), internalAdd.greaterOrEqual(other), Dd<LibraryType>::joinMetaVariables(*this, other)); |
|||
|
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
Add<LibraryType, ValueType> Add<LibraryType, ValueType>::pow(Add<LibraryType, ValueType> const& other) const { |
|||
return Add<LibraryType, ValueType>(this->getDdManager(), internalAdd.pow(other), Dd<LibraryType>::joinMetaVariables(*this, other)); |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
Add<LibraryType, ValueType> Add<LibraryType, ValueType>::mod(Add<LibraryType, ValueType> const& other) const { |
|||
return Add<LibraryType, ValueType>(this->getDdManager(), internalAdd.mod(other), Dd<LibraryType>::joinMetaVariables(*this, other)); |
|||
|
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
Add<LibraryType, ValueType> Add<LibraryType, ValueType>::logxy(Add<LibraryType, ValueType> const& other) const { |
|||
return Add<LibraryType, ValueType>(this->getDdManager(), internalAdd.logxy(other), Dd<LibraryType>::joinMetaVariables(*this, other)); |
|||
|
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
Add<LibraryType, ValueType> Add<LibraryType, ValueType>::floor() const { |
|||
return Add<LibraryType, ValueType>(this->getDdManager(), internalAdd.floor(), this->getContainedMetaVariables()); |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
Add<LibraryType, ValueType> Add<LibraryType, ValueType>::ceil() const { |
|||
return Add<LibraryType, ValueType>(this->getDdManager(), internalAdd.ceil(), this->getContainedMetaVariables()); |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
Add<LibraryType, ValueType> Add<LibraryType, ValueType>::minimum(Add<LibraryType, ValueType> const& other) const { |
|||
return Add<LibraryType, ValueType>(this->getDdManager(), internalAdd.minimum(other), Dd<LibraryType>::joinMetaVariables(*this, other)); |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
Add<LibraryType, ValueType> Add<LibraryType, ValueType>::maximum(Add<LibraryType, ValueType> const& other) const { |
|||
return Add<LibraryType, ValueType>(this->getDdManager(), internalAdd.maximum(other), Dd<LibraryType>::joinMetaVariables(*this, other)); |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
Add<LibraryType, ValueType> Add<LibraryType, ValueType>::sumAbstract(std::set<storm::expressions::Variable> const& metaVariables) const { |
|||
Bdd<LibraryType> cube = this->getCube(metaVariables); |
|||
return Add<LibraryType, ValueType>(this->getDdManager(), internalAdd.sumAbstract(cube), Dd<LibraryType>::subtractMetaVariables(*this, cube)); |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
Add<LibraryType, ValueType> Add<LibraryType, ValueType>::minAbstract(std::set<storm::expressions::Variable> const& metaVariables) const { |
|||
Bdd<LibraryType> cube = this->getCube(metaVariables); |
|||
return Add<LibraryType, ValueType>(this->getDdManager(), internalAdd.minAbstract(cube), Dd<LibraryType>::subtractMetaVariables(*this, cube)); |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
Add<LibraryType, ValueType> Add<LibraryType, ValueType>::maxAbstract(std::set<storm::expressions::Variable> const& metaVariables) const { |
|||
Bdd<LibraryType> cube = this->getCube(metaVariables); |
|||
return Add<LibraryType, ValueType>(this->getDdManager(), internalAdd.maxAbstract(cube), Dd<LibraryType>::subtractMetaVariables(*this, cube)); |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
bool Add<LibraryType, ValueType>::equalModuloPrecision(Add<LibraryType, ValueType> const& other, double precision, bool relative) const { |
|||
return internalAdd.equalModuloPrecision(other, precision, relative); |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
Add<LibraryType, ValueType> Add<LibraryType, ValueType>::swapVariables(std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& metaVariablePairs) const { |
|||
std::set<storm::expressions::Variable> newContainedMetaVariables; |
|||
std::vector<InternalAdd<LibraryType, ValueType>> from; |
|||
std::vector<InternalAdd<LibraryType, ValueType>> to; |
|||
for (auto const& metaVariablePair : metaVariablePairs) { |
|||
DdMetaVariable<LibraryType> const& variable1 = this->getDdManager()->getMetaVariable(metaVariablePair.first); |
|||
DdMetaVariable<LibraryType> const& variable2 = this->getDdManager()->getMetaVariable(metaVariablePair.second); |
|||
|
|||
// Keep track of the contained meta variables in the DD.
|
|||
if (this->containsMetaVariable(metaVariablePair.first)) { |
|||
newContainedMetaVariables.insert(metaVariablePair.second); |
|||
} |
|||
if (this->containsMetaVariable(metaVariablePair.second)) { |
|||
newContainedMetaVariables.insert(metaVariablePair.first); |
|||
} |
|||
|
|||
for (auto const& ddVariable : variable1.getDdVariables()) { |
|||
from.push_back(ddVariable.toAdd()); |
|||
} |
|||
for (auto const& ddVariable : variable2.getDdVariables()) { |
|||
to.push_back(ddVariable.toAdd()); |
|||
} |
|||
} |
|||
return Bdd<LibraryType>(this->getDdManager(), internalAdd.swapVariables(from, to), newContainedMetaVariables); |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
Add<LibraryType, ValueType> Add<LibraryType, ValueType>::multiplyMatrix(Add<LibraryType, ValueType> const& otherMatrix, std::set<storm::expressions::Variable> const& summationMetaVariables) const { |
|||
// Create the CUDD summation variables.
|
|||
std::vector<InternalAdd<LibraryType, ValueType>> summationDdVariables; |
|||
for (auto const& metaVariable : summationMetaVariables) { |
|||
for (auto const& ddVariable : this->getDdManager()->getMetaVariable(metaVariable).getDdVariables()) { |
|||
summationDdVariables.push_back(ddVariable.toAdd()); |
|||
} |
|||
} |
|||
|
|||
std::set<storm::expressions::Variable> unionOfMetaVariables = Dd<LibraryType>::joinMetaVariables(*this, otherMatrix); |
|||
std::set<storm::expressions::Variable> containedMetaVariables; |
|||
std::set_difference(unionOfMetaVariables.begin(), unionOfMetaVariables.end(), summationMetaVariables.begin(), summationMetaVariables.end(), std::inserter(containedMetaVariables, containedMetaVariables.begin())); |
|||
|
|||
return Add<LibraryType, ValueType>(this->getDdManager(), internalAdd.multiplyMatrix(otherMatrix, summationDdVariables), containedMetaVariables); |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
Bdd<LibraryType> Add<LibraryType, ValueType>::greater(ValueType const& value) const { |
|||
return Bdd<LibraryType>(this->getDdManager(), internalAdd.greater(value), this->getContainedMetaVariables()); |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
Bdd<LibraryType> Add<LibraryType, ValueType>::greaterOrEqual(ValueType const& value) const { |
|||
return Bdd<LibraryType>(this->getDdManager(), internalAdd.greaterOrEqual(value), this->getContainedMetaVariables()); |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
Bdd<LibraryType> Add<LibraryType, ValueType>::less(ValueType const& value) const { |
|||
return Bdd<LibraryType>(this->getDdManager(), internalAdd.less(value), this->getContainedMetaVariables()); |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
Bdd<LibraryType> Add<LibraryType, ValueType>::lessOrEqual(ValueType const& value) const { |
|||
return Bdd<LibraryType>(this->getDdManager(), internalAdd.lessOrEqual(value), this->getContainedMetaVariables()); |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
Bdd<LibraryType> Add<LibraryType, ValueType>::notZero() const { |
|||
return this->toBdd(); |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
Add<LibraryType, ValueType> Add<LibraryType, ValueType>::constrain(Add<LibraryType, ValueType> const& constraint) const { |
|||
return Add<LibraryType, ValueType>(this->getDdManager(), internalAdd.constrain(constraint), Dd<LibraryType>::joinMetaVariables(*this, constraint)); |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
Add<LibraryType, ValueType> Add<LibraryType, ValueType>::restrict(Add<LibraryType, ValueType> const& constraint) const { |
|||
return Add<LibraryType, ValueType>(this->getDdManager(), internalAdd.restrict(constraint), Dd<LibraryType>::joinMetaVariables(*this, constraint)); |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
Bdd<LibraryType> Add<LibraryType, ValueType>::getSupport() const { |
|||
return Bdd<LibraryType>(this->getDdManager(), internalAdd.getSupport(), this->getContainedMetaVariables()); |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
uint_fast64_t Add<LibraryType, ValueType>::getNonZeroCount() const { |
|||
std::size_t numberOfDdVariables = 0; |
|||
for (auto const& metaVariable : this->getContainedMetaVariables()) { |
|||
numberOfDdVariables += this->getDdManager()->getMetaVariable(metaVariable).getNumberOfDdVariables(); |
|||
} |
|||
return internalAdd.getNonZeroCount(numberOfDdVariables); |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
uint_fast64_t Add<LibraryType, ValueType>::getLeafCount() const { |
|||
return internalAdd.getLeafCount(); |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
uint_fast64_t Add<LibraryType, ValueType>::getNodeCount() const { |
|||
return internalAdd.getNodeCount(); |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
ValueType Add<LibraryType, ValueType>::getMin() const { |
|||
return internalAdd.getMin(); |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
ValueType Add<LibraryType, ValueType>::getMax() const { |
|||
return internalAdd.getMax(); |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
void Add<LibraryType, ValueType>::setValue(storm::expressions::Variable const& metaVariable, int_fast64_t variableValue, ValueType const& targetValue) { |
|||
std::map<storm::expressions::Variable, int_fast64_t> metaVariableToValueMap; |
|||
metaVariableToValueMap.emplace(metaVariable, variableValue); |
|||
this->setValue(metaVariableToValueMap, targetValue); |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
void Add<LibraryType, ValueType>::setValue(storm::expressions::Variable const& metaVariable1, int_fast64_t variableValue1, storm::expressions::Variable const& metaVariable2, int_fast64_t variableValue2, ValueType const& targetValue) { |
|||
std::map<storm::expressions::Variable, int_fast64_t> metaVariableToValueMap; |
|||
metaVariableToValueMap.emplace(metaVariable1, variableValue1); |
|||
metaVariableToValueMap.emplace(metaVariable2, variableValue2); |
|||
this->setValue(metaVariableToValueMap, targetValue); |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
void Add<LibraryType, ValueType>::setValue(std::map<storm::expressions::Variable, int_fast64_t> const& metaVariableToValueMap, ValueType const& targetValue) { |
|||
Bdd<LibraryType> valueEncoding = this->getDdManager()->getBddOne(); |
|||
for (auto const& nameValuePair : metaVariableToValueMap) { |
|||
valueEncoding &= this->getDdManager()->getEncoding(nameValuePair.first, nameValuePair.second); |
|||
// Also record that the DD now contains the meta variable.
|
|||
this->addMetaVariable(nameValuePair.first); |
|||
} |
|||
|
|||
internalAdd = valueEncoding.toAdd().ite(this->getDdManager()->getConstant(targetValue), internalAdd); |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
ValueType Add<LibraryType, ValueType>::getValue(std::map<storm::expressions::Variable, int_fast64_t> const& metaVariableToValueMap) const { |
|||
std::set<storm::expressions::Variable> remainingMetaVariables(this->getContainedMetaVariables()); |
|||
Bdd<LibraryType> valueEncoding = this->getDdManager()->getBddOne(); |
|||
for (auto const& nameValuePair : metaVariableToValueMap) { |
|||
valueEncoding &= this->getDdManager()->getEncoding(nameValuePair.first, nameValuePair.second); |
|||
if (this->containsMetaVariable(nameValuePair.first)) { |
|||
remainingMetaVariables.erase(nameValuePair.first); |
|||
} |
|||
} |
|||
|
|||
STORM_LOG_THROW(remainingMetaVariables.empty(), storm::exceptions::InvalidArgumentException, "Cannot evaluate function for which not all inputs were given."); |
|||
|
|||
Add<LibraryType, ValueType> value = *this * valueEncoding.toAdd(); |
|||
value = value.sumAbstract(this->getContainedMetaVariables()); |
|||
return value.getMax(); |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
bool Add<LibraryType, ValueType>::isOne() const { |
|||
return internalAdd.isOne(); |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
bool Add<LibraryType, ValueType>::isZero() const { |
|||
return internalAdd.isZero(); |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
bool Add<LibraryType, ValueType>::isConstant() const { |
|||
return internalAdd.isConstant(); |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
uint_fast64_t Add<LibraryType, ValueType>::getIndex() const { |
|||
return internalAdd.getIndex(); |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
std::vector<ValueType> Add<LibraryType, ValueType>::toVector() const { |
|||
return this->toVector(Odd<LibraryType>(*this)); |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
std::vector<ValueType> Add<LibraryType, ValueType>::toVector(Odd<LibraryType> const& rowOdd) const { |
|||
std::vector<ValueType> result(rowOdd.getTotalOffset()); |
|||
std::vector<uint_fast64_t> ddVariableIndices = this->getDdManager().getSortedVariableIndices(); |
|||
addToVector(rowOdd, ddVariableIndices, result); |
|||
return result; |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
std::vector<ValueType> Add<LibraryType, ValueType>::toVector(std::set<storm::expressions::Variable> const& groupMetaVariables, storm::dd::Odd<LibraryType> const& rowOdd, std::vector<uint_fast64_t> const& groupOffsets) const { |
|||
std::set<storm::expressions::Variable> rowMetaVariables; |
|||
|
|||
// Prepare the proper sets of meta variables.
|
|||
for (auto const& variable : this->getContainedMetaVariables()) { |
|||
if (groupMetaVariables.find(variable) != groupMetaVariables.end()) { |
|||
continue; |
|||
} |
|||
|
|||
rowMetaVariables.insert(variable); |
|||
} |
|||
std::vector<uint_fast64_t> ddGroupVariableIndices; |
|||
for (auto const& variable : groupMetaVariables) { |
|||
DdMetaVariable<LibraryType> const& metaVariable = this->getDdManager()->getMetaVariable(variable); |
|||
for (auto const& ddVariable : metaVariable.getDdVariables()) { |
|||
ddGroupVariableIndices.push_back(ddVariable.getIndex()); |
|||
} |
|||
} |
|||
std::vector<uint_fast64_t> ddRowVariableIndices; |
|||
for (auto const& variable : rowMetaVariables) { |
|||
DdMetaVariable<LibraryType> const& metaVariable = this->getDdManager()->getMetaVariable(variable); |
|||
for (auto const& ddVariable : metaVariable.getDdVariables()) { |
|||
ddRowVariableIndices.push_back(ddVariable.getIndex()); |
|||
} |
|||
} |
|||
|
|||
return internalAdd.toVector(ddGroupVariableIndices, rowOdd, ddRowVariableIndices, groupOffsets); |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
storm::storage::SparseMatrix<ValueType> Add<LibraryType, ValueType>::toMatrix() const { |
|||
std::set<storm::expressions::Variable> rowVariables; |
|||
std::set<storm::expressions::Variable> columnVariables; |
|||
|
|||
for (auto const& variable : this->getContainedMetaVariables()) { |
|||
if (variable.getName().size() > 0 && variable.getName().back() == '\'') { |
|||
columnVariables.insert(variable); |
|||
} else { |
|||
rowVariables.insert(variable); |
|||
} |
|||
} |
|||
|
|||
return toMatrix(rowVariables, columnVariables, Odd<LibraryType>(this->sumAbstract(rowVariables)), Odd<LibraryType>(this->sumAbstract(columnVariables))); |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
storm::storage::SparseMatrix<ValueType> Add<LibraryType, ValueType>::toMatrix(storm::dd::Odd<LibraryType> const& rowOdd, storm::dd::Odd<LibraryType> const& columnOdd) const { |
|||
std::set<storm::expressions::Variable> rowMetaVariables; |
|||
std::set<storm::expressions::Variable> columnMetaVariables; |
|||
|
|||
for (auto const& variable : this->getContainedMetaVariables()) { |
|||
if (variable.getName().size() > 0 && variable.getName().back() == '\'') { |
|||
columnMetaVariables.insert(variable); |
|||
} else { |
|||
rowMetaVariables.insert(variable); |
|||
} |
|||
} |
|||
|
|||
return toMatrix(rowMetaVariables, columnMetaVariables, rowOdd, columnOdd); |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
storm::storage::SparseMatrix<ValueType> Add<LibraryType, ValueType>::toMatrix(std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, storm::dd::Odd<LibraryType> const& rowOdd, storm::dd::Odd<LibraryType> const& columnOdd) const { |
|||
std::vector<uint_fast64_t> ddRowVariableIndices; |
|||
std::vector<uint_fast64_t> ddColumnVariableIndices; |
|||
|
|||
for (auto const& variable : rowMetaVariables) { |
|||
DdMetaVariable<LibraryType> const& metaVariable = this->getDdManager()->getMetaVariable(variable); |
|||
for (auto const& ddVariable : metaVariable.getDdVariables()) { |
|||
ddRowVariableIndices.push_back(ddVariable.getIndex()); |
|||
} |
|||
} |
|||
std::sort(ddRowVariableIndices.begin(), ddRowVariableIndices.end()); |
|||
|
|||
for (auto const& variable : columnMetaVariables) { |
|||
DdMetaVariable<LibraryType> const& metaVariable = this->getDdManager()->getMetaVariable(variable); |
|||
for (auto const& ddVariable : metaVariable.getDdVariables()) { |
|||
ddColumnVariableIndices.push_back(ddVariable.getIndex()); |
|||
} |
|||
} |
|||
std::sort(ddColumnVariableIndices.begin(), ddColumnVariableIndices.end()); |
|||
|
|||
return internalAdd.toMatrix(rowOdd, ddRowVariableIndices, columnOdd, ddColumnVariableIndices); |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
storm::storage::SparseMatrix<ValueType> Add<LibraryType, ValueType>::toMatrix(std::set<storm::expressions::Variable> const& groupMetaVariables, storm::dd::Odd<LibraryType> const& rowOdd, storm::dd::Odd<LibraryType> const& columnOdd) const { |
|||
std::set<storm::expressions::Variable> rowMetaVariables; |
|||
std::set<storm::expressions::Variable> columnMetaVariables; |
|||
|
|||
for (auto const& variable : this->getContainedMetaVariables()) { |
|||
// If the meta variable is a group meta variable, we do not insert it into the set of row/column meta variables.
|
|||
if (groupMetaVariables.find(variable) != groupMetaVariables.end()) { |
|||
continue; |
|||
} |
|||
|
|||
if (variable.getName().size() > 0 && variable.getName().back() == '\'') { |
|||
columnMetaVariables.insert(variable); |
|||
} else { |
|||
rowMetaVariables.insert(variable); |
|||
} |
|||
} |
|||
|
|||
// Create the canonical row group sizes and build the matrix.
|
|||
return toMatrix(rowMetaVariables, columnMetaVariables, groupMetaVariables, rowOdd, columnOdd); |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
storm::storage::SparseMatrix<ValueType> Add<LibraryType, ValueType>::toMatrix(std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::set<storm::expressions::Variable> const& groupMetaVariables, storm::dd::Odd<LibraryType> const& rowOdd, storm::dd::Odd<LibraryType> const& columnOdd) const { |
|||
std::vector<uint_fast64_t> ddRowVariableIndices; |
|||
std::vector<uint_fast64_t> ddColumnVariableIndices; |
|||
std::vector<uint_fast64_t> ddGroupVariableIndices; |
|||
std::set<storm::expressions::Variable> rowAndColumnMetaVariables; |
|||
|
|||
for (auto const& variable : rowMetaVariables) { |
|||
DdMetaVariable<LibraryType> const& metaVariable = this->getDdManager()->getMetaVariable(variable); |
|||
for (auto const& ddVariable : metaVariable.getDdVariables()) { |
|||
ddRowVariableIndices.push_back(ddVariable.getIndex()); |
|||
} |
|||
rowAndColumnMetaVariables.insert(variable); |
|||
} |
|||
std::sort(ddRowVariableIndices.begin(), ddRowVariableIndices.end()); |
|||
for (auto const& variable : columnMetaVariables) { |
|||
DdMetaVariable<LibraryType> const& metaVariable = this->getDdManager()->getMetaVariable(variable); |
|||
for (auto const& ddVariable : metaVariable.getDdVariables()) { |
|||
ddColumnVariableIndices.push_back(ddVariable.getIndex()); |
|||
} |
|||
rowAndColumnMetaVariables.insert(variable); |
|||
} |
|||
std::sort(ddColumnVariableIndices.begin(), ddColumnVariableIndices.end()); |
|||
for (auto const& variable : groupMetaVariables) { |
|||
DdMetaVariable<LibraryType> const& metaVariable = this->getDdManager()->getMetaVariable(variable); |
|||
for (auto const& ddVariable : metaVariable.getDdVariables()) { |
|||
ddGroupVariableIndices.push_back(ddVariable.getIndex()); |
|||
} |
|||
} |
|||
std::sort(ddGroupVariableIndices.begin(), ddGroupVariableIndices.end()); |
|||
|
|||
return internalAdd.toMatrix(ddGroupVariableIndices, rowOdd, ddRowVariableIndices, columnOdd, ddColumnVariableIndices); |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<ValueType>> Add<LibraryType, ValueType>::toMatrixVector(storm::dd::Add<LibraryType, ValueType> const& vector, std::vector<uint_fast64_t>&& rowGroupSizes, std::set<storm::expressions::Variable> const& groupMetaVariables, storm::dd::Odd<LibraryType> const& rowOdd, storm::dd::Odd<LibraryType> const& columnOdd) const { |
|||
std::set<storm::expressions::Variable> rowMetaVariables; |
|||
std::set<storm::expressions::Variable> columnMetaVariables; |
|||
|
|||
for (auto const& variable : this->getContainedMetaVariables()) { |
|||
// If the meta variable is a group meta variable, we do not insert it into the set of row/column meta variables.
|
|||
if (groupMetaVariables.find(variable) != groupMetaVariables.end()) { |
|||
continue; |
|||
} |
|||
|
|||
if (variable.getName().size() > 0 && variable.getName().back() == '\'') { |
|||
columnMetaVariables.insert(variable); |
|||
} else { |
|||
rowMetaVariables.insert(variable); |
|||
} |
|||
} |
|||
|
|||
// Create the canonical row group sizes and build the matrix.
|
|||
return toMatrixVector(vector, std::move(rowGroupSizes), rowMetaVariables, columnMetaVariables, groupMetaVariables, rowOdd, columnOdd); |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<ValueType>> Add<LibraryType, ValueType>::toMatrixVector(storm::dd::Add<LibraryType, ValueType> const& vector, std::vector<uint_fast64_t>&& rowGroupIndices, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::set<storm::expressions::Variable> const& groupMetaVariables, storm::dd::Odd<LibraryType> const& rowOdd, storm::dd::Odd<LibraryType> const& columnOdd) const { |
|||
std::vector<uint_fast64_t> ddRowVariableIndices; |
|||
std::vector<uint_fast64_t> ddColumnVariableIndices; |
|||
std::vector<uint_fast64_t> ddGroupVariableIndices; |
|||
std::set<storm::expressions::Variable> rowAndColumnMetaVariables; |
|||
|
|||
for (auto const& variable : rowMetaVariables) { |
|||
DdMetaVariable<LibraryType> const& metaVariable = this->getDdManager()->getMetaVariable(variable); |
|||
for (auto const& ddVariable : metaVariable.getDdVariables()) { |
|||
ddRowVariableIndices.push_back(ddVariable.getIndex()); |
|||
} |
|||
rowAndColumnMetaVariables.insert(variable); |
|||
} |
|||
std::sort(ddRowVariableIndices.begin(), ddRowVariableIndices.end()); |
|||
for (auto const& variable : columnMetaVariables) { |
|||
DdMetaVariable<LibraryType> const& metaVariable = this->getDdManager()->getMetaVariable(variable); |
|||
for (auto const& ddVariable : metaVariable.getDdVariables()) { |
|||
ddColumnVariableIndices.push_back(ddVariable.getIndex()); |
|||
} |
|||
rowAndColumnMetaVariables.insert(variable); |
|||
} |
|||
std::sort(ddColumnVariableIndices.begin(), ddColumnVariableIndices.end()); |
|||
for (auto const& variable : groupMetaVariables) { |
|||
DdMetaVariable<LibraryType> const& metaVariable = this->getDdManager()->getMetaVariable(variable); |
|||
for (auto const& ddVariable : metaVariable.getDdVariables()) { |
|||
ddGroupVariableIndices.push_back(ddVariable.getIndex()); |
|||
} |
|||
} |
|||
std::sort(ddGroupVariableIndices.begin(), ddGroupVariableIndices.end()); |
|||
|
|||
return internalAdd.toMatrixVector(vector.internalAdd, ddGroupVariableIndices, std::move(rowGroupIndices), rowOdd, ddRowVariableIndices, columnOdd, ddColumnVariableIndices); |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
void Add<LibraryType, ValueType>::exportToDot(std::string const& filename) const { |
|||
internalAdd.exportToDot(filename, this->getDdManager()->getDdVariableNames()); |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
AddIterator<LibraryType, ValueType> Add<LibraryType, ValueType>::begin(bool enumerateDontCareMetaVariables) const { |
|||
internalAdd.begin(this->getContainedMetaVariables(), enumerateDontCareMetaVariables); |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
AddIterator<LibraryType, ValueType> Add<LibraryType, ValueType>::end(bool enumerateDontCareMetaVariables) const { |
|||
return internalAdd.end(enumerateDontCareMetaVariables); |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
std::ostream& operator<<(std::ostream& out, Add<LibraryType, ValueType> const& add) { |
|||
out << "ADD with " << add.getNonZeroCount() << " nnz, " << add.getNodeCount() << " nodes, " << add.getLeafCount() << " leaves" << std::endl; |
|||
std::vector<std::string> variableNames; |
|||
for (auto const& variable : add.getContainedMetaVariables()) { |
|||
variableNames.push_back(variable.getName()); |
|||
} |
|||
out << "contained variables: " << boost::algorithm::join(variableNames, ", ") << std::endl; |
|||
return out; |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
void Add<LibraryType, ValueType>::addToVector(Odd<LibraryType> const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<ValueType>& targetVector) const { |
|||
std::function<ValueType (ValueType const&, ValueType const&)> fct = [] (ValueType const& a, ValueType const& b) -> ValueType { return a + b; }; |
|||
return internalAdd.composeVector(odd, ddVariableIndices, targetVector, fct); |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
Add<LibraryType, ValueType> Add<LibraryType, ValueType>::fromVector(std::shared_ptr<DdManager<LibraryType> const> ddManager, std::vector<ValueType> const& values, Odd<LibraryType> const& odd, std::set<storm::expressions::Variable> const& metaVariables) { |
|||
return Add<LibraryType, ValueType>(ddManager, InternalAdd<LibraryType, ValueType>::fromVector(ddManager, values, odd, ddManager->getSortedVariableIndices(metaVariables)), metaVariables); |
|||
} |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
Bdd<LibraryType> Add<LibraryType, ValueType>::toBdd() const { |
|||
return Bdd<DdType::CUDD>(this->getDdManager(), internalAdd.toBdd(), this->getContainedMetaVariables()); |
|||
} |
|||
|
|||
template class Add<storm::dd::DdType::CUDD, double>; |
|||
} |
|||
} |
|||
1084
src/storage/dd/cudd/CuddAdd.cpp
File diff suppressed because it is too large
View File
File diff suppressed because it is too large
View File
@ -1,828 +0,0 @@ |
|||
#ifndef STORM_STORAGE_DD_CUDDADD_H_ |
|||
#define STORM_STORAGE_DD_CUDDADD_H_ |
|||
|
|||
#include <boost/optional.hpp> |
|||
#include <map> |
|||
|
|||
#include "src/storage/dd/Add.h" |
|||
#include "src/storage/dd/cudd/CuddDd.h" |
|||
#include "src/storage/dd/cudd/CuddDdForwardIterator.h" |
|||
#include "src/storage/expressions/Variable.h" |
|||
#include "src/utility/OsDetection.h" |
|||
|
|||
// Include the C++-interface of CUDD. |
|||
#include "cuddObj.hh" |
|||
|
|||
namespace storm { |
|||
namespace storage { |
|||
template<typename T> class SparseMatrix; |
|||
class BitVector; |
|||
template<typename E, typename V> class MatrixEntry; |
|||
} |
|||
|
|||
namespace dd { |
|||
// Forward-declare some classes. |
|||
template<DdType Type> class DdManager; |
|||
template<DdType Type> class Odd; |
|||
template<DdType Type> class Bdd; |
|||
|
|||
template<> |
|||
class Add<DdType::CUDD> : public Dd<DdType::CUDD> { |
|||
public: |
|||
// Declare the DdManager and DdIterator class as friend so it can access the internals of a DD. |
|||
friend class DdManager<DdType::CUDD>; |
|||
friend class DdForwardIterator<DdType::CUDD>; |
|||
friend class Bdd<DdType::CUDD>; |
|||
friend class Odd<DdType::CUDD>; |
|||
|
|||
/*! |
|||
* Creates an ADD from the given explicit vector. |
|||
* |
|||
* @param ddManager The manager responsible for this DD. |
|||
* @param values The vector that is to be represented by the ADD. |
|||
* @param odd An ODD that is used to do the translation. |
|||
* @param metaVariables The meta variables to use to encode the vector. |
|||
*/ |
|||
Add(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, std::vector<double> const& values, Odd<DdType::CUDD> const& odd, std::set<storm::expressions::Variable> const& metaVariables); |
|||
|
|||
// Instantiate all copy/move constructors/assignments with the default implementation. |
|||
Add() = default; |
|||
Add(Add<DdType::CUDD> const& other) = default; |
|||
Add& operator=(Add<DdType::CUDD> const& other) = default; |
|||
#ifndef WINDOWS |
|||
Add(Add<DdType::CUDD>&& other) = default; |
|||
Add& operator=(Add<DdType::CUDD>&& other) = default; |
|||
#endif |
|||
|
|||
/*! |
|||
* 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==(Add<DdType::CUDD> 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!=(Add<DdType::CUDD> 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. |
|||
*/ |
|||
Add<DdType::CUDD> ite(Add<DdType::CUDD> const& thenDd, Add<DdType::CUDD> const& elseDd) 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. |
|||
*/ |
|||
Add<DdType::CUDD> operator!() const; |
|||
|
|||
/*! |
|||
* Performs a logical or of the current anBd 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. |
|||
*/ |
|||
Add<DdType::CUDD> operator||(Add<DdType::CUDD> 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 |
|||
*/ |
|||
Add<DdType::CUDD>& operator|=(Add<DdType::CUDD> const& other); |
|||
|
|||
/*! |
|||
* Adds the two ADDs. |
|||
* |
|||
* @param other The ADD to add to the current one. |
|||
* @return The result of the addition. |
|||
*/ |
|||
Add<DdType::CUDD> operator+(Add<DdType::CUDD> 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. |
|||
*/ |
|||
Add<DdType::CUDD>& operator+=(Add<DdType::CUDD> const& other); |
|||
|
|||
/*! |
|||
* Multiplies the two ADDs. |
|||
* |
|||
* @param other The ADD to multiply with the current one. |
|||
* @return The result of the multiplication. |
|||
*/ |
|||
Add<DdType::CUDD> operator*(Add<DdType::CUDD> 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. |
|||
*/ |
|||
Add<DdType::CUDD>& operator*=(Add<DdType::CUDD> 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. |
|||
*/ |
|||
Add<DdType::CUDD> operator-(Add<DdType::CUDD> const& other) const; |
|||
|
|||
/*! |
|||
* Subtracts the ADD from the constant zero function. |
|||
* |
|||
* @return The resulting function represented as a ADD. |
|||
*/ |
|||
Add<DdType::CUDD> operator-() 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. |
|||
*/ |
|||
Add<DdType::CUDD>& operator-=(Add<DdType::CUDD> 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. |
|||
*/ |
|||
Add<DdType::CUDD> operator/(Add<DdType::CUDD> 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. |
|||
*/ |
|||
Add<DdType::CUDD>& operator/=(Add<DdType::CUDD> 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. |
|||
*/ |
|||
Add<DdType::CUDD> equals(Add<DdType::CUDD> 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. |
|||
*/ |
|||
Add<DdType::CUDD> notEquals(Add<DdType::CUDD> 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. |
|||
*/ |
|||
Add<DdType::CUDD> less(Add<DdType::CUDD> 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. |
|||
*/ |
|||
Add<DdType::CUDD> lessOrEqual(Add<DdType::CUDD> 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. |
|||
*/ |
|||
Add<DdType::CUDD> greater(Add<DdType::CUDD> 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. |
|||
*/ |
|||
Add<DdType::CUDD> greaterOrEqual(Add<DdType::CUDD> 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. |
|||
*/ |
|||
Add<DdType::CUDD> pow(Add<DdType::CUDD> 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. |
|||
*/ |
|||
Add<DdType::CUDD> mod(Add<DdType::CUDD> 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. |
|||
*/ |
|||
Add<DdType::CUDD> logxy(Add<DdType::CUDD> const& other) const; |
|||
|
|||
/*! |
|||
* Retrieves the function that floors all values in the current ADD. |
|||
* |
|||
* @retur The resulting ADD. |
|||
*/ |
|||
Add<DdType::CUDD> floor() const; |
|||
|
|||
/*! |
|||
* Retrieves the function that ceils all values in the current ADD. |
|||
* |
|||
* @retur The resulting ADD. |
|||
*/ |
|||
Add<DdType::CUDD> 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. |
|||
*/ |
|||
Add<DdType::CUDD> minimum(Add<DdType::CUDD> 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. |
|||
*/ |
|||
Add<DdType::CUDD> maximum(Add<DdType::CUDD> const& other) const; |
|||
|
|||
/*! |
|||
* Sum-abstracts from the given meta variables. |
|||
* |
|||
* @param metaVariables The meta variables from which to abstract. |
|||
*/ |
|||
Add<DdType::CUDD> sumAbstract(std::set<storm::expressions::Variable> const& metaVariables) const; |
|||
|
|||
/*! |
|||
* Min-abstracts from the given meta variables. |
|||
* |
|||
* @param metaVariables The meta variables from which to abstract. |
|||
*/ |
|||
Add<DdType::CUDD> minAbstract(std::set<storm::expressions::Variable> const& metaVariables) const; |
|||
|
|||
/*! |
|||
* Max-abstracts from the given meta variables. |
|||
* |
|||
* @param metaVariables The meta variables from which to abstract. |
|||
*/ |
|||
Add<DdType::CUDD> maxAbstract(std::set<storm::expressions::Variable> const& metaVariables) 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(Add<DdType::CUDD> const& other, double precision, bool relative = true) const; |
|||
|
|||
/*! |
|||
* Swaps the given pairs of meta variables in the ADD. The pairs of meta variables must be guaranteed to have |
|||
* the same number of underlying ADD variables. |
|||
* |
|||
* @param metaVariablePairs A vector of meta variable pairs that are to be swapped for one another. |
|||
* @return The resulting ADD. |
|||
*/ |
|||
Add<DdType::CUDD> swapVariables(std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& metaVariablePairs) 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 summationMetaVariables The names of the meta variables over which to sum during the matrix- |
|||
* matrix multiplication. |
|||
* @return An ADD representing the result of the matrix-matrix multiplication. |
|||
*/ |
|||
Add<DdType::CUDD> multiplyMatrix(Add<DdType::CUDD> const& otherMatrix, std::set<storm::expressions::Variable> const& summationMetaVariables) 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. |
|||
*/ |
|||
Bdd<DdType::CUDD> greater(double 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. |
|||
*/ |
|||
Bdd<DdType::CUDD> greaterOrEqual(double 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. |
|||
*/ |
|||
Bdd<DdType::CUDD> less(double 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. |
|||
*/ |
|||
Bdd<DdType::CUDD> lessOrEqual(double 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. |
|||
*/ |
|||
Bdd<DdType::CUDD> 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. |
|||
*/ |
|||
Add<DdType::CUDD> constrain(Add<DdType::CUDD> 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. |
|||
*/ |
|||
Add<DdType::CUDD> restrict(Add<DdType::CUDD> const& constraint) const; |
|||
|
|||
/*! |
|||
* Retrieves the support of the current ADD. |
|||
* |
|||
* @return The support represented as a BDD. |
|||
*/ |
|||
Bdd<DdType::CUDD> getSupport() const override; |
|||
|
|||
/*! |
|||
* Retrieves the number of encodings that are mapped to a non-zero value. |
|||
* |
|||
* @return The number of encodings that are mapped to a non-zero value. |
|||
*/ |
|||
virtual uint_fast64_t getNonZeroCount() const override; |
|||
|
|||
/*! |
|||
* Retrieves the number of leaves of the ADD. |
|||
* |
|||
* @return The number of leaves of the ADD. |
|||
*/ |
|||
virtual uint_fast64_t getLeafCount() const override; |
|||
|
|||
/*! |
|||
* Retrieves the number of nodes necessary to represent the DD. |
|||
* |
|||
* @return The number of nodes in this DD. |
|||
*/ |
|||
virtual uint_fast64_t getNodeCount() const override; |
|||
|
|||
/*! |
|||
* Retrieves the lowest function value of any encoding. |
|||
* |
|||
* @return The lowest function value of any encoding. |
|||
*/ |
|||
double getMin() const; |
|||
|
|||
/*! |
|||
* Retrieves the highest function value of any encoding. |
|||
* |
|||
* @return The highest function value of any encoding. |
|||
*/ |
|||
double getMax() const; |
|||
|
|||
/*! |
|||
* Sets the function values of all encodings that have the given value of the meta variable to the given |
|||
* target value. |
|||
* |
|||
* @param metaVariable The meta variable that has to be equal to the given value. |
|||
* @param variableValue The value that the meta variable is supposed to have. This must be within the range |
|||
* of the meta variable. |
|||
* @param targetValue The new function value of the modified encodings. |
|||
*/ |
|||
void setValue(storm::expressions::Variable const& metaVariable, int_fast64_t variableValue, double targetValue); |
|||
|
|||
/*! |
|||
* Sets the function values of all encodings that have the given values of the two meta variables to the |
|||
* given target value. |
|||
* |
|||
* @param metaVariable1 The first meta variable that has to be equal to the first given |
|||
* value. |
|||
* @param variableValue1 The value that the first meta variable is supposed to have. This must be within the |
|||
* range of the meta variable. |
|||
* @param metaVariable2 The second meta variable that has to be equal to the second given |
|||
* value. |
|||
* @param variableValue2 The value that the second meta variable is supposed to have. This must be within |
|||
* the range of the meta variable. |
|||
* @param targetValue The new function value of the modified encodings. |
|||
*/ |
|||
void setValue(storm::expressions::Variable const& metaVariable1, int_fast64_t variableValue1, storm::expressions::Variable const& metaVariable2, int_fast64_t variableValue2, double targetValue); |
|||
|
|||
/*! |
|||
* Sets the function values of all encodings that have the given values of the given meta variables to the |
|||
* given target value. |
|||
* |
|||
* @param metaVariableToValueMap A mapping of meta variables to the values they are supposed to have. All |
|||
* values must be within the range of the respective meta variable. |
|||
* @param targetValue The new function value of the modified encodings. |
|||
*/ |
|||
void setValue(std::map<storm::expressions::Variable, int_fast64_t> const& metaVariableToValueMap = std::map<storm::expressions::Variable, int_fast64_t>(), double targetValue = 0); |
|||
|
|||
/*! |
|||
* Retrieves the value of the function when all meta variables are assigned the values of the given mapping. |
|||
* Note that the mapping must specify values for all meta variables contained in the DD. |
|||
* |
|||
* @param metaVariableToValueMap A mapping of meta variables to their values. |
|||
* @return The value of the function evaluated with the given input. |
|||
*/ |
|||
double getValue(std::map<storm::expressions::Variable, int_fast64_t> const& metaVariableToValueMap = std::map<storm::expressions::Variable, int_fast64_t>()) 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 override; |
|||
|
|||
/*! |
|||
* Converts the ADD to a vector. |
|||
* |
|||
* @return The vector that is represented by this ADD. |
|||
*/ |
|||
template<typename ValueType> |
|||
std::vector<ValueType> toVector() const; |
|||
|
|||
/*! |
|||
* Converts the ADD to a 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. |
|||
* @return The vector that is represented by this ADD. |
|||
*/ |
|||
template<typename ValueType> |
|||
std::vector<ValueType> toVector(storm::dd::Odd<DdType::CUDD> const& rowOdd) const; |
|||
|
|||
/*! |
|||
* Converts the ADD to a row-grouped vector. The given offset-labeled DD is used to determine the correct |
|||
* row group of each entry. Note that the group meta variables are assumed to be at the very top in the |
|||
* variable ordering. |
|||
* |
|||
* @param groupMetaVariables The meta variables responsible for the row-grouping. |
|||
* @param rowOdd The ODD used for determining the correct row. |
|||
* @return The vector that is represented by this ADD. |
|||
*/ |
|||
template<typename ValueType> |
|||
std::vector<ValueType> toVector(std::set<storm::expressions::Variable> const& groupMetaVariables, storm::dd::Odd<DdType::CUDD> const& rowOdd, std::vector<uint_fast64_t> groupOffsets) const; |
|||
|
|||
/*! |
|||
* Converts the ADD to a (sparse) double matrix. All contained non-primed variables are assumed to encode the |
|||
* row, whereas all primed variables are assumed to encode the column. |
|||
* |
|||
* @return The matrix that is represented by this ADD. |
|||
*/ |
|||
storm::storage::SparseMatrix<double> toMatrix() const; |
|||
|
|||
/*! |
|||
* Converts the ADD to a (sparse) double matrix. All contained non-primed variables are assumed to encode the |
|||
* row, whereas all primed variables are assumed to encode the column. The given offset-labeled DDs are used |
|||
* to determine the correct row and column, respectively, for each entry. |
|||
* |
|||
* @param rowOdd The ODD used for determining the correct row. |
|||
* @param columnOdd The ODD used for determining the correct column. |
|||
* @return The matrix that is represented by this ADD. |
|||
*/ |
|||
storm::storage::SparseMatrix<double> toMatrix(storm::dd::Odd<DdType::CUDD> const& rowOdd, storm::dd::Odd<DdType::CUDD> const& columnOdd) const; |
|||
|
|||
/*! |
|||
* Converts the ADD to a (sparse) double matrix. The given offset-labeled DDs are used to determine the |
|||
* correct row and column, respectively, for each entry. |
|||
* |
|||
* @param rowMetaVariables The meta variables that encode the rows of the matrix. |
|||
* @param columnMetaVariables The meta variables that encode the columns of the matrix. |
|||
* @param rowOdd The ODD used for determining the correct row. |
|||
* @param columnOdd The ODD used for determining the correct column. |
|||
* @return The matrix that is represented by this ADD. |
|||
*/ |
|||
storm::storage::SparseMatrix<double> toMatrix(std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, storm::dd::Odd<DdType::CUDD> const& rowOdd, storm::dd::Odd<DdType::CUDD> const& columnOdd) const; |
|||
|
|||
/*! |
|||
* Converts the ADD to a row-grouped (sparse) double matrix. The given offset-labeled DDs are used to |
|||
* determine the correct row and column, respectively, for each entry. Note: this function assumes that |
|||
* the meta variables used to distinguish different row groups are at the very top of the ADD. |
|||
* |
|||
* @param groupMetaVariables The meta variables that are used to distinguish different row groups. |
|||
* @param rowOdd The ODD used for determining the correct row. |
|||
* @param columnOdd The ODD used for determining the correct column. |
|||
* @return The matrix that is represented by this ADD. |
|||
*/ |
|||
storm::storage::SparseMatrix<double> toMatrix(std::set<storm::expressions::Variable> const& groupMetaVariables, storm::dd::Odd<DdType::CUDD> const& rowOdd, storm::dd::Odd<DdType::CUDD> const& columnOdd) const; |
|||
|
|||
/*! |
|||
* Converts the ADD to a row-grouped (sparse) double matrix and the given vector to a row-grouped vector. |
|||
* The given offset-labeled DDs are used to determine the correct row and column, respectively, for each |
|||
* entry. Note: this function assumes that the meta variables used to distinguish different row groups are |
|||
* at the very top of the ADD. |
|||
* |
|||
* @param vector The symbolic vector to convert. |
|||
* @param rowGroupSizes A vector specifying the sizes of the row groups. |
|||
* @param groupMetaVariables The meta variables that are used to distinguish different row groups. |
|||
* @param rowOdd The ODD used for determining the correct row. |
|||
* @param columnOdd The ODD used for determining the correct column. |
|||
* @return The matrix that is represented by this ADD. |
|||
*/ |
|||
std::pair<storm::storage::SparseMatrix<double>, std::vector<double>> toMatrixVector(storm::dd::Add<storm::dd::DdType::CUDD> const& vector, std::vector<uint_fast64_t>&& rowGroupSizes, std::set<storm::expressions::Variable> const& groupMetaVariables, storm::dd::Odd<DdType::CUDD> const& rowOdd, storm::dd::Odd<DdType::CUDD> const& columnOdd) 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. |
|||
*/ |
|||
void exportToDot(std::string const& filename = "") const override; |
|||
|
|||
/*! |
|||
* Retrieves an iterator that points to the first meta variable assignment with a non-zero function value. |
|||
* |
|||
* @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. |
|||
*/ |
|||
DdForwardIterator<DdType::CUDD> begin(bool enumerateDontCareMetaVariables = true) const; |
|||
|
|||
/*! |
|||
* Retrieves an iterator that points past the end of the container. |
|||
* |
|||
* @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. |
|||
*/ |
|||
DdForwardIterator<DdType::CUDD> end(bool enumerateDontCareMetaVariables = true) const; |
|||
|
|||
friend std::ostream & operator<<(std::ostream& out, const Add<DdType::CUDD>& add); |
|||
|
|||
/*! |
|||
* 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. |
|||
*/ |
|||
Bdd<DdType::CUDD> toBdd() const; |
|||
|
|||
private: |
|||
|
|||
/*! |
|||
* Retrieves the CUDD ADD object associated with this ADD. |
|||
* |
|||
* @return The CUDD ADD object associated with this ADD. |
|||
*/ |
|||
ADD getCuddAdd() const; |
|||
|
|||
/*! |
|||
* Retrieves the raw DD node of CUDD associated with this ADD. |
|||
* |
|||
* @return The DD node of CUDD associated with this ADD. |
|||
*/ |
|||
DdNode* getCuddDdNode() const; |
|||
|
|||
/*! |
|||
* Creates an ADD that encapsulates the given CUDD ADD. |
|||
* |
|||
* @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. |
|||
*/ |
|||
Add(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, ADD cuddAdd, std::set<storm::expressions::Variable> const& containedMetaVariables = std::set<storm::expressions::Variable>()); |
|||
|
|||
/*! |
|||
* Converts the ADD to a row-grouped (sparse) double matrix. If the optional vector is given, it is also |
|||
* translated to an explicit row-grouped vector with the same row-grouping. The given offset-labeled DDs |
|||
* are used to determine the correct row and column, respectively, for each entry. Note: this function |
|||
* assumes that the meta variables used to distinguish different row groups are at the very top of the ADD. |
|||
* |
|||
* @param rowMetaVariables The meta variables that encode the rows of the matrix. |
|||
* @param columnMetaVariables The meta variables that encode the columns of the matrix. |
|||
* @param groupMetaVariables The meta variables that are used to distinguish different row groups. |
|||
* @param rowOdd The ODD used for determining the correct row. |
|||
* @param columnOdd The ODD used for determining the correct column. |
|||
* @return The matrix that is represented by this ADD and and a vector corresponding to the symbolic vector |
|||
* (if it was given). |
|||
*/ |
|||
storm::storage::SparseMatrix<double> toMatrix(std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::set<storm::expressions::Variable> const& groupMetaVariables, storm::dd::Odd<DdType::CUDD> const& rowOdd, storm::dd::Odd<DdType::CUDD> const& columnOdd) const; |
|||
|
|||
/*! |
|||
* Converts the ADD to a row-grouped (sparse) double matrix and the given vector to an equally row-grouped |
|||
* explicit vector. The given offset-labeled DDs are used to determine the correct row and column, |
|||
* respectively, for each entry. Note: this function assumes that the meta variables used to distinguish |
|||
* different row groups are at the very top of the ADD. |
|||
* |
|||
* @param vector The vector that is to be transformed to an equally grouped explicit vector. |
|||
* @param rowGroupSizes A vector specifying the sizes of the row groups. |
|||
* @param rowMetaVariables The meta variables that encode the rows of the matrix. |
|||
* @param columnMetaVariables The meta variables that encode the columns of the matrix. |
|||
* @param groupMetaVariables The meta variables that are used to distinguish different row groups. |
|||
* @param rowOdd The ODD used for determining the correct row. |
|||
* @param columnOdd The ODD used for determining the correct column. |
|||
* @return The matrix that is represented by this ADD and and a vector corresponding to the symbolic vector |
|||
* (if it was given). |
|||
*/ |
|||
std::pair<storm::storage::SparseMatrix<double>,std::vector<double>> toMatrixVector(storm::dd::Add<storm::dd::DdType::CUDD> const& vector, std::vector<uint_fast64_t>&& rowGroupSizes, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::set<storm::expressions::Variable> const& groupMetaVariables, storm::dd::Odd<DdType::CUDD> const& rowOdd, storm::dd::Odd<DdType::CUDD> const& columnOdd) const; |
|||
|
|||
/*! |
|||
* Helper function to convert the DD into a (sparse) matrix. |
|||
* |
|||
* @param dd The DD to convert. |
|||
* @param rowIndications A vector indicating at which position in the columnsAndValues vector the entries |
|||
* of row i start. Note: this vector is modified in the computation. More concretely, each entry i in the |
|||
* vector will be increased by the number of entries in the row. This can be used to count the number |
|||
* of entries in each row. If the values are not to be modified, a copy needs to be provided or the entries |
|||
* need to be restored afterwards. |
|||
* @param columnsAndValues The vector that will hold the columns and values of non-zero entries upon successful |
|||
* completion. |
|||
* @param rowGroupOffsets The row offsets at which a given row group starts. |
|||
* @param rowOdd The ODD used for the row translation. |
|||
* @param columnOdd The ODD used for the column translation. |
|||
* @param currentRowLevel The currently considered row level in the DD. |
|||
* @param currentColumnLevel The currently considered row level in the DD. |
|||
* @param maxLevel The number of levels that need to be considered. |
|||
* @param currentRowOffset The current row offset. |
|||
* @param currentColumnOffset The current row offset. |
|||
* @param ddRowVariableIndices The (sorted) indices of all DD row variables that need to be considered. |
|||
* @param ddColumnVariableIndices The (sorted) indices of all DD row variables that need to be considered. |
|||
* @param generateValues If set to true, the vector columnsAndValues is filled with the actual entries, which |
|||
* only works if the offsets given in rowIndications are already correct. If they need to be computed first, |
|||
* this flag needs to be false. |
|||
*/ |
|||
void toMatrixRec(DdNode const* dd, std::vector<uint_fast64_t>& rowIndications, std::vector<storm::storage::MatrixEntry<uint_fast64_t, double>>& columnsAndValues, std::vector<uint_fast64_t> const& rowGroupOffsets, Odd<DdType::CUDD> const& rowOdd, Odd<DdType::CUDD> const& columnOdd, uint_fast64_t currentRowLevel, uint_fast64_t currentColumnLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, uint_fast64_t currentColumnOffset, std::vector<uint_fast64_t> const& ddRowVariableIndices, std::vector<uint_fast64_t> const& ddColumnVariableIndices, bool generateValues = true) const; |
|||
|
|||
/*! |
|||
* Helper function to convert the DD into an (explicit) vector. |
|||
* |
|||
* @param dd The DD to convert. |
|||
* @param result The vector that will hold the values upon successful completion. |
|||
* @param rowGroupOffsets The row offsets at which a given row group starts. |
|||
* @param rowOdd The ODD used for the row translation. |
|||
* @param currentRowLevel The currently considered row level in the DD. |
|||
* @param maxLevel The number of levels that need to be considered. |
|||
* @param currentRowOffset The current row offset. |
|||
* @param ddRowVariableIndices The (sorted) indices of all DD row variables that need to be considered. |
|||
*/ |
|||
template<typename ValueType> |
|||
void toVectorRec(DdNode const* dd, std::vector<ValueType>& result, std::vector<uint_fast64_t> const& rowGroupOffsets, Odd<DdType::CUDD> const& rowOdd, uint_fast64_t currentRowLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, std::vector<uint_fast64_t> const& ddRowVariableIndices) const; |
|||
|
|||
/*! |
|||
* Splits the given matrix DD into the groups using the given group variables. |
|||
* |
|||
* @param dd The DD to split. |
|||
* @param groups A vector that is to be filled with the DDs for the individual groups. |
|||
* @param ddGroupVariableIndices The (sorted) indices of all DD group variables that need to be considered. |
|||
* @param currentLevel The currently considered level in the DD. |
|||
* @param maxLevel The number of levels that need to be considered. |
|||
* @param remainingMetaVariables The meta variables that remain in the DDs after the groups have been split. |
|||
*/ |
|||
void splitGroupsRec(DdNode* dd, std::vector<Add<DdType::CUDD>>& groups, std::vector<uint_fast64_t> const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::set<storm::expressions::Variable> const& remainingMetaVariables) const; |
|||
|
|||
/*! |
|||
* Splits the given matrix and vector DDs into the groups using the given group variables. |
|||
* |
|||
* @param dd1 The matrix DD to split. |
|||
* @param dd2 The vector DD to split. |
|||
* @param groups A vector that is to be filled with the pairs of matrix/vector DDs for the individual groups. |
|||
* @param ddGroupVariableIndices The (sorted) indices of all DD group variables that need to be considered. |
|||
* @param currentLevel The currently considered level in the DD. |
|||
* @param maxLevel The number of levels that need to be considered. |
|||
* @param remainingMetaVariables1 The meta variables that remain in the matrix DD after the groups have been split. |
|||
* @param remainingMetaVariables2 The meta variables that remain in the vector DD after the groups have been split. |
|||
*/ |
|||
void splitGroupsRec(DdNode* dd1, DdNode* dd2, std::vector<std::pair<Add<DdType::CUDD>, Add<DdType::CUDD>>>& groups, std::vector<uint_fast64_t> const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::set<storm::expressions::Variable> const& remainingMetaVariables1, std::set<storm::expressions::Variable> const& remainingMetaVariables2) const; |
|||
|
|||
/*! |
|||
* Adds the current (DD-based) vector to the given explicit one. |
|||
* |
|||
* @param odd The ODD used for the translation. |
|||
* @param ddVariableIndices The (sorted) indices of all DD variables that need to be considered. |
|||
* @param targetVector The vector to which the translated DD-based vector is to be added. |
|||
*/ |
|||
template<typename ValueType> |
|||
void addToVector(Odd<DdType::CUDD> const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<ValueType>& targetVector) const; |
|||
|
|||
/*! |
|||
* Performs a recursive step to perform the given function between the given DD-based vector and the given |
|||
* explicit vector. |
|||
* |
|||
* @param dd The DD to add to the explicit vector. |
|||
* @param currentLevel The currently considered level in the DD. |
|||
* @param maxLevel The number of levels that need to be considered. |
|||
* @param currentOffset The current offset. |
|||
* @param odd The ODD used for the translation. |
|||
* @param ddVariableIndices The (sorted) indices of all DD variables that need to be considered. |
|||
* @param targetVector The vector to which the translated DD-based vector is to be added. |
|||
*/ |
|||
template<typename ValueType> |
|||
void modifyVectorRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd<DdType::CUDD> const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<ValueType>& targetVector, std::function<ValueType (ValueType const&, double const&)> const& function) const; |
|||
|
|||
/*! |
|||
* Builds an ADD representing the given vector. |
|||
* |
|||
* @param ddManager The manager responsible for the ADD. |
|||
* @param values The vector that is to be represented by the ADD. |
|||
* @param odd The ODD used for the translation. |
|||
* @param metaVariables The meta variables used for the translation. |
|||
* @return The resulting (CUDD) ADD. |
|||
*/ |
|||
template<typename ValueType> |
|||
static ADD fromVector(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, std::vector<ValueType> const& values, Odd<DdType::CUDD> const& odd, std::set<storm::expressions::Variable> const& metaVariables); |
|||
|
|||
/*! |
|||
* Builds an ADD representing the given vector. |
|||
* |
|||
* @param manager The manager responsible for the ADD. |
|||
* @param currentOffset The current offset in the vector. |
|||
* @param currentLevel The current level in the DD. |
|||
* @param maxLevel The maximal level in the DD. |
|||
* @param values The vector that is to be represented by the ADD. |
|||
* @param odd The ODD used for the translation. |
|||
* @param ddVariableIndices The (sorted) list of DD variable indices to use. |
|||
* @return The resulting (CUDD) ADD node. |
|||
*/ |
|||
template<typename ValueType> |
|||
static DdNode* fromVectorRec(::DdManager* manager, uint_fast64_t& currentOffset, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector<ValueType> const& values, Odd<DdType::CUDD> const& odd, std::vector<uint_fast64_t> const& ddVariableIndices); |
|||
|
|||
// The ADD created by CUDD. |
|||
ADD cuddAdd; |
|||
}; |
|||
} |
|||
} |
|||
|
|||
#endif /* STORM_STORAGE_DD_CUDDADD_H_ */ |
|||
@ -0,0 +1,757 @@ |
|||
#include "src/storage/dd/cudd/InternalCuddAdd.h"
|
|||
|
|||
#include "src/storage/dd/cudd/CuddOdd.h"
|
|||
|
|||
#include "src/storage/dd/cudd/InternalCuddDdManager.h"
|
|||
#include "src/storage/dd/cudd/InternalCuddBdd.h"
|
|||
|
|||
#include "src/storage/SparseMatrix.h"
|
|||
|
|||
#include "src/utility/constants.h"
|
|||
|
|||
namespace storm { |
|||
namespace dd { |
|||
template<typename ValueType> |
|||
bool InternalAdd<DdType::CUDD, ValueType>::operator==(InternalAdd<DdType::CUDD, ValueType> const& other) const { |
|||
return this->getCuddAdd() == other.getCuddAdd(); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
bool InternalAdd<DdType::CUDD, ValueType>::operator!=(InternalAdd<DdType::CUDD, ValueType> const& other) const { |
|||
return !(*this == other); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::ite(InternalAdd<DdType::CUDD, ValueType> const& thenDd, InternalAdd<DdType::CUDD, ValueType> const& elseDd) const { |
|||
return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().Ite(thenDd.getCuddAdd(), elseDd.getCuddAdd())); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::operator!() const { |
|||
return InternalAdd<DdType::CUDD, ValueType>(ddManager, ~this->getCuddAdd()); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::operator||(InternalAdd<DdType::CUDD, ValueType> const& other) const { |
|||
return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd() | other.getCuddAdd()); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
InternalAdd<DdType::CUDD, ValueType>& InternalAdd<DdType::CUDD, ValueType>::operator|=(InternalAdd<DdType::CUDD, ValueType> const& other) { |
|||
this->cuddAdd = this->getCuddAdd() | other.getCuddAdd(); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::operator+(InternalAdd<DdType::CUDD, ValueType> const& other) const { |
|||
return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd() + other.getCuddAdd()); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
InternalAdd<DdType::CUDD, ValueType>& InternalAdd<DdType::CUDD, ValueType>::operator+=(InternalAdd<DdType::CUDD, ValueType> const& other) { |
|||
this->cuddAdd = this->getCuddAdd() + other.getCuddAdd(); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::operator*(InternalAdd<DdType::CUDD, ValueType> const& other) const { |
|||
return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd() * other.getCuddAdd()); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
InternalAdd<DdType::CUDD, ValueType>& InternalAdd<DdType::CUDD, ValueType>::operator*=(InternalAdd<DdType::CUDD, ValueType> const& other) { |
|||
this->cuddAdd = this->getCuddAdd() * other.getCuddAdd(); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::operator-(InternalAdd<DdType::CUDD, ValueType> const& other) const { |
|||
return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd() - other.getCuddAdd()); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
InternalAdd<DdType::CUDD, ValueType>& InternalAdd<DdType::CUDD, ValueType>::operator-=(InternalAdd<DdType::CUDD, ValueType> const& other) { |
|||
this->cuddAdd = this->getCuddAdd() - other.getCuddAdd(); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::operator/(InternalAdd<DdType::CUDD, ValueType> const& other) const { |
|||
return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd() / other.getCuddAdd()); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
InternalAdd<DdType::CUDD, ValueType>& InternalAdd<DdType::CUDD, ValueType>::operator/=(InternalAdd<DdType::CUDD, ValueType> const& other) { |
|||
this->cuddAdd = this->getCuddAdd() / other.getCuddAdd(); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::equals(InternalAdd<DdType::CUDD, ValueType> const& other) const { |
|||
return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().Equals(other.getCuddAdd())); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::notEquals(InternalAdd<DdType::CUDD, ValueType> const& other) const { |
|||
return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().NotEquals(other.getCuddAdd())); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::less(InternalAdd<DdType::CUDD, ValueType> const& other) const { |
|||
return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().LessThan(other.getCuddAdd())); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::lessOrEqual(InternalAdd<DdType::CUDD, ValueType> const& other) const { |
|||
return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().LessThanOrEqual(other.getCuddAdd())); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::greater(InternalAdd<DdType::CUDD, ValueType> const& other) const { |
|||
return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().GreaterThan(other.getCuddAdd())); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::greaterOrEqual(InternalAdd<DdType::CUDD, ValueType> const& other) const { |
|||
return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().GreaterThanOrEqual(other.getCuddAdd())); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::pow(InternalAdd<DdType::CUDD, ValueType> const& other) const { |
|||
return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().Pow(other.getCuddAdd())); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::mod(InternalAdd<DdType::CUDD, ValueType> const& other) const { |
|||
return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().Mod(other.getCuddAdd())); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::logxy(InternalAdd<DdType::CUDD, ValueType> const& other) const { |
|||
return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().LogXY(other.getCuddAdd())); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::floor() const { |
|||
return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().Floor()); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::ceil() const { |
|||
return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().Ceil()); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::minimum(InternalAdd<DdType::CUDD, ValueType> const& other) const { |
|||
return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().Minimum(other.getCuddAdd())); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::maximum(InternalAdd<DdType::CUDD, ValueType> const& other) const { |
|||
return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().Maximum(other.getCuddAdd())); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::sumAbstract(InternalBdd<DdType::CUDD> const& cube) const { |
|||
return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().ExistAbstract(cube.getCuddBdd())); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::minAbstract(InternalBdd<DdType::CUDD> const& cube) const { |
|||
return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().MinAbstract(cube.getCuddBdd())); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::maxAbstract(InternalBdd<DdType::CUDD> const& cube) const { |
|||
return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().MaxAbstract(cube.getCuddBdd())); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
bool InternalAdd<DdType::CUDD, ValueType>::equalModuloPrecision(InternalAdd<DdType::CUDD, ValueType> const& other, double precision, bool relative) const { |
|||
if (relative) { |
|||
return this->getCuddAdd().EqualSupNormRel(other.getCuddAdd(), precision); |
|||
} else { |
|||
return this->getCuddAdd().EqualSupNorm(other.getCuddAdd(), precision); |
|||
} |
|||
}; |
|||
|
|||
template<typename ValueType> |
|||
InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::swapVariables(std::vector<InternalAdd<DdType::CUDD, ValueType>> const& from, std::vector<InternalAdd<DdType::CUDD, ValueType>> const& to) const { |
|||
std::vector<ADD> fromAdd; |
|||
std::vector<ADD> toAdd; |
|||
for (auto it1 = from.begin(), ite1 = from.end(), it2 = to.begin(); it1 != ite1; ++it1, ++it2) { |
|||
fromAdd.push_back(it1->getCuddAdd()); |
|||
toAdd.push_back(it2->getCuddAdd()); |
|||
} |
|||
return InternalBdd<DdType::CUDD>(ddManager, this->getCuddBdd().SwapVariables(fromAdd, toAdd)); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::multiplyMatrix(InternalAdd<DdType::CUDD, ValueType> const& otherMatrix, std::vector<InternalAdd<DdType::CUDD, ValueType>> const& summationDdVariables) const { |
|||
// Create the CUDD summation variables.
|
|||
std::vector<ADD> summationAdds; |
|||
for (auto const& ddVariable : summationDdVariables) { |
|||
summationAdds.push_back(ddVariable.toAdd().getCuddAdd()); |
|||
} |
|||
|
|||
return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().MatrixMultiply(otherMatrix.getCuddAdd(), summationAdds)); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, ValueType>::greater(ValueType const& value) const { |
|||
return InternalBdd<DdType::CUDD>(ddManager, this->getCuddAdd().BddStrictThreshold(value)); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, ValueType>::greaterOrEqual(ValueType const& value) const { |
|||
return InternalBdd<DdType::CUDD>(ddManager, this->getCuddAdd().BddThreshold(value)); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, ValueType>::less(ValueType const& value) const { |
|||
return InternalBdd<DdType::CUDD>(ddManager, ~this->getCuddAdd().BddThreshold(value)); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, ValueType>::lessOrEqual(ValueType const& value) const { |
|||
return InternalBdd<DdType::CUDD>(ddManager, ~this->getCuddAdd().BddStrictThreshold(value)); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, ValueType>::notZero() const { |
|||
return this->toBdd(); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::constrain(InternalAdd<DdType::CUDD, ValueType> const& constraint) const { |
|||
return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().Constrain(constraint.getCuddAdd())); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::restrict(InternalAdd<DdType::CUDD, ValueType> const& constraint) const { |
|||
return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().Restrict(constraint.getCuddAdd())); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, ValueType>::getSupport() const { |
|||
return InternalBdd<DdType::CUDD>(ddManager, this->getCuddAdd().Support()); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
uint_fast64_t InternalAdd<DdType::CUDD, ValueType>::getNonZeroCount(uint_fast64_t numberOfDdVariables) const { |
|||
return static_cast<uint_fast64_t>(this->getCuddAdd().CountMinterm(static_cast<int>(numberOfDdVariables))); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
uint_fast64_t InternalAdd<DdType::CUDD, ValueType>::getLeafCount() const { |
|||
return static_cast<uint_fast64_t>(this->getCuddAdd().CountLeaves()); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
uint_fast64_t InternalAdd<DdType::CUDD, ValueType>::getNodeCount() const { |
|||
return static_cast<uint_fast64_t>(this->getCuddAdd().nodeCount()); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
ValueType InternalAdd<DdType::CUDD, ValueType>::getMin() const { |
|||
ADD constantMinAdd = this->getCuddAdd().FindMin(); |
|||
return static_cast<double>(Cudd_V(constantMinAdd.getNode())); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
ValueType InternalAdd<DdType::CUDD, ValueType>::getMax() const { |
|||
ADD constantMaxAdd = this->getCuddAdd().FindMax(); |
|||
return static_cast<double>(Cudd_V(constantMaxAdd.getNode())); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, ValueType>::toBdd() const { |
|||
return InternalBdd<DdType::CUDD>(ddManager, this->getCuddAdd().BddPattern()); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
bool InternalAdd<DdType::CUDD, ValueType>::isOne() const { |
|||
return this->getCuddAdd().IsOne(); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
bool InternalAdd<DdType::CUDD, ValueType>::isZero() const { |
|||
return this->getCuddAdd().IsZero(); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
bool InternalAdd<DdType::CUDD, ValueType>::isConstant() const { |
|||
return Cudd_IsConstant(this->getCuddAdd().getNode()); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
uint_fast64_t InternalAdd<DdType::CUDD, ValueType>::getIndex() const { |
|||
return static_cast<uint_fast64_t>(this->getCuddAdd().NodeReadIndex()); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
void InternalAdd<DdType::CUDD, ValueType>::exportToDot(std::string const& filename, std::vector<std::string> const& ddVariableNamesAsStrings) const { |
|||
// Build the name input of the DD.
|
|||
std::vector<char*> ddNames; |
|||
std::string ddName("f"); |
|||
ddNames.push_back(new char[ddName.size() + 1]); |
|||
std::copy(ddName.c_str(), ddName.c_str() + 2, ddNames.back()); |
|||
|
|||
// Now build the variables names.
|
|||
std::vector<char*> ddVariableNames; |
|||
for (auto const& element : ddVariableNamesAsStrings) { |
|||
ddVariableNames.push_back(new char[element.size() + 1]); |
|||
std::copy(element.c_str(), element.c_str() + element.size() + 1, ddVariableNames.back()); |
|||
} |
|||
|
|||
// Open the file, dump the DD and close it again.
|
|||
FILE* filePointer = fopen(filename.c_str() , "w"); |
|||
std::vector<ADD> cuddAddVector = { this->getCuddAdd() }; |
|||
this->getDdManager()->getCuddManager().DumpDot(cuddAddVector, &ddVariableNames[0], &ddNames[0], filePointer); |
|||
fclose(filePointer); |
|||
|
|||
// Finally, delete the names.
|
|||
for (char* element : ddNames) { |
|||
delete[] element; |
|||
} |
|||
for (char* element : ddVariableNames) { |
|||
delete[] element; |
|||
} |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
AddIterator<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::begin(std::set<storm::expressions::Variable> const& metaVariables, bool enumerateDontCareMetaVariables) const { |
|||
int* cube; |
|||
double value; |
|||
DdGen* generator = this->getCuddAdd().FirstCube(&cube, &value); |
|||
return AddIterator<DdType::CUDD, ValueType>(ddManager, generator, cube, value, (Cudd_IsGenEmpty(generator) != 0), &metaVariables, enumerateDontCareMetaVariables); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
AddIterator<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::end(bool enumerateDontCareMetaVariables) const { |
|||
return AddIterator<DdType::CUDD, ValueType>(ddManager, nullptr, nullptr, 0, true, nullptr, enumerateDontCareMetaVariables); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
ADD InternalAdd<DdType::CUDD, ValueType>::getCuddAdd() const { |
|||
return this->cuddAdd; |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
DdNode* InternalAdd<DdType::CUDD, ValueType>::getCuddDdNode() const { |
|||
return this->getCuddAdd().getNode(); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
std::vector<ValueType> InternalAdd<DdType::CUDD, ValueType>::toVector(std::vector<uint_fast64_t> const& ddGroupVariableIndices, storm::dd::Odd<DdType::CUDD> const& rowOdd, std::vector<uint_fast64_t> const& ddRowVariableIndices, std::vector<uint_fast64_t> const& groupOffsets) const { |
|||
// Start by splitting the symbolic vector into groups.
|
|||
std::vector<InternalAdd<DdType::CUDD, ValueType>> groups; |
|||
splitGroupsRec(this->getCuddDdNode(), groups, ddGroupVariableIndices, 0, ddGroupVariableIndices.size()); |
|||
|
|||
// Now iterate over the groups and add them to the resulting vector.
|
|||
std::vector<ValueType> result(groupOffsets.back(), storm::utility::zero<ValueType>()); |
|||
for (uint_fast64_t i = 0; i < groups.size(); ++i) { |
|||
toVectorRec(groups[i].getCuddDdNode(), result, groupOffsets, rowOdd, 0, ddRowVariableIndices.size(), 0, ddRowVariableIndices); |
|||
} |
|||
|
|||
return result; |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
void InternalAdd<DdType::CUDD, ValueType>::addToExplicitVector(storm::dd::Odd<DdType::CUDD> const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<ValueType>& targetVector) const { |
|||
composeVector(odd, ddVariableIndices, targetVector, std::plus<ValueType>()); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
void InternalAdd<DdType::CUDD, ValueType>::composeVector(storm::dd::Odd<DdType::CUDD> const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<ValueType>& targetVector, std::function<ValueType (ValueType const&, ValueType const&)> const& function) const { |
|||
composeVectorRec(this->getCuddDdNode(), 0, ddVariableIndices.size(), 0, odd, ddVariableIndices, targetVector, function); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
void InternalAdd<DdType::CUDD, ValueType>::composeVectorRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd<DdType::CUDD> const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<ValueType>& targetVector, std::function<ValueType (ValueType const&, ValueType const&)> const& function) const { |
|||
// For the empty DD, we do not need to add any entries.
|
|||
if (dd == Cudd_ReadZero(this->getDdManager()->getCuddManager().getManager())) { |
|||
return; |
|||
} |
|||
|
|||
// If we are at the maximal level, the value to be set is stored as a constant in the DD.
|
|||
if (currentLevel == maxLevel) { |
|||
targetVector[currentOffset] = function(targetVector[currentOffset], Cudd_V(dd)); |
|||
} else if (ddVariableIndices[currentLevel] < dd->index) { |
|||
// If we skipped a level, we need to enumerate the explicit entries for the case in which the bit is set
|
|||
// and for the one in which it is not set.
|
|||
composeVectorRec(dd, currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, targetVector, function); |
|||
composeVectorRec(dd, currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, targetVector, function); |
|||
} else { |
|||
// Otherwise, we simply recursively call the function for both (different) cases.
|
|||
composeVectorRec(Cudd_E(dd), currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, targetVector, function); |
|||
composeVectorRec(Cudd_T(dd), currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, targetVector, function); |
|||
} |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
void InternalAdd<DdType::CUDD, ValueType>::toVectorRec(DdNode const* dd, std::vector<ValueType>& result, std::vector<uint_fast64_t> const& rowGroupOffsets, Odd<DdType::CUDD> const& rowOdd, uint_fast64_t currentRowLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, std::vector<uint_fast64_t> const& ddRowVariableIndices) const { |
|||
// For the empty DD, we do not need to add any entries.
|
|||
if (dd == Cudd_ReadZero(ddManager->getCuddManager().getManager())) { |
|||
return; |
|||
} |
|||
|
|||
// If we are at the maximal level, the value to be set is stored as a constant in the DD.
|
|||
if (currentRowLevel == maxLevel) { |
|||
result[rowGroupOffsets[currentRowOffset]] = Cudd_V(dd); |
|||
} else if (ddRowVariableIndices[currentRowLevel] < dd->index) { |
|||
toVectorRec(dd, result, rowGroupOffsets, rowOdd.getElseSuccessor(), currentRowLevel + 1, maxLevel, currentRowOffset, ddRowVariableIndices); |
|||
toVectorRec(dd, result, rowGroupOffsets, rowOdd.getThenSuccessor(), currentRowLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), ddRowVariableIndices); |
|||
} else { |
|||
toVectorRec(Cudd_E(dd), result, rowGroupOffsets, rowOdd.getElseSuccessor(), currentRowLevel + 1, maxLevel, currentRowOffset, ddRowVariableIndices); |
|||
toVectorRec(Cudd_T(dd), result, rowGroupOffsets, rowOdd.getThenSuccessor(), currentRowLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), ddRowVariableIndices); |
|||
} |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
storm::storage::SparseMatrix<ValueType> InternalAdd<DdType::CUDD, ValueType>::toMatrix(storm::dd::Odd<DdType::CUDD> const& rowOdd, std::vector<uint_fast64_t> const& ddRowVariableIndices, storm::dd::Odd<DdType::CUDD> const& columnOdd, std::vector<uint_fast64_t> const& ddColumnVariableIndices) const { |
|||
// Prepare the vectors that represent the matrix.
|
|||
std::vector<uint_fast64_t> rowIndications(rowOdd.getTotalOffset() + 1); |
|||
std::vector<storm::storage::MatrixEntry<uint_fast64_t, double>> columnsAndValues(this->getNonZeroCount()); |
|||
|
|||
// Create a trivial row grouping.
|
|||
std::vector<uint_fast64_t> trivialRowGroupIndices(rowIndications.size()); |
|||
uint_fast64_t i = 0; |
|||
for (auto& entry : trivialRowGroupIndices) { |
|||
entry = i; |
|||
++i; |
|||
} |
|||
|
|||
// Use the toMatrixRec function to compute the number of elements in each row. Using the flag, we prevent
|
|||
// it from actually generating the entries in the entry vector.
|
|||
toMatrixRec(this->getCuddDdNode(), rowIndications, columnsAndValues, trivialRowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, false); |
|||
|
|||
// TODO: counting might be faster by just summing over the primed variables and then using the ODD to convert
|
|||
// the resulting (DD) vector to an explicit vector.
|
|||
|
|||
// Now that we computed the number of entries in each row, compute the corresponding offsets in the entry vector.
|
|||
uint_fast64_t tmp = 0; |
|||
uint_fast64_t tmp2 = 0; |
|||
for (uint_fast64_t i = 1; i < rowIndications.size(); ++i) { |
|||
tmp2 = rowIndications[i]; |
|||
rowIndications[i] = rowIndications[i - 1] + tmp; |
|||
std::swap(tmp, tmp2); |
|||
} |
|||
rowIndications[0] = 0; |
|||
|
|||
// Now actually fill the entry vector.
|
|||
toMatrixRec(this->getCuddDdNode(), rowIndications, columnsAndValues, trivialRowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, true); |
|||
|
|||
// Since the last call to toMatrixRec modified the rowIndications, we need to restore the correct values.
|
|||
for (uint_fast64_t i = rowIndications.size() - 1; i > 0; --i) { |
|||
rowIndications[i] = rowIndications[i - 1]; |
|||
} |
|||
rowIndications[0] = 0; |
|||
|
|||
// Construct matrix and return result.
|
|||
return storm::storage::SparseMatrix<double>(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(trivialRowGroupIndices), false); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
void InternalAdd<DdType::CUDD, ValueType>::toMatrixRec(DdNode const* dd, std::vector<uint_fast64_t>& rowIndications, std::vector<storm::storage::MatrixEntry<uint_fast64_t, double>>& columnsAndValues, std::vector<uint_fast64_t> const& rowGroupOffsets, Odd<DdType::CUDD> const& rowOdd, Odd<DdType::CUDD> const& columnOdd, uint_fast64_t currentRowLevel, uint_fast64_t currentColumnLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, uint_fast64_t currentColumnOffset, std::vector<uint_fast64_t> const& ddRowVariableIndices, std::vector<uint_fast64_t> const& ddColumnVariableIndices, bool generateValues) const { |
|||
// For the empty DD, we do not need to add any entries.
|
|||
if (dd == Cudd_ReadZero(this->getDdManager()->getCuddManager().getManager())) { |
|||
return; |
|||
} |
|||
|
|||
// If we are at the maximal level, the value to be set is stored as a constant in the DD.
|
|||
if (currentRowLevel + currentColumnLevel == maxLevel) { |
|||
if (generateValues) { |
|||
columnsAndValues[rowIndications[rowGroupOffsets[currentRowOffset]]] = storm::storage::MatrixEntry<uint_fast64_t, double>(currentColumnOffset, Cudd_V(dd)); |
|||
} |
|||
++rowIndications[rowGroupOffsets[currentRowOffset]]; |
|||
} else { |
|||
DdNode const* elseElse; |
|||
DdNode const* elseThen; |
|||
DdNode const* thenElse; |
|||
DdNode const* thenThen; |
|||
|
|||
if (ddColumnVariableIndices[currentColumnLevel] < dd->index) { |
|||
elseElse = elseThen = thenElse = thenThen = dd; |
|||
} else if (ddRowVariableIndices[currentColumnLevel] < dd->index) { |
|||
elseElse = thenElse = Cudd_E(dd); |
|||
elseThen = thenThen = Cudd_T(dd); |
|||
} else { |
|||
DdNode const* elseNode = Cudd_E(dd); |
|||
if (ddColumnVariableIndices[currentColumnLevel] < elseNode->index) { |
|||
elseElse = elseThen = elseNode; |
|||
} else { |
|||
elseElse = Cudd_E(elseNode); |
|||
elseThen = Cudd_T(elseNode); |
|||
} |
|||
|
|||
DdNode const* thenNode = Cudd_T(dd); |
|||
if (ddColumnVariableIndices[currentColumnLevel] < thenNode->index) { |
|||
thenElse = thenThen = thenNode; |
|||
} else { |
|||
thenElse = Cudd_E(thenNode); |
|||
thenThen = Cudd_T(thenNode); |
|||
} |
|||
} |
|||
|
|||
// Visit else-else.
|
|||
toMatrixRec(elseElse, rowIndications, columnsAndValues, rowGroupOffsets, rowOdd.getElseSuccessor(), columnOdd.getElseSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset, currentColumnOffset, ddRowVariableIndices, ddColumnVariableIndices, generateValues); |
|||
// Visit else-then.
|
|||
toMatrixRec(elseThen, rowIndications, columnsAndValues, rowGroupOffsets, rowOdd.getElseSuccessor(), columnOdd.getThenSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset, currentColumnOffset + columnOdd.getElseOffset(), ddRowVariableIndices, ddColumnVariableIndices, generateValues); |
|||
// Visit then-else.
|
|||
toMatrixRec(thenElse, rowIndications, columnsAndValues, rowGroupOffsets, rowOdd.getThenSuccessor(), columnOdd.getElseSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), currentColumnOffset, ddRowVariableIndices, ddColumnVariableIndices, generateValues); |
|||
// Visit then-then.
|
|||
toMatrixRec(thenThen, rowIndications, columnsAndValues, rowGroupOffsets, rowOdd.getThenSuccessor(), columnOdd.getThenSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), currentColumnOffset + columnOdd.getElseOffset(), ddRowVariableIndices, ddColumnVariableIndices, generateValues); |
|||
} |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
storm::storage::SparseMatrix<ValueType> InternalAdd<DdType::CUDD, ValueType>::toMatrix(std::vector<uint_fast64_t> const& ddGroupVariableIndices, InternalBdd<DdType::CUDD> const& groupVariableCube, storm::dd::Odd<DdType::CUDD> const& rowOdd, std::vector<uint_fast64_t> const& ddRowVariableIndices, storm::dd::Odd<DdType::CUDD> const& columnOdd, std::vector<uint_fast64_t> const& ddColumnVariableIndices, InternalBdd<DdType::CUDD> const& columnVariableCube) const { |
|||
// Start by computing the offsets (in terms of rows) for each row group.
|
|||
InternalAdd<DdType::CUDD, ValueType> stateToNumberOfChoices = this->notZero().existsAbstract(columnVariableCube).toAdd().sumAbstract(groupVariableCube); |
|||
std::vector<ValueType> rowGroupIndicesAsValueType = stateToNumberOfChoices.toVector(rowOdd); |
|||
std::vector<uint_fast64_t> rowGroupIndices(rowGroupIndicesAsValueType.size() + 1); |
|||
std::transform(rowGroupIndicesAsValueType.begin(), rowGroupIndicesAsValueType.end(), rowGroupIndices.begin(), [] (ValueType const& value) { return static_cast<uint_fast64_t>(value); }); |
|||
uint_fast64_t tmp = 0; |
|||
uint_fast64_t tmp2 = 0; |
|||
for (uint_fast64_t i = 1; i < rowGroupIndices.size(); ++i) { |
|||
tmp2 = rowGroupIndices[i]; |
|||
rowGroupIndices[i] = rowGroupIndices[i - 1] + tmp; |
|||
std::swap(tmp, tmp2); |
|||
} |
|||
rowGroupIndices[0] = 0; |
|||
|
|||
// Next, we split the matrix into one for each group. This only works if the group variables are at the very
|
|||
// top.
|
|||
std::vector<InternalAdd<DdType::CUDD, ValueType>> groups; |
|||
splitGroupsRec(this->getCuddDdNode(), groups, ddGroupVariableIndices, 0, ddGroupVariableIndices.size()); |
|||
|
|||
// Create the actual storage for the non-zero entries.
|
|||
std::vector<storm::storage::MatrixEntry<uint_fast64_t, double>> columnsAndValues(this->getNonZeroCount()); |
|||
|
|||
// Now compute the indices at which the individual rows start.
|
|||
std::vector<uint_fast64_t> rowIndications(rowGroupIndices.back() + 1); |
|||
|
|||
std::vector<InternalAdd<DdType::CUDD, ValueType>> statesWithGroupEnabled(groups.size()); |
|||
InternalAdd<DdType::CUDD, ValueType> stateToRowGroupCount = this->getDdManager()->getAddZero(); |
|||
for (uint_fast64_t i = 0; i < groups.size(); ++i) { |
|||
auto const& dd = groups[i]; |
|||
|
|||
toMatrixRec(dd.getCuddDdNode(), rowIndications, columnsAndValues, rowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, false); |
|||
|
|||
statesWithGroupEnabled[i] = dd.notZero().existsAbstract(columnVariableCube).toAdd(); |
|||
stateToRowGroupCount += statesWithGroupEnabled[i]; |
|||
statesWithGroupEnabled[i].addToVector(rowOdd, ddRowVariableIndices, rowGroupIndices); |
|||
} |
|||
|
|||
// Since we modified the rowGroupIndices, we need to restore the correct values.
|
|||
std::function<uint_fast64_t (uint_fast64_t const&, double const&)> fct = [] (uint_fast64_t const& a, double const& b) -> uint_fast64_t { return a - static_cast<uint_fast64_t>(b); }; |
|||
composeVectorRec(stateToRowGroupCount.getCuddDdNode(), 0, ddRowVariableIndices.size(), 0, rowOdd, ddRowVariableIndices, rowGroupIndices, fct); |
|||
|
|||
// Now that we computed the number of entries in each row, compute the corresponding offsets in the entry vector.
|
|||
tmp = 0; |
|||
tmp2 = 0; |
|||
for (uint_fast64_t i = 1; i < rowIndications.size(); ++i) { |
|||
tmp2 = rowIndications[i]; |
|||
rowIndications[i] = rowIndications[i - 1] + tmp; |
|||
std::swap(tmp, tmp2); |
|||
} |
|||
rowIndications[0] = 0; |
|||
|
|||
// Now actually fill the entry vector.
|
|||
for (uint_fast64_t i = 0; i < groups.size(); ++i) { |
|||
auto const& dd = groups[i]; |
|||
|
|||
toMatrixRec(dd.getCuddDdNode(), rowIndications, columnsAndValues, rowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, true); |
|||
|
|||
statesWithGroupEnabled[i].addToVector(rowOdd, ddRowVariableIndices, rowGroupIndices); |
|||
} |
|||
|
|||
// Since we modified the rowGroupIndices, we need to restore the correct values.
|
|||
composeVectorRec(stateToRowGroupCount.getCuddDdNode(), 0, ddRowVariableIndices.size(), 0, rowOdd, ddRowVariableIndices, rowGroupIndices, fct); |
|||
|
|||
// Since the last call to toMatrixRec modified the rowIndications, we need to restore the correct values.
|
|||
for (uint_fast64_t i = rowIndications.size() - 1; i > 0; --i) { |
|||
rowIndications[i] = rowIndications[i - 1]; |
|||
} |
|||
rowIndications[0] = 0; |
|||
|
|||
return storm::storage::SparseMatrix<ValueType>(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices), true); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<ValueType>> InternalAdd<DdType::CUDD, ValueType>::toMatrixVector(InternalAdd<DdType::CUDD, ValueType> const& vector, std::vector<uint_fast64_t> const& ddGroupVariableIndices, std::vector<uint_fast64_t>&& rowGroupIndices, storm::dd::Odd<DdType::CUDD> const& rowOdd, std::vector<uint_fast64_t> const& ddRowVariableIndices, storm::dd::Odd<DdType::CUDD> const& columnOdd, std::vector<uint_fast64_t> const& ddColumnVariableIndices, InternalBdd<DdType::CUDD> const& columnVariableCube) { |
|||
// Transform the row group sizes to the actual row group indices.
|
|||
rowGroupIndices.resize(rowGroupIndices.size() + 1); |
|||
uint_fast64_t tmp = 0; |
|||
uint_fast64_t tmp2 = 0; |
|||
for (uint_fast64_t i = 1; i < rowGroupIndices.size(); ++i) { |
|||
tmp2 = rowGroupIndices[i]; |
|||
rowGroupIndices[i] = rowGroupIndices[i - 1] + tmp; |
|||
std::swap(tmp, tmp2); |
|||
} |
|||
rowGroupIndices[0] = 0; |
|||
|
|||
// Create the explicit vector we need to fill later.
|
|||
std::vector<double> explicitVector(rowGroupIndices.back()); |
|||
|
|||
// Next, we split the matrix into one for each group. This only works if the group variables are at the very top.
|
|||
std::vector<std::pair<InternalAdd<DdType::CUDD, ValueType>, InternalAdd<DdType::CUDD, ValueType>>> groups; |
|||
splitGroupsRec(this->getCuddDdNode(), vector.getCuddDdNode(), groups, ddGroupVariableIndices, 0, ddGroupVariableIndices.size()); |
|||
|
|||
// Create the actual storage for the non-zero entries.
|
|||
std::vector<storm::storage::MatrixEntry<uint_fast64_t, double>> columnsAndValues(this->getNonZeroCount()); |
|||
|
|||
// Now compute the indices at which the individual rows start.
|
|||
std::vector<uint_fast64_t> rowIndications(rowGroupIndices.back() + 1); |
|||
|
|||
std::vector<storm::dd::InternalAdd<DdType::CUDD, ValueType>> statesWithGroupEnabled(groups.size()); |
|||
storm::dd::InternalAdd<storm::dd::DdType::CUDD, ValueType> stateToRowGroupCount = this->getDdManager()->getAddZero(); |
|||
for (uint_fast64_t i = 0; i < groups.size(); ++i) { |
|||
std::pair<storm::dd::InternalAdd<DdType::CUDD, ValueType>, storm::dd::InternalAdd<DdType::CUDD, ValueType>> ddPair = groups[i]; |
|||
|
|||
toMatrixRec(ddPair.first.getCuddDdNode(), rowIndications, columnsAndValues, rowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, false); |
|||
toVectorRec(ddPair.second.getCuddDdNode(), explicitVector, rowGroupIndices, rowOdd, 0, ddRowVariableIndices.size(), 0, ddRowVariableIndices); |
|||
|
|||
statesWithGroupEnabled[i] = (ddPair.first.notZero().existsAbstract(columnVariableCube) || ddPair.second.notZero()).toAdd(); |
|||
stateToRowGroupCount += statesWithGroupEnabled[i]; |
|||
statesWithGroupEnabled[i].addToVector(rowOdd, ddRowVariableIndices, rowGroupIndices); |
|||
} |
|||
|
|||
// Since we modified the rowGroupIndices, we need to restore the correct values.
|
|||
std::function<uint_fast64_t (uint_fast64_t const&, double const&)> fct = [] (uint_fast64_t const& a, double const& b) -> uint_fast64_t { return a - static_cast<uint_fast64_t>(b); }; |
|||
composeVectorRec(stateToRowGroupCount.getCuddDdNode(), 0, ddRowVariableIndices.size(), 0, rowOdd, ddRowVariableIndices, rowGroupIndices, fct); |
|||
|
|||
// Now that we computed the number of entries in each row, compute the corresponding offsets in the entry vector.
|
|||
tmp = 0; |
|||
tmp2 = 0; |
|||
for (uint_fast64_t i = 1; i < rowIndications.size(); ++i) { |
|||
tmp2 = rowIndications[i]; |
|||
rowIndications[i] = rowIndications[i - 1] + tmp; |
|||
std::swap(tmp, tmp2); |
|||
} |
|||
rowIndications[0] = 0; |
|||
|
|||
// Now actually fill the entry vector.
|
|||
for (uint_fast64_t i = 0; i < groups.size(); ++i) { |
|||
auto const& dd = groups[i].first; |
|||
|
|||
toMatrixRec(dd.getCuddDdNode(), rowIndications, columnsAndValues, rowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, true); |
|||
|
|||
statesWithGroupEnabled[i].addToVector(rowOdd, ddRowVariableIndices, rowGroupIndices); |
|||
} |
|||
|
|||
// Since we modified the rowGroupIndices, we need to restore the correct values.
|
|||
composeVectorRec(stateToRowGroupCount.getCuddDdNode(), 0, ddRowVariableIndices.size(), 0, rowOdd, ddRowVariableIndices, rowGroupIndices, fct); |
|||
|
|||
// Since the last call to toMatrixRec modified the rowIndications, we need to restore the correct values.
|
|||
for (uint_fast64_t i = rowIndications.size() - 1; i > 0; --i) { |
|||
rowIndications[i] = rowIndications[i - 1]; |
|||
} |
|||
rowIndications[0] = 0; |
|||
|
|||
return std::make_pair(storm::storage::SparseMatrix<ValueType>(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices), true), std::move(explicitVector)); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
void InternalAdd<DdType::CUDD, ValueType>::splitGroupsRec(DdNode* dd, std::vector<InternalAdd<DdType::CUDD, ValueType>>& groups, std::vector<uint_fast64_t> const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel) const { |
|||
// For the empty DD, we do not need to create a group.
|
|||
if (dd == Cudd_ReadZero(this->getDdManager()->getCuddManager().getManager())) { |
|||
return; |
|||
} |
|||
|
|||
if (currentLevel == maxLevel) { |
|||
groups.push_back(InternalAdd<DdType::CUDD, ValueType>(ddManager, ADD(ddManager->getCuddManager(), dd))); |
|||
} else if (ddGroupVariableIndices[currentLevel] < dd->index) { |
|||
splitGroupsRec(dd, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); |
|||
splitGroupsRec(dd, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); |
|||
} else { |
|||
splitGroupsRec(Cudd_E(dd), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); |
|||
splitGroupsRec(Cudd_T(dd), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); |
|||
} |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
void InternalAdd<DdType::CUDD, ValueType>::splitGroupsRec(DdNode* dd1, DdNode* dd2, std::vector<std::pair<InternalAdd<DdType::CUDD, ValueType>, InternalAdd<DdType::CUDD, ValueType>>>& groups, std::vector<uint_fast64_t> const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel) const { |
|||
// For the empty DD, we do not need to create a group.
|
|||
if (dd1 == Cudd_ReadZero(ddManager->getCuddManager().getManager()) && dd2 == Cudd_ReadZero(ddManager->getCuddManager().getManager())) { |
|||
return; |
|||
} |
|||
|
|||
if (currentLevel == maxLevel) { |
|||
groups.push_back(std::make_pair(InternalAdd<DdType::CUDD, ValueType>(ddManager, ADD(ddManager->getCuddManager(), dd1)), |
|||
InternalAdd<DdType::CUDD, ValueType>(ddManager, ADD(ddManager->getCuddManager(), dd2)))); |
|||
} else if (ddGroupVariableIndices[currentLevel] < dd1->index) { |
|||
if (ddGroupVariableIndices[currentLevel] < dd2->index) { |
|||
splitGroupsRec(dd1, dd2, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); |
|||
splitGroupsRec(dd1, dd2, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); |
|||
} else { |
|||
splitGroupsRec(dd1, Cudd_T(dd2), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); |
|||
splitGroupsRec(dd1, Cudd_E(dd2), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); |
|||
} |
|||
} else if (ddGroupVariableIndices[currentLevel] < dd2->index) { |
|||
splitGroupsRec(Cudd_T(dd1), dd2, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); |
|||
splitGroupsRec(Cudd_E(dd1), dd2, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); |
|||
} else { |
|||
splitGroupsRec(Cudd_T(dd1), Cudd_T(dd2), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); |
|||
splitGroupsRec(Cudd_E(dd1), Cudd_E(dd2), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); |
|||
} |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::fromVector(InternalDdManager<DdType::CUDD> const* ddManager, std::vector<ValueType> const& values, storm::dd::Odd<DdType::CUDD> const& odd, std::vector<uint_fast64_t> const& ddVariableIndices) { |
|||
uint_fast64_t offset = 0; |
|||
return InternalAdd<DdType::CUDD, ValueType>(ddManager, ADD(ddManager->getCuddManager(), fromVectorRec(ddManager->getCuddManager().getManager(), offset, 0, ddVariableIndices.size(), values, odd, ddVariableIndices))); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
DdNode* InternalAdd<DdType::CUDD, ValueType>::fromVectorRec(::DdManager* manager, uint_fast64_t& currentOffset, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector<ValueType> const& values, Odd<DdType::CUDD> const& odd, std::vector<uint_fast64_t> const& ddVariableIndices) { |
|||
if (currentLevel == maxLevel) { |
|||
// If we are in a terminal node of the ODD, we need to check whether the then-offset of the ODD is one
|
|||
// (meaning the encoding is a valid one) or zero (meaning the encoding is not valid). Consequently, we
|
|||
// need to copy the next value of the vector iff the then-offset is greater than zero.
|
|||
if (odd.getThenOffset() > 0) { |
|||
return Cudd_addConst(manager, values[currentOffset++]); |
|||
} else { |
|||
return Cudd_ReadZero(manager); |
|||
} |
|||
} else { |
|||
// If the total offset is zero, we can just return the constant zero DD.
|
|||
if (odd.getThenOffset() + odd.getElseOffset() == 0) { |
|||
return Cudd_ReadZero(manager); |
|||
} |
|||
|
|||
// Determine the new else-successor.
|
|||
DdNode* elseSuccessor = nullptr; |
|||
if (odd.getElseOffset() > 0) { |
|||
elseSuccessor = fromVectorRec(manager, currentOffset, currentLevel + 1, maxLevel, values, odd.getElseSuccessor(), ddVariableIndices); |
|||
} else { |
|||
elseSuccessor = Cudd_ReadZero(manager); |
|||
} |
|||
Cudd_Ref(elseSuccessor); |
|||
|
|||
// Determine the new then-successor.
|
|||
DdNode* thenSuccessor = nullptr; |
|||
if (odd.getThenOffset() > 0) { |
|||
thenSuccessor = fromVectorRec(manager, currentOffset, currentLevel + 1, maxLevel, values, odd.getThenSuccessor(), ddVariableIndices); |
|||
} else { |
|||
thenSuccessor = Cudd_ReadZero(manager); |
|||
} |
|||
Cudd_Ref(thenSuccessor); |
|||
|
|||
// Create a node representing ITE(currentVar, thenSuccessor, elseSuccessor);
|
|||
DdNode* result = Cudd_addIthVar(manager, static_cast<int>(ddVariableIndices[currentLevel])); |
|||
Cudd_Ref(result); |
|||
DdNode* newResult = Cudd_addIte(manager, result, thenSuccessor, elseSuccessor); |
|||
Cudd_Ref(newResult); |
|||
|
|||
// Dispose of the intermediate results
|
|||
Cudd_RecursiveDeref(manager, result); |
|||
Cudd_RecursiveDeref(manager, thenSuccessor); |
|||
Cudd_RecursiveDeref(manager, elseSuccessor); |
|||
|
|||
// Before returning, we remove the protection imposed by the previous call to Cudd_Ref.
|
|||
Cudd_Deref(newResult); |
|||
|
|||
return newResult; |
|||
} |
|||
} |
|||
|
|||
template class InternalAdd<DdType::CUDD, double>; |
|||
} |
|||
} |
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue