Added support for cloning IR expressions.

Former-commit-id: 913269b3a5

src/adapters/Z3ExpressionAdapter.h

@@ -83,7 +83,7 @@ namespace storm {
                         break;
                     default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
                         << "Unknown boolean binary operator: '" << expression->getFunctionType() << "'.";
-                }    
+                }
             }
             
             virtual void visit(BinaryRelationExpression* expression) {

src/counterexamples/SMTMinimalCommandSetGenerator.h

@@ -209,6 +209,17 @@ namespace storm {
                 }
                 assertDisjunction(context, solver, expressionVector);
             }
+            
+            /*!
+             * Asserts cuts that rule out a lot of suboptimal solutions.
+             *
+             * @param program The program for which to derive the cuts.
+             * @param context The Z3 context in which to build the expressions.
+             * @param solver The solver to use for the satisfiability evaluation.
+             */
+            static void assertCuts(storm::ir::Program const& program, z3::context& context, z3::solver& solver) {
+                
+            }
 
             /*!
              * Asserts that the disjunction of the given formulae holds.
@@ -396,7 +407,10 @@ namespace storm {
                 // (5) Build the initial constraint system.
                 assertInitialConstraints(program, labeledMdp, psiStates, context, solver, variableInformation, relevancyInformation);
                 
-                // (6) Find the smallest set of commands that satisfies all constraints. If the probability of
+                // (6) Add constraints that cut off a lot of suboptimal solutions.
+                assertCuts(program, context, solver);
+                
+                // (7) Find the smallest set of commands that satisfies all constraints. If the probability of
                 // satisfying phi until psi exceeds the given threshold, the set of labels is minimal and can be returned.
                 // Otherwise, the current solution has to be ruled out and the next smallest solution is retrieved from
                 // the solver.
@@ -449,7 +463,7 @@ namespace storm {
                 }
                 std::cout << std::endl;
                 
-                // (7) Return the resulting command set.
+                // (8) Return the resulting command set.
                 return commandSet;
                 
 #else

src/ir/expressions/BaseExpression.h

@@ -64,6 +64,13 @@ namespace storm {
                  */
                 virtual ~BaseExpression();
                 
+                /*!
+                 * Performes a deep-copy of the expression.
+                 *
+                 * @return A deep-copy of the expression.
+                 */
+                virtual std::shared_ptr<BaseExpression> clone() const = 0;
+                
                 /*!
                  * Copies the expression tree underneath (including) the current node and performs the provided renaming.
                  *
@@ -71,7 +78,7 @@ namespace storm {
                  * @param variableState An object knowing about the global variable state.
                  */
                 virtual std::shared_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const = 0;
-                
+                                
                 /*!
                  * Retrieves the value of the expression as an integer given the provided variable valuation.
                  *

src/ir/expressions/BinaryBooleanFunctionExpression.cpp

@@ -23,6 +23,10 @@ namespace storm {
                 // Nothing to do here.
             }
 
+            std::shared_ptr<BaseExpression> BinaryBooleanFunctionExpression::clone() const {
+                return std::shared_ptr<BaseExpression>(new BinaryBooleanFunctionExpression(this->getLeft()->clone(), this->getRight()->clone(), functionType));
+            }
+            
             std::shared_ptr<BaseExpression> BinaryBooleanFunctionExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
                 return std::shared_ptr<BaseExpression>(new BinaryBooleanFunctionExpression(this->getLeft()->clone(renaming, variableState), this->getRight()->clone(renaming, variableState), this->functionType));
             }

src/ir/expressions/BinaryBooleanFunctionExpression.h

@@ -40,6 +40,8 @@ namespace storm {
                  */
                 BinaryBooleanFunctionExpression(BinaryBooleanFunctionExpression const& binaryBooleanFunctionExpression);
                 
+                virtual std::shared_ptr<BaseExpression> clone() const override;
+                
                 virtual std::shared_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
                 
                 virtual bool getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override;

src/ir/expressions/BinaryNumericalFunctionExpression.cpp

@@ -23,6 +23,10 @@ namespace storm {
                 // Nothing to do here.
             }
 
+            std::shared_ptr<BaseExpression> BinaryNumericalFunctionExpression::clone() const {
+                return std::shared_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(this->getType(), this->getLeft()->clone(), this->getRight()->clone(), functionType));
+            }
+
             std::shared_ptr<BaseExpression> BinaryNumericalFunctionExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
                 return std::shared_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(this->getType(), this->getLeft()->clone(renaming, variableState), this->getRight()->clone(renaming, variableState), this->functionType));
             }

