Started working on making the main executable build again.

Former-commit-id: 9aaad15b9f

src/adapters/ExplicitModelAdapter.h

@@ -101,7 +101,7 @@ namespace storm {
             static std::unique_ptr<storm::models::AbstractModel<ValueType>> translateProgram(storm::prism::Program program, bool rewards = true, std::string const& rewardModelName = "", std::string const& constantDefinitionString = "") {
                 // Start by defining the undefined constants in the model.
                 // First, we need to parse the constant definition string.
-                std::map<std::string, storm::expressions::Expression> constantDefinitions = storm::utility::prism::parseConstantDefinitionString(program, constantDefinitionString);
+                std::map<storm::expressions::Variable, storm::expressions::Expression> constantDefinitions = storm::utility::prism::parseConstantDefinitionString(program, constantDefinitionString);
                 
                 storm::prism::Program preparedProgram = program.defineUndefinedConstants(constantDefinitions);
                 STORM_LOG_THROW(!preparedProgram.hasUndefinedConstants(), storm::exceptions::InvalidArgumentException, "Program still contains undefined constants.");

src/adapters/MathsatExpressionAdapter.h

@@ -265,9 +265,9 @@ namespace storm {
                 msat_decl msatDeclaration;
                 if (variable.getType().isBooleanType()) {
                     msatDeclaration = msat_declare_function(env, variable.getName().c_str(), msat_get_bool_type(env));
-                } else if (variable.getType().isUnboundedIntegralType()) {
+                } else if (variable.getType().isUnboundedIntegerType()) {
                     msatDeclaration = msat_declare_function(env, variable.getName().c_str(), msat_get_integer_type(env));
-                } else if (variable.getType().isBoundedIntegralType()) {
+                } else if (variable.getType().isBoundedIntegerType()) {
                     msatDeclaration = msat_declare_function(env, variable.getName().c_str(), msat_get_bv_type(env, variable.getType().getWidth()));
                 } else if (variable.getType().isRationalType()) {
                     msatDeclaration = msat_declare_function(env, variable.getName().c_str(), msat_get_rational_type(env));

src/adapters/Z3ExpressionAdapter.h

@@ -310,9 +310,9 @@ namespace storm {
                 z3::expr z3Variable(context);
                 if (variable.getType().isBooleanType()) {
                     z3Variable = context.bool_const(variable.getName().c_str());
-                } else if (variable.getType().isUnboundedIntegralType()) {
+                } else if (variable.getType().isUnboundedIntegerType()) {
                     z3Variable = context.int_const(variable.getName().c_str());
-                } else if (variable.getType().isBoundedIntegralType()) {
+                } else if (variable.getType().isBoundedIntegerType()) {
                     z3Variable = context.bv_const(variable.getName().c_str(), variable.getType().getWidth());
                 } else if (variable.getType().isRationalType()) {
                     z3Variable = context.real_const(variable.getName().c_str());

src/solver/Z3SmtSolver.cpp

@@ -210,7 +210,7 @@ namespace storm {
 
                 if (variableInterpretation.getType().isBooleanType()) {
                     stormModel.setBooleanValue(this->getManager().getVariable(variableI.name().str()), variableInterpretation.isTrue());
-                } else if (variableInterpretation.getType().isIntegralType()) {
+                } else if (variableInterpretation.getType().isIntegerType()) {
                     stormModel.setIntegerValue(this->getManager().getVariable(variableI.name().str()), variableInterpretation.evaluateAsInt());
                 } else if (variableInterpretation.getType().isRationalType()) {
                     stormModel.setRationalValue(this->getManager().getVariable(variableI.name().str()), variableInterpretation.evaluateAsDouble());

src/storage/expressions/BaseExpression.cpp

@@ -14,8 +14,12 @@ namespace storm {
             return this->type;
         }
         
-        bool BaseExpression::hasIntegralType() const {
-            return this->getType().isIntegralType();
+        bool BaseExpression::hasIntegerType() const {
+            return this->getType().isIntegerType();
+        }
+
+        bool BaseExpression::hasBoundedIntegerType() const {
+            return this->getType().isBoundedIntegerType();
         }
         
         bool BaseExpression::hasNumericalType() const {

src/storage/expressions/BaseExpression.h

@@ -175,12 +175,19 @@ namespace storm {
             bool hasNumericalType() const;
             
             /*!
-             * Retrieves whether the expression has an integral type, i.e., integer.
+             * Retrieves whether the expression has an integer type.
              *
-             * @return True iff the expression has an integral type.
+             * @return True iff the expression has an integer type.
              */
-            bool hasIntegralType() const;
+            bool hasIntegerType() const;
             
+            /*!
+             * Retrieves whether the expression has a bounded integer type.
+             *
+             * @return True iff the expression has a bounded integer type.
+             */
+            bool hasBoundedIntegerType() const;
+
             /*!
              * Retrieves whether the expression has a boolean type.
              *

src/storage/expressions/BinaryNumericalFunctionExpression.cpp

@@ -28,7 +28,7 @@ namespace storm {
         }
         
         int_fast64_t BinaryNumericalFunctionExpression::evaluateAsInt(Valuation const* valuation) const {
-            STORM_LOG_THROW(this->hasIntegralType(), storm::exceptions::InvalidTypeException, "Unable to evaluate expression as integer.");
+            STORM_LOG_THROW(this->hasIntegerType(), storm::exceptions::InvalidTypeException, "Unable to evaluate expression as integer.");
             
             int_fast64_t firstOperandEvaluation = this->getFirstOperand()->evaluateAsInt(valuation);
             int_fast64_t secondOperandEvaluation = this->getSecondOperand()->evaluateAsInt(valuation);

src/storage/expressions/Expression.cpp

@@ -142,8 +142,12 @@ namespace storm {
             return this->getBaseExpression().hasBooleanType();
         }
         
-        bool Expression::hasIntegralType() const {
-            return this->getBaseExpression().hasIntegralType();
+        bool Expression::hasIntegerType() const {
+            return this->getBaseExpression().hasIntegerType();
+        }
+        
+        bool Expression::hasBoundedIntegerType() const {
+            return this->getBaseExpression().hasBoundedIntegerType();
         }
         
         boost::any Expression::accept(ExpressionVisitor& visitor) const {

src/storage/expressions/Expression.h

@@ -267,7 +267,14 @@ namespace storm {
              *
              * @return True iff the expression has a integral return type.
              */
-            bool hasIntegralType() const;
+            bool hasIntegerType() const;
+
+            /*!
+             * Retrieves whether the expression has an integral return type.
+             *
+             * @return True iff the expression has a integral return type.
+             */
+            bool hasBoundedIntegerType() const;
             
             /*!
              * Accepts the given visitor.

src/storage/expressions/Type.cpp

@@ -114,22 +114,22 @@ namespace storm {
         }
         
         bool Type::isNumericalType() const {
-            return this->isIntegralType() || this->isRationalType();
+            return this->isIntegerType() || this->isRationalType();
         }
         
-        bool Type::isIntegralType() const {
-            return this->isUnboundedIntegralType() || this->isBoundedIntegralType();
+        bool Type::isIntegerType() const {
+            return this->isUnboundedIntegerType() || this->isBoundedIntegerType();
         }
         
         bool Type::isBooleanType() const {
             return this->innerType->isBooleanType();
         }
         
-        bool Type::isUnboundedIntegralType() const {
+        bool Type::isUnboundedIntegerType() const {
             return this->innerType->isIntegerType();
         }
         
-        bool Type::isBoundedIntegralType() const {
+        bool Type::isBoundedIntegerType() const {
             return this->innerType->isBoundedIntegerType();
         }
         

src/storage/expressions/Type.h

@@ -161,7 +161,7 @@ namespace storm {
              *
              * @return True iff the type is a integral one.
              */
-            bool isIntegralType() const;
+            bool isIntegerType() const;
 
             /*!
              * Checks whether this type is a boolean type.
@@ -175,14 +175,14 @@ namespace storm {
              *
              * @return True iff the type is a unbounded integral one.
              */
-            bool isUnboundedIntegralType() const;
+            bool isUnboundedIntegerType() const;
             
             /*!
              * Checks whether this type is a bounded integral type.
              *
              * @return True iff the type is a bounded integral one.
              */
-            bool isBoundedIntegralType() const;
+            bool isBoundedIntegerType() const;
             
             /*!
              * Retrieves the bit width of the type, provided that it is a bounded integral type.

src/storage/expressions/UnaryNumericalFunctionExpression.cpp

@@ -23,7 +23,7 @@ namespace storm {
         }
         
         int_fast64_t UnaryNumericalFunctionExpression::evaluateAsInt(Valuation const* valuation) const {
-            STORM_LOG_THROW(this->hasIntegralType(), storm::exceptions::InvalidTypeException, "Unable to evaluate expression as integer.");
+            STORM_LOG_THROW(this->hasIntegerType(), storm::exceptions::InvalidTypeException, "Unable to evaluate expression as integer.");
 
             int_fast64_t operandEvaluated = this->getOperand()->evaluateAsInt(valuation);
             switch (this->getOperatorType()) {

src/storage/expressions/Variable.cpp

@@ -44,14 +44,18 @@ namespace storm {
         }
         
         bool Variable::hasIntegerType() const {
-            return this->getType().isIntegralType();
+            return this->getType().isIntegerType();
         }
 
+        bool Variable::hasBoundedIntegerType() const {
+            return this->getType().isBoundedIntegerType();
+        }
+        
         bool Variable::hasRationalType() const {
             return this->getType().isRationalType();
         }
 
-        bool Variable::hasNumericType() const {
+        bool Variable::hasNumericalType() const {
             return this->getType().isNumericalType();
         }
     }

src/storage/expressions/Variable.h

@@ -105,6 +105,13 @@ namespace storm {
              */
             bool hasIntegerType() const;
 
+            /*!
+             * Checks whether the variable is of integral type.
+             *
+             * @return True iff the variable if of integral type.
+             */
+            bool hasBoundedIntegerType() const;
+            
             /*!
              * Checks whether the variable is of rational type.
              *
@@ -117,7 +124,7 @@ namespace storm {
              *
              * @return True iff the variable if of boolean type.
              */
-            bool hasNumericType() const;
+            bool hasNumericalType() const;
 
         private:
             // The manager that is responsible for this variable.

src/storage/expressions/VariableExpression.cpp

@@ -25,7 +25,7 @@ namespace storm {
 
         int_fast64_t VariableExpression::evaluateAsInt(Valuation const* valuation) const {
             STORM_LOG_ASSERT(valuation != nullptr, "Evaluating expressions with unknowns without valuation.");
-            STORM_LOG_THROW(this->hasIntegralType(), storm::exceptions::InvalidTypeException, "Cannot evaluate expression as integer: return type is not an integer.");
+            STORM_LOG_THROW(this->hasIntegerType(), storm::exceptions::InvalidTypeException, "Cannot evaluate expression as integer: return type is not an integer.");
             
             return valuation->getIntegerValue(this->getVariable());
         }
@@ -34,7 +34,7 @@ namespace storm {
             STORM_LOG_ASSERT(valuation != nullptr, "Evaluating expressions with unknowns without valuation.");
             STORM_LOG_THROW(this->hasNumericalType(), storm::exceptions::InvalidTypeException, "Cannot evaluate expression as double: return type is not a double.");
             
-            if (this->getType().isIntegralType()) {
+            if (this->getType().isIntegerType()) {
                 return static_cast<double>(valuation->getIntegerValue(this->getVariable()));
             } else {
                 return valuation->getRationalValue(this->getVariable());

src/utility/PrismUtility.h

@@ -189,9 +189,9 @@ namespace storm {
                 labeledEntry.addValue(probability, labels);
             }
             
-            static std::map<std::string, storm::expressions::Expression> parseConstantDefinitionString(storm::prism::Program const& program, std::string const& constantDefinitionString) {
-                std::map<std::string, storm::expressions::Expression> constantDefinitions;
-                std::set<std::string> definedConstants;
+            static std::map<storm::expressions::Variable, storm::expressions::Expression> parseConstantDefinitionString(storm::prism::Program const& program, std::string const& constantDefinitionString) {
+                std::map<storm::expressions::Variable, storm::expressions::Expression> constantDefinitions;
+                std::set<storm::expressions::Variable> definedConstants;
                 
                 if (!constantDefinitionString.empty()) {
                     // Parse the string that defines the undefined constants of the model and make sure that it contains exactly
@@ -217,24 +217,25 @@ namespace storm {
                         if (program.hasConstant(constantName)) {
                             // Get the actual constant and check whether it's in fact undefined.
                             auto const& constant = program.getConstant(constantName);
+                            storm::expressions::Variable variable = constant.getExpressionVariable();
                             STORM_LOG_THROW(!constant.isDefined(), storm::exceptions::InvalidArgumentException, "Illegally trying to define already defined constant '" << constantName <<"'.");
-                            STORM_LOG_THROW(definedConstants.find(constantName) == definedConstants.end(), storm::exceptions::InvalidArgumentException, "Illegally trying to define constant '" << constantName <<"' twice.");
-                            definedConstants.insert(constantName);
+                            STORM_LOG_THROW(definedConstants.find(variable) == definedConstants.end(), storm::exceptions::InvalidArgumentException, "Illegally trying to define constant '" << constantName <<"' twice.");
+                            definedConstants.insert(variable);
                             
-                            if (constant.getType() == storm::expressions::ExpressionReturnType::Bool) {
+                            if (constant.getType().isBooleanType()) {
                                 if (value == "true") {
-                                    constantDefinitions[constantName] = storm::expressions::Expression::createTrue();
+                                    constantDefinitions[variable] = program.getManager().boolean(true);
                                 } else if (value == "false") {
-                                    constantDefinitions[constantName] = storm::expressions::Expression::createFalse();
+                                    constantDefinitions[variable] = program.getManager().boolean(false);
                                 } else {
                                     throw storm::exceptions::InvalidArgumentException() << "Illegal value for boolean constant: " << value << ".";
                                 }
-                            } else if (constant.getType() == storm::expressions::ExpressionReturnType::Int) {
+                            } else if (constant.getType().isIntegerType()) {
                                 int_fast64_t integerValue = std::stoi(value);
-                                constantDefinitions[constantName] = storm::expressions::Expression::createIntegerLiteral(integerValue);
-                            } else if (constant.getType() == storm::expressions::ExpressionReturnType::Double) {
+                                constantDefinitions[variable] = program.getManager().integer(integerValue);
+                            } else if (constant.getType().isRationalType()) {
                                 double doubleValue = std::stod(value);
-                                constantDefinitions[constantName] = storm::expressions::Expression::createDoubleLiteral(doubleValue);
+                                constantDefinitions[variable] = program.getManager().rational(doubleValue);
                             }
                         } else {
                             throw storm::exceptions::InvalidArgumentException() << "Illegal constant definition string: unknown undefined constant " << constantName << ".";

test/functional/storage/ExpressionTest.cpp

@@ -50,7 +50,7 @@ TEST(Expression, AccessorTest) {
     EXPECT_TRUE(falseExpression.isFalse());
     EXPECT_TRUE(falseExpression.getVariables() == std::set<storm::expressions::Variable>());
 
-    EXPECT_TRUE(threeExpression.hasIntegralType());
+    EXPECT_TRUE(threeExpression.hasIntegerType());
     EXPECT_TRUE(threeExpression.isLiteral());
     EXPECT_FALSE(threeExpression.isTrue());
     EXPECT_FALSE(threeExpression.isFalse());
@@ -68,7 +68,7 @@ TEST(Expression, AccessorTest) {
     EXPECT_FALSE(boolVarExpression.isFalse());
     EXPECT_TRUE(boolVarExpression.getVariables() == std::set<storm::expressions::Variable>({manager->getVariable("x")}));
 
-    EXPECT_TRUE(intVarExpression.hasIntegralType());
+    EXPECT_TRUE(intVarExpression.hasIntegerType());
     EXPECT_FALSE(intVarExpression.isLiteral());
     EXPECT_FALSE(intVarExpression.isTrue());
     EXPECT_FALSE(intVarExpression.isFalse());
@@ -106,13 +106,13 @@ TEST(Expression, OperatorTest) {
     ASSERT_NO_THROW(tempExpression = storm::expressions::ite(boolVarExpression, threeExpression, rationalVarExpression));
     EXPECT_TRUE(tempExpression.hasRationalType());
     ASSERT_NO_THROW(tempExpression = storm::expressions::ite(boolVarExpression, threeExpression, intVarExpression));
-    EXPECT_TRUE(tempExpression.hasIntegralType());
+    EXPECT_TRUE(tempExpression.hasIntegerType());
     ASSERT_NO_THROW(tempExpression = storm::expressions::ite(boolVarExpression, trueExpression, falseExpression));
     EXPECT_TRUE(tempExpression.hasBooleanType());
     
     ASSERT_THROW(tempExpression = trueExpression + piExpression, storm::exceptions::InvalidTypeException);
     ASSERT_NO_THROW(tempExpression = threeExpression + threeExpression);
-    EXPECT_TRUE(tempExpression.hasIntegralType());
+    EXPECT_TRUE(tempExpression.hasIntegerType());
     ASSERT_NO_THROW(tempExpression = threeExpression + piExpression);
     EXPECT_TRUE(tempExpression.hasRationalType());
     ASSERT_NO_THROW(tempExpression = rationalVarExpression + rationalVarExpression);
@@ -120,7 +120,7 @@ TEST(Expression, OperatorTest) {
     
     ASSERT_THROW(tempExpression = trueExpression - piExpression, storm::exceptions::InvalidTypeException);
     ASSERT_NO_THROW(tempExpression = threeExpression - threeExpression);
-    EXPECT_TRUE(tempExpression.hasIntegralType());
+    EXPECT_TRUE(tempExpression.hasIntegerType());
     ASSERT_NO_THROW(tempExpression = threeExpression - piExpression);
     EXPECT_TRUE(tempExpression.hasRationalType());
     ASSERT_NO_THROW(tempExpression = rationalVarExpression - rationalVarExpression);
@@ -128,7 +128,7 @@ TEST(Expression, OperatorTest) {
     
     ASSERT_THROW(tempExpression = -trueExpression, storm::exceptions::InvalidTypeException);
     ASSERT_NO_THROW(tempExpression = -threeExpression);
-    EXPECT_TRUE(tempExpression.hasIntegralType());
+    EXPECT_TRUE(tempExpression.hasIntegerType());
     ASSERT_NO_THROW(tempExpression = -piExpression);
     EXPECT_TRUE(tempExpression.hasRationalType());
     ASSERT_NO_THROW(tempExpression = -rationalVarExpression);
@@ -136,15 +136,15 @@ TEST(Expression, OperatorTest) {
 
     ASSERT_THROW(tempExpression = trueExpression * piExpression, storm::exceptions::InvalidTypeException);
     ASSERT_NO_THROW(tempExpression = threeExpression * threeExpression);
-    EXPECT_TRUE(tempExpression.hasIntegralType());
+    EXPECT_TRUE(tempExpression.hasIntegerType());
     ASSERT_NO_THROW(tempExpression = threeExpression * piExpression);
     EXPECT_TRUE(tempExpression.hasRationalType());
     ASSERT_NO_THROW(tempExpression = intVarExpression * intVarExpression);
-    EXPECT_TRUE(tempExpression.hasIntegralType());
+    EXPECT_TRUE(tempExpression.hasIntegerType());
 
     ASSERT_THROW(tempExpression = trueExpression / piExpression, storm::exceptions::InvalidTypeException);
     ASSERT_NO_THROW(tempExpression = threeExpression / threeExpression);
-    EXPECT_TRUE(tempExpression.hasIntegralType());
+    EXPECT_TRUE(tempExpression.hasIntegerType());
     ASSERT_NO_THROW(tempExpression = threeExpression / piExpression);
     EXPECT_TRUE(tempExpression.hasRationalType());
     ASSERT_NO_THROW(tempExpression = rationalVarExpression / intVarExpression);
@@ -206,13 +206,13 @@ TEST(Expression, OperatorTest) {
     
     ASSERT_THROW(tempExpression = storm::expressions::minimum(trueExpression, piExpression), storm::exceptions::InvalidTypeException);
     ASSERT_NO_THROW(tempExpression = storm::expressions::minimum(threeExpression, threeExpression));
-    EXPECT_TRUE(tempExpression.hasIntegralType());
+    EXPECT_TRUE(tempExpression.hasIntegerType());
     ASSERT_NO_THROW(tempExpression = storm::expressions::minimum(intVarExpression, rationalVarExpression));
     EXPECT_TRUE(tempExpression.hasRationalType());
 
     ASSERT_THROW(tempExpression = storm::expressions::maximum(trueExpression, piExpression), storm::exceptions::InvalidTypeException);
     ASSERT_NO_THROW(tempExpression = storm::expressions::maximum(threeExpression, threeExpression));
-    EXPECT_TRUE(tempExpression.hasIntegralType());
+    EXPECT_TRUE(tempExpression.hasIntegerType());
     ASSERT_NO_THROW(tempExpression = storm::expressions::maximum(intVarExpression, rationalVarExpression));
     EXPECT_TRUE(tempExpression.hasRationalType());
     
@@ -236,19 +236,19 @@ TEST(Expression, OperatorTest) {
     
     ASSERT_THROW(tempExpression = storm::expressions::floor(trueExpression), storm::exceptions::InvalidTypeException);
     ASSERT_NO_THROW(tempExpression = storm::expressions::floor(threeExpression));
-    EXPECT_TRUE(tempExpression.hasIntegralType());
+    EXPECT_TRUE(tempExpression.hasIntegerType());
     ASSERT_NO_THROW(tempExpression = storm::expressions::floor(rationalVarExpression));
-    EXPECT_TRUE(tempExpression.hasIntegralType());
+    EXPECT_TRUE(tempExpression.hasIntegerType());
 
     ASSERT_THROW(tempExpression = storm::expressions::ceil(trueExpression), storm::exceptions::InvalidTypeException);
     ASSERT_NO_THROW(tempExpression = storm::expressions::ceil(threeExpression));
-    EXPECT_TRUE(tempExpression.hasIntegralType());
+    EXPECT_TRUE(tempExpression.hasIntegerType());
     ASSERT_NO_THROW(tempExpression = storm::expressions::ceil(rationalVarExpression));
-    EXPECT_TRUE(tempExpression.hasIntegralType());
+    EXPECT_TRUE(tempExpression.hasIntegerType());
 
     ASSERT_THROW(tempExpression = trueExpression ^ piExpression, storm::exceptions::InvalidTypeException);
     ASSERT_NO_THROW(tempExpression = threeExpression ^ threeExpression);
-    EXPECT_TRUE(tempExpression.hasIntegralType());
+    EXPECT_TRUE(tempExpression.hasIntegerType());
     ASSERT_NO_THROW(tempExpression = intVarExpression ^ rationalVarExpression);
     EXPECT_TRUE(tempExpression.hasRationalType());
 }