dehnert
11 years ago
45 changed files with 1354 additions and 760 deletions
-
86src/adapters/MathsatExpressionAdapter.h
-
106src/adapters/Z3ExpressionAdapter.h
-
62src/solver/MathsatSmtSolver.cpp
-
30src/solver/MathsatSmtSolver.h
-
26src/solver/SmtSolver.cpp
-
60src/solver/SmtSolver.h
-
91src/solver/Z3SmtSolver.cpp
-
20src/solver/Z3SmtSolver.h
-
6src/storage/expressions/BaseExpression.cpp
-
25src/storage/expressions/BaseExpression.h
-
2src/storage/expressions/BinaryBooleanFunctionExpression.cpp
-
3src/storage/expressions/BinaryBooleanFunctionExpression.h
-
9src/storage/expressions/BinaryExpression.cpp
-
4src/storage/expressions/BinaryExpression.h
-
2src/storage/expressions/BinaryNumericalFunctionExpression.cpp
-
3src/storage/expressions/BinaryNumericalFunctionExpression.h
-
2src/storage/expressions/BinaryRelationExpression.cpp
-
3src/storage/expressions/BinaryRelationExpression.h
-
6src/storage/expressions/BooleanLiteralExpression.cpp
-
4src/storage/expressions/BooleanLiteralExpression.h
-
6src/storage/expressions/DoubleLiteralExpression.cpp
-
4src/storage/expressions/DoubleLiteralExpression.h
-
73src/storage/expressions/Expression.cpp
-
64src/storage/expressions/Expression.h
-
247src/storage/expressions/ExpressionManager.cpp
-
333src/storage/expressions/ExpressionManager.h
-
20src/storage/expressions/ExpressionReturnType.h
-
13src/storage/expressions/IfThenElseExpression.cpp
-
4src/storage/expressions/IfThenElseExpression.h
-
6src/storage/expressions/IntegerLiteralExpression.cpp
-
4src/storage/expressions/IntegerLiteralExpression.h
-
177src/storage/expressions/SimpleValuation.cpp
-
148src/storage/expressions/SimpleValuation.h
-
2src/storage/expressions/UnaryBooleanFunctionExpression.cpp
-
3src/storage/expressions/UnaryBooleanFunctionExpression.h
-
6src/storage/expressions/UnaryExpression.cpp
-
4src/storage/expressions/UnaryExpression.h
-
2src/storage/expressions/UnaryNumericalFunctionExpression.cpp
-
3src/storage/expressions/UnaryNumericalFunctionExpression.h
-
82src/storage/expressions/Valuation.cpp
-
136src/storage/expressions/Valuation.h
-
54src/storage/expressions/Variable.cpp
-
138src/storage/expressions/Variable.h
-
20src/storage/expressions/VariableExpression.cpp
-
15src/storage/expressions/VariableExpression.h
@ -0,0 +1,247 @@ |
|||
#include "src/storage/expressions/ExpressionManager.h"
|
|||
|
|||
#include "src/storage/expressions/Expressions.h"
|
|||
#include "src/storage/expressions/Variable.h"
|
|||
#include "src/utility/macros.h"
|
|||
#include "src/exceptions/InvalidStateException.h"
|
|||
|
|||
namespace storm { |
|||
namespace expressions { |
|||
|
|||
VariableIterator::VariableIterator(ExpressionManager const& manager, std::unordered_map<std::string, uint_fast64_t>::const_iterator nameIndexIterator, std::unordered_map<std::string, uint_fast64_t>::const_iterator nameIndexIteratorEnd, VariableSelection const& selection) : manager(manager), nameIndexIterator(nameIndexIterator), nameIndexIteratorEnd(nameIndexIteratorEnd), selection(selection) { |
|||
moveUntilNextSelectedElement(false); |
|||
} |
|||
|
|||
bool VariableIterator::operator==(VariableIterator const& other) { |
|||
return this->nameIndexIterator == other.nameIndexIterator; |
|||
} |
|||
|
|||
bool VariableIterator::operator!=(VariableIterator const& other) { |
|||
return !(*this == other); |
|||
} |
|||
|
|||
VariableIterator::value_type& VariableIterator::operator*() { |
|||
return currentElement; |
|||
} |
|||
|
|||
VariableIterator& VariableIterator::operator++(int) { |
|||
moveUntilNextSelectedElement(); |
|||
return *this; |
|||
} |
|||
|
|||
VariableIterator& VariableIterator::operator++() { |
|||
moveUntilNextSelectedElement(); |
|||
return *this; |
|||
} |
|||
|
|||
void VariableIterator::moveUntilNextSelectedElement(bool atLeastOneStep) { |
|||
if (atLeastOneStep && nameIndexIterator != nameIndexIteratorEnd) { |
|||
++nameIndexIterator; |
|||
} |
|||
|
|||
// Move the underlying iterator forward until a variable matches the selection.
|
|||
while (nameIndexIterator != nameIndexIteratorEnd |
|||
&& (selection == VariableSelection::OnlyRegularVariables && (nameIndexIterator->second & ExpressionManager::auxiliaryMask) != 0) |
|||
&& (selection == VariableSelection::OnlyAuxiliaryVariables && (nameIndexIterator->second & ExpressionManager::auxiliaryMask) == 0)) { |
|||
++nameIndexIterator; |
|||
} |
|||
|
|||
ExpressionReturnType type = ExpressionReturnType::Undefined; |
|||
if ((nameIndexIterator->second & ExpressionManager::booleanMask) != 0) { |
|||
type = ExpressionReturnType::Bool; |
|||
} else if ((nameIndexIterator->second & ExpressionManager::integerMask) != 0) { |
|||
type = ExpressionReturnType::Int; |
|||
} else if ((nameIndexIterator->second & ExpressionManager::rationalMask) != 0) { |
|||
type = ExpressionReturnType::Double; |
|||
} |
|||
|
|||
if (nameIndexIterator != nameIndexIteratorEnd) { |
|||
currentElement = std::make_pair(Variable(manager, nameIndexIterator->second), type); |
|||
} |
|||
} |
|||
|
|||
ExpressionManager::ExpressionManager() : nameToIndexMapping(), variableTypeToCountMapping(), auxiliaryVariableTypeToCountMapping() { |
|||
variableTypeToCountMapping[static_cast<std::size_t>(storm::expressions::ExpressionReturnType::Bool)] = 0; |
|||
variableTypeToCountMapping[static_cast<std::size_t>(storm::expressions::ExpressionReturnType::Int)] = 0; |
|||
variableTypeToCountMapping[static_cast<std::size_t>(storm::expressions::ExpressionReturnType::Double)] = 0; |
|||
auxiliaryVariableTypeToCountMapping[static_cast<std::size_t>(storm::expressions::ExpressionReturnType::Bool)] = 0; |
|||
auxiliaryVariableTypeToCountMapping[static_cast<std::size_t>(storm::expressions::ExpressionReturnType::Int)] = 0; |
|||
auxiliaryVariableTypeToCountMapping[static_cast<std::size_t>(storm::expressions::ExpressionReturnType::Double)] = 0; |
|||
} |
|||
|
|||
Expression ExpressionManager::boolean(bool value) const { |
|||
return Expression(std::shared_ptr<BaseExpression const>(new BooleanLiteralExpression(*this, value))); |
|||
} |
|||
|
|||
Expression ExpressionManager::integer(int_fast64_t value) const { |
|||
return Expression(std::shared_ptr<BaseExpression const>(new IntegerLiteralExpression(*this, value))); |
|||
} |
|||
|
|||
Expression ExpressionManager::rational(double value) const { |
|||
return Expression(std::shared_ptr<BaseExpression const>(new DoubleLiteralExpression(*this, value))); |
|||
} |
|||
|
|||
bool ExpressionManager::operator==(ExpressionManager const& other) const { |
|||
return this == &other; |
|||
} |
|||
|
|||
bool ExpressionManager::isValidVariableName(std::string const& name) { |
|||
return name.size() < 2 || name.at(0) != '_' || name.at(1) != '_'; |
|||
} |
|||
|
|||
bool ExpressionManager::variableExists(std::string const& name) const { |
|||
auto nameIndexPair = nameToIndexMapping.find(name); |
|||
return nameIndexPair != nameToIndexMapping.end(); |
|||
} |
|||
|
|||
Variable ExpressionManager::declareVariable(std::string const& name, storm::expressions::ExpressionReturnType const& variableType) { |
|||
STORM_LOG_THROW(!variableExists(name), storm::exceptions::InvalidArgumentException, "Variable with name '" << name << "' already exists."); |
|||
return declareOrGetVariable(name, variableType); |
|||
} |
|||
|
|||
Variable ExpressionManager::declareAuxiliaryVariable(std::string const& name, storm::expressions::ExpressionReturnType const& variableType) { |
|||
STORM_LOG_THROW(!variableExists(name), storm::exceptions::InvalidArgumentException, "Variable with name '" << name << "' already exists."); |
|||
return declareOrGetAuxiliaryVariable(name, variableType); |
|||
} |
|||
|
|||
Variable ExpressionManager::declareOrGetVariable(std::string const& name, storm::expressions::ExpressionReturnType const& variableType) { |
|||
STORM_LOG_THROW(isValidVariableName(name), storm::exceptions::InvalidArgumentException, "Invalid variable name '" << name << "'."); |
|||
uint_fast64_t newIndex = 0; |
|||
switch (variableType) { |
|||
case ExpressionReturnType::Bool: |
|||
newIndex = variableTypeToCountMapping[static_cast<std::size_t>(ExpressionReturnType::Bool)]++ | booleanMask; |
|||
break; |
|||
case ExpressionReturnType::Int: |
|||
newIndex = variableTypeToCountMapping[static_cast<std::size_t>(ExpressionReturnType::Int)]++ | integerMask; |
|||
break; |
|||
case ExpressionReturnType::Double: |
|||
newIndex = variableTypeToCountMapping[static_cast<std::size_t>(ExpressionReturnType::Double)]++ | rationalMask; |
|||
break; |
|||
case ExpressionReturnType::Undefined: |
|||
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Illegal variable type."); |
|||
} |
|||
|
|||
nameToIndexMapping[name] = newIndex; |
|||
indexToNameMapping[newIndex] = name; |
|||
return Variable(*this, newIndex); |
|||
} |
|||
|
|||
Variable ExpressionManager::declareOrGetAuxiliaryVariable(std::string const& name, storm::expressions::ExpressionReturnType const& variableType) { |
|||
auto nameIndexPair = nameToIndexMapping.find(name); |
|||
if (nameIndexPair != nameToIndexMapping.end()) { |
|||
return Variable(*this, nameIndexPair->second); |
|||
} else { |
|||
STORM_LOG_THROW(isValidVariableName(name), storm::exceptions::InvalidArgumentException, "Invalid variable name '" << name << "'."); |
|||
uint_fast64_t newIndex = auxiliaryMask; |
|||
switch (variableType) { |
|||
case ExpressionReturnType::Bool: |
|||
newIndex |= auxiliaryVariableTypeToCountMapping[static_cast<std::size_t>(ExpressionReturnType::Bool)]++ | booleanMask; |
|||
break; |
|||
case ExpressionReturnType::Int: |
|||
newIndex |= auxiliaryVariableTypeToCountMapping[static_cast<std::size_t>(ExpressionReturnType::Int)]++ | integerMask; |
|||
break; |
|||
case ExpressionReturnType::Double: |
|||
newIndex |= auxiliaryVariableTypeToCountMapping[static_cast<std::size_t>(ExpressionReturnType::Double)]++ | rationalMask; |
|||
break; |
|||
case ExpressionReturnType::Undefined: |
|||
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Illegal variable type."); |
|||
} |
|||
|
|||
nameToIndexMapping[name] = newIndex; |
|||
indexToNameMapping[newIndex] = name; |
|||
return Variable(*this, newIndex); |
|||
} |
|||
} |
|||
|
|||
Variable ExpressionManager::getVariable(std::string const& name) const { |
|||
auto nameIndexPair = nameToIndexMapping.find(name); |
|||
STORM_LOG_THROW(nameIndexPair != nameToIndexMapping.end(), storm::exceptions::InvalidArgumentException, "Unknown variable '" << name << "'."); |
|||
return Variable(*this, nameIndexPair->second); |
|||
} |
|||
|
|||
Expression ExpressionManager::getVariableExpression(std::string const& name) const { |
|||
return Expression(getVariable(name)); |
|||
} |
|||
|
|||
Variable ExpressionManager::declareFreshVariable(storm::expressions::ExpressionReturnType const& variableType) { |
|||
std::string newName = "__x" + std::to_string(freshVariableCounter++); |
|||
return declareVariable(newName, variableType); |
|||
} |
|||
|
|||
Variable ExpressionManager::declareFreshAuxiliaryVariable(storm::expressions::ExpressionReturnType const& variableType) { |
|||
std::string newName = "__x" + std::to_string(freshVariableCounter++); |
|||
return declareAuxiliaryVariable(newName, variableType); |
|||
} |
|||
|
|||
uint_fast64_t ExpressionManager::getNumberOfVariables(storm::expressions::ExpressionReturnType const& variableType) const { |
|||
return variableTypeToCountMapping[static_cast<std::size_t>(variableType)]; |
|||
} |
|||
|
|||
uint_fast64_t ExpressionManager::getNumberOfVariables() const { |
|||
return numberOfVariables; |
|||
} |
|||
|
|||
uint_fast64_t ExpressionManager::getNumberOfBooleanVariables() const { |
|||
return getNumberOfVariables(storm::expressions::ExpressionReturnType::Bool); |
|||
} |
|||
|
|||
uint_fast64_t ExpressionManager::getNumberOfIntegerVariables() const { |
|||
return getNumberOfVariables(storm::expressions::ExpressionReturnType::Int); |
|||
} |
|||
|
|||
uint_fast64_t ExpressionManager::getNumberOfRationalVariables() const { |
|||
return getNumberOfVariables(storm::expressions::ExpressionReturnType::Double); |
|||
} |
|||
|
|||
uint_fast64_t ExpressionManager::getNumberOfAuxiliaryVariables(storm::expressions::ExpressionReturnType const& variableType) const { |
|||
return auxiliaryVariableTypeToCountMapping[static_cast<std::size_t>(variableType)]; |
|||
} |
|||
|
|||
uint_fast64_t ExpressionManager::getNumberOfAuxiliaryVariables() const { |
|||
return numberOfAuxiliaryVariables; |
|||
} |
|||
|
|||
uint_fast64_t ExpressionManager::getNumberOfAuxiliaryBooleanVariables() const { |
|||
return getNumberOfAuxiliaryVariables(storm::expressions::ExpressionReturnType::Bool); |
|||
} |
|||
|
|||
uint_fast64_t ExpressionManager::getNumberOfAuxiliaryIntegerVariables() const { |
|||
return getNumberOfAuxiliaryVariables(storm::expressions::ExpressionReturnType::Int); |
|||
} |
|||
|
|||
uint_fast64_t ExpressionManager::getNumberOfAuxiliaryRationalVariables() const { |
|||
return getNumberOfAuxiliaryVariables(storm::expressions::ExpressionReturnType::Double); |
|||
} |
|||
|
|||
std::string const& ExpressionManager::getVariableName(uint_fast64_t index) const { |
|||
auto indexTypeNamePair = indexToNameMapping.find(index); |
|||
STORM_LOG_THROW(indexTypeNamePair != indexToNameMapping.end(), storm::exceptions::InvalidArgumentException, "Unknown variable index '" << index << "'."); |
|||
return indexTypeNamePair->second; |
|||
} |
|||
|
|||
ExpressionReturnType ExpressionManager::getVariableType(uint_fast64_t index) const { |
|||
if ((index & booleanMask) != 0) { |
|||
return ExpressionReturnType::Bool; |
|||
} else if ((index & integerMask) != 0) { |
|||
return ExpressionReturnType::Int; |
|||
} else if ((index & rationalMask) != 0) { |
|||
return ExpressionReturnType::Double; |
|||
} else { |
|||
return ExpressionReturnType::Undefined; |
|||
} |
|||
} |
|||
|
|||
uint_fast64_t ExpressionManager::getOffset(uint_fast64_t index) const { |
|||
return index & offsetMask; |
|||
} |
|||
|
|||
ExpressionManager::const_iterator ExpressionManager::begin() const { |
|||
return ExpressionManager::const_iterator(*this, this->nameToIndexMapping.end(), this->nameToIndexMapping.begin(), const_iterator::VariableSelection::OnlyRegularVariables); |
|||
} |
|||
|
|||
ExpressionManager::const_iterator ExpressionManager::end() const { |
|||
return ExpressionManager::const_iterator(*this, this->nameToIndexMapping.end(), this->nameToIndexMapping.end(), const_iterator::VariableSelection::OnlyRegularVariables); |
|||
} |
|||
|
|||
} // namespace expressions
|
|||
} // namespace storm
|
|||
@ -0,0 +1,333 @@ |
|||
#ifndef STORM_STORAGE_EXPRESSIONS_EXPRESSIONMANAGER_H_ |
|||
#define STORM_STORAGE_EXPRESSIONS_EXPRESSIONMANAGER_H_ |
|||
|
|||
#include <cstdint> |
|||
#include <iterator> |
|||
#include <vector> |
|||
|
|||
#include "src/storage/expressions/Expression.h" |
|||
#include "src/utility/OsDetection.h" |
|||
|
|||
namespace storm { |
|||
namespace expressions { |
|||
// Forward-declare manager class for iterator class. |
|||
class ExpressionManager; |
|||
|
|||
class VariableIterator : public std::iterator<std::input_iterator_tag, std::pair<storm::expressions::Variable, storm::expressions::ExpressionReturnType> const> { |
|||
public: |
|||
enum class VariableSelection { OnlyRegularVariables, OnlyAuxiliaryVariables, AllVariables }; |
|||
|
|||
VariableIterator(ExpressionManager const& manager, std::unordered_map<std::string, uint_fast64_t>::const_iterator nameIndexIterator, std::unordered_map<std::string, uint_fast64_t>::const_iterator nameIndexIteratorEnd, VariableSelection const& selection); |
|||
VariableIterator(VariableIterator const& other) = default; |
|||
VariableIterator& operator=(VariableIterator const& other) = default; |
|||
|
|||
// Define the basic input iterator operations. |
|||
bool operator==(VariableIterator const& other); |
|||
bool operator!=(VariableIterator const& other); |
|||
value_type& operator*(); |
|||
VariableIterator& operator++(int); |
|||
VariableIterator& operator++(); |
|||
|
|||
private: |
|||
/*! |
|||
* Moves the current element to the next selected element or the end iterator if there is no such element. |
|||
* |
|||
* @param atLeastOneStep A flag indicating whether at least one step should be made. |
|||
*/ |
|||
void moveUntilNextSelectedElement(bool atLeastOneStep = true); |
|||
|
|||
// The manager responsible for the variable to iterate over. |
|||
ExpressionManager const& manager; |
|||
|
|||
// The underlying iterator that ranges over all names and the corresponding indices. |
|||
std::unordered_map<std::string, uint_fast64_t>::const_iterator nameIndexIterator; |
|||
|
|||
// The iterator indicating the end of the underlying iterator range. |
|||
std::unordered_map<std::string, uint_fast64_t>::const_iterator nameIndexIteratorEnd; |
|||
|
|||
// A field indicating which variables we are supposed to iterate over. |
|||
VariableSelection selection; |
|||
|
|||
// The current element that is shown to the outside upon dereferencing. |
|||
std::pair<storm::expressions::Variable, storm::expressions::ExpressionReturnType> currentElement; |
|||
}; |
|||
|
|||
/*! |
|||
* This class is responsible for managing a set of typed variables and all expressions using these variables. |
|||
*/ |
|||
class ExpressionManager { |
|||
public: |
|||
friend class VariableIterator; |
|||
|
|||
typedef VariableIterator const_iterator; |
|||
|
|||
/*! |
|||
* Creates a new manager that is unaware of any variables. |
|||
*/ |
|||
ExpressionManager(); |
|||
|
|||
// Explicitly delete copy construction/assignment, since the manager is supposed to be stored as a pointer |
|||
// of some sort. This is because the expression classes store a reference to the manager and it must |
|||
// therefore be guaranteed that they do not become invalid, because the manager has been copied. |
|||
ExpressionManager(ExpressionManager const& other) = delete; |
|||
ExpressionManager& operator=(ExpressionManager const& other) = delete; |
|||
#ifndef WINDOWS |
|||
// Create default instantiations for the move construction/assignment. |
|||
ExpressionManager(ExpressionManager&& other) = default; |
|||
ExpressionManager& operator=(ExpressionManager&& other) = default; |
|||
#endif |
|||
|
|||
/*! |
|||
* Creates an expression that characterizes the given boolean literal. |
|||
* |
|||
* @param value The value of the boolean literal. |
|||
* @return The resulting expression. |
|||
*/ |
|||
Expression boolean(bool value) const; |
|||
|
|||
/*! |
|||
* Creates an expression that characterizes the given integer literal. |
|||
* |
|||
* @param value The value of the integer literal. |
|||
* @return The resulting expression. |
|||
*/ |
|||
Expression integer(int_fast64_t value) const; |
|||
|
|||
/*! |
|||
* Creates an expression that characterizes the given rational literal. |
|||
* |
|||
* @param value The value of the rational literal. |
|||
* @return The resulting expression. |
|||
*/ |
|||
Expression rational(double value) const; |
|||
|
|||
/*! |
|||
* Compares the two expression managers for equality, which holds iff they are the very same object. |
|||
*/ |
|||
bool operator==(ExpressionManager const& other) const; |
|||
|
|||
/*! |
|||
* Declares a variable with a name that must not yet exist and its corresponding type. Note that the name |
|||
* must not start with two underscores since these variables are reserved for internal use only. |
|||
* |
|||
* @param name The name of the variable. |
|||
* @param variableType The type of the variable. |
|||
* @return The newly declared variable. |
|||
*/ |
|||
Variable declareVariable(std::string const& name, storm::expressions::ExpressionReturnType const& variableType); |
|||
|
|||
/*! |
|||
* Declares an auxiliary variable with a name that must not yet exist and its corresponding type. |
|||
* |
|||
* @param name The name of the variable. |
|||
* @param variableType The type of the variable. |
|||
* @return The newly declared variable. |
|||
*/ |
|||
Variable declareAuxiliaryVariable(std::string const& name, storm::expressions::ExpressionReturnType const& variableType); |
|||
|
|||
/*! |
|||
* Declares a variable with the given name if it does not yet exist. |
|||
* |
|||
* @param name The name of the variable to declare. |
|||
* @param variableType The type of the variable to declare. |
|||
* @return The variable. |
|||
*/ |
|||
Variable declareOrGetVariable(std::string const& name, storm::expressions::ExpressionReturnType const& variableType); |
|||
|
|||
/*! |
|||
* Declares a variable with the given name if it does not yet exist. |
|||
* |
|||
* @param name The name of the variable to declare. |
|||
* @param variableType The type of the variable to declare. |
|||
* @return The variable. |
|||
*/ |
|||
Variable declareOrGetAuxiliaryVariable(std::string const& name, storm::expressions::ExpressionReturnType const& variableType); |
|||
|
|||
/*! |
|||
* Retrieves the expression that represents the variable with the given name. |
|||
* |
|||
* @param name The name of the variable to retrieve. |
|||
*/ |
|||
Variable getVariable(std::string const& name) const; |
|||
|
|||
/*! |
|||
* Retrieves an expression that represents the variable with the given name. |
|||
* |
|||
* @param name The name of the variable |
|||
* @return An expression that represents the variable with the given name. |
|||
*/ |
|||
Expression getVariableExpression(std::string const& name) const; |
|||
|
|||
/*! |
|||
* Declares a variable with the given type whose name is guaranteed to be unique and not yet in use. |
|||
* |
|||
* @param variableType The type of the variable to declare. |
|||
* @return The variable. |
|||
*/ |
|||
Variable declareFreshVariable(storm::expressions::ExpressionReturnType const& variableType); |
|||
|
|||
/*! |
|||
* Declares an auxiliary variable with the given type whose name is guaranteed to be unique and not yet in use. |
|||
* |
|||
* @param variableType The type of the variable to declare. |
|||
* @return The variable. |
|||
*/ |
|||
Variable declareFreshAuxiliaryVariable(storm::expressions::ExpressionReturnType const& variableType); |
|||
|
|||
/*! |
|||
* Retrieves the number of variables with the given type. |
|||
* |
|||
* @return The number of variables with the given type. |
|||
*/ |
|||
uint_fast64_t getNumberOfVariables(storm::expressions::ExpressionReturnType const& variableType) const; |
|||
|
|||
/*! |
|||
* Retrieves the number of variables. |
|||
* |
|||
* @return The number of variables. |
|||
*/ |
|||
uint_fast64_t getNumberOfVariables() const; |
|||
|
|||
/*! |
|||
* Retrieves the number of boolean variables. |
|||
* |
|||
* @return The number of boolean variables. |
|||
*/ |
|||
uint_fast64_t getNumberOfBooleanVariables() const; |
|||
|
|||
/*! |
|||
* Retrieves the number of integer variables. |
|||
* |
|||
* @return The number of integer variables. |
|||
*/ |
|||
uint_fast64_t getNumberOfIntegerVariables() const; |
|||
|
|||
/*! |
|||
* Retrieves the number of rational variables. |
|||
* |
|||
* @return The number of rational variables. |
|||
*/ |
|||
uint_fast64_t getNumberOfRationalVariables() const; |
|||
|
|||
/*! |
|||
* Retrieves the number of auxiliary variables with the given type. |
|||
* |
|||
* @return The number of auxiliary variables with the given type. |
|||
*/ |
|||
uint_fast64_t getNumberOfAuxiliaryVariables(storm::expressions::ExpressionReturnType const& variableType) const; |
|||
|
|||
/*! |
|||
* Retrieves the number of auxiliary variables. |
|||
* |
|||
* @return The number of auxiliary variables. |
|||
*/ |
|||
uint_fast64_t getNumberOfAuxiliaryVariables() const; |
|||
|
|||
/*! |
|||
* Retrieves the number of boolean variables. |
|||
* |
|||
* @return The number of boolean variables. |
|||
*/ |
|||
uint_fast64_t getNumberOfAuxiliaryBooleanVariables() const; |
|||
|
|||
/*! |
|||
* Retrieves the number of integer variables. |
|||
* |
|||
* @return The number of integer variables. |
|||
*/ |
|||
uint_fast64_t getNumberOfAuxiliaryIntegerVariables() const; |
|||
|
|||
/*! |
|||
* Retrieves the number of rational variables. |
|||
* |
|||
* @return The number of rational variables. |
|||
*/ |
|||
uint_fast64_t getNumberOfAuxiliaryRationalVariables() const; |
|||
|
|||
/*! |
|||
* Retrieves the name of the variable with the given index. |
|||
* |
|||
* @param index The index of the variable whose name to retrieve. |
|||
* @return The name of the variable. |
|||
*/ |
|||
std::string const& getVariableName(uint_fast64_t index) const; |
|||
|
|||
/*! |
|||
* Retrieves the type of the variable with the given index. |
|||
* |
|||
* @param index The index of the variable whose name to retrieve. |
|||
* @return The type of the variable. |
|||
*/ |
|||
ExpressionReturnType getVariableType(uint_fast64_t index) const; |
|||
|
|||
/*! |
|||
* Retrieves the offset of the variable with the given index within the group of equally typed variables. |
|||
* |
|||
* @param index The index of the variable. |
|||
* @return The offset of the variable. |
|||
*/ |
|||
uint_fast64_t getOffset(uint_fast64_t index) const; |
|||
|
|||
/*! |
|||
* Retrieves an iterator to all variables managed by this manager. |
|||
* |
|||
* @return An iterator to all variables managed by this manager. |
|||
*/ |
|||
const_iterator begin() const; |
|||
|
|||
/*! |
|||
* Retrieves an iterator that points beyond the last variable managed by this manager. |
|||
* |
|||
* @return An iterator that points beyond the last variable managed by this manager. |
|||
*/ |
|||
const_iterator end() const; |
|||
|
|||
private: |
|||
/*! |
|||
* Checks whether the given variable name is valid. |
|||
* |
|||
* @param name The name to check. |
|||
* @return True iff the variable name is valid. |
|||
*/ |
|||
static bool isValidVariableName(std::string const& name); |
|||
|
|||
/*! |
|||
* Retrieves whether a variable with the given name exists. |
|||
* |
|||
* @param name The name of the variable to check for. |
|||
* @return True iff a variable with this name exists. |
|||
*/ |
|||
bool variableExists(std::string const& name) const; |
|||
|
|||
// A mapping from all variable names (auxiliary + normal) to their indices. |
|||
std::unordered_map<std::string, uint_fast64_t> nameToIndexMapping; |
|||
|
|||
// A mapping from all variable indices to their names. |
|||
std::unordered_map<uint_fast64_t, std::string> indexToNameMapping; |
|||
|
|||
// Store counts for variables. |
|||
std::vector<uint_fast64_t> variableTypeToCountMapping; |
|||
|
|||
// The number of declared variables. |
|||
uint_fast64_t numberOfVariables; |
|||
|
|||
// Store counts for auxiliary variables. |
|||
std::vector<uint_fast64_t> auxiliaryVariableTypeToCountMapping; |
|||
|
|||
// The number of declared auxiliary variables. |
|||
uint_fast64_t numberOfAuxiliaryVariables; |
|||
|
|||
// A counter used to create fresh variables. |
|||
uint_fast64_t freshVariableCounter; |
|||
|
|||
// A mask that can be used to query whether a variable is an auxiliary variable. |
|||
static const uint_fast64_t auxiliaryMask = (1 << 63); |
|||
static const uint_fast64_t booleanMask = (1 << 62); |
|||
static const uint_fast64_t integerMask = (1 << 61); |
|||
static const uint_fast64_t rationalMask = (1 << 60); |
|||
static const uint_fast64_t offsetMask = (1 << 60) - 1; |
|||
}; |
|||
} |
|||
} |
|||
|
|||
#endif /* STORM_STORAGE_EXPRESSIONS_EXPRESSIONMANAGER_H_ */ |
|||
@ -1,177 +0,0 @@ |
|||
#include "src/storage/expressions/SimpleValuation.h"
|
|||
|
|||
#include <set>
|
|||
|
|||
#include <boost/functional/hash.hpp>
|
|||
#include "src/utility/macros.h"
|
|||
#include "src/exceptions/InvalidArgumentException.h"
|
|||
#include "src/exceptions/InvalidAccessException.h"
|
|||
|
|||
namespace storm { |
|||
namespace expressions { |
|||
bool SimpleValuation::operator==(SimpleValuation const& other) const { |
|||
return this->identifierToValueMap == other.identifierToValueMap; |
|||
} |
|||
|
|||
void SimpleValuation::addBooleanIdentifier(std::string const& name, bool initialValue) { |
|||
STORM_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) { |
|||
STORM_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) { |
|||
STORM_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->identifierToValueMap[name] = value; |
|||
} |
|||
|
|||
void SimpleValuation::setIntegerValue(std::string const& name, int_fast64_t value) { |
|||
this->identifierToValueMap[name] = value; |
|||
} |
|||
|
|||
void SimpleValuation::setDoubleValue(std::string const& name, double value) { |
|||
this->identifierToValueMap[name] = value; |
|||
} |
|||
|
|||
void SimpleValuation::removeIdentifier(std::string const& name) { |
|||
auto nameValuePair = this->identifierToValueMap.find(name); |
|||
STORM_LOG_THROW(nameValuePair != this->identifierToValueMap.end(), storm::exceptions::InvalidArgumentException, "Deleting unknown identifier '" << name << "'."); |
|||
this->identifierToValueMap.erase(nameValuePair); |
|||
} |
|||
|
|||
ExpressionReturnType SimpleValuation::getIdentifierType(std::string const& name) const { |
|||
auto nameValuePair = this->identifierToValueMap.find(name); |
|||
STORM_LOG_THROW(nameValuePair != this->identifierToValueMap.end(), storm::exceptions::InvalidAccessException, "Access to unkown identifier '" << name << "'."); |
|||
if (nameValuePair->second.type() == typeid(bool)) { |
|||
return ExpressionReturnType::Bool; |
|||
} else if (nameValuePair->second.type() == typeid(int_fast64_t)) { |
|||
return ExpressionReturnType::Int; |
|||
} else { |
|||
return ExpressionReturnType::Double; |
|||
} |
|||
} |
|||
|
|||
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 nameValuePair = this->identifierToValueMap.find(name); |
|||
STORM_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 nameValuePair = this->identifierToValueMap.find(name); |
|||
STORM_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 nameValuePair = this->identifierToValueMap.find(name); |
|||
STORM_LOG_THROW(nameValuePair != this->identifierToValueMap.end(), storm::exceptions::InvalidAccessException, "Access to unkown identifier '" << name << "'."); |
|||
return boost::get<double>(nameValuePair->second); |
|||
} |
|||
|
|||
std::size_t SimpleValuation::getNumberOfIdentifiers() const { |
|||
return this->identifierToValueMap.size(); |
|||
} |
|||
|
|||
std::set<std::string> SimpleValuation::getIdentifiers() const { |
|||
std::set<std::string> result; |
|||
for (auto const& nameValuePair : this->identifierToValueMap) { |
|||
result.insert(nameValuePair.first); |
|||
} |
|||
return result; |
|||
} |
|||
|
|||
std::set<std::string> SimpleValuation::getBooleanIdentifiers() const { |
|||
std::set<std::string> result; |
|||
for (auto const& nameValuePair : this->identifierToValueMap) { |
|||
if (nameValuePair.second.type() == typeid(bool)) { |
|||
result.insert(nameValuePair.first); |
|||
} |
|||
} |
|||
return result; |
|||
} |
|||
|
|||
std::set<std::string> SimpleValuation::getIntegerIdentifiers() const { |
|||
std::set<std::string> result; |
|||
for (auto const& nameValuePair : this->identifierToValueMap) { |
|||
if (nameValuePair.second.type() == typeid(int_fast64_t)) { |
|||
result.insert(nameValuePair.first); |
|||
} |
|||
} |
|||
return result; |
|||
} |
|||
|
|||
std::set<std::string> SimpleValuation::getDoubleIdentifiers() const { |
|||
std::set<std::string> result; |
|||
for (auto const& nameValuePair : this->identifierToValueMap) { |
|||
if (nameValuePair.second.type() == typeid(double)) { |
|||
result.insert(nameValuePair.first); |
|||
} |
|||
} |
|||
return result; |
|||
} |
|||
|
|||
std::ostream& operator<<(std::ostream& stream, SimpleValuation const& valuation) { |
|||
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 << "}"; |
|||
|
|||
return stream; |
|||
} |
|||
|
|||
std::size_t SimpleValuationPointerHash::operator()(SimpleValuation* valuation) const { |
|||
size_t seed = 0; |
|||
for (auto const& nameValuePair : valuation->identifierToValueMap) { |
|||
boost::hash_combine(seed, nameValuePair.first); |
|||
boost::hash_combine(seed, nameValuePair.second); |
|||
} |
|||
return seed; |
|||
} |
|||
|
|||
bool SimpleValuationPointerCompare::operator()(SimpleValuation* valuation1, SimpleValuation* valuation2) const { |
|||
return *valuation1 == *valuation2; |
|||
} |
|||
|
|||
bool SimpleValuationPointerLess::operator()(SimpleValuation* valuation1, SimpleValuation* valuation2) const { |
|||
return valuation1->identifierToValueMap < valuation2->identifierToValueMap; |
|||
} |
|||
} |
|||
} |
|||
@ -1,148 +0,0 @@ |
|||
#ifndef STORM_STORAGE_EXPRESSIONS_SIMPLEVALUATION_H_ |
|||
#define STORM_STORAGE_EXPRESSIONS_SIMPLEVALUATION_H_ |
|||
|
|||
#include <boost/container/flat_map.hpp> |
|||
#include <boost/variant.hpp> |
|||
#include <iostream> |
|||
|
|||
#include "src/storage/expressions/Valuation.h" |
|||
#include "src/storage/expressions/ExpressionReturnType.h" |
|||
#include "src/utility/OsDetection.h" |
|||
|
|||
namespace storm { |
|||
namespace expressions { |
|||
class SimpleValuation : public Valuation { |
|||
public: |
|||
friend class SimpleValuationPointerHash; |
|||
friend class SimpleValuationPointerLess; |
|||
|
|||
// Instantiate some constructors and assignments with their default implementations. |
|||
SimpleValuation() = default; |
|||
SimpleValuation(SimpleValuation const&) = default; |
|||
SimpleValuation& operator=(SimpleValuation const&) = default; |
|||
#ifndef WINDOWS |
|||
SimpleValuation(SimpleValuation&&) = default; |
|||
SimpleValuation& operator=(SimpleValuation&&) = default; |
|||
#endif |
|||
virtual ~SimpleValuation() = default; |
|||
|
|||
/*! |
|||
* Compares two simple valuations wrt. equality. |
|||
*/ |
|||
bool operator==(SimpleValuation const& other) const; |
|||
|
|||
/*! |
|||
* Adds a boolean identifier with the given name. |
|||
* |
|||
* @param name The name of the boolean identifier to add. |
|||
* @param initialValue The initial value of the identifier. |
|||
*/ |
|||
void addBooleanIdentifier(std::string const& name, bool initialValue = false); |
|||
|
|||
/*! |
|||
* Adds a integer identifier with the given name. |
|||
* |
|||
* @param name The name of the integer identifier to add. |
|||
* @param initialValue The initial value of the identifier. |
|||
*/ |
|||
void addIntegerIdentifier(std::string const& name, int_fast64_t initialValue = 0); |
|||
|
|||
/*! |
|||
* Adds a double identifier with the given name. |
|||
* |
|||
* @param name The name of the double identifier to add. |
|||
* @param initialValue The initial value of the identifier. |
|||
*/ |
|||
void addDoubleIdentifier(std::string const& name, double initialValue = 0); |
|||
|
|||
/*! |
|||
* Sets the value of the boolean identifier with the given name to the given value. |
|||
* |
|||
* @param name The name of the boolean identifier whose value to set. |
|||
* @param value The new value of the boolean identifier. |
|||
*/ |
|||
void setBooleanValue(std::string const& name, bool value); |
|||
|
|||
/*! |
|||
* Sets the value of the integer identifier with the given name to the given value. |
|||
* |
|||
* @param name The name of the integer identifier whose value to set. |
|||
* @param value The new value of the integer identifier. |
|||
*/ |
|||
void setIntegerValue(std::string const& name, int_fast64_t value); |
|||
|
|||
/*! |
|||
* Sets the value of the double identifier with the given name to the given value. |
|||
* |
|||
* @param name The name of the double identifier whose value to set. |
|||
* @param value The new value of the double identifier. |
|||
*/ |
|||
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); |
|||
|
|||
/*! |
|||
* Retrieves the type of the identifier with the given name. |
|||
* |
|||
* @param name The name of the identifier whose type to retrieve. |
|||
* @return The type of the identifier with the given name. |
|||
*/ |
|||
ExpressionReturnType getIdentifierType(std::string const& name) const; |
|||
|
|||
// 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 std::size_t getNumberOfIdentifiers() const override; |
|||
virtual std::set<std::string> getIdentifiers() const override; |
|||
virtual std::set<std::string> getBooleanIdentifiers() const override; |
|||
virtual std::set<std::string> getIntegerIdentifiers() const override; |
|||
virtual std::set<std::string> getDoubleIdentifiers() 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; |
|||
|
|||
friend std::ostream& operator<<(std::ostream& stream, SimpleValuation const& valuation); |
|||
|
|||
private: |
|||
// A mapping of boolean identifiers to their local indices in the value container. |
|||
boost::container::flat_map<std::string, boost::variant<bool, int_fast64_t, double>> identifierToValueMap; |
|||
}; |
|||
|
|||
/*! |
|||
* A helper class that can pe used as the hash functor for data structures that need to hash a simple valuations |
|||
* given via pointers. |
|||
*/ |
|||
class SimpleValuationPointerHash { |
|||
public: |
|||
std::size_t operator()(SimpleValuation* valuation) const; |
|||
}; |
|||
|
|||
/*! |
|||
* A helper class that can be used as the comparison functor wrt. equality for data structures that need to |
|||
* store pointers to a simple valuations and need to compare the elements wrt. their content (rather than |
|||
* pointer equality). |
|||
*/ |
|||
class SimpleValuationPointerCompare { |
|||
public: |
|||
bool operator()(SimpleValuation* valuation1, SimpleValuation* valuation2) const; |
|||
}; |
|||
|
|||
/*! |
|||
* A helper class that can be used as the comparison functor wrt. "<" for data structures that need to |
|||
* store pointers to a simple valuations and need to compare the elements wrt. their content (rather than |
|||
* pointer equality). |
|||
*/ |
|||
class SimpleValuationPointerLess { |
|||
public: |
|||
bool operator()(SimpleValuation* valuation1, SimpleValuation* valuation2) const; |
|||
}; |
|||
} |
|||
} |
|||
|
|||
#endif /* STORM_STORAGE_EXPRESSIONS_SIMPLEVALUATION_H_ */ |
|||
@ -0,0 +1,82 @@ |
|||
#include "src/storage/expressions/Valuation.h"
|
|||
|
|||
#include <boost/functional/hash.hpp>
|
|||
|
|||
#include "src/storage/expressions/ExpressionManager.h"
|
|||
#include "src/storage/expressions/Variable.h"
|
|||
|
|||
namespace storm { |
|||
namespace expressions { |
|||
Valuation::Valuation(ExpressionManager const& manager) : manager(manager), booleanValues(nullptr), integerValues(nullptr), rationalValues(nullptr) { |
|||
if (manager.getNumberOfBooleanVariables() > 0) { |
|||
booleanValues = std::unique_ptr<std::vector<bool>>(new std::vector<bool>(manager.getNumberOfBooleanVariables())); |
|||
} |
|||
if (manager.getNumberOfIntegerVariables() > 0) { |
|||
integerValues = std::unique_ptr<std::vector<int_fast64_t>>(new std::vector<int_fast64_t>(manager.getNumberOfIntegerVariables())); |
|||
} |
|||
if (manager.getNumberOfRationalVariables() > 0) { |
|||
rationalValues = std::unique_ptr<std::vector<double>>(new std::vector<double>(manager.getNumberOfRationalVariables())); |
|||
} |
|||
} |
|||
|
|||
Valuation::Valuation(Valuation const& other) : manager(other.manager) { |
|||
if (other.booleanValues != nullptr) { |
|||
booleanValues = std::unique_ptr<std::vector<bool>>(new std::vector<bool>(*other.booleanValues)); |
|||
} |
|||
if (other.integerValues != nullptr) { |
|||
integerValues = std::unique_ptr<std::vector<int_fast64_t>>(new std::vector<int_fast64_t>(*other.integerValues)); |
|||
} |
|||
if (other.booleanValues != nullptr) { |
|||
rationalValues = std::unique_ptr<std::vector<double>>(new std::vector<double>(*other.rationalValues)); |
|||
} |
|||
} |
|||
|
|||
bool Valuation::operator==(Valuation const& other) const { |
|||
return manager == other.manager && booleanValues == other.booleanValues && integerValues == other.integerValues && rationalValues == other.rationalValues; |
|||
} |
|||
|
|||
bool Valuation::getBooleanValue(Variable const& booleanVariable) const { |
|||
return (*booleanValues)[booleanVariable.getOffset()]; |
|||
} |
|||
|
|||
int_fast64_t Valuation::getIntegerValue(Variable const& integerVariable) const { |
|||
return (*integerValues)[integerVariable.getOffset()]; |
|||
} |
|||
|
|||
double Valuation::getRationalValue(Variable const& rationalVariable) const { |
|||
return (*rationalValues)[rationalVariable.getOffset()]; |
|||
} |
|||
|
|||
void Valuation::setBooleanValue(Variable const& booleanVariable, bool value) { |
|||
(*booleanValues)[booleanVariable.getOffset()] = value; |
|||
} |
|||
|
|||
void Valuation::setIntegerValue(Variable const& integerVariable, int_fast64_t value) { |
|||
(*integerValues)[integerVariable.getOffset()] = value; |
|||
} |
|||
|
|||
void Valuation::setRationalValue(Variable const& rationalVariable, double value) { |
|||
(*rationalValues)[rationalVariable.getOffset()] = value; |
|||
} |
|||
|
|||
ExpressionManager const& Valuation::getManager() const { |
|||
return manager; |
|||
} |
|||
|
|||
std::size_t ValuationPointerHash::operator()(Valuation* valuation) const { |
|||
size_t seed = 0; |
|||
boost::hash_combine(seed, valuation->booleanValues); |
|||
boost::hash_combine(seed, valuation->integerValues); |
|||
boost::hash_combine(seed, valuation->rationalValues); |
|||
return seed; |
|||
} |
|||
|
|||
bool ValuationPointerCompare::operator()(Valuation* valuation1, Valuation* valuation2) const { |
|||
return *valuation1 == *valuation2; |
|||
} |
|||
|
|||
bool ValuationPointerLess::operator()(Valuation* valuation1, Valuation* valuation2) const { |
|||
return valuation1->booleanValues < valuation2->booleanValues || valuation1->integerValues < valuation2->integerValues || valuation1->rationalValues < valuation2->rationalValues; |
|||
} |
|||
} |
|||
} |
|||
@ -1,100 +1,138 @@ |
|||
#ifndef STORM_STORAGE_EXPRESSIONS_VALUATION_H_ |
|||
#define STORM_STORAGE_EXPRESSIONS_VALUATION_H_ |
|||
|
|||
#include <string> |
|||
#include <set> |
|||
#include <cstdint> |
|||
#include <vector> |
|||
|
|||
namespace storm { |
|||
namespace expressions { |
|||
class ExpressionManager; |
|||
class Variable; |
|||
|
|||
/*! |
|||
* The base class of all valuations where a valuation assigns a concrete value to all identifiers. This is, for |
|||
* example, used for evaluating expressions. |
|||
* A class to store a valuation of variables. This is, for example, used for evaluating expressions. |
|||
*/ |
|||
class Valuation { |
|||
public: |
|||
/*! |
|||
* Retrieves the boolean value of the identifier with the given name. |
|||
* |
|||
* @param name The name of the boolean identifier whose value to retrieve. |
|||
* @return The value of the boolean identifier. |
|||
*/ |
|||
virtual bool getBooleanValue(std::string const& name) const = 0; |
|||
friend class ValuationPointerHash; |
|||
friend class ValuationPointerLess; |
|||
|
|||
/*! |
|||
* Retrieves the integer value of the identifier with the given name. |
|||
* Creates a valuation of all non-auxiliary variables managed by the given manager. If the manager is |
|||
* modified in the sense that additional variables are added, all valuations over its variables are |
|||
* invalidated. |
|||
* |
|||
* @param name The name of the integer identifier whose value to retrieve. |
|||
* @return The value of the integer identifier. |
|||
* @param manager The manager of the variables. |
|||
*/ |
|||
virtual int_fast64_t getIntegerValue(std::string const& name) const = 0; |
|||
Valuation(ExpressionManager const& manager); |
|||
|
|||
/*! |
|||
* Retrieves the double value of the identifier with the given name. |
|||
* Deep-copies the valuation. |
|||
* |
|||
* @param name The name of the double identifier whose value to retrieve. |
|||
* @return The value of the double identifier. |
|||
* @param other The valuation to copy |
|||
*/ |
|||
virtual double getDoubleValue(std::string const& name) const = 0; |
|||
Valuation(Valuation const& other); |
|||
|
|||
/*! |
|||
* Retrieves whether there exists a boolean identifier with the given name in the valuation. |
|||
* Checks whether the two valuations are semantically equivalent. |
|||
* |
|||
* @param name The name of the boolean identifier to query. |
|||
* @return True iff the identifier exists and is of boolean type. |
|||
* @param other The valuation with which to compare. |
|||
* @return True iff the two valuations are semantically equivalent. |
|||
*/ |
|||
virtual bool containsBooleanIdentifier(std::string const& name) const = 0; |
|||
bool operator==(Valuation const& other) const; |
|||
|
|||
/*! |
|||
* Retrieves whether there exists a integer identifier with the given name in the valuation. |
|||
* Retrieves the value of the given boolean variable. |
|||
* |
|||
* @param name The name of the integer identifier to query. |
|||
* @return True iff the identifier exists and is of boolean type. |
|||
* @param booleanVariable The boolean variable whose value to retrieve. |
|||
* @return The value of the boolean variable. |
|||
*/ |
|||
virtual bool containsIntegerIdentifier(std::string const& name) const = 0; |
|||
bool getBooleanValue(Variable const& booleanVariable) const; |
|||
|
|||
/*! |
|||
* Retrieves whether there exists a double identifier with the given name in the valuation. |
|||
* Sets the value of the given boolean variable to the provided value. |
|||
* |
|||
* @param name The name of the double identifier to query. |
|||
* @return True iff the identifier exists and is of boolean type. |
|||
* @param booleanVariable The variable whose value to set. |
|||
* @param value The new value of the variable. |
|||
*/ |
|||
virtual bool containsDoubleIdentifier(std::string const& name) const = 0; |
|||
void setBooleanValue(Variable const& booleanVariable, bool value); |
|||
|
|||
/*! |
|||
* Retrieves the number of identifiers in this valuation. |
|||
* Retrieves the value of the given integer variable. |
|||
* |
|||
* @return The number of identifiers in this valuation. |
|||
* @param integerVariable The integer variable whose value to retrieve. |
|||
* @return The value of the integer variable. |
|||
*/ |
|||
virtual std::size_t getNumberOfIdentifiers() const = 0; |
|||
|
|||
int_fast64_t getIntegerValue(Variable const& integerVariable) const; |
|||
|
|||
/*! |
|||
* Retrieves the set of all identifiers contained in this valuation. |
|||
* Sets the value of the given boolean variable to the provided value. |
|||
* |
|||
* @return The set of all identifiers contained in this valuation. |
|||
* @param integerVariable The variable whose value to set. |
|||
* @param value The new value of the variable. |
|||
*/ |
|||
virtual std::set<std::string> getIdentifiers() const = 0; |
|||
void setIntegerValue(Variable const& integerVariable, int_fast64_t value); |
|||
|
|||
/*! |
|||
* Retrieves the set of boolean identifiers contained in this valuation. |
|||
* Retrieves the value of the given rational variable. |
|||
* |
|||
* @return The set of boolean identifiers contained in this valuation. |
|||
* @param rationalVariable The rational variable whose value to retrieve. |
|||
* @return The value of the rational variable. |
|||
*/ |
|||
virtual std::set<std::string> getBooleanIdentifiers() const = 0; |
|||
|
|||
double getRationalValue(Variable const& rationalVariable) const; |
|||
|
|||
/*! |
|||
* Retrieves the set of integer identifiers contained in this valuation. |
|||
* Sets the value of the given boolean variable to the provided value. |
|||
* |
|||
* @return The set of integer identifiers contained in this valuation. |
|||
* @param integerVariable The variable whose value to set. |
|||
* @param value The new value of the variable. |
|||
*/ |
|||
virtual std::set<std::string> getIntegerIdentifiers() const = 0; |
|||
|
|||
void setRationalValue(Variable const& rationalVariable, double value); |
|||
|
|||
/*! |
|||
* Retrieves the set of double identifiers contained in this valuation. |
|||
* Retrieves the manager responsible for the variables of this valuation. |
|||
* |
|||
* @return The set of double identifiers contained in this valuation. |
|||
* @return The manager. |
|||
*/ |
|||
virtual std::set<std::string> getDoubleIdentifiers() const = 0; |
|||
ExpressionManager const& getManager() const; |
|||
|
|||
private: |
|||
// The manager responsible for the variables of this valuation. |
|||
ExpressionManager const& manager; |
|||
|
|||
// Containers that store the values of the variables of the appropriate type. |
|||
std::unique_ptr<std::vector<bool>> booleanValues; |
|||
std::unique_ptr<std::vector<int_fast64_t>> integerValues; |
|||
std::unique_ptr<std::vector<double>> rationalValues; |
|||
}; |
|||
|
|||
/*! |
|||
* A helper class that can pe used as the hash functor for data structures that need to hash valuations given |
|||
* via pointers. |
|||
*/ |
|||
class ValuationPointerHash { |
|||
public: |
|||
std::size_t operator()(Valuation* valuation) const; |
|||
}; |
|||
|
|||
/*! |
|||
* A helper class that can be used as the comparison functor wrt. equality for data structures that need to |
|||
* store pointers to valuations and need to compare the elements wrt. their content (rather than pointer |
|||
* equality). |
|||
*/ |
|||
class ValuationPointerCompare { |
|||
public: |
|||
bool operator()(Valuation* valuation1, Valuation* valuation2) const; |
|||
}; |
|||
|
|||
/*! |
|||
* A helper class that can be used as the comparison functor wrt. "<" for data structures that need to |
|||
* store pointers to valuations and need to compare the elements wrt. their content (rather than pointer |
|||
* equality). |
|||
*/ |
|||
class ValuationPointerLess { |
|||
public: |
|||
bool operator()(Valuation* valuation1, Valuation* valuation2) const; |
|||
}; |
|||
} |
|||
} |
|||
|
|||
@ -0,0 +1,54 @@ |
|||
#include "src/storage/expressions/Variable.h"
|
|||
#include "src/storage/expressions/ExpressionManager.h"
|
|||
|
|||
namespace storm { |
|||
namespace expressions { |
|||
Variable::Variable(ExpressionManager const& manager, uint_fast64_t index) : manager(manager), index(index) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
bool Variable::operator==(Variable const& other) const { |
|||
return manager == other.manager && index == other.index; |
|||
} |
|||
|
|||
storm::expressions::Expression Variable::getExpression() const { |
|||
return storm::expressions::Expression(*this); |
|||
} |
|||
|
|||
uint_fast64_t Variable::getIndex() const { |
|||
return index; |
|||
} |
|||
|
|||
uint_fast64_t Variable::getOffset() const { |
|||
return manager.getOffset(index); |
|||
} |
|||
|
|||
std::string const& Variable::getName() const { |
|||
return manager.getVariableName(index); |
|||
} |
|||
|
|||
ExpressionReturnType Variable::getType() const { |
|||
return manager.getVariableType(index); |
|||
} |
|||
|
|||
ExpressionManager const& Variable::getManager() const { |
|||
return manager; |
|||
} |
|||
|
|||
bool Variable::hasBooleanType() const { |
|||
return this->getType() == ExpressionReturnType::Bool; |
|||
} |
|||
|
|||
bool Variable::hasIntegralType() const { |
|||
return this->getType() == ExpressionReturnType::Int; |
|||
} |
|||
|
|||
bool Variable::hasRationalType() const { |
|||
return this->getType() == ExpressionReturnType::Double; |
|||
} |
|||
|
|||
bool Variable::hasNumericType() const { |
|||
return this->getType() == ExpressionReturnType::Int || this->getType() == ExpressionReturnType::Double; |
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,138 @@ |
|||
#ifndef STORM_STORAGE_EXPRESSIONS_VARIABLE_H_ |
|||
#define STORM_STORAGE_EXPRESSIONS_VARIABLE_H_ |
|||
|
|||
#include <cstdint> |
|||
#include <memory> |
|||
|
|||
#include "src/utility/OsDetection.h" |
|||
#include "src/storage/expressions/ExpressionReturnType.h" |
|||
#include "src/storage/expressions/Expression.h" |
|||
|
|||
namespace storm { |
|||
namespace expressions { |
|||
class ExpressionManager; |
|||
|
|||
// This class captures a simple variable. |
|||
class Variable { |
|||
public: |
|||
/*! |
|||
* Constructs a variable with the given index and type. |
|||
* |
|||
* @param manager The manager that is responsible for this variable. |
|||
* @param index The (unique) index of the variable. |
|||
*/ |
|||
Variable(ExpressionManager const& manager, uint_fast64_t index); |
|||
|
|||
// Default-instantiate some copy/move construction/assignment. |
|||
Variable(Variable const& other) = default; |
|||
Variable& operator=(Variable const& other) = default; |
|||
#ifndef WINDOWS |
|||
Variable(Variable&& other) = default; |
|||
Variable& operator=(Variable&& other) = default; |
|||
#endif |
|||
|
|||
/*! |
|||
* Checks the two variables for equality. |
|||
* |
|||
* @param other The variable to compare with. |
|||
* @return True iff the two variables are the same. |
|||
*/ |
|||
bool operator==(Variable const& other) const; |
|||
|
|||
/*! |
|||
* Retrieves the name of the variable. |
|||
* |
|||
* @return name The name of the variable. |
|||
*/ |
|||
std::string const& getName() const; |
|||
|
|||
/*! |
|||
* Retrieves the type of the variable. |
|||
* |
|||
* @return The type of the variable. |
|||
*/ |
|||
ExpressionReturnType getType() const; |
|||
|
|||
/*! |
|||
* Retrieves an expression that represents the variable. |
|||
* |
|||
* @return An expression that represents the varible. |
|||
*/ |
|||
storm::expressions::Expression getExpression() const; |
|||
|
|||
/*! |
|||
* Retrieves the manager responsible for this variable. |
|||
*/ |
|||
ExpressionManager const& getManager() const; |
|||
|
|||
/*! |
|||
* Retrieves the index of the variable. |
|||
* |
|||
* @return The index of the variable. |
|||
*/ |
|||
uint_fast64_t getIndex() const; |
|||
|
|||
/*! |
|||
* Retrieves the offset of the variable in the group of all equally typed variables. |
|||
* |
|||
* @return The offset of the variable. |
|||
*/ |
|||
uint_fast64_t getOffset() const; |
|||
|
|||
/*! |
|||
* Checks whether the variable is of boolean type. |
|||
* |
|||
* @return True iff the variable if of boolean type. |
|||
*/ |
|||
bool hasBooleanType() const; |
|||
|
|||
/*! |
|||
* Checks whether the variable is of integral type. |
|||
* |
|||
* @return True iff the variable if of integral type. |
|||
*/ |
|||
bool hasIntegralType() const; |
|||
|
|||
/*! |
|||
* Checks whether the variable is of rational type. |
|||
* |
|||
* @return True iff the variable if of rational type. |
|||
*/ |
|||
bool hasRationalType() const; |
|||
|
|||
/*! |
|||
* Checks whether the variable is of boolean type. |
|||
* |
|||
* @return True iff the variable if of boolean type. |
|||
*/ |
|||
bool hasNumericType() const; |
|||
|
|||
private: |
|||
// The manager that is responsible for this variable. |
|||
ExpressionManager const& manager; |
|||
|
|||
// The index of the variable. |
|||
uint_fast64_t index; |
|||
}; |
|||
} |
|||
} |
|||
|
|||
namespace std { |
|||
// Provide a hashing operator, so we can put variables in unordered collections. |
|||
template <> |
|||
struct hash<storm::expressions::Variable> { |
|||
std::size_t operator()(storm::expressions::Variable const& variable) const { |
|||
return std::hash<uint_fast64_t>()(variable.getIndex()); |
|||
} |
|||
}; |
|||
|
|||
// Provide a less operator, so we can put variables in ordered collections. |
|||
template <> |
|||
struct less<storm::expressions::Variable> { |
|||
std::size_t operator()(storm::expressions::Variable const& variable1, storm::expressions::Variable const& variable2) const { |
|||
return variable1.getIndex() < variable2.getIndex(); |
|||
} |
|||
}; |
|||
} |
|||
|
|||
#endif /* STORM_STORAGE_EXPRESSIONS_VARIABLE_H_ */ |
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue