diff --git a/src/solver/MathsatSmtSolver.cpp b/src/solver/MathsatSmtSolver.cpp index edd1e3da0..4d85b851d 100644 --- a/src/solver/MathsatSmtSolver.cpp +++ b/src/solver/MathsatSmtSolver.cpp @@ -219,7 +219,7 @@ namespace storm { #endif } - storm::expressions::Valuation MathsatSmtSolver::getModelAsValuation() + storm::expressions::SimpleValuation MathsatSmtSolver::getModelAsValuation() { #ifdef STORM_HAVE_MSAT STORM_LOG_THROW(this->lastResult == SmtSolver::CheckResult::Sat, storm::exceptions::InvalidStateException, "Unable to create model for formula that was not determined to be satisfiable."); @@ -239,8 +239,8 @@ namespace storm { } #ifdef STORM_HAVE_MSAT - storm::expressions::Valuation MathsatSmtSolver::convertMathsatModelToValuation() { - storm::expressions::Valuation stormModel(this->getManager()); + storm::expressions::SimpleValuation MathsatSmtSolver::convertMathsatModelToValuation() { + storm::expressions::SimpleValuation stormModel(this->getManager()); msat_model_iterator modelIterator = msat_create_model_iterator(env); STORM_LOG_THROW(!MSAT_ERROR_MODEL_ITERATOR(modelIterator), storm::exceptions::UnexpectedException, "MathSat returned an illegal model iterator."); @@ -267,11 +267,11 @@ namespace storm { } #endif - std::vector MathsatSmtSolver::allSat(std::vector const& important) + std::vector MathsatSmtSolver::allSat(std::vector const& important) { #ifdef STORM_HAVE_MSAT - std::vector valuations; - this->allSat(important, [&valuations](storm::expressions::Valuation const& valuation) -> bool { valuations.push_back(valuation); return true; }); + std::vector valuations; + this->allSat(important, [&valuations](storm::expressions::SimpleValuation const& valuation) -> bool { valuations.push_back(valuation); return true; }); return valuations; #else STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support."); @@ -282,14 +282,14 @@ namespace storm { #ifdef STORM_HAVE_MSAT class AllsatValuationCallbackUserData { public: - AllsatValuationCallbackUserData(storm::expressions::ExpressionManager const& manager, storm::adapters::MathsatExpressionAdapter& adapter, msat_env& env, std::function const& callback) : manager(manager), adapter(adapter), env(env), callback(callback) { + AllsatValuationCallbackUserData(storm::expressions::ExpressionManager const& manager, storm::adapters::MathsatExpressionAdapter& adapter, msat_env& env, std::function const& callback) : manager(manager), adapter(adapter), env(env), callback(callback) { // Intentionally left empty. } static int allsatValuationsCallback(msat_term* model, int size, void* user_data) { AllsatValuationCallbackUserData* user = reinterpret_cast(user_data); - storm::expressions::Valuation valuation(user->manager); + storm::expressions::SimpleValuation valuation(user->manager); for (int i = 0; i < size; ++i) { bool currentTermValue = true; msat_term currentTerm = model[i]; @@ -319,7 +319,7 @@ namespace storm { msat_env& env; // The function that is to be called when the MathSAT model has been translated to a valuation. - std::function const& callback; + std::function const& callback; }; class AllsatModelReferenceCallbackUserData { @@ -354,7 +354,7 @@ namespace storm { #endif - uint_fast64_t MathsatSmtSolver::allSat(std::vector const& important, std::function const& callback) { + uint_fast64_t MathsatSmtSolver::allSat(std::vector const& important, std::function const& callback) { #ifdef STORM_HAVE_MSAT // Create a backtracking point, because MathSAT will modify the assertions stack during its AllSat procedure. this->push(); diff --git a/src/solver/MathsatSmtSolver.h b/src/solver/MathsatSmtSolver.h index f3dd1f84b..badca77a8 100644 --- a/src/solver/MathsatSmtSolver.h +++ b/src/solver/MathsatSmtSolver.h @@ -81,13 +81,13 @@ namespace storm { virtual CheckResult checkWithAssumptions(std::initializer_list const& assumptions) override; - virtual storm::expressions::Valuation getModelAsValuation() override; + virtual storm::expressions::SimpleValuation getModelAsValuation() override; virtual std::shared_ptr getModel() override; - virtual std::vector allSat(std::vector const& important) override; + virtual std::vector allSat(std::vector const& important) override; - virtual uint_fast64_t allSat(std::vector const& important, std::function const& callback) override; + virtual uint_fast64_t allSat(std::vector const& important, std::function const& callback) override; virtual uint_fast64_t allSat(std::vector const& important, std::function const& callback) override; @@ -98,7 +98,7 @@ namespace storm { virtual storm::expressions::Expression getInterpolant(std::vector const& groupsA) override; private: - storm::expressions::Valuation convertMathsatModelToValuation(); + storm::expressions::SimpleValuation convertMathsatModelToValuation(); #ifdef STORM_HAVE_MSAT // The MathSAT environment. diff --git a/src/solver/SmtSolver.cpp b/src/solver/SmtSolver.cpp index 0de0d48ea..d1f2536d6 100644 --- a/src/solver/SmtSolver.cpp +++ b/src/solver/SmtSolver.cpp @@ -40,7 +40,7 @@ namespace storm { } } - storm::expressions::Valuation SmtSolver::getModelAsValuation() { + storm::expressions::SimpleValuation SmtSolver::getModelAsValuation() { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This solver does not support model generation."); } @@ -48,11 +48,11 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This solver does not support model generation."); } - std::vector SmtSolver::allSat(std::vector const& important) { + std::vector SmtSolver::allSat(std::vector const& important) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This solver does not support model generation."); } - uint_fast64_t SmtSolver::allSat(std::vector const& important, std::function const& callback) { + uint_fast64_t SmtSolver::allSat(std::vector const& important, std::function const& callback) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This solver does not support model generation."); } diff --git a/src/solver/SmtSolver.h b/src/solver/SmtSolver.h index 389f03d8f..7425e8187 100644 --- a/src/solver/SmtSolver.h +++ b/src/solver/SmtSolver.h @@ -4,7 +4,7 @@ #include #include "src/storage/expressions/Expressions.h" -#include "src/storage/expressions/Valuation.h" +#include "src/storage/expressions/SimpleValuation.h" #include "src/storage/expressions/ExpressionManager.h" #include @@ -158,7 +158,7 @@ namespace storm { * * @return A valuation that holds the values of the variables in the current model. */ - virtual storm::expressions::Valuation getModelAsValuation(); + virtual storm::expressions::SimpleValuation getModelAsValuation(); /*! * If the last call to check() or checkWithAssumptions() returned Sat, this method retrieves a model that @@ -181,7 +181,7 @@ namespace storm { * * @returns the set of all valuations of the important atoms, such that the currently asserted formulas are satisfiable */ - virtual std::vector allSat(std::vector const& important); + virtual std::vector allSat(std::vector const& important); /*! * Performs AllSat over the (provided) important atoms. That is, this function determines all models of the @@ -194,7 +194,7 @@ namespace storm { * * @return The number of models of the important atoms that where found. */ - virtual uint_fast64_t allSat(std::vector const& important, std::function const& callback); + virtual uint_fast64_t allSat(std::vector const& important, std::function const& callback); /*! * Performs AllSat over the (provided) important atoms. That is, this function determines all models of the diff --git a/src/solver/Z3SmtSolver.cpp b/src/solver/Z3SmtSolver.cpp index 24cea0c53..6527ed348 100644 --- a/src/solver/Z3SmtSolver.cpp +++ b/src/solver/Z3SmtSolver.cpp @@ -180,7 +180,7 @@ namespace storm { #endif } - storm::expressions::Valuation Z3SmtSolver::getModelAsValuation() + storm::expressions::SimpleValuation Z3SmtSolver::getModelAsValuation() { #ifdef STORM_HAVE_Z3 STORM_LOG_THROW(this->lastResult == SmtSolver::CheckResult::Sat, storm::exceptions::InvalidStateException, "Unable to create model for formula that was not determined to be satisfiable."); @@ -200,8 +200,8 @@ namespace storm { } #ifdef STORM_HAVE_Z3 - storm::expressions::Valuation Z3SmtSolver::convertZ3ModelToValuation(z3::model const& model) { - storm::expressions::Valuation stormModel(this->getManager()); + storm::expressions::SimpleValuation Z3SmtSolver::convertZ3ModelToValuation(z3::model const& model) { + storm::expressions::SimpleValuation stormModel(this->getManager()); for (unsigned i = 0; i < model.num_consts(); ++i) { z3::func_decl variableI = model.get_const_decl(i); @@ -223,18 +223,18 @@ namespace storm { } #endif - std::vector Z3SmtSolver::allSat(std::vector const& important) + std::vector Z3SmtSolver::allSat(std::vector const& important) { #ifdef STORM_HAVE_Z3 - std::vector valuations; - this->allSat(important, [&valuations](storm::expressions::Valuation const& valuation) -> bool { valuations.push_back(valuation); return true; }); + std::vector valuations; + this->allSat(important, [&valuations](storm::expressions::SimpleValuation const& valuation) -> bool { valuations.push_back(valuation); return true; }); return valuations; #else STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support."); #endif } - uint_fast64_t Z3SmtSolver::allSat(std::vector const& important, std::function const& callback) { + uint_fast64_t Z3SmtSolver::allSat(std::vector const& important, std::function const& callback) { #ifdef STORM_HAVE_Z3 for (storm::expressions::Variable const& variable : important) { STORM_LOG_THROW(variable.hasBooleanType(), storm::exceptions::InvalidArgumentException, "The important atoms for AllSat must be boolean variables."); @@ -252,7 +252,7 @@ namespace storm { z3::model model = this->solver->get_model(); z3::expr modelExpr = this->context->bool_val(true); - storm::expressions::Valuation valuation(this->getManager()); + storm::expressions::SimpleValuation valuation(this->getManager()); for (storm::expressions::Variable const& importantAtom : important) { z3::expr z3ImportantAtom = this->expressionAdapter->translateExpression(importantAtom.getExpression()); @@ -294,7 +294,7 @@ namespace storm { z3::model model = this->solver->get_model(); z3::expr modelExpr = this->context->bool_val(true); - storm::expressions::Valuation valuation(this->getManager()); + storm::expressions::SimpleValuation valuation(this->getManager()); for (storm::expressions::Variable const& importantAtom : important) { z3::expr z3ImportantAtom = this->expressionAdapter->translateExpression(importantAtom.getExpression()); diff --git a/src/solver/Z3SmtSolver.h b/src/solver/Z3SmtSolver.h index 725b52e16..1e0fd2a43 100644 --- a/src/solver/Z3SmtSolver.h +++ b/src/solver/Z3SmtSolver.h @@ -53,13 +53,13 @@ namespace storm { virtual CheckResult checkWithAssumptions(std::initializer_list const& assumptions) override; - virtual storm::expressions::Valuation getModelAsValuation() override; + virtual storm::expressions::SimpleValuation getModelAsValuation() override; virtual std::shared_ptr getModel() override; - virtual std::vector allSat(std::vector const& important) override; + virtual std::vector allSat(std::vector const& important) override; - virtual uint_fast64_t allSat(std::vector const& important, std::function const& callback) override; + virtual uint_fast64_t allSat(std::vector const& important, std::function const& callback) override; virtual uint_fast64_t allSat(std::vector const& important, std::function const& callback) override; @@ -73,7 +73,7 @@ namespace storm { * @param model The Z3 model to convert. * @return The valuation of variables corresponding to the given model. */ - storm::expressions::Valuation convertZ3ModelToValuation(z3::model const& model); + storm::expressions::SimpleValuation convertZ3ModelToValuation(z3::model const& model); // The context used by the solver. std::unique_ptr context; diff --git a/src/storage/expressions/BaseExpression.cpp b/src/storage/expressions/BaseExpression.cpp index b8bb495e5..5685edd11 100644 --- a/src/storage/expressions/BaseExpression.cpp +++ b/src/storage/expressions/BaseExpression.cpp @@ -1,4 +1,5 @@ #include "src/storage/expressions/BaseExpression.h" +#include "src/storage/expressions/ExpressionManager.h" #include "src/utility/macros.h" #include "src/exceptions/InvalidTypeException.h" #include "src/exceptions/InvalidAccessException.h" @@ -14,15 +15,15 @@ namespace storm { } bool BaseExpression::hasIntegralType() const { - return this->getType() == manager.getIntegerType(); + return this->getType().isIntegralType(); } bool BaseExpression::hasNumericalType() const { - return this->getReturnType() == ExpressionReturnType::Double || this->getReturnType() == ExpressionReturnType::Int; + return this->getType().isNumericalType(); } bool BaseExpression::hasBooleanType() const { - return this->getReturnType() == ExpressionReturnType::Bool; + return this->getType().isBooleanType(); } int_fast64_t BaseExpression::evaluateAsInt(Valuation const* valuation) const { diff --git a/src/storage/expressions/Expression.h b/src/storage/expressions/Expression.h index bf5a3b08a..8334f415f 100644 --- a/src/storage/expressions/Expression.h +++ b/src/storage/expressions/Expression.h @@ -19,6 +19,7 @@ namespace storm { public: friend class ExpressionManager; friend class Variable; + template friend class SubstitutionVisitor; Expression() = default; diff --git a/src/storage/expressions/ExpressionManager.h b/src/storage/expressions/ExpressionManager.h index 30b47a503..3cc84b5bc 100644 --- a/src/storage/expressions/ExpressionManager.h +++ b/src/storage/expressions/ExpressionManager.h @@ -7,6 +7,7 @@ #include #include +#include "src/storage/expressions/Variable.h" #include "src/storage/expressions/Expression.h" #include "src/utility/OsDetection.h" diff --git a/src/storage/expressions/IdentifierSubstitutionVisitor.cpp b/src/storage/expressions/IdentifierSubstitutionVisitor.cpp deleted file mode 100644 index 30b83b9c7..000000000 --- a/src/storage/expressions/IdentifierSubstitutionVisitor.cpp +++ /dev/null @@ -1,127 +0,0 @@ -#include -#include -#include - -#include "src/storage/expressions/IdentifierSubstitutionVisitor.h" -#include "src/storage/expressions/Expressions.h" - -namespace storm { - namespace expressions { - template - IdentifierSubstitutionVisitor::IdentifierSubstitutionVisitor(MapType const& identifierToIdentifierMap) : identifierToIdentifierMap(identifierToIdentifierMap) { - // Intentionally left empty. - } - - template - Expression IdentifierSubstitutionVisitor::substitute(Expression const& expression) { - return Expression(boost::any_cast>(expression.getBaseExpression().accept(*this))); - } - - template - boost::any IdentifierSubstitutionVisitor::visit(IfThenElseExpression const& expression) { - std::shared_ptr conditionExpression = boost::any_cast>(expression.getCondition()->accept(*this)); - std::shared_ptr thenExpression = boost::any_cast>(expression.getThenExpression()->accept(*this)); - std::shared_ptr elseExpression = boost::any_cast>(expression.getElseExpression()->accept(*this)); - - // If the arguments did not change, we simply push the expression itself. - if (conditionExpression.get() == expression.getCondition().get() && thenExpression.get() == expression.getThenExpression().get() && elseExpression.get() == expression.getElseExpression().get()) { - return expression.getSharedPointer(); - } else { - return std::shared_ptr(new IfThenElseExpression(expression.getReturnType(), conditionExpression, thenExpression, elseExpression)); - } - } - - template - boost::any IdentifierSubstitutionVisitor::visit(BinaryBooleanFunctionExpression const& expression) { - std::shared_ptr firstExpression = boost::any_cast>(expression.getFirstOperand()->accept(*this)); - std::shared_ptr secondExpression = boost::any_cast>(expression.getSecondOperand()->accept(*this)); - - // If the arguments did not change, we simply push the expression itself. - if (firstExpression.get() == expression.getFirstOperand().get() && secondExpression.get() == expression.getSecondOperand().get()) { - return expression.getSharedPointer(); - } else { - return std::shared_ptr(new BinaryBooleanFunctionExpression(expression.getReturnType(), firstExpression, secondExpression, expression.getOperatorType())); - } - } - - template - boost::any IdentifierSubstitutionVisitor::visit(BinaryNumericalFunctionExpression const& expression) { - std::shared_ptr firstExpression = boost::any_cast>(expression.getFirstOperand()->accept(*this)); - std::shared_ptr secondExpression = boost::any_cast>(expression.getSecondOperand()->accept(*this)); - - // If the arguments did not change, we simply push the expression itself. - if (firstExpression.get() == expression.getFirstOperand().get() && secondExpression.get() == expression.getSecondOperand().get()) { - return expression.getSharedPointer(); - } else { - return std::shared_ptr(new BinaryNumericalFunctionExpression(expression.getReturnType(), firstExpression, secondExpression, expression.getOperatorType())); - } - } - - template - boost::any IdentifierSubstitutionVisitor::visit(BinaryRelationExpression const& expression) { - std::shared_ptr firstExpression = boost::any_cast>(expression.getFirstOperand()->accept(*this)); - std::shared_ptr secondExpression = boost::any_cast>(expression.getSecondOperand()->accept(*this)); - - // If the arguments did not change, we simply push the expression itself. - if (firstExpression.get() == expression.getFirstOperand().get() && secondExpression.get() == expression.getSecondOperand().get()) { - return expression.getSharedPointer(); - } else { - return std::shared_ptr(new BinaryRelationExpression(expression.getReturnType(), firstExpression, secondExpression, expression.getRelationType())); - } - } - - template - boost::any IdentifierSubstitutionVisitor::visit(VariableExpression const& expression) { - // If the variable is in the key set of the substitution, we need to replace it. - auto const& namePair = this->identifierToIdentifierMap.find(expression.getVariableName()); - if (namePair != this->identifierToIdentifierMap.end()) { - return std::shared_ptr(new VariableExpression(expression.getReturnType(), namePair->second)); - } else { - return expression.getSharedPointer(); - } - } - - template - boost::any IdentifierSubstitutionVisitor::visit(UnaryBooleanFunctionExpression const& expression) { - std::shared_ptr operandExpression = boost::any_cast>(expression.getOperand()->accept(*this)); - - // If the argument did not change, we simply push the expression itself. - if (operandExpression.get() == expression.getOperand().get()) { - return expression.getSharedPointer(); - } else { - return std::shared_ptr(new UnaryBooleanFunctionExpression(expression.getReturnType(), operandExpression, expression.getOperatorType())); - } - } - - template - boost::any IdentifierSubstitutionVisitor::visit(UnaryNumericalFunctionExpression const& expression) { - std::shared_ptr operandExpression = boost::any_cast>(expression.getOperand()->accept(*this)); - - // If the argument did not change, we simply push the expression itself. - if (operandExpression.get() == expression.getOperand().get()) { - return expression.getSharedPointer(); - } else { - return std::shared_ptr(new UnaryNumericalFunctionExpression(expression.getReturnType(), operandExpression, expression.getOperatorType())); - } - } - - template - boost::any IdentifierSubstitutionVisitor::visit(BooleanLiteralExpression const& expression) { - return expression.getSharedPointer(); - } - - template - boost::any IdentifierSubstitutionVisitor::visit(IntegerLiteralExpression const& expression) { - return expression.getSharedPointer(); - } - - template - boost::any IdentifierSubstitutionVisitor::visit(DoubleLiteralExpression const& expression) { - return expression.getSharedPointer(); - } - - // Explicitly instantiate the class with map and unordered_map. - template class IdentifierSubstitutionVisitor< std::map >; - template class IdentifierSubstitutionVisitor< std::unordered_map >; - } -} diff --git a/src/storage/expressions/IdentifierSubstitutionVisitor.h b/src/storage/expressions/IdentifierSubstitutionVisitor.h deleted file mode 100644 index a2044c9db..000000000 --- a/src/storage/expressions/IdentifierSubstitutionVisitor.h +++ /dev/null @@ -1,49 +0,0 @@ -#ifndef STORM_STORAGE_EXPRESSIONS_IDENTIFIERSUBSTITUTIONVISITOR_H_ -#define STORM_STORAGE_EXPRESSIONS_IDENTIFIERSUBSTITUTIONVISITOR_H_ - -#include - -#include "src/storage/expressions/Expression.h" -#include "src/storage/expressions/ExpressionVisitor.h" - -namespace storm { - namespace expressions { - template - class IdentifierSubstitutionVisitor : public ExpressionVisitor { - public: - /*! - * Creates a new substitution visitor that uses the given map to replace identifiers. - * - * @param identifierToExpressionMap A mapping from identifiers to expressions. - */ - IdentifierSubstitutionVisitor(MapType const& identifierToExpressionMap); - - /*! - * Substitutes the identifiers in the given expression according to the previously given map and returns the - * resulting expression. - * - * @param expression The expression in which to substitute the identifiers. - * @return The expression in which all identifiers in the key set of the previously given mapping are - * substituted with the mapped-to expressions. - */ - Expression substitute(Expression const& expression); - - virtual boost::any visit(IfThenElseExpression const& expression) override; - virtual boost::any visit(BinaryBooleanFunctionExpression const& expression) override; - virtual boost::any visit(BinaryNumericalFunctionExpression const& expression) override; - virtual boost::any visit(BinaryRelationExpression const& expression) override; - virtual boost::any visit(VariableExpression const& expression) override; - virtual boost::any visit(UnaryBooleanFunctionExpression const& expression) override; - virtual boost::any visit(UnaryNumericalFunctionExpression const& expression) override; - virtual boost::any visit(BooleanLiteralExpression const& expression) override; - virtual boost::any visit(IntegerLiteralExpression const& expression) override; - virtual boost::any visit(DoubleLiteralExpression const& expression) override; - - private: - // A mapping of identifier names to expressions with which they shall be replaced. - MapType const& identifierToIdentifierMap; - }; - } -} - -#endif /* STORM_STORAGE_EXPRESSIONS_IDENTIFIERSUBSTITUTIONVISITOR_H_ */ \ No newline at end of file diff --git a/src/storage/expressions/LinearCoefficientVisitor.h b/src/storage/expressions/LinearCoefficientVisitor.h index 2860da273..faf02414b 100644 --- a/src/storage/expressions/LinearCoefficientVisitor.h +++ b/src/storage/expressions/LinearCoefficientVisitor.h @@ -5,7 +5,7 @@ #include "src/storage/expressions/Expression.h" #include "src/storage/expressions/ExpressionVisitor.h" -#include "src/storage/expressions/Valuation.h" +#include "src/storage/expressions/SimpleValuation.h" namespace storm { namespace expressions { @@ -24,7 +24,7 @@ namespace storm { * @return A pair consisting of a mapping from identifiers to their coefficients and the coefficient of * the constant atom. */ - std::pair getLinearCoefficients(Expression const& expression); + std::pair getLinearCoefficients(Expression const& expression); virtual boost::any visit(IfThenElseExpression const& expression) override; virtual boost::any visit(BinaryBooleanFunctionExpression const& expression) override; diff --git a/src/storage/expressions/SimpleValuation.cpp b/src/storage/expressions/SimpleValuation.cpp index 331a0d8ad..bf2154620 100644 --- a/src/storage/expressions/SimpleValuation.cpp +++ b/src/storage/expressions/SimpleValuation.cpp @@ -59,11 +59,11 @@ namespace storm { (*rationalValues)[rationalVariable.getOffset()] = value; } - std::size_t SimpleValuationPointerHash::operator()(SimpleValuation* SimpleValuation) const { + std::size_t SimpleValuationPointerHash::operator()(SimpleValuation* valuation) const { size_t seed = 0; - boost::hash_combine(seed, SimpleValuation->booleanValues); - boost::hash_combine(seed, SimpleValuation->integerValues); - boost::hash_combine(seed, SimpleValuation->rationalValues); + boost::hash_combine(seed, valuation->booleanValues); + boost::hash_combine(seed, valuation->integerValues); + boost::hash_combine(seed, valuation->rationalValues); return seed; } diff --git a/src/storage/expressions/SimpleValuation.h b/src/storage/expressions/SimpleValuation.h index 3efadd7b4..53142fd31 100644 --- a/src/storage/expressions/SimpleValuation.h +++ b/src/storage/expressions/SimpleValuation.h @@ -14,6 +14,9 @@ namespace storm { */ class SimpleValuation : public Valuation { public: + friend class SimpleValuationPointerHash; + friend class SimpleValuationPointerLess; + /*! * Creates a new valuation over the non-auxiliary variables of the given manager. */ @@ -34,7 +37,7 @@ namespace storm { */ bool operator==(SimpleValuation const& other) const; - // + // Override virtual functions of base class. virtual bool getBooleanValue(Variable const& booleanVariable) const override; virtual void setBooleanValue(Variable const& booleanVariable, bool value) override; virtual int_fast64_t getIntegerValue(Variable const& integerVariable) const override; diff --git a/src/storage/expressions/SubstitutionVisitor.cpp b/src/storage/expressions/SubstitutionVisitor.cpp index 0924d9eb8..4f26d7e1a 100644 --- a/src/storage/expressions/SubstitutionVisitor.cpp +++ b/src/storage/expressions/SubstitutionVisitor.cpp @@ -8,7 +8,7 @@ namespace storm { namespace expressions { template - SubstitutionVisitor::SubstitutionVisitor(MapType const& identifierToExpressionMap) : identifierToExpressionMap(identifierToExpressionMap) { + SubstitutionVisitor::SubstitutionVisitor(MapType const& variableToExpressionMapping) : variableToExpressionMapping(variableToExpressionMapping) { // Intentionally left empty. } @@ -27,7 +27,7 @@ namespace storm { if (conditionExpression.get() == expression.getCondition().get() && thenExpression.get() == expression.getThenExpression().get() && elseExpression.get() == expression.getElseExpression().get()) { return expression.getSharedPointer(); } else { - return static_cast>(std::shared_ptr(new IfThenElseExpression(expression.getReturnType(), conditionExpression, thenExpression, elseExpression))); + return static_cast>(std::shared_ptr(new IfThenElseExpression(expression.getManager(), expression.getType(), conditionExpression, thenExpression, elseExpression))); } } @@ -40,7 +40,7 @@ namespace storm { if (firstExpression.get() == expression.getFirstOperand().get() && secondExpression.get() == expression.getSecondOperand().get()) { return expression.getSharedPointer(); } else { - return static_cast>(std::shared_ptr(new BinaryBooleanFunctionExpression(expression.getReturnType(), firstExpression, secondExpression, expression.getOperatorType()))); + return static_cast>(std::shared_ptr(new BinaryBooleanFunctionExpression(expression.getManager(), expression.getType(), firstExpression, secondExpression, expression.getOperatorType()))); } } @@ -53,7 +53,7 @@ namespace storm { if (firstExpression.get() == expression.getFirstOperand().get() && secondExpression.get() == expression.getSecondOperand().get()) { return expression.getSharedPointer(); } else { - return static_cast>(std::shared_ptr(new BinaryNumericalFunctionExpression(expression.getReturnType(), firstExpression, secondExpression, expression.getOperatorType()))); + return static_cast>(std::shared_ptr(new BinaryNumericalFunctionExpression(expression.getManager(), expression.getType(), firstExpression, secondExpression, expression.getOperatorType()))); } } @@ -66,15 +66,15 @@ namespace storm { if (firstExpression.get() == expression.getFirstOperand().get() && secondExpression.get() == expression.getSecondOperand().get()) { return expression.getSharedPointer(); } else { - return static_cast>(std::shared_ptr(new BinaryRelationExpression(expression.getReturnType(), firstExpression, secondExpression, expression.getRelationType()))); + return static_cast>(std::shared_ptr(new BinaryRelationExpression(expression.getManager(), expression.getType(), firstExpression, secondExpression, expression.getRelationType()))); } } template boost::any SubstitutionVisitor::visit(VariableExpression const& expression) { // If the variable is in the key set of the substitution, we need to replace it. - auto const& nameExpressionPair = this->identifierToExpressionMap.find(expression.getVariableName()); - if (nameExpressionPair != this->identifierToExpressionMap.end()) { + auto const& nameExpressionPair = this->variableToExpressionMapping.find(expression.getVariable()); + if (nameExpressionPair != this->variableToExpressionMapping.end()) { return nameExpressionPair->second.getBaseExpressionPointer(); } else { return expression.getSharedPointer(); @@ -89,7 +89,7 @@ namespace storm { if (operandExpression.get() == expression.getOperand().get()) { return expression.getSharedPointer(); } else { - return static_cast>(std::shared_ptr(new UnaryBooleanFunctionExpression(expression.getReturnType(), operandExpression, expression.getOperatorType()))); + return static_cast>(std::shared_ptr(new UnaryBooleanFunctionExpression(expression.getManager(), expression.getType(), operandExpression, expression.getOperatorType()))); } } @@ -101,7 +101,7 @@ namespace storm { if (operandExpression.get() == expression.getOperand().get()) { return expression.getSharedPointer(); } else { - return static_cast>(std::shared_ptr(new UnaryNumericalFunctionExpression(expression.getReturnType(), operandExpression, expression.getOperatorType()))); + return static_cast>(std::shared_ptr(new UnaryNumericalFunctionExpression(expression.getManager(), expression.getType(), operandExpression, expression.getOperatorType()))); } } @@ -121,7 +121,7 @@ namespace storm { } // Explicitly instantiate the class with map and unordered_map. - template class SubstitutionVisitor>; - template class SubstitutionVisitor>; + template class SubstitutionVisitor>; + template class SubstitutionVisitor>; } } diff --git a/src/storage/expressions/SubstitutionVisitor.h b/src/storage/expressions/SubstitutionVisitor.h index e2dec9e5c..343521335 100644 --- a/src/storage/expressions/SubstitutionVisitor.h +++ b/src/storage/expressions/SubstitutionVisitor.h @@ -12,11 +12,11 @@ namespace storm { class SubstitutionVisitor : public ExpressionVisitor { public: /*! - * Creates a new substitution visitor that uses the given map to replace identifiers. + * Creates a new substitution visitor that uses the given map to replace variables. * - * @param identifierToExpressionMap A mapping from identifiers to expressions. + * @param variableToExpressionMapping A mapping from variables to expressions. */ - SubstitutionVisitor(MapType const& identifierToExpressionMap); + SubstitutionVisitor(MapType const& variableToExpressionMapping); /*! * Substitutes the identifiers in the given expression according to the previously given map and returns the @@ -40,8 +40,8 @@ namespace storm { virtual boost::any visit(DoubleLiteralExpression const& expression) override; private: - // A mapping of identifier names to expressions with which they shall be replaced. - MapType const& identifierToExpressionMap; + // A mapping of variables to expressions with which they shall be replaced. + MapType const& variableToExpressionMapping; }; } } diff --git a/src/storage/expressions/Valuation.h b/src/storage/expressions/Valuation.h index 034df3a28..00ffb4283 100644 --- a/src/storage/expressions/Valuation.h +++ b/src/storage/expressions/Valuation.h @@ -14,9 +14,6 @@ namespace storm { */ class Valuation { public: - friend class ValuationPointerHash; - friend class ValuationPointerLess; - /*! * 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