sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Made internal changes to SimpleValuations to (hopefully) make it nice and fast. 

Former-commit-id: 1e9f18f522
tempestpy_adaptions
dehnert 11 years ago
parent
9d3e78ab89
commit
024b98978f
4 changed files with 38 additions and 95 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 5
      src/storage/dd/CuddDdForwardIterator.cpp
  2. 2
      src/storage/dd/CuddDdForwardIterator.h
  3. 98
      src/storage/expressions/SimpleValuation.cpp
  4. 28
      src/storage/expressions/SimpleValuation.h

5
src/storage/dd/CuddDdForwardIterator.cpp
View File

@ -5,6 +5,10 @@
namespace storm {
namespace dd {
DdForwardIterator<DdType::CUDD>::DdForwardIterator() : ddManager(), generator(), cube(), value(), isAtEnd(), metaVariables(), 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) : 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<DdType::CUDD>::~DdForwardIterator() {
// We free the pointers sind Cudd allocates them using malloc rather than new/delete.
if (this->cube != nullptr) {
free(this->cube);
}

2
src/storage/dd/CuddDdForwardIterator.h
View File

@ -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;

98
src/storage/expressions/SimpleValuation.cpp
View File

@ -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<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;
}
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 << "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<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 +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;
}
}
}

28
src/storage/expressions/SimpleValuation.h
View File

@ -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
@ -92,22 +87,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;
};
/*!

Write Preview
Loading…
Cancel
Save