src/ir/expressions/BinaryNumericalFunctionExpression.h

@@ -41,6 +41,8 @@ namespace storm {
                  */
                 BinaryNumericalFunctionExpression(BinaryNumericalFunctionExpression const& binaryNumericalFunctionExpression);
 
+                virtual std::shared_ptr<BaseExpression> clone() const override;
+                
                 virtual std::shared_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
                 
                 /*!

src/ir/expressions/BinaryRelationExpression.cpp

@@ -23,6 +23,10 @@ namespace storm {
                 // Nothing to do here.
             }
             
+            std::shared_ptr<BaseExpression> BinaryRelationExpression::clone() const {
+                return std::shared_ptr<BaseExpression>(new BinaryRelationExpression(this->getLeft()->clone(), this->getRight()->clone(), relationType));
+            }
+
             std::shared_ptr<BaseExpression> BinaryRelationExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
                 return std::shared_ptr<BaseExpression>(new BinaryRelationExpression(this->getLeft()->clone(renaming, variableState), this->getRight()->clone(renaming, variableState), this->relationType));
             }

src/ir/expressions/BinaryRelationExpression.h

@@ -40,6 +40,8 @@ namespace storm {
                  */
                 BinaryRelationExpression(BinaryRelationExpression const& binaryRelationExpression);
                 
+                virtual std::shared_ptr<BaseExpression> clone() const override;
+                
                 virtual std::shared_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
                 
                 virtual bool getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override;

src/ir/expressions/BooleanConstantExpression.cpp

@@ -19,6 +19,10 @@ namespace storm {
                 // Nothing to do here.
             }
 
+            std::shared_ptr<BaseExpression> BooleanConstantExpression::clone() const {
+                return std::shared_ptr<BaseExpression>(new BooleanConstantExpression(*this));
+            }
+
             std::shared_ptr<BaseExpression> BooleanConstantExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
                 return std::shared_ptr<BaseExpression>(new BooleanConstantExpression(*this));
             }

src/ir/expressions/BooleanConstantExpression.h

@@ -33,6 +33,8 @@ namespace storm {
                  */
                 BooleanConstantExpression(BooleanConstantExpression const& booleanConstantExpression);
                 
+                virtual std::shared_ptr<BaseExpression> clone() const override;
+
                 virtual std::shared_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
                 
                 virtual bool getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override;

src/ir/expressions/BooleanLiteral.h

@@ -1,62 +0,0 @@
-/*
- * BooleanLiteral.h
- *
- *  Created on: 03.01.2013
- *      Author: chris
- */
-
-#ifndef STORM_IR_EXPRESSIONS_BOOLEANLITERAL_H_
-#define STORM_IR_EXPRESSIONS_BOOLEANLITERAL_H_
-
-#include "src/ir/expressions/BaseExpression.h"
-
-namespace storm {
-namespace ir {
-namespace expressions {
-
-class BooleanLiteral : public BaseExpression {
-public:
-	bool value;
-
-	BooleanLiteral(bool value) : BaseExpression(bool_), value(value) {
-
-	}
-
-	virtual ~BooleanLiteral() {
-
-	}
-
-	virtual std::shared_ptr<BaseExpression> clone(const std::map<std::string, std::string>& renaming, const std::map<std::string, uint_fast64_t>& bools, const std::map<std::string, uint_fast64_t>& ints) override {
-		return std::shared_ptr<BaseExpression>(new BooleanLiteral(this->value));
-	}
-
-	virtual bool getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override {
-		return value;
-	}
-
-	virtual void accept(ExpressionVisitor* visitor) override {
-		visitor->visit(this);
-	}
-
-	virtual std::string toString() const override {
-		if (value) {
-			return std::string("true");
-		} else {
-			return std::string("false");
-		}
-	}
-	
-	virtual std::string dump(std::string prefix) const override {
-		std::stringstream result;
-		result << prefix << "BooleanLiteral " << this->toString() << std::endl;
-		return result.str();
-	}
-};
-
-}
-
-}
-
-}
-
-#endif /* STORM_IR_EXPRESSIONS_BOOLEANLITERAL_H_ */

src/ir/expressions/BooleanLiteralExpression.cpp

@@ -20,6 +20,10 @@ namespace storm {
                 // Nothing to do here.
             }
 
+            std::shared_ptr<BaseExpression> BooleanLiteralExpression::clone() const {
+                return std::shared_ptr<BaseExpression>(new BooleanLiteralExpression(*this));
+            }
+                                                       
             std::shared_ptr<BaseExpression> BooleanLiteralExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
                 return std::shared_ptr<BaseExpression>(new BooleanLiteralExpression(this->value));
             }

src/ir/expressions/BooleanLiteralExpression.h

@@ -33,6 +33,8 @@ namespace storm {
                  */
                 BooleanLiteralExpression(BooleanLiteralExpression const& booleanLiteralExpression);
                 
+                virtual std::shared_ptr<BaseExpression> clone() const override;
+                
                 virtual std::shared_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
                 
                 virtual bool getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override;

src/ir/expressions/DoubleConstantExpression.cpp

@@ -19,6 +19,10 @@ namespace storm {
                 // Nothing to do here.
             }
             
+            std::shared_ptr<BaseExpression> DoubleConstantExpression::clone() const {
+                return std::shared_ptr<BaseExpression>(new DoubleConstantExpression(*this));
+            }
+            
             std::shared_ptr<BaseExpression> DoubleConstantExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
                 return std::shared_ptr<BaseExpression>(new DoubleConstantExpression(*this));
             }

src/ir/expressions/DoubleConstantExpression.h

@@ -33,6 +33,8 @@ namespace storm {
                  */
                 DoubleConstantExpression(DoubleConstantExpression const& doubleConstantExpression);
                 
+                virtual std::shared_ptr<BaseExpression> clone() const override;
+                
                 virtual std::shared_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
                 
                 virtual double getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override;

src/ir/expressions/DoubleLiteral.h

@@ -1,62 +0,0 @@
-/*
- * DoubleLiteral.h
- *
- *  Created on: 03.01.2013
- *      Author: chris
- */
-
-#ifndef STORM_IR_EXPRESSIONS_DOUBLELITERAL_H_
-#define STORM_IR_EXPRESSIONS_DOUBLELITERAL_H_
-
-#include "src/ir/expressions/BaseExpression.h"
-
-#include "boost/lexical_cast.hpp"
-
-namespace storm {
-
-namespace ir {
-
-namespace expressions {
-
-class DoubleLiteral : public BaseExpression {
-public:
-	double value;
-
-	DoubleLiteral(double value) : BaseExpression(double_), value(value) {
-
-	}
-
-	virtual ~DoubleLiteral() {
-
-	}
-
-	virtual std::shared_ptr<BaseExpression> clone(const std::map<std::string, std::string>& renaming, const std::map<std::string, uint_fast64_t>& bools, const std::map<std::string, uint_fast64_t>& ints) override {
-		return std::shared_ptr<BaseExpression>(new DoubleLiteral(this->value));
-	}
-
-	virtual double getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override {
-		return value;
-	}
-
-	virtual void accept(ExpressionVisitor* visitor) override {
-		visitor->visit(this);
-	}
-
-	virtual std::string toString() const override {
-		return boost::lexical_cast<std::string>(value);
-	}
-	
-	virtual std::string dump(std::string prefix) const override {
-		std::stringstream result;
-		result << prefix << "DoubleLiteral " << this->toString() << std::endl;
-		return result.str();
-	}
-};
-
-}
-
-}
-
-}
-
-#endif /* STORM_IR_EXPRESSIONS_DOUBLELITERAL_H_ */

src/ir/expressions/DoubleLiteralExpression.cpp

@@ -22,6 +22,10 @@ namespace storm {
                 // Nothing to do here.
             }
             
+            std::shared_ptr<BaseExpression> DoubleLiteralExpression::clone() const {
+                return std::shared_ptr<BaseExpression>(new DoubleLiteralExpression(*this));
+            }
+
             std::shared_ptr<BaseExpression> DoubleLiteralExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
                 return std::shared_ptr<BaseExpression>(new DoubleLiteralExpression(this->value));
             }

src/ir/expressions/DoubleLiteralExpression.h

@@ -33,6 +33,8 @@ namespace storm {
                  */
                 DoubleLiteralExpression(DoubleLiteralExpression const& doubleLiteralExpression);
                 
+                virtual std::shared_ptr<BaseExpression> clone() const override;
+                
                 virtual std::shared_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
                 
                 virtual double getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override;

src/ir/expressions/IntegerConstantExpression.cpp

@@ -19,6 +19,10 @@ namespace storm {
                 // Nothing to do here.
             }
             
+            std::shared_ptr<BaseExpression> IntegerConstantExpression::clone() const {
+                return std::shared_ptr<BaseExpression>(new IntegerConstantExpression(*this));
+            }
+            
             std::shared_ptr<BaseExpression> IntegerConstantExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
                 return std::shared_ptr<BaseExpression>(new IntegerConstantExpression(*this));
             }

src/ir/expressions/IntegerConstantExpression.h

@@ -33,6 +33,8 @@ namespace storm {
                  */
                 IntegerConstantExpression(IntegerConstantExpression const& integerConstantExpression);
                 
+                virtual std::shared_ptr<BaseExpression> clone() const override;
+                
                 virtual std::shared_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
                 
                 virtual double getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override;

src/ir/expressions/IntegerLiteral.h

@@ -1,58 +0,0 @@
-/*
- * IntegerLiteral.h
- *
- *  Created on: 03.01.2013
- *      Author: chris
- */
-
-#ifndef STORM_IR_EXPRESSIONS_INTEGERLITERAL_H_
-#define STORM_IR_EXPRESSIONS_INTEGERLITERAL_H_
-
-#include "src/ir/expressions/BaseExpression.h"
-
-namespace storm {
-
-namespace ir {
-
-namespace expressions {
-
-class IntegerLiteral : public BaseExpression {
-public:
-	int_fast64_t value;
-
-	IntegerLiteral(int_fast64_t value) : BaseExpression(int_), value(value) {
-	}
-
-	virtual ~IntegerLiteral() {
-	}
-
-	virtual std::shared_ptr<BaseExpression> clone(const std::map<std::string, std::string>& renaming, const std::map<std::string, uint_fast64_t>& bools, const std::map<std::string, uint_fast64_t>& ints) override {
-		return std::shared_ptr<BaseExpression>(new IntegerLiteral(this->value));
-	}
-
-	virtual int_fast64_t getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override {
-		return value;
-	}
-
-	virtual void accept(ExpressionVisitor* visitor) override {
-		visitor->visit(this);
-	}
-	
-	virtual std::string toString() const override {
-		return boost::lexical_cast<std::string>(value);
-	}
-
-	virtual std::string dump(std::string prefix) const override {
-		std::stringstream result;
-		result << prefix << "IntegerLiteral " << this->toString() << std::endl;
-		return result.str();
-	}
-};
-
-}
-
-}
-
-}
-
-#endif /* STORM_IR_EXPRESSIONS_INTEGERLITERAL_H_ */

src/ir/expressions/IntegerLiteralExpression.cpp

@@ -22,6 +22,10 @@ namespace storm {
                 // Nothing to do here.
             }
             
+            std::shared_ptr<BaseExpression> IntegerLiteralExpression::clone() const {
+                return std::shared_ptr<BaseExpression>(new IntegerLiteralExpression(*this));
+            }
+            
             std::shared_ptr<BaseExpression> IntegerLiteralExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
                 return std::shared_ptr<BaseExpression>(new IntegerLiteralExpression(this->value));
             }

src/ir/expressions/IntegerLiteralExpression.h

@@ -33,6 +33,8 @@ namespace storm {
                  */
                 IntegerLiteralExpression(IntegerLiteralExpression const& integerLiteralExpression);
                 
+                virtual std::shared_ptr<BaseExpression> clone() const override;
+                
                 virtual std::shared_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
                 
                 virtual double getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override;

src/ir/expressions/UnaryBooleanFunctionExpression.cpp

@@ -21,6 +21,10 @@ namespace storm {
                 // Nothing to do here.
             }
             
+            std::shared_ptr<BaseExpression> UnaryBooleanFunctionExpression::clone() const {
+                return std::shared_ptr<BaseExpression>(new UnaryBooleanFunctionExpression(this->getChild()->clone(), functionType));
+            }
+            
             std::shared_ptr<BaseExpression> UnaryBooleanFunctionExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
                 return std::shared_ptr<BaseExpression>(new UnaryBooleanFunctionExpression(this->getChild()->clone(renaming, variableState), this->functionType));
             }

src/ir/expressions/UnaryBooleanFunctionExpression.h

