diff --git a/CMakeLists.txt b/CMakeLists.txt index 09eef57a9..7913af7d7 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -251,6 +251,7 @@ file(GLOB_RECURSE STORM_SETTINGS_FILES ${PROJECT_SOURCE_DIR}/src/settings/*.h ${ file(GLOB_RECURSE STORM_SOLVER_FILES ${PROJECT_SOURCE_DIR}/src/solver/*.h ${PROJECT_SOURCE_DIR}/src/solver/*.cpp) file(GLOB STORM_STORAGE_FILES ${PROJECT_SOURCE_DIR}/src/storage/*.h ${PROJECT_SOURCE_DIR}/src/storage/*.cpp) file(GLOB_RECURSE STORM_STORAGE_DD_FILES ${PROJECT_SOURCE_DIR}/src/storage/dd/*.h ${PROJECT_SOURCE_DIR}/src/storage/dd/*.cpp) +file(GLOB_RECURSE STORM_STORAGE_EXPRESSIONS_FILES ${PROJECT_SOURCE_DIR}/src/storage/expressions/*.h ${PROJECT_SOURCE_DIR}/src/storage/expressions/*.cpp) file(GLOB_RECURSE STORM_UTILITY_FILES ${PROJECT_SOURCE_DIR}/src/utility/*.h ${PROJECT_SOURCE_DIR}/src/utility/*.cpp) file(GLOB STORM_IR_FILES ${PROJECT_SOURCE_DIR}/src/ir/*.h ${PROJECT_SOURCE_DIR}/src/ir/*.cpp) file(GLOB_RECURSE STORM_IR_EXPRESSIONS_FILES ${PROJECT_SOURCE_DIR}/src/ir/expressions/*.h ${PROJECT_SOURCE_DIR}/src/ir/expressions/*.cpp) @@ -284,6 +285,7 @@ source_group(settings FILES ${STORM_SETTINGS_FILES}) source_group(solver FILES ${STORM_SOLVER_FILES}) source_group(storage FILES ${STORM_STORAGE_FILES}) source_group(storage\\dd FILES ${STORM_STORAGE_DD_FILES}) +source_group(storage\\expressions FILES ${STORM_STORAGE_EXPRESSIONS_FILES}) source_group(utility FILES ${STORM_UTILITY_FILES}) source_group(functional-test FILES ${STORM_FUNCTIONAL_TEST_FILES}) source_group(performance-test FILES ${STORM_PERFORMANCE_TEST_FILES}) diff --git a/src/storage/expressions/BaseExpression.h b/src/storage/expressions/BaseExpression.h new file mode 100644 index 000000000..85b521726 --- /dev/null +++ b/src/storage/expressions/BaseExpression.h @@ -0,0 +1,26 @@ +#ifndef STORM_STORAGE_EXPRESSIONS_BASEEXPRESSION_H_ +#define STORM_STORAGE_EXPRESSIONS_BASEEXPRESSION_H_ + +#include "src/storage/expressions/Valuation.h" + +namespace storm { + namespace expressions { + class BaseExpression { + public: + /*! + * Each node in an expression tree has a uniquely defined type from this enum. + */ + enum ReturnType {undefined, bool_, int_, double_}; + + std::unique_ptr substitute() const = 0; + + virtual int_fast64_t evaluateAsInt(Evaluation const& evaluation) const = 0; + + virtual bool evaluateAsBool(Evaluation const& evaluation) const = 0; + + virtual double evaluateAsDouble(Evaluation const& evaluation) const = 0; + }; + } +} + +#endif /* STORM_STORAGE_EXPRESSIONS_BASEEXPRESSION_H_ */ \ No newline at end of file diff --git a/src/storage/expressions/Expression.cpp b/src/storage/expressions/Expression.cpp new file mode 100644 index 000000000..335fa3ca7 --- /dev/null +++ b/src/storage/expressions/Expression.cpp @@ -0,0 +1,13 @@ +#include "src/storage/expressions/Expression.h" + +namespace storm { + namespace expressions { + virtual Expression Expression::operator+(Expression const& other) { + return Expression(this->getBaseExpression() + other.getBaseExpression()); + } + + BaseExpression const& getBaseExpression() const { + return *this->expressionPtr; + } + } +} diff --git a/src/storage/expressions/Expression.h b/src/storage/expressions/Expression.h new file mode 100644 index 000000000..c44219736 --- /dev/null +++ b/src/storage/expressions/Expression.h @@ -0,0 +1,42 @@ +#ifndef STORM_STORAGE_EXPRESSIONS_EXPRESSION_H_ +#define STORM_STORAGE_EXPRESSIONS_EXPRESSION_H_ + +namespace storm { + namespace expressions { + class Expression { + Expression() = default; + + // Static factory methods to create atomic expression parts. + + // Virtual operator overloading. + virtual Expression operator+(Expression const& other); + + /*! + * Substitutes all occurrences of identifiers according to the given substitution. Note that this + * substitution is done simultaneously, i.e., identifiers appearing in the expressions that were "plugged + * in" are not substituted. + * + * @param substitutionFilter A function that returns true iff the given identifier is supposed to be + * substituted. + * @param substitution A substitution that returns for each identifier an expression that is supposed to + * replace the identifier. + * @return An expression in which all identifiers + */ + Expression substitute(std::function const& substitution) const; + + private: + /*! + * Retrieves the base expression underlying this expression object. Note that prior to calling this, the + * expression object must be properly initialized. + * + * @return A reference to the underlying base expression. + */ + BaseExpression const& getBaseExpression() const; + + // A pointer to the underlying base expression. + std::unique_ptr expressionPtr; + }; + } +} + +#endif /* STORM_STORAGE_EXPRESSIONS_EXPRESSION_H_ */ \ No newline at end of file diff --git a/src/storage/expressions/SimpleValuation.cpp b/src/storage/expressions/SimpleValuation.cpp new file mode 100644 index 000000000..20c9f9f2f --- /dev/null +++ b/src/storage/expressions/SimpleValuation.cpp @@ -0,0 +1,29 @@ +#include "src/storage/expressions/SimpleValuation.h" + +namespace storm { + namespace expressions { + SimpleValuation::SimpleValuation(std::size_t booleanVariableCount, std::size_t integerVariableCount, std::size_t doubleVariableCount) : identifierToIndexMap(), booleanValues(booleanVariableCount), integerValues(integerVariableCount), doubleValues(doubleVariableCount) { + // Intentionally left empty. + } + + SimpleValuation::SimpleValuation(std::shared_ptr> identifierToIndexMap, std::vector booleanValues, std::vector integerValues, std::vector doubleValues) : identifierToIndexMap(identifierToIndexMap), booleanValues(booleanValues), integerValues(integerValues), doubleValues(doubleValues) { + // Intentionally left empty. + } + + void SimpleValuation::setIdentifierIndex(std::string const& name, uint_fast64_t index) { + (*this->identifierToIndexMap)[name] = index; + } + + bool SimpleValuation::getBooleanValue(std::string const& name) const { + return false; + } + + int_fast64_t SimpleValuation::getIntegerValue(std::string const& name) const { + return 0; + } + + double SimpleValuation::getDoubleValue(std::string const& name) const { + return 0.0; + } + } +} \ No newline at end of file diff --git a/src/storage/expressions/SimpleValuation.h b/src/storage/expressions/SimpleValuation.h new file mode 100644 index 000000000..fd7d3c8b0 --- /dev/null +++ b/src/storage/expressions/SimpleValuation.h @@ -0,0 +1,40 @@ +#ifndef STORM_STORAGE_EXPRESSIONS_SIMPLEVALUATION_H_ +#define STORM_STORAGE_EXPRESSIONS_SIMPLEVALUATION_H_ + +#include +#include +#include +#include + +#include "src/storage/expressions/Valuation.h" + +namespace storm { + namespace expressions { + class SimpleValuation : public Valuation { + public: + SimpleValuation(std::size_t booleanVariableCount, std::size_t integerVariableCount, std::size_t doubleVariableCount); + + SimpleValuation(std::shared_ptr> identifierToIndexMap, std::vector booleanValues, std::vector integerValues, std::vector doubleValues); + + SimpleValuation() = default; + SimpleValuation(SimpleValuation const&) = default; + SimpleValuation(SimpleValuation&&) = default; + SimpleValuation& operator=(SimpleValuation const&) = default; + SimpleValuation& operator=(SimpleValuation&&) = default; + + void setIdentifierIndex(std::string const& name, uint_fast64_t index); + + 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; + + private: + std::shared_ptr> identifierToIndexMap; + std::vector booleanValues; + std::vector integerValues; + std::vector doubleValues; + }; + } +} + +#endif /* STORM_STORAGE_EXPRESSIONS_SIMPLEVALUATION_H_ */ \ No newline at end of file diff --git a/src/storage/expressions/Valuation.h b/src/storage/expressions/Valuation.h new file mode 100644 index 000000000..c2d0b01cb --- /dev/null +++ b/src/storage/expressions/Valuation.h @@ -0,0 +1,15 @@ +#ifndef STORM_STORAGE_EXPRESSIONS_VALUATION_H_ +#define STORM_STORAGE_EXPRESSIONS_VALUATION_H_ + +namespace storm { + namespace expressions { + class Valuation { + public: + virtual bool getBooleanValue(std::string const& name) const = 0; + virtual int_fast64_t getIntegerValue(std::string const& name) const = 0; + virtual double getDoubleValue(std::string const& name) const = 0; + }; + } +} + +#endif /* STORM_STORAGE_EXPRESSIONS_VALUATION_H_ */ \ No newline at end of file diff --git a/test/functional/storage/ExpressionTest.cpp b/test/functional/storage/ExpressionTest.cpp new file mode 100644 index 000000000..9d9307bea --- /dev/null +++ b/test/functional/storage/ExpressionTest.cpp @@ -0,0 +1,9 @@ +#include "gtest/gtest.h" + +#include + +#include "src/storage/expressions/SimpleValuation.h" + +TEST(Expression, SimpleValuationTest) { + ASSERT_NO_THROW(storm::expressions::SimpleValuation evaluation(1, 1, 1)); +} \ No newline at end of file