diff --git a/src/storage/dd/CuddDdForwardIterator.cpp b/src/storage/dd/CuddDdForwardIterator.cpp index c0e754c8b..017845b47 100644 --- a/src/storage/dd/CuddDdForwardIterator.cpp +++ b/src/storage/dd/CuddDdForwardIterator.cpp @@ -5,6 +5,10 @@ namespace storm { namespace dd { + DdForwardIterator::DdForwardIterator() : ddManager(), generator(), cube(), value(), isAtEnd(), metaVariables(), cubeCounter(), relevantDontCareDdVariables(), currentValuation() { + // Intentionally left empty. + } + DdForwardIterator::DdForwardIterator(std::shared_ptr> ddManager, DdGen* generator, int* cube, double value, bool isAtEnd, std::set const* metaVariables) : ddManager(ddManager), generator(generator), cube(cube), value(value), isAtEnd(isAtEnd), metaVariables(metaVariables), 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. @@ -49,6 +53,7 @@ namespace storm { } DdForwardIterator::~DdForwardIterator() { + // We free the pointers sind Cudd allocates them using malloc rather than new/delete. if (this->cube != nullptr) { free(this->cube); } diff --git a/src/storage/dd/CuddDdForwardIterator.h b/src/storage/dd/CuddDdForwardIterator.h index 054438d2e..0515475a4 100644 --- a/src/storage/dd/CuddDdForwardIterator.h +++ b/src/storage/dd/CuddDdForwardIterator.h @@ -25,7 +25,7 @@ namespace storm { friend class Dd; // Default-instantiate the constructor. - DdForwardIterator() = default; + DdForwardIterator(); // Forbid copy-construction and copy assignment, because ownership of the internal pointer is unclear then. DdForwardIterator(DdForwardIterator const& other) = delete; diff --git a/src/storage/expressions/SimpleValuation.cpp b/src/storage/expressions/SimpleValuation.cpp index d29e6a7c8..f930f7e10 100644 --- a/src/storage/expressions/SimpleValuation.cpp +++ b/src/storage/expressions/SimpleValuation.cpp @@ -2,102 +2,74 @@ #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()), integerIdentifierToIndexMap(new std::unordered_map()), doubleIdentifierToIndexMap(new std::unordered_map()), 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; } 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(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(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(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 << "valuation { "; + for (auto const& nameValuePair : valuation.identifierToValueMap) { + stream << nameValuePair.first << ": " << nameValuePair.second << std::endl; } - stream << "] double ["; - if (!valuation.doubleValues.empty()) { - for (uint_fast64_t i = 0; i < valuation.doubleValues.size() - 1; ++i) { - stream << valuation.doubleValues[i] << ", "; - } - 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(seed, value); - } - for (auto const& value : valuation->integerValues) { - boost::hash_combine(seed, value); - } - for (auto const& value : valuation->doubleValues) { - boost::hash_combine(seed, value); + for (auto const& nameValuePair : valuation->identifierToValueMap) { + boost::hash_combine(seed, nameValuePair.first); + boost::hash_combine(seed, nameValuePair.second); } return seed; } @@ -107,21 +79,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..55caab46b 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 -#include -#include +#include +#include #include #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 @@ -92,22 +87,7 @@ namespace storm { private: // A mapping of boolean identifiers to their local indices in the value container. - std::shared_ptr> booleanIdentifierToIndexMap; - - // A mapping of integer identifiers to their local indices in the value container. - std::shared_ptr> integerIdentifierToIndexMap; - - // A mapping of double identifiers to their local indices in the value container. - std::shared_ptr> doubleIdentifierToIndexMap; - - // The value container for all boolean identifiers. - std::vector booleanValues; - - // The value container for all integer identifiers. - std::vector integerValues; - - // The value container for all double identifiers. - std::vector doubleValues; + boost::container::flat_map> identifierToValueMap; }; /*!