@@ -39,6 +39,8 @@ namespace storm {
                  */
                 UnaryBooleanFunctionExpression(UnaryBooleanFunctionExpression const& unaryBooleanFunctionExpression);
                 
+                virtual std::shared_ptr<BaseExpression> clone() const override;
+                
                 virtual std::shared_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
 
                 /*!

src/ir/expressions/UnaryNumericalFunctionExpression.cpp

@@ -19,6 +19,10 @@ namespace storm {
                 // Nothing to do here.
             }
             
+            std::shared_ptr<BaseExpression> UnaryNumericalFunctionExpression::clone() const {
+                return std::shared_ptr<BaseExpression>(new UnaryNumericalFunctionExpression(this->getType(), this->getChild()->clone(), functionType));
+            }
+            
             std::shared_ptr<BaseExpression> UnaryNumericalFunctionExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
                 return std::shared_ptr<BaseExpression>(new UnaryNumericalFunctionExpression(this->getType(), this->getChild()->clone(renaming, variableState), this->functionType));
             }

src/ir/expressions/UnaryNumericalFunctionExpression.h

@@ -39,6 +39,8 @@ namespace storm {
                  */
                 UnaryNumericalFunctionExpression(UnaryNumericalFunctionExpression const& unaryNumericalFunctionExpression);
                 
+                virtual std::shared_ptr<BaseExpression> clone() const override;
+                
                 virtual std::shared_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
                 
                 virtual int_fast64_t getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override;

src/ir/expressions/VariableExpression.cpp

@@ -26,6 +26,10 @@ namespace storm {
                 // Nothing to do here.
             }
             
+            std::shared_ptr<BaseExpression> VariableExpression::clone() const {
+                return std::shared_ptr<BaseExpression>(new VariableExpression(*this));
+            }
+            
             std::shared_ptr<BaseExpression> VariableExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
                 // Perform the proper cloning.
                 auto renamingPair = renaming.find(this->variableName);

src/ir/expressions/VariableExpression.h

@@ -52,6 +52,8 @@ namespace storm {
                  */
                 VariableExpression(VariableExpression const& variableExpression);
                 
+                virtual std::shared_ptr<BaseExpression> clone() const override;
+                
 				virtual std::shared_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
 				
 				virtual void accept(ExpressionVisitor* visitor) override;

src/utility/IRUtility.h

@@ -0,0 +1,54 @@
+/*
+ * IRUtility.h
+ *
+ *  Created on: 05.10.2013
+ *      Author: Christian Dehnert
+ */
+
+#ifndef STORM_UTILITY_IRUTILITY_H_
+#define STORM_UTILITY_IRUTILITY_H_
+
+#include <IR.h>
+
+#include "log4cplus/logger.h"
+#include "log4cplus/loggingmacros.h"
+
+extern log4cplus::Logger logger;
+
+namespace storm {
+    namespace utility {
+        namespace ir {
+
+            /*!
+             * Computes the weakest precondition of the given boolean expression wrt. the given updates. The weakest
+             * precondition is the most liberal expression that must hold in order to satisfy the given boolean
+             * expression after performing the updates. The updates must be disjoint in the sense that they must not
+             * assign an expression to a variable twice or more.
+             *
+             * @param expression The expression for which to build the weakest precondition.
+             * @param update The update with respect to which to compute the weakest precondition.
+             */
+            std::shared_ptr<storm::ir::expressions::BaseExpression> getWeakestPrecondition(std::shared_ptr<storm::ir::expressions::BaseExpression> booleanExpression, std::vector<storm::ir::Update> const& updates) {
+                std::map<std::string, std::shared_ptr<storm::ir::expressions::BaseExpression>> variableToExpressionMap;
+                
+                // Construct the full substitution we need to perform later.
+                for (auto const& update : updates) {
+                    for (uint_fast64_t assignmentIndex = 0; assignmentIndex < update.getNumberOfAssignments(); ++assignmentIndex) {
+                        storm::ir::Assignment const& update.getAssignment(assignmentIndex);
+                        
+                        variableToExpressionMap[assignment.getVariableName()] = assignment.getExpression();
+                    }
+                }
+                
+                // Copy the given expression and apply the substitution.
+                std::shared_ptr<storm::ir::expressions::BaseExpression> copiedExpression = booleanExpression->clone();
+                copiedExpression->substitute(variableToExpressionMap);
+                
+                return copiedExpression;
+            }
+            
+        } // namespace ir
+    } // namespace utility
+} // namespace storm
+
+#endif /* STORM_UTILITY_IRUTILITY_H_ */