diff --git a/src/storage/dd/CuddDd.cpp b/src/storage/dd/CuddDd.cpp
index 72abb87bf..cdff92894 100644
--- a/src/storage/dd/CuddDd.cpp
+++ b/src/storage/dd/CuddDd.cpp
@@ -473,15 +473,15 @@ namespace storm {
return this->ddManager;
}
- DdForwardIterator<DdType::CUDD> Dd<DdType::CUDD>::begin() const {
+ DdForwardIterator<DdType::CUDD> Dd<DdType::CUDD>::begin(bool enumerateDontCareMetaVariables) const {
int* cube;
double value;
DdGen* generator = this->getCuddAdd().FirstCube(&cube, &value);
- return DdForwardIterator<DdType::CUDD>(this->getDdManager(), generator, cube, value, Cudd_IsGenEmpty(generator), &this->getContainedMetaVariableNames());
+ return DdForwardIterator<DdType::CUDD>(this->getDdManager(), generator, cube, value, Cudd_IsGenEmpty(generator), &this->getContainedMetaVariableNames(), enumerateDontCareMetaVariables);
}
- DdForwardIterator<DdType::CUDD> Dd<DdType::CUDD>::end() const {
- return DdForwardIterator<DdType::CUDD>(this->getDdManager(), nullptr, nullptr, 0, true, nullptr);
+ DdForwardIterator<DdType::CUDD> Dd<DdType::CUDD>::end(bool enumerateDontCareMetaVariables) const {
+ return DdForwardIterator<DdType::CUDD>(this->getDdManager(), nullptr, nullptr, 0, true, nullptr, enumerateDontCareMetaVariables);
}
std::ostream & operator<<(std::ostream& out, const Dd<DdType::CUDD>& dd) {
diff --git a/src/storage/dd/CuddDd.h b/src/storage/dd/CuddDd.h
index f345c28a2..9f638d329 100644
--- a/src/storage/dd/CuddDd.h
+++ b/src/storage/dd/CuddDd.h
@@ -440,16 +440,20 @@ namespace storm {
/*!
* Retrieves an iterator that points to the first meta variable assignment with a non-zero function value.
*
+ * @param enumerateDontCareMetaVariables If set to true, all meta variable assignments are enumerated, even
+ * if a meta variable does not at all influence the the function value.
* @return An iterator that points to the first meta variable assignment with a non-zero function value.
*/
- DdForwardIterator<DdType::CUDD> begin() const;
+ DdForwardIterator<DdType::CUDD> begin(bool enumerateDontCareMetaVariables = true) const;
/*!
* Retrieves an iterator that points past the end of the container.
*
+ * @param enumerateDontCareMetaVariables If set to true, all meta variable assignments are enumerated, even
+ * if a meta variable does not at all influence the the function value.
* @return An iterator that points past the end of the container.
*/
- DdForwardIterator<DdType::CUDD> end() const;
+ DdForwardIterator<DdType::CUDD> end(bool enumerateDontCareMetaVariables = true) const;
friend std::ostream & operator<<(std::ostream& out, const Dd<DdType::CUDD>& dd);
private:
diff --git a/src/storage/dd/CuddDdForwardIterator.cpp b/src/storage/dd/CuddDdForwardIterator.cpp
index c0e754c8b..cce5c112c 100644
--- a/src/storage/dd/CuddDdForwardIterator.cpp
+++ b/src/storage/dd/CuddDdForwardIterator.cpp
@@ -5,7 +5,11 @@
namespace storm {
namespace dd {
- DdForwardIterator<DdType::CUDD>::DdForwardIterator(std::shared_ptr<DdManager<DdType::CUDD>> ddManager, DdGen* generator, int* cube, double value, bool isAtEnd, std::set<std::string> const* metaVariables) : ddManager(ddManager), generator(generator), cube(cube), value(value), isAtEnd(isAtEnd), metaVariables(metaVariables), cubeCounter(), relevantDontCareDdVariables(), currentValuation() {
+ DdForwardIterator<DdType::CUDD>::DdForwardIterator() : ddManager(), generator(), cube(), value(), isAtEnd(), metaVariables(), enumerateDontCareMetaVariables(), cubeCounter(), relevantDontCareDdVariables(), currentValuation() {
+ // Intentionally left empty.
+ }
+
+ DdForwardIterator<DdType::CUDD>::DdForwardIterator(std::shared_ptr<DdManager<DdType::CUDD>> ddManager, DdGen* generator, int* cube, double value, bool isAtEnd, std::set<std::string> const* metaVariables, bool enumerateDontCareMetaVariables) : ddManager(ddManager), generator(generator), cube(cube), value(value), isAtEnd(isAtEnd), metaVariables(metaVariables), enumerateDontCareMetaVariables(enumerateDontCareMetaVariables), cubeCounter(), relevantDontCareDdVariables(), currentValuation() {
// If the given generator is not yet at its end, we need to create the current valuation from the cube from
// scratch.
if (!this->isAtEnd) {
@@ -49,6 +53,7 @@ namespace storm {
}
DdForwardIterator<DdType::CUDD>::~DdForwardIterator() {
+ // We free the pointers sind Cudd allocates them using malloc rather than new/delete.
if (this->cube != nullptr) {
free(this->cube);
}
@@ -108,29 +113,60 @@ namespace storm {
// don't cares. In the latter case, we add them to a special list, so we can iterate over their concrete
// valuations later.
for (auto const& metaVariableName : *this->metaVariables) {
+ bool metaVariableAppearsInCube = false;
+ std::vector<std::tuple<ADD, std::string, uint_fast64_t>> localRelenvantDontCareDdVariables;
auto const& metaVariable = this->ddManager->getMetaVariable(metaVariableName);
if (metaVariable.getType() == DdMetaVariable<DdType::CUDD>::MetaVariableType::Bool) {
if (this->cube[metaVariable.getDdVariables()[0].getCuddAdd().NodeReadIndex()] == 0) {
- currentValuation.setBooleanValue(metaVariableName, false);
+ metaVariableAppearsInCube = true;
+ if (!currentValuation.containsBooleanIdentifier(metaVariableName)) {
+ currentValuation.addBooleanIdentifier(metaVariableName, false);
+ } else {
+ currentValuation.setBooleanValue(metaVariableName, false);
+ }
} else if (this->cube[metaVariable.getDdVariables()[0].getCuddAdd().NodeReadIndex()] == 1) {
- currentValuation.setBooleanValue(metaVariableName, true);
+ metaVariableAppearsInCube = true;
+ if (!currentValuation.containsBooleanIdentifier(metaVariableName)) {
+ currentValuation.addBooleanIdentifier(metaVariableName, true);
+ } else {
+ currentValuation.setBooleanValue(metaVariableName, true);
+ }
} else {
- relevantDontCareDdVariables.push_back(std::make_tuple(metaVariable.getDdVariables()[0].getCuddAdd(), metaVariableName, 0));
+ localRelenvantDontCareDdVariables.push_back(std::make_tuple(metaVariable.getDdVariables()[0].getCuddAdd(), metaVariableName, 0));
}
} else {
int_fast64_t intValue = 0;
for (uint_fast64_t bitIndex = 0; bitIndex < metaVariable.getNumberOfDdVariables(); ++bitIndex) {
if (cube[metaVariable.getDdVariables()[bitIndex].getCuddAdd().NodeReadIndex()] == 0) {
// Leave bit unset.
+ metaVariableAppearsInCube = true;
} else if (cube[metaVariable.getDdVariables()[bitIndex].getCuddAdd().NodeReadIndex()] == 1) {
intValue |= 1ull << (metaVariable.getNumberOfDdVariables() - bitIndex - 1);
+ metaVariableAppearsInCube = true;
} else {
// Temporarily leave bit unset so we can iterate trough the other option later.
// Add the bit to the relevant don't care bits.
- this->relevantDontCareDdVariables.push_back(std::make_tuple(metaVariable.getDdVariables()[bitIndex].getCuddAdd(), metaVariableName, metaVariable.getNumberOfDdVariables() - bitIndex - 1));
+ localRelenvantDontCareDdVariables.push_back(std::make_tuple(metaVariable.getDdVariables()[bitIndex].getCuddAdd(), metaVariableName, metaVariable.getNumberOfDdVariables() - bitIndex - 1));
}
}
- currentValuation.setIntegerValue(metaVariableName, intValue + metaVariable.getLow());
+ if (this->enumerateDontCareMetaVariables || metaVariableAppearsInCube) {
+ if (!currentValuation.containsIntegerIdentifier(metaVariableName)) {
+ currentValuation.addIntegerIdentifier(metaVariableName);
+ }
+ currentValuation.setIntegerValue(metaVariableName, intValue + metaVariable.getLow());
+ }
+ }
+
+ // If all meta variables are to be enumerated or the meta variable appeared in the cube, we register the
+ // missing bits to later enumerate all possible valuations.
+ if (this->enumerateDontCareMetaVariables || metaVariableAppearsInCube) {
+ relevantDontCareDdVariables.insert(relevantDontCareDdVariables.end(), localRelenvantDontCareDdVariables.begin(), localRelenvantDontCareDdVariables.end());
+ }
+
+ // If the meta variable does not appear in the cube and we're not supposed to enumerate such meta variables
+ // we remove the meta variable from the valuation.
+ if (!this->enumerateDontCareMetaVariables && !metaVariableAppearsInCube) {
+ currentValuation.removeIdentifier(metaVariableName);
}
}
diff --git a/src/storage/dd/CuddDdForwardIterator.h b/src/storage/dd/CuddDdForwardIterator.h
index 054438d2e..8b08af929 100644
--- a/src/storage/dd/CuddDdForwardIterator.h
+++ b/src/storage/dd/CuddDdForwardIterator.h
@@ -25,7 +25,7 @@ namespace storm {
friend class Dd<DdType::CUDD>;
// Default-instantiate the constructor.
- DdForwardIterator() = default;
+ DdForwardIterator();
// Forbid copy-construction and copy assignment, because ownership of the internal pointer is unclear then.
DdForwardIterator(DdForwardIterator<DdType::CUDD> const& other) = delete;
@@ -82,8 +82,10 @@ namespace storm {
* @param isAtEnd A flag that indicates whether the iterator is at its end and may not be moved forward any
* more.
* @param metaVariables The meta variables that appear in the DD.
+ * @param enumerateDontCareMetaVariables If set to true, all meta variable assignments are enumerated, even
+ * if a meta variable does not at all influence the the function value.
*/
- DdForwardIterator(std::shared_ptr<DdManager<DdType::CUDD>> ddManager, DdGen* generator, int* cube, double value, bool isAtEnd, std::set<std::string> const* metaVariables = nullptr);
+ DdForwardIterator(std::shared_ptr<DdManager<DdType::CUDD>> ddManager, DdGen* generator, int* cube, double value, bool isAtEnd, std::set<std::string> const* metaVariables = nullptr, bool enumerateDontCareMetaVariables = true);
/*!
* Recreates the internal information when a new cube needs to be treated.
@@ -114,6 +116,10 @@ namespace storm {
// The set of meta variables appearing in the DD.
std::set<std::string> const* metaVariables;
+ // A flag that indicates whether the iterator is supposed to enumerate meta variable valuations even if
+ // they don't influence the function value.
+ bool enumerateDontCareMetaVariables;
+
// A number that represents how many assignments of the current cube have already been returned previously.
// This is needed, because cubes may represent many assignments (if they have don't care variables).
uint_fast64_t cubeCounter;
diff --git a/src/storage/expressions/SimpleValuation.cpp b/src/storage/expressions/SimpleValuation.cpp
index d29e6a7c8..4a5441e99 100644
--- a/src/storage/expressions/SimpleValuation.cpp
+++ b/src/storage/expressions/SimpleValuation.cpp
@@ -2,102 +2,109 @@
#include "src/storage/expressions/SimpleValuation.h"
#include "src/exceptions/ExceptionMacros.h"
#include "src/exceptions/InvalidArgumentException.h"
+#include "src/exceptions/InvalidAccessException.h"
namespace storm {
namespace expressions {
- SimpleValuation::SimpleValuation() : booleanIdentifierToIndexMap(new std::unordered_map<std::string, uint_fast64_t>()), integerIdentifierToIndexMap(new std::unordered_map<std::string, uint_fast64_t>()), doubleIdentifierToIndexMap(new std::unordered_map<std::string, uint_fast64_t>()), booleanValues(), integerValues(), doubleValues() {
- // Intentionally left empty.
- }
-
bool SimpleValuation::operator==(SimpleValuation const& other) const {
- return this->booleanIdentifierToIndexMap.get() == other.booleanIdentifierToIndexMap.get() && this->integerIdentifierToIndexMap.get() == other.integerIdentifierToIndexMap.get() && this->doubleIdentifierToIndexMap.get() == other.doubleIdentifierToIndexMap.get() && this->booleanValues == other.booleanValues && this->integerValues == other.integerValues && this->doubleValues == other.doubleValues;
+ return this->identifierToValueMap == other.identifierToValueMap;
}
void SimpleValuation::addBooleanIdentifier(std::string const& name, bool initialValue) {
- LOG_THROW(this->booleanIdentifierToIndexMap->find(name) == this->booleanIdentifierToIndexMap->end(), storm::exceptions::InvalidArgumentException, "Boolean identifier '" << name << "' already registered.");
-
- this->booleanIdentifierToIndexMap->emplace(name, this->booleanValues.size());
- this->booleanValues.push_back(initialValue);
+ LOG_THROW(this->identifierToValueMap.find(name) == this->identifierToValueMap.end(), storm::exceptions::InvalidArgumentException, "Identifier '" << name << "' already registered.");
+ this->identifierToValueMap.emplace(name, initialValue);
}
void SimpleValuation::addIntegerIdentifier(std::string const& name, int_fast64_t initialValue) {
- LOG_THROW(this->booleanIdentifierToIndexMap->find(name) == this->booleanIdentifierToIndexMap->end(), storm::exceptions::InvalidArgumentException, "Integer identifier '" << name << "' already registered.");
-
- this->integerIdentifierToIndexMap->emplace(name, this->integerValues.size());
- this->integerValues.push_back(initialValue);
+ LOG_THROW(this->identifierToValueMap.find(name) == this->identifierToValueMap.end(), storm::exceptions::InvalidArgumentException, "Identifier '" << name << "' already registered.");
+ this->identifierToValueMap.emplace(name, initialValue);
}
void SimpleValuation::addDoubleIdentifier(std::string const& name, double initialValue) {
- LOG_THROW(this->booleanIdentifierToIndexMap->find(name) == this->booleanIdentifierToIndexMap->end(), storm::exceptions::InvalidArgumentException, "Double identifier '" << name << "' already registered.");
-
- this->doubleIdentifierToIndexMap->emplace(name, this->doubleValues.size());
- this->doubleValues.push_back(initialValue);
+ LOG_THROW(this->identifierToValueMap.find(name) == this->identifierToValueMap.end(), storm::exceptions::InvalidArgumentException, "Identifier '" << name << "' already registered.");
+ this->identifierToValueMap.emplace(name, initialValue);
}
void SimpleValuation::setBooleanValue(std::string const& name, bool value) {
- this->booleanValues[this->booleanIdentifierToIndexMap->at(name)] = value;
+ this->identifierToValueMap[name] = value;
}
void SimpleValuation::setIntegerValue(std::string const& name, int_fast64_t value) {
- this->integerValues[this->integerIdentifierToIndexMap->at(name)] = value;
+ this->identifierToValueMap[name] = value;
}
void SimpleValuation::setDoubleValue(std::string const& name, double value) {
- this->doubleValues[this->doubleIdentifierToIndexMap->at(name)] = value;
+ this->identifierToValueMap[name] = value;
+ }
+
+ void SimpleValuation::removeIdentifier(std::string const& name) {
+ auto nameValuePair = this->identifierToValueMap.find(name);
+ LOG_THROW(nameValuePair != this->identifierToValueMap.end(), storm::exceptions::InvalidArgumentException, "Deleting unknown identifier '" << name << "'.");
+ this->identifierToValueMap.erase(nameValuePair);
+ }
+
+ bool SimpleValuation::containsBooleanIdentifier(std::string const& name) const {
+ auto nameValuePair = this->identifierToValueMap.find(name);
+ if (nameValuePair == this->identifierToValueMap.end()) {
+ return false;
+ }
+ return nameValuePair->second.type() == typeid(bool);
+ }
+
+ bool SimpleValuation::containsIntegerIdentifier(std::string const& name) const {
+ auto nameValuePair = this->identifierToValueMap.find(name);
+ if (nameValuePair == this->identifierToValueMap.end()) {
+ return false;
+ }
+ return nameValuePair->second.type() == typeid(int_fast64_t);
+ }
+
+ bool SimpleValuation::containsDoubleIdentifier(std::string const& name) const {
+ auto nameValuePair = this->identifierToValueMap.find(name);
+ if (nameValuePair == this->identifierToValueMap.end()) {
+ return false;
+ }
+ return nameValuePair->second.type() == typeid(double);
}
bool SimpleValuation::getBooleanValue(std::string const& name) const {
- auto const& nameIndexPair = this->booleanIdentifierToIndexMap->find(name);
- return this->booleanValues[nameIndexPair->second];
+ auto nameValuePair = this->identifierToValueMap.find(name);
+ LOG_THROW(nameValuePair != this->identifierToValueMap.end(), storm::exceptions::InvalidAccessException, "Access to unkown identifier '" << name << "'.");
+ return boost::get<bool>(nameValuePair->second);
}
int_fast64_t SimpleValuation::getIntegerValue(std::string const& name) const {
- auto const& nameIndexPair = this->integerIdentifierToIndexMap->find(name);
- return this->integerValues[nameIndexPair->second];
+ auto nameValuePair = this->identifierToValueMap.find(name);
+ LOG_THROW(nameValuePair != this->identifierToValueMap.end(), storm::exceptions::InvalidAccessException, "Access to unkown identifier '" << name << "'.");
+ return boost::get<int_fast64_t>(nameValuePair->second);
}
double SimpleValuation::getDoubleValue(std::string const& name) const {
- auto const& nameIndexPair = this->doubleIdentifierToIndexMap->find(name);
- return this->doubleValues[nameIndexPair->second];
+ auto nameValuePair = this->identifierToValueMap.find(name);
+ LOG_THROW(nameValuePair != this->identifierToValueMap.end(), storm::exceptions::InvalidAccessException, "Access to unkown identifier '" << name << "'.");
+ return boost::get<double>(nameValuePair->second);
}
std::ostream& operator<<(std::ostream& stream, SimpleValuation const& valuation) {
- stream << "valuation { bool [";
- if (!valuation.booleanValues.empty()) {
- for (uint_fast64_t i = 0; i < valuation.booleanValues.size() - 1; ++i) {
- stream << valuation.booleanValues[i] << ", ";
- }
- stream << valuation.booleanValues.back();
- }
- stream << "] int [";
- if (!valuation.integerValues.empty()) {
- for (uint_fast64_t i = 0; i < valuation.integerValues.size() - 1; ++i) {
- stream << valuation.integerValues[i] << ", ";
- }
- stream << valuation.integerValues.back();
- }
- stream << "] double [";
- if (!valuation.doubleValues.empty()) {
- for (uint_fast64_t i = 0; i < valuation.doubleValues.size() - 1; ++i) {
- stream << valuation.doubleValues[i] << ", ";
+ stream << "{ ";
+ uint_fast64_t elementIndex = 0;
+ for (auto const& nameValuePair : valuation.identifierToValueMap) {
+ stream << nameValuePair.first << " -> " << nameValuePair.second << " ";
+ ++elementIndex;
+ if (elementIndex < valuation.identifierToValueMap.size()) {
+ stream << ", ";
}
- stream << valuation.doubleValues.back();
}
- stream << "] }";
+ stream << "}";
return stream;
}
std::size_t SimpleValuationPointerHash::operator()(SimpleValuation* valuation) const {
size_t seed = 0;
- for (auto const& value : valuation->booleanValues) {
- boost::hash_combine<bool>(seed, value);
- }
- for (auto const& value : valuation->integerValues) {
- boost::hash_combine<int_fast64_t>(seed, value);
- }
- for (auto const& value : valuation->doubleValues) {
- boost::hash_combine<double>(seed, value);
+ for (auto const& nameValuePair : valuation->identifierToValueMap) {
+ boost::hash_combine(seed, nameValuePair.first);
+ boost::hash_combine(seed, nameValuePair.second);
}
return seed;
}
@@ -107,21 +114,7 @@ namespace storm {
}
bool SimpleValuationPointerLess::operator()(SimpleValuation* valuation1, SimpleValuation* valuation2) const {
- // Compare boolean variables.
- bool less = valuation1->booleanValues < valuation2->booleanValues;
- if (less) {
- return true;
- }
- less = valuation1->integerValues < valuation2->integerValues;
- if (less) {
- return true;
- }
- less = valuation1->doubleValues < valuation2->doubleValues;
- if (less) {
- return true;
- } else {
- return false;
- }
+ return valuation1->identifierToValueMap < valuation2->identifierToValueMap;
}
}
}
\ No newline at end of file
diff --git a/src/storage/expressions/SimpleValuation.h b/src/storage/expressions/SimpleValuation.h
index a196921a6..0ea05a511 100644
--- a/src/storage/expressions/SimpleValuation.h
+++ b/src/storage/expressions/SimpleValuation.h
@@ -1,9 +1,8 @@
#ifndef STORM_STORAGE_EXPRESSIONS_SIMPLEVALUATION_H_
#define STORM_STORAGE_EXPRESSIONS_SIMPLEVALUATION_H_
-#include <memory>
-#include <vector>
-#include <unordered_map>
+#include <boost/container/flat_map.hpp>
+#include <boost/variant.hpp>
#include <iostream>
#include "src/storage/expressions/Valuation.h"
@@ -16,12 +15,8 @@ namespace storm {
friend class SimpleValuationPointerHash;
friend class SimpleValuationPointerLess;
- /*!
- * Creates a simple valuation without any identifiers.
- */
- SimpleValuation();
-
// Instantiate some constructors and assignments with their default implementations.
+ SimpleValuation() = default;
SimpleValuation(SimpleValuation const&) = default;
SimpleValuation& operator=(SimpleValuation const&) = default;
#ifndef WINDOWS
@@ -83,7 +78,17 @@ namespace storm {
*/
void setDoubleValue(std::string const& name, double value);
+ /*!
+ * Removes the given identifier from this valuation.
+ *
+ * @param name The name of the identifier that is to be removed.
+ */
+ void removeIdentifier(std::string const& name);
+
// Override base class methods.
+ virtual bool containsBooleanIdentifier(std::string const& name) const override;
+ virtual bool containsIntegerIdentifier(std::string const& name) const override;
+ virtual bool containsDoubleIdentifier(std::string const& name) const override;
virtual bool getBooleanValue(std::string const& name) const override;
virtual int_fast64_t getIntegerValue(std::string const& name) const override;
virtual double getDoubleValue(std::string const& name) const override;
@@ -92,22 +97,7 @@ namespace storm {
private:
// A mapping of boolean identifiers to their local indices in the value container.
- std::shared_ptr<std::unordered_map<std::string, uint_fast64_t>> booleanIdentifierToIndexMap;
-
- // A mapping of integer identifiers to their local indices in the value container.
- std::shared_ptr<std::unordered_map<std::string, uint_fast64_t>> integerIdentifierToIndexMap;
-
- // A mapping of double identifiers to their local indices in the value container.
- std::shared_ptr<std::unordered_map<std::string, uint_fast64_t>> doubleIdentifierToIndexMap;
-
- // The value container for all boolean identifiers.
- std::vector<bool> booleanValues;
-
- // The value container for all integer identifiers.
- std::vector<int_fast64_t> integerValues;
-
- // The value container for all double identifiers.
- std::vector<double> doubleValues;
+ boost::container::flat_map<std::string, boost::variant<bool, int_fast64_t, double>> identifierToValueMap;
};
/*!
diff --git a/src/storage/expressions/Valuation.h b/src/storage/expressions/Valuation.h
index 7aa32a859..19792b720 100644
--- a/src/storage/expressions/Valuation.h
+++ b/src/storage/expressions/Valuation.h
@@ -34,6 +34,31 @@ namespace storm {
* @return The value of the double identifier.
*/
virtual double getDoubleValue(std::string const& name) const = 0;
+
+ /*!
+ * Retrieves whether there exists a boolean identifier with the given name in the valuation.
+ *
+ * @param name The name of the boolean identifier to query.
+ * @return True iff the identifier exists and is of boolean type.
+ */
+ virtual bool containsBooleanIdentifier(std::string const& name) const = 0;
+
+ /*!
+ * Retrieves whether there exists a integer identifier with the given name in the valuation.
+ *
+ * @param name The name of the integer identifier to query.
+ * @return True iff the identifier exists and is of boolean type.
+ */
+ virtual bool containsIntegerIdentifier(std::string const& name) const = 0;
+
+ /*!
+ * Retrieves whether there exists a double identifier with the given name in the valuation.
+ *
+ * @param name The name of the double identifier to query.
+ * @return True iff the identifier exists and is of boolean type.
+ */
+ virtual bool containsDoubleIdentifier(std::string const& name) const = 0;
+
};
}
}
diff --git a/test/functional/storage/CuddDdTest.cpp b/test/functional/storage/CuddDdTest.cpp
index 91d14f202..ce40c94d1 100644
--- a/test/functional/storage/CuddDdTest.cpp
+++ b/test/functional/storage/CuddDdTest.cpp
@@ -307,4 +307,26 @@ TEST(CuddDd, ForwardIteratorTest) {
++numberOfValuations;
}
EXPECT_EQ(9, numberOfValuations);
+
+ dd = manager->getRange("x");
+ dd = dd.ite(manager->getOne(), manager->getOne());
+ ASSERT_NO_THROW(it = dd.begin());
+ ASSERT_NO_THROW(ite = dd.end());
+ numberOfValuations = 0;
+ while (it != ite) {
+ ASSERT_NO_THROW(valuationValuePair = *it);
+ ASSERT_NO_THROW(++it);
+ ++numberOfValuations;
+ }
+ EXPECT_EQ(16, numberOfValuations);
+
+ ASSERT_NO_THROW(it = dd.begin(false));
+ ASSERT_NO_THROW(ite = dd.end());
+ numberOfValuations = 0;
+ while (it != ite) {
+ ASSERT_NO_THROW(valuationValuePair = *it);
+ ASSERT_NO_THROW(++it);
+ ++numberOfValuations;
+ }
+ EXPECT_EQ(1, numberOfValuations);
}