diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h index f6526ff11..ac0ae6455 100644 --- a/src/adapters/ExplicitModelAdapter.h +++ b/src/adapters/ExplicitModelAdapter.h @@ -101,7 +101,7 @@ namespace storm { static std::unique_ptr> 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 constantDefinitions = storm::utility::prism::parseConstantDefinitionString(program, constantDefinitionString); + std::map 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."); diff --git a/src/adapters/MathsatExpressionAdapter.h b/src/adapters/MathsatExpressionAdapter.h index d62ab8310..3795ca965 100644 --- a/src/adapters/MathsatExpressionAdapter.h +++ b/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)); diff --git a/src/adapters/Z3ExpressionAdapter.h b/src/adapters/Z3ExpressionAdapter.h index 556548e88..a0b671d38 100644 --- a/src/adapters/Z3ExpressionAdapter.h +++ b/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()); diff --git a/src/solver/Z3SmtSolver.cpp b/src/solver/Z3SmtSolver.cpp index 0ee80e469..b8dcdb75b 100644 --- a/src/solver/Z3SmtSolver.cpp +++ b/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()); diff --git a/src/storage/expressions/BaseExpression.cpp b/src/storage/expressions/BaseExpression.cpp index af5d5d96e..90033870d 100644 --- a/src/storage/expressions/BaseExpression.cpp +++ b/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 { diff --git a/src/storage/expressions/BaseExpression.h b/src/storage/expressions/BaseExpression.h index 15e88379e..5f9faf1f9 100644 --- a/src/storage/expressions/BaseExpression.h +++ b/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. * diff --git a/src/storage/expressions/BinaryNumericalFunctionExpression.cpp b/src/storage/expressions/BinaryNumericalFunctionExpression.cpp index d28a72168..f00e2d73e 100644 --- a/src/storage/expressions/BinaryNumericalFunctionExpression.cpp +++ b/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); diff --git a/src/storage/expressions/Expression.cpp b/src/storage/expressions/Expression.cpp index 4be75c347..839dd7c24 100644 --- a/src/storage/expressions/Expression.cpp +++ b/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 { diff --git a/src/storage/expressions/Expression.h b/src/storage/expressions/Expression.h index a52acdce7..22d0c2f87 100644 --- a/src/storage/expressions/Expression.h +++ b/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. diff --git a/src/storage/expressions/Type.cpp b/src/storage/expressions/Type.cpp index 9efa6cf65..e3357da72 100644 --- a/src/storage/expressions/Type.cpp +++ b/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(); } diff --git a/src/storage/expressions/Type.h b/src/storage/expressions/Type.h index 849f915f6..22ebc94ca 100644 --- a/src/storage/expressions/Type.h +++ b/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. diff --git a/src/storage/expressions/UnaryNumericalFunctionExpression.cpp b/src/storage/expressions/UnaryNumericalFunctionExpression.cpp index 86c743a4a..5f2474c93 100644 --- a/src/storage/expressions/UnaryNumericalFunctionExpression.cpp +++ b/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()) { diff --git a/src/storage/expressions/Variable.cpp b/src/storage/expressions/Variable.cpp index 8b998107d..1423aee11 100644 --- a/src/storage/expressions/Variable.cpp +++ b/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(); } } diff --git a/src/storage/expressions/Variable.h b/src/storage/expressions/Variable.h index a55a40c28..d1bb31b7e 100644 --- a/src/storage/expressions/Variable.h +++ b/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. diff --git a/src/storage/expressions/VariableExpression.cpp b/src/storage/expressions/VariableExpression.cpp index 350abb8b9..93c693515 100644 --- a/src/storage/expressions/VariableExpression.cpp +++ b/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(valuation->getIntegerValue(this->getVariable())); } else { return valuation->getRationalValue(this->getVariable()); diff --git a/src/utility/PrismUtility.h b/src/utility/PrismUtility.h index 5dda96313..e42a83107 100644 --- a/src/utility/PrismUtility.h +++ b/src/utility/PrismUtility.h @@ -189,9 +189,9 @@ namespace storm { labeledEntry.addValue(probability, labels); } - static std::map parseConstantDefinitionString(storm::prism::Program const& program, std::string const& constantDefinitionString) { - std::map constantDefinitions; - std::set definedConstants; + static std::map parseConstantDefinitionString(storm::prism::Program const& program, std::string const& constantDefinitionString) { + std::map constantDefinitions; + std::set 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 << "."; diff --git a/test/functional/storage/ExpressionTest.cpp b/test/functional/storage/ExpressionTest.cpp index 9e45105c0..358015988 100644 --- a/test/functional/storage/ExpressionTest.cpp +++ b/test/functional/storage/ExpressionTest.cpp @@ -50,7 +50,7 @@ TEST(Expression, AccessorTest) { EXPECT_TRUE(falseExpression.isFalse()); EXPECT_TRUE(falseExpression.getVariables() == std::set()); - 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({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()); }