diff --git a/src/modelchecker/csl/helper/HybridCtmcCslHelper.cpp b/src/modelchecker/csl/helper/HybridCtmcCslHelper.cpp
index 35e23184c..5f776fdc0 100644
--- a/src/modelchecker/csl/helper/HybridCtmcCslHelper.cpp
+++ b/src/modelchecker/csl/helper/HybridCtmcCslHelper.cpp
@@ -6,7 +6,6 @@
#include "src/storage/dd/DdManager.h"
#include "src/storage/dd/Add.h"
#include "src/storage/dd/Bdd.h"
-#include "src/storage/dd/cudd/CuddOdd.h"
#include "src/utility/macros.h"
#include "src/utility/graph.h"
@@ -80,7 +79,7 @@ namespace storm {
storm::dd::Add<DdType, ValueType> b = (statesWithProbabilityGreater0NonPsi.template toAdd<ValueType>() * rateMatrix * psiStates.swapVariables(model.getRowColumnMetaVariablePairs()).template toAdd<ValueType>()).sumAbstract(model.getColumnVariables()) / model.getManager().getConstant(uniformizationRate);
// Create an ODD for the translation to an explicit representation.
- storm::dd::Odd<DdType> odd(statesWithProbabilityGreater0NonPsi);
+ storm::dd::Odd odd = statesWithProbabilityGreater0NonPsi.createOdd();
// Convert the symbolic parts to their explicit representation.
storm::storage::SparseMatrix<ValueType> explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd);
@@ -107,7 +106,7 @@ namespace storm {
unboundedResult->filter(SymbolicQualitativeCheckResult<DdType>(model.getReachableStates(), relevantStates));
// Build an ODD for the relevant states.
- storm::dd::Odd<DdType> odd(relevantStates);
+ storm::dd::Odd odd = relevantStates.createOdd();
std::vector<ValueType> result;
if (unboundedResult->isHybridQuantitativeCheckResult()) {
@@ -146,7 +145,7 @@ namespace storm {
storm::dd::Add<DdType, ValueType> b = (statesWithProbabilityGreater0NonPsi.template toAdd<ValueType>() * rateMatrix * psiStates.swapVariables(model.getRowColumnMetaVariablePairs()).template toAdd<ValueType>()).sumAbstract(model.getColumnVariables()) / model.getManager().getConstant(uniformizationRate);
// Build an ODD for the relevant states and translate the symbolic parts to their explicit representation.
- storm::dd::Odd<DdType> odd = storm::dd::Odd<DdType>(statesWithProbabilityGreater0NonPsi);
+ storm::dd::Odd odd = statesWithProbabilityGreater0NonPsi.createOdd();
storm::storage::SparseMatrix<ValueType> explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd);
std::vector<ValueType> explicitB = b.toVector(odd);
@@ -166,7 +165,7 @@ namespace storm {
hybridResult.filter(SymbolicQualitativeCheckResult<DdType>(model.getReachableStates(), relevantStates));
// Build an ODD for the relevant states.
- odd = storm::dd::Odd<DdType>(relevantStates);
+ odd = relevantStates.createOdd();
std::unique_ptr<CheckResult> explicitResult = hybridResult.toExplicitQuantitativeCheckResult();
std::vector<ValueType> newSubresult = std::move(explicitResult->asExplicitQuantitativeCheckResult<ValueType>().getValueVector());
@@ -179,7 +178,7 @@ namespace storm {
// If the lower and upper bounds coincide, we have only determined the relevant states at this
// point, but we still need to construct the starting vector.
if (lowerBound == upperBound) {
- odd = storm::dd::Odd<DdType>(relevantStates);
+ odd = relevantStates.createOdd();
newSubresult = psiStates.template toAdd<ValueType>().toVector(odd);
}
@@ -194,7 +193,7 @@ namespace storm {
// In this case, the interval is of the form [t, t] with t != 0, t != inf.
// Build an ODD for the relevant states.
- storm::dd::Odd<DdType> odd = storm::dd::Odd<DdType>(statesWithProbabilityGreater0);
+ storm::dd::Odd odd = statesWithProbabilityGreater0.createOdd();
std::vector<ValueType> newSubresult = psiStates.template toAdd<ValueType>().toVector(odd);
@@ -225,7 +224,7 @@ namespace storm {
STORM_LOG_THROW(rewardModel.hasStateRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
// Create ODD for the translation.
- storm::dd::Odd<DdType> odd(model.getReachableStates());
+ storm::dd::Odd odd =model.getReachableStates().createOdd();
// Initialize result to state rewards of the model.
std::vector<ValueType> result = rewardModel.getStateRewardVector().toVector(odd);
@@ -261,7 +260,7 @@ namespace storm {
STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive.");
// Create ODD for the translation.
- storm::dd::Odd<DdType> odd(model.getReachableStates());
+ storm::dd::Odd odd = model.getReachableStates().createOdd();
// Compute the uniformized matrix.
storm::dd::Add<DdType, ValueType> uniformizedMatrix = computeUniformizedMatrix(model, rateMatrix, exitRateVector, model.getReachableStates(), uniformizationRate);
@@ -281,7 +280,7 @@ namespace storm {
storm::dd::Add<DdType, ValueType> probabilityMatrix = computeProbabilityMatrix(model, rateMatrix, exitRateVector);
// Create ODD for the translation.
- storm::dd::Odd<DdType> odd(model.getReachableStates());
+ storm::dd::Odd odd = model.getReachableStates().createOdd();
storm::storage::SparseMatrix<ValueType> explicitProbabilityMatrix = probabilityMatrix.toMatrix(odd, odd);
std::vector<ValueType> explicitExitRateVector = exitRateVector.toVector(odd);
diff --git a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp
index 899d090e5..be420f5f5 100644
--- a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp
+++ b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp
@@ -3,7 +3,7 @@
#include "src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.h"
#include "src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h"
-#include "src/storage/dd/cudd/CuddOdd.h"
+#include "src/storage/dd/Odd.h"
#include "src/storage/dd/DdManager.h"
#include "src/utility/macros.h"
@@ -94,7 +94,7 @@ namespace storm {
SymbolicQualitativeCheckResult<DdType> const& subResult = subResultPointer->asSymbolicQualitativeCheckResult<DdType>();
// Create ODD for the translation.
- storm::dd::Odd<DdType> odd(this->getModel().getReachableStates());
+ storm::dd::Odd odd = this->getModel().getReachableStates().createOdd();
storm::storage::SparseMatrix<ValueType> explicitProbabilityMatrix = this->getModel().getTransitionMatrix().toMatrix(odd, odd);
diff --git a/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp
index 71c858bdc..a30f88898 100644
--- a/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp
+++ b/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp
@@ -2,8 +2,6 @@
#include "src/modelchecker/prctl/helper/HybridMdpPrctlHelper.h"
-#include "src/storage/dd/cudd/CuddOdd.h"
-
#include "src/models/symbolic/Mdp.h"
#include "src/models/symbolic/StandardRewardModel.h"
diff --git a/src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp b/src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp
index 1263ee82e..757b0992d 100644
--- a/src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp
+++ b/src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp
@@ -6,7 +6,7 @@
#include "src/storage/dd/DdManager.h"
#include "src/storage/dd/Add.h"
#include "src/storage/dd/Bdd.h"
-#include "src/storage/dd/cudd/CuddOdd.h"
+#include "src/storage/dd/Odd.h"
#include "src/utility/graph.h"
#include "src/utility/constants.h"
@@ -43,7 +43,7 @@ namespace storm {
// If there are maybe states, we need to solve an equation system.
if (!maybeStates.isZero()) {
// Create the ODD for the translation between symbolic and explicit storage.
- storm::dd::Odd<DdType> odd(maybeStates);
+ storm::dd::Odd odd = maybeStates.createOdd();
// Create the matrix and the vector for the equation system.
storm::dd::Add<DdType, ValueType> maybeStatesAdd = maybeStates.template toAdd<ValueType>();
@@ -98,7 +98,7 @@ namespace storm {
// If there are maybe states, we need to perform matrix-vector multiplications.
if (!maybeStates.isZero()) {
// Create the ODD for the translation between symbolic and explicit storage.
- storm::dd::Odd<DdType> odd(maybeStates);
+ storm::dd::Odd odd = maybeStates.createOdd();
// Create the matrix and the vector for the equation system.
storm::dd::Add<DdType, ValueType> maybeStatesAdd = maybeStates.template toAdd<ValueType>();
@@ -139,7 +139,7 @@ namespace storm {
STORM_LOG_THROW(rewardModel.hasStateRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
// Create the ODD for the translation between symbolic and explicit storage.
- storm::dd::Odd<DdType> odd(model.getReachableStates());
+ storm::dd::Odd odd = model.getReachableStates().createOdd();
// Create the solution vector (and initialize it to the state rewards of the model).
std::vector<ValueType> x = rewardModel.getStateRewardVector().toVector(odd);
@@ -164,7 +164,7 @@ namespace storm {
storm::dd::Add<DdType> totalRewardVector = rewardModel.getTotalRewardVector(transitionMatrix, model.getColumnVariables());
// Create the ODD for the translation between symbolic and explicit storage.
- storm::dd::Odd<DdType> odd(model.getReachableStates());
+ storm::dd::Odd odd = model.getReachableStates().createOdd();
// Create the solution vector.
std::vector<ValueType> x(model.getNumberOfStates(), storm::utility::zero<ValueType>());
@@ -204,7 +204,7 @@ namespace storm {
// If there are maybe states, we need to solve an equation system.
if (!maybeStates.isZero()) {
// Create the ODD for the translation between symbolic and explicit storage.
- storm::dd::Odd<DdType> odd(maybeStates);
+ storm::dd::Odd odd = maybeStates.createOdd();
// Create the matrix and the vector for the equation system.
storm::dd::Add<DdType> maybeStatesAdd = maybeStates.template toAdd<ValueType>();
diff --git a/src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp b/src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp
index c612998f6..22b104034 100644
--- a/src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp
+++ b/src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp
@@ -3,7 +3,7 @@
#include "src/storage/dd/DdManager.h"
#include "src/storage/dd/Add.h"
#include "src/storage/dd/Bdd.h"
-#include "src/storage/dd/cudd/CuddOdd.h"
+#include "src/storage/dd/Odd.h"
#include "src/utility/graph.h"
#include "src/utility/constants.h"
@@ -47,7 +47,7 @@ namespace storm {
// If there are maybe states, we need to solve an equation system.
if (!maybeStates.isZero()) {
// Create the ODD for the translation between symbolic and explicit storage.
- storm::dd::Odd<DdType> odd(maybeStates);
+ storm::dd::Odd odd = maybeStates.createOdd();
// Create the matrix and the vector for the equation system.
storm::dd::Add<DdType, ValueType> maybeStatesAdd = maybeStates.template toAdd<ValueType>();
@@ -107,7 +107,7 @@ namespace storm {
// If there are maybe states, we need to perform matrix-vector multiplications.
if (!maybeStates.isZero()) {
// Create the ODD for the translation between symbolic and explicit storage.
- storm::dd::Odd<DdType> odd(maybeStates);
+ storm::dd::Odd odd = maybeStates.createOdd();
// Create the matrix and the vector for the equation system.
storm::dd::Add<DdType, ValueType> maybeStatesAdd = maybeStates.template toAdd<ValueType>();
@@ -149,7 +149,7 @@ namespace storm {
STORM_LOG_THROW(rewardModel.hasStateRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
// Create the ODD for the translation between symbolic and explicit storage.
- storm::dd::Odd<DdType> odd(model.getReachableStates());
+ storm::dd::Odd odd =model.getReachableStates().createOdd();
// Translate the symbolic matrix to its explicit representations.
storm::storage::SparseMatrix<ValueType> explicitMatrix = transitionMatrix.toMatrix(model.getNondeterminismVariables(), odd, odd);
@@ -174,7 +174,7 @@ namespace storm {
storm::dd::Add<DdType, ValueType> totalRewardVector = rewardModel.getTotalRewardVector(transitionMatrix, model.getColumnVariables());
// Create the ODD for the translation between symbolic and explicit storage.
- storm::dd::Odd<DdType> odd(model.getReachableStates());
+ storm::dd::Odd odd = model.getReachableStates().createOdd();
// Create the solution vector.
std::vector<ValueType> x(model.getNumberOfStates(), storm::utility::zero<ValueType>());
@@ -220,7 +220,7 @@ namespace storm {
// If there are maybe states, we need to solve an equation system.
if (!maybeStates.isZero()) {
// Create the ODD for the translation between symbolic and explicit storage.
- storm::dd::Odd<DdType> odd(maybeStates);
+ storm::dd::Odd odd = maybeStates.createOdd();
// Create the matrix and the vector for the equation system.
storm::dd::Add<DdType, ValueType> maybeStatesAdd = maybeStates.template toAdd<ValueType>();
diff --git a/src/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp b/src/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp
index 69092b13b..56530a78b 100644
--- a/src/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp
+++ b/src/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp
@@ -4,7 +4,6 @@
#include "src/storage/dd/DdManager.h"
#include "src/storage/dd/Add.h"
#include "src/storage/dd/Bdd.h"
-#include "src/storage/dd/cudd/CuddOdd.h"
#include "src/solver/SymbolicLinearEquationSolver.h"
@@ -38,9 +37,6 @@ namespace storm {
} else {
// If there are maybe states, we need to solve an equation system.
if (!maybeStates.isZero()) {
- // Create the ODD for the translation between symbolic and explicit storage.
- storm::dd::Odd<DdType> odd(maybeStates);
-
// Create the matrix and the vector for the equation system.
storm::dd::Add<DdType, ValueType> maybeStatesAdd = maybeStates.template toAdd<ValueType>();
@@ -86,9 +82,6 @@ namespace storm {
// If there are maybe states, we need to perform matrix-vector multiplications.
if (!maybeStates.isZero()) {
- // Create the ODD for the translation between symbolic and explicit storage.
- storm::dd::Odd<DdType> odd(maybeStates);
-
// Create the matrix and the vector for the equation system.
storm::dd::Add<DdType, ValueType> maybeStatesAdd = maybeStates.template toAdd<ValueType>();
@@ -159,9 +152,6 @@ namespace storm {
} else {
// If there are maybe states, we need to solve an equation system.
if (!maybeStates.isZero()) {
- // Create the ODD for the translation between symbolic and explicit storage.
- storm::dd::Odd<DdType> odd(maybeStates);
-
// Create the matrix and the vector for the equation system.
storm::dd::Add<DdType, ValueType> maybeStatesAdd = maybeStates.template toAdd<ValueType>();
diff --git a/src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp b/src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp
index c2618fd41..a9ce5d7fb 100644
--- a/src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp
+++ b/src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp
@@ -5,7 +5,6 @@
#include "src/storage/dd/DdManager.h"
#include "src/storage/dd/Add.h"
#include "src/storage/dd/Bdd.h"
-#include "src/storage/dd/cudd/CuddOdd.h"
#include "src/utility/graph.h"
#include "src/utility/constants.h"
diff --git a/src/modelchecker/results/HybridQuantitativeCheckResult.cpp b/src/modelchecker/results/HybridQuantitativeCheckResult.cpp
index 2e3d47a72..040379c42 100644
--- a/src/modelchecker/results/HybridQuantitativeCheckResult.cpp
+++ b/src/modelchecker/results/HybridQuantitativeCheckResult.cpp
@@ -11,7 +11,7 @@
namespace storm {
namespace modelchecker {
template<storm::dd::DdType Type, typename ValueType>
- HybridQuantitativeCheckResult<Type, ValueType>::HybridQuantitativeCheckResult(storm::dd::Bdd<Type> const& reachableStates, storm::dd::Bdd<Type> const& symbolicStates, storm::dd::Add<Type, ValueType> const& symbolicValues, storm::dd::Bdd<Type> const& explicitStates, storm::dd::Odd<Type> const& odd, std::vector<ValueType> const& explicitValues) : reachableStates(reachableStates), symbolicStates(symbolicStates), symbolicValues(symbolicValues), explicitStates(explicitStates), odd(odd), explicitValues(explicitValues) {
+ HybridQuantitativeCheckResult<Type, ValueType>::HybridQuantitativeCheckResult(storm::dd::Bdd<Type> const& reachableStates, storm::dd::Bdd<Type> const& symbolicStates, storm::dd::Add<Type, ValueType> const& symbolicValues, storm::dd::Bdd<Type> const& explicitStates, storm::dd::Odd const& odd, std::vector<ValueType> const& explicitValues) : reachableStates(reachableStates), symbolicStates(symbolicStates), symbolicValues(symbolicValues), explicitStates(explicitStates), odd(odd), explicitValues(explicitValues) {
// Intentionally left empty.
}
@@ -39,7 +39,7 @@ namespace storm {
template<storm::dd::DdType Type, typename ValueType>
std::unique_ptr<CheckResult> HybridQuantitativeCheckResult<Type, ValueType>::toExplicitQuantitativeCheckResult() const {
storm::dd::Bdd<Type> allStates = symbolicStates || explicitStates;
- storm::dd::Odd<Type> allStatesOdd(allStates);
+ storm::dd::Odd allStatesOdd = allStates.createOdd();
std::vector<ValueType> fullExplicitValues = symbolicValues.toVector(allStatesOdd);
this->odd.expandExplicitVector(allStatesOdd, this->explicitValues, fullExplicitValues);
@@ -77,7 +77,7 @@ namespace storm {
}
template<storm::dd::DdType Type, typename ValueType>
- storm::dd::Odd<Type> const& HybridQuantitativeCheckResult<Type, ValueType>::getOdd() const {
+ storm::dd::Odd const& HybridQuantitativeCheckResult<Type, ValueType>::getOdd() const {
return odd;
}
@@ -130,10 +130,10 @@ namespace storm {
// Start by computing the new set of states that is stored explictly and the corresponding ODD.
this->explicitStates = this->explicitStates && filter.asSymbolicQualitativeCheckResult<Type>().getTruthValuesVector();
- storm::dd::Odd<Type> newOdd(explicitStates);
+ storm::dd::Odd newOdd = explicitStates.createOdd();
// Then compute the new vector of explicit values and set the new data fields.
- this->explicitValues = this->odd.filterExplicitVector(explicitStates, this->explicitValues);
+ this->explicitValues = explicitStates.filterExplicitVector(this->odd, explicitValues);
this->odd = newOdd;
}
diff --git a/src/modelchecker/results/HybridQuantitativeCheckResult.h b/src/modelchecker/results/HybridQuantitativeCheckResult.h
index fa5b0a62c..9e40ae29e 100644
--- a/src/modelchecker/results/HybridQuantitativeCheckResult.h
+++ b/src/modelchecker/results/HybridQuantitativeCheckResult.h
@@ -4,7 +4,7 @@
#include "src/storage/dd/DdType.h"
#include "src/storage/dd/Add.h"
#include "src/storage/dd/Bdd.h"
-#include "src/storage/dd/cudd/CuddOdd.h"
+#include "src/storage/dd/Odd.h"
#include "src/modelchecker/results/QuantitativeCheckResult.h"
#include "src/utility/OsDetection.h"
@@ -14,7 +14,7 @@ namespace storm {
class HybridQuantitativeCheckResult : public QuantitativeCheckResult {
public:
HybridQuantitativeCheckResult() = default;
- HybridQuantitativeCheckResult(storm::dd::Bdd<Type> const& reachableStates, storm::dd::Bdd<Type> const& symbolicStates, storm::dd::Add<Type, ValueType> const& symbolicValues, storm::dd::Bdd<Type> const& explicitStates, storm::dd::Odd<Type> const& odd, std::vector<ValueType> const& explicitValues);
+ HybridQuantitativeCheckResult(storm::dd::Bdd<Type> const& reachableStates, storm::dd::Bdd<Type> const& symbolicStates, storm::dd::Add<Type, ValueType> const& symbolicValues, storm::dd::Bdd<Type> const& explicitStates, storm::dd::Odd const& odd, std::vector<ValueType> const& explicitValues);
HybridQuantitativeCheckResult(HybridQuantitativeCheckResult const& other) = default;
HybridQuantitativeCheckResult& operator=(HybridQuantitativeCheckResult const& other) = default;
@@ -38,7 +38,7 @@ namespace storm {
storm::dd::Bdd<Type> const& getExplicitStates() const;
- storm::dd::Odd<Type> const& getOdd() const;
+ storm::dd::Odd const& getOdd() const;
std::vector<ValueType> const& getExplicitValueVector() const;
@@ -64,7 +64,7 @@ namespace storm {
storm::dd::Bdd<Type> explicitStates;
// The ODD that enables translation of the explicit values to a symbolic format.
- storm::dd::Odd<Type> odd;
+ storm::dd::Odd odd;
// The explicit value vector.
std::vector<ValueType> explicitValues;
diff --git a/src/storage/dd/Add.cpp b/src/storage/dd/Add.cpp
index 22f0f9a29..8120ab953 100644
--- a/src/storage/dd/Add.cpp
+++ b/src/storage/dd/Add.cpp
@@ -4,7 +4,7 @@
#include "src/storage/dd/DdMetaVariable.h"
#include "src/storage/dd/DdManager.h"
-#include "src/storage/dd/cudd/CuddOdd.h"
+#include "src/storage/dd/Odd.h"
#include "src/storage/SparseMatrix.h"
@@ -380,11 +380,11 @@ namespace storm {
template<DdType LibraryType, typename ValueType>
std::vector<ValueType> Add<LibraryType, ValueType>::toVector() const {
- return this->toVector(Odd<LibraryType>(*this));
+ return this->toVector(this->createOdd());
}
template<DdType LibraryType, typename ValueType>
- std::vector<ValueType> Add<LibraryType, ValueType>::toVector(Odd<LibraryType> const& rowOdd) const {
+ std::vector<ValueType> Add<LibraryType, ValueType>::toVector(Odd const& rowOdd) const {
std::vector<ValueType> result(rowOdd.getTotalOffset());
std::vector<uint_fast64_t> ddVariableIndices = this->getSortedVariableIndices();
internalAdd.composeWithExplicitVector(rowOdd, ddVariableIndices, result, std::plus<ValueType>());
@@ -392,7 +392,7 @@ namespace storm {
}
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::vector<ValueType> Add<LibraryType, ValueType>::toVector(std::set<storm::expressions::Variable> const& groupMetaVariables, storm::dd::Odd const& rowOdd, std::vector<uint_fast64_t> const& groupOffsets) const {
std::set<storm::expressions::Variable> rowMetaVariables;
// Prepare the proper sets of meta variables.
@@ -445,11 +445,11 @@ namespace storm {
}
}
- return toMatrix(rowVariables, columnVariables, Odd<LibraryType>(this->sumAbstract(rowVariables)), Odd<LibraryType>(this->sumAbstract(columnVariables)));
+ return toMatrix(rowVariables, columnVariables, this->sumAbstract(rowVariables).createOdd(), this->sumAbstract(columnVariables).createOdd());
}
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 {
+ storm::storage::SparseMatrix<ValueType> Add<LibraryType, ValueType>::toMatrix(storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const {
std::set<storm::expressions::Variable> rowMetaVariables;
std::set<storm::expressions::Variable> columnMetaVariables;
@@ -465,7 +465,7 @@ namespace storm {
}
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 {
+ 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 const& rowOdd, storm::dd::Odd const& columnOdd) const {
std::vector<uint_fast64_t> ddRowVariableIndices;
std::vector<uint_fast64_t> ddColumnVariableIndices;
@@ -528,7 +528,7 @@ namespace storm {
}
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 {
+ storm::storage::SparseMatrix<ValueType> Add<LibraryType, ValueType>::toMatrix(std::set<storm::expressions::Variable> const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const {
std::set<storm::expressions::Variable> rowMetaVariables;
std::set<storm::expressions::Variable> columnMetaVariables;
@@ -550,7 +550,7 @@ namespace storm {
}
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 {
+ 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 const& rowOdd, storm::dd::Odd const& columnOdd) const {
std::vector<uint_fast64_t> ddRowVariableIndices;
std::vector<uint_fast64_t> ddColumnVariableIndices;
std::vector<uint_fast64_t> ddGroupVariableIndices;
@@ -652,7 +652,7 @@ namespace storm {
}
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::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 const& rowOdd, storm::dd::Odd const& columnOdd) const {
std::set<storm::expressions::Variable> rowMetaVariables;
std::set<storm::expressions::Variable> columnMetaVariables;
@@ -674,7 +674,7 @@ namespace storm {
}
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::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 const& rowOdd, storm::dd::Odd const& columnOdd) const {
std::vector<uint_fast64_t> ddRowVariableIndices;
std::vector<uint_fast64_t> ddColumnVariableIndices;
std::vector<uint_fast64_t> ddGroupVariableIndices;
@@ -803,7 +803,7 @@ namespace storm {
}
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) {
+ Add<LibraryType, ValueType> Add<LibraryType, ValueType>::fromVector(std::shared_ptr<DdManager<LibraryType> const> ddManager, std::vector<ValueType> const& values, Odd const& odd, std::set<storm::expressions::Variable> const& metaVariables) {
return Add<LibraryType, ValueType>(ddManager, InternalAdd<LibraryType, ValueType>::fromVector(ddManager->getInternalDdManagerPointer(), values, odd, ddManager->getSortedVariableIndices(metaVariables)), metaVariables);
}
@@ -811,6 +811,11 @@ namespace storm {
Bdd<LibraryType> Add<LibraryType, ValueType>::toBdd() const {
return Bdd<DdType::CUDD>(this->getDdManager(), internalAdd.toBdd(), this->getContainedMetaVariables());
}
+
+ template<DdType LibraryType, typename ValueType>
+ Odd Add<LibraryType, ValueType>::createOdd() const {
+ return internalAdd.createOdd(this->getSortedVariableIndices());
+ }
template<DdType LibraryType, typename ValueType>
Add<LibraryType, ValueType>::operator InternalAdd<LibraryType, ValueType>() const {
diff --git a/src/storage/dd/Add.h b/src/storage/dd/Add.h
index 295132840..6991a9dd6 100644
--- a/src/storage/dd/Add.h
+++ b/src/storage/dd/Add.h
@@ -8,15 +8,13 @@
#include "src/storage/dd/cudd/InternalCuddAdd.h"
#include "src/storage/dd/cudd/CuddAddIterator.h"
+#include "src/storage/dd/Odd.h"
namespace storm {
namespace dd {
template<DdType LibraryType>
class Bdd;
- template<DdType LibraryType>
- class Odd;
-
template<DdType LibraryType, typename ValueType>
class AddIterator;
@@ -25,7 +23,6 @@ namespace storm {
public:
friend class DdManager<LibraryType>;
friend class Bdd<LibraryType>;
- friend class Odd<LibraryType>;
template<DdType LibraryTypePrime, typename ValueTypePrime>
friend class Add;
@@ -46,7 +43,7 @@ namespace storm {
* @param metaVariables The meta variables used for the translation.
* @return The resulting (CUDD) ADD.
*/
- static 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);
+ static Add<LibraryType, ValueType> fromVector(std::shared_ptr<DdManager<LibraryType> const> ddManager, std::vector<ValueType> const& values, Odd const& odd, std::set<storm::expressions::Variable> const& metaVariables);
/*!
* Retrieves whether the two DDs represent the same function.
@@ -525,7 +522,7 @@ namespace storm {
* @param rowOdd The ODD used for determining the correct row.
* @return The vector that is represented by this ADD.
*/
- std::vector<ValueType> toVector(storm::dd::Odd<LibraryType> const& rowOdd) const;
+ std::vector<ValueType> toVector(storm::dd::Odd const& rowOdd) const;
/*!
* Converts the ADD to a row-grouped vector. The given offset-labeled DD is used to determine the correct
@@ -536,7 +533,7 @@ namespace storm {
* @param rowOdd The ODD used for determining the correct row.
* @return The vector that is represented by this ADD.
*/
- std::vector<ValueType> toVector(std::set<storm::expressions::Variable> const& groupMetaVariables, storm::dd::Odd<LibraryType> const& rowOdd, std::vector<uint_fast64_t> const& groupOffsets) const;
+ std::vector<ValueType> toVector(std::set<storm::expressions::Variable> const& groupMetaVariables, storm::dd::Odd const& rowOdd, std::vector<uint_fast64_t> const& groupOffsets) const;
/*!
* Converts the ADD to a (sparse) double matrix. All contained non-primed variables are assumed to encode the
@@ -555,7 +552,7 @@ namespace storm {
* @param columnOdd The ODD used for determining the correct column.
* @return The matrix that is represented by this ADD.
*/
- storm::storage::SparseMatrix<ValueType> toMatrix(storm::dd::Odd<LibraryType> const& rowOdd, storm::dd::Odd<LibraryType> const& columnOdd) const;
+ storm::storage::SparseMatrix<ValueType> toMatrix(storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const;
/*!
* Converts the ADD to a (sparse) double matrix. The given offset-labeled DDs are used to determine the
@@ -567,7 +564,7 @@ namespace storm {
* @param columnOdd The ODD used for determining the correct column.
* @return The matrix that is represented by this ADD.
*/
- storm::storage::SparseMatrix<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;
+ storm::storage::SparseMatrix<ValueType> toMatrix(std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const;
/*!
* Converts the ADD to a row-grouped (sparse) double matrix. The given offset-labeled DDs are used to
@@ -579,7 +576,7 @@ namespace storm {
* @param columnOdd The ODD used for determining the correct column.
* @return The matrix that is represented by this ADD.
*/
- storm::storage::SparseMatrix<ValueType> toMatrix(std::set<storm::expressions::Variable> const& groupMetaVariables, storm::dd::Odd<LibraryType> const& rowOdd, storm::dd::Odd<LibraryType> const& columnOdd) const;
+ storm::storage::SparseMatrix<ValueType> toMatrix(std::set<storm::expressions::Variable> const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const;
/*!
* Converts the ADD to a row-grouped (sparse) double matrix and the given vector to a row-grouped vector.
@@ -594,7 +591,7 @@ namespace storm {
* @param columnOdd The ODD used for determining the correct column.
* @return The matrix that is represented by this ADD.
*/
- std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<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::pair<storm::storage::SparseMatrix<ValueType>, std::vector<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 const& rowOdd, storm::dd::Odd const& columnOdd) const;
/*!
* Exports the DD to the given file in the dot format.
@@ -631,6 +628,13 @@ namespace storm {
*/
Bdd<LibraryType> toBdd() const;
+ /*!
+ * Creates an ODD based on the current ADD.
+ *
+ * @return The corresponding ODD.
+ */
+ Odd createOdd() const;
+
private:
/*!
* Creates a DD that encapsulates the given CUDD ADD.
@@ -660,7 +664,7 @@ namespace storm {
* @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<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;
+ storm::storage::SparseMatrix<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 const& rowOdd, storm::dd::Odd const& columnOdd) const;
/*!
* Converts the ADD to a row-grouped (sparse) double matrix and the given vector to an equally row-grouped
@@ -678,7 +682,7 @@ namespace storm {
* @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<ValueType>, std::vector<ValueType>> toMatrixVector(storm::dd::Add<LibraryType, ValueType> 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<LibraryType> const& rowOdd, storm::dd::Odd<LibraryType> const& columnOdd) const;
+ std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<ValueType>> toMatrixVector(storm::dd::Add<LibraryType, ValueType> 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 const& rowOdd, storm::dd::Odd const& columnOdd) const;
// The internal ADD that depends on the chosen library.
InternalAdd<LibraryType, ValueType> internalAdd;
diff --git a/src/storage/dd/Bdd.cpp b/src/storage/dd/Bdd.cpp
index e199ad58a..49c736e08 100644
--- a/src/storage/dd/Bdd.cpp
+++ b/src/storage/dd/Bdd.cpp
@@ -6,6 +6,7 @@
#include "src/storage/dd/DdMetaVariable.h"
#include "src/storage/dd/DdManager.h"
+#include "src/storage/dd/Odd.h"
#include "src/storage/BitVector.h"
@@ -21,7 +22,7 @@ namespace storm {
}
template<DdType LibraryType>
- Bdd<LibraryType> Bdd<LibraryType>::fromVector(std::shared_ptr<DdManager<LibraryType> const> ddManager, std::vector<double> const& explicitValues, storm::dd::Odd<LibraryType> const& odd, std::set<storm::expressions::Variable> const& metaVariables, storm::logic::ComparisonType comparisonType, double value) {
+ Bdd<LibraryType> Bdd<LibraryType>::fromVector(std::shared_ptr<DdManager<LibraryType> const> ddManager, std::vector<double> const& explicitValues, storm::dd::Odd const& odd, std::set<storm::expressions::Variable> const& metaVariables, storm::logic::ComparisonType comparisonType, double value) {
switch (comparisonType) {
case storm::logic::ComparisonType::Less:
return fromVector<double>(ddManager, explicitValues, odd, metaVariables, std::bind(std::greater<double>(), value, std::placeholders::_1));
@@ -36,7 +37,7 @@ namespace storm {
template<DdType LibraryType>
template<typename ValueType>
- Bdd<LibraryType> Bdd<LibraryType>::fromVector(std::shared_ptr<DdManager<LibraryType> const> ddManager, std::vector<ValueType> const& values, Odd<LibraryType> const& odd, std::set<storm::expressions::Variable> const& metaVariables, std::function<bool (ValueType const&)> const& filter) {
+ Bdd<LibraryType> Bdd<LibraryType>::fromVector(std::shared_ptr<DdManager<LibraryType> const> ddManager, std::vector<ValueType> const& values, Odd const& odd, std::set<storm::expressions::Variable> const& metaVariables, std::function<bool (ValueType const&)> const& filter) {
return Bdd<LibraryType>(ddManager, InternalBdd<LibraryType>::fromVector(&ddManager->internalDdManager, values, odd, ddManager->getSortedVariableIndices(metaVariables), filter), metaVariables);
}
@@ -175,7 +176,7 @@ namespace storm {
}
template<DdType LibraryType>
- storm::storage::BitVector Bdd<LibraryType>::toVector(storm::dd::Odd<LibraryType> const& rowOdd) const {
+ storm::storage::BitVector Bdd<LibraryType>::toVector(storm::dd::Odd const& rowOdd) const {
return internalBdd.toVector(rowOdd, this->getSortedVariableIndices());
}
@@ -232,6 +233,19 @@ namespace storm {
return cube;
}
+ template<DdType LibraryType>
+ Odd Bdd<LibraryType>::createOdd() const {
+ return internalBdd.createOdd(this->getSortedVariableIndices());
+ }
+
+ template<DdType LibraryType>
+ template<typename ValueType>
+ std::vector<ValueType> Bdd<LibraryType>::filterExplicitVector(Odd const& odd, std::vector<ValueType> const& values) const {
+ std::vector<ValueType> result(this->getNonZeroCount());
+ internalBdd.filterExplicitVector(odd, this->getSortedVariableIndices(), values, result);
+ return result;
+ }
+
template<DdType LibraryType>
Bdd<LibraryType>::operator InternalBdd<LibraryType>() const {
return internalBdd;
@@ -239,10 +253,13 @@ namespace storm {
template class Bdd<DdType::CUDD>;
- template Bdd<DdType::CUDD> Bdd<DdType::CUDD>::fromVector(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, std::function<bool (double const&)> const& filter);
- template Bdd<DdType::CUDD> Bdd<DdType::CUDD>::fromVector(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, std::vector<uint_fast64_t> const& values, Odd<DdType::CUDD> const& odd, std::set<storm::expressions::Variable> const& metaVariables, std::function<bool (uint_fast64_t const&)> const& filter);
+ template Bdd<DdType::CUDD> Bdd<DdType::CUDD>::fromVector(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, std::vector<double> const& values, Odd const& odd, std::set<storm::expressions::Variable> const& metaVariables, std::function<bool (double const&)> const& filter);
+ template Bdd<DdType::CUDD> Bdd<DdType::CUDD>::fromVector(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, std::vector<uint_fast64_t> const& values, Odd const& odd, std::set<storm::expressions::Variable> const& metaVariables, std::function<bool (uint_fast64_t const&)> const& filter);
template Add<DdType::CUDD, double> Bdd<DdType::CUDD>::toAdd() const;
template Add<DdType::CUDD, uint_fast64_t> Bdd<DdType::CUDD>::toAdd() const;
+
+ template std::vector<double> Bdd<DdType::CUDD>::filterExplicitVector(Odd const& odd, std::vector<double> const& values) const;
+ template std::vector<uint_fast64_t> Bdd<DdType::CUDD>::filterExplicitVector(Odd const& odd, std::vector<uint_fast64_t> const& values) const;
}
}
\ No newline at end of file
diff --git a/src/storage/dd/Bdd.h b/src/storage/dd/Bdd.h
index ecb1028e9..e5c0fe5b3 100644
--- a/src/storage/dd/Bdd.h
+++ b/src/storage/dd/Bdd.h
@@ -11,7 +11,6 @@ namespace storm {
template<DdType LibraryType, typename ValueType>
class Add;
- template<DdType LibraryType>
class Odd;
template<DdType LibraryType>
@@ -22,8 +21,6 @@ namespace storm {
template<DdType LibraryTypePrime, typename ValueTypePrime>
friend class Add;
- friend class Odd<LibraryType>;
-
// Instantiate all copy/move constructors/assignments with the default implementation.
Bdd() = default;
Bdd(Bdd<LibraryType> const& other) = default;
@@ -41,7 +38,7 @@ namespace storm {
* @param comparisonType The relation that needs to hold for the values (wrt. to the given value).
* @param value The value to compare with.
*/
- static Bdd<LibraryType> fromVector(std::shared_ptr<DdManager<LibraryType> const> ddManager, std::vector<double> const& explicitValues, storm::dd::Odd<LibraryType> const& odd, std::set<storm::expressions::Variable> const& metaVariables, storm::logic::ComparisonType comparisonType, double value);
+ static Bdd<LibraryType> fromVector(std::shared_ptr<DdManager<LibraryType> const> ddManager, std::vector<double> const& explicitValues, storm::dd::Odd const& odd, std::set<storm::expressions::Variable> const& metaVariables, storm::logic::ComparisonType comparisonType, double value);
/*!
* Retrieves whether the two BDDs represent the same function.
@@ -222,7 +219,7 @@ namespace storm {
* @param rowOdd The ODD used for determining the correct row.
* @return The bit vector that is represented by this BDD.
*/
- storm::storage::BitVector toVector(storm::dd::Odd<LibraryType> const& rowOdd) const;
+ storm::storage::BitVector toVector(storm::dd::Odd const& rowOdd) const;
virtual Bdd<LibraryType> getSupport() const override;
@@ -244,6 +241,23 @@ namespace storm {
*/
static Bdd<LibraryType> getCube(DdManager<LibraryType> const& manager, std::set<storm::expressions::Variable> const& metaVariables);
+ /*!
+ * Creates an ODD based on the current BDD.
+ *
+ * @return The corresponding ODD.
+ */
+ Odd createOdd() const;
+
+ /*!
+ * Filters the given explicit vector using the symbolic representation of which values to select.
+ *
+ * @param selectedValues A symbolic representation of which values to select.
+ * @param values The value vector from which to select the values.
+ * @return The resulting vector.
+ */
+ template<typename ValueType>
+ std::vector<ValueType> filterExplicitVector(Odd const& odd, std::vector<ValueType> const& values) const;
+
private:
/*!
* We provide a conversion operator from the BDD to its internal type to ease calling the internal functions.
@@ -270,7 +284,7 @@ namespace storm {
* @return The resulting (CUDD) BDD.
*/
template<typename ValueType>
- static Bdd<LibraryType> fromVector(std::shared_ptr<DdManager<LibraryType> const> ddManager, std::vector<ValueType> const& values, Odd<LibraryType> const& odd, std::set<storm::expressions::Variable> const& metaVariables, std::function<bool (ValueType const&)> const& filter);
+ static Bdd<LibraryType> fromVector(std::shared_ptr<DdManager<LibraryType> const> ddManager, std::vector<ValueType> const& values, Odd const& odd, std::set<storm::expressions::Variable> const& metaVariables, std::function<bool (ValueType const&)> const& filter);
// The internal BDD that depends on the chosen library.
InternalBdd<LibraryType> internalBdd;
diff --git a/src/storage/dd/Dd.h b/src/storage/dd/Dd.h
index e347f1021..d91989d6a 100644
--- a/src/storage/dd/Dd.h
+++ b/src/storage/dd/Dd.h
@@ -17,15 +17,11 @@ namespace storm {
template<DdType LibraryType>
class Bdd;
- template<DdType LibraryType>
- class Odd;
-
template<DdType LibraryType>
class Dd {
public:
// Declare the DdManager so it can access the internals of a DD.
friend class DdManager<LibraryType>;
- friend class Odd<LibraryType>;
// Instantiate all copy/move constructors/assignments with the default implementation.
Dd() = default;
diff --git a/src/storage/dd/DdManager.h b/src/storage/dd/DdManager.h
index c6b238905..fa7e5d3ea 100644
--- a/src/storage/dd/DdManager.h
+++ b/src/storage/dd/DdManager.h
@@ -16,15 +16,11 @@
namespace storm {
namespace dd {
- template<DdType LibraryType>
- class Odd;
-
// Declare DdManager class so we can then specialize it for the different DD types.
template<DdType LibraryType>
class DdManager : public std::enable_shared_from_this<DdManager<LibraryType>> {
public:
friend class Bdd<LibraryType>;
- friend class Odd<LibraryType>;
template<DdType LibraryTypePrime, typename ValueType>
friend class Add;
diff --git a/src/storage/dd/Odd.cpp b/src/storage/dd/Odd.cpp
index 23e855253..7bf0f18ab 100644
--- a/src/storage/dd/Odd.cpp
+++ b/src/storage/dd/Odd.cpp
@@ -1 +1,143 @@
-#include "src/storage/dd/Odd.h"
\ No newline at end of file
+#include "src/storage/dd/Odd.h"
+
+#include <set>
+#include <fstream>
+#include <boost/algorithm/string/join.hpp>
+
+#include "src/utility/macros.h"
+#include "src/exceptions/InvalidArgumentException.h"
+
+namespace storm {
+ namespace dd {
+ Odd::Odd(std::shared_ptr<Odd> elseNode, uint_fast64_t elseOffset, std::shared_ptr<Odd> thenNode, uint_fast64_t thenOffset) : elseNode(elseNode), thenNode(thenNode), elseOffset(elseOffset), thenOffset(thenOffset) {
+ // Intentionally left empty.
+ }
+
+ Odd const& Odd::getThenSuccessor() const {
+ return *this->thenNode;
+ }
+
+ Odd const& Odd::getElseSuccessor() const {
+ return *this->elseNode;
+ }
+
+ uint_fast64_t Odd::getElseOffset() const {
+ return this->elseOffset;
+ }
+
+ void Odd::setElseOffset(uint_fast64_t newOffset) {
+ this->elseOffset = newOffset;
+ }
+
+ uint_fast64_t Odd::getThenOffset() const {
+ return this->thenOffset;
+ }
+
+ void Odd::setThenOffset(uint_fast64_t newOffset) {
+ this->thenOffset = newOffset;
+ }
+
+ uint_fast64_t Odd::getTotalOffset() const {
+ return this->elseOffset + this->thenOffset;
+ }
+
+ uint_fast64_t Odd::getNodeCount() const {
+ // If the ODD contains a constant (and thus has no children), the size is 1.
+ if (this->elseNode == nullptr && this->thenNode == nullptr) {
+ return 1;
+ }
+
+ // If the two successors are actually the same, we need to count the subnodes only once.
+ if (this->elseNode == this->thenNode) {
+ return this->elseNode->getNodeCount();
+ } else {
+ return this->elseNode->getNodeCount() + this->thenNode->getNodeCount();
+ }
+ }
+
+ uint_fast64_t Odd::getHeight() const {
+ if (this->isTerminalNode()) {
+ return 1;
+ } else {
+ return 1 + this->getElseSuccessor().getHeight();
+ }
+ }
+
+ bool Odd::isTerminalNode() const {
+ return this->elseNode == nullptr && this->thenNode == nullptr;
+ }
+
+ void Odd::expandExplicitVector(storm::dd::Odd const& newOdd, std::vector<double> const& oldValues, std::vector<double>& newValues) const {
+ expandValuesToVectorRec(0, *this, oldValues, 0, newOdd, newValues);
+ }
+
+ void Odd::expandValuesToVectorRec(uint_fast64_t oldOffset, storm::dd::Odd const& oldOdd, std::vector<double> const& oldValues, uint_fast64_t newOffset, storm::dd::Odd const& newOdd, std::vector<double>& newValues) {
+ if (oldOdd.isTerminalNode()) {
+ STORM_LOG_THROW(newOdd.isTerminalNode(), storm::exceptions::InvalidArgumentException, "The ODDs for the translation must have the same height.");
+ if (oldOdd.getThenOffset() != 0) {
+ newValues[newOffset] += oldValues[oldOffset];
+ }
+ } else {
+ expandValuesToVectorRec(oldOffset, oldOdd.getElseSuccessor(), oldValues, newOffset, newOdd.getElseSuccessor(), newValues);
+ expandValuesToVectorRec(oldOffset + oldOdd.getElseOffset(), oldOdd.getThenSuccessor(), oldValues, newOffset + newOdd.getElseOffset(), newOdd.getThenSuccessor(), newValues);
+ }
+ }
+
+ void Odd::exportToDot(std::string const& filename) const {
+ std::ofstream dotFile;
+ dotFile.open (filename);
+
+ // Print header.
+ dotFile << "digraph \"ODD\" {" << std::endl << "center=true;" << std::endl << "edge [dir = none];" << std::endl;
+
+ // Print levels as ranks.
+ dotFile << "{ node [shape = plaintext];" << std::endl << "edge [style = invis];" << std::endl;
+ std::vector<std::string> levelNames;
+ for (uint_fast64_t level = 0; level < this->getHeight(); ++level) {
+ levelNames.push_back("\"" + std::to_string(level) + "\"");
+ }
+ dotFile << boost::join(levelNames, " -> ") << ";";
+ dotFile << "}" << std::endl;
+
+ std::map<uint_fast64_t, std::vector<std::reference_wrapper<storm::dd::Odd const>>> levelToOddNodesMap;
+ this->addToLevelToOddNodesMap(levelToOddNodesMap);
+
+ for (auto const& levelNodes : levelToOddNodesMap) {
+ dotFile << "{ rank = same; \"" << levelNodes.first << "\"" << std::endl;;
+ for (auto const& node : levelNodes.second) {
+ dotFile << "\"" << &node.get() << "\";" << std::endl;
+ }
+ dotFile << "}" << std::endl;
+ }
+
+ std::set<storm::dd::Odd const*> printedNodes;
+ for (auto const& levelNodes : levelToOddNodesMap) {
+ for (auto const& node : levelNodes.second) {
+ if (printedNodes.find(&node.get()) != printedNodes.end()) {
+ continue;
+ } else {
+ printedNodes.insert(&node.get());
+ }
+
+ dotFile << "\"" << &node.get() << "\" [label=\"" << levelNodes.first << "\"];" << std::endl;
+ if (!node.get().isTerminalNode()) {
+ dotFile << "\"" << &node.get() << "\" -> \"" << &node.get().getElseSuccessor() << "\" [style=dashed, label=\"0\"];" << std::endl;
+ dotFile << "\"" << &node.get() << "\" -> \"" << &node.get().getThenSuccessor() << "\" [style=solid, label=\"" << node.get().getElseOffset() << "\"];" << std::endl;
+ }
+ }
+ }
+
+ dotFile << "}" << std::endl;
+
+ dotFile.close();
+ }
+
+ void Odd::addToLevelToOddNodesMap(std::map<uint_fast64_t, std::vector<std::reference_wrapper<storm::dd::Odd const>>>& levelToOddNodesMap, uint_fast64_t level) const {
+ levelToOddNodesMap[level].push_back(*this);
+ if (!this->isTerminalNode()) {
+ this->getElseSuccessor().addToLevelToOddNodesMap(levelToOddNodesMap, level + 1);
+ this->getThenSuccessor().addToLevelToOddNodesMap(levelToOddNodesMap, level + 1);
+ }
+ }
+ }
+}
\ No newline at end of file
diff --git a/src/storage/dd/Odd.h b/src/storage/dd/Odd.h
index a4c0a62a3..131785adf 100644
--- a/src/storage/dd/Odd.h
+++ b/src/storage/dd/Odd.h
@@ -1,12 +1,151 @@
#ifndef STORM_STORAGE_DD_ODD_H_
#define STORM_STORAGE_DD_ODD_H_
-#include "src/storage/dd/DdType.h"
+#include <vector>
+#include <map>
namespace storm {
namespace dd {
- template<DdType Type>
- class Odd;
+ class Odd {
+ public:
+ /*!
+ * Constructs an offset-labeled DD with the given topmost DD node, else- and then-successor.
+ *
+ * @param dd The DD node associated with this ODD node.
+ * @param elseNode The else-successor of thie ODD node.
+ * @param elseOffset The offset of the else-successor.
+ * @param thenNode The then-successor of thie ODD node.
+ * @param thenOffset The offset of the then-successor.
+ */
+ Odd(std::shared_ptr<Odd> elseNode, uint_fast64_t elseOffset, std::shared_ptr<Odd> thenNode, uint_fast64_t thenOffset);
+
+ // Instantiate all copy/move constructors/assignments with the default implementation.
+ Odd() = default;
+ Odd(Odd const& other) = default;
+ Odd& operator=(Odd const& other) = default;
+#ifndef WINDOWS
+ Odd(Odd&& other) = default;
+ Odd& operator=(Odd&& other) = default;
+#endif
+
+ /*!
+ * Retrieves the then-successor of this ODD node.
+ *
+ * @return The then-successor of this ODD node.
+ */
+ Odd const& getThenSuccessor() const;
+
+ /*!
+ * Retrieves the else-successor of this ODD node.
+ *
+ * @return The else-successor of this ODD node.
+ */
+ Odd const& getElseSuccessor() const;
+
+ /*!
+ * Retrieves the else-offset of this ODD node.
+ *
+ * @return The else-offset of this ODD node.
+ */
+ uint_fast64_t getElseOffset() const;
+
+ /*!
+ * Sets the else-offset of this ODD node.
+ *
+ * @param newOffset The new else-offset of this ODD node.
+ */
+ void setElseOffset(uint_fast64_t newOffset);
+
+ /*!
+ * Retrieves the then-offset of this ODD node.
+ *
+ * @return The then-offset of this ODD node.
+ */
+ uint_fast64_t getThenOffset() const;
+
+ /*!
+ * Sets the then-offset of this ODD node.
+ *
+ * @param newOffset The new then-offset of this ODD node.
+ */
+ void setThenOffset(uint_fast64_t newOffset);
+
+ /*!
+ * Retrieves the total offset, i.e., the sum of the then- and else-offset.
+ *
+ * @return The total offset of this ODD.
+ */
+ uint_fast64_t getTotalOffset() const;
+
+ /*!
+ * Retrieves the size of the ODD. Note: the size is computed by a traversal, so this may be costlier than
+ * expected.
+ *
+ * @return The size (in nodes) of this ODD.
+ */
+ uint_fast64_t getNodeCount() const;
+
+ /*!
+ * Retrieves the height of the ODD.
+ *
+ * @return The height of the ODD.
+ */
+ uint_fast64_t getHeight() const;
+
+ /*!
+ * Checks whether the given ODD node is a terminal node, i.e. has no successors.
+ *
+ * @return True iff the node is terminal.
+ */
+ bool isTerminalNode() const;
+
+ /*!
+ * Adds the old values to the new values. It does so by writing the old values at their correct positions
+ * wrt. to the new ODD.
+ *
+ * @param newOdd The new ODD to use.
+ * @param oldValues The old vector of values (which is being read).
+ * @param newValues The new vector of values (which is being written).
+ */
+ void expandExplicitVector(storm::dd::Odd const& newOdd, std::vector<double> const& oldValues, std::vector<double>& newValues) const;
+
+ /*!
+ * Exports the ODD in the dot format to the given file.
+ *
+ * @param filename The name of the file to which to write the dot output.
+ */
+ void exportToDot(std::string const& filename) const;
+
+ private:
+ /*!
+ * Adds all nodes below the current one to the given mapping.
+ *
+ * @param levelToOddNodesMap A mapping of the level to the ODD node.
+ * @param The level of the current node.
+ */
+ void addToLevelToOddNodesMap(std::map<uint_fast64_t, std::vector<std::reference_wrapper<storm::dd::Odd const>>>& levelToOddNodesMap, uint_fast64_t level = 0) const;
+
+ /*!
+ * Adds the values of the old explicit values to the new explicit values where the positions in the old vector
+ * are given by the current old ODD and the positions in the new vector are given by the new ODD.
+ *
+ * @param oldOffset The offset in the old explicit values.
+ * @param oldOdd The ODD to use for the old explicit values.
+ * @param oldValues The vector of old values.
+ * @param newOffset The offset in the new explicit values.
+ * @param newOdd The ODD to use for the new explicit values.
+ * @param newValues The vector of new values.
+ */
+ static void expandValuesToVectorRec(uint_fast64_t oldOffset, storm::dd::Odd const& oldOdd, std::vector<double> const& oldValues, uint_fast64_t newOffset, storm::dd::Odd const& newOdd, std::vector<double>& newValues);
+
+ // The then- and else-nodes.
+ std::shared_ptr<Odd> elseNode;
+ std::shared_ptr<Odd> thenNode;
+
+ // The offsets that need to be added if the then- or else-successor is taken, respectively.
+ uint_fast64_t elseOffset;
+ uint_fast64_t thenOffset;
+ };
}
}
diff --git a/src/storage/dd/cudd/CuddOdd.cpp b/src/storage/dd/cudd/CuddOdd.cpp
deleted file mode 100644
index 96e4a339f..000000000
--- a/src/storage/dd/cudd/CuddOdd.cpp
+++ /dev/null
@@ -1,332 +0,0 @@
-#include "src/storage/dd/cudd/CuddOdd.h"
-
-#include <fstream>
-#include <algorithm>
-#include <boost/functional/hash.hpp>
-#include <boost/algorithm/string/join.hpp>
-
-#include "src/exceptions/InvalidArgumentException.h"
-#include "src/utility/macros.h"
-
-#include "src/storage/dd/DdManager.h"
-#include "src/storage/dd/DdMetaVariable.h"
-
-namespace storm {
- namespace dd {
- template<typename ValueType>
- Odd<DdType::CUDD>::Odd(Add<DdType::CUDD, ValueType> const& add) {
- std::shared_ptr<DdManager<DdType::CUDD> const> manager = add.getDdManager();
-
- // First, we need to determine the involved DD variables indices.
- std::vector<uint_fast64_t> ddVariableIndices = add.getSortedVariableIndices();
-
- // Prepare a unique table for each level that keeps the constructed ODD nodes unique.
- std::vector<std::unordered_map<DdNode*, std::shared_ptr<Odd<DdType::CUDD>>>> uniqueTableForLevels(ddVariableIndices.size() + 1);
-
- // Now construct the ODD structure from the ADD.
- std::shared_ptr<Odd<DdType::CUDD>> rootOdd = buildOddFromAddRec(add.internalAdd.getCuddDdNode(), manager->internalDdManager.getCuddManager(), 0, ddVariableIndices.size(), ddVariableIndices, uniqueTableForLevels);
-
- // Finally, move the children of the root ODD into this ODD.
- this->elseNode = std::move(rootOdd->elseNode);
- this->thenNode = std::move(rootOdd->thenNode);
- this->elseOffset = rootOdd->elseOffset;
- this->thenOffset = rootOdd->thenOffset;
- }
-
- Odd<DdType::CUDD>::Odd(Bdd<DdType::CUDD> const& bdd) {
- std::shared_ptr<DdManager<DdType::CUDD> const> manager = bdd.getDdManager();
-
- // First, we need to determine the involved DD variables indices.
- std::vector<uint_fast64_t> ddVariableIndices = bdd.getSortedVariableIndices();
-
- // Prepare a unique table for each level that keeps the constructed ODD nodes unique.
- std::vector<std::unordered_map<std::pair<DdNode*, bool>, std::shared_ptr<Odd<DdType::CUDD>>, HashFunctor>> uniqueTableForLevels(ddVariableIndices.size() + 1);
-
- // Now construct the ODD structure from the BDD.
- std::shared_ptr<Odd<DdType::CUDD>> rootOdd = buildOddFromBddRec(Cudd_Regular(bdd.internalBdd.getCuddDdNode()), manager->internalDdManager.getCuddManager(), 0, Cudd_IsComplement(bdd.internalBdd.getCuddDdNode()), ddVariableIndices.size(), ddVariableIndices, uniqueTableForLevels);
-
- // Finally, move the children of the root ODD into this ODD.
- this->elseNode = std::move(rootOdd->elseNode);
- this->thenNode = std::move(rootOdd->thenNode);
- this->elseOffset = rootOdd->elseOffset;
- this->thenOffset = rootOdd->thenOffset;
- }
-
- Odd<DdType::CUDD>::Odd(std::shared_ptr<Odd<DdType::CUDD>> elseNode, uint_fast64_t elseOffset, std::shared_ptr<Odd<DdType::CUDD>> thenNode, uint_fast64_t thenOffset) : elseNode(elseNode), thenNode(thenNode), elseOffset(elseOffset), thenOffset(thenOffset) {
- // Intentionally left empty.
- }
-
- Odd<DdType::CUDD> const& Odd<DdType::CUDD>::getThenSuccessor() const {
- return *this->thenNode;
- }
-
- Odd<DdType::CUDD> const& Odd<DdType::CUDD>::getElseSuccessor() const {
- return *this->elseNode;
- }
-
- uint_fast64_t Odd<DdType::CUDD>::getElseOffset() const {
- return this->elseOffset;
- }
-
- void Odd<DdType::CUDD>::setElseOffset(uint_fast64_t newOffset) {
- this->elseOffset = newOffset;
- }
-
- uint_fast64_t Odd<DdType::CUDD>::getThenOffset() const {
- return this->thenOffset;
- }
-
- void Odd<DdType::CUDD>::setThenOffset(uint_fast64_t newOffset) {
- this->thenOffset = newOffset;
- }
-
- uint_fast64_t Odd<DdType::CUDD>::getTotalOffset() const {
- return this->elseOffset + this->thenOffset;
- }
-
- uint_fast64_t Odd<DdType::CUDD>::getNodeCount() const {
- // If the ODD contains a constant (and thus has no children), the size is 1.
- if (this->elseNode == nullptr && this->thenNode == nullptr) {
- return 1;
- }
-
- // If the two successors are actually the same, we need to count the subnodes only once.
- if (this->elseNode == this->thenNode) {
- return this->elseNode->getNodeCount();
- } else {
- return this->elseNode->getNodeCount() + this->thenNode->getNodeCount();
- }
- }
-
- uint_fast64_t Odd<DdType::CUDD>::getHeight() const {
- if (this->isTerminalNode()) {
- return 1;
- } else {
- return 1 + this->getElseSuccessor().getHeight();
- }
- }
-
- bool Odd<DdType::CUDD>::isTerminalNode() const {
- return this->elseNode == nullptr && this->thenNode == nullptr;
- }
-
- std::vector<double> Odd<DdType::CUDD>::filterExplicitVector(storm::dd::Bdd<DdType::CUDD> const& selectedValues, std::vector<double> const& values) const {
- std::vector<double> result(selectedValues.getNonZeroCount());
-
- // First, we need to determine the involved DD variables indices.
- std::vector<uint_fast64_t> ddVariableIndices = selectedValues.getSortedVariableIndices();
-
- uint_fast64_t currentIndex = 0;
- addSelectedValuesToVectorRec(selectedValues.internalBdd.getCuddDdNode(), selectedValues.getDdManager()->internalDdManager.getCuddManager(), 0, Cudd_IsComplement(selectedValues.internalBdd.getCuddDdNode()), ddVariableIndices.size(), ddVariableIndices, 0, *this, result, currentIndex, values);
- return result;
- }
-
- void Odd<DdType::CUDD>::expandExplicitVector(storm::dd::Odd<DdType::CUDD> const& newOdd, std::vector<double> const& oldValues, std::vector<double>& newValues) const {
- expandValuesToVectorRec(0, *this, oldValues, 0, newOdd, newValues);
- }
-
- void Odd<DdType::CUDD>::expandValuesToVectorRec(uint_fast64_t oldOffset, storm::dd::Odd<DdType::CUDD> const& oldOdd, std::vector<double> const& oldValues, uint_fast64_t newOffset, storm::dd::Odd<DdType::CUDD> const& newOdd, std::vector<double>& newValues) {
- if (oldOdd.isTerminalNode()) {
- STORM_LOG_THROW(newOdd.isTerminalNode(), storm::exceptions::InvalidArgumentException, "The ODDs for the translation must have the same height.");
- if (oldOdd.getThenOffset() != 0) {
- newValues[newOffset] += oldValues[oldOffset];
- }
- } else {
- expandValuesToVectorRec(oldOffset, oldOdd.getElseSuccessor(), oldValues, newOffset, newOdd.getElseSuccessor(), newValues);
- expandValuesToVectorRec(oldOffset + oldOdd.getElseOffset(), oldOdd.getThenSuccessor(), oldValues, newOffset + newOdd.getElseOffset(), newOdd.getThenSuccessor(), newValues);
- }
- }
-
- void Odd<DdType::CUDD>::addSelectedValuesToVectorRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector<uint_fast64_t> const& ddVariableIndices, uint_fast64_t currentOffset, storm::dd::Odd<DdType::CUDD> const& odd, std::vector<double>& result, uint_fast64_t& currentIndex, std::vector<double> const& values) {
- // If there are no more values to select, we can directly return.
- if (dd == Cudd_ReadLogicZero(manager.getManager()) && !complement) {
- return;
- } else if (dd == Cudd_ReadOne(manager.getManager()) && complement) {
- return;
- }
-
- if (currentLevel == maxLevel) {
- // If the DD is not the zero leaf, then the then-offset is 1.
- bool selected = false;
- if (dd != Cudd_ReadLogicZero(manager.getManager())) {
- selected = !complement;
- }
-
- if (selected) {
- result[currentIndex++] = values[currentOffset];
- }
- } 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.
- addSelectedValuesToVectorRec(dd, manager, currentLevel + 1, complement, maxLevel, ddVariableIndices, currentOffset, odd.getElseSuccessor(), result, currentIndex, values);
- addSelectedValuesToVectorRec(dd, manager, currentLevel + 1, complement, maxLevel, ddVariableIndices, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), result, currentIndex, values);
- } else {
- // Otherwise, we compute the ODDs for both the then- and else successors.
- DdNode* thenDdNode = Cudd_T(dd);
- DdNode* elseDdNode = Cudd_E(dd);
-
- // Determine whether we have to evaluate the successors as if they were complemented.
- bool elseComplemented = Cudd_IsComplement(elseDdNode) ^ complement;
- bool thenComplemented = Cudd_IsComplement(thenDdNode) ^ complement;
-
- addSelectedValuesToVectorRec(Cudd_Regular(elseDdNode), manager, currentLevel + 1, elseComplemented, maxLevel, ddVariableIndices, currentOffset, odd.getElseSuccessor(), result, currentIndex, values);
- addSelectedValuesToVectorRec(Cudd_Regular(thenDdNode), manager, currentLevel + 1, thenComplemented, maxLevel, ddVariableIndices, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), result, currentIndex, values);
- }
- }
-
- void Odd<DdType::CUDD>::exportToDot(std::string const& filename) const {
- std::ofstream dotFile;
- dotFile.open (filename);
-
- // Print header.
- dotFile << "digraph \"ODD\" {" << std::endl << "center=true;" << std::endl << "edge [dir = none];" << std::endl;
-
- // Print levels as ranks.
- dotFile << "{ node [shape = plaintext];" << std::endl << "edge [style = invis];" << std::endl;
- std::vector<std::string> levelNames;
- for (uint_fast64_t level = 0; level < this->getHeight(); ++level) {
- levelNames.push_back("\"" + std::to_string(level) + "\"");
- }
- dotFile << boost::join(levelNames, " -> ") << ";";
- dotFile << "}" << std::endl;
-
- std::map<uint_fast64_t, std::vector<std::reference_wrapper<storm::dd::Odd<DdType::CUDD> const>>> levelToOddNodesMap;
- this->addToLevelToOddNodesMap(levelToOddNodesMap);
-
- for (auto const& levelNodes : levelToOddNodesMap) {
- dotFile << "{ rank = same; \"" << levelNodes.first << "\"" << std::endl;;
- for (auto const& node : levelNodes.second) {
- dotFile << "\"" << &node.get() << "\";" << std::endl;
- }
- dotFile << "}" << std::endl;
- }
-
- std::set<storm::dd::Odd<DdType::CUDD> const*> printedNodes;
- for (auto const& levelNodes : levelToOddNodesMap) {
- for (auto const& node : levelNodes.second) {
- if (printedNodes.find(&node.get()) != printedNodes.end()) {
- continue;
- } else {
- printedNodes.insert(&node.get());
- }
-
- dotFile << "\"" << &node.get() << "\" [label=\"" << levelNodes.first << "\"];" << std::endl;
- if (!node.get().isTerminalNode()) {
- dotFile << "\"" << &node.get() << "\" -> \"" << &node.get().getElseSuccessor() << "\" [style=dashed, label=\"0\"];" << std::endl;
- dotFile << "\"" << &node.get() << "\" -> \"" << &node.get().getThenSuccessor() << "\" [style=solid, label=\"" << node.get().getElseOffset() << "\"];" << std::endl;
- }
- }
- }
-
- dotFile << "}" << std::endl;
-
- dotFile.close();
- }
-
- void Odd<DdType::CUDD>::addToLevelToOddNodesMap(std::map<uint_fast64_t, std::vector<std::reference_wrapper<storm::dd::Odd<DdType::CUDD> const>>>& levelToOddNodesMap, uint_fast64_t level) const {
- levelToOddNodesMap[level].push_back(*this);
- if (!this->isTerminalNode()) {
- this->getElseSuccessor().addToLevelToOddNodesMap(levelToOddNodesMap, level + 1);
- this->getThenSuccessor().addToLevelToOddNodesMap(levelToOddNodesMap, level + 1);
- }
- }
-
- std::shared_ptr<Odd<DdType::CUDD>> Odd<DdType::CUDD>::buildOddFromAddRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<std::unordered_map<DdNode*, std::shared_ptr<Odd<DdType::CUDD>>>>& uniqueTableForLevels) {
- // Check whether the ODD for this node has already been computed (for this level) and if so, return this instead.
- auto const& iterator = uniqueTableForLevels[currentLevel].find(dd);
- if (iterator != uniqueTableForLevels[currentLevel].end()) {
- return iterator->second;
- } else {
- // Otherwise, we need to recursively compute the ODD.
-
- // If we are already past the maximal level that is to be considered, we can simply create an Odd without
- // successors
- if (currentLevel == maxLevel) {
- uint_fast64_t elseOffset = 0;
- uint_fast64_t thenOffset = 0;
-
- // If the DD is not the zero leaf, then the then-offset is 1.
- if (dd != Cudd_ReadZero(manager.getManager())) {
- thenOffset = 1;
- }
-
- return std::shared_ptr<Odd<DdType::CUDD>>(new Odd<DdType::CUDD>(nullptr, elseOffset, nullptr, thenOffset));
- } else if (ddVariableIndices[currentLevel] < static_cast<uint_fast64_t>(dd->index)) {
- // If we skipped the level in the DD, we compute the ODD just for the else-successor and use the same
- // node for the then-successor as well.
- std::shared_ptr<Odd<DdType::CUDD>> elseNode = buildOddFromAddRec(dd, manager, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels);
- std::shared_ptr<Odd<DdType::CUDD>> thenNode = elseNode;
- return std::shared_ptr<Odd<DdType::CUDD>>(new Odd<DdType::CUDD>(elseNode, elseNode->getElseOffset() + elseNode->getThenOffset(), thenNode, thenNode->getElseOffset() + thenNode->getThenOffset()));
- } else {
- // Otherwise, we compute the ODDs for both the then- and else successors.
- bool elseComplemented = Cudd_IsComplement(Cudd_E(dd));
- bool thenComplemented = Cudd_IsComplement(Cudd_T(dd));
- std::shared_ptr<Odd<DdType::CUDD>> elseNode = buildOddFromAddRec(Cudd_E(dd), manager, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels);
- std::shared_ptr<Odd<DdType::CUDD>> thenNode = buildOddFromAddRec(Cudd_T(dd), manager, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels);
- uint_fast64_t totalElseOffset = elseNode->getElseOffset() + elseNode->getThenOffset();
- uint_fast64_t totalThenOffset = thenNode->getElseOffset() + thenNode->getThenOffset();
- return std::shared_ptr<Odd<DdType::CUDD>>(new Odd<DdType::CUDD>(elseNode, elseComplemented ? (1ull << (maxLevel - currentLevel - 1)) - totalElseOffset : totalElseOffset, thenNode, thenComplemented ? (1ull << (maxLevel - currentLevel - 1)) - totalThenOffset : totalThenOffset));
- }
- }
- }
-
- std::size_t Odd<DdType::CUDD>::HashFunctor::operator()(std::pair<DdNode*, bool> const& key) const {
- std::size_t result = 0;
- boost::hash_combine(result, key.first);
- boost::hash_combine(result, key.second);
- return result;
- }
-
- std::shared_ptr<Odd<DdType::CUDD>> Odd<DdType::CUDD>::buildOddFromBddRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<std::unordered_map<std::pair<DdNode*, bool>, std::shared_ptr<Odd<DdType::CUDD>>, HashFunctor>>& uniqueTableForLevels) {
- // Check whether the ODD for this node has already been computed (for this level) and if so, return this instead.
- auto const& iterator = uniqueTableForLevels[currentLevel].find(std::make_pair(dd, complement));
- if (iterator != uniqueTableForLevels[currentLevel].end()) {
- return iterator->second;
- } else {
- // Otherwise, we need to recursively compute the ODD.
-
- // If we are already past the maximal level that is to be considered, we can simply create an Odd without
- // successors
- if (currentLevel == maxLevel) {
- uint_fast64_t elseOffset = 0;
- uint_fast64_t thenOffset = 0;
-
- // If the DD is not the zero leaf, then the then-offset is 1.
- if (dd != Cudd_ReadZero(manager.getManager())) {
- thenOffset = 1;
- }
-
- // If we need to complement the 'terminal' node, we need to negate its offset.
- if (complement) {
- thenOffset = 1 - thenOffset;
- }
-
- return std::shared_ptr<Odd<DdType::CUDD>>(new Odd<DdType::CUDD>(nullptr, elseOffset, nullptr, thenOffset));
- } else if (ddVariableIndices[currentLevel] < static_cast<uint_fast64_t>(dd->index)) {
- // If we skipped the level in the DD, we compute the ODD just for the else-successor and use the same
- // node for the then-successor as well.
- std::shared_ptr<Odd<DdType::CUDD>> elseNode = buildOddFromBddRec(dd, manager, currentLevel + 1, complement, maxLevel, ddVariableIndices, uniqueTableForLevels);
- std::shared_ptr<Odd<DdType::CUDD>> thenNode = elseNode;
- uint_fast64_t totalOffset = elseNode->getElseOffset() + elseNode->getThenOffset();
- return std::shared_ptr<Odd<DdType::CUDD>>(new Odd<DdType::CUDD>(elseNode, totalOffset, thenNode, totalOffset));
- } else {
- // Otherwise, we compute the ODDs for both the then- and else successors.
- DdNode* thenDdNode = Cudd_T(dd);
- DdNode* elseDdNode = Cudd_E(dd);
-
- // Determine whether we have to evaluate the successors as if they were complemented.
- bool elseComplemented = Cudd_IsComplement(elseDdNode) ^ complement;
- bool thenComplemented = Cudd_IsComplement(thenDdNode) ^ complement;
-
- std::shared_ptr<Odd<DdType::CUDD>> elseNode = buildOddFromBddRec(Cudd_Regular(elseDdNode), manager, currentLevel + 1, elseComplemented, maxLevel, ddVariableIndices, uniqueTableForLevels);
- std::shared_ptr<Odd<DdType::CUDD>> thenNode = buildOddFromBddRec(Cudd_Regular(thenDdNode), manager, currentLevel + 1, thenComplemented, maxLevel, ddVariableIndices, uniqueTableForLevels);
-
- return std::shared_ptr<Odd<DdType::CUDD>>(new Odd<DdType::CUDD>(elseNode, elseNode->getElseOffset() + elseNode->getThenOffset(), thenNode, thenNode->getElseOffset() + thenNode->getThenOffset()));
- }
- }
- }
-
- template Odd<DdType::CUDD>::Odd(Add<DdType::CUDD, double> const& add);
- template Odd<DdType::CUDD>::Odd(Add<DdType::CUDD, uint_fast64_t> const& add);
- }
-}
\ No newline at end of file
diff --git a/src/storage/dd/cudd/CuddOdd.h b/src/storage/dd/cudd/CuddOdd.h
deleted file mode 100644
index 79be50332..000000000
--- a/src/storage/dd/cudd/CuddOdd.h
+++ /dev/null
@@ -1,235 +0,0 @@
-#ifndef STORM_STORAGE_DD_CUDDODD_H_
-#define STORM_STORAGE_DD_CUDDODD_H_
-
-#include <memory>
-#include <unordered_map>
-
-#include "src/storage/dd/Odd.h"
-#include "src/storage/dd/Add.h"
-#include "src/utility/OsDetection.h"
-
-// Include the C++-interface of CUDD.
-#include "cuddObj.hh"
-
-namespace storm {
- namespace dd {
- template<>
- class Odd<DdType::CUDD> {
- public:
- /*!
- * Constructs an offset-labeled DD from the given ADD.
- *
- * @param add The ADD for which to build the offset-labeled ADD.
- */
- template<typename ValueType>
- Odd(Add<DdType::CUDD, ValueType> const& add);
-
- /*!
- * Constructs an offset-labeled DD from the given BDD.
- *
- * @param bdd The BDD for which to build the offset-labeled ADD.
- */
- Odd(Bdd<DdType::CUDD> const& bdd);
-
- // Instantiate all copy/move constructors/assignments with the default implementation.
- Odd() = default;
- Odd(Odd<DdType::CUDD> const& other) = default;
- Odd& operator=(Odd<DdType::CUDD> const& other) = default;
-#ifndef WINDOWS
- Odd(Odd<DdType::CUDD>&& other) = default;
- Odd& operator=(Odd<DdType::CUDD>&& other) = default;
-#endif
-
- /*!
- * Retrieves the then-successor of this ODD node.
- *
- * @return The then-successor of this ODD node.
- */
- Odd<DdType::CUDD> const& getThenSuccessor() const;
-
- /*!
- * Retrieves the else-successor of this ODD node.
- *
- * @return The else-successor of this ODD node.
- */
- Odd<DdType::CUDD> const& getElseSuccessor() const;
-
- /*!
- * Retrieves the else-offset of this ODD node.
- *
- * @return The else-offset of this ODD node.
- */
- uint_fast64_t getElseOffset() const;
-
- /*!
- * Sets the else-offset of this ODD node.
- *
- * @param newOffset The new else-offset of this ODD node.
- */
- void setElseOffset(uint_fast64_t newOffset);
-
- /*!
- * Retrieves the then-offset of this ODD node.
- *
- * @return The then-offset of this ODD node.
- */
- uint_fast64_t getThenOffset() const;
-
- /*!
- * Sets the then-offset of this ODD node.
- *
- * @param newOffset The new then-offset of this ODD node.
- */
- void setThenOffset(uint_fast64_t newOffset);
-
- /*!
- * Retrieves the total offset, i.e., the sum of the then- and else-offset.
- *
- * @return The total offset of this ODD.
- */
- uint_fast64_t getTotalOffset() const;
-
- /*!
- * Retrieves the size of the ODD. Note: the size is computed by a traversal, so this may be costlier than
- * expected.
- *
- * @return The size (in nodes) of this ODD.
- */
- uint_fast64_t getNodeCount() const;
-
- /*!
- * Retrieves the height of the ODD.
- *
- * @return The height of the ODD.
- */
- uint_fast64_t getHeight() const;
-
- /*!
- * Checks whether the given ODD node is a terminal node, i.e. has no successors.
- *
- * @return True iff the node is terminal.
- */
- bool isTerminalNode() const;
-
- /*!
- * Filters the given explicit vector using the symbolic representation of which values to select.
- *
- * @param selectedValues A symbolic representation of which values to select.
- * @param values The value vector from which to select the values.
- * @return The resulting vector.
- */
- std::vector<double> filterExplicitVector(storm::dd::Bdd<DdType::CUDD> const& selectedValues, std::vector<double> const& values) const;
-
- /*!
- * Adds the old values to the new values. It does so by writing the old values at their correct positions
- * wrt. to the new ODD.
- *
- * @param newOdd The new ODD to use.
- * @param oldValues The old vector of values (which is being read).
- * @param newValues The new vector of values (which is being written).
- */
- void expandExplicitVector(storm::dd::Odd<DdType::CUDD> const& newOdd, std::vector<double> const& oldValues, std::vector<double>& newValues) const;
-
- /*!
- * Exports the ODD in the dot format to the given file.
- *
- * @param filename The name of the file to which to write the dot output.
- */
- void exportToDot(std::string const& filename) const;
-
- private:
- // Declare a hash functor that is used for the unique tables in the construction process.
- class HashFunctor {
- public:
- std::size_t operator()(std::pair<DdNode*, bool> const& key) const;
- };
-
- /*!
- * Adds all nodes below the current one to the given mapping.
- *
- * @param levelToOddNodesMap A mapping of the level to the ODD node.
- * @param The level of the current node.
- */
- void addToLevelToOddNodesMap(std::map<uint_fast64_t, std::vector<std::reference_wrapper<storm::dd::Odd<DdType::CUDD> const>>>& levelToOddNodesMap, uint_fast64_t level = 0) const;
-
- /*!
- * Constructs an offset-labeled DD with the given topmost DD node, else- and then-successor.
- *
- * @param dd The DD node associated with this ODD node.
- * @param elseNode The else-successor of thie ODD node.
- * @param elseOffset The offset of the else-successor.
- * @param thenNode The then-successor of thie ODD node.
- * @param thenOffset The offset of the then-successor.
- */
- Odd(std::shared_ptr<Odd<DdType::CUDD>> elseNode, uint_fast64_t elseOffset, std::shared_ptr<Odd<DdType::CUDD>> thenNode, uint_fast64_t thenOffset);
-
- /*!
- * Recursively builds the ODD from an ADD (that has no complement edges).
- *
- * @param dd The DD for which to build the ODD.
- * @param manager The manager responsible for the DD.
- * @param currentLevel The currently considered level in the DD.
- * @param maxLevel The number of levels that need to be considered.
- * @param ddVariableIndices The (sorted) indices of all DD variables that need to be considered.
- * @param uniqueTableForLevels A vector of unique tables, one for each level to be considered, that keeps
- * ODD nodes for the same DD and level unique.
- * @return A pointer to the constructed ODD for the given arguments.
- */
- static std::shared_ptr<Odd<DdType::CUDD>> buildOddFromAddRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<std::unordered_map<DdNode*, std::shared_ptr<Odd<DdType::CUDD>>>>& uniqueTableForLevels);
-
- /*!
- * Recursively builds the ODD from a BDD (that potentially has complement edges).
- *
- * @param dd The DD for which to build the ODD.
- * @param manager The manager responsible for the DD.
- * @param currentLevel The currently considered level in the DD.
- * @param complement A flag indicating whether or not the given node is to be considered as complemented.
- * @param maxLevel The number of levels that need to be considered.
- * @param ddVariableIndices The (sorted) indices of all DD variables that need to be considered.
- * @param uniqueTableForLevels A vector of unique tables, one for each level to be considered, that keeps
- * ODD nodes for the same DD and level unique.
- * @return A pointer to the constructed ODD for the given arguments.
- */
- static std::shared_ptr<Odd<DdType::CUDD>> buildOddFromBddRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<std::unordered_map<std::pair<DdNode*, bool>, std::shared_ptr<Odd<DdType::CUDD>>, HashFunctor>>& uniqueTableForLevels);
-
- /*!
- * Adds the selected values the target vector.
- *
- * @param dd The current node of the DD representing the selected values.
- * @param manager The manager responsible for the DD.
- * @param currentLevel The currently considered level in the DD.
- * @param maxLevel The number of levels that need to be considered.
- * @param ddVariableIndices The sorted list of variable indices to use.
- * @param currentOffset The offset along the path taken in the DD representing the selected values.
- * @param odd The current ODD node.
- * @param result The target vector to which to write the values.
- * @param currentIndex The index at which the next element is to be written.
- * @param values The value vector from which to select the values.
- */
- static void addSelectedValuesToVectorRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector<uint_fast64_t> const& ddVariableIndices, uint_fast64_t currentOffset, storm::dd::Odd<DdType::CUDD> const& odd, std::vector<double>& result, uint_fast64_t& currentIndex, std::vector<double> const& values);
-
- /*!
- * Adds the values of the old explicit values to the new explicit values where the positions in the old vector
- * are given by the current old ODD and the positions in the new vector are given by the new ODD.
- *
- * @param oldOffset The offset in the old explicit values.
- * @param oldOdd The ODD to use for the old explicit values.
- * @param oldValues The vector of old values.
- * @param newOffset The offset in the new explicit values.
- * @param newOdd The ODD to use for the new explicit values.
- * @param newValues The vector of new values.
- */
- static void expandValuesToVectorRec(uint_fast64_t oldOffset, storm::dd::Odd<DdType::CUDD> const& oldOdd, std::vector<double> const& oldValues, uint_fast64_t newOffset, storm::dd::Odd<DdType::CUDD> const& newOdd, std::vector<double>& newValues);
-
- // The then- and else-nodes.
- std::shared_ptr<Odd<DdType::CUDD>> elseNode;
- std::shared_ptr<Odd<DdType::CUDD>> thenNode;
-
- // The offsets that need to be added if the then- or else-successor is taken, respectively.
- uint_fast64_t elseOffset;
- uint_fast64_t thenOffset;
- };
- }
-}
-
-#endif /* STORM_STORAGE_DD_CUDDODD_H_ */
\ No newline at end of file
diff --git a/src/storage/dd/cudd/InternalCuddAdd.cpp b/src/storage/dd/cudd/InternalCuddAdd.cpp
index fd7fb87bc..15a1706d8 100644
--- a/src/storage/dd/cudd/InternalCuddAdd.cpp
+++ b/src/storage/dd/cudd/InternalCuddAdd.cpp
@@ -1,9 +1,9 @@
#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/dd/cudd/CuddAddIterator.h"
+#include "src/storage/dd/Odd.h"
#include "src/storage/SparseMatrix.h"
@@ -350,17 +350,69 @@ namespace storm {
}
template<typename ValueType>
- void InternalAdd<DdType::CUDD, ValueType>::composeWithExplicitVector(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 {
+ Odd InternalAdd<DdType::CUDD, ValueType>::createOdd(std::vector<uint_fast64_t> const& ddVariableIndices) const {
+ // Prepare a unique table for each level that keeps the constructed ODD nodes unique.
+ std::vector<std::unordered_map<DdNode*, std::shared_ptr<Odd>>> uniqueTableForLevels(ddVariableIndices.size() + 1);
+
+ // Now construct the ODD structure from the ADD.
+ std::shared_ptr<Odd> rootOdd = createOddRec(this->getCuddDdNode(), ddManager->getCuddManager(), 0, ddVariableIndices.size(), ddVariableIndices, uniqueTableForLevels);
+
+ // Return a copy of the root node to remove the shared_ptr encapsulation.
+ return Odd(*rootOdd);
+ }
+
+ template<typename ValueType>
+ std::shared_ptr<Odd> InternalAdd<DdType::CUDD, ValueType>::createOddRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<std::unordered_map<DdNode*, std::shared_ptr<Odd>>>& uniqueTableForLevels) {
+ // Check whether the ODD for this node has already been computed (for this level) and if so, return this instead.
+ auto const& iterator = uniqueTableForLevels[currentLevel].find(dd);
+ if (iterator != uniqueTableForLevels[currentLevel].end()) {
+ return iterator->second;
+ } else {
+ // Otherwise, we need to recursively compute the ODD.
+
+ // If we are already past the maximal level that is to be considered, we can simply create an Odd without
+ // successors
+ if (currentLevel == maxLevel) {
+ uint_fast64_t elseOffset = 0;
+ uint_fast64_t thenOffset = 0;
+
+ // If the DD is not the zero leaf, then the then-offset is 1.
+ if (dd != Cudd_ReadZero(manager.getManager())) {
+ thenOffset = 1;
+ }
+
+ return std::make_shared<Odd>(nullptr, elseOffset, nullptr, thenOffset);
+ } else if (ddVariableIndices[currentLevel] < static_cast<uint_fast64_t>(dd->index)) {
+ // If we skipped the level in the DD, we compute the ODD just for the else-successor and use the same
+ // node for the then-successor as well.
+ std::shared_ptr<Odd> elseNode = createOddRec(dd, manager, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels);
+ std::shared_ptr<Odd> thenNode = elseNode;
+ return std::make_shared<Odd>(elseNode, elseNode->getElseOffset() + elseNode->getThenOffset(), thenNode, thenNode->getElseOffset() + thenNode->getThenOffset());
+ } else {
+ // Otherwise, we compute the ODDs for both the then- and else successors.
+ bool elseComplemented = Cudd_IsComplement(Cudd_E(dd));
+ bool thenComplemented = Cudd_IsComplement(Cudd_T(dd));
+ std::shared_ptr<Odd> elseNode = createOddRec(Cudd_E(dd), manager, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels);
+ std::shared_ptr<Odd> thenNode = createOddRec(Cudd_T(dd), manager, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels);
+ uint_fast64_t totalElseOffset = elseNode->getElseOffset() + elseNode->getThenOffset();
+ uint_fast64_t totalThenOffset = thenNode->getElseOffset() + thenNode->getThenOffset();
+ return std::make_shared<Odd>(elseNode, elseComplemented ? (1ull << (maxLevel - currentLevel - 1)) - totalElseOffset : totalElseOffset, thenNode, thenComplemented ? (1ull << (maxLevel - currentLevel - 1)) - totalThenOffset : totalThenOffset);
+ }
+ }
+ }
+
+ template<typename ValueType>
+ void InternalAdd<DdType::CUDD, ValueType>::composeWithExplicitVector(storm::dd::Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<ValueType>& targetVector, std::function<ValueType (ValueType const&, ValueType const&)> const& function) const {
composeWithExplicitVectorRec(this->getCuddDdNode(), nullptr, 0, ddVariableIndices.size(), 0, odd, ddVariableIndices, targetVector, function);
}
template<typename ValueType>
- void InternalAdd<DdType::CUDD, ValueType>::composeWithExplicitVector(storm::dd::Odd<DdType::CUDD> const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<uint_fast64_t> const& offsets, std::vector<ValueType>& targetVector, std::function<ValueType (ValueType const&, ValueType const&)> const& function) const {
+ void InternalAdd<DdType::CUDD, ValueType>::composeWithExplicitVector(storm::dd::Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<uint_fast64_t> const& offsets, std::vector<ValueType>& targetVector, std::function<ValueType (ValueType const&, ValueType const&)> const& function) const {
composeWithExplicitVectorRec(this->getCuddDdNode(), &offsets, 0, ddVariableIndices.size(), 0, odd, ddVariableIndices, targetVector, function);
}
template<typename ValueType>
- void InternalAdd<DdType::CUDD, ValueType>::composeWithExplicitVectorRec(DdNode const* dd, std::vector<uint_fast64_t> const* offsets, 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 {
+ void InternalAdd<DdType::CUDD, ValueType>::composeWithExplicitVectorRec(DdNode const* dd, std::vector<uint_fast64_t> const* offsets, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd 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(ddManager->getCuddManager().getManager())) {
return;
@@ -441,12 +493,12 @@ namespace storm {
}
template<typename ValueType>
- void InternalAdd<DdType::CUDD, ValueType>::toMatrixComponents(std::vector<uint_fast64_t> const& rowGroupIndices, std::vector<uint_fast64_t>& rowIndications, std::vector<storm::storage::MatrixEntry<uint_fast64_t, ValueType>>& columnsAndValues, Odd<DdType::CUDD> const& rowOdd, Odd<DdType::CUDD> const& columnOdd, std::vector<uint_fast64_t> const& ddRowVariableIndices, std::vector<uint_fast64_t> const& ddColumnVariableIndices, bool writeValues) const {
+ void InternalAdd<DdType::CUDD, ValueType>::toMatrixComponents(std::vector<uint_fast64_t> const& rowGroupIndices, std::vector<uint_fast64_t>& rowIndications, std::vector<storm::storage::MatrixEntry<uint_fast64_t, ValueType>>& columnsAndValues, Odd const& rowOdd, Odd const& columnOdd, std::vector<uint_fast64_t> const& ddRowVariableIndices, std::vector<uint_fast64_t> const& ddColumnVariableIndices, bool writeValues) const {
return toMatrixComponentsRec(this->getCuddDdNode(), rowGroupIndices, rowIndications, columnsAndValues, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, writeValues);
}
template<typename ValueType>
- void InternalAdd<DdType::CUDD, ValueType>::toMatrixComponentsRec(DdNode const* dd, std::vector<uint_fast64_t> const& rowGroupOffsets, std::vector<uint_fast64_t>& rowIndications, std::vector<storm::storage::MatrixEntry<uint_fast64_t, ValueType>>& columnsAndValues, 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 {
+ void InternalAdd<DdType::CUDD, ValueType>::toMatrixComponentsRec(DdNode const* dd, std::vector<uint_fast64_t> const& rowGroupOffsets, std::vector<uint_fast64_t>& rowIndications, std::vector<storm::storage::MatrixEntry<uint_fast64_t, ValueType>>& columnsAndValues, Odd const& rowOdd, Odd 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(ddManager->getCuddManager().getManager())) {
return;
@@ -498,233 +550,14 @@ namespace storm {
}
}
-
-// template<typename ValueType>
-// storm::storage::SparseMatrix<ValueType> InternalAdd<DdType::CUDD, ValueType>::toMatrix(uint_fast64_t numberOfDdVariables, 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(numberOfDdVariables));
-//
-// // 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>
-// 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, uint_fast64_t> stateToNumberOfChoices = this->notZero().existsAbstract(columnVariableCube).template toAdd<uint_fast64_t>().sumAbstract(groupVariableCube);
-// std::vector<ValueType> rowGroupIndices = stateToNumberOfChoices.toVector(rowOdd);
-// 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;
-//
-// // 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&, uint_fast64_t 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) const {
-// // 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* 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) {
+ 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 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) {
+ 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 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
diff --git a/src/storage/dd/cudd/InternalCuddAdd.h b/src/storage/dd/cudd/InternalCuddAdd.h
index 2643912d0..fab7cbef6 100644
--- a/src/storage/dd/cudd/InternalCuddAdd.h
+++ b/src/storage/dd/cudd/InternalCuddAdd.h
@@ -2,9 +2,11 @@
#define STORM_STORAGE_DD_CUDD_INTERNALCUDDADD_H_
#include <set>
+#include <unordered_map>
#include "src/storage/dd/DdType.h"
#include "src/storage/dd/InternalAdd.h"
+#include "src/storage/dd/Odd.h"
#include "src/storage/expressions/Variable.h"
@@ -25,24 +27,19 @@ namespace storm {
namespace dd {
template<DdType LibraryType>
class DdManager;
-
+
template<DdType LibraryType>
class InternalDdManager;
template<DdType LibraryType>
class InternalBdd;
-
+
template<DdType LibraryType, typename ValueType>
class AddIterator;
- template<DdType LibraryType>
- class Odd;
-
template<typename ValueType>
class InternalAdd<DdType::CUDD, ValueType> {
public:
- friend class Odd<DdType::CUDD>;
-
/*!
* Creates an ADD that encapsulates the given CUDD ADD.
*
@@ -500,19 +497,26 @@ namespace storm {
* if a meta variable does not at all influence the the function value.
* @return An iterator that points past the end of the container.
*/
- AddIterator<DdType::CUDD, ValueType> end(std::shared_ptr<DdManager<DdType::CUDD> const> fullDdManager, bool enumerateDontCareMetaVariables = true) const;
+ AddIterator<DdType::CUDD, ValueType> end(std::shared_ptr<DdManager<DdType::CUDD> const> fullDdManager, bool enumerateDontCareMetaVariables = true) const;
- void composeWithExplicitVector(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;
+ void composeWithExplicitVector(Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<ValueType>& targetVector, std::function<ValueType (ValueType const&, ValueType const&)> const& function) const;
- void composeWithExplicitVector(Odd<DdType::CUDD> const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<uint_fast64_t> const& offsets, std::vector<ValueType>& targetVector, std::function<ValueType (ValueType const&, ValueType const&)> const& function) const;
+ void composeWithExplicitVector(Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<uint_fast64_t> const& offsets, std::vector<ValueType>& targetVector, std::function<ValueType (ValueType const&, ValueType const&)> const& function) const;
std::vector<InternalAdd<DdType::CUDD, ValueType>> splitIntoGroups(std::vector<uint_fast64_t> const& ddGroupVariableIndices) const;
- void toMatrixComponents(std::vector<uint_fast64_t> const& rowGroupIndices, std::vector<uint_fast64_t>& rowIndications, std::vector<storm::storage::MatrixEntry<uint_fast64_t, ValueType>>& columnsAndValues, Odd<DdType::CUDD> const& rowOdd, Odd<DdType::CUDD> const& columnOdd, std::vector<uint_fast64_t> const& ddRowVariableIndices, std::vector<uint_fast64_t> const& ddColumnVariableIndices, bool writeValues) const;
+ void toMatrixComponents(std::vector<uint_fast64_t> const& rowGroupIndices, std::vector<uint_fast64_t>& rowIndications, std::vector<storm::storage::MatrixEntry<uint_fast64_t, ValueType>>& columnsAndValues, Odd const& rowOdd, Odd const& columnOdd, std::vector<uint_fast64_t> const& ddRowVariableIndices, std::vector<uint_fast64_t> const& ddColumnVariableIndices, bool writeValues) const;
std::vector<std::pair<InternalAdd<DdType::CUDD, ValueType>, InternalAdd<DdType::CUDD, ValueType>>> splitIntoGroups(InternalAdd<DdType::CUDD, ValueType> vector, std::vector<uint_fast64_t> const& ddGroupVariableIndices) const;
- static 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);
+ static InternalAdd<DdType::CUDD, ValueType> fromVector(InternalDdManager<DdType::CUDD> const* ddManager, std::vector<ValueType> const& values, storm::dd::Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices);
+
+ /*!
+ * Creates an ODD based on the current ADD.
+ *
+ * @return The corresponding ODD.
+ */
+ Odd createOdd(std::vector<uint_fast64_t> const& ddVariableIndices) const;
private:
/*!
@@ -541,7 +545,7 @@ namespace storm {
* @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.
*/
- void composeWithExplicitVectorRec(DdNode const* dd, std::vector<uint_fast64_t> const* offsets, 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;
+ void composeWithExplicitVectorRec(DdNode const* dd, std::vector<uint_fast64_t> const* offsets, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<ValueType>& targetVector, std::function<ValueType (ValueType const&, ValueType const&)> const& function) const;
/*!
* Splits the given matrix DD into the groups using the given group variables.
@@ -582,7 +586,7 @@ namespace storm {
* 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 toMatrixComponentsRec(DdNode const* dd, std::vector<uint_fast64_t> const& rowGroupOffsets, std::vector<uint_fast64_t>& rowIndications, std::vector<storm::storage::MatrixEntry<uint_fast64_t, ValueType>>& columnsAndValues, 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 writeValues) const;
+ void toMatrixComponentsRec(DdNode const* dd, std::vector<uint_fast64_t> const& rowGroupOffsets, std::vector<uint_fast64_t>& rowIndications, std::vector<storm::storage::MatrixEntry<uint_fast64_t, ValueType>>& columnsAndValues, Odd const& rowOdd, Odd 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 writeValues) const;
/*!
* Builds an ADD representing the given vector.
@@ -596,7 +600,21 @@ namespace storm {
* @param ddVariableIndices The (sorted) list of DD variable indices to use.
* @return The resulting (CUDD) ADD node.
*/
- 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);
+ static DdNode* fromVectorRec(::DdManager* manager, uint_fast64_t& currentOffset, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector<ValueType> const& values, Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices);
+
+ /*!
+ * Recursively builds the ODD from an ADD (that has no complement edges).
+ *
+ * @param dd The DD for which to build the ODD.
+ * @param manager The manager responsible for the DD.
+ * @param currentLevel The currently considered level in the DD.
+ * @param maxLevel The number of levels that need to be considered.
+ * @param ddVariableIndices The (sorted) indices of all DD variables that need to be considered.
+ * @param uniqueTableForLevels A vector of unique tables, one for each level to be considered, that keeps
+ * ODD nodes for the same DD and level unique.
+ * @return A pointer to the constructed ODD for the given arguments.
+ */
+ static std::shared_ptr<Odd> createOddRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<std::unordered_map<DdNode*, std::shared_ptr<Odd>>>& uniqueTableForLevels);
InternalDdManager<DdType::CUDD> const* ddManager;
diff --git a/src/storage/dd/cudd/InternalCuddBdd.cpp b/src/storage/dd/cudd/InternalCuddBdd.cpp
index 72d12d6ae..3bfb98c5c 100644
--- a/src/storage/dd/cudd/InternalCuddBdd.cpp
+++ b/src/storage/dd/cudd/InternalCuddBdd.cpp
@@ -1,7 +1,9 @@
#include "src/storage/dd/cudd/InternalCuddBdd.h"
+#include <boost/functional/hash.hpp>
+
#include "src/storage/dd/cudd/InternalCuddDdManager.h"
-#include "src/storage/dd/cudd/CuddOdd.h"
+#include "src/storage/dd/Odd.h"
#include "src/storage/BitVector.h"
@@ -12,7 +14,7 @@ namespace storm {
}
template<typename ValueType>
- InternalBdd<DdType::CUDD> InternalBdd<DdType::CUDD>::fromVector(InternalDdManager<DdType::CUDD> const* ddManager, std::vector<ValueType> const& values, Odd<DdType::CUDD> const& odd, std::vector<uint_fast64_t> const& sortedDdVariableIndices, std::function<bool (ValueType const&)> const& filter) {
+ InternalBdd<DdType::CUDD> InternalBdd<DdType::CUDD>::fromVector(InternalDdManager<DdType::CUDD> const* ddManager, std::vector<ValueType> const& values, Odd const& odd, std::vector<uint_fast64_t> const& sortedDdVariableIndices, std::function<bool (ValueType const&)> const& filter) {
uint_fast64_t offset = 0;
return InternalBdd<DdType::CUDD>(ddManager, BDD(ddManager->getCuddManager(), fromVectorRec(ddManager->getCuddManager().getManager(), offset, 0, sortedDdVariableIndices.size(), values, odd, sortedDdVariableIndices, filter)));
}
@@ -175,7 +177,7 @@ namespace storm {
}
template<typename ValueType>
- DdNode* InternalBdd<DdType::CUDD>::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, std::function<bool (ValueType const&)> const& filter) {
+ DdNode* InternalBdd<DdType::CUDD>::fromVectorRec(::DdManager* manager, uint_fast64_t& currentOffset, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector<ValueType> const& values, Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::function<bool (ValueType const&)> const& filter) {
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
@@ -231,13 +233,13 @@ namespace storm {
}
}
- storm::storage::BitVector InternalBdd<DdType::CUDD>::toVector(storm::dd::Odd<DdType::CUDD> const& rowOdd, std::vector<uint_fast64_t> const& ddVariableIndices) const {
+ storm::storage::BitVector InternalBdd<DdType::CUDD>::toVector(storm::dd::Odd const& rowOdd, std::vector<uint_fast64_t> const& ddVariableIndices) const {
storm::storage::BitVector result(rowOdd.getTotalOffset());
this->toVectorRec(this->getCuddDdNode(), ddManager->getCuddManager(), result, rowOdd, Cudd_IsComplement(this->getCuddDdNode()), 0, ddVariableIndices.size(), 0, ddVariableIndices);
return result;
}
- void InternalBdd<DdType::CUDD>::toVectorRec(DdNode const* dd, Cudd const& manager, storm::storage::BitVector& result, Odd<DdType::CUDD> const& rowOdd, bool complement, uint_fast64_t currentRowLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, std::vector<uint_fast64_t> const& ddRowVariableIndices) const {
+ void InternalBdd<DdType::CUDD>::toVectorRec(DdNode const* dd, Cudd const& manager, storm::storage::BitVector& result, Odd const& rowOdd, bool complement, uint_fast64_t currentRowLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, std::vector<uint_fast64_t> const& ddRowVariableIndices) const {
// If there are no more values to select, we can directly return.
if (dd == Cudd_ReadLogicZero(manager.getManager()) && !complement) {
return;
@@ -265,10 +267,127 @@ namespace storm {
}
}
- template InternalBdd<DdType::CUDD> InternalBdd<DdType::CUDD>::fromVector(InternalDdManager<DdType::CUDD> const* ddManager, std::vector<double> const& values, Odd<DdType::CUDD> const& odd, std::vector<uint_fast64_t> const& sortedDdVariableIndices, std::function<bool (double const&)> const& filter);
- template InternalBdd<DdType::CUDD> InternalBdd<DdType::CUDD>::fromVector(InternalDdManager<DdType::CUDD> const* ddManager, std::vector<uint_fast64_t> const& values, Odd<DdType::CUDD> const& odd, std::vector<uint_fast64_t> const& sortedDdVariableIndices, std::function<bool (uint_fast64_t const&)> const& filter);
+ Odd InternalBdd<DdType::CUDD>::createOdd(std::vector<uint_fast64_t> const& ddVariableIndices) const {
+ // Prepare a unique table for each level that keeps the constructed ODD nodes unique.
+ std::vector<std::unordered_map<std::pair<DdNode*, bool>, std::shared_ptr<Odd>, HashFunctor>> uniqueTableForLevels(ddVariableIndices.size() + 1);
+
+ // Now construct the ODD structure from the BDD.
+ std::shared_ptr<Odd> rootOdd = createOddRec(Cudd_Regular(this->getCuddDdNode()), ddManager->getCuddManager(), 0, Cudd_IsComplement(this->getCuddDdNode()), ddVariableIndices.size(), ddVariableIndices, uniqueTableForLevels);
+
+ // Return a copy of the root node to remove the shared_ptr encapsulation.
+ return Odd(*rootOdd);
+ }
+
+ std::size_t InternalBdd<DdType::CUDD>::HashFunctor::operator()(std::pair<DdNode*, bool> const& key) const {
+ std::size_t result = 0;
+ boost::hash_combine(result, key.first);
+ boost::hash_combine(result, key.second);
+ return result;
+ }
+
+ std::shared_ptr<Odd> InternalBdd<DdType::CUDD>::createOddRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<std::unordered_map<std::pair<DdNode*, bool>, std::shared_ptr<Odd>, HashFunctor>>& uniqueTableForLevels) {
+ // Check whether the ODD for this node has already been computed (for this level) and if so, return this instead.
+ auto const& iterator = uniqueTableForLevels[currentLevel].find(std::make_pair(dd, complement));
+ if (iterator != uniqueTableForLevels[currentLevel].end()) {
+ return iterator->second;
+ } else {
+ // Otherwise, we need to recursively compute the ODD.
+
+ // If we are already past the maximal level that is to be considered, we can simply create an Odd without
+ // successors
+ if (currentLevel == maxLevel) {
+ uint_fast64_t elseOffset = 0;
+ uint_fast64_t thenOffset = 0;
+
+ // If the DD is not the zero leaf, then the then-offset is 1.
+ if (dd != Cudd_ReadZero(manager.getManager())) {
+ thenOffset = 1;
+ }
+
+ // If we need to complement the 'terminal' node, we need to negate its offset.
+ if (complement) {
+ thenOffset = 1 - thenOffset;
+ }
+
+ return std::make_shared<Odd>(nullptr, elseOffset, nullptr, thenOffset);
+ } else if (ddVariableIndices[currentLevel] < static_cast<uint_fast64_t>(dd->index)) {
+ // If we skipped the level in the DD, we compute the ODD just for the else-successor and use the same
+ // node for the then-successor as well.
+ std::shared_ptr<Odd> elseNode = createOddRec(dd, manager, currentLevel + 1, complement, maxLevel, ddVariableIndices, uniqueTableForLevels);
+ std::shared_ptr<Odd> thenNode = elseNode;
+ uint_fast64_t totalOffset = elseNode->getElseOffset() + elseNode->getThenOffset();
+ return std::make_shared<Odd>(elseNode, totalOffset, thenNode, totalOffset);
+ } else {
+ // Otherwise, we compute the ODDs for both the then- and else successors.
+ DdNode* thenDdNode = Cudd_T(dd);
+ DdNode* elseDdNode = Cudd_E(dd);
+
+ // Determine whether we have to evaluate the successors as if they were complemented.
+ bool elseComplemented = Cudd_IsComplement(elseDdNode) ^ complement;
+ bool thenComplemented = Cudd_IsComplement(thenDdNode) ^ complement;
+
+ std::shared_ptr<Odd> elseNode = createOddRec(Cudd_Regular(elseDdNode), manager, currentLevel + 1, elseComplemented, maxLevel, ddVariableIndices, uniqueTableForLevels);
+ std::shared_ptr<Odd> thenNode = createOddRec(Cudd_Regular(thenDdNode), manager, currentLevel + 1, thenComplemented, maxLevel, ddVariableIndices, uniqueTableForLevels);
+
+ return std::make_shared<Odd>(elseNode, elseNode->getElseOffset() + elseNode->getThenOffset(), thenNode, thenNode->getElseOffset() + thenNode->getThenOffset());
+ }
+ }
+ }
+
+ template<typename ValueType>
+ void InternalBdd<DdType::CUDD>::filterExplicitVector(Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<ValueType> const& sourceValues, std::vector<ValueType>& targetValues) const {
+ uint_fast64_t currentIndex = 0;
+ filterExplicitVectorRec(this->getCuddDdNode(), ddManager->getCuddManager(), 0, Cudd_IsComplement(this->getCuddDdNode()), ddVariableIndices.size(), ddVariableIndices, 0, odd, targetValues, currentIndex, sourceValues);
+ }
+
+ template<typename ValueType>
+ void InternalBdd<DdType::CUDD>::filterExplicitVectorRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector<uint_fast64_t> const& ddVariableIndices, uint_fast64_t currentOffset, storm::dd::Odd const& odd, std::vector<ValueType>& result, uint_fast64_t& currentIndex, std::vector<ValueType> const& values) {
+ // If there are no more values to select, we can directly return.
+ if (dd == Cudd_ReadLogicZero(manager.getManager()) && !complement) {
+ return;
+ } else if (dd == Cudd_ReadOne(manager.getManager()) && complement) {
+ return;
+ }
+
+ if (currentLevel == maxLevel) {
+ // If the DD is not the zero leaf, then the then-offset is 1.
+ bool selected = false;
+ if (dd != Cudd_ReadLogicZero(manager.getManager())) {
+ selected = !complement;
+ }
+
+ if (selected) {
+ result[currentIndex++] = values[currentOffset];
+ }
+ } 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.
+ filterExplicitVectorRec(dd, manager, currentLevel + 1, complement, maxLevel, ddVariableIndices, currentOffset, odd.getElseSuccessor(), result, currentIndex, values);
+ filterExplicitVectorRec(dd, manager, currentLevel + 1, complement, maxLevel, ddVariableIndices, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), result, currentIndex, values);
+ } else {
+ // Otherwise, we compute the ODDs for both the then- and else successors.
+ DdNode* thenDdNode = Cudd_T(dd);
+ DdNode* elseDdNode = Cudd_E(dd);
+
+ // Determine whether we have to evaluate the successors as if they were complemented.
+ bool elseComplemented = Cudd_IsComplement(elseDdNode) ^ complement;
+ bool thenComplemented = Cudd_IsComplement(thenDdNode) ^ complement;
+
+ filterExplicitVectorRec(Cudd_Regular(elseDdNode), manager, currentLevel + 1, elseComplemented, maxLevel, ddVariableIndices, currentOffset, odd.getElseSuccessor(), result, currentIndex, values);
+ filterExplicitVectorRec(Cudd_Regular(thenDdNode), manager, currentLevel + 1, thenComplemented, maxLevel, ddVariableIndices, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), result, currentIndex, values);
+ }
+ }
+
+ template InternalBdd<DdType::CUDD> InternalBdd<DdType::CUDD>::fromVector(InternalDdManager<DdType::CUDD> const* ddManager, std::vector<double> const& values, Odd const& odd, std::vector<uint_fast64_t> const& sortedDdVariableIndices, std::function<bool (double const&)> const& filter);
+ template InternalBdd<DdType::CUDD> InternalBdd<DdType::CUDD>::fromVector(InternalDdManager<DdType::CUDD> const* ddManager, std::vector<uint_fast64_t> const& values, Odd const& odd, std::vector<uint_fast64_t> const& sortedDdVariableIndices, std::function<bool (uint_fast64_t const&)> const& filter);
template InternalAdd<DdType::CUDD, double> InternalBdd<DdType::CUDD>::toAdd() const;
template InternalAdd<DdType::CUDD, uint_fast64_t> InternalBdd<DdType::CUDD>::toAdd() const;
+
+ template void InternalBdd<DdType::CUDD>::filterExplicitVectorRec<double>(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector<uint_fast64_t> const& ddVariableIndices, uint_fast64_t currentOffset, storm::dd::Odd const& odd, std::vector<double>& result, uint_fast64_t& currentIndex, std::vector<double> const& values);
+ template void InternalBdd<DdType::CUDD>::filterExplicitVectorRec<uint_fast64_t>(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector<uint_fast64_t> const& ddVariableIndices, uint_fast64_t currentOffset, storm::dd::Odd const& odd, std::vector<uint_fast64_t>& result, uint_fast64_t& currentIndex, std::vector<uint_fast64_t> const& values);
+
+ template void InternalBdd<DdType::CUDD>::filterExplicitVector(Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<double> const& sourceValues, std::vector<double>& targetValues) const;
+ template void InternalBdd<DdType::CUDD>::filterExplicitVector(Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<uint_fast64_t> const& sourceValues, std::vector<uint_fast64_t>& targetValues) const;
}
}
\ No newline at end of file
diff --git a/src/storage/dd/cudd/InternalCuddBdd.h b/src/storage/dd/cudd/InternalCuddBdd.h
index daf77db9b..7f74f0b79 100644
--- a/src/storage/dd/cudd/InternalCuddBdd.h
+++ b/src/storage/dd/cudd/InternalCuddBdd.h
@@ -2,6 +2,7 @@
#define STORM_STORAGE_DD_CUDD_INTERNALCUDDBDD_H_
#include <set>
+#include <unordered_map>
#include "src/storage/dd/DdType.h"
#include "src/storage/dd/InternalBdd.h"
@@ -30,14 +31,12 @@ namespace storm {
template<DdType LibraryType, typename ValueType>
class InternalAdd;
- template<storm::dd::DdType LibraryType>
class Odd;
template<>
class InternalBdd<DdType::CUDD> {
public:
friend class InternalAdd<DdType::CUDD, double>;
- friend class Odd<DdType::CUDD>;
/*!
* Creates a DD that encapsulates the given CUDD ADD.
@@ -66,7 +65,7 @@ namespace storm {
* @return The resulting BDD.
*/
template<typename ValueType>
- static InternalBdd<storm::dd::DdType::CUDD> fromVector(InternalDdManager<DdType::CUDD> const* ddManager, std::vector<ValueType> const& values, Odd<DdType::CUDD> const& odd, std::vector<uint_fast64_t> const& sortedDdVariableIndices, std::function<bool (ValueType const&)> const& filter);
+ static InternalBdd<storm::dd::DdType::CUDD> fromVector(InternalDdManager<DdType::CUDD> const* ddManager, std::vector<ValueType> const& values, Odd const& odd, std::vector<uint_fast64_t> const& sortedDdVariableIndices, std::function<bool (ValueType const&)> const& filter);
/*!
* Retrieves whether the two BDDs represent the same function.
@@ -289,7 +288,17 @@ namespace storm {
* @param rowOdd The ODD used for determining the correct row.
* @return The bit vector that is represented by this BDD.
*/
- storm::storage::BitVector toVector(storm::dd::Odd<DdType::CUDD> const& rowOdd, std::vector<uint_fast64_t> const& ddVariableIndices) const;
+ storm::storage::BitVector toVector(storm::dd::Odd const& rowOdd, std::vector<uint_fast64_t> const& ddVariableIndices) const;
+
+ /*!
+ * Creates an ODD based on the current BDD.
+ *
+ * @return The corresponding ODD.
+ */
+ Odd createOdd(std::vector<uint_fast64_t> const& ddVariableIndices) const;
+
+ template<typename ValueType>
+ void filterExplicitVector(Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<ValueType> const& sourceValues, std::vector<ValueType>& targetValues) const;
private:
/*!
@@ -305,7 +314,7 @@ namespace storm {
* @return The resulting (CUDD) BDD 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, std::function<bool (ValueType const&)> const& filter);
+ static DdNode* fromVectorRec(::DdManager* manager, uint_fast64_t& currentOffset, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector<ValueType> const& values, Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::function<bool (ValueType const&)> const& filter);
/*!
* Helper function to convert the DD into a bit vector.
@@ -320,7 +329,45 @@ namespace storm {
* @param currentRowOffset The current row offset.
* @param ddRowVariableIndices The (sorted) indices of all DD row variables that need to be considered.
*/
- void toVectorRec(DdNode const* dd, Cudd const& manager, storm::storage::BitVector& result, Odd<DdType::CUDD> const& rowOdd, bool complement, uint_fast64_t currentRowLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, std::vector<uint_fast64_t> const& ddRowVariableIndices) const;
+ void toVectorRec(DdNode const* dd, Cudd const& manager, storm::storage::BitVector& result, Odd const& rowOdd, bool complement, uint_fast64_t currentRowLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, std::vector<uint_fast64_t> const& ddRowVariableIndices) const;
+
+ // Declare a hash functor that is used for the unique tables in the construction process of ODDs.
+ class HashFunctor {
+ public:
+ std::size_t operator()(std::pair<DdNode*, bool> const& key) const;
+ };
+
+ /*!
+ * Recursively builds the ODD from a BDD (that potentially has complement edges).
+ *
+ * @param dd The DD for which to build the ODD.
+ * @param manager The manager responsible for the DD.
+ * @param currentLevel The currently considered level in the DD.
+ * @param complement A flag indicating whether or not the given node is to be considered as complemented.
+ * @param maxLevel The number of levels that need to be considered.
+ * @param ddVariableIndices The (sorted) indices of all DD variables that need to be considered.
+ * @param uniqueTableForLevels A vector of unique tables, one for each level to be considered, that keeps
+ * ODD nodes for the same DD and level unique.
+ * @return A pointer to the constructed ODD for the given arguments.
+ */
+ static std::shared_ptr<Odd> createOddRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<std::unordered_map<std::pair<DdNode*, bool>, std::shared_ptr<Odd>, HashFunctor>>& uniqueTableForLevels);
+
+ /*!
+ * Adds the selected values the target vector.
+ *
+ * @param dd The current node of the DD representing the selected values.
+ * @param manager The manager responsible for the DD.
+ * @param currentLevel The currently considered level in the DD.
+ * @param maxLevel The number of levels that need to be considered.
+ * @param ddVariableIndices The sorted list of variable indices to use.
+ * @param currentOffset The offset along the path taken in the DD representing the selected values.
+ * @param odd The current ODD node.
+ * @param result The target vector to which to write the values.
+ * @param currentIndex The index at which the next element is to be written.
+ * @param values The value vector from which to select the values.
+ */
+ template<typename ValueType>
+ static void filterExplicitVectorRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector<uint_fast64_t> const& ddVariableIndices, uint_fast64_t currentOffset, storm::dd::Odd const& odd, std::vector<ValueType>& result, uint_fast64_t& currentIndex, std::vector<ValueType> const& values);
/*!
* Retrieves the CUDD BDD object associated with this DD.
diff --git a/src/storage/dd/cudd/InternalCuddDdManager.h b/src/storage/dd/cudd/InternalCuddDdManager.h
index 7e3b2e655..e56bad54d 100644
--- a/src/storage/dd/cudd/InternalCuddDdManager.h
+++ b/src/storage/dd/cudd/InternalCuddDdManager.h
@@ -17,14 +17,10 @@ namespace storm {
template<DdType LibraryType>
class InternalBdd;
- template<DdType LibraryType>
- class Odd;
-
template<>
class InternalDdManager<DdType::CUDD> {
public:
friend class InternalBdd<DdType::CUDD>;
- friend class Odd<DdType::CUDD>;
template<DdType LibraryType, typename ValueType>
friend class InternalAdd;
diff --git a/test/functional/storage/CuddDdTest.cpp b/test/functional/storage/CuddDdTest.cpp
index d4b578664..03ef4f304 100644
--- a/test/functional/storage/CuddDdTest.cpp
+++ b/test/functional/storage/CuddDdTest.cpp
@@ -3,7 +3,7 @@
#include "src/exceptions/InvalidArgumentException.h"
#include "src/storage/dd/DdManager.h"
#include "src/storage/dd/Add.h"
-#include "src/storage/dd/cudd/CuddOdd.h"
+#include "src/storage/dd/Odd.h"
#include "src/storage/dd/DdMetaVariable.h"
#include "src/settings/SettingsManager.h"
@@ -323,8 +323,8 @@ TEST(CuddDd, AddOddTest) {
std::pair<storm::expressions::Variable, storm::expressions::Variable> x = manager->addMetaVariable("x", 1, 9);
storm::dd::Add<storm::dd::DdType::CUDD, double> dd = manager->template getIdentity<double>(x.first);
- storm::dd::Odd<storm::dd::DdType::CUDD> odd;
- ASSERT_NO_THROW(odd = storm::dd::Odd<storm::dd::DdType::CUDD>(dd));
+ storm::dd::Odd odd;
+ ASSERT_NO_THROW(odd = dd.createOdd());
EXPECT_EQ(9ul, odd.getTotalOffset());
EXPECT_EQ(12ul, odd.getNodeCount());
@@ -340,10 +340,10 @@ TEST(CuddDd, AddOddTest) {
dd += manager->getEncoding(x.first, 1).template toAdd<double>() * manager->getRange(x.second).template toAdd<double>() + manager->getEncoding(x.second, 1).template toAdd<double>() * manager->getRange(x.first).template toAdd<double>();
// Create the ODDs.
- storm::dd::Odd<storm::dd::DdType::CUDD> rowOdd;
- ASSERT_NO_THROW(rowOdd = storm::dd::Odd<storm::dd::DdType::CUDD>(manager->getRange(x.first).template toAdd<double>()));
- storm::dd::Odd<storm::dd::DdType::CUDD> columnOdd;
- ASSERT_NO_THROW(columnOdd = storm::dd::Odd<storm::dd::DdType::CUDD>(manager->getRange(x.second).template toAdd<double>()));
+ storm::dd::Odd rowOdd;
+ ASSERT_NO_THROW(rowOdd = manager->getRange(x.first).template toAdd<double>().createOdd());
+ storm::dd::Odd columnOdd;
+ ASSERT_NO_THROW(columnOdd = manager->getRange(x.second).template toAdd<double>().createOdd());
// Try to translate the matrix.
storm::storage::SparseMatrix<double> matrix;
@@ -367,8 +367,8 @@ TEST(CuddDd, BddOddTest) {
std::pair<storm::expressions::Variable, storm::expressions::Variable> x = manager->addMetaVariable("x", 1, 9);
storm::dd::Add<storm::dd::DdType::CUDD, double> dd = manager->template getIdentity<double>(x.first);
- storm::dd::Odd<storm::dd::DdType::CUDD> odd;
- ASSERT_NO_THROW(odd = storm::dd::Odd<storm::dd::DdType::CUDD>(dd));
+ storm::dd::Odd odd;
+ ASSERT_NO_THROW(odd = dd.createOdd());
EXPECT_EQ(9ul, odd.getTotalOffset());
EXPECT_EQ(12ul, odd.getNodeCount());
@@ -386,10 +386,10 @@ TEST(CuddDd, BddOddTest) {
dd += manager->getEncoding(x.first, 1).template toAdd<double>() * manager->getRange(x.second).template toAdd<double>() + manager->getEncoding(x.second, 1).template toAdd<double>() * manager->getRange(x.first).template toAdd<double>();
// Create the ODDs.
- storm::dd::Odd<storm::dd::DdType::CUDD> rowOdd;
- ASSERT_NO_THROW(rowOdd = storm::dd::Odd<storm::dd::DdType::CUDD>(manager->getRange(x.first)));
- storm::dd::Odd<storm::dd::DdType::CUDD> columnOdd;
- ASSERT_NO_THROW(columnOdd = storm::dd::Odd<storm::dd::DdType::CUDD>(manager->getRange(x.second)));
+ storm::dd::Odd rowOdd;
+ ASSERT_NO_THROW(rowOdd = manager->getRange(x.first).createOdd());
+ storm::dd::Odd columnOdd;
+ ASSERT_NO_THROW(columnOdd = manager->getRange(x.second).createOdd());
// Try to translate the matrix.
storm::storage::SparseMatrix<double> matrix;