diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp index 6039c2c11..9679168b6 100644 --- a/src/parser/PrismParser.cpp +++ b/src/parser/PrismParser.cpp @@ -585,7 +585,7 @@ namespace storm { auto const& renamingPair = renaming.find(variable.getName()); LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Boolean variable '" << variable.getName() << " was not renamed."); - booleanVariables.push_back(storm::prism::BooleanVariable(renamingPair->second, variable.getInitialValueExpression().substitute(expressionRenaming), this->getFilename(), get_line(qi::_1))); + booleanVariables.push_back(storm::prism::BooleanVariable(renamingPair->second, variable.getInitialValueExpression().substitute(expressionRenaming), this->getFilename(), get_line(qi::_1))); } // Rename the integer variables. @@ -594,7 +594,7 @@ namespace storm { auto const& renamingPair = renaming.find(variable.getName()); LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Integer variable '" << variable.getName() << " was not renamed."); - integerVariables.push_back(storm::prism::IntegerVariable(renamingPair->second, variable.getLowerBoundExpression().substitute(expressionRenaming), variable.getUpperBoundExpression().substitute(expressionRenaming), variable.getInitialValueExpression().substitute(expressionRenaming), this->getFilename(), get_line(qi::_1))); + integerVariables.push_back(storm::prism::IntegerVariable(renamingPair->second, variable.getLowerBoundExpression().substitute(expressionRenaming), variable.getUpperBoundExpression().substitute(expressionRenaming), variable.getInitialValueExpression().substitute(expressionRenaming), this->getFilename(), get_line(qi::_1))); } // Rename commands. @@ -606,12 +606,12 @@ namespace storm { for (auto const& assignment : update.getAssignments()) { auto const& renamingPair = renaming.find(assignment.getVariableName()); if (renamingPair != renaming.end()) { - assignments.emplace_back(renamingPair->second, assignment.getExpression().substitute(expressionRenaming), this->getFilename(), get_line(qi::_1)); + assignments.emplace_back(renamingPair->second, assignment.getExpression().substitute(expressionRenaming), this->getFilename(), get_line(qi::_1)); } else { - assignments.emplace_back(assignment.getVariableName(), assignment.getExpression().substitute(expressionRenaming), this->getFilename(), get_line(qi::_1)); + assignments.emplace_back(assignment.getVariableName(), assignment.getExpression().substitute(expressionRenaming), this->getFilename(), get_line(qi::_1)); } } - updates.emplace_back(globalProgramInformation.currentUpdateIndex, update.getLikelihoodExpression().substitute(expressionRenaming), assignments, this->getFilename(), get_line(qi::_1)); + updates.emplace_back(globalProgramInformation.currentUpdateIndex, update.getLikelihoodExpression().substitute(expressionRenaming), assignments, this->getFilename(), get_line(qi::_1)); ++globalProgramInformation.currentUpdateIndex; } @@ -621,7 +621,7 @@ namespace storm { newActionName = renamingPair->second; } - commands.emplace_back(globalProgramInformation.currentCommandIndex, newActionName, command.getGuardExpression().substitute(expressionRenaming), updates, this->getFilename(), get_line(qi::_1)); + commands.emplace_back(globalProgramInformation.currentCommandIndex, newActionName, command.getGuardExpression().substitute(expressionRenaming), updates, this->getFilename(), get_line(qi::_1)); ++globalProgramInformation.currentCommandIndex; } diff --git a/src/storage/expressions/Expression.cpp b/src/storage/expressions/Expression.cpp index 7eb94966b..93e356009 100644 --- a/src/storage/expressions/Expression.cpp +++ b/src/storage/expressions/Expression.cpp @@ -27,15 +27,21 @@ namespace storm { // Intentionally left empty. } - template class MapType> - Expression Expression::substitute(MapType const& identifierToExpressionMap) const { - return SubstitutionVisitor(identifierToExpressionMap).substitute(this->getBaseExpressionPointer().get()); + Expression Expression::substitute(std::map const& identifierToExpressionMap) const { + return SubstitutionVisitor< std::map >(identifierToExpressionMap).substitute(this->getBaseExpressionPointer().get()); } + + Expression Expression::substitute(std::unordered_map const& identifierToExpressionMap) const { + return SubstitutionVisitor< std::unordered_map >(identifierToExpressionMap).substitute(this->getBaseExpressionPointer().get()); + } - template class MapType> - Expression Expression::substitute(MapType const& identifierToIdentifierMap) const { - return IdentifierSubstitutionVisitor(identifierToIdentifierMap).substitute(this->getBaseExpressionPointer().get()); + Expression Expression::substitute(std::map const& identifierToIdentifierMap) const { + return IdentifierSubstitutionVisitor< std::map >(identifierToIdentifierMap).substitute(this->getBaseExpressionPointer().get()); } + + Expression Expression::substitute(std::unordered_map const& identifierToIdentifierMap) const { + return IdentifierSubstitutionVisitor< std::unordered_map >(identifierToIdentifierMap).substitute(this->getBaseExpressionPointer().get()); + } bool Expression::evaluateAsBool(Valuation const* valuation) const { return this->getBaseExpression().evaluateAsBool(valuation); @@ -247,11 +253,6 @@ namespace storm { return Expression(std::shared_ptr(new UnaryNumericalFunctionExpression(ExpressionReturnType::Int, this->getBaseExpressionPointer(), UnaryNumericalFunctionExpression::OperatorType::Ceil))); } - template Expression Expression::substitute(std::map const&) const; - template Expression Expression::substitute(std::unordered_map const&) const; - template Expression Expression::substitute(std::map const&) const; - template Expression Expression::substitute(std::unordered_map const&) const; - std::ostream& operator<<(std::ostream& stream, Expression const& expression) { stream << expression.getBaseExpression(); return stream; diff --git a/src/storage/expressions/Expression.h b/src/storage/expressions/Expression.h index ea7d99572..3001def0a 100644 --- a/src/storage/expressions/Expression.h +++ b/src/storage/expressions/Expression.h @@ -2,6 +2,8 @@ #define STORM_STORAGE_EXPRESSIONS_EXPRESSION_H_ #include +#include +#include #include "src/storage/expressions/BaseExpression.h" #include "src/utility/OsDetection.h" @@ -76,8 +78,18 @@ namespace storm { * @return An expression in which all identifiers in the key set of the mapping are replaced by the * expression they are mapped to. */ - template class MapType> - Expression substitute(MapType const& identifierToExpressionMap) const; + Expression substitute(std::map const& identifierToExpressionMap) const; + + /*! + * Substitutes all occurrences of identifiers according to the given map. Note that this substitution is + * done simultaneously, i.e., identifiers appearing in the expressions that were "plugged in" are not + * substituted. + * + * @param identifierToExpressionMap A mapping from identifiers to the expression they are substituted with. + * @return An expression in which all identifiers in the key set of the mapping are replaced by the + * expression they are mapped to. + */ + Expression substitute(std::unordered_map const& identifierToExpressionMap) const; /*! * Substitutes all occurrences of identifiers with different names given by a mapping. @@ -86,8 +98,16 @@ namespace storm { * @return An expression in which all identifiers in the key set of the mapping are replaced by the * identifiers they are mapped to. */ - template class MapType> - Expression substitute(MapType const& identifierToIdentifierMap) const; + Expression substitute(std::map const& identifierToIdentifierMap) const; + + /*! + * Substitutes all occurrences of identifiers with different names given by a mapping. + * + * @param identifierToIdentifierMap A mapping from identifiers to identifiers they are substituted with. + * @return An expression in which all identifiers in the key set of the mapping are replaced by the + * identifiers they are mapped to. + */ + Expression substitute(std::unordered_map const& identifierToIdentifierMap) const; /*! * Evaluates the expression under the valuation of unknowns (variables and constants) given by the diff --git a/src/storage/expressions/IdentifierSubstitutionVisitor.cpp b/src/storage/expressions/IdentifierSubstitutionVisitor.cpp index 17161775a..1b058bed2 100644 --- a/src/storage/expressions/IdentifierSubstitutionVisitor.cpp +++ b/src/storage/expressions/IdentifierSubstitutionVisitor.cpp @@ -1,5 +1,6 @@ #include #include +#include #include "src/storage/expressions/IdentifierSubstitutionVisitor.h" @@ -19,18 +20,18 @@ namespace storm { namespace expressions { - template class MapType> - IdentifierSubstitutionVisitor::IdentifierSubstitutionVisitor(MapType const& identifierToIdentifierMap) : identifierToIdentifierMap(identifierToIdentifierMap) { + template + IdentifierSubstitutionVisitor::IdentifierSubstitutionVisitor(MapType const& identifierToIdentifierMap) : identifierToIdentifierMap(identifierToIdentifierMap) { // Intentionally left empty. } - template class MapType> + template Expression IdentifierSubstitutionVisitor::substitute(BaseExpression const* expression) { expression->accept(this); return Expression(this->expressionStack.top()); } - template class MapType> + template void IdentifierSubstitutionVisitor::visit(IfThenElseExpression const* expression) { expression->getCondition()->accept(this); std::shared_ptr conditionExpression = expressionStack.top(); @@ -52,7 +53,7 @@ namespace storm { } } - template class MapType> + template void IdentifierSubstitutionVisitor::visit(BinaryBooleanFunctionExpression const* expression) { expression->getFirstOperand()->accept(this); std::shared_ptr firstExpression = expressionStack.top(); @@ -70,7 +71,7 @@ namespace storm { } } - template class MapType> + template void IdentifierSubstitutionVisitor::visit(BinaryNumericalFunctionExpression const* expression) { expression->getFirstOperand()->accept(this); std::shared_ptr firstExpression = expressionStack.top(); @@ -88,7 +89,7 @@ namespace storm { } } - template class MapType> + template void IdentifierSubstitutionVisitor::visit(BinaryRelationExpression const* expression) { expression->getFirstOperand()->accept(this); std::shared_ptr firstExpression = expressionStack.top(); @@ -106,7 +107,7 @@ namespace storm { } } - template class MapType> + template void IdentifierSubstitutionVisitor::visit(BooleanConstantExpression const* expression) { // If the boolean constant is in the key set of the substitution, we need to replace it. auto const& namePair = this->identifierToIdentifierMap.find(expression->getConstantName()); @@ -117,7 +118,7 @@ namespace storm { } } - template class MapType> + template void IdentifierSubstitutionVisitor::visit(DoubleConstantExpression const* expression) { // If the double constant is in the key set of the substitution, we need to replace it. auto const& namePair = this->identifierToIdentifierMap.find(expression->getConstantName()); @@ -128,7 +129,7 @@ namespace storm { } } - template class MapType> + template void IdentifierSubstitutionVisitor::visit(IntegerConstantExpression const* expression) { // If the integer constant is in the key set of the substitution, we need to replace it. auto const& namePair = this->identifierToIdentifierMap.find(expression->getConstantName()); @@ -139,7 +140,7 @@ namespace storm { } } - template class MapType> + template void 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()); @@ -150,7 +151,7 @@ namespace storm { } } - template class MapType> + template void IdentifierSubstitutionVisitor::visit(UnaryBooleanFunctionExpression const* expression) { expression->getOperand()->accept(this); std::shared_ptr operandExpression = expressionStack.top(); @@ -164,7 +165,7 @@ namespace storm { } } - template class MapType> + template void IdentifierSubstitutionVisitor::visit(UnaryNumericalFunctionExpression const* expression) { expression->getOperand()->accept(this); std::shared_ptr operandExpression = expressionStack.top(); @@ -178,23 +179,23 @@ namespace storm { } } - template class MapType> + template void IdentifierSubstitutionVisitor::visit(BooleanLiteralExpression const* expression) { this->expressionStack.push(expression->getSharedPointer()); } - template class MapType> + template void IdentifierSubstitutionVisitor::visit(IntegerLiteralExpression const* expression) { this->expressionStack.push(expression->getSharedPointer()); } - template class MapType> + template void IdentifierSubstitutionVisitor::visit(DoubleLiteralExpression const* expression) { this->expressionStack.push(expression->getSharedPointer()); } // Explicitly instantiate the class with map and unordered_map. - template class IdentifierSubstitutionVisitor; - template class IdentifierSubstitutionVisitor; + 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 index 6be7aa9ca..e8412d949 100644 --- a/src/storage/expressions/IdentifierSubstitutionVisitor.h +++ b/src/storage/expressions/IdentifierSubstitutionVisitor.h @@ -8,7 +8,7 @@ namespace storm { namespace expressions { - template class MapType> + template class IdentifierSubstitutionVisitor : public ExpressionVisitor { public: /*! @@ -16,7 +16,7 @@ namespace storm { * * @param identifierToExpressionMap A mapping from identifiers to expressions. */ - IdentifierSubstitutionVisitor(MapType const& identifierToExpressionMap); + IdentifierSubstitutionVisitor(MapType const& identifierToExpressionMap); /*! * Substitutes the identifiers in the given expression according to the previously given map and returns the @@ -47,7 +47,7 @@ namespace storm { std::stack> expressionStack; // A mapping of identifier names to expressions with which they shall be replaced. - MapType const& identifierToIdentifierMap; + MapType const& identifierToIdentifierMap; }; } } diff --git a/src/storage/expressions/SubstitutionVisitor.cpp b/src/storage/expressions/SubstitutionVisitor.cpp index c3f2ea0a8..54b533d49 100644 --- a/src/storage/expressions/SubstitutionVisitor.cpp +++ b/src/storage/expressions/SubstitutionVisitor.cpp @@ -1,5 +1,6 @@ #include #include +#include #include "src/storage/expressions/SubstitutionVisitor.h" @@ -19,18 +20,18 @@ namespace storm { namespace expressions { - template class MapType> - SubstitutionVisitor::SubstitutionVisitor(MapType const& identifierToExpressionMap) : identifierToExpressionMap(identifierToExpressionMap) { + template + SubstitutionVisitor::SubstitutionVisitor(MapType const& identifierToExpressionMap) : identifierToExpressionMap(identifierToExpressionMap) { // Intentionally left empty. } - template class MapType> + template Expression SubstitutionVisitor::substitute(BaseExpression const* expression) { expression->accept(this); return Expression(this->expressionStack.top()); } - template class MapType> + template void SubstitutionVisitor::visit(IfThenElseExpression const* expression) { expression->getCondition()->accept(this); std::shared_ptr conditionExpression = expressionStack.top(); @@ -52,7 +53,7 @@ namespace storm { } } - template class MapType> + template void SubstitutionVisitor::visit(BinaryBooleanFunctionExpression const* expression) { expression->getFirstOperand()->accept(this); std::shared_ptr firstExpression = expressionStack.top(); @@ -70,7 +71,7 @@ namespace storm { } } - template class MapType> + template void SubstitutionVisitor::visit(BinaryNumericalFunctionExpression const* expression) { expression->getFirstOperand()->accept(this); std::shared_ptr firstExpression = expressionStack.top(); @@ -88,7 +89,7 @@ namespace storm { } } - template class MapType> + template void SubstitutionVisitor::visit(BinaryRelationExpression const* expression) { expression->getFirstOperand()->accept(this); std::shared_ptr firstExpression = expressionStack.top(); @@ -106,7 +107,7 @@ namespace storm { } } - template class MapType> + template void SubstitutionVisitor::visit(BooleanConstantExpression const* expression) { // If the boolean constant is in the key set of the substitution, we need to replace it. auto const& nameExpressionPair = this->identifierToExpressionMap.find(expression->getConstantName()); @@ -117,7 +118,7 @@ namespace storm { } } - template class MapType> + template void SubstitutionVisitor::visit(DoubleConstantExpression const* expression) { // If the double constant is in the key set of the substitution, we need to replace it. auto const& nameExpressionPair = this->identifierToExpressionMap.find(expression->getConstantName()); @@ -128,7 +129,7 @@ namespace storm { } } - template class MapType> + template void SubstitutionVisitor::visit(IntegerConstantExpression const* expression) { // If the integer constant is in the key set of the substitution, we need to replace it. auto const& nameExpressionPair = this->identifierToExpressionMap.find(expression->getConstantName()); @@ -139,7 +140,7 @@ namespace storm { } } - template class MapType> + template void 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()); @@ -150,7 +151,7 @@ namespace storm { } } - template class MapType> + template void SubstitutionVisitor::visit(UnaryBooleanFunctionExpression const* expression) { expression->getOperand()->accept(this); std::shared_ptr operandExpression = expressionStack.top(); @@ -164,7 +165,7 @@ namespace storm { } } - template class MapType> + template void SubstitutionVisitor::visit(UnaryNumericalFunctionExpression const* expression) { expression->getOperand()->accept(this); std::shared_ptr operandExpression = expressionStack.top(); @@ -178,23 +179,23 @@ namespace storm { } } - template class MapType> + template void SubstitutionVisitor::visit(BooleanLiteralExpression const* expression) { this->expressionStack.push(expression->getSharedPointer()); } - template class MapType> + template void SubstitutionVisitor::visit(IntegerLiteralExpression const* expression) { this->expressionStack.push(expression->getSharedPointer()); } - template class MapType> + template void SubstitutionVisitor::visit(DoubleLiteralExpression const* expression) { this->expressionStack.push(expression->getSharedPointer()); } // Explicitly instantiate the class with map and unordered_map. - template class SubstitutionVisitor; - template class SubstitutionVisitor; + template class SubstitutionVisitor< std::map >; + template class SubstitutionVisitor< std::unordered_map >; } } diff --git a/src/storage/expressions/SubstitutionVisitor.h b/src/storage/expressions/SubstitutionVisitor.h index ad29ad6ab..d46d62cee 100644 --- a/src/storage/expressions/SubstitutionVisitor.h +++ b/src/storage/expressions/SubstitutionVisitor.h @@ -8,7 +8,7 @@ namespace storm { namespace expressions { - template class MapType> + template class SubstitutionVisitor : public ExpressionVisitor { public: /*! @@ -16,7 +16,7 @@ namespace storm { * * @param identifierToExpressionMap A mapping from identifiers to expressions. */ - SubstitutionVisitor(MapType const& identifierToExpressionMap); + SubstitutionVisitor(MapType const& identifierToExpressionMap); /*! * Substitutes the identifiers in the given expression according to the previously given map and returns the @@ -47,7 +47,7 @@ namespace storm { std::stack> expressionStack; // A mapping of identifier names to expressions with which they shall be replaced. - MapType const& identifierToExpressionMap; + MapType const& identifierToExpressionMap; }; } } diff --git a/src/storage/prism/Assignment.cpp b/src/storage/prism/Assignment.cpp index f15797e6d..3b63703ed 100644 --- a/src/storage/prism/Assignment.cpp +++ b/src/storage/prism/Assignment.cpp @@ -15,7 +15,7 @@ namespace storm { } Assignment Assignment::substitute(std::map const& substitution) const { - return Assignment(this->getVariableName(), this->getExpression().substitute(substitution), this->getFilename(), this->getLineNumber()); + return Assignment(this->getVariableName(), this->getExpression().substitute(substitution), this->getFilename(), this->getLineNumber()); } std::ostream& operator<<(std::ostream& stream, Assignment const& assignment) { diff --git a/src/storage/prism/BooleanVariable.cpp b/src/storage/prism/BooleanVariable.cpp index 478b9322d..ef88cefc4 100644 --- a/src/storage/prism/BooleanVariable.cpp +++ b/src/storage/prism/BooleanVariable.cpp @@ -11,7 +11,7 @@ namespace storm { } BooleanVariable BooleanVariable::substitute(std::map const& substitution) const { - return BooleanVariable(this->getName(), this->getInitialValueExpression().substitute(substitution), this->getFilename(), this->getLineNumber()); + return BooleanVariable(this->getName(), this->getInitialValueExpression().substitute(substitution), this->getFilename(), this->getLineNumber()); } std::ostream& operator<<(std::ostream& stream, BooleanVariable const& variable) { diff --git a/src/storage/prism/Command.cpp b/src/storage/prism/Command.cpp index f075ff6c6..4b36942df 100644 --- a/src/storage/prism/Command.cpp +++ b/src/storage/prism/Command.cpp @@ -37,7 +37,7 @@ namespace storm { newUpdates.emplace_back(update.substitute(substitution)); } - return Command(this->getGlobalIndex(), this->getActionName(), this->getGuardExpression().substitute(substitution), newUpdates, this->getFilename(), this->getLineNumber()); + return Command(this->getGlobalIndex(), this->getActionName(), this->getGuardExpression().substitute(substitution), newUpdates, this->getFilename(), this->getLineNumber()); } std::ostream& operator<<(std::ostream& stream, Command const& command) { diff --git a/src/storage/prism/Constant.cpp b/src/storage/prism/Constant.cpp index 160e9ad22..3df0a26bc 100644 --- a/src/storage/prism/Constant.cpp +++ b/src/storage/prism/Constant.cpp @@ -27,7 +27,7 @@ namespace storm { } Constant Constant::substitute(std::map const& substitution) const { - return Constant(this->getType(), this->getName(), this->getExpression().substitute(substitution), this->getFilename(), this->getLineNumber()); + return Constant(this->getType(), this->getName(), this->getExpression().substitute(substitution), this->getFilename(), this->getLineNumber()); } std::ostream& operator<<(std::ostream& stream, Constant const& constant) { diff --git a/src/storage/prism/Formula.cpp b/src/storage/prism/Formula.cpp index 3bf72a7de..fbda0c69d 100644 --- a/src/storage/prism/Formula.cpp +++ b/src/storage/prism/Formula.cpp @@ -19,7 +19,7 @@ namespace storm { } Formula Formula::substitute(std::map const& substitution) const { - return Formula(this->getName(), this->getExpression().substitute(substitution), this->getFilename(), this->getLineNumber()); + return Formula(this->getName(), this->getExpression().substitute(substitution), this->getFilename(), this->getLineNumber()); } std::ostream& operator<<(std::ostream& stream, Formula const& formula) { diff --git a/src/storage/prism/IntegerVariable.cpp b/src/storage/prism/IntegerVariable.cpp index a80b6394e..1968a07ca 100644 --- a/src/storage/prism/IntegerVariable.cpp +++ b/src/storage/prism/IntegerVariable.cpp @@ -19,7 +19,7 @@ namespace storm { } IntegerVariable IntegerVariable::substitute(std::map const& substitution) const { - return IntegerVariable(this->getName(), this->getLowerBoundExpression().substitute(substitution), this->getUpperBoundExpression().substitute(substitution), this->getInitialValueExpression().substitute(substitution), this->getFilename(), this->getLineNumber()); + return IntegerVariable(this->getName(), this->getLowerBoundExpression().substitute(substitution), this->getUpperBoundExpression().substitute(substitution), this->getInitialValueExpression().substitute(substitution), this->getFilename(), this->getLineNumber()); } std::ostream& operator<<(std::ostream& stream, IntegerVariable const& variable) { diff --git a/src/storage/prism/Label.cpp b/src/storage/prism/Label.cpp index a78f9079f..cb8a13f25 100644 --- a/src/storage/prism/Label.cpp +++ b/src/storage/prism/Label.cpp @@ -15,7 +15,7 @@ namespace storm { } Label Label::substitute(std::map const& substitution) const { - return Label(this->getName(), this->getStatePredicateExpression().substitute(substitution), this->getFilename(), this->getLineNumber()); + return Label(this->getName(), this->getStatePredicateExpression().substitute(substitution), this->getFilename(), this->getLineNumber()); } std::ostream& operator<<(std::ostream& stream, Label const& label) { diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index cdbba3e22..1c4118b8b 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -229,7 +229,7 @@ namespace storm { LOG_THROW(constantDefinitions.find(constant.getName()) == constantDefinitions.end(), storm::exceptions::InvalidArgumentException, "Illegally defining already defined constant '" << constant.getName() << "'."); // Now replace the occurrences of undefined constants in its defining expression. - newConstants.emplace_back(constant.getType(), constant.getName(), constant.getExpression().substitute(constantDefinitions), constant.getFilename(), constant.getLineNumber()); + newConstants.emplace_back(constant.getType(), constant.getName(), constant.getExpression().substitute(constantDefinitions), constant.getFilename(), constant.getLineNumber()); } else { auto const& variableExpressionPair = constantDefinitions.find(constant.getName()); @@ -306,7 +306,7 @@ namespace storm { newRewardModels.emplace_back(rewardModel.substitute(constantSubstitution)); } - storm::expressions::Expression newInitialStateExpression = this->getInitialStatesExpression().substitute(constantSubstitution); + storm::expressions::Expression newInitialStateExpression = this->getInitialStatesExpression().substitute(constantSubstitution); std::vector