Functional tests now work again.

Former-commit-id: 46d964ad22

src/parser/PrismParser.cpp

@@ -225,7 +225,7 @@ namespace storm {
         storm::prism::Constant PrismParser::createUndefinedBooleanConstant(std::string const& newConstant) const {
             if (!this->secondRun) {
                 try {
-                    storm::expressions::Variable newVariable = manager->declareVariable(newConstant, manager->getBooleanType());
+                    storm::expressions::Variable newVariable = manager->declareBooleanVariable(newConstant);
                     this->identifiers_.add(newConstant, newVariable.getExpression());
                 } catch (storm::exceptions::InvalidArgumentException const& e) {
                     if (manager->hasVariable(newConstant)) {
@@ -241,7 +241,7 @@ namespace storm {
         storm::prism::Constant PrismParser::createUndefinedIntegerConstant(std::string const& newConstant) const {
             if (!this->secondRun) {
                 try {
-                    storm::expressions::Variable newVariable = manager->declareVariable(newConstant, manager->getIntegerType());
+                    storm::expressions::Variable newVariable = manager->declareIntegerVariable(newConstant);
                     this->identifiers_.add(newConstant, newVariable.getExpression());
                 } catch (storm::exceptions::InvalidArgumentException const& e) {
                     if (manager->hasVariable(newConstant)) {
@@ -257,7 +257,7 @@ namespace storm {
         storm::prism::Constant PrismParser::createUndefinedDoubleConstant(std::string const& newConstant) const {
             if (!this->secondRun) {
                 try {
-                    storm::expressions::Variable newVariable = manager->declareVariable(newConstant, manager->getRationalType());
+                    storm::expressions::Variable newVariable = manager->declareRationalVariable(newConstant);
                     this->identifiers_.add(newConstant, newVariable.getExpression());
                 } catch (storm::exceptions::InvalidArgumentException const& e) {
                     if (manager->hasVariable(newConstant)) {
@@ -273,7 +273,7 @@ namespace storm {
         storm::prism::Constant PrismParser::createDefinedBooleanConstant(std::string const& newConstant, storm::expressions::Expression expression) const {
             if (!this->secondRun) {
                 try {
-                    storm::expressions::Variable newVariable = manager->declareVariable(newConstant, manager->getBooleanType());
+                    storm::expressions::Variable newVariable = manager->declareBooleanVariable(newConstant);
                     this->identifiers_.add(newConstant, newVariable.getExpression());
                 } catch (storm::exceptions::InvalidArgumentException const& e) {
                     if (manager->hasVariable(newConstant)) {
@@ -289,7 +289,7 @@ namespace storm {
         storm::prism::Constant PrismParser::createDefinedIntegerConstant(std::string const& newConstant, storm::expressions::Expression expression) const {
             if (!this->secondRun) {
                 try {
-                    storm::expressions::Variable newVariable = manager->declareVariable(newConstant, manager->getIntegerType());
+                    storm::expressions::Variable newVariable = manager->declareIntegerVariable(newConstant);
                     this->identifiers_.add(newConstant, newVariable.getExpression());
                 } catch (storm::exceptions::InvalidArgumentException const& e) {
                     if (manager->hasVariable(newConstant)) {
@@ -305,7 +305,7 @@ namespace storm {
         storm::prism::Constant PrismParser::createDefinedDoubleConstant(std::string const& newConstant, storm::expressions::Expression expression) const {
             if (!this->secondRun) {
                 try {
-                    storm::expressions::Variable newVariable = manager->declareVariable(newConstant, manager->getIntegerType());
+                    storm::expressions::Variable newVariable = manager->declareRationalVariable(newConstant);
                     this->identifiers_.add(newConstant, newVariable.getExpression());
                 } catch (storm::exceptions::InvalidArgumentException const& e) {
                     if (manager->hasVariable(newConstant)) {
@@ -361,7 +361,7 @@ namespace storm {
         storm::prism::BooleanVariable PrismParser::createBooleanVariable(std::string const& variableName, storm::expressions::Expression initialValueExpression) const {
             if (!this->secondRun) {
                 try {
-                    storm::expressions::Variable newVariable = manager->declareVariable(variableName, manager->getBooleanType());
+                    storm::expressions::Variable newVariable = manager->declareBooleanVariable(variableName);
                     this->identifiers_.add(variableName, newVariable.getExpression());
                 } catch (storm::exceptions::InvalidArgumentException const& e) {
                     if (manager->hasVariable(variableName)) {
@@ -377,7 +377,7 @@ namespace storm {
         storm::prism::IntegerVariable PrismParser::createIntegerVariable(std::string const& variableName, storm::expressions::Expression lowerBoundExpression, storm::expressions::Expression upperBoundExpression, storm::expressions::Expression initialValueExpression) const {
             if (!this->secondRun) {
                 try {
-                    storm::expressions::Variable newVariable = manager->declareVariable(variableName, manager->getIntegerType());
+                    storm::expressions::Variable newVariable = manager->declareIntegerVariable(variableName);
                     this->identifiers_.add(variableName, newVariable.getExpression());
                 } catch (storm::exceptions::InvalidArgumentException const& e) {
                     if (manager->hasVariable(variableName)) {
@@ -406,14 +406,14 @@ namespace storm {
                 for (auto const& variable : moduleToRename.getBooleanVariables()) {
                     auto const& renamingPair = renaming.find(variable.getName());
                     STORM_LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Boolean variable '" << variable.getName() << " was not renamed.");
-                    storm::expressions::Variable renamedVariable = manager->declareVariable(renamingPair->second, manager->getBooleanType());
-                    this->identifiers_.add(renamingPair->first, renamedVariable.getExpression());
+                    storm::expressions::Variable renamedVariable = manager->declareBooleanVariable(renamingPair->second);
+                    this->identifiers_.add(renamingPair->second, renamedVariable.getExpression());
                 }
                 for (auto const& variable : moduleToRename.getIntegerVariables()) {
                     auto const& renamingPair = renaming.find(variable.getName());
                     STORM_LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Integer variable '" << variable.getName() << " was not renamed.");
-                    storm::expressions::Variable renamedVariable = manager->declareVariable(renamingPair->second, manager->getBooleanType());
-                    this->identifiers_.add(renamingPair->first, renamedVariable.getExpression());
+                    storm::expressions::Variable renamedVariable = manager->declareIntegerVariable(renamingPair->second);
+                    this->identifiers_.add(renamingPair->second, renamedVariable.getExpression());
                 }
                 
                 // Return a dummy module in the first pass.

src/solver/GlpkLpSolver.cpp

@@ -48,59 +48,59 @@ namespace storm {
         }
         
         storm::expressions::Variable GlpkLpSolver::addBoundedContinuousVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient) {
-            storm::expressions::Variable newVariable = manager->declareVariable(name, manager->getRationalType());
+            storm::expressions::Variable newVariable = manager->declareRationalVariable(name);
             this->addVariable(newVariable, GLP_CV, GLP_DB, lowerBound, upperBound, objectiveFunctionCoefficient);
             return newVariable;
         }
         
         storm::expressions::Variable GlpkLpSolver::addLowerBoundedContinuousVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient) {
-            storm::expressions::Variable newVariable = manager->declareVariable(name, manager->getRationalType());
+            storm::expressions::Variable newVariable = manager->declareRationalVariable(name);
             this->addVariable(newVariable, GLP_CV, GLP_LO, lowerBound, 0, objectiveFunctionCoefficient);
             return newVariable;
         }
         
         storm::expressions::Variable GlpkLpSolver::addUpperBoundedContinuousVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient) {
-            storm::expressions::Variable newVariable = manager->declareVariable(name, manager->getRationalType());
+            storm::expressions::Variable newVariable = manager->declareRationalVariable(name);
             this->addVariable(newVariable, GLP_CV, GLP_UP, 0, upperBound, objectiveFunctionCoefficient);
             return newVariable;
         }
         
         storm::expressions::Variable GlpkLpSolver::addUnboundedContinuousVariable(std::string const& name, double objectiveFunctionCoefficient) {
-            storm::expressions::Variable newVariable = manager->declareVariable(name, manager->getRationalType());
+            storm::expressions::Variable newVariable = manager->declareRationalVariable(name);
             this->addVariable(newVariable, GLP_CV, GLP_FR, 0, 0, objectiveFunctionCoefficient);
             return newVariable;
         }
         
         storm::expressions::Variable GlpkLpSolver::addBoundedIntegerVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient) {
-            storm::expressions::Variable newVariable = manager->declareVariable(name, manager->getIntegerType());
+            storm::expressions::Variable newVariable = manager->declareIntegerVariable(name);
             this->addVariable(newVariable, GLP_IV, GLP_DB, lowerBound, upperBound, objectiveFunctionCoefficient);
             this->modelContainsIntegerVariables = true;
             return newVariable;
         }
         
         storm::expressions::Variable GlpkLpSolver::addLowerBoundedIntegerVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient) {
-            storm::expressions::Variable newVariable = manager->declareVariable(name, manager->getIntegerType());
+            storm::expressions::Variable newVariable = manager->declareIntegerVariable(name);
             this->addVariable(newVariable, GLP_IV, GLP_LO, lowerBound, 0, objectiveFunctionCoefficient);
             this->modelContainsIntegerVariables = true;
             return newVariable;
         }
 
         storm::expressions::Variable GlpkLpSolver::addUpperBoundedIntegerVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient) {
-            storm::expressions::Variable newVariable = manager->declareVariable(name, manager->getIntegerType());
+            storm::expressions::Variable newVariable = manager->declareIntegerVariable(name);
             this->addVariable(newVariable, GLP_IV, GLP_UP, 0, upperBound, objectiveFunctionCoefficient);
             this->modelContainsIntegerVariables = true;
             return newVariable;
         }
         
         storm::expressions::Variable GlpkLpSolver::addUnboundedIntegerVariable(std::string const& name, double objectiveFunctionCoefficient) {
-            storm::expressions::Variable newVariable = manager->declareVariable(name, manager->getIntegerType());
+            storm::expressions::Variable newVariable = manager->declareIntegerVariable(name);
             this->addVariable(newVariable, GLP_IV, GLP_FR, 0, 0, objectiveFunctionCoefficient);
             this->modelContainsIntegerVariables = true;
             return newVariable;
         }
         
         storm::expressions::Variable GlpkLpSolver::addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient) {
-            storm::expressions::Variable newVariable = manager->declareVariable(name, manager->getIntegerType());
+            storm::expressions::Variable newVariable = manager->declareIntegerVariable(name);
             this->addVariable(newVariable, GLP_BV, GLP_FR, 0, 0, objectiveFunctionCoefficient);
             this->modelContainsIntegerVariables = true;
             return newVariable;

src/solver/LpSolver.h

@@ -34,7 +34,7 @@ namespace storm {
              * @param modelSense A value indicating whether the objective function of this model is to be minimized or
              * maximized.
              */
-            LpSolver(ModelSense const& modelSense) : currentModelHasBeenOptimized(false), modelSense(modelSense) {
+            LpSolver(ModelSense const& modelSense) : manager(new storm::expressions::ExpressionManager()), currentModelHasBeenOptimized(false), modelSense(modelSense) {
                 // Intentionally left empty.
             }
 

src/storage/dd/CuddDdForwardIterator.cpp

@@ -5,7 +5,7 @@
 
 namespace storm {
     namespace dd {
-        DdForwardIterator<DdType::CUDD>::DdForwardIterator() : ddManager(), generator(), cube(), value(), isAtEnd(), metaVariables(), enumerateDontCareMetaVariables(), cubeCounter(), relevantDontCareDdVariables(), currentValuation(ddManager->getExpressionManager().getSharedPointer()) {
+        DdForwardIterator<DdType::CUDD>::DdForwardIterator() : ddManager(), generator(), cube(), value(), isAtEnd(), metaVariables(), enumerateDontCareMetaVariables(), cubeCounter(), relevantDontCareDdVariables(), currentValuation() {
             // Intentionally left empty.
         }
         
@@ -90,9 +90,9 @@ namespace storm {
                 } else {
                     storm::expressions::Variable const& metaVariable = std::get<1>(this->relevantDontCareDdVariables[index]);
                     if ((this->cubeCounter & (1ull << index)) != 0) {
-                        currentValuation.setIntegerValue(metaVariable, ((currentValuation.getIntegerValue(metaVariable) - ddMetaVariable.getLow()) | (1ull << std::get<2>(this->relevantDontCareDdVariables[index]))) + ddMetaVariable.getLow());
+                        currentValuation.setBoundedIntegerValue(metaVariable, ((currentValuation.getBoundedIntegerValue(metaVariable) - ddMetaVariable.getLow()) | (1ull << std::get<2>(this->relevantDontCareDdVariables[index]))) + ddMetaVariable.getLow());
                     } else {
-                        currentValuation.setIntegerValue(metaVariable, ((currentValuation.getIntegerValue(metaVariable) - ddMetaVariable.getLow()) & ~(1ull << std::get<2>(this->relevantDontCareDdVariables[index]))) + ddMetaVariable.getLow());
+                        currentValuation.setBoundedIntegerValue(metaVariable, ((currentValuation.getBoundedIntegerValue(metaVariable) - ddMetaVariable.getLow()) & ~(1ull << std::get<2>(this->relevantDontCareDdVariables[index]))) + ddMetaVariable.getLow());
                     }
                 }
             }
@@ -134,7 +134,7 @@ namespace storm {
                         }
                     }
                     if (this->enumerateDontCareMetaVariables || metaVariableAppearsInCube) {
-                        currentValuation.setIntegerValue(metaVariable, intValue + ddMetaVariable.getLow());
+                        currentValuation.setBoundedIntegerValue(metaVariable, intValue + ddMetaVariable.getLow());
                     }
                 }
                 

src/storage/dd/CuddDdManager.cpp

@@ -110,8 +110,8 @@ namespace storm {
             
             std::size_t numberOfBits = static_cast<std::size_t>(std::ceil(std::log2(high - low + 1)));
             
-            storm::expressions::Variable unprimed = manager->declareVariable(name, manager->getBoundedIntegerType(numberOfBits));
-            storm::expressions::Variable primed = manager->declareVariable(name + "'", manager->getBoundedIntegerType(numberOfBits));
+            storm::expressions::Variable unprimed = manager->declareBoundedIntegerVariable(name, numberOfBits);
+            storm::expressions::Variable primed = manager->declareBoundedIntegerVariable(name + "'", numberOfBits);
             
             std::vector<Dd<DdType::CUDD>> variables;
             std::vector<Dd<DdType::CUDD>> variablesPrime;
@@ -138,8 +138,8 @@ namespace storm {
             // Check whether a meta variable already exists.
             STORM_LOG_THROW(!this->hasMetaVariable(name), storm::exceptions::InvalidArgumentException, "A meta variable '" << name << "' already exists.");
             
-            storm::expressions::Variable unprimed = manager->declareVariable(name, manager->getBooleanType());
-            storm::expressions::Variable primed = manager->declareVariable(name + "'", manager->getBooleanType());
+            storm::expressions::Variable unprimed = manager->declareBooleanVariable(name);
+            storm::expressions::Variable primed = manager->declareBooleanVariable(name + "'");
 
             std::vector<Dd<DdType::CUDD>> variables;
             std::vector<Dd<DdType::CUDD>> variablesPrime;

src/storage/expressions/Expression.cpp

@@ -166,7 +166,7 @@ namespace storm {
         }
         
         Expression operator-(Expression const& first) {
-            return Expression(std::shared_ptr<BaseExpression>(new UnaryNumericalFunctionExpression(first.getBaseExpression().getManager(), first.getType(), first.getBaseExpressionPointer(), UnaryNumericalFunctionExpression::OperatorType::Minus)));
+            return Expression(std::shared_ptr<BaseExpression>(new UnaryNumericalFunctionExpression(first.getBaseExpression().getManager(), first.getType().minus(), first.getBaseExpressionPointer(), UnaryNumericalFunctionExpression::OperatorType::Minus)));
         }
         
         Expression operator*(Expression const& first, Expression const& second) {

src/storage/expressions/ExpressionManager.cpp

@@ -51,7 +51,7 @@ namespace storm {
             }
         }
         
-        ExpressionManager::ExpressionManager() : nameToIndexMapping(), indexToNameMapping(), indexToTypeMapping(), variableTypeToCountMapping(), numberOfVariables(0), auxiliaryVariableTypeToCountMapping(), numberOfAuxiliaryVariables(0), freshVariableCounter(0), booleanType(nullptr), integerType(nullptr), rationalType(nullptr) {
+        ExpressionManager::ExpressionManager() : nameToIndexMapping(), indexToNameMapping(), indexToTypeMapping(), numberOfVariables(0), variableTypeToCountMapping(), auxiliaryVariableTypeToCountMapping(), numberOfAuxiliaryVariables(0), freshVariableCounter(0), booleanType(nullptr), integerType(nullptr), rationalType(nullptr) {
             // Intentionally left empty.
         }
         
@@ -126,6 +126,10 @@ namespace storm {
             return this->declareVariable(name, this->getIntegerType());
         }
 
+        Variable ExpressionManager::declareBoundedIntegerVariable(std::string const& name, std::size_t width) {
+            return this->declareVariable(name, this->getBoundedIntegerType(width));
+        }
+        
         Variable ExpressionManager::declareRationalVariable(std::string const& name) {
             return this->declareVariable(name, this->getRationalType());
         }
@@ -218,6 +222,12 @@ namespace storm {
             return getNumberOfVariables(getIntegerType());
         }
         
+        uint_fast64_t ExpressionManager::getNumberOfBoundedIntegerVariables() const {
+            // The bit width of the type is not of importance here, since bit vector types are considered the same when
+            // it comes to counting.
+            return getNumberOfVariables(getBoundedIntegerType(0));
+        }
+        
         uint_fast64_t ExpressionManager::getNumberOfRationalVariables() const {
             return getNumberOfVariables(getRationalType());
         }
@@ -243,6 +253,12 @@ namespace storm {
             return getNumberOfAuxiliaryVariables(getIntegerType());
         }
         
+        uint_fast64_t ExpressionManager::getNumberOfAuxiliaryBoundedIntegerVariables() const {
+            // The bit width of the type is not of importance here, since bit vector types are considered the same when
+            // it comes to counting.
+            return getNumberOfAuxiliaryVariables(getBoundedIntegerType(0));
+        }
+        
         uint_fast64_t ExpressionManager::getNumberOfAuxiliaryRationalVariables() const {
             return getNumberOfAuxiliaryVariables(getRationalType());
         }
@@ -279,5 +295,9 @@ namespace storm {
             return this->shared_from_this();
         }
         
+        bool ExpressionManager::ManagerTypeEquality::operator()(Type const& a, Type const& b) const {
+            return a.getMask() == b.getMask();
+        }
+        
     } // namespace expressions
 } // namespace storm

src/storage/expressions/ExpressionManager.h

@@ -166,6 +166,17 @@ namespace storm {
              */
             Variable declareIntegerVariable(std::string const& name);
 
+            /*!
+             * Declares a new bounded integer variable with a name that must not yet exist and the bounded type of the
+             * given bit width. Note that the name must not start with two underscores since these variables are
+             * reserved for internal use only.
+             *
+             * @param name The name of the variable.
+             * @param width The bit width of the bounded type.
+             * @return The newly declared variable.
+             */
+            Variable declareBoundedIntegerVariable(std::string const& name, std::size_t width);
+            
             /*!
              * Declares a new rational variable with a name that must not yet exist and its corresponding type. Note that
              * the name must not start with two underscores since these variables are reserved for internal use only.
@@ -241,13 +252,6 @@ namespace storm {
              */
             Variable declareFreshAuxiliaryVariable(storm::expressions::Type const& variableType);
             
-            /*!
-             * Retrieves the number of variables with the given type.
-             *
-             * @return The number of variables with the given type.
-             */
-            uint_fast64_t getNumberOfVariables(storm::expressions::Type const& variableType) const;
-            
             /*!
              * Retrieves the number of variables.
              *
@@ -270,18 +274,18 @@ namespace storm {
             uint_fast64_t getNumberOfIntegerVariables() const;
 
             /*!
-             * Retrieves the number of rational variables.
+             * Retrieves the number of bounded integer variables.
              *
-             * @return The number of rational variables.
+             * @return The number of bounded integer variables.
              */
-            uint_fast64_t getNumberOfRationalVariables() const;
+            uint_fast64_t getNumberOfBoundedIntegerVariables() const;
             
             /*!
-             * Retrieves the number of auxiliary variables with the given type.
+             * Retrieves the number of rational variables.
              *
-             * @return The number of auxiliary variables with the given type.
+             * @return The number of rational variables.
              */
-            uint_fast64_t getNumberOfAuxiliaryVariables(storm::expressions::Type const& variableType) const;
+            uint_fast64_t getNumberOfRationalVariables() const;
             
             /*!
              * Retrieves the number of auxiliary variables.
@@ -291,23 +295,30 @@ namespace storm {
             uint_fast64_t getNumberOfAuxiliaryVariables() const;
             
             /*!
-             * Retrieves the number of boolean variables.
+             * Retrieves the number of auxiliary boolean variables.
              *
-             * @return The number of boolean variables.
+             * @return The number of auxiliary boolean variables.
              */
             uint_fast64_t getNumberOfAuxiliaryBooleanVariables() const;
             
             /*!
-             * Retrieves the number of integer variables.
+             * Retrieves the number of auxiliary integer variables.
              *
-             * @return The number of integer variables.
+             * @return The number of auxiliary integer variables.
              */
             uint_fast64_t getNumberOfAuxiliaryIntegerVariables() const;
             
             /*!
-             * Retrieves the number of rational variables.
+             * Retrieves the number of auxiliary bounded integer variables.
              *
-             * @return The number of rational variables.
+             * @return The number of auxiliary bounded integer variables.
+             */
+            uint_fast64_t getNumberOfAuxiliaryBoundedIntegerVariables() const;
+            
+            /*!
+             * Retrieves the number of auxiliary rational variables.
+             *
+             * @return The number of auxiliary rational variables.
              */
             uint_fast64_t getNumberOfAuxiliaryRationalVariables() const;
             
@@ -364,6 +375,12 @@ namespace storm {
             std::shared_ptr<ExpressionManager const> getSharedPointer() const;
 
         private:
+            // A functor used for treating bit vector types of different bit widths equally when it comes to the variable
+            // count.
+            struct ManagerTypeEquality {
+                bool operator()(Type const& a, Type const& b) const;
+            };
+            
             /*!
              * Checks whether the given variable name is valid.
              *
@@ -392,23 +409,39 @@ namespace storm {
              */
             Variable declareOrGetVariable(std::string const& name, storm::expressions::Type const& variableType, bool auxiliary, bool checkName);
             
+            /*!
+             * Retrieves the number of variables with the given type. Note that this considers bounded integer variables
+             * to be of the same type, no matter which bit width they have.
+             *
+             * @param variableType The type for which to query the number of variables.
+             */
+            uint_fast64_t getNumberOfVariables(storm::expressions::Type const& variableType) const;
+            
+            /*!
+             * Retrieves the number of auxiliary variables with the given type. Note that this considers bounded integer
+             * variables to be of the same type, no matter which bit width they have.
+             *
+             * @param variableType The type for which to query the number of auxiliary variables.
+             */
+            uint_fast64_t getNumberOfAuxiliaryVariables(storm::expressions::Type const& variableType) const;
+            
             // A mapping from all variable names (auxiliary + normal) to their indices.
             std::unordered_map<std::string, uint_fast64_t> nameToIndexMapping;
             
             // A mapping from all variable indices to their names.
-            std::unordered_map<uint_fast64_t, std::string> indexToNameMapping;
+            std::unordered_map<uint64_t, std::string> indexToNameMapping;
 
             // A mapping from all variable indices to their types.
-            std::unordered_map<uint_fast64_t, Type> indexToTypeMapping;
-            
-            // Store counts for variables.
-            std::unordered_map<Type, uint_fast64_t> variableTypeToCountMapping;
+            std::unordered_map<uint64_t, Type> indexToTypeMapping;
             
             // The number of declared variables.
             uint_fast64_t numberOfVariables;
 
+            // Store counts for variables.
+            std::unordered_map<Type, uint_fast64_t, std::hash<Type>, ManagerTypeEquality> variableTypeToCountMapping;
+
             // Store counts for auxiliary variables.
-            std::unordered_map<Type, uint_fast64_t> auxiliaryVariableTypeToCountMapping;
+            std::unordered_map<Type, uint_fast64_t, std::hash<Type>, ManagerTypeEquality> auxiliaryVariableTypeToCountMapping;
 
             // The number of declared auxiliary variables.
             uint_fast64_t numberOfAuxiliaryVariables;

src/storage/expressions/LinearCoefficientVisitor.cpp

@@ -32,8 +32,8 @@ namespace storm {
                 variableToCoefficientMapping = std::move(other.variableToCoefficientMapping);
                 std::swap(constantPart, other.constantPart);
             }
-            for (auto const& otherVariableCoefficientPair : other.variableToCoefficientMapping) {
-                this->variableToCoefficientMapping[otherVariableCoefficientPair.first] *= other.constantPart;
+            for (auto& variableCoefficientPair : this->variableToCoefficientMapping) {
+                variableCoefficientPair.second *= other.constantPart;
             }
             constantPart *= other.constantPart;
             return *this;
@@ -110,7 +110,7 @@ namespace storm {
             } else {
                 STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression is non-linear.");
             }
-            return rightResult;
+            return leftResult;
         }
         
         boost::any LinearCoefficientVisitor::visit(BinaryRelationExpression const& expression) {

src/storage/expressions/SimpleValuation.cpp

@@ -11,13 +11,16 @@ namespace storm {
             // Intentionally left empty.
         }
 
-        SimpleValuation::SimpleValuation(std::shared_ptr<storm::expressions::ExpressionManager const> const& manager) : Valuation(manager), booleanValues(nullptr), integerValues(nullptr), rationalValues(nullptr) {
+        SimpleValuation::SimpleValuation(std::shared_ptr<storm::expressions::ExpressionManager const> const& manager) : Valuation(manager), booleanValues(nullptr), integerValues(nullptr), boundedIntegerValues(nullptr), rationalValues(nullptr) {
             if (this->getManager().getNumberOfBooleanVariables() > 0) {
                 booleanValues = std::unique_ptr<std::vector<bool>>(new std::vector<bool>(this->getManager().getNumberOfBooleanVariables()));
             }
             if (this->getManager().getNumberOfIntegerVariables() > 0) {
                 integerValues = std::unique_ptr<std::vector<int_fast64_t>>(new std::vector<int_fast64_t>(this->getManager().getNumberOfIntegerVariables()));
             }
+            if (this->getManager().getNumberOfBoundedIntegerVariables() > 0) {
+                boundedIntegerValues = std::unique_ptr<std::vector<int_fast64_t>>(new std::vector<int_fast64_t>(this->getManager().getNumberOfBoundedIntegerVariables()));
+            }
             if (this->getManager().getNumberOfRationalVariables() > 0) {
                 rationalValues = std::unique_ptr<std::vector<double>>(new std::vector<double>(this->getManager().getNumberOfRationalVariables()));
             }
@@ -30,6 +33,9 @@ namespace storm {
             if (other.integerValues != nullptr) {
                 integerValues = std::unique_ptr<std::vector<int_fast64_t>>(new std::vector<int_fast64_t>(*other.integerValues));
             }
+            if (other.boundedIntegerValues != nullptr) {
+                boundedIntegerValues = std::unique_ptr<std::vector<int_fast64_t>>(new std::vector<int_fast64_t>(*other.boundedIntegerValues));
+            }
             if (other.rationalValues != nullptr) {
                 rationalValues = std::unique_ptr<std::vector<double>>(new std::vector<double>(*other.rationalValues));
             }
@@ -44,6 +50,9 @@ namespace storm {
                 if (other.integerValues != nullptr) {
                     integerValues = std::unique_ptr<std::vector<int_fast64_t>>(new std::vector<int_fast64_t>(*other.integerValues));
                 }
+                if (other.boundedIntegerValues != nullptr) {
+                    boundedIntegerValues = std::unique_ptr<std::vector<int_fast64_t>>(new std::vector<int_fast64_t>(*other.boundedIntegerValues));
+                }
                 if (other.booleanValues != nullptr) {
                     rationalValues = std::unique_ptr<std::vector<double>>(new std::vector<double>(*other.rationalValues));
                 }
@@ -81,6 +90,10 @@ namespace storm {
             return (*integerValues)[integerVariable.getOffset()];
         }
 
+        int_fast64_t SimpleValuation::getBoundedIntegerValue(Variable const& integerVariable) const {
+            return (*boundedIntegerValues)[integerVariable.getOffset()];
+        }
+        
         double SimpleValuation::getRationalValue(Variable const& rationalVariable) const {
             return (*rationalValues)[rationalVariable.getOffset()];
         }
@@ -93,6 +106,10 @@ namespace storm {
             (*integerValues)[integerVariable.getOffset()] = value;
         }
         
+        void SimpleValuation::setBoundedIntegerValue(Variable const& integerVariable, int_fast64_t value) {
+            (*boundedIntegerValues)[integerVariable.getOffset()] = value;
+        }
+        
         void SimpleValuation::setRationalValue(Variable const& rationalVariable, double value) {
             (*rationalValues)[rationalVariable.getOffset()] = value;
         }

src/storage/expressions/SimpleValuation.h

@@ -47,7 +47,9 @@ namespace storm {
             virtual bool getBooleanValue(Variable const& booleanVariable) const override;
             virtual void setBooleanValue(Variable const& booleanVariable, bool value) override;
             virtual int_fast64_t getIntegerValue(Variable const& integerVariable) const override;
+            virtual int_fast64_t getBoundedIntegerValue(Variable const& integerVariable) const override;
             virtual void setIntegerValue(Variable const& integerVariable, int_fast64_t value) override;
+            virtual void setBoundedIntegerValue(Variable const& integerVariable, int_fast64_t value) override;
             virtual double getRationalValue(Variable const& rationalVariable) const override;
             virtual void setRationalValue(Variable const& rationalVariable, double value) override;
             
@@ -55,6 +57,7 @@ namespace storm {
             // Containers that store the values of the variables of the appropriate type.
             std::unique_ptr<std::vector<bool>> booleanValues;
             std::unique_ptr<std::vector<int_fast64_t>> integerValues;
+            std::unique_ptr<std::vector<int_fast64_t>> boundedIntegerValues;
             std::unique_ptr<std::vector<double>> rationalValues;
         };
         

src/storage/expressions/Type.cpp

@@ -4,6 +4,7 @@
 
 #include "src/storage/expressions/ExpressionManager.h"
 #include "src/utility/macros.h"
+#include "src/exceptions/InvalidTypeException.h"
 
 namespace storm {
     namespace expressions {
@@ -145,7 +146,7 @@ namespace storm {
         }
         
         Type Type::plusMinusTimes(Type const& other) const {
-            STORM_LOG_ASSERT(this->isNumericalType() && other.isNumericalType(), "Operator requires numerical operands.");
+            STORM_LOG_THROW(this->isNumericalType() && other.isNumericalType(), storm::exceptions::InvalidTypeException, "Operator requires numerical operands.");
             if (this->isRationalType() || other.isRationalType()) {
                 return this->getManager().getRationalType();
             }
@@ -153,17 +154,20 @@ namespace storm {
         }
         
         Type Type::minus() const {
-            STORM_LOG_ASSERT(this->isNumericalType(), "Operator requires numerical operand.");
+            STORM_LOG_THROW(this->isNumericalType(), storm::exceptions::InvalidTypeException, "Operator requires numerical operand.");
             return *this;
         }
         
         Type Type::divide(Type const& other) const {
-            STORM_LOG_ASSERT(this->isNumericalType() && other.isNumericalType(), "Operator requires numerical operands.");
+            STORM_LOG_THROW(this->isNumericalType() && other.isNumericalType(), storm::exceptions::InvalidTypeException, "Operator requires numerical operands.");
+            if (this->isRationalType() || other.isRationalType()) {
                 return this->getManager().getRationalType();
             }
+            return this->getManager().getIntegerType();
+        }
         
         Type Type::power(Type const& other) const {
-            STORM_LOG_ASSERT(this->isNumericalType() && other.isNumericalType(), "Operator requires numerical operands.");
+            STORM_LOG_THROW(this->isNumericalType() && other.isNumericalType(), storm::exceptions::InvalidTypeException, "Operator requires numerical operands.");
             if (this->isRationalType() || other.isRationalType()) {
                 return getManager().getRationalType();
             }
@@ -171,33 +175,42 @@ namespace storm {
         }
         
         Type Type::logicalConnective(Type const& other) const {
-            STORM_LOG_ASSERT(this->isBooleanType() && other.isBooleanType(), "Operator requires boolean operands.");
+            STORM_LOG_THROW(this->isBooleanType() && other.isBooleanType(), storm::exceptions::InvalidTypeException, "Operator requires boolean operands.");
             return *this;
         }
         
         Type Type::logicalConnective() const {
-            STORM_LOG_ASSERT(this->isBooleanType(), "Operator requires boolean operand.");
+            STORM_LOG_THROW(this->isBooleanType(), storm::exceptions::InvalidTypeException, "Operator requires boolean operand.");
             return *this;
         }
         
         Type Type::numericalComparison(Type const& other) const {
-            STORM_LOG_ASSERT(this->isNumericalType() && other.isNumericalType(), "Operator requires numerical operands.");
+            STORM_LOG_THROW(this->isNumericalType() && other.isNumericalType(), storm::exceptions::InvalidTypeException, "Operator requires numerical operands.");
             return this->getManager().getBooleanType();
         }
         
         Type Type::ite(Type const& thenType, Type const& elseType) const {
-            STORM_LOG_ASSERT(this->isBooleanType(), "Operator requires boolean condition.");
-            STORM_LOG_ASSERT(thenType == elseType, "Operator requires equal types.");
+            STORM_LOG_THROW(this->isBooleanType(), storm::exceptions::InvalidTypeException, "Operator requires boolean condition.");
+            if (thenType == elseType) {
+                return thenType;
+            } else {
+                STORM_LOG_THROW(thenType.isNumericalType() == elseType.isNumericalType(), storm::exceptions::InvalidTypeException, "Operator 'ite' requires proper types.");
+                if (thenType.isRationalType() || elseType.isRationalType()) {
+                    return this->getManager().getRationalType();
+                } else {
+                    return this->getManager().getIntegerType();
+                }
+            }
             return thenType;
         }
         
         Type Type::floorCeil() const {
-            STORM_LOG_ASSERT(this->isRationalType(), "Operator requires rational operand.");
+            STORM_LOG_THROW(this->isNumericalType(), storm::exceptions::InvalidTypeException, "Operator requires rational operand.");
             return this->getManager().getIntegerType();
         }
         
         Type Type::minimumMaximum(Type const& other) const {
-            STORM_LOG_ASSERT(this->isNumericalType() && other.isNumericalType(), "Operator requires numerical operands.");
+            STORM_LOG_THROW(this->isNumericalType() && other.isNumericalType(), storm::exceptions::InvalidTypeException, "Operator requires numerical operands.");
             if (this->isRationalType() || other.isRationalType()) {
                 return this->getManager().getRationalType();
             }

src/storage/expressions/Valuation.h

@@ -48,13 +48,29 @@ namespace storm {
             virtual int_fast64_t getIntegerValue(Variable const& integerVariable) const = 0;
 
             /*!
-             * Sets the value of the given boolean variable to the provided value.
+             * Retrieves the value of the given bounded integer variable.
+             *
+             * @param integerVariable The bounded integer variable whose value to retrieve.
+             * @return The value of the bounded integer variable.
+             */
+            virtual int_fast64_t getBoundedIntegerValue(Variable const& integerVariable) const = 0;
+            
+            /*!
+             * Sets the value of the given integer variable to the provided value.
              *
              * @param integerVariable The variable whose value to set.
              * @param value The new value of the variable.
              */
             virtual void setIntegerValue(Variable const& integerVariable, int_fast64_t value) = 0;
 
+            /*!
+             * Sets the value of the given bounded integer variable to the provided value.
+             *
+             * @param integerVariable The variable whose value to set.
+             * @param value The new value of the variable.
+             */
+            virtual void setBoundedIntegerValue(Variable const& integerVariable, int_fast64_t value) = 0;
+
             /*!
              * Retrieves the value of the given rational variable.
              *

src/storage/prism/Program.cpp

@@ -16,7 +16,6 @@ namespace storm {
             
             // Create a new initial construct if the corresponding flag was set.
             if (fixInitialConstruct) {
-                if (this->getInitialConstruct().getInitialStatesExpression().isFalse()) {
                 storm::expressions::Expression newInitialExpression = manager->boolean(true);
                 
                 for (auto const& booleanVariable : this->getGlobalBooleanVariables()) {
@@ -35,7 +34,6 @@ namespace storm {
                 }
                 this->initialConstruct = storm::prism::InitialConstruct(newInitialExpression, this->getInitialConstruct().getFilename(), this->getInitialConstruct().getLineNumber());
             }
-            }
             
             if (checkValidity) {
                 this->checkValidity();

test/functional/parser/PrismParserTest.cpp

@@ -58,7 +58,7 @@ TEST(PrismParser, ComplexTest) {
     
     formula test = a >= 10 & (max(a,b) > floor(e));
     formula test2 = a+b;
-    formula test3 = (a + b > 10 ? floor(a) : h) + a;
+    formula test3 = (a + b > 10 ? floor(e) : h) + a;
     
     global g : bool init false;
     global h : [0 .. b];
@@ -68,7 +68,7 @@ TEST(PrismParser, ComplexTest) {
         j : bool init c;
         k : [125..a] init a;
 
-        [a] test&false -> (i'=true)&(k'=1+1) + 1 : (k'=floor(a) + max(k, b) - 1 + k);
+        [a] test&false -> (i'=true)&(k'=1+1) + 1 : (k'=floor(e) + max(k, b) - 1 + k);
     endmodule
                                               
     module mod2

test/functional/solver/GlpkLpSolverTest.cpp

@@ -51,7 +51,7 @@ TEST(GlpkLpSolver, LPOptimizeMin) {
     ASSERT_NO_THROW(solver.update());
 
     ASSERT_NO_THROW(solver.addConstraint("", x + y + z <= solver.getConstant(12)));
-    ASSERT_NO_THROW(solver.addConstraint("", solver.getConstant(0.5) * y + z - x == solver.getConstant(5)));
+    ASSERT_NO_THROW(solver.addConstraint("", solver.getConstant(0.5) * y + z - x <= solver.getConstant(5)));
     ASSERT_NO_THROW(solver.addConstraint("", y - x <= solver.getConstant(5.5)));
     ASSERT_NO_THROW(solver.update());
 
@@ -117,7 +117,7 @@ TEST(GlpkLpSolver, MILPOptimizeMin) {
     ASSERT_NO_THROW(solver.update());
 
     ASSERT_NO_THROW(solver.addConstraint("", x + y + z <= solver.getConstant(12)));
-    ASSERT_NO_THROW(solver.addConstraint("", solver.getConstant(0.5) * y + z - x == solver.getConstant(5)));
+    ASSERT_NO_THROW(solver.addConstraint("", solver.getConstant(0.5) * y + z - x <= solver.getConstant(5)));
     ASSERT_NO_THROW(solver.addConstraint("", y - x <= solver.getConstant(5.5)));
     ASSERT_NO_THROW(solver.update());
 

test/functional/solver/GurobiLpSolverTest.cpp

@@ -51,7 +51,7 @@ TEST(GurobiLpSolver, LPOptimizeMin) {
     ASSERT_NO_THROW(solver.update());
     
     ASSERT_NO_THROW(solver.addConstraint("", x + y + z <= solver.getConstant(12)));
-    ASSERT_NO_THROW(solver.addConstraint("", solver.getConstant(0.5) * y + z - x == solver.getConstant(5)));
+    ASSERT_NO_THROW(solver.addConstraint("", solver.getConstant(0.5) * y + z - x <= solver.getConstant(5)));
     ASSERT_NO_THROW(solver.addConstraint("", y - x <= solver.getConstant(5.5)));
     ASSERT_NO_THROW(solver.update());
     
@@ -117,7 +117,7 @@ TEST(GurobiLpSolver, MILPOptimizeMin) {
     ASSERT_NO_THROW(solver.update());
     
     ASSERT_NO_THROW(solver.addConstraint("", x + y + z <= solver.getConstant(12)));
-    ASSERT_NO_THROW(solver.addConstraint("", solver.getConstant(0.5) * y + z - x == solver.getConstant(5)));
+    ASSERT_NO_THROW(solver.addConstraint("", solver.getConstant(0.5) * y + z - x <= solver.getConstant(5)));
     ASSERT_NO_THROW(solver.addConstraint("", y - x <= solver.getConstant(5.5)));
     ASSERT_NO_THROW(solver.update());