Merge branch 'master' into SmtSolvers

Former-commit-id: c3550e8ad9

src/parser/PrismParser.cpp

@@ -572,7 +572,7 @@ namespace storm {
         storm::prism::Constant PrismParser::createUndefinedBooleanConstant(std::string const& newConstant) const {
             if (!this->secondRun) {
                 LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
-                this->identifiers_.add(newConstant, storm::expressions::Expression::createBooleanConstant(newConstant));
+                this->identifiers_.add(newConstant, storm::expressions::Expression::createBooleanVariable(newConstant));
             }
             return storm::prism::Constant(storm::expressions::ExpressionReturnType::Bool, newConstant, this->getFilename());
         }
@@ -580,7 +580,7 @@ namespace storm {
         storm::prism::Constant PrismParser::createUndefinedIntegerConstant(std::string const& newConstant) const {
             if (!this->secondRun) {
                 LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
-                this->identifiers_.add(newConstant, storm::expressions::Expression::createIntegerConstant(newConstant));
+                this->identifiers_.add(newConstant, storm::expressions::Expression::createIntegerVariable(newConstant));
             }
             return storm::prism::Constant(storm::expressions::ExpressionReturnType::Int, newConstant, this->getFilename());
         }
@@ -588,7 +588,7 @@ namespace storm {
         storm::prism::Constant PrismParser::createUndefinedDoubleConstant(std::string const& newConstant) const {
             if (!this->secondRun) {
                 LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
-                this->identifiers_.add(newConstant, storm::expressions::Expression::createDoubleConstant(newConstant));
+                this->identifiers_.add(newConstant, storm::expressions::Expression::createDoubleVariable(newConstant));
             }
             return storm::prism::Constant(storm::expressions::ExpressionReturnType::Double, newConstant, this->getFilename());
         }
@@ -596,7 +596,7 @@ namespace storm {
         storm::prism::Constant PrismParser::createDefinedBooleanConstant(std::string const& newConstant, storm::expressions::Expression expression) const {
             if (!this->secondRun) {
                 LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
-                this->identifiers_.add(newConstant, storm::expressions::Expression::createBooleanConstant(newConstant));
+                this->identifiers_.add(newConstant, storm::expressions::Expression::createBooleanVariable(newConstant));
             }
             return storm::prism::Constant(storm::expressions::ExpressionReturnType::Bool, newConstant, expression, this->getFilename());
         }
@@ -604,7 +604,7 @@ namespace storm {
         storm::prism::Constant PrismParser::createDefinedIntegerConstant(std::string const& newConstant, storm::expressions::Expression expression) const {
             if (!this->secondRun) {
                 LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
-                this->identifiers_.add(newConstant, storm::expressions::Expression::createIntegerConstant(newConstant));
+                this->identifiers_.add(newConstant, storm::expressions::Expression::createIntegerVariable(newConstant));
             }
             return storm::prism::Constant(storm::expressions::ExpressionReturnType::Int, newConstant, expression, this->getFilename());
         }
@@ -612,7 +612,7 @@ namespace storm {
         storm::prism::Constant PrismParser::createDefinedDoubleConstant(std::string const& newConstant, storm::expressions::Expression expression) const {
             if (!this->secondRun) {
                 LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
-                this->identifiers_.add(newConstant, storm::expressions::Expression::createDoubleConstant(newConstant));
+                this->identifiers_.add(newConstant, storm::expressions::Expression::createDoubleVariable(newConstant));
             }
             return storm::prism::Constant(storm::expressions::ExpressionReturnType::Double, newConstant, expression, this->getFilename());
         }

src/storage/expressions/BaseExpression.cpp

@@ -1,6 +1,7 @@
 #include "src/storage/expressions/BaseExpression.h"
 #include "src/exceptions/ExceptionMacros.h"
 #include "src/exceptions/InvalidTypeException.h"
+#include "src/exceptions/InvalidAccessException.h"
 
 namespace storm {
     namespace expressions {        
@@ -36,10 +37,30 @@ namespace storm {
             LOG_THROW(false, storm::exceptions::InvalidTypeException, "Unable to evaluate expression as double.");
         }
         
-        bool BaseExpression::isConstant() const {
+        uint_fast64_t BaseExpression::getArity() const {
+            return 0;
+        }
+        
+        std::shared_ptr<BaseExpression const> BaseExpression::getOperand(uint_fast64_t operandIndex) const {
+            LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to access operand " << operandIndex << " in expression of arity 0.");
+        }
+        
+        std::string const& BaseExpression::getIdentifier() const {
+            LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to access identifier of non-constant, non-variable expression.");
+        }
+        
+        bool BaseExpression::containsVariables() const {
             return false;
         }
-
+        
+        bool BaseExpression::isLiteral() const {
+            return false;
+        }
+        
+        bool BaseExpression::isVariable() const {
+            return false;
+        }
+        
         bool BaseExpression::isTrue() const {
             return false;
         }

src/storage/expressions/BaseExpression.h

@@ -74,11 +74,48 @@ namespace storm {
             virtual double evaluateAsDouble(Valuation const* valuation = nullptr) const;
 
             /*!
-             * Retrieves whether the expression is constant, i.e., contains no variables or undefined constants.
+             * Returns the arity of the expression.
              *
-             * @return True iff the expression is constant.
+             * @return The arity of the expression.
              */
-            virtual bool isConstant() const;
+            virtual uint_fast64_t getArity() const;
+            
+            /*!
+             * Retrieves the given operand from the expression.
+             *
+             * @param operandIndex The index of the operand to retrieve. This must be lower than the arity of the expression.
+             * @return The operand at the given index.
+             */
+            virtual std::shared_ptr<BaseExpression const> getOperand(uint_fast64_t operandIndex) const;
+            
+            /*!
+             * Retrieves the identifier associated with this expression. This is only legal to call if the expression
+             * is a variable.
+             *
+             * @return The identifier associated with this expression.
+             */
+            virtual std::string const& getIdentifier() const;
+            
+            /*!
+             * Retrieves whether the expression contains a variable.
+             *
+             * @return True iff the expression contains a variable.
+             */
+            virtual bool containsVariables() const;
+            
+            /*!
+             * Retrieves whether the expression is a literal.
+             *
+             * @return True iff the expression is a literal.
+             */
+            virtual bool isLiteral() const;
+            
+            /*!
+             * Retrieves whether the expression is a variable.
+             *
+             * @return True iff the expression is a variable.
+             */
+            virtual bool isVariable() const;
             
             /*!
              * Checks if the expression is equal to the boolean literal true.
@@ -101,13 +138,6 @@ namespace storm {
              */
             virtual std::set<std::string> getVariables() const = 0;
             
-            /*!
-             * Retrieves the set of all constants that appear in the expression.
-             *
-             * @return The set of all constants that appear in the expression.
-             */
-            virtual std::set<std::string> getConstants() const = 0;
-            
             /*!
              * Simplifies the expression according to some simple rules.
              *

src/storage/expressions/BinaryBooleanFunctionExpression.cpp

@@ -30,7 +30,7 @@ namespace storm {
             
             return result;
         }
-        
+                
         std::shared_ptr<BaseExpression const> BinaryBooleanFunctionExpression::simplify() const {
             std::shared_ptr<BaseExpression const> firstOperandSimplified = this->getFirstOperand()->simplify();
             std::shared_ptr<BaseExpression const> secondOperandSimplified = this->getSecondOperand()->simplify();

src/storage/expressions/BinaryExpression.cpp

@@ -1,13 +1,16 @@
 #include "src/storage/expressions/BinaryExpression.h"
 
+#include "src/exceptions/ExceptionMacros.h"
+#include "src/exceptions/InvalidAccessException.h"
+
 namespace storm {
     namespace expressions {
         BinaryExpression::BinaryExpression(ExpressionReturnType returnType, std::shared_ptr<BaseExpression const> const& firstOperand, std::shared_ptr<BaseExpression const> const& secondOperand) : BaseExpression(returnType), firstOperand(firstOperand), secondOperand(secondOperand) {
             // Intentionally left empty.
         }
-                
-        bool BinaryExpression::isConstant() const {
-            return this->getFirstOperand()->isConstant() && this->getSecondOperand()->isConstant();
+        
+        bool BinaryExpression::containsVariables() const {
+            return this->getFirstOperand()->containsVariables() || this->getSecondOperand()->containsVariables();
         }
         
         std::set<std::string> BinaryExpression::getVariables() const {
@@ -17,13 +20,6 @@ namespace storm {
             return firstVariableSet;
         }
         
-        std::set<std::string> BinaryExpression::getConstants() const {
-            std::set<std::string> firstConstantSet = this->getFirstOperand()->getVariables();
-            std::set<std::string> secondConstantSet = this->getSecondOperand()->getVariables();
-            firstConstantSet.insert(secondConstantSet.begin(), secondConstantSet.end());
-            return firstConstantSet;
-        }
-        
         std::shared_ptr<BaseExpression const> const& BinaryExpression::getFirstOperand() const {
             return this->firstOperand;
         }
@@ -31,5 +27,18 @@ namespace storm {
         std::shared_ptr<BaseExpression const> const& BinaryExpression::getSecondOperand() const {
             return this->secondOperand;
         }
+        
+        uint_fast64_t BinaryExpression::getArity() const {
+            return 2;
+        }
+        
+        std::shared_ptr<BaseExpression const> BinaryExpression::getOperand(uint_fast64_t operandIndex) const {
+            LOG_THROW(operandIndex < 2, storm::exceptions::InvalidAccessException, "Unable to access operand " << operandIndex << " in expression of arity 2.");
+            if (operandIndex == 1) {
+                return this->getFirstOperand();
+            } else {
+                return this->getSecondOperand();
+            }
+        }
     }
 }

src/storage/expressions/BinaryExpression.h

@@ -30,9 +30,10 @@ namespace storm {
             virtual ~BinaryExpression() = default;
 
             // Override base class methods.
-            virtual bool isConstant() const override;
+            virtual bool containsVariables() const override;
+            virtual uint_fast64_t getArity() const override;
+            virtual std::shared_ptr<BaseExpression const> getOperand(uint_fast64_t operandIndex) const override;
             virtual std::set<std::string> getVariables() const override;
-            virtual std::set<std::string> getConstants() const override;
             
             /*!
              * Retrieves the first operand of the expression.

src/storage/expressions/BooleanConstantExpression.cpp

@@ -1,23 +0,0 @@
-#include "src/storage/expressions/BooleanConstantExpression.h"
-#include "src/exceptions/ExceptionMacros.h"
-
-namespace storm {
-    namespace expressions {
-        BooleanConstantExpression::BooleanConstantExpression(std::string const& constantName) : ConstantExpression(ExpressionReturnType::Bool, constantName) {
-            // Intentionally left empty.
-        }
-                
-        bool BooleanConstantExpression::evaluateAsBool(Valuation const* valuation) const {
-            LOG_ASSERT(valuation != nullptr, "Evaluating expressions with unknowns without valuation.");
-            return valuation->getBooleanValue(this->getConstantName());
-        }
-        
-        void BooleanConstantExpression::accept(ExpressionVisitor* visitor) const {
-            visitor->visit(this);
-        }
-        
-        std::shared_ptr<BaseExpression const> BooleanConstantExpression::simplify() const {
-            return this->shared_from_this();
-        }
-    }
-}

src/storage/expressions/BooleanConstantExpression.h

@@ -1,35 +0,0 @@
-#ifndef STORM_STORAGE_EXPRESSIONS_BOOLEANCONSTANTEXPRESSION_H_
-#define STORM_STORAGE_EXPRESSIONS_BOOLEANCONSTANTEXPRESSION_H_
-
-#include "src/storage/expressions/ConstantExpression.h"
-#include "src/utility/OsDetection.h"
-
-namespace storm {
-    namespace expressions {
-        class BooleanConstantExpression : public ConstantExpression {
-        public:
-            /*!
-             * Creates a boolean constant expression with the given constant name.
-             *
-             * @param constantName The name of the boolean constant associated with this expression.
-             */
-            BooleanConstantExpression(std::string const& constantName);
-            
-            // Instantiate constructors and assignments with their default implementations.
-            BooleanConstantExpression(BooleanConstantExpression const& other) = default;
-            BooleanConstantExpression& operator=(BooleanConstantExpression const& other) = default;
-#ifndef WINDOWS
-            BooleanConstantExpression(BooleanConstantExpression&&) = default;
-            BooleanConstantExpression& operator=(BooleanConstantExpression&&) = default;
-#endif
-            virtual ~BooleanConstantExpression() = default;
-            
-            // Override base class methods.
-            virtual bool evaluateAsBool(Valuation const* valuation = nullptr) const override;
-            virtual void accept(ExpressionVisitor* visitor) const override;
-            virtual std::shared_ptr<BaseExpression const> simplify() const override;
-        };
-    }
-}
-
-#endif /* STORM_STORAGE_EXPRESSIONS_BOOLEANCONSTANTEXPRESSION_H_ */

src/storage/expressions/BooleanLiteralExpression.cpp

@@ -10,7 +10,7 @@ namespace storm {
             return this->getValue();
         }
         
-        bool BooleanLiteralExpression::isConstant() const {
+        bool BooleanLiteralExpression::isLiteral() const {
             return true;
         }
         
@@ -26,10 +26,6 @@ namespace storm {
             return std::set<std::string>();
         }
         
-        std::set<std::string> BooleanLiteralExpression::getConstants() const {
-            return std::set<std::string>();
-        }
-        
         std::shared_ptr<BaseExpression const> BooleanLiteralExpression::simplify() const {
             return this->shared_from_this();
         }

src/storage/expressions/BooleanLiteralExpression.h

@@ -26,11 +26,10 @@ namespace storm {
 
             // Override base class methods.
             virtual bool evaluateAsBool(Valuation const* valuation = nullptr) const override;
-            virtual bool isConstant() const override;
+            virtual bool isLiteral() const override;
             virtual bool isTrue() const override;
             virtual bool isFalse() const override;
             virtual std::set<std::string> getVariables() const override;
-            virtual std::set<std::string> getConstants() const override;
             virtual std::shared_ptr<BaseExpression const> simplify() const override;
             virtual void accept(ExpressionVisitor* visitor) const override;
             

src/storage/expressions/ConstantExpression.cpp

@@ -1,25 +0,0 @@
-#include "src/storage/expressions/ConstantExpression.h"
-
-namespace storm {
-    namespace expressions {
-        ConstantExpression::ConstantExpression(ExpressionReturnType returnType, std::string const& constantName) : BaseExpression(returnType), constantName(constantName) {
-            // Intentionally left empty.
-        }
-        
-        std::set<std::string> ConstantExpression::getVariables() const {
-            return std::set<std::string>();
-        }
-        
-        std::set<std::string> ConstantExpression::getConstants() const {
-            return {this->getConstantName()};
-        }
-        
-        std::string const& ConstantExpression::getConstantName() const {
-            return this->constantName;
-        }
-        
-        void ConstantExpression::printToStream(std::ostream& stream) const {
-            stream << this->getConstantName();
-        }
-    }
-}

src/storage/expressions/ConstantExpression.h

@@ -1,50 +0,0 @@
-#ifndef STORM_STORAGE_EXPRESSIONS_CONSTANTEXPRESSION_H_
-#define STORM_STORAGE_EXPRESSIONS_CONSTANTEXPRESSION_H_
-
-#include "src/storage/expressions/BaseExpression.h"
-#include "src/utility/OsDetection.h"
-
-namespace storm {
-    namespace expressions {
-        class ConstantExpression : public BaseExpression {
-        public:
-            /*!
-             * Creates a constant expression with the given return type and constant name.
-             *
-             * @param returnType The return type of the expression.
-             * @param constantName The name of the constant associated with this expression.
-             */
-            ConstantExpression(ExpressionReturnType returnType, std::string const& constantName);
-            
-            // Instantiate constructors and assignments with their default implementations.
-            ConstantExpression(ConstantExpression const& other) = default;
-            ConstantExpression& operator=(ConstantExpression const& other) = default;
-#ifndef WINDOWS
-            ConstantExpression(ConstantExpression&&) = default;
-            ConstantExpression& operator=(ConstantExpression&&) = default;
-#endif
-            virtual ~ConstantExpression() = default;
-            
-            // Override base class methods.
-            virtual std::set<std::string> getVariables() const override;
-            virtual std::set<std::string> getConstants() const override;
-            
-            /*!
-             * Retrieves the name of the constant.
-             *
-             * @return The name of the constant.
-             */
-            std::string const& getConstantName() const;
-
-        protected:
-            // Override base class method.
-            virtual void printToStream(std::ostream& stream) const override;
-            
-        private:
-            // The name of the constant.
-            std::string constantName;
-        };
-    }
-}
-
-#endif /* STORM_STORAGE_EXPRESSIONS_CONSTANTEXPRESSION_H_ */

src/storage/expressions/DoubleConstantExpression.cpp

@@ -1,23 +0,0 @@
-#include "src/storage/expressions/DoubleConstantExpression.h"
-#include "src/exceptions/ExceptionMacros.h"
-
-namespace storm {
-    namespace expressions {
-        DoubleConstantExpression::DoubleConstantExpression(std::string const& constantName) : ConstantExpression(ExpressionReturnType::Double, constantName) {
-            // Intentionally left empty.
-        }
-        
-        double DoubleConstantExpression::evaluateAsDouble(Valuation const* valuation) const {
-            LOG_ASSERT(valuation != nullptr, "Evaluating expressions with unknowns without valuation.");
-            return valuation->getDoubleValue(this->getConstantName());
-        }
-        
-        std::shared_ptr<BaseExpression const> DoubleConstantExpression::simplify() const {
-            return this->shared_from_this();
-        }
-        
-        void DoubleConstantExpression::accept(ExpressionVisitor* visitor) const {
-            visitor->visit(this);
-        }
-    }
-}

src/storage/expressions/DoubleConstantExpression.h

@@ -1,35 +0,0 @@
-#ifndef STORM_STORAGE_EXPRESSIONS_DOUBLECONSTANTEXPRESSION_H_
-#define STORM_STORAGE_EXPRESSIONS_DOUBLECONSTANTEXPRESSION_H_
-
-#include "src/storage/expressions/ConstantExpression.h"
-#include "src/utility/OsDetection.h"
-
-namespace storm {
-    namespace expressions {
-        class DoubleConstantExpression : public ConstantExpression {
-        public:
-            /*!
-             * Creates a double constant expression with the given constant name.
-             *
-             * @param constantName The name of the double constant associated with this expression.
-             */
-            DoubleConstantExpression(std::string const& constantName);
-            
-            // Instantiate constructors and assignments with their default implementations.
-            DoubleConstantExpression(DoubleConstantExpression const& other) = default;
-            DoubleConstantExpression& operator=(DoubleConstantExpression const& other) = default;
-#ifndef WINDOWS
-            DoubleConstantExpression(DoubleConstantExpression&&) = default;
-            DoubleConstantExpression& operator=(DoubleConstantExpression&&) = default;
-#endif
-            virtual ~DoubleConstantExpression() = default;
-            
-            // Override base class methods.
-            virtual double evaluateAsDouble(Valuation const* valuation = nullptr) const override;
-            virtual void accept(ExpressionVisitor* visitor) const override;
-            virtual std::shared_ptr<BaseExpression const> simplify() const override;
-        };
-    }
-}
-
-#endif /* STORM_STORAGE_EXPRESSIONS_DOUBLECONSTANTEXPRESSION_H_ */

src/storage/expressions/DoubleLiteralExpression.cpp

@@ -10,7 +10,7 @@ namespace storm {
             return this->getValue();
         }
         
-        bool DoubleLiteralExpression::isConstant() const {
+        bool DoubleLiteralExpression::isLiteral() const {
             return true;
         }
         
@@ -18,10 +18,6 @@ namespace storm {
             return std::set<std::string>();
         }
         
-        std::set<std::string> DoubleLiteralExpression::getConstants() const {
-            return std::set<std::string>();
-        }
-        
         std::shared_ptr<BaseExpression const> DoubleLiteralExpression::simplify() const {
             return this->shared_from_this();
         }

src/storage/expressions/DoubleLiteralExpression.h

@@ -26,9 +26,8 @@ namespace storm {
             
             // Override base class methods.
             virtual double evaluateAsDouble(Valuation const* valuation = nullptr) const override;
-            virtual bool isConstant() const override;
+            virtual bool isLiteral() const override;
             virtual std::set<std::string> getVariables() const override;
-            virtual std::set<std::string> getConstants() const override;
             virtual std::shared_ptr<BaseExpression const> simplify() const override;
             virtual void accept(ExpressionVisitor* visitor) const override;
 

src/storage/expressions/Expression.cpp

@@ -5,23 +5,10 @@
 #include "src/storage/expressions/SubstitutionVisitor.h"
 #include "src/storage/expressions/IdentifierSubstitutionVisitor.h"
 #include "src/storage/expressions/TypeCheckVisitor.h"
+#include "src/storage/expressions/Expressions.h"
 #include "src/exceptions/InvalidTypeException.h"
 #include "src/exceptions/ExceptionMacros.h"
 
-#include "src/storage/expressions/IfThenElseExpression.h"
-#include "src/storage/expressions/BinaryBooleanFunctionExpression.h"
-#include "src/storage/expressions/BinaryNumericalFunctionExpression.h"
-#include "src/storage/expressions/BinaryRelationExpression.h"
-#include "src/storage/expressions/BooleanConstantExpression.h"
-#include "src/storage/expressions/IntegerConstantExpression.h"
-#include "src/storage/expressions/DoubleConstantExpression.h"
-#include "src/storage/expressions/BooleanLiteralExpression.h"
-#include "src/storage/expressions/IntegerLiteralExpression.h"
-#include "src/storage/expressions/DoubleLiteralExpression.h"
-#include "src/storage/expressions/VariableExpression.h"
-#include "src/storage/expressions/UnaryBooleanFunctionExpression.h"
-#include "src/storage/expressions/UnaryNumericalFunctionExpression.h"
-
 namespace storm {
     namespace expressions {
         Expression::Expression(std::shared_ptr<BaseExpression const> const& expressionPtr) : expressionPtr(expressionPtr) {
@@ -68,8 +55,28 @@ namespace storm {
             return Expression(this->getBaseExpression().simplify());
         }
         
-        bool Expression::isConstant() const {
-            return this->getBaseExpression().isConstant();
+        uint_fast64_t Expression::getArity() const {
+            return this->getBaseExpression().getArity();
+        }
+        
+        Expression Expression::getOperand(uint_fast64_t operandIndex) const {
+            return Expression(this->getBaseExpression().getOperand(operandIndex));
+        }
+        
+        std::string const& Expression::getIdentifier() const {
+            return this->getBaseExpression().getIdentifier();
+        }
+        
+        bool Expression::containsVariables() const {
+            return this->getBaseExpression().containsVariables();
+        }
+        
+        bool Expression::isLiteral() const {
+            return this->getBaseExpression().isLiteral();
+        }
+        
+        bool Expression::isVariable() const {
+            return this->getBaseExpression().isVariable();
         }
         
         bool Expression::isTrue() const {
@@ -84,17 +91,6 @@ namespace storm {
             return this->getBaseExpression().getVariables();
         }
         
-        std::set<std::string> Expression::getConstants() const {
-            return this->getBaseExpression().getConstants();
-        }
-        
-        std::set<std::string> Expression::getIdentifiers() const {
-            std::set<std::string> result = this->getConstants();
-            std::set<std::string> variables = this->getVariables();
-            result.insert(variables.begin(), variables.end());
-            return result;
-        }
-        
         BaseExpression const& Expression::getBaseExpression() const {
             return *this->expressionPtr;
         }
@@ -151,18 +147,6 @@ namespace storm {
             return Expression(std::shared_ptr<BaseExpression>(new VariableExpression(ExpressionReturnType::Undefined, variableName)));
         }
         
-        Expression Expression::createBooleanConstant(std::string const& constantName) {
-            return Expression(std::shared_ptr<BaseExpression>(new BooleanConstantExpression(constantName)));
-        }
-        
-        Expression Expression::createIntegerConstant(std::string const& constantName) {
-            return Expression(std::shared_ptr<BaseExpression>(new IntegerConstantExpression(constantName)));
-        }
-        
-        Expression Expression::createDoubleConstant(std::string const& constantName) {
-            return Expression(std::shared_ptr<BaseExpression>(new DoubleConstantExpression(constantName)));
-        }
-        
         Expression Expression::operator+(Expression const& other) const {
             LOG_THROW(this->hasNumericalReturnType() && other.hasNumericalReturnType(), storm::exceptions::InvalidTypeException, "Operator '+' requires numerical operands.");
             return Expression(std::shared_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(this->getReturnType() == ExpressionReturnType::Int && other.getReturnType() == ExpressionReturnType::Int ? ExpressionReturnType::Int : ExpressionReturnType::Double, this->getBaseExpressionPointer(), other.getBaseExpressionPointer(), BinaryNumericalFunctionExpression::OperatorType::Plus)));

src/storage/expressions/Expression.h

@@ -39,9 +39,6 @@ namespace storm {
             static Expression createIntegerVariable(std::string const& variableName);
             static Expression createDoubleVariable(std::string const& variableName);
             static Expression createUndefinedVariable(std::string const& variableName);
-            static Expression createBooleanConstant(std::string const& constantName);
-            static Expression createIntegerConstant(std::string const& constantName);
-            static Expression createDoubleConstant(std::string const& constantName);
             
             // Provide operator overloads to conveniently construct new expressions from other expressions.
             Expression operator+(Expression const& other) const;
@@ -127,9 +124,8 @@ namespace storm {
             void check(std::unordered_map<std::string, storm::expressions::ExpressionReturnType> const& identifierToTypeMap) const;
             
             /*!
-             * Evaluates the expression under the valuation of unknowns (variables and constants) given by the
-             * valuation and returns the resulting boolean value. If the return type of the expression is not a boolean
-             * an exception is thrown.
+             * Evaluates the expression under the valuation of variables given by the valuation and returns the
+             * resulting boolean value. If the return type of the expression is not a boolean an exception is thrown.
              *
              * @param valuation The valuation of unknowns under which to evaluate the expression.
              * @return The boolean value of the expression under the given valuation.
@@ -137,9 +133,8 @@ namespace storm {
             bool evaluateAsBool(Valuation const* valuation = nullptr) const;
             
             /*!
-             * Evaluates the expression under the valuation of unknowns (variables and constants) given by the
-             * valuation and returns the resulting integer value. If the return type of the expression is not an integer
-             * an exception is thrown.
+             * Evaluates the expression under the valuation of variables given by the valuation and returns the
+             * resulting integer value. If the return type of the expression is not an integer an exception is thrown.
              *
              * @param valuation The valuation of unknowns under which to evaluate the expression.
              * @return The integer value of the expression under the given valuation.
@@ -147,9 +142,8 @@ namespace storm {
             int_fast64_t evaluateAsInt(Valuation const* valuation = nullptr) const;
             
             /*!
-             * Evaluates the expression under the valuation of unknowns (variables and constants) given by the
-             * valuation and returns the resulting double value. If the return type of the expression is not a double
-             * an exception is thrown.
+             * Evaluates the expression under the valuation of variables given by the valuation and returns the
+             * resulting double value. If the return type of the expression is not a double an exception is thrown.
              *
              * @param valuation The valuation of unknowns under which to evaluate the expression.
              * @return The double value of the expression under the given valuation.
@@ -164,11 +158,48 @@ namespace storm {
             Expression simplify();
             
             /*!
-             * Retrieves whether the expression is constant, i.e., contains no variables or undefined constants.
+             * Retrieves the arity of the expression.
              *
-             * @return True iff the expression is constant.
+             * @return The arity of the expression.
              */
-            bool isConstant() const;
+            uint_fast64_t getArity() const;
+            
+            /*!
+             * Retrieves the given operand from the expression.
+             *
+             * @param operandIndex The index of the operand to retrieve. This must be lower than the arity of the expression.
+             * @return The operand at the given index.
+             */
+            Expression getOperand(uint_fast64_t operandIndex) const;
+            
+            /*!
+             * Retrieves the identifier associated with this expression. This is only legal to call if the expression
+             * is a variable.
+             *
+             * @return The identifier associated with this expression.
+             */
+            std::string const& getIdentifier() const;
+            
+            /*!
+             * Retrieves whether the expression contains a variable.
+             *
+             * @return True iff the expression contains a variable.
+             */
+            bool containsVariables() const;
+            
+            /*!
+             * Retrieves whether the expression is a literal.
+             *
+             * @return True iff the expression is a literal.
+             */
+            bool isLiteral() const;
+            
+            /*!
+             * Retrieves whether the expression is a variable.
+             *
+             * @return True iff the expression is a variable.
+             */
+            bool isVariable() const;
             
             /*!
              * Checks if the expression is equal to the boolean literal true.
@@ -191,20 +222,6 @@ namespace storm {
              */
             std::set<std::string> getVariables() const;
             
-            /*!
-             * Retrieves the set of all constants that appear in the expression.
-             *
-             * @return The set of all constants that appear in the expression.
-             */
-            std::set<std::string> getConstants() const;
-            
-            /*!
-             * Retrieves the set of all identifiers (constants and variables) that appear in the expression.
-             *
-             * @return The est of all identifiers that appear in the expression.
-             */
-            std::set<std::string> getIdentifiers() const;
-            
             /*!
              * Retrieves the base expression underlying this expression object. Note that prior to calling this, the
              * expression object must be properly initialized.

src/storage/expressions/ExpressionVisitor.h

@@ -8,10 +8,6 @@ namespace storm {
         class BinaryBooleanFunctionExpression;
         class BinaryNumericalFunctionExpression;
         class BinaryRelationExpression;
-        class BooleanConstantExpression;
-        class DoubleConstantExpression;
-        class IntegerConstantExpression;
-        class IntegerConstantExpression;
         class VariableExpression;
         class UnaryBooleanFunctionExpression;
         class UnaryNumericalFunctionExpression;
@@ -25,9 +21,6 @@ namespace storm {
             virtual void visit(BinaryBooleanFunctionExpression const* expression) = 0;
             virtual void visit(BinaryNumericalFunctionExpression const* expression) = 0;
             virtual void visit(BinaryRelationExpression const* expression) = 0;
-            virtual void visit(BooleanConstantExpression const* expression) = 0;
-            virtual void visit(DoubleConstantExpression const* expression) = 0;
-            virtual void visit(IntegerConstantExpression const* expression) = 0;
             virtual void visit(VariableExpression const* expression) = 0;
             virtual void visit(UnaryBooleanFunctionExpression const* expression) = 0;
             virtual void visit(UnaryNumericalFunctionExpression const* expression) = 0;

src/storage/expressions/Expressions.h

@@ -2,12 +2,9 @@
 #include "src/storage/expressions/BinaryBooleanFunctionExpression.h"
 #include "src/storage/expressions/BinaryNumericalFunctionExpression.h"
 #include "src/storage/expressions/BinaryRelationExpression.h"
-#include "src/storage/expressions/BooleanConstantExpression.h"
 #include "src/storage/expressions/BooleanLiteralExpression.h"
-#include "src/storage/expressions/DoubleConstantExpression.h"
-#include "src/storage/expressions/DoubleLiteralExpression.h"
-#include "src/storage/expressions/IntegerConstantExpression.h"
 #include "src/storage/expressions/IntegerLiteralExpression.h"
+#include "src/storage/expressions/DoubleLiteralExpression.h"
 #include "src/storage/expressions/UnaryBooleanFunctionExpression.h"
 #include "src/storage/expressions/UnaryNumericalFunctionExpression.h"
 #include "src/storage/expressions/VariableExpression.h"

src/storage/expressions/IdentifierSubstitutionVisitor.cpp

@@ -3,20 +3,7 @@
 #include <string>
 
 #include "src/storage/expressions/IdentifierSubstitutionVisitor.h"
-
-#include "src/storage/expressions/IfThenElseExpression.h"
-#include "src/storage/expressions/BinaryBooleanFunctionExpression.h"
-#include "src/storage/expressions/BinaryNumericalFunctionExpression.h"
-#include "src/storage/expressions/BinaryRelationExpression.h"
-#include "src/storage/expressions/BooleanConstantExpression.h"
-#include "src/storage/expressions/IntegerConstantExpression.h"
-#include "src/storage/expressions/DoubleConstantExpression.h"
-#include "src/storage/expressions/BooleanLiteralExpression.h"
-#include "src/storage/expressions/IntegerLiteralExpression.h"
-#include "src/storage/expressions/DoubleLiteralExpression.h"
-#include "src/storage/expressions/VariableExpression.h"
-#include "src/storage/expressions/UnaryBooleanFunctionExpression.h"
-#include "src/storage/expressions/UnaryNumericalFunctionExpression.h"
+#include "src/storage/expressions/Expressions.h"
 
 namespace storm {
     namespace expressions  {
@@ -106,40 +93,7 @@ namespace storm {
                 this->expressionStack.push(std::shared_ptr<BaseExpression>(new BinaryRelationExpression(expression->getReturnType(), firstExpression, secondExpression, expression->getRelationType())));
             }
         }
-        
-        template<typename MapType>
-        void IdentifierSubstitutionVisitor<MapType>::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());
-            if (namePair != this->identifierToIdentifierMap.end()) {
-                this->expressionStack.push(std::shared_ptr<BaseExpression>(new BooleanConstantExpression(namePair->second)));
-            } else {
-                this->expressionStack.push(expression->getSharedPointer());
-            }
-        }
-        
-        template<typename MapType>
-        void IdentifierSubstitutionVisitor<MapType>::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());
-            if (namePair != this->identifierToIdentifierMap.end()) {
-                this->expressionStack.push(std::shared_ptr<BaseExpression>(new DoubleConstantExpression(namePair->second)));
-            } else {
-                this->expressionStack.push(expression->getSharedPointer());
-            }
-        }
-        
-        template<typename MapType>
-        void IdentifierSubstitutionVisitor<MapType>::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());
-            if (namePair != this->identifierToIdentifierMap.end()) {
-                this->expressionStack.push(std::shared_ptr<BaseExpression>(new IntegerConstantExpression(namePair->second)));
-            } else {
-                this->expressionStack.push(expression->getSharedPointer());
-            }
-        }
-        
+                
         template<typename MapType>
         void IdentifierSubstitutionVisitor<MapType>::visit(VariableExpression const* expression) {
             // If the variable is in the key set of the substitution, we need to replace it.

src/storage/expressions/IdentifierSubstitutionVisitor.h

@@ -32,9 +32,6 @@ namespace storm {
             virtual void visit(BinaryBooleanFunctionExpression const* expression) override;
             virtual void visit(BinaryNumericalFunctionExpression const* expression) override;
             virtual void visit(BinaryRelationExpression const* expression) override;
-            virtual void visit(BooleanConstantExpression const* expression) override;
-            virtual void visit(DoubleConstantExpression const* expression) override;
-            virtual void visit(IntegerConstantExpression const* expression) override;
             virtual void visit(VariableExpression const* expression) override;
             virtual void visit(UnaryBooleanFunctionExpression const* expression) override;
             virtual void visit(UnaryNumericalFunctionExpression const* expression) override;

src/storage/expressions/IfThenElseExpression.cpp

@@ -33,10 +33,6 @@ namespace storm {
             }
         }
         
-        bool IfThenElseExpression::isConstant() const {
-            return this->condition->isConstant() && this->thenExpression->isConstant() && this->elseExpression->isConstant();
-        }
-        
         std::set<std::string> IfThenElseExpression::getVariables() const {
             std::set<std::string> result = this->condition->getVariables();
             std::set<std::string> tmp = this->thenExpression->getVariables();
@@ -46,15 +42,6 @@ namespace storm {
             return result;
         }
         
-        std::set<std::string> IfThenElseExpression::getConstants() const {
-            std::set<std::string> result = this->condition->getConstants();
-            std::set<std::string> tmp = this->thenExpression->getConstants();
-            result.insert(tmp.begin(), tmp.end());
-            tmp = this->elseExpression->getConstants();
-            result.insert(tmp.begin(), tmp.end());
-            return result;
-        }
-        
         std::shared_ptr<BaseExpression const> IfThenElseExpression::simplify() const {
             std::shared_ptr<BaseExpression const> conditionSimplified;
             if (conditionSimplified->isTrue()) {

src/storage/expressions/IfThenElseExpression.h

@@ -30,9 +30,7 @@ namespace storm {
             virtual bool evaluateAsBool(Valuation const* valuation = nullptr) const override;
             virtual int_fast64_t evaluateAsInt(Valuation const* valuation = nullptr) const override;
             virtual double evaluateAsDouble(Valuation const* valuation = nullptr) const override;
-            virtual bool isConstant() const override;
             virtual std::set<std::string> getVariables() const override;
-            virtual std::set<std::string> getConstants() const override;
             virtual std::shared_ptr<BaseExpression const> simplify() const override;
             virtual void accept(ExpressionVisitor* visitor) const override;
             

src/storage/expressions/IntegerConstantExpression.cpp

@@ -1,27 +0,0 @@
-#include "src/storage/expressions/IntegerConstantExpression.h"
-#include "src/exceptions/ExceptionMacros.h"
-
-namespace storm {
-    namespace expressions {
-        IntegerConstantExpression::IntegerConstantExpression(std::string const& constantName) : ConstantExpression(ExpressionReturnType::Int, constantName) {
-            // Intentionally left empty.
-        }
-        
-        int_fast64_t IntegerConstantExpression::evaluateAsInt(Valuation const* valuation) const {
-            LOG_ASSERT(valuation != nullptr, "Evaluating expressions with unknowns without valuation.");
-            return valuation->getIntegerValue(this->getConstantName());
-        }
-        
-        double IntegerConstantExpression::evaluateAsDouble(Valuation const* valuation) const {
-            return static_cast<double>(this->evaluateAsInt(valuation));
-        }
-        
-        std::shared_ptr<BaseExpression const> IntegerConstantExpression::simplify() const {
-            return this->shared_from_this();
-        }
-        
-        void IntegerConstantExpression::accept(ExpressionVisitor* visitor) const {
-            visitor->visit(this);
-        }
-    }
-}

src/storage/expressions/IntegerConstantExpression.h

@@ -1,36 +0,0 @@
-#ifndef STORM_STORAGE_EXPRESSIONS_INTEGERCONSTANTEXPRESSION_H_
-#define STORM_STORAGE_EXPRESSIONS_INTEGERCONSTANTEXPRESSION_H_
-
-#include "src/storage/expressions/ConstantExpression.h"
-#include "src/utility/OsDetection.h"
-
-namespace storm {
-    namespace expressions {
-        class IntegerConstantExpression : public ConstantExpression {
-        public:
-            /*!
-             * Creates an integer constant expression with the given constant name.
-             *
-             * @param constantName The name of the integer constant associated with this expression.
-             */
-            IntegerConstantExpression(std::string const& constantName);
-            
-            // Instantiate constructors and assignments with their default implementations.
-            IntegerConstantExpression(IntegerConstantExpression const& other) = default;
-            IntegerConstantExpression& operator=(IntegerConstantExpression const& other) = default;
-#ifndef WINDOWS
-            IntegerConstantExpression(IntegerConstantExpression&&) = default;
-            IntegerConstantExpression& operator=(IntegerConstantExpression&&) = default;
-#endif
-            virtual ~IntegerConstantExpression() = default;
-            
-            // Override base class methods.
-            virtual int_fast64_t evaluateAsInt(Valuation const* valuation = nullptr) const override;
-            virtual double evaluateAsDouble(Valuation const* valuation = nullptr) const override;
-            virtual std::shared_ptr<BaseExpression const> simplify() const override;
-            virtual void accept(ExpressionVisitor* visitor) const;
-        };
-    }
-}
-
-#endif /* STORM_STORAGE_EXPRESSIONS_INTEGERCONSTANTEXPRESSION_H_ */

src/storage/expressions/IntegerLiteralExpression.cpp

@@ -14,7 +14,7 @@ namespace storm {
             return static_cast<double>(this->evaluateAsInt(valuation));
         }
         
-        bool IntegerLiteralExpression::isConstant() const {
+        bool IntegerLiteralExpression::isLiteral() const {
             return true;
         }
         
@@ -22,10 +22,6 @@ namespace storm {
             return std::set<std::string>();
         }
         
-        std::set<std::string> IntegerLiteralExpression::getConstants() const {
-            return std::set<std::string>();
-        }
-        
         std::shared_ptr<BaseExpression const> IntegerLiteralExpression::simplify() const {
             return this->shared_from_this();
         }

src/storage/expressions/IntegerLiteralExpression.h

@@ -27,9 +27,8 @@ namespace storm {
             // Override base class methods.
             virtual int_fast64_t evaluateAsInt(Valuation const* valuation = nullptr) const override;
             virtual double evaluateAsDouble(Valuation const* valuation = nullptr) const override;
-            virtual bool isConstant() const override;
+            virtual bool isLiteral() const override;
             virtual std::set<std::string> getVariables() const override;
-            virtual std::set<std::string> getConstants() const override;
             virtual std::shared_ptr<BaseExpression const> simplify() const override;
             virtual void accept(ExpressionVisitor* visitor) const override;
             

src/storage/expressions/SubstitutionVisitor.cpp

@@ -94,39 +94,6 @@ namespace storm {
             }
         }
         
-		template<typename MapType>
-        void SubstitutionVisitor<MapType>::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());
-            if (nameExpressionPair != this->identifierToExpressionMap.end()) {
-                this->expressionStack.push(nameExpressionPair->second.getBaseExpressionPointer());
-            } else {
-                this->expressionStack.push(expression->getSharedPointer());
-            }
-        }
-        
-		template<typename MapType>
-        void SubstitutionVisitor<MapType>::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());
-            if (nameExpressionPair != this->identifierToExpressionMap.end()) {
-                this->expressionStack.push(nameExpressionPair->second.getBaseExpressionPointer());
-            } else {
-                this->expressionStack.push(expression->getSharedPointer());
-            }
-        }
-        
-		template<typename MapType>
-        void SubstitutionVisitor<MapType>::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());
-            if (nameExpressionPair != this->identifierToExpressionMap.end()) {
-                this->expressionStack.push(nameExpressionPair->second.getBaseExpressionPointer());
-            } else {
-                this->expressionStack.push(expression->getSharedPointer());
-            }
-        }
-        
 		template<typename MapType>
         void SubstitutionVisitor<MapType>::visit(VariableExpression const* expression) {
             // If the variable is in the key set of the substitution, we need to replace it.

src/storage/expressions/SubstitutionVisitor.h

@@ -32,9 +32,6 @@ namespace storm {
             virtual void visit(BinaryBooleanFunctionExpression const* expression) override;
             virtual void visit(BinaryNumericalFunctionExpression const* expression) override;
             virtual void visit(BinaryRelationExpression const* expression) override;
-            virtual void visit(BooleanConstantExpression const* expression) override;
-            virtual void visit(DoubleConstantExpression const* expression) override;
-            virtual void visit(IntegerConstantExpression const* expression) override;
             virtual void visit(VariableExpression const* expression) override;
             virtual void visit(UnaryBooleanFunctionExpression const* expression) override;
             virtual void visit(UnaryNumericalFunctionExpression const* expression) override;

src/storage/expressions/TypeCheckVisitor.cpp

@@ -40,28 +40,7 @@ namespace storm {
             expression->getFirstOperand()->accept(this);
             expression->getSecondOperand()->accept(this);
         }
-        
-        template<typename MapType>
-        void TypeCheckVisitor<MapType>::visit(BooleanConstantExpression const* expression) {
-            auto identifierTypePair = this->identifierToTypeMap.find(expression->getConstantName());
-            LOG_THROW(identifierTypePair != this->identifierToTypeMap.end(), storm::exceptions::InvalidArgumentException, "No type available for identifier '" << expression->getConstantName() << "'.");
-            LOG_THROW(identifierTypePair->second == ExpressionReturnType::Bool, storm::exceptions::InvalidTypeException, "Type mismatch for constant '" << expression->getConstantName() << "': expected 'bool', but found '" << expression->getReturnType() << "'.");
-        }
-        
-        template<typename MapType>
-        void TypeCheckVisitor<MapType>::visit(DoubleConstantExpression const* expression) {
-            auto identifierTypePair = this->identifierToTypeMap.find(expression->getConstantName());
-            LOG_THROW(identifierTypePair != this->identifierToTypeMap.end(), storm::exceptions::InvalidArgumentException, "No type available for identifier '" << expression->getConstantName() << "'.");
-            LOG_THROW(identifierTypePair->second == ExpressionReturnType::Double, storm::exceptions::InvalidTypeException, "Type mismatch for constant '" << expression->getConstantName() << "': expected 'double', but found '" << expression->getReturnType() << "'.");
-        }
-        
-        template<typename MapType>
-        void TypeCheckVisitor<MapType>::visit(IntegerConstantExpression const* expression) {
-            auto identifierTypePair = this->identifierToTypeMap.find(expression->getConstantName());
-            LOG_THROW(identifierTypePair != this->identifierToTypeMap.end(), storm::exceptions::InvalidArgumentException, "No type available for identifier '" << expression->getConstantName() << "'.");
-            LOG_THROW(identifierTypePair->second == ExpressionReturnType::Int, storm::exceptions::InvalidTypeException, "Type mismatch for constant '" << expression->getConstantName() << "': expected 'int', but found '" << expression->getReturnType() << "'.");
-        }
-        
+                
         template<typename MapType>
         void TypeCheckVisitor<MapType>::visit(VariableExpression const* expression) {
             auto identifierTypePair = this->identifierToTypeMap.find(expression->getVariableName());

src/storage/expressions/TypeCheckVisitor.h

@@ -30,9 +30,6 @@ namespace storm {
             virtual void visit(BinaryBooleanFunctionExpression const* expression) override;
             virtual void visit(BinaryNumericalFunctionExpression const* expression) override;
             virtual void visit(BinaryRelationExpression const* expression) override;
-            virtual void visit(BooleanConstantExpression const* expression) override;
-            virtual void visit(DoubleConstantExpression const* expression) override;
-            virtual void visit(IntegerConstantExpression const* expression) override;
             virtual void visit(VariableExpression const* expression) override;
             virtual void visit(UnaryBooleanFunctionExpression const* expression) override;
             virtual void visit(UnaryNumericalFunctionExpression const* expression) override;

src/storage/expressions/UnaryExpression.cpp

@@ -1,25 +1,33 @@
 #include "src/storage/expressions/UnaryExpression.h"
 
+#include "src/exceptions/ExceptionMacros.h"
+#include "src/exceptions/InvalidAccessException.h"
+
 namespace storm {
     namespace expressions {
         UnaryExpression::UnaryExpression(ExpressionReturnType returnType, std::shared_ptr<BaseExpression const> const& operand) : BaseExpression(returnType), operand(operand) {
             // Intentionally left empty.
         }
 
-        bool UnaryExpression::isConstant() const {
-            return this->getOperand()->isConstant();
+        bool UnaryExpression::containsVariables() const {
+            return this->getOperand()->containsVariables();
         }
         
         std::set<std::string> UnaryExpression::getVariables() const {
             return this->getOperand()->getVariables();
         }
         
-        std::set<std::string> UnaryExpression::getConstants() const {
-            return this->getOperand()->getVariables();
-        }
-        
         std::shared_ptr<BaseExpression const> const& UnaryExpression::getOperand() const {
             return this->operand;
         }
+        
+        uint_fast64_t UnaryExpression::getArity() const {
+            return 1;
+        }
+        
+        std::shared_ptr<BaseExpression const> UnaryExpression::getOperand(uint_fast64_t operandIndex) const {
+            LOG_THROW(operandIndex == 0, storm::exceptions::InvalidAccessException, "Unable to access operand " << operandIndex << " in expression of arity 2.");
+            return this->getOperand();
+        }
     }
 }

src/storage/expressions/UnaryExpression.h

@@ -26,9 +26,10 @@ namespace storm {
             virtual ~UnaryExpression() = default;
             
             // Override base class methods.
-            virtual bool isConstant() const override;
+            virtual bool containsVariables() const override;
+            virtual uint_fast64_t getArity() const override;
+            virtual std::shared_ptr<BaseExpression const> getOperand(uint_fast64_t operandIndex) const override;
             virtual std::set<std::string> getVariables() const override;
-            virtual std::set<std::string> getConstants() const override;
             
             /*!
              * Retrieves the operand of the unary expression.

src/storage/expressions/VariableExpression.cpp

@@ -41,12 +41,16 @@ namespace storm {
             return 0;
         }
         
-        std::set<std::string> VariableExpression::getVariables() const {
-            return {this->getVariableName()};
+        std::string const& VariableExpression::getIdentifier() const {
+            return this->getVariableName();
+        }
+        
+        bool VariableExpression::containsVariables() const {
+            return true;
         }
         
-        std::set<std::string> VariableExpression::getConstants() const {
-            return std::set<std::string>();
+        std::set<std::string> VariableExpression::getVariables() const {
+            return {this->getVariableName()};
         }
         
         std::shared_ptr<BaseExpression const> VariableExpression::simplify() const {

src/storage/expressions/VariableExpression.h

@@ -29,8 +29,9 @@ namespace storm {
             virtual bool evaluateAsBool(Valuation const* valuation = nullptr) const override;
             virtual int_fast64_t evaluateAsInt(Valuation const* valuation = nullptr) const override;
             virtual double evaluateAsDouble(Valuation const* valuation = nullptr) const override;
+            virtual std::string const& getIdentifier() const override;
+            virtual bool containsVariables() const override;
             virtual std::set<std::string> getVariables() const override;
-            virtual std::set<std::string> getConstants() const override;
             virtual std::shared_ptr<BaseExpression const> simplify() const override;
             virtual void accept(ExpressionVisitor* visitor) const override;
 

src/storage/prism/Program.cpp

@@ -343,11 +343,9 @@ namespace storm {
                 
                 // Check defining expressions of defined constants.
                 if (constant.isDefined()) {
-                    LOG_THROW(constant.getExpression().getVariables().empty(), storm::exceptions::WrongFormatException, "Error in " << constant.getFilename() << ", line " << constant.getLineNumber() << ": definition of constant " << constant.getName() << " must not refer to variables.");
-                    
-                    std::set<std::string> containedConstantNames = constant.getExpression().getConstants();
-                    bool isValid = std::includes(constantNames.begin(), constantNames.end(), containedConstantNames.begin(), containedConstantNames.end());
-                    LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << constant.getFilename() << ", line " << constant.getLineNumber() << ": defining expression refers to unknown constants.");
+                    std::set<std::string> containedIdentifiers = constant.getExpression().getVariables();
+                    bool isValid = std::includes(constantNames.begin(), constantNames.end(), containedIdentifiers.begin(), containedIdentifiers.end());
+                    LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << constant.getFilename() << ", line " << constant.getLineNumber() << ": defining expression refers to unknown identifiers.");
                     
                     // Now check that the constants appear with the right types.
                     try {
@@ -373,12 +371,11 @@ namespace storm {
                 LOG_THROW(allIdentifiers.find(variable.getName()) == allIdentifiers.end(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": duplicate identifier '" << variable.getName() << "'.");
                 
                 // Check the initial value of the variable.
-                LOG_THROW(variable.getInitialValueExpression().getVariables().empty(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression must not refer to variables.");
-                std::set<std::string> containedConstants = variable.getInitialValueExpression().getConstants();
-                bool isValid = std::includes(constantNames.begin(), constantNames.end(), containedConstants.begin(), containedConstants.end());
+                std::set<std::string> containedIdentifiers = variable.getInitialValueExpression().getVariables();
+                bool isValid = std::includes(constantNames.begin(), constantNames.end(), containedIdentifiers.begin(), containedIdentifiers.end());
                 LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants.");
                 try {
-                variable.getInitialValueExpression().check(identifierToTypeMap);
+                    variable.getInitialValueExpression().check(identifierToTypeMap);
                 } catch (storm::exceptions::InvalidTypeException const& e) {
                     LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": " << e.what());
                 }
@@ -396,9 +393,8 @@ namespace storm {
                 LOG_THROW(allIdentifiers.find(variable.getName()) == allIdentifiers.end(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": duplicate identifier '" << variable.getName() << "'.");
                 
                 // Check that bound expressions of the range.
-                LOG_THROW(variable.getLowerBoundExpression().getVariables().empty(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": lower bound expression must not refer to variables.");
-                std::set<std::string> containedConstants = variable.getLowerBoundExpression().getConstants();
-                bool isValid = std::includes(constantNames.begin(), constantNames.end(), containedConstants.begin(), containedConstants.end());
+                std::set<std::string> containedIdentifiers = variable.getLowerBoundExpression().getVariables();
+                bool isValid = std::includes(constantNames.begin(), constantNames.end(), containedIdentifiers.begin(), containedIdentifiers.end());
                 LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": lower bound expression refers to unknown constants.");
                 try {
                     variable.getLowerBoundExpression().check(identifierToTypeMap);
@@ -406,9 +402,8 @@ namespace storm {
                     LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": " << e.what());
                 }
 
-                LOG_THROW(variable.getUpperBoundExpression().getVariables().empty(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": upper bound expression must not refer to variables.");
-                containedConstants = variable.getLowerBoundExpression().getConstants();
-                isValid = std::includes(constantNames.begin(), constantNames.end(), containedConstants.begin(), containedConstants.end());
+                containedIdentifiers = variable.getLowerBoundExpression().getVariables();
+                isValid = std::includes(constantNames.begin(), constantNames.end(), containedIdentifiers.begin(), containedIdentifiers.end());
                 LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": upper bound expression refers to unknown constants.");
                 try {
                     variable.getUpperBoundExpression().check(identifierToTypeMap);
@@ -417,9 +412,8 @@ namespace storm {
                 }
                 
                 // Check the initial value of the variable.
-                LOG_THROW(variable.getInitialValueExpression().getVariables().empty(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression must not refer to variables.");
-                containedConstants = variable.getInitialValueExpression().getConstants();
-                isValid = std::includes(constantNames.begin(), constantNames.end(), containedConstants.begin(), containedConstants.end());
+                containedIdentifiers = variable.getInitialValueExpression().getVariables();
+                isValid = std::includes(constantNames.begin(), constantNames.end(), containedIdentifiers.begin(), containedIdentifiers.end());
                 LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants.");
                 try {
                     variable.getInitialValueExpression().check(identifierToTypeMap);
@@ -443,9 +437,8 @@ namespace storm {
                     LOG_THROW(allIdentifiers.find(variable.getName()) == allIdentifiers.end(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": duplicate identifier '" << variable.getName() << "'.");
                     
                     // Check the initial value of the variable.
-                    LOG_THROW(variable.getInitialValueExpression().getVariables().empty(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression must not refer to variables.");
-                    std::set<std::string> containedConstants = variable.getInitialValueExpression().getConstants();
-                    bool isValid = std::includes(constantNames.begin(), constantNames.end(), containedConstants.begin(), containedConstants.end());
+                    std::set<std::string> containedIdentifiers = variable.getInitialValueExpression().getVariables();
+                    bool isValid = std::includes(constantNames.begin(), constantNames.end(), containedIdentifiers.begin(), containedIdentifiers.end());
                     LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants.");
                     try {
                         variable.getInitialValueExpression().check(identifierToTypeMap);
@@ -468,9 +461,8 @@ namespace storm {
                     identifierToTypeMap.emplace(variable.getName(), storm::expressions::ExpressionReturnType::Int);
                     
                     // Check that bound expressions of the range.
-                    LOG_THROW(variable.getLowerBoundExpression().getVariables().empty(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": lower bound expression must not refer to variables.");
-                    std::set<std::string> containedConstants = variable.getLowerBoundExpression().getConstants();
-                    bool isValid = std::includes(constantNames.begin(), constantNames.end(), containedConstants.begin(), containedConstants.end());
+                    std::set<std::string> containedIdentifiers = variable.getLowerBoundExpression().getVariables();
+                    bool isValid = std::includes(constantNames.begin(), constantNames.end(), containedIdentifiers.begin(), containedIdentifiers.end());
                     LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": lower bound expression refers to unknown constants.");
                     try {
                         variable.getLowerBoundExpression().check(identifierToTypeMap);
@@ -478,9 +470,8 @@ namespace storm {
                         LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": " << e.what());
                     }
 
-                    LOG_THROW(variable.getUpperBoundExpression().getVariables().empty(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": upper bound expression must not refer to variables.");
-                    containedConstants = variable.getLowerBoundExpression().getConstants();
-                    isValid = std::includes(constantNames.begin(), constantNames.end(), containedConstants.begin(), containedConstants.end());
+                    containedIdentifiers = variable.getLowerBoundExpression().getVariables();
+                    isValid = std::includes(constantNames.begin(), constantNames.end(), containedIdentifiers.begin(), containedIdentifiers.end());
                     LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": upper bound expression refers to unknown constants.");
                     try {
                         variable.getUpperBoundExpression().check(identifierToTypeMap);
@@ -489,9 +480,8 @@ namespace storm {
                     }
                     
                     // Check the initial value of the variable.
-                    LOG_THROW(variable.getInitialValueExpression().getVariables().empty(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression must not refer to variables.");
-                    containedConstants = variable.getInitialValueExpression().getConstants();
-                    isValid = std::includes(constantNames.begin(), constantNames.end(), containedConstants.begin(), containedConstants.end());
+                    containedIdentifiers = variable.getInitialValueExpression().getVariables();
+                    isValid = std::includes(constantNames.begin(), constantNames.end(), containedIdentifiers.begin(), containedIdentifiers.end());
                     LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants.");
                     try {
                         variable.getInitialValueExpression().check(identifierToTypeMap);
@@ -521,7 +511,7 @@ namespace storm {
                 
                 for (auto const& command : module.getCommands()) {
                     // Check the guard.
-                    std::set<std::string> containedIdentifiers = command.getGuardExpression().getIdentifiers();
+                    std::set<std::string> containedIdentifiers = command.getGuardExpression().getVariables();
                     bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end());
                     LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": guard refers to unknown identifiers.");
                     try {
@@ -533,7 +523,7 @@ namespace storm {
                     
                     // Check all updates.
                     for (auto const& update : command.getUpdates()) {
-                        containedIdentifiers = update.getLikelihoodExpression().getIdentifiers();
+                        containedIdentifiers = update.getLikelihoodExpression().getVariables();
                         isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end());
                         LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": likelihood expression refers to unknown identifiers.");
                         try {
@@ -556,7 +546,7 @@ namespace storm {
                             auto variableTypePair = identifierToTypeMap.find(assignment.getVariableName());
                             LOG_THROW(variableTypePair->second == assignment.getExpression().getReturnType(), storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": illegally assigning a value of type '" << assignment.getExpression().getReturnType() << "' to variable '" << variableTypePair->first << "' of type '" << variableTypePair->second << "'.");
                             
-                            containedIdentifiers = assignment.getExpression().getIdentifiers();
+                            containedIdentifiers = assignment.getExpression().getVariables();
                             isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end());
                             LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": likelihood expression refers to unknown identifiers.");
                             try {
@@ -575,7 +565,7 @@ namespace storm {
             // Now check the reward models.
             for (auto const& rewardModel : this->getRewardModels()) {
                 for (auto const& stateReward : rewardModel.getStateRewards()) {
-                    std::set<std::string> containedIdentifiers = stateReward.getStatePredicateExpression().getIdentifiers();
+                    std::set<std::string> containedIdentifiers = stateReward.getStatePredicateExpression().getVariables();
                     bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end());
                     LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << stateReward.getFilename() << ", line " << stateReward.getLineNumber() << ": state reward expression refers to unknown identifiers.");
                     try {
@@ -585,7 +575,7 @@ namespace storm {
                     }
                     LOG_THROW(stateReward.getStatePredicateExpression().hasBooleanReturnType(), storm::exceptions::WrongFormatException, "Error in " << stateReward.getFilename() << ", line " << stateReward.getLineNumber() << ": state predicate must evaluate to type 'bool'.");
                     
-                    containedIdentifiers = stateReward.getRewardValueExpression().getIdentifiers();
+                    containedIdentifiers = stateReward.getRewardValueExpression().getVariables();
                     isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end());
                     LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << stateReward.getFilename() << ", line " << stateReward.getLineNumber() << ": state reward value expression refers to unknown identifiers.");
                     try {
@@ -597,7 +587,7 @@ namespace storm {
                 }
                 
                 for (auto const& transitionReward : rewardModel.getTransitionRewards()) {
-                    std::set<std::string> containedIdentifiers = transitionReward.getStatePredicateExpression().getIdentifiers();
+                    std::set<std::string> containedIdentifiers = transitionReward.getStatePredicateExpression().getVariables();
                     bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end());
                     LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << transitionReward.getFilename() << ", line " << transitionReward.getLineNumber() << ": state reward expression refers to unknown identifiers.");
                     try {
@@ -607,7 +597,7 @@ namespace storm {
                     }
                     LOG_THROW(transitionReward.getStatePredicateExpression().hasBooleanReturnType(), storm::exceptions::WrongFormatException, "Error in " << transitionReward.getFilename() << ", line " << transitionReward.getLineNumber() << ": state predicate must evaluate to type 'bool'.");
                     
-                    containedIdentifiers = transitionReward.getRewardValueExpression().getIdentifiers();
+                    containedIdentifiers = transitionReward.getRewardValueExpression().getVariables();
                     isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end());
                     LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << transitionReward.getFilename() << ", line " << transitionReward.getLineNumber() << ": state reward value expression refers to unknown identifiers.");
                     try {
@@ -620,7 +610,7 @@ namespace storm {
             }
             
             // Check the initial states expression.
-            std::set<std::string> containedIdentifiers = this->getInitialConstruct().getInitialStatesExpression().getIdentifiers();
+            std::set<std::string> containedIdentifiers = this->getInitialConstruct().getInitialStatesExpression().getVariables();
             bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end());
             LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << this->getInitialConstruct().getFilename() << ", line " << this->getInitialConstruct().getLineNumber() << ": initial expression refers to unknown identifiers.");
             try {
@@ -634,7 +624,7 @@ namespace storm {
                 // Check for duplicate identifiers.
                 LOG_THROW(allIdentifiers.find(label.getName()) == allIdentifiers.end(), storm::exceptions::WrongFormatException, "Error in " << label.getFilename() << ", line " << label.getLineNumber() << ": duplicate identifier '" << label.getName() << "'.");
                 
-                std::set<std::string> containedIdentifiers = label.getStatePredicateExpression().getIdentifiers();
+                std::set<std::string> containedIdentifiers = label.getStatePredicateExpression().getVariables();
                 bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end());
                 LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << label.getFilename() << ", line " << label.getLineNumber() << ": label expression refers to unknown identifiers.");
                 try {
@@ -651,7 +641,7 @@ namespace storm {
                 // Check for duplicate identifiers.
                 LOG_THROW(allIdentifiers.find(formula.getName()) == allIdentifiers.end(), storm::exceptions::WrongFormatException, "Error in " << formula.getFilename() << ", line " << formula.getLineNumber() << ": duplicate identifier '" << formula.getName() << "'.");
                 
-                std::set<std::string> containedIdentifiers = formula.getExpression().getIdentifiers();
+                std::set<std::string> containedIdentifiers = formula.getExpression().getVariables();
                 bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end());
                 LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << formula.getFilename() << ", line " << formula.getLineNumber() << ": formula expression refers to unknown identifiers.");
                 try {

test/functional/storage/ExpressionTest.cpp

@@ -15,9 +15,6 @@ TEST(Expression, FactoryMethodTest) {
     EXPECT_NO_THROW(storm::expressions::Expression::createBooleanVariable("x"));
     EXPECT_NO_THROW(storm::expressions::Expression::createIntegerVariable("y"));
     EXPECT_NO_THROW(storm::expressions::Expression::createDoubleVariable("z"));
-    EXPECT_NO_THROW(storm::expressions::Expression::createBooleanConstant("a"));
-    EXPECT_NO_THROW(storm::expressions::Expression::createIntegerConstant("b"));
-    EXPECT_NO_THROW(storm::expressions::Expression::createDoubleConstant("c"));
 }
 
 TEST(Expression, AccessorTest) {
@@ -28,9 +25,6 @@ TEST(Expression, AccessorTest) {
     storm::expressions::Expression boolVarExpression;
     storm::expressions::Expression intVarExpression;
     storm::expressions::Expression doubleVarExpression;
-    storm::expressions::Expression boolConstExpression;
-    storm::expressions::Expression intConstExpression;
-    storm::expressions::Expression doubleConstExpression;
     
     ASSERT_NO_THROW(trueExpression = storm::expressions::Expression::createTrue());
     ASSERT_NO_THROW(falseExpression = storm::expressions::Expression::createFalse());
@@ -39,79 +33,48 @@ TEST(Expression, AccessorTest) {
     ASSERT_NO_THROW(boolVarExpression = storm::expressions::Expression::createBooleanVariable("x"));
     ASSERT_NO_THROW(intVarExpression = storm::expressions::Expression::createIntegerVariable("y"));
     ASSERT_NO_THROW(doubleVarExpression = storm::expressions::Expression::createDoubleVariable("z"));
-    ASSERT_NO_THROW(boolConstExpression = storm::expressions::Expression::createBooleanConstant("a"));
-    ASSERT_NO_THROW(intConstExpression = storm::expressions::Expression::createIntegerConstant("b"));
-    ASSERT_NO_THROW(doubleConstExpression = storm::expressions::Expression::createDoubleConstant("c"));
     
     EXPECT_TRUE(trueExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool);
-    EXPECT_TRUE(trueExpression.isConstant());
+    EXPECT_TRUE(trueExpression.isLiteral());
     EXPECT_TRUE(trueExpression.isTrue());
     EXPECT_FALSE(trueExpression.isFalse());
     EXPECT_TRUE(trueExpression.getVariables() == std::set<std::string>());
-    EXPECT_TRUE(trueExpression.getConstants() == std::set<std::string>());
     
     EXPECT_TRUE(falseExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool);
-    EXPECT_TRUE(falseExpression.isConstant());
+    EXPECT_TRUE(falseExpression.isLiteral());
     EXPECT_FALSE(falseExpression.isTrue());
     EXPECT_TRUE(falseExpression.isFalse());
     EXPECT_TRUE(falseExpression.getVariables() == std::set<std::string>());
-    EXPECT_TRUE(falseExpression.getConstants() == std::set<std::string>());
 
     EXPECT_TRUE(threeExpression.getReturnType() == storm::expressions::ExpressionReturnType::Int);
-    EXPECT_TRUE(threeExpression.isConstant());
+    EXPECT_TRUE(threeExpression.isLiteral());
     EXPECT_FALSE(threeExpression.isTrue());
     EXPECT_FALSE(threeExpression.isFalse());
     EXPECT_TRUE(threeExpression.getVariables() == std::set<std::string>());
-    EXPECT_TRUE(threeExpression.getConstants() == std::set<std::string>());
     
     EXPECT_TRUE(piExpression.getReturnType() == storm::expressions::ExpressionReturnType::Double);
-    EXPECT_TRUE(piExpression.isConstant());
+    EXPECT_TRUE(piExpression.isLiteral());
     EXPECT_FALSE(piExpression.isTrue());
     EXPECT_FALSE(piExpression.isFalse());
     EXPECT_TRUE(piExpression.getVariables() == std::set<std::string>());
-    EXPECT_TRUE(piExpression.getConstants() == std::set<std::string>());
     
     EXPECT_TRUE(boolVarExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool);
-    EXPECT_FALSE(boolVarExpression.isConstant());
+    EXPECT_FALSE(boolVarExpression.isLiteral());
     EXPECT_FALSE(boolVarExpression.isTrue());
     EXPECT_FALSE(boolVarExpression.isFalse());
     EXPECT_TRUE(boolVarExpression.getVariables() == std::set<std::string>({"x"}));
-    EXPECT_TRUE(boolVarExpression.getConstants() == std::set<std::string>());
 
     EXPECT_TRUE(intVarExpression.getReturnType() == storm::expressions::ExpressionReturnType::Int);
-    EXPECT_FALSE(intVarExpression.isConstant());
+    EXPECT_FALSE(intVarExpression.isLiteral());
     EXPECT_FALSE(intVarExpression.isTrue());
     EXPECT_FALSE(intVarExpression.isFalse());
     EXPECT_TRUE(intVarExpression.getVariables() == std::set<std::string>({"y"}));
-    EXPECT_TRUE(intVarExpression.getConstants() == std::set<std::string>());
 
     EXPECT_TRUE(doubleVarExpression.getReturnType() == storm::expressions::ExpressionReturnType::Double);
-    EXPECT_FALSE(doubleVarExpression.isConstant());
+    EXPECT_FALSE(doubleVarExpression.isLiteral());
     EXPECT_FALSE(doubleVarExpression.isTrue());
     EXPECT_FALSE(doubleVarExpression.isFalse());
     EXPECT_TRUE(doubleVarExpression.getVariables() == std::set<std::string>({"z"}));
-    EXPECT_TRUE(doubleVarExpression.getConstants() == std::set<std::string>());
-
-    EXPECT_TRUE(boolConstExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool);
-    EXPECT_FALSE(boolConstExpression.isConstant());
-    EXPECT_FALSE(boolConstExpression.isTrue());
-    EXPECT_FALSE(boolConstExpression.isFalse());
-    EXPECT_TRUE(boolConstExpression.getVariables() == std::set<std::string>());
-    EXPECT_TRUE(boolConstExpression.getConstants() == std::set<std::string>({"a"}));
-    
-    EXPECT_TRUE(intConstExpression.getReturnType() == storm::expressions::ExpressionReturnType::Int);
-    EXPECT_FALSE(intConstExpression.isConstant());
-    EXPECT_FALSE(intConstExpression.isTrue());
-    EXPECT_FALSE(intConstExpression.isFalse());
-    EXPECT_TRUE(intConstExpression.getVariables() == std::set<std::string>());
-    EXPECT_TRUE(intConstExpression.getConstants() == std::set<std::string>({"b"}));
-
-    EXPECT_TRUE(doubleConstExpression.getReturnType() == storm::expressions::ExpressionReturnType::Double);
-    EXPECT_FALSE(doubleConstExpression.isConstant());
-    EXPECT_FALSE(doubleConstExpression.isTrue());
-    EXPECT_FALSE(doubleConstExpression.isFalse());
-    EXPECT_TRUE(doubleConstExpression.getVariables() == std::set<std::string>());
-    EXPECT_TRUE(doubleConstExpression.getConstants() == std::set<std::string>({"c"}));
 }
 
 TEST(Expression, OperatorTest) {
@@ -122,9 +85,6 @@ TEST(Expression, OperatorTest) {
     storm::expressions::Expression boolVarExpression;
     storm::expressions::Expression intVarExpression;
     storm::expressions::Expression doubleVarExpression;
-    storm::expressions::Expression boolConstExpression;
-    storm::expressions::Expression intConstExpression;
-    storm::expressions::Expression doubleConstExpression;
     
     ASSERT_NO_THROW(trueExpression = storm::expressions::Expression::createTrue());
     ASSERT_NO_THROW(falseExpression = storm::expressions::Expression::createFalse());
@@ -133,18 +93,15 @@ TEST(Expression, OperatorTest) {
     ASSERT_NO_THROW(boolVarExpression = storm::expressions::Expression::createBooleanVariable("x"));
     ASSERT_NO_THROW(intVarExpression = storm::expressions::Expression::createIntegerVariable("y"));
     ASSERT_NO_THROW(doubleVarExpression = storm::expressions::Expression::createDoubleVariable("z"));
-    ASSERT_NO_THROW(boolConstExpression = storm::expressions::Expression::createBooleanConstant("a"));
-    ASSERT_NO_THROW(intConstExpression = storm::expressions::Expression::createIntegerConstant("b"));
-    ASSERT_NO_THROW(doubleConstExpression = storm::expressions::Expression::createDoubleConstant("c"));
     
     storm::expressions::Expression tempExpression;
 
     ASSERT_THROW(tempExpression = trueExpression.ite(falseExpression, piExpression), storm::exceptions::InvalidTypeException);
-    ASSERT_NO_THROW(tempExpression = boolConstExpression.ite(threeExpression, doubleVarExpression));
+    ASSERT_NO_THROW(tempExpression = boolVarExpression.ite(threeExpression, doubleVarExpression));
     EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Double);
-    ASSERT_NO_THROW(tempExpression = boolConstExpression.ite(threeExpression, intVarExpression));
+    ASSERT_NO_THROW(tempExpression = boolVarExpression.ite(threeExpression, intVarExpression));
     EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Int);
-    ASSERT_NO_THROW(tempExpression = boolConstExpression.ite(trueExpression, falseExpression));
+    ASSERT_NO_THROW(tempExpression = boolVarExpression.ite(trueExpression, falseExpression));
     EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool);
     
     ASSERT_THROW(tempExpression = trueExpression + piExpression, storm::exceptions::InvalidTypeException);
@@ -152,7 +109,7 @@ TEST(Expression, OperatorTest) {
     EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Int);
     ASSERT_NO_THROW(tempExpression = threeExpression + piExpression);
     EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Double);
-    ASSERT_NO_THROW(tempExpression = doubleVarExpression + doubleConstExpression);
+    ASSERT_NO_THROW(tempExpression = doubleVarExpression + doubleVarExpression);
     EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Double);
     
     ASSERT_THROW(tempExpression = trueExpression - piExpression, storm::exceptions::InvalidTypeException);
@@ -160,7 +117,7 @@ TEST(Expression, OperatorTest) {
     EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Int);
     ASSERT_NO_THROW(tempExpression = threeExpression - piExpression);
     EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Double);
-    ASSERT_NO_THROW(tempExpression = doubleVarExpression - doubleConstExpression);
+    ASSERT_NO_THROW(tempExpression = doubleVarExpression - doubleVarExpression);
     EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Double);
     
     ASSERT_THROW(tempExpression = -trueExpression, storm::exceptions::InvalidTypeException);
@@ -176,7 +133,7 @@ TEST(Expression, OperatorTest) {
     EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Int);
     ASSERT_NO_THROW(tempExpression = threeExpression * piExpression);
     EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Double);
-    ASSERT_NO_THROW(tempExpression = intVarExpression * intConstExpression);
+    ASSERT_NO_THROW(tempExpression = intVarExpression * intVarExpression);
     EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Int);
 
     ASSERT_THROW(tempExpression = trueExpression / piExpression, storm::exceptions::InvalidTypeException);
@@ -184,19 +141,19 @@ TEST(Expression, OperatorTest) {
     EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Int);
     ASSERT_NO_THROW(tempExpression = threeExpression / piExpression);
     EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Double);
-    ASSERT_NO_THROW(tempExpression = doubleVarExpression / intConstExpression);
+    ASSERT_NO_THROW(tempExpression = doubleVarExpression / intVarExpression);
     EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Double);
 
     ASSERT_THROW(tempExpression = trueExpression && piExpression, storm::exceptions::InvalidTypeException);
     ASSERT_NO_THROW(tempExpression = trueExpression && falseExpression);
     EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool);
-    ASSERT_NO_THROW(tempExpression = boolVarExpression && boolConstExpression);
+    ASSERT_NO_THROW(tempExpression = boolVarExpression && boolVarExpression);
     EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool);
 
     ASSERT_THROW(tempExpression = trueExpression || piExpression, storm::exceptions::InvalidTypeException);
     ASSERT_NO_THROW(tempExpression = trueExpression || falseExpression);
     EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool);
-    ASSERT_NO_THROW(tempExpression = boolVarExpression || boolConstExpression);
+    ASSERT_NO_THROW(tempExpression = boolVarExpression || boolVarExpression);
     EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool);
 
     ASSERT_THROW(tempExpression = !threeExpression, storm::exceptions::InvalidTypeException);
@@ -208,79 +165,79 @@ TEST(Expression, OperatorTest) {
     ASSERT_THROW(tempExpression = trueExpression == piExpression, storm::exceptions::InvalidTypeException);
     ASSERT_NO_THROW(tempExpression = threeExpression == threeExpression);
     EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool);
-    ASSERT_NO_THROW(tempExpression = intVarExpression == doubleConstExpression);
+    ASSERT_NO_THROW(tempExpression = intVarExpression == doubleVarExpression);
     EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool);
 
     ASSERT_THROW(tempExpression = trueExpression != piExpression, storm::exceptions::InvalidTypeException);
     ASSERT_NO_THROW(tempExpression = threeExpression != threeExpression);
     EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool);
-    ASSERT_NO_THROW(tempExpression = intVarExpression != doubleConstExpression);
+    ASSERT_NO_THROW(tempExpression = intVarExpression != doubleVarExpression);
     EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool);
 
     ASSERT_THROW(tempExpression = trueExpression > piExpression, storm::exceptions::InvalidTypeException);
     ASSERT_NO_THROW(tempExpression = threeExpression > threeExpression);
     EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool);
-    ASSERT_NO_THROW(tempExpression = intVarExpression > doubleConstExpression);
+    ASSERT_NO_THROW(tempExpression = intVarExpression > doubleVarExpression);
     EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool);
     
     ASSERT_THROW(tempExpression = trueExpression >= piExpression, storm::exceptions::InvalidTypeException);
     ASSERT_NO_THROW(tempExpression = threeExpression >= threeExpression);
     EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool);
-    ASSERT_NO_THROW(tempExpression = intVarExpression >= doubleConstExpression);
+    ASSERT_NO_THROW(tempExpression = intVarExpression >= doubleVarExpression);
     EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool);
     
     ASSERT_THROW(tempExpression = trueExpression < piExpression, storm::exceptions::InvalidTypeException);
     ASSERT_NO_THROW(tempExpression = threeExpression < threeExpression);
     EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool);
-    ASSERT_NO_THROW(tempExpression = intVarExpression < doubleConstExpression);
+    ASSERT_NO_THROW(tempExpression = intVarExpression < doubleVarExpression);
     EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool);
     
     ASSERT_THROW(tempExpression = trueExpression <= piExpression, storm::exceptions::InvalidTypeException);
     ASSERT_NO_THROW(tempExpression = threeExpression <= threeExpression);
     EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool);
-    ASSERT_NO_THROW(tempExpression = intVarExpression <= doubleConstExpression);
+    ASSERT_NO_THROW(tempExpression = intVarExpression <= doubleVarExpression);
     EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool);
     
     ASSERT_THROW(tempExpression = storm::expressions::Expression::minimum(trueExpression, piExpression), storm::exceptions::InvalidTypeException);
     ASSERT_NO_THROW(tempExpression = storm::expressions::Expression::minimum(threeExpression, threeExpression));
     EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Int);
-    ASSERT_NO_THROW(tempExpression = storm::expressions::Expression::minimum(intVarExpression, doubleConstExpression));
+    ASSERT_NO_THROW(tempExpression = storm::expressions::Expression::minimum(intVarExpression, doubleVarExpression));
     EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Double);
 
     ASSERT_THROW(tempExpression = storm::expressions::Expression::maximum(trueExpression, piExpression), storm::exceptions::InvalidTypeException);
     ASSERT_NO_THROW(tempExpression = storm::expressions::Expression::maximum(threeExpression, threeExpression));
     EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Int);
-    ASSERT_NO_THROW(tempExpression = storm::expressions::Expression::maximum(intVarExpression, doubleConstExpression));
+    ASSERT_NO_THROW(tempExpression = storm::expressions::Expression::maximum(intVarExpression, doubleVarExpression));
     EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Double);
     
     ASSERT_THROW(tempExpression = trueExpression.implies(piExpression), storm::exceptions::InvalidTypeException);
     ASSERT_NO_THROW(tempExpression = trueExpression.implies(falseExpression));
     EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool);
-    ASSERT_NO_THROW(tempExpression = boolVarExpression.implies(boolConstExpression));
+    ASSERT_NO_THROW(tempExpression = boolVarExpression.implies(boolVarExpression));
     EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool);
     
     ASSERT_THROW(tempExpression = trueExpression.iff(piExpression), storm::exceptions::InvalidTypeException);
     ASSERT_NO_THROW(tempExpression = trueExpression.iff(falseExpression));
     EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool);
-    ASSERT_NO_THROW(tempExpression = boolVarExpression.iff(boolConstExpression));
+    ASSERT_NO_THROW(tempExpression = boolVarExpression.iff(boolVarExpression));
     EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool);
     
     ASSERT_THROW(tempExpression = trueExpression ^ piExpression, storm::exceptions::InvalidTypeException);
     ASSERT_NO_THROW(tempExpression = trueExpression ^ falseExpression);
     EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool);
-    ASSERT_NO_THROW(tempExpression = boolVarExpression ^ boolConstExpression);
+    ASSERT_NO_THROW(tempExpression = boolVarExpression ^ boolVarExpression);
     EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool);
     
     ASSERT_THROW(tempExpression = trueExpression.floor(), storm::exceptions::InvalidTypeException);
     ASSERT_NO_THROW(tempExpression = threeExpression.floor());
     EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Int);
-    ASSERT_NO_THROW(tempExpression = doubleConstExpression.floor());
+    ASSERT_NO_THROW(tempExpression = doubleVarExpression.floor());
     EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Int);
 
     ASSERT_THROW(tempExpression = trueExpression.ceil(), storm::exceptions::InvalidTypeException);
     ASSERT_NO_THROW(tempExpression = threeExpression.ceil());
     EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Int);
-    ASSERT_NO_THROW(tempExpression = doubleConstExpression.ceil());
+    ASSERT_NO_THROW(tempExpression = doubleVarExpression.ceil());
     EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Int);
 }
 
@@ -292,9 +249,6 @@ TEST(Expression, SubstitutionTest) {
     storm::expressions::Expression boolVarExpression;
     storm::expressions::Expression intVarExpression;
     storm::expressions::Expression doubleVarExpression;
-    storm::expressions::Expression boolConstExpression;
-    storm::expressions::Expression intConstExpression;
-    storm::expressions::Expression doubleConstExpression;
     
     ASSERT_NO_THROW(trueExpression = storm::expressions::Expression::createTrue());
     ASSERT_NO_THROW(falseExpression = storm::expressions::Expression::createFalse());
@@ -303,14 +257,11 @@ TEST(Expression, SubstitutionTest) {
     ASSERT_NO_THROW(boolVarExpression = storm::expressions::Expression::createBooleanVariable("x"));
     ASSERT_NO_THROW(intVarExpression = storm::expressions::Expression::createIntegerVariable("y"));
     ASSERT_NO_THROW(doubleVarExpression = storm::expressions::Expression::createDoubleVariable("z"));
-    ASSERT_NO_THROW(boolConstExpression = storm::expressions::Expression::createBooleanConstant("a"));
-    ASSERT_NO_THROW(intConstExpression = storm::expressions::Expression::createIntegerConstant("b"));
-    ASSERT_NO_THROW(doubleConstExpression = storm::expressions::Expression::createDoubleConstant("c"));
     
     storm::expressions::Expression tempExpression;
-    ASSERT_NO_THROW(tempExpression = (intVarExpression < threeExpression || boolVarExpression) && boolConstExpression);
+    ASSERT_NO_THROW(tempExpression = (intVarExpression < threeExpression || boolVarExpression) && boolVarExpression);
 
-    std::map<std::string, storm::expressions::Expression> substution = { std::make_pair("y", doubleConstExpression), std::make_pair("x", storm::expressions::Expression::createTrue()), std::make_pair("a", storm::expressions::Expression::createTrue()) };
+    std::map<std::string, storm::expressions::Expression> substution = { std::make_pair("y", doubleVarExpression), std::make_pair("x", storm::expressions::Expression::createTrue()), std::make_pair("a", storm::expressions::Expression::createTrue()) };
     storm::expressions::Expression substitutedExpression;
     ASSERT_NO_THROW(substitutedExpression = tempExpression.substitute(substution));
     EXPECT_TRUE(substitutedExpression.simplify().isTrue());
@@ -347,9 +298,6 @@ TEST(Expression, SimpleEvaluationTest) {
     storm::expressions::Expression boolVarExpression;
     storm::expressions::Expression intVarExpression;
     storm::expressions::Expression doubleVarExpression;
-    storm::expressions::Expression boolConstExpression;
-    storm::expressions::Expression intConstExpression;
-    storm::expressions::Expression doubleConstExpression;
     
     ASSERT_NO_THROW(trueExpression = storm::expressions::Expression::createTrue());
     ASSERT_NO_THROW(falseExpression = storm::expressions::Expression::createFalse());
@@ -358,13 +306,10 @@ TEST(Expression, SimpleEvaluationTest) {
     ASSERT_NO_THROW(boolVarExpression = storm::expressions::Expression::createBooleanVariable("x"));
     ASSERT_NO_THROW(intVarExpression = storm::expressions::Expression::createIntegerVariable("y"));
     ASSERT_NO_THROW(doubleVarExpression = storm::expressions::Expression::createDoubleVariable("z"));
-    ASSERT_NO_THROW(boolConstExpression = storm::expressions::Expression::createBooleanConstant("a"));
-    ASSERT_NO_THROW(intConstExpression = storm::expressions::Expression::createIntegerConstant("b"));
-    ASSERT_NO_THROW(doubleConstExpression = storm::expressions::Expression::createDoubleConstant("c"));
     
     storm::expressions::Expression tempExpression;
     
-    ASSERT_NO_THROW(tempExpression = (intVarExpression < threeExpression || boolVarExpression) && boolConstExpression);
+    ASSERT_NO_THROW(tempExpression = (intVarExpression < threeExpression || boolVarExpression) && boolVarExpression);
     
     ASSERT_NO_THROW(storm::expressions::SimpleValuation valuation);
     storm::expressions::SimpleValuation valuation;
@@ -379,7 +324,7 @@ TEST(Expression, SimpleEvaluationTest) {
     ASSERT_THROW(tempExpression.evaluateAsInt(&valuation), storm::exceptions::InvalidTypeException);
     EXPECT_FALSE(tempExpression.evaluateAsBool(&valuation));
     ASSERT_NO_THROW(valuation.setBooleanValue("a", true));
-    EXPECT_TRUE(tempExpression.evaluateAsBool(&valuation));
+    EXPECT_FALSE(tempExpression.evaluateAsBool(&valuation));
     ASSERT_NO_THROW(valuation.setIntegerValue("y", 3));
     EXPECT_FALSE(tempExpression.evaluateAsBool(&valuation));