diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c b/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c index 92bd3cb07..12dbbcc46 100644 --- a/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c +++ b/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c @@ -471,6 +471,23 @@ TASK_IMPL_1(MTBDD, mtbdd_bool_to_double, MTBDD, dd) return mtbdd_uapply(dd, TASK(mtbdd_op_bool_to_double), 0); } +TASK_IMPL_2(MTBDD, mtbdd_op_bool_to_uint64, MTBDD, a, size_t, v) +{ + /* We only expect "double" terminals, or false */ + if (a == mtbdd_false) return mtbdd_uint64(0); + if (a == mtbdd_true) return mtbdd_uint64(1); + + // Ugly hack to get rid of the error "unused variable v" (because there is no version of uapply without a parameter). + (void)v; + + return mtbdd_invalid; +} + +TASK_IMPL_1(MTBDD, mtbdd_bool_to_uint64, MTBDD, dd) +{ + return mtbdd_uapply(dd, TASK(mtbdd_op_bool_to_uint64), 0); +} + /** * Calculate the number of satisfying variable assignments according to . */ diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h b/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h index 4f5250b56..ef8b1c17c 100644 --- a/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h +++ b/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h @@ -94,6 +94,13 @@ TASK_DECL_2(MTBDD, mtbdd_op_bool_to_double, MTBDD, size_t) TASK_DECL_1(MTBDD, mtbdd_bool_to_double, MTBDD) #define mtbdd_bool_to_double(dd) CALL(mtbdd_bool_to_double, dd) +/** + * Monad that converts Boolean to a uint MTBDD, translate terminals true to 1 and to 0 otherwise; + */ +TASK_DECL_2(MTBDD, mtbdd_op_bool_to_uint64, MTBDD, size_t) +TASK_DECL_1(MTBDD, mtbdd_bool_to_uint64, MTBDD) +#define mtbdd_bool_to_uint64(dd) CALL(mtbdd_bool_to_uint64, dd) + /** * Count the number of assignments (minterms) leading to a non-zero */ diff --git a/resources/3rdparty/sylvan/src/sylvan_obj_bdd_storm.hpp b/resources/3rdparty/sylvan/src/sylvan_obj_bdd_storm.hpp index c5020144b..3c453ae9f 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj_bdd_storm.hpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj_bdd_storm.hpp @@ -1 +1,2 @@ Mtbdd toDoubleMtbdd() const; + Mtbdd toUint64Mtbdd() const; diff --git a/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp b/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp index d2687ac8e..71ca7256e 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp @@ -4,6 +4,12 @@ Bdd::toDoubleMtbdd() const { return mtbdd_bool_to_double(bdd); } +Mtbdd +Bdd::toUint64Mtbdd() const { + LACE_ME; + return mtbdd_bool_to_uint64(bdd); +} + Mtbdd Mtbdd::Minus(const Mtbdd &other) const { diff --git a/src/storage/dd/Add.cpp b/src/storage/dd/Add.cpp index 4afc3fbc4..64d02c99f 100644 --- a/src/storage/dd/Add.cpp +++ b/src/storage/dd/Add.cpp @@ -338,7 +338,7 @@ namespace storm { Add value = *this * valueEncoding.template toAdd(); value = value.sumAbstract(this->getContainedMetaVariables()); - return value.getMax(); + return value.internalAdd.getValue(); } template diff --git a/src/storage/dd/cudd/InternalCuddAdd.cpp b/src/storage/dd/cudd/InternalCuddAdd.cpp index 6ba175ae4..1cbff380d 100644 --- a/src/storage/dd/cudd/InternalCuddAdd.cpp +++ b/src/storage/dd/cudd/InternalCuddAdd.cpp @@ -260,6 +260,11 @@ namespace storm { return static_cast(Cudd_V(constantMaxAdd.getNode())); } + template + ValueType InternalAdd::getValue() const { + return static_cast(Cudd_V(this->getCuddAdd().getNode())); + } + template bool InternalAdd::isOne() const { return this->getCuddAdd().IsOne(); diff --git a/src/storage/dd/cudd/InternalCuddAdd.h b/src/storage/dd/cudd/InternalCuddAdd.h index 8543ffda5..b93a6205b 100644 --- a/src/storage/dd/cudd/InternalCuddAdd.h +++ b/src/storage/dd/cudd/InternalCuddAdd.h @@ -414,6 +414,13 @@ namespace storm { */ ValueType getMax() const; + /*! + * Retrieves the value of this ADD that is required to be a leaf. + * + * @return The value of the leaf. + */ + ValueType getValue() const; + /*! * Retrieves whether this ADD represents the constant one function. * diff --git a/src/storage/dd/sylvan/InternalSylvanAdd.cpp b/src/storage/dd/sylvan/InternalSylvanAdd.cpp index 7afffec7d..2fa479044 100644 --- a/src/storage/dd/sylvan/InternalSylvanAdd.cpp +++ b/src/storage/dd/sylvan/InternalSylvanAdd.cpp @@ -254,6 +254,11 @@ namespace storm { return static_cast(this->sylvanMtbdd.getDoubleMax()); } + template + ValueType InternalAdd::getValue() const { + return getValue(this->sylvanMtbdd.GetMTBDD()); + } + template bool InternalAdd::isOne() const { return *this == ddManager->getAddOne(); @@ -348,16 +353,16 @@ namespace storm { template void InternalAdd::composeWithExplicitVector(storm::dd::Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector, std::function const& function) const { - composeWithExplicitVectorRec(this->getSylvanMtbdd().GetMTBDD(), nullptr, 0, ddVariableIndices.size(), 0, odd, ddVariableIndices, targetVector, function); + composeWithExplicitVectorRec(mtbdd_regular(this->getSylvanMtbdd().GetMTBDD()), mtbdd_isnegated(this->getSylvanMtbdd().GetMTBDD()), nullptr, 0, ddVariableIndices.size(), 0, odd, ddVariableIndices, targetVector, function); } template void InternalAdd::composeWithExplicitVector(storm::dd::Odd const& odd, std::vector const& ddVariableIndices, std::vector const& offsets, std::vector& targetVector, std::function const& function) const { - composeWithExplicitVectorRec(mtbdd_regular(this->getSylvanMtbdd().GetMTBDD()), &offsets, 0, ddVariableIndices.size(), 0, odd, ddVariableIndices, targetVector, function); + composeWithExplicitVectorRec(mtbdd_regular(this->getSylvanMtbdd().GetMTBDD()), mtbdd_isnegated(this->getSylvanMtbdd().GetMTBDD()), &offsets, 0, ddVariableIndices.size(), 0, odd, ddVariableIndices, targetVector, function); } template - void InternalAdd::composeWithExplicitVectorRec(MTBDD dd, std::vector const* offsets, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector, std::function const& function) const { + void InternalAdd::composeWithExplicitVectorRec(MTBDD dd, bool negated, std::vector const* offsets, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector, std::function const& function) const { // For the empty DD, we do not need to add any entries. if (mtbdd_isleaf(dd) && mtbdd_iszero(dd)) { return; @@ -370,12 +375,19 @@ namespace storm { } else if (mtbdd_isleaf(dd) || ddVariableIndices[currentLevel] < mtbdd_getvar(dd)) { // 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. - composeWithExplicitVectorRec(dd, offsets, currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, targetVector, function); - composeWithExplicitVectorRec(dd, offsets, currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, targetVector, function); + composeWithExplicitVectorRec(dd, negated, offsets, currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, targetVector, function); + composeWithExplicitVectorRec(dd, negated, offsets, currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, targetVector, function); } else { // Otherwise, we simply recursively call the function for both (different) cases. - composeWithExplicitVectorRec(mtbdd_regular(mtbdd_getlow(dd)), offsets, currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, targetVector, function); - composeWithExplicitVectorRec(mtbdd_regular(mtbdd_gethigh(dd)), offsets, currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, targetVector, function); + MTBDD thenNode = mtbdd_gethigh(dd); + MTBDD elseNode = mtbdd_getlow(dd); + + // Determine whether we have to evaluate the successors as if they were complemented. + bool elseComplemented = mtbdd_isnegated(elseNode) ^ negated; + bool thenComplemented = mtbdd_isnegated(thenNode) ^ negated; + + composeWithExplicitVectorRec(mtbdd_regular(elseNode), elseComplemented, offsets, currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, targetVector, function); + composeWithExplicitVectorRec(mtbdd_regular(thenNode), thenComplemented, offsets, currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, targetVector, function); } } @@ -594,14 +606,17 @@ namespace storm { template ValueType InternalAdd::getValue(MTBDD const& node) { - STORM_LOG_ASSERT(mtbdd_isleaf(node), "Expected leaf."); + STORM_LOG_ASSERT(mtbdd_isleaf(node), "Expected leaf, but got variable " << mtbdd_getvar(node) << "."); + + bool negated = mtbdd_isnegated(node); + MTBDD n = mtbdd_regular(node); if (std::is_same::value) { - STORM_LOG_ASSERT(mtbdd_gettype(node) == 1, "Expected a double value."); - return mtbdd_getuint64(node); + STORM_LOG_ASSERT(mtbdd_gettype(n) == 1, "Expected a double value."); + return negated ? -mtbdd_getdouble(n) : mtbdd_getdouble(n); } else if (std::is_same::value) { STORM_LOG_ASSERT(mtbdd_gettype(node) == 0, "Expected an unsigned value."); - return mtbdd_getdouble(node); + return negated ? -mtbdd_getuint64(node) : mtbdd_getuint64(node); } else { STORM_LOG_ASSERT(false, "Illegal or unknown type in MTBDD."); } diff --git a/src/storage/dd/sylvan/InternalSylvanAdd.h b/src/storage/dd/sylvan/InternalSylvanAdd.h index ea67289fb..c93793560 100644 --- a/src/storage/dd/sylvan/InternalSylvanAdd.h +++ b/src/storage/dd/sylvan/InternalSylvanAdd.h @@ -411,7 +411,14 @@ namespace storm { * @return The highest function value of any encoding. */ ValueType getMax() const; - + + /*! + * Retrieves the value of this ADD that is required to be a leaf. + * + * @return The value of the leaf. + */ + ValueType getValue() const; + /*! * Retrieves whether this ADD represents the constant one function. * @@ -564,6 +571,7 @@ namespace storm { * explicit vector. * * @param dd The DD to add to the explicit vector. + * @param negated A flag indicating whether the DD node is to be interpreted as being negated. * @param currentLevel The currently considered level in the DD. * @param maxLevel The number of levels that need to be considered. * @param currentOffset The current offset. @@ -571,7 +579,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(MTBDD dd, std::vector const* offsets, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector, std::function const& function) const; + void composeWithExplicitVectorRec(MTBDD dd, bool negated, std::vector const* offsets, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector, std::function const& function) const; /*! * Splits the given matrix DD into the groups using the given group variables. diff --git a/src/storage/dd/sylvan/InternalSylvanBdd.cpp b/src/storage/dd/sylvan/InternalSylvanBdd.cpp index 8e9fd8c53..cccb2af2d 100644 --- a/src/storage/dd/sylvan/InternalSylvanBdd.cpp +++ b/src/storage/dd/sylvan/InternalSylvanBdd.cpp @@ -8,7 +8,8 @@ #include "src/storage/BitVector.h" -#include +#include "src/utility/macros.h" +#include "src/exceptions/InvalidOperationException.h" namespace storm { namespace dd { @@ -227,7 +228,13 @@ namespace storm { template InternalAdd InternalBdd::toAdd() const { - return InternalAdd(ddManager, this->sylvanBdd.toDoubleMtbdd()); + if (std::is_same::value) { + return InternalAdd(ddManager, this->sylvanBdd.toDoubleMtbdd()); + } else if (std::is_same::value) { + return InternalAdd(ddManager, this->sylvanBdd.toUint64Mtbdd()); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Illegal ADD type."); + } } storm::storage::BitVector InternalBdd::toVector(storm::dd::Odd const& rowOdd, std::vector const& ddVariableIndices) const { @@ -269,7 +276,7 @@ namespace storm { std::vector, std::shared_ptr, HashFunctor>> uniqueTableForLevels(ddVariableIndices.size() + 1); // Now construct the ODD structure from the BDD. - std::shared_ptr rootOdd = createOddRec(bdd_regular(this->getSylvanBdd().GetBDD()), 0, bdd_isnegated(this->getSylvanBdd().GetBDD()), ddVariableIndices.size(), ddVariableIndices, uniqueTableForLevels); + std::shared_ptr rootOdd = createOddRec(bdd_regular(this->getSylvanBdd().GetBDD()), bdd_isnegated(this->getSylvanBdd().GetBDD()), 0, ddVariableIndices.size(), ddVariableIndices, uniqueTableForLevels); // Return a copy of the root node to remove the shared_ptr encapsulation. return Odd(*rootOdd); @@ -282,7 +289,7 @@ namespace storm { return result; } - std::shared_ptr InternalBdd::createOddRec(BDD dd, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector const& ddVariableIndices, std::vector, std::shared_ptr, HashFunctor>>& uniqueTableForLevels) { + std::shared_ptr InternalBdd::createOddRec(BDD dd, bool complement, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector const& ddVariableIndices, std::vector, std::shared_ptr, 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()) { @@ -310,7 +317,7 @@ namespace storm { } else if (bdd_isterminal(dd) || ddVariableIndices[currentLevel] < sylvan_var(dd)) { // 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 elseNode = createOddRec(dd, currentLevel + 1, complement, maxLevel, ddVariableIndices, uniqueTableForLevels); + std::shared_ptr elseNode = createOddRec(dd, complement, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels); std::shared_ptr thenNode = elseNode; uint_fast64_t totalOffset = elseNode->getElseOffset() + elseNode->getThenOffset(); return std::make_shared(elseNode, totalOffset, thenNode, totalOffset); @@ -323,8 +330,8 @@ namespace storm { bool elseComplemented = bdd_isnegated(elseDdNode) ^ complement; bool thenComplemented = bdd_isnegated(thenDdNode) ^ complement; - std::shared_ptr elseNode = createOddRec(bdd_regular(elseDdNode), currentLevel + 1, elseComplemented, maxLevel, ddVariableIndices, uniqueTableForLevels); - std::shared_ptr thenNode = createOddRec(bdd_regular(thenDdNode), currentLevel + 1, thenComplemented, maxLevel, ddVariableIndices, uniqueTableForLevels); + std::shared_ptr elseNode = createOddRec(bdd_regular(elseDdNode), elseComplemented, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels); + std::shared_ptr thenNode = createOddRec(bdd_regular(thenDdNode), thenComplemented, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels); return std::make_shared(elseNode, elseNode->getElseOffset() + elseNode->getThenOffset(), thenNode, thenNode->getElseOffset() + thenNode->getThenOffset()); } diff --git a/src/storage/dd/sylvan/InternalSylvanBdd.h b/src/storage/dd/sylvan/InternalSylvanBdd.h index 5fef343ae..b1effdf47 100644 --- a/src/storage/dd/sylvan/InternalSylvanBdd.h +++ b/src/storage/dd/sylvan/InternalSylvanBdd.h @@ -352,15 +352,15 @@ namespace storm { * Recursively builds the ODD from a BDD (that potentially has complement edges). * * @param dd The BDD for which to build the ODD. - * @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 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 createOddRec(BDD dd, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector const& ddVariableIndices, std::vector, std::shared_ptr, HashFunctor>>& uniqueTableForLevels); + static std::shared_ptr createOddRec(BDD dd, bool complement, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector const& ddVariableIndices, std::vector, std::shared_ptr, HashFunctor>>& uniqueTableForLevels); /*! * Helper function to convert the DD into a bit vector. diff --git a/test/functional/storage/SylvanDdTest.cpp b/test/functional/storage/SylvanDdTest.cpp index 3b7e8e06d..9cf188c24 100644 --- a/test/functional/storage/SylvanDdTest.cpp +++ b/test/functional/storage/SylvanDdTest.cpp @@ -339,30 +339,30 @@ TEST(SylvanDd, AddOddTest) { EXPECT_TRUE(i+1 == ddAsVector[i]); } -// // Create a non-trivial matrix. -// dd = manager->template getIdentity(x.first).equals(manager->template getIdentity(x.second)) * manager->getRange(x.first).template toAdd(); -// dd += manager->getEncoding(x.first, 1).template toAdd() * manager->getRange(x.second).template toAdd() + manager->getEncoding(x.second, 1).template toAdd() * manager->getRange(x.first).template toAdd(); -// -// // Create the ODDs. -// storm::dd::Odd rowOdd; -// ASSERT_NO_THROW(rowOdd = manager->getRange(x.first).template toAdd().createOdd()); -// storm::dd::Odd columnOdd; -// ASSERT_NO_THROW(columnOdd = manager->getRange(x.second).template toAdd().createOdd()); -// -// // Try to translate the matrix. -// storm::storage::SparseMatrix matrix; -// ASSERT_NO_THROW(matrix = dd.toMatrix({x.first}, {x.second}, rowOdd, columnOdd)); -// -// EXPECT_EQ(9ul, matrix.getRowCount()); -// EXPECT_EQ(9ul, matrix.getColumnCount()); -// EXPECT_EQ(25ul, matrix.getNonzeroEntryCount()); -// -// dd = manager->getRange(x.first).template toAdd() * manager->getRange(x.second).template toAdd() * manager->getEncoding(a.first, 0).template toAdd().ite(dd, dd + manager->template getConstant(1)); -// ASSERT_NO_THROW(matrix = dd.toMatrix({a.first}, rowOdd, columnOdd)); -// EXPECT_EQ(18ul, matrix.getRowCount()); -// EXPECT_EQ(9ul, matrix.getRowGroupCount()); -// EXPECT_EQ(9ul, matrix.getColumnCount()); -// EXPECT_EQ(106ul, matrix.getNonzeroEntryCount()); + // Create a non-trivial matrix. + dd = manager->template getIdentity(x.first).equals(manager->template getIdentity(x.second)).template toAdd() * manager->getRange(x.first).template toAdd(); + dd += manager->getEncoding(x.first, 1).template toAdd() * manager->getRange(x.second).template toAdd() + manager->getEncoding(x.second, 1).template toAdd() * manager->getRange(x.first).template toAdd(); + + // Create the ODDs. + storm::dd::Odd rowOdd; + ASSERT_NO_THROW(rowOdd = manager->getRange(x.first).template toAdd().createOdd()); + storm::dd::Odd columnOdd; + ASSERT_NO_THROW(columnOdd = manager->getRange(x.second).template toAdd().createOdd()); + + // Try to translate the matrix. + storm::storage::SparseMatrix matrix; + ASSERT_NO_THROW(matrix = dd.toMatrix({x.first}, {x.second}, rowOdd, columnOdd)); + + EXPECT_EQ(9ul, matrix.getRowCount()); + EXPECT_EQ(9ul, matrix.getColumnCount()); + EXPECT_EQ(25ul, matrix.getNonzeroEntryCount()); + + dd = manager->getRange(x.first).template toAdd() * manager->getRange(x.second).template toAdd() * manager->getEncoding(a.first, 0).template toAdd().ite(dd, dd + manager->template getConstant(1)); + ASSERT_NO_THROW(matrix = dd.toMatrix({a.first}, rowOdd, columnOdd)); + EXPECT_EQ(18ul, matrix.getRowCount()); + EXPECT_EQ(9ul, matrix.getRowGroupCount()); + EXPECT_EQ(9ul, matrix.getColumnCount()); + EXPECT_EQ(106ul, matrix.getNonzeroEntryCount()); } TEST(SylvanDd, BddOddTest) { @@ -381,13 +381,13 @@ TEST(SylvanDd, BddOddTest) { ASSERT_NO_THROW(ddAsVector = dd.toVector()); EXPECT_EQ(9ul, ddAsVector.size()); for (uint_fast64_t i = 0; i < ddAsVector.size(); ++i) { - EXPECT_TRUE(i+1 == ddAsVector[i]); + EXPECT_EQ(i+1, ddAsVector[i]); } - storm::dd::Add vectorAdd = storm::dd::Add::fromVector(manager, ddAsVector, odd, {x.first}); + storm::dd::Add vectorAdd = storm::dd::Add::fromVector(*manager, ddAsVector, odd, {x.first}); // Create a non-trivial matrix. - dd = manager->template getIdentity(x.first).equals(manager->template getIdentity(x.second)) * manager->getRange(x.first).template toAdd(); + dd = manager->template getIdentity(x.first).equals(manager->template getIdentity(x.second)).template toAdd() * manager->getRange(x.first).template toAdd(); dd += manager->getEncoding(x.first, 1).template toAdd() * manager->getRange(x.second).template toAdd() + manager->getEncoding(x.second, 1).template toAdd() * manager->getRange(x.first).template toAdd(); // Create the ODDs.