diff --git a/src/adapters/MathsatExpressionAdapter.h b/src/adapters/MathsatExpressionAdapter.h index 16c449adb..b9f5c3d4d 100644 --- a/src/adapters/MathsatExpressionAdapter.h +++ b/src/adapters/MathsatExpressionAdapter.h @@ -17,10 +17,26 @@ #include "src/exceptions/InvalidArgumentException.h" #include "src/exceptions/NotImplementedException.h" +namespace std { + // Define hashing operator for MathSAT's declarations. + template <> + struct std::hash { + std::size_t operator()(msat_decl const& declaration) const { + return std::hash()(declaration.repr); + } + }; +} + +// Define equality operator to make hashing work. +bool operator==(msat_decl decl1, msat_decl decl2) { + return decl1.repr == decl2.repr; +} + namespace storm { namespace adapters { #ifdef STORM_HAVE_MSAT + class MathsatExpressionAdapter : public storm::expressions::ExpressionVisitor { public: /*! @@ -29,7 +45,7 @@ namespace storm { * @param manager The manager that can be used to build expressions. * @param env The MathSAT environment in which to build the expressions. */ - MathsatExpressionAdapter(storm::expressions::ExpressionManager& manager, msat_env& env) : manager(manager), env(env), variableToDeclarationMap() { + MathsatExpressionAdapter(storm::expressions::ExpressionManager& manager, msat_env& env) : manager(manager), env(env), variableToDeclarationMapping() { // Intentionally left empty. } @@ -52,7 +68,19 @@ namespace storm { * @return An equivalent term for MathSAT. */ msat_term translateExpression(storm::expressions::Variable const& variable) { - return msat_make_constant(env, variableToDeclarationMap[variable]); + return msat_make_constant(env, variableToDeclarationMapping[variable]); + } + + /*! + * Retrieves the variable that is associated with the given MathSAT variable declaration. + * + * @param msatVariableDeclaration The MathSAT variable declaration. + * @return The variable associated with the given declaration. + */ + storm::expressions::Variable const& getVariable(msat_decl msatVariableDeclaration) const { + auto const& declarationVariablePair = declarationToVariableMapping.find(msatVariableDeclaration); + STORM_LOG_ASSERT(declarationVariablePair != declarationToVariableMapping.end(), "Unknown variable declaration."); + return declarationVariablePair->second; } virtual boost::any visit(expressions::BinaryBooleanFunctionExpression const& expression) override { @@ -101,13 +129,13 @@ namespace storm { switch (expression.getRelationType()) { case storm::expressions::BinaryRelationExpression::RelationType::Equal: - if (expression.getFirstOperand()->getReturnType() == storm::expressions::ExpressionReturnType::Bool && expression.getSecondOperand()->getReturnType() == storm::expressions::ExpressionReturnType::Bool) { + if (expression.getFirstOperand()->getType().isBooleanType() && expression.getSecondOperand()->getType().isBooleanType()) { return msat_make_iff(env, leftResult, rightResult); } else { return msat_make_equal(env, leftResult, rightResult); } case storm::expressions::BinaryRelationExpression::RelationType::NotEqual: - if (expression.getFirstOperand()->getReturnType() == storm::expressions::ExpressionReturnType::Bool && expression.getSecondOperand()->getReturnType() == storm::expressions::ExpressionReturnType::Bool) { + if (expression.getFirstOperand()->getType().isBooleanType() && expression.getSecondOperand()->getType().isBooleanType()) { return msat_make_not(env, msat_make_iff(env, leftResult, rightResult)); } else { return msat_make_not(env, msat_make_equal(env, leftResult, rightResult)); @@ -176,7 +204,7 @@ namespace storm { } virtual boost::any visit(expressions::VariableExpression const& expression) override { - return msat_make_constant(env, variableToDeclarationMap[expression.getVariable()]); + return msat_make_constant(env, variableToDeclarationMapping[expression.getVariable()]); } storm::expressions::Expression translateExpression(msat_term const& term) { @@ -229,7 +257,10 @@ namespace storm { msat_env& env; // A mapping of variable names to their declaration in the MathSAT environment. - std::unordered_map variableToDeclarationMap; + std::unordered_map variableToDeclarationMapping; + + // A mapping from MathSAT variable declaration to our variables. + std::unordered_map declarationToVariableMapping; }; #endif } // namespace adapters diff --git a/src/adapters/Z3ExpressionAdapter.h b/src/adapters/Z3ExpressionAdapter.h index e97231c42..045261d05 100644 --- a/src/adapters/Z3ExpressionAdapter.h +++ b/src/adapters/Z3ExpressionAdapter.h @@ -30,15 +30,23 @@ namespace storm { * @param context A reference to the Z3 context over which to build the expressions. The lifetime of the * context needs to be guaranteed as long as the instance of this adapter is used. */ - Z3ExpressionAdapter(storm::expressions::ExpressionManager& manager, z3::context& context) : manager(manager), context(context), additionalAssertions(), variableToExpressionMap() { + Z3ExpressionAdapter(storm::expressions::ExpressionManager& manager, z3::context& context) : manager(manager), context(context), additionalAssertions(), variableToExpressionMapping() { // Here, we need to create the mapping from all variables known to the manager to their z3 counterparts. for (auto const& variableTypePair : manager) { - switch (variableTypePair.second) { - case storm::expressions::ExpressionReturnType::Bool: variableToExpressionMap.insert(std::make_pair(variableTypePair.first, context.bool_const(variableTypePair.first.getName().c_str()))); break; - case storm::expressions::ExpressionReturnType::Int: variableToExpressionMap.insert(std::make_pair(variableTypePair.first, context.int_const(variableTypePair.first.getName().c_str()))); break; - case storm::expressions::ExpressionReturnType::Double: variableToExpressionMap.insert(std::make_pair(variableTypePair.first, context.real_const(variableTypePair.first.getName().c_str()))); break; - default: STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Encountered variable '" << variableTypePair.first.getName() << "' with unknown type while trying to create solver variables."); + z3::expr z3Variable(context); + if (variableTypePair.second.isBooleanType()) { + z3Variable = context.bool_const(variableTypePair.first.getName().c_str()); + } else if (variableTypePair.second.isUnboundedIntegralType()) { + z3Variable = context.int_const(variableTypePair.first.getName().c_str()); + } else if (variableTypePair.second.isBoundedIntegralType()) { + z3Variable = context.bv_const(variableTypePair.first.getName().c_str(), variableTypePair.second.getWidth()); + } else if (variableTypePair.second.isRationalType()) { + z3Variable = context.real_const(variableTypePair.first.getName().c_str()); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Encountered variable '" << variableTypePair.first.getName() << "' with unknown type while trying to create solver variables."); } + variableToExpressionMapping.insert(std::make_pair(variableTypePair.first, z3Variable)); + declarationToVariableMapping.insert(std::make_pair(z3Variable.decl(), variableTypePair.first)); } } @@ -66,11 +74,23 @@ namespace storm { * @return An equivalent expression for Z3. */ z3::expr translateExpression(storm::expressions::Variable const& variable) { - auto const& variableExpressionPair = variableToExpressionMap.find(variable); - STORM_LOG_ASSERT(variableExpressionPair != variableToExpressionMap.end(), "Unable to find variable."); + auto const& variableExpressionPair = variableToExpressionMapping.find(variable); + STORM_LOG_ASSERT(variableExpressionPair != variableToExpressionMapping.end(), "Unable to find variable."); return variableExpressionPair->second; } + /*! + * Finds the counterpart to the given z3 variable declaration. + * + * @param z3Declaration The declaration for which to find the equivalent. + * @return The equivalent counterpart. + */ + storm::expressions::Variable const& getVariable(z3::func_decl z3Declaration) { + auto const& declarationVariablePair = declarationToVariableMapping.find(z3Declaration); + STORM_LOG_ASSERT(declarationVariablePair != declarationToVariableMapping.end(), "Unable to find declaration."); + return declarationVariablePair->second; + } + storm::expressions::Expression translateExpression(z3::expr const& expr) { if (expr.is_app()) { switch (expr.decl().decl_kind()) { @@ -264,13 +284,13 @@ namespace storm { case storm::expressions::UnaryNumericalFunctionExpression::OperatorType::Minus: return 0 - childResult; case storm::expressions::UnaryNumericalFunctionExpression::OperatorType::Floor: { - storm::expressions::Variable freshAuxiliaryVariable = manager.declareFreshAuxiliaryVariable(storm::expressions::ExpressionReturnType::Int); + storm::expressions::Variable freshAuxiliaryVariable = manager.declareFreshAuxiliaryVariable(manager.getIntegerType()); z3::expr floorVariable = context.int_const(freshAuxiliaryVariable.getName().c_str()); additionalAssertions.push_back(z3::expr(context, Z3_mk_int2real(context, floorVariable)) <= childResult && childResult < (z3::expr(context, Z3_mk_int2real(context, floorVariable)) + 1)); return floorVariable; } case storm::expressions::UnaryNumericalFunctionExpression::OperatorType::Ceil:{ - storm::expressions::Variable freshAuxiliaryVariable = manager.declareFreshAuxiliaryVariable(storm::expressions::ExpressionReturnType::Int); + storm::expressions::Variable freshAuxiliaryVariable = manager.declareFreshAuxiliaryVariable(manager.getIntegerType()); z3::expr ceilVariable = context.int_const(freshAuxiliaryVariable.getName().c_str()); additionalAssertions.push_back(z3::expr(context, Z3_mk_int2real(context, ceilVariable)) - 1 <= childResult && childResult < z3::expr(context, Z3_mk_int2real(context, ceilVariable))); return ceilVariable; @@ -287,7 +307,7 @@ namespace storm { } virtual boost::any visit(storm::expressions::VariableExpression const& expression) override { - return variableToExpressionMap.at(expression.getVariable()); + return variableToExpressionMapping.at(expression.getVariable()); } private: @@ -301,8 +321,11 @@ namespace storm { // assertion that was added. std::vector additionalAssertions; - // A mapping from variable names to their Z3 equivalent. - std::unordered_map variableToExpressionMap; + // A mapping from variables to their Z3 equivalent. + std::unordered_map variableToExpressionMapping; + + // A mapping from z3 declarations to the corresponding variables. + std::unordered_map declarationToVariableMapping; }; #endif } // namespace adapters diff --git a/src/solver/MathsatSmtSolver.cpp b/src/solver/MathsatSmtSolver.cpp index b2793fb33..edd1e3da0 100644 --- a/src/solver/MathsatSmtSolver.cpp +++ b/src/solver/MathsatSmtSolver.cpp @@ -8,13 +8,13 @@ namespace storm { namespace solver { #ifdef STORM_HAVE_MSAT - MathsatSmtSolver::MathsatAllsatModelReference::MathsatAllsatModelReference(storm::expressions::ExpressionManager const& manager, msat_env const& env, msat_term* model, std::unordered_map const& variableNameToSlotMapping) : ModelReference(manager), env(env), model(model), variableNameToSlotMapping(variableNameToSlotMapping) { + MathsatSmtSolver::MathsatAllsatModelReference::MathsatAllsatModelReference(storm::expressions::ExpressionManager const& manager, msat_env const& env, msat_term* model, std::unordered_map const& variableToSlotMapping) : ModelReference(manager), env(env), model(model), variableToSlotMapping(variableToSlotMapping) { // Intentionally left empty. } bool MathsatSmtSolver::MathsatAllsatModelReference::getBooleanValue(storm::expressions::Variable const& variable) const { - std::unordered_map::const_iterator variableSlotPair = variableNameToSlotMapping.find(variable); - STORM_LOG_THROW(variableSlotPair != variableNameToSlotMapping.end(), storm::exceptions::InvalidArgumentException, "Cannot retrieve value of unknown variable '" << variable.getName() << "' from model."); + std::unordered_map::const_iterator variableSlotPair = variableToSlotMapping.find(variable); + STORM_LOG_THROW(variableSlotPair != variableToSlotMapping.end(), storm::exceptions::InvalidArgumentException, "Cannot retrieve value of unknown variable '" << variable.getName() << "' from model."); msat_term selectedTerm = model[variableSlotPair->second]; if (msat_term_is_not(env, selectedTerm)) { @@ -56,7 +56,7 @@ namespace storm { double MathsatSmtSolver::MathsatModelReference::getRationalValue(storm::expressions::Variable const& variable) const { STORM_LOG_ASSERT(variable.hasBooleanType(), "Variable is non-boolean type."); - msat_term msatVariable = expressionAdapter.translateExpression(storm::expressions::Expression::createBooleanVariable(name)); + msat_term msatVariable = expressionAdapter.translateExpression(variable); msat_term msatValue = msat_get_model_value(env, msatVariable); STORM_LOG_ASSERT(!MSAT_ERROR_TERM(msatValue), "Unable to retrieve value of variable in model. This could be caused by calls to the solver between checking for satisfiability and model retrieval."); storm::expressions::Expression value = expressionAdapter.translateExpression(msatValue); @@ -64,7 +64,7 @@ namespace storm { } #endif - MathsatSmtSolver::MathsatSmtSolver(storm::expressions::ExpressionManager const& manager, Options const& options) + MathsatSmtSolver::MathsatSmtSolver(storm::expressions::ExpressionManager& manager, Options const& options) #ifdef STORM_HAVE_MSAT : SmtSolver(manager), expressionAdapter(nullptr), lastCheckAssumptions(false), lastResult(CheckResult::Unknown) #endif @@ -87,7 +87,7 @@ namespace storm { STORM_LOG_THROW(!MSAT_ERROR_ENV(env), storm::exceptions::UnexpectedException, "Unable to create Mathsat environment."); msat_destroy_config(config); - expressionAdapter = std::unique_ptr(new storm::adapters::MathsatExpressionAdapter(env)); + expressionAdapter = std::unique_ptr(new storm::adapters::MathsatExpressionAdapter(manager, env)); #endif } @@ -232,7 +232,7 @@ namespace storm { std::shared_ptr MathsatSmtSolver::getModel() { #ifdef STORM_HAVE_MSAT STORM_LOG_THROW(this->lastResult == SmtSolver::CheckResult::Sat, storm::exceptions::InvalidStateException, "Unable to create model for formula that was not determined to be satisfiable."); - return std::shared_ptr(new MathsatModelReference(env, *expressionAdapter)); + return std::shared_ptr(new MathsatModelReference(this->getManager(), env, *expressionAdapter)); #else STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support."); #endif @@ -240,7 +240,7 @@ namespace storm { #ifdef STORM_HAVE_MSAT storm::expressions::Valuation MathsatSmtSolver::convertMathsatModelToValuation() { - storm::expressions::Valuation stormModel; + storm::expressions::Valuation stormModel(this->getManager()); msat_model_iterator modelIterator = msat_create_model_iterator(env); STORM_LOG_THROW(!MSAT_ERROR_MODEL_ITERATOR(modelIterator), storm::exceptions::UnexpectedException, "MathSat returned an illegal model iterator."); @@ -250,32 +250,24 @@ namespace storm { msat_model_iterator_next(modelIterator, &t, &v); storm::expressions::Expression variableInterpretation = this->expressionAdapter->translateExpression(v); - char* name = msat_decl_get_name(msat_term_get_decl(t)); - - switch (variableInterpretation.getReturnType()) { - case storm::expressions::ExpressionReturnType::Bool: - stormModel.addBooleanIdentifier(std::string(name), variableInterpretation.evaluateAsBool()); - break; - case storm::expressions::ExpressionReturnType::Int: - stormModel.addIntegerIdentifier(std::string(name), variableInterpretation.evaluateAsInt()); - break; - case storm::expressions::ExpressionReturnType::Double: - stormModel.addDoubleIdentifier(std::string(name), variableInterpretation.evaluateAsDouble()); - break; - default: - STORM_LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Variable interpretation in model is not of type bool, int or double.") - break; - } - - msat_free(name); - + storm::expressions::Variable stormVariable = this->expressionAdapter->getVariable(msat_term_get_decl(t)); + + if (stormVariable.hasBooleanType()) { + stormModel.setBooleanValue(stormVariable, variableInterpretation.isTrue()); + } else if (stormVariable.hasIntegralType()) { + stormModel.setIntegerValue(stormVariable, variableInterpretation.evaluateAsInt()); + } else if (stormVariable.hasRationalType()) { + stormModel.setRationalValue(stormVariable, variableInterpretation.evaluateAsDouble()); + } else { + STORM_LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Variable interpretation in model is not of type bool, int or rational."); + } } return stormModel; } #endif - std::vector MathsatSmtSolver::allSat(std::vector const& important) + std::vector MathsatSmtSolver::allSat(std::vector const& important) { #ifdef STORM_HAVE_MSAT std::vector valuations; @@ -290,14 +282,14 @@ namespace storm { #ifdef STORM_HAVE_MSAT class AllsatValuationCallbackUserData { public: - AllsatValuationCallbackUserData(msat_env& env, std::function const& callback) : env(env), callback(callback) { + AllsatValuationCallbackUserData(storm::expressions::ExpressionManager const& manager, storm::adapters::MathsatExpressionAdapter& adapter, msat_env& env, std::function const& callback) : manager(manager), adapter(adapter), env(env), callback(callback) { // Intentionally left empty. } static int allsatValuationsCallback(msat_term* model, int size, void* user_data) { AllsatValuationCallbackUserData* user = reinterpret_cast(user_data); - storm::expressions::Valuation valuation; + storm::expressions::Valuation valuation(user->manager); for (int i = 0; i < size; ++i) { bool currentTermValue = true; msat_term currentTerm = model[i]; @@ -305,10 +297,8 @@ namespace storm { currentTerm = msat_term_get_arg(currentTerm, 0); currentTermValue = false; } - char* name = msat_decl_get_name(msat_term_get_decl(currentTerm)); - std::string nameAsString(name); - msat_free(name); - valuation.addBooleanIdentifier(nameAsString, currentTermValue); + storm::expressions::Variable stormVariable = user->adapter.getVariable(msat_term_get_decl(currentTerm)); + valuation.setBooleanValue(stormVariable, currentTermValue); } if (user->callback(valuation)) { @@ -319,6 +309,12 @@ namespace storm { } protected: + // The manager responsible for the expression.s + storm::expressions::ExpressionManager const& manager; + + // The adapter to use for expression translation. + storm::adapters::MathsatExpressionAdapter& adapter; + // The MathSAT environment. It is used to retrieve the values of the atoms in a model. msat_env& env; @@ -328,13 +324,13 @@ namespace storm { class AllsatModelReferenceCallbackUserData { public: - AllsatModelReferenceCallbackUserData(msat_env& env, std::unordered_map const& atomNameToSlotMapping, std::function const& callback) : env(env), atomNameToSlotMapping(atomNameToSlotMapping), callback(callback) { + AllsatModelReferenceCallbackUserData(storm::expressions::ExpressionManager const& manager, msat_env& env, std::unordered_map const& atomToSlotMapping, std::function const& callback) : manager(manager), env(env), atomToSlotMapping(atomToSlotMapping), callback(callback) { // Intentionally left empty. } static int allsatModelReferenceCallback(msat_term* model, int size, void* user_data) { AllsatModelReferenceCallbackUserData* user = reinterpret_cast(user_data); - MathsatSmtSolver::MathsatAllsatModelReference modelReference(user->env, model, user->atomNameToSlotMapping); + MathsatSmtSolver::MathsatAllsatModelReference modelReference(user->manager, user->env, model, user->atomToSlotMapping); if (user->callback(modelReference)) { return 1; } else { @@ -343,11 +339,14 @@ namespace storm { } protected: + // The manager responsible for the expression.s + storm::expressions::ExpressionManager const& manager; + // The MathSAT environment. It is used to retrieve the values of the atoms in a model. msat_env& env; - // Store a mapping from the names of atoms to their slots in the model. - std::unordered_map const& atomNameToSlotMapping; + // Store a mapping from atoms to their slots in the model. + std::unordered_map const& atomToSlotMapping; // The function that is to be called when the MathSAT model has been translated to a valuation. std::function const& callback; @@ -355,7 +354,7 @@ namespace storm { #endif - uint_fast64_t MathsatSmtSolver::allSat(std::vector const& important, std::function const& callback) { + uint_fast64_t MathsatSmtSolver::allSat(std::vector const& important, std::function const& callback) { #ifdef STORM_HAVE_MSAT // Create a backtracking point, because MathSAT will modify the assertions stack during its AllSat procedure. this->push(); @@ -363,12 +362,12 @@ namespace storm { std::vector msatImportant; msatImportant.reserve(important.size()); - for (storm::expressions::Expression const& atom : important) { - STORM_LOG_THROW(atom.isVariable() && atom.hasBooleanReturnType(), storm::exceptions::InvalidArgumentException, "The important atoms for AllSat must be boolean variables."); - msatImportant.push_back(expressionAdapter->translateExpression(atom)); + for (storm::expressions::Variable const& variable : important) { + STORM_LOG_THROW(variable.hasBooleanType(), storm::exceptions::InvalidArgumentException, "The important atoms for AllSat must be boolean variables."); + msatImportant.push_back(expressionAdapter->translateExpression(variable)); } - AllsatValuationCallbackUserData allSatUserData(env, callback); + AllsatValuationCallbackUserData allSatUserData(this->getManager(), *expressionAdapter, env, callback); int numberOfModels = msat_all_sat(env, msatImportant.data(), msatImportant.size(), &AllsatValuationCallbackUserData::allsatValuationsCallback, &allSatUserData); // Restore original assertion stack and return. @@ -379,22 +378,22 @@ namespace storm { #endif } - uint_fast64_t MathsatSmtSolver::allSat(std::vector const& important, std::function const& callback) { + uint_fast64_t MathsatSmtSolver::allSat(std::vector const& important, std::function const& callback) { #ifdef STORM_HAVE_MSAT // Create a backtracking point, because MathSAT will modify the assertions stack during its AllSat procedure. this->push(); std::vector msatImportant; msatImportant.reserve(important.size()); - std::unordered_map atomNameToSlotMapping; + std::unordered_map atomToSlotMapping; - for (storm::expressions::Expression const& atom : important) { - STORM_LOG_THROW(atom.isVariable() && atom.hasBooleanReturnType(), storm::exceptions::InvalidArgumentException, "The important atoms for AllSat must be boolean variables."); - msatImportant.push_back(expressionAdapter->translateExpression(atom)); - atomNameToSlotMapping[atom.getIdentifier()] = msatImportant.size() - 1; + for (storm::expressions::Variable const& variable : important) { + STORM_LOG_THROW(variable.hasBooleanType(), storm::exceptions::InvalidArgumentException, "The important atoms for AllSat must be boolean variables."); + msatImportant.push_back(expressionAdapter->translateExpression(variable)); + atomToSlotMapping[variable] = msatImportant.size() - 1; } - AllsatModelReferenceCallbackUserData allSatUserData(env, atomNameToSlotMapping, callback); + AllsatModelReferenceCallbackUserData allSatUserData(this->getManager(), env, atomToSlotMapping, callback); int numberOfModels = msat_all_sat(env, msatImportant.data(), msatImportant.size(), &AllsatModelReferenceCallbackUserData::allsatModelReferenceCallback, &allSatUserData); // Restore original assertion stack and return. diff --git a/src/solver/MathsatSmtSolver.h b/src/solver/MathsatSmtSolver.h index 38d958dbb..f3dd1f84b 100644 --- a/src/solver/MathsatSmtSolver.h +++ b/src/solver/MathsatSmtSolver.h @@ -42,7 +42,7 @@ namespace storm { private: msat_env const& env; msat_term* model; - std::unordered_map const& variableNameToSlotMapping; + std::unordered_map const& variableToSlotMapping; }; #endif @@ -61,7 +61,7 @@ namespace storm { }; #endif - MathsatSmtSolver(storm::expressions::ExpressionManager const& manager, Options const& options = Options()); + MathsatSmtSolver(storm::expressions::ExpressionManager& manager, Options const& options = Options()); virtual ~MathsatSmtSolver(); diff --git a/src/solver/Z3SmtSolver.cpp b/src/solver/Z3SmtSolver.cpp index 6d8e7e1f4..24cea0c53 100644 --- a/src/solver/Z3SmtSolver.cpp +++ b/src/solver/Z3SmtSolver.cpp @@ -205,23 +205,18 @@ namespace storm { for (unsigned i = 0; i < model.num_consts(); ++i) { z3::func_decl variableI = model.get_const_decl(i); + storm::expressions::Variable stormVariable = this->expressionAdapter->getVariable(variableI); storm::expressions::Expression variableInterpretation = this->expressionAdapter->translateExpression(model.get_const_interp(variableI)); - switch (variableInterpretation.getReturnType()) { - case storm::expressions::ExpressionReturnType::Bool: - stormModel.setBooleanValue(this->getManager().getVariable(variableI.name().str()), variableInterpretation.isTrue()); - break; - case storm::expressions::ExpressionReturnType::Int: - stormModel.setIntegerValue(this->getManager().getVariable(variableI.name().str()), variableInterpretation.evaluateAsInt()); - break; - case storm::expressions::ExpressionReturnType::Double: - stormModel.setRationalValue(this->getManager().getVariable(variableI.name().str()), variableInterpretation.evaluateAsDouble()); - break; - default: - STORM_LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Variable interpretation in model is not of type bool, int or double.") - break; - } - + if (variableInterpretation.getType().isBooleanType()) { + stormModel.setBooleanValue(this->getManager().getVariable(variableI.name().str()), variableInterpretation.isTrue()); + } else if (variableInterpretation.getType().isIntegralType()) { + 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()); + } else { + STORM_LOG_ASSERT(false, "Variable interpretation in model is not of type bool, int or rational."); + } } return stormModel; diff --git a/src/storage/expressions/BaseExpression.cpp b/src/storage/expressions/BaseExpression.cpp index 59950fc9a..b8bb495e5 100644 --- a/src/storage/expressions/BaseExpression.cpp +++ b/src/storage/expressions/BaseExpression.cpp @@ -5,23 +5,23 @@ namespace storm { namespace expressions { - BaseExpression::BaseExpression(ExpressionManager const& manager, ExpressionReturnType returnType) : manager(manager), returnType(returnType) { + BaseExpression::BaseExpression(ExpressionManager const& manager, Type const& type) : manager(manager), type(type) { // Intentionally left empty. } - ExpressionReturnType BaseExpression::getReturnType() const { - return this->returnType; + Type const& BaseExpression::getType() const { + return this->type; } - bool BaseExpression::hasIntegralReturnType() const { - return this->getReturnType() == ExpressionReturnType::Int; + bool BaseExpression::hasIntegralType() const { + return this->getType() == manager.getIntegerType(); } - bool BaseExpression::hasNumericalReturnType() const { + bool BaseExpression::hasNumericalType() const { return this->getReturnType() == ExpressionReturnType::Double || this->getReturnType() == ExpressionReturnType::Int; } - bool BaseExpression::hasBooleanReturnType() const { + bool BaseExpression::hasBooleanType() const { return this->getReturnType() == ExpressionReturnType::Bool; } diff --git a/src/storage/expressions/BaseExpression.h b/src/storage/expressions/BaseExpression.h index dd589c345..301cd861f 100644 --- a/src/storage/expressions/BaseExpression.h +++ b/src/storage/expressions/BaseExpression.h @@ -7,7 +7,7 @@ #include #include -#include "src/storage/expressions/ExpressionReturnType.h" +#include "src/storage/expressions/Type.h" #include "src/storage/expressions/Valuation.h" #include "src/storage/expressions/ExpressionVisitor.h" #include "src/storage/expressions/OperatorType.h" @@ -27,9 +27,9 @@ namespace storm { /*! * Constructs a base expression with the given return type. * - * @param returnType The return type of the expression. + * @param type The type of the expression. */ - BaseExpression(ExpressionManager const& manager, ExpressionReturnType returnType); + BaseExpression(ExpressionManager const& manager, Type const& type); // Create default versions of constructors and assignments. BaseExpression(BaseExpression const&) = default; @@ -167,25 +167,25 @@ namespace storm { virtual boost::any accept(ExpressionVisitor& visitor) const = 0; /*! - * Retrieves whether the expression has a numerical return type, i.e., integer or double. + * Retrieves whether the expression has a numerical type, i.e., integer or double. * - * @return True iff the expression has a numerical return type. + * @return True iff the expression has a numerical type. */ - bool hasNumericalReturnType() const; + bool hasNumericalType() const; /*! - * Retrieves whether the expression has an integral return type, i.e., integer. + * Retrieves whether the expression has an integral type, i.e., integer. * - * @return True iff the expression has an integral return type. + * @return True iff the expression has an integral type. */ - bool hasIntegralReturnType() const; + bool hasIntegralType() const; /*! - * Retrieves whether the expression has a boolean return type. + * Retrieves whether the expression has a boolean type. * - * @return True iff the expression has a boolean return type. + * @return True iff the expression has a boolean type. */ - bool hasBooleanReturnType() const; + bool hasBooleanType() const; /*! * Retrieves a shared pointer to this expression. @@ -202,11 +202,11 @@ namespace storm { ExpressionManager const& getManager() const; /*! - * Retrieves the return type of the expression. + * Retrieves the type of the expression. * - * @return The return type of the expression. + * @return The type of the expression. */ - ExpressionReturnType getReturnType() const; + Type const& getType() const; friend std::ostream& operator<<(std::ostream& stream, BaseExpression const& expression); @@ -223,7 +223,7 @@ namespace storm { ExpressionManager const& manager; // The return type of this expression. - ExpressionReturnType returnType; + Type const& type; }; } } diff --git a/src/storage/expressions/BinaryBooleanFunctionExpression.cpp b/src/storage/expressions/BinaryBooleanFunctionExpression.cpp index 7be4bf766..f9f495a16 100644 --- a/src/storage/expressions/BinaryBooleanFunctionExpression.cpp +++ b/src/storage/expressions/BinaryBooleanFunctionExpression.cpp @@ -5,7 +5,7 @@ namespace storm { namespace expressions { - BinaryBooleanFunctionExpression::BinaryBooleanFunctionExpression(ExpressionManager const& manager, ExpressionReturnType returnType, std::shared_ptr const& firstOperand, std::shared_ptr const& secondOperand, OperatorType operatorType) : BinaryExpression(manager, returnType, firstOperand, secondOperand), operatorType(operatorType) { + BinaryBooleanFunctionExpression::BinaryBooleanFunctionExpression(ExpressionManager const& manager, Type const& type, std::shared_ptr const& firstOperand, std::shared_ptr const& secondOperand, OperatorType operatorType) : BinaryExpression(manager, type, firstOperand, secondOperand), operatorType(operatorType) { // Intentionally left empty. } @@ -24,7 +24,7 @@ namespace storm { } bool BinaryBooleanFunctionExpression::evaluateAsBool(Valuation const* valuation) const { - STORM_LOG_THROW(this->hasBooleanReturnType(), storm::exceptions::InvalidTypeException, "Unable to evaluate expression as boolean."); + STORM_LOG_THROW(this->hasBooleanType(), storm::exceptions::InvalidTypeException, "Unable to evaluate expression as boolean."); bool firstOperandEvaluation = this->getFirstOperand()->evaluateAsBool(valuation); bool secondOperandEvaluation = this->getSecondOperand()->evaluateAsBool(valuation); @@ -70,15 +70,15 @@ namespace storm { case OperatorType::Implies: if (firstOperandSimplified->isTrue()) { return secondOperandSimplified; } else if (firstOperandSimplified->isFalse()) { - return std::shared_ptr(new BooleanLiteralExpression(true)); + return std::shared_ptr(new BooleanLiteralExpression(this->getManager(), true)); } else if (secondOperandSimplified->isTrue()) { - return std::shared_ptr(new BooleanLiteralExpression(true)); + return std::shared_ptr(new BooleanLiteralExpression(this->getManager(), true)); } break; case OperatorType::Iff: if (firstOperandSimplified->isTrue() && secondOperandSimplified->isTrue()) { - return std::shared_ptr(new BooleanLiteralExpression(true)); + return std::shared_ptr(new BooleanLiteralExpression(this->getManager(), true)); } else if (firstOperandSimplified->isFalse() && secondOperandSimplified->isFalse()) { - return std::shared_ptr(new BooleanLiteralExpression(true)); + return std::shared_ptr(new BooleanLiteralExpression(this->getManager(), true)); } break; } @@ -87,7 +87,7 @@ namespace storm { if (firstOperandSimplified.get() == this->getFirstOperand().get() && secondOperandSimplified.get() == this->getSecondOperand().get()) { return this->shared_from_this(); } else { - return std::shared_ptr(new BinaryBooleanFunctionExpression(this->getReturnType(), firstOperandSimplified, secondOperandSimplified, this->getOperatorType())); + return std::shared_ptr(new BinaryBooleanFunctionExpression(this->getManager(), this->getType(), firstOperandSimplified, secondOperandSimplified, this->getOperatorType())); } } diff --git a/src/storage/expressions/BinaryBooleanFunctionExpression.h b/src/storage/expressions/BinaryBooleanFunctionExpression.h index 9c20d6159..6eaefcbb6 100644 --- a/src/storage/expressions/BinaryBooleanFunctionExpression.h +++ b/src/storage/expressions/BinaryBooleanFunctionExpression.h @@ -17,12 +17,12 @@ namespace storm { * Creates a binary boolean function expression with the given return type, operands and operator. * * @param manager The manager responsible for this expression. - * @param returnType The return type of the expression. + * @param type The return type of the expression. * @param firstOperand The first operand of the expression. * @param secondOperand The second operand of the expression. * @param functionType The operator of the expression. */ - BinaryBooleanFunctionExpression(ExpressionManager const& manager, ExpressionReturnType returnType, std::shared_ptr const& firstOperand, std::shared_ptr const& secondOperand, OperatorType operatorType); + BinaryBooleanFunctionExpression(ExpressionManager const& manager, Type const& type, std::shared_ptr const& firstOperand, std::shared_ptr const& secondOperand, OperatorType operatorType); // Instantiate constructors and assignments with their default implementations. BinaryBooleanFunctionExpression(BinaryBooleanFunctionExpression const& other) = default; diff --git a/src/storage/expressions/BinaryExpression.cpp b/src/storage/expressions/BinaryExpression.cpp index 7df83d390..c03e7b718 100644 --- a/src/storage/expressions/BinaryExpression.cpp +++ b/src/storage/expressions/BinaryExpression.cpp @@ -5,7 +5,7 @@ namespace storm { namespace expressions { - BinaryExpression::BinaryExpression(ExpressionManager const& manager, ExpressionReturnType returnType, std::shared_ptr const& firstOperand, std::shared_ptr const& secondOperand) : BaseExpression(manager, returnType), firstOperand(firstOperand), secondOperand(secondOperand) { + BinaryExpression::BinaryExpression(ExpressionManager const& manager, Type const& type, std::shared_ptr const& firstOperand, std::shared_ptr const& secondOperand) : BaseExpression(manager, type), firstOperand(firstOperand), secondOperand(secondOperand) { // Intentionally left empty. } diff --git a/src/storage/expressions/BinaryExpression.h b/src/storage/expressions/BinaryExpression.h index 0c29d7614..69a61ab99 100644 --- a/src/storage/expressions/BinaryExpression.h +++ b/src/storage/expressions/BinaryExpression.h @@ -15,11 +15,11 @@ namespace storm { * Constructs a binary expression with the given return type and operands. * * @param manager The manager responsible for this expression. - * @param returnType The return type of the expression. + * @param type The return type of the expression. * @param firstOperand The first operand of the expression. * @param secondOperand The second operand of the expression. */ - BinaryExpression(ExpressionManager const& manager, ExpressionReturnType returnType, std::shared_ptr const& firstOperand, std::shared_ptr const& secondOperand); + BinaryExpression(ExpressionManager const& manager, Type const& type, std::shared_ptr const& firstOperand, std::shared_ptr const& secondOperand); // Instantiate constructors and assignments with their default implementations. BinaryExpression(BinaryExpression const& other) = default; diff --git a/src/storage/expressions/BinaryNumericalFunctionExpression.cpp b/src/storage/expressions/BinaryNumericalFunctionExpression.cpp index 4df59c0a5..d28a72168 100644 --- a/src/storage/expressions/BinaryNumericalFunctionExpression.cpp +++ b/src/storage/expressions/BinaryNumericalFunctionExpression.cpp @@ -7,7 +7,7 @@ namespace storm { namespace expressions { - BinaryNumericalFunctionExpression::BinaryNumericalFunctionExpression(ExpressionManager const& manager, ExpressionReturnType returnType, std::shared_ptr const& firstOperand, std::shared_ptr const& secondOperand, OperatorType operatorType) : BinaryExpression(manager, returnType, firstOperand, secondOperand), operatorType(operatorType) { + BinaryNumericalFunctionExpression::BinaryNumericalFunctionExpression(ExpressionManager const& manager, Type const& type, std::shared_ptr const& firstOperand, std::shared_ptr const& secondOperand, OperatorType operatorType) : BinaryExpression(manager, type, firstOperand, secondOperand), operatorType(operatorType) { // Intentionally left empty. } @@ -28,7 +28,7 @@ namespace storm { } int_fast64_t BinaryNumericalFunctionExpression::evaluateAsInt(Valuation const* valuation) const { - STORM_LOG_THROW(this->hasIntegralReturnType(), storm::exceptions::InvalidTypeException, "Unable to evaluate expression as integer."); + STORM_LOG_THROW(this->hasIntegralType(), 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); @@ -44,7 +44,7 @@ namespace storm { } double BinaryNumericalFunctionExpression::evaluateAsDouble(Valuation const* valuation) const { - STORM_LOG_THROW(this->hasNumericalReturnType(), storm::exceptions::InvalidTypeException, "Unable to evaluate expression as double."); + STORM_LOG_THROW(this->hasNumericalType(), storm::exceptions::InvalidTypeException, "Unable to evaluate expression as double."); double firstOperandEvaluation = this->getFirstOperand()->evaluateAsDouble(valuation); double secondOperandEvaluation = this->getSecondOperand()->evaluateAsDouble(valuation); @@ -66,7 +66,7 @@ namespace storm { if (firstOperandSimplified.get() == this->getFirstOperand().get() && secondOperandSimplified.get() == this->getSecondOperand().get()) { return this->shared_from_this(); } else { - return std::shared_ptr(new BinaryNumericalFunctionExpression(this->getReturnType(), firstOperandSimplified, secondOperandSimplified, this->getOperatorType())); + return std::shared_ptr(new BinaryNumericalFunctionExpression(this->getManager(), this->getType(), firstOperandSimplified, secondOperandSimplified, this->getOperatorType())); } } diff --git a/src/storage/expressions/BinaryNumericalFunctionExpression.h b/src/storage/expressions/BinaryNumericalFunctionExpression.h index 28c03787c..bf69016d0 100644 --- a/src/storage/expressions/BinaryNumericalFunctionExpression.h +++ b/src/storage/expressions/BinaryNumericalFunctionExpression.h @@ -17,12 +17,12 @@ namespace storm { * Constructs a binary numerical function expression with the given return type, operands and operator. * * @param manager The manager responsible for this expression. - * @param returnType The return type of the expression. + * @param type The return type of the expression. * @param firstOperand The first operand of the expression. * @param secondOperand The second operand of the expression. * @param functionType The operator of the expression. */ - BinaryNumericalFunctionExpression(ExpressionManager const& manager, ExpressionReturnType returnType, std::shared_ptr const& firstOperand, std::shared_ptr const& secondOperand, OperatorType operatorType); + BinaryNumericalFunctionExpression(ExpressionManager const& manager, Type const& type, std::shared_ptr const& firstOperand, std::shared_ptr const& secondOperand, OperatorType operatorType); // Instantiate constructors and assignments with their default implementations. BinaryNumericalFunctionExpression(BinaryNumericalFunctionExpression const& other) = default; diff --git a/src/storage/expressions/BinaryRelationExpression.cpp b/src/storage/expressions/BinaryRelationExpression.cpp index 3524ab08b..98efc4ad0 100644 --- a/src/storage/expressions/BinaryRelationExpression.cpp +++ b/src/storage/expressions/BinaryRelationExpression.cpp @@ -5,7 +5,7 @@ namespace storm { namespace expressions { - BinaryRelationExpression::BinaryRelationExpression(ExpressionManager const& manager, ExpressionReturnType returnType, std::shared_ptr const& firstOperand, std::shared_ptr const& secondOperand, RelationType relationType) : BinaryExpression(manager, returnType, firstOperand, secondOperand), relationType(relationType) { + BinaryRelationExpression::BinaryRelationExpression(ExpressionManager const& manager, Type const& type, std::shared_ptr const& firstOperand, std::shared_ptr const& secondOperand, RelationType relationType) : BinaryExpression(manager, type, firstOperand, secondOperand), relationType(relationType) { // Intentionally left empty. } @@ -21,7 +21,7 @@ namespace storm { } bool BinaryRelationExpression::evaluateAsBool(Valuation const* valuation) const { - STORM_LOG_THROW(this->hasBooleanReturnType(), storm::exceptions::InvalidTypeException, "Unable to evaluate expression as boolean."); + STORM_LOG_THROW(this->hasBooleanType(), storm::exceptions::InvalidTypeException, "Unable to evaluate expression as boolean."); double firstOperandEvaluated = this->getFirstOperand()->evaluateAsDouble(valuation); double secondOperandEvaluated = this->getSecondOperand()->evaluateAsDouble(valuation); @@ -42,7 +42,7 @@ namespace storm { if (firstOperandSimplified.get() == this->getFirstOperand().get() && secondOperandSimplified.get() == this->getSecondOperand().get()) { return this->shared_from_this(); } else { - return std::shared_ptr(new BinaryRelationExpression(this->getReturnType(), firstOperandSimplified, secondOperandSimplified, this->getRelationType())); + return std::shared_ptr(new BinaryRelationExpression(this->getManager(), this->getType(), firstOperandSimplified, secondOperandSimplified, this->getRelationType())); } } diff --git a/src/storage/expressions/BinaryRelationExpression.h b/src/storage/expressions/BinaryRelationExpression.h index 16c11a9e6..079a935a6 100644 --- a/src/storage/expressions/BinaryRelationExpression.h +++ b/src/storage/expressions/BinaryRelationExpression.h @@ -17,12 +17,12 @@ namespace storm { * Creates a binary relation expression with the given return type, operands and relation type. * * @param manager The manager responsible for this expression. - * @param returnType The return type of the expression. + * @param type The return type of the expression. * @param firstOperand The first operand of the expression. * @param secondOperand The second operand of the expression. * @param relationType The operator of the expression. */ - BinaryRelationExpression(ExpressionManager const& manager, ExpressionReturnType returnType, std::shared_ptr const& firstOperand, std::shared_ptr const& secondOperand, RelationType relationType); + BinaryRelationExpression(ExpressionManager const& manager, Type const& type, std::shared_ptr const& firstOperand, std::shared_ptr const& secondOperand, RelationType relationType); // Instantiate constructors and assignments with their default implementations. BinaryRelationExpression(BinaryRelationExpression const& other) = default; diff --git a/src/storage/expressions/BooleanLiteralExpression.cpp b/src/storage/expressions/BooleanLiteralExpression.cpp index f9c72bffe..195dc7aae 100644 --- a/src/storage/expressions/BooleanLiteralExpression.cpp +++ b/src/storage/expressions/BooleanLiteralExpression.cpp @@ -1,8 +1,9 @@ #include "src/storage/expressions/BooleanLiteralExpression.h" +#include "src/storage/expressions/ExpressionManager.h" namespace storm { namespace expressions { - BooleanLiteralExpression::BooleanLiteralExpression(ExpressionManager const& manager, bool value) : BaseExpression(manager, ExpressionReturnType::Bool), value(value) { + BooleanLiteralExpression::BooleanLiteralExpression(ExpressionManager const& manager, bool value) : BaseExpression(manager, manager.getBooleanType()), value(value) { // Intentionally left empty. } diff --git a/src/storage/expressions/DoubleLiteralExpression.cpp b/src/storage/expressions/DoubleLiteralExpression.cpp index 5d2af19cf..23bf0fc39 100644 --- a/src/storage/expressions/DoubleLiteralExpression.cpp +++ b/src/storage/expressions/DoubleLiteralExpression.cpp @@ -1,8 +1,9 @@ #include "src/storage/expressions/DoubleLiteralExpression.h" +#include "src/storage/expressions/ExpressionManager.h" namespace storm { namespace expressions { - DoubleLiteralExpression::DoubleLiteralExpression(ExpressionManager const& manager, double value) : BaseExpression(manager, ExpressionReturnType::Double), value(value) { + DoubleLiteralExpression::DoubleLiteralExpression(ExpressionManager const& manager, double value) : BaseExpression(manager, manager.getRationalType()), value(value) { // Intentionally left empty. } diff --git a/src/storage/expressions/Expression.cpp b/src/storage/expressions/Expression.cpp index f0768c0cd..2adbb4235 100644 --- a/src/storage/expressions/Expression.cpp +++ b/src/storage/expressions/Expression.cpp @@ -117,62 +117,25 @@ namespace storm { return this->expressionPtr; } - ExpressionReturnType Expression::getReturnType() const { - return this->getBaseExpression().getReturnType(); + Type Expression::getType() const { + return this->getBaseExpression().getType(); } bool Expression::hasNumericalReturnType() const { - return this->getReturnType() == ExpressionReturnType::Int || this->getReturnType() == ExpressionReturnType::Double; + return this->getBaseExpression().hasNumericalType(); } bool Expression::hasBooleanReturnType() const { - return this->getReturnType() == ExpressionReturnType::Bool; + return this->getBaseExpression().hasBooleanType(); } bool Expression::hasIntegralReturnType() const { - return this->getReturnType() == ExpressionReturnType::Int; + return this->getBaseExpression().hasIntegralType(); } - - Expression Expression::createBooleanLiteral(bool value) { - return Expression(std::shared_ptr(new BooleanLiteralExpression(value))); - } - - Expression Expression::createTrue() { - return createBooleanLiteral(true); - } - - Expression Expression::createFalse() { - return createBooleanLiteral(false); - } - - Expression Expression::createIntegerLiteral(int_fast64_t value) { - return Expression(std::shared_ptr(new IntegerLiteralExpression(value))); - } - - Expression Expression::createDoubleLiteral(double value) { - return Expression(std::shared_ptr(new DoubleLiteralExpression(value))); - } - - Expression Expression::createBooleanVariable(std::string const& variableName) { - return Expression(std::shared_ptr(new VariableExpression(ExpressionReturnType::Bool, variableName))); - } - - Expression Expression::createIntegerVariable(std::string const& variableName) { - return Expression(std::shared_ptr(new VariableExpression(ExpressionReturnType::Int, variableName))); - } - - Expression Expression::createDoubleVariable(std::string const& variableName) { - return Expression(std::shared_ptr(new VariableExpression(ExpressionReturnType::Double, variableName))); - } - - Expression Expression::createUndefinedVariable(std::string const& variableName) { - return Expression(std::shared_ptr(new VariableExpression(ExpressionReturnType::Undefined, variableName))); - } - + Expression Expression::operator+(Expression const& other) const { assertSameManager(this->getBaseExpression(), other.getBaseExpression()); - STORM_LOG_THROW(this->hasNumericalReturnType() && other.hasNumericalReturnType(), storm::exceptions::InvalidTypeException, "Operator '+' requires numerical operands."); - return Expression(std::shared_ptr(new BinaryNumericalFunctionExpression(this->getBaseExpression().getManager(), this->getReturnType() == ExpressionReturnType::Int && other.getReturnType() == ExpressionReturnType::Int ? ExpressionReturnType::Int : ExpressionReturnType::Double, this->getBaseExpressionPointer(), other.getBaseExpressionPointer(), BinaryNumericalFunctionExpression::OperatorType::Plus))); + return Expression(std::shared_ptr(new BinaryNumericalFunctionExpression(this->getBaseExpression().getManager(), this->getType().plusMinusTimes(other.getType()), this->getBaseExpressionPointer(), other.getBaseExpressionPointer(), BinaryNumericalFunctionExpression::OperatorType::Plus))); } Expression Expression::operator-(Expression const& other) const { diff --git a/src/storage/expressions/Expression.h b/src/storage/expressions/Expression.h index 395a6982e..bf5a3b08a 100644 --- a/src/storage/expressions/Expression.h +++ b/src/storage/expressions/Expression.h @@ -242,11 +242,11 @@ namespace storm { std::shared_ptr const& getBaseExpressionPointer() const; /*! - * Retrieves the return type of the expression. + * Retrieves the type of the expression. * - * @return The return type of the expression. + * @return The type of the expression. */ - ExpressionReturnType getReturnType() const; + Type getType() const; /*! * Retrieves whether the expression has a numerical return type, i.e., integer or double. diff --git a/src/storage/expressions/ExpressionManager.cpp b/src/storage/expressions/ExpressionManager.cpp index 9e518871e..42e555431 100644 --- a/src/storage/expressions/ExpressionManager.cpp +++ b/src/storage/expressions/ExpressionManager.cpp @@ -46,27 +46,13 @@ namespace storm { ++nameIndexIterator; } - ExpressionReturnType type = ExpressionReturnType::Undefined; - if ((nameIndexIterator->second & ExpressionManager::booleanMask) != 0) { - type = ExpressionReturnType::Bool; - } else if ((nameIndexIterator->second & ExpressionManager::integerMask) != 0) { - type = ExpressionReturnType::Int; - } else if ((nameIndexIterator->second & ExpressionManager::rationalMask) != 0) { - type = ExpressionReturnType::Double; - } - if (nameIndexIterator != nameIndexIteratorEnd) { - currentElement = std::make_pair(Variable(manager, nameIndexIterator->second), type); + currentElement = std::make_pair(Variable(manager, nameIndexIterator->second), manager.getVariableType(nameIndexIterator->second)); } } - ExpressionManager::ExpressionManager() : nameToIndexMapping(), variableTypeToCountMapping(), auxiliaryVariableTypeToCountMapping() { - variableTypeToCountMapping[static_cast(storm::expressions::ExpressionReturnType::Bool)] = 0; - variableTypeToCountMapping[static_cast(storm::expressions::ExpressionReturnType::Int)] = 0; - variableTypeToCountMapping[static_cast(storm::expressions::ExpressionReturnType::Double)] = 0; - auxiliaryVariableTypeToCountMapping[static_cast(storm::expressions::ExpressionReturnType::Bool)] = 0; - auxiliaryVariableTypeToCountMapping[static_cast(storm::expressions::ExpressionReturnType::Int)] = 0; - auxiliaryVariableTypeToCountMapping[static_cast(storm::expressions::ExpressionReturnType::Double)] = 0; + ExpressionManager::ExpressionManager() : nameToIndexMapping(), indexToNameMapping(), indexToTypeMapping(), variableTypeToCountMapping(), numberOfVariables(0), auxiliaryVariableTypeToCountMapping(), numberOfAuxiliaryVariables(0), freshVariableCounter(0) { + // Intentionally left empty. } Expression ExpressionManager::boolean(bool value) const { @@ -85,6 +71,22 @@ namespace storm { return this == &other; } + Type ExpressionManager::getBooleanType() const { + return Type(std::shared_ptr(new BooleanType())); + } + + Type ExpressionManager::getIntegerType() const { + return Type(std::shared_ptr(new IntegerType())); + } + + Type ExpressionManager::getBoundedIntegerType(std::size_t width) const { + return Type(std::shared_ptr(new BoundedIntegerType(width))); + } + + Type ExpressionManager::getRationalType() const { + return Type(std::shared_ptr(new RationalType())); + } + bool ExpressionManager::isValidVariableName(std::string const& name) { return name.size() < 2 || name.at(0) != '_' || name.at(1) != '_'; } @@ -94,61 +96,52 @@ namespace storm { return nameIndexPair != nameToIndexMapping.end(); } - Variable ExpressionManager::declareVariable(std::string const& name, storm::expressions::ExpressionReturnType const& variableType) { + Variable ExpressionManager::declareVariable(std::string const& name, storm::expressions::Type const& variableType) { STORM_LOG_THROW(!variableExists(name), storm::exceptions::InvalidArgumentException, "Variable with name '" << name << "' already exists."); return declareOrGetVariable(name, variableType); } - Variable ExpressionManager::declareAuxiliaryVariable(std::string const& name, storm::expressions::ExpressionReturnType const& variableType) { + Variable ExpressionManager::declareAuxiliaryVariable(std::string const& name, storm::expressions::Type const& variableType) { STORM_LOG_THROW(!variableExists(name), storm::exceptions::InvalidArgumentException, "Variable with name '" << name << "' already exists."); return declareOrGetAuxiliaryVariable(name, variableType); } - Variable ExpressionManager::declareOrGetVariable(std::string const& name, storm::expressions::ExpressionReturnType const& variableType) { + Variable ExpressionManager::declareOrGetVariable(std::string const& name, storm::expressions::Type const& variableType) { STORM_LOG_THROW(isValidVariableName(name), storm::exceptions::InvalidArgumentException, "Invalid variable name '" << name << "'."); - uint_fast64_t newIndex = 0; - switch (variableType) { - case ExpressionReturnType::Bool: - newIndex = variableTypeToCountMapping[static_cast(ExpressionReturnType::Bool)]++ | booleanMask; - break; - case ExpressionReturnType::Int: - newIndex = variableTypeToCountMapping[static_cast(ExpressionReturnType::Int)]++ | integerMask; - break; - case ExpressionReturnType::Double: - newIndex = variableTypeToCountMapping[static_cast(ExpressionReturnType::Double)]++ | rationalMask; - break; - case ExpressionReturnType::Undefined: - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Illegal variable type."); + auto nameIndexPair = nameToIndexMapping.find(name); + if (nameIndexPair != nameToIndexMapping.end()) { + return Variable(*this, nameIndexPair->second); + } else { + std::unordered_map::iterator typeCountPair = variableTypeToCountMapping.find(variableType); + uint_fast64_t& oldCount = variableTypeToCountMapping[variableType]; + + // Compute the index of the new variable. + uint_fast64_t newIndex = oldCount++ | variableType.getMask(); + + // Properly insert the variable into the data structure. + nameToIndexMapping[name] = newIndex; + indexToNameMapping[newIndex] = name; + indexToTypeMapping[newIndex] = variableType; + return Variable(*this, newIndex); } - - nameToIndexMapping[name] = newIndex; - indexToNameMapping[newIndex] = name; - return Variable(*this, newIndex); } - Variable ExpressionManager::declareOrGetAuxiliaryVariable(std::string const& name, storm::expressions::ExpressionReturnType const& variableType) { + Variable ExpressionManager::declareOrGetAuxiliaryVariable(std::string const& name, storm::expressions::Type const& variableType) { + STORM_LOG_THROW(isValidVariableName(name), storm::exceptions::InvalidArgumentException, "Invalid variable name '" << name << "'."); auto nameIndexPair = nameToIndexMapping.find(name); if (nameIndexPair != nameToIndexMapping.end()) { return Variable(*this, nameIndexPair->second); } else { - STORM_LOG_THROW(isValidVariableName(name), storm::exceptions::InvalidArgumentException, "Invalid variable name '" << name << "'."); - uint_fast64_t newIndex = auxiliaryMask; - switch (variableType) { - case ExpressionReturnType::Bool: - newIndex |= auxiliaryVariableTypeToCountMapping[static_cast(ExpressionReturnType::Bool)]++ | booleanMask; - break; - case ExpressionReturnType::Int: - newIndex |= auxiliaryVariableTypeToCountMapping[static_cast(ExpressionReturnType::Int)]++ | integerMask; - break; - case ExpressionReturnType::Double: - newIndex |= auxiliaryVariableTypeToCountMapping[static_cast(ExpressionReturnType::Double)]++ | rationalMask; - break; - case ExpressionReturnType::Undefined: - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Illegal variable type."); - } + std::unordered_map::iterator typeCountPair = auxiliaryVariableTypeToCountMapping.find(variableType); + uint_fast64_t& oldCount = auxiliaryVariableTypeToCountMapping[variableType]; + // Compute the index of the new variable. + uint_fast64_t newIndex = oldCount++ | variableType.getMask() | auxiliaryMask; + + // Properly insert the variable into the data structure. nameToIndexMapping[name] = newIndex; indexToNameMapping[newIndex] = name; + indexToTypeMapping[newIndex] = variableType; return Variable(*this, newIndex); } } @@ -163,18 +156,23 @@ namespace storm { return Expression(getVariable(name)); } - Variable ExpressionManager::declareFreshVariable(storm::expressions::ExpressionReturnType const& variableType) { + Variable ExpressionManager::declareFreshVariable(storm::expressions::Type const& variableType) { std::string newName = "__x" + std::to_string(freshVariableCounter++); return declareVariable(newName, variableType); } - Variable ExpressionManager::declareFreshAuxiliaryVariable(storm::expressions::ExpressionReturnType const& variableType) { + Variable ExpressionManager::declareFreshAuxiliaryVariable(storm::expressions::Type const& variableType) { std::string newName = "__x" + std::to_string(freshVariableCounter++); return declareAuxiliaryVariable(newName, variableType); } - uint_fast64_t ExpressionManager::getNumberOfVariables(storm::expressions::ExpressionReturnType const& variableType) const { - return variableTypeToCountMapping[static_cast(variableType)]; + uint_fast64_t ExpressionManager::getNumberOfVariables(storm::expressions::Type const& variableType) const { + auto typeCountPair = variableTypeToCountMapping.find(variableType); + if (typeCountPair == variableTypeToCountMapping.end()) { + return 0; + } else { + return typeCountPair->second; + } } uint_fast64_t ExpressionManager::getNumberOfVariables() const { @@ -182,19 +180,24 @@ namespace storm { } uint_fast64_t ExpressionManager::getNumberOfBooleanVariables() const { - return getNumberOfVariables(storm::expressions::ExpressionReturnType::Bool); + return getNumberOfVariables(getBooleanType()); } uint_fast64_t ExpressionManager::getNumberOfIntegerVariables() const { - return getNumberOfVariables(storm::expressions::ExpressionReturnType::Int); + return getNumberOfVariables(getIntegerType()); } uint_fast64_t ExpressionManager::getNumberOfRationalVariables() const { - return getNumberOfVariables(storm::expressions::ExpressionReturnType::Double); + return getNumberOfVariables(getRationalType()); } - uint_fast64_t ExpressionManager::getNumberOfAuxiliaryVariables(storm::expressions::ExpressionReturnType const& variableType) const { - return auxiliaryVariableTypeToCountMapping[static_cast(variableType)]; + uint_fast64_t ExpressionManager::getNumberOfAuxiliaryVariables(storm::expressions::Type const& variableType) const { + auto typeCountPair = auxiliaryVariableTypeToCountMapping.find(variableType); + if (typeCountPair == auxiliaryVariableTypeToCountMapping.end()) { + return 0; + } else { + return typeCountPair->second; + } } uint_fast64_t ExpressionManager::getNumberOfAuxiliaryVariables() const { @@ -202,15 +205,15 @@ namespace storm { } uint_fast64_t ExpressionManager::getNumberOfAuxiliaryBooleanVariables() const { - return getNumberOfAuxiliaryVariables(storm::expressions::ExpressionReturnType::Bool); + return getNumberOfAuxiliaryVariables(getBooleanType()); } uint_fast64_t ExpressionManager::getNumberOfAuxiliaryIntegerVariables() const { - return getNumberOfAuxiliaryVariables(storm::expressions::ExpressionReturnType::Int); + return getNumberOfAuxiliaryVariables(getIntegerType()); } uint_fast64_t ExpressionManager::getNumberOfAuxiliaryRationalVariables() const { - return getNumberOfAuxiliaryVariables(storm::expressions::ExpressionReturnType::Double); + return getNumberOfAuxiliaryVariables(getRationalType()); } std::string const& ExpressionManager::getVariableName(uint_fast64_t index) const { @@ -219,16 +222,10 @@ namespace storm { return indexTypeNamePair->second; } - ExpressionReturnType ExpressionManager::getVariableType(uint_fast64_t index) const { - if ((index & booleanMask) != 0) { - return ExpressionReturnType::Bool; - } else if ((index & integerMask) != 0) { - return ExpressionReturnType::Int; - } else if ((index & rationalMask) != 0) { - return ExpressionReturnType::Double; - } else { - return ExpressionReturnType::Undefined; - } + Type const& ExpressionManager::getVariableType(uint_fast64_t index) const { + auto indexTypePair = indexToTypeMapping.find(index); + STORM_LOG_ASSERT(indexTypePair != indexToTypeMapping.end(), "Unable to retrieve type of unknown variable index."); + return indexTypePair->second; } uint_fast64_t ExpressionManager::getOffset(uint_fast64_t index) const { diff --git a/src/storage/expressions/ExpressionManager.h b/src/storage/expressions/ExpressionManager.h index 9722e706b..30b47a503 100644 --- a/src/storage/expressions/ExpressionManager.h +++ b/src/storage/expressions/ExpressionManager.h @@ -4,6 +4,8 @@ #include #include #include +#include +#include #include "src/storage/expressions/Expression.h" #include "src/utility/OsDetection.h" @@ -13,7 +15,7 @@ namespace storm { // Forward-declare manager class for iterator class. class ExpressionManager; - class VariableIterator : public std::iterator const> { + class VariableIterator : public std::iterator const> { public: enum class VariableSelection { OnlyRegularVariables, OnlyAuxiliaryVariables, AllVariables }; @@ -49,7 +51,7 @@ namespace storm { VariableSelection selection; // The current element that is shown to the outside upon dereferencing. - std::pair currentElement; + std::pair currentElement; }; /*! @@ -106,6 +108,35 @@ namespace storm { */ bool operator==(ExpressionManager const& other) const; + /*! + * Retrieves the boolean type. + * + * @return The boolean type. + */ + Type getBooleanType() const; + + /*! + * Retrieves the integer type. + * + * @return The integer type. + */ + Type getIntegerType() const; + + /*! + * Retrieves the bounded integer type. + * + * @param width The bit width of the bounded type. + * @return The bounded integer type. + */ + Type getBoundedIntegerType(std::size_t width) const; + + /*! + * Retrieves the rational type. + * + * @return The rational type. + */ + Type getRationalType() const; + /*! * Declares a 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. @@ -114,7 +145,7 @@ namespace storm { * @param variableType The type of the variable. * @return The newly declared variable. */ - Variable declareVariable(std::string const& name, storm::expressions::ExpressionReturnType const& variableType); + Variable declareVariable(std::string const& name, storm::expressions::Type const& variableType); /*! * Declares an auxiliary variable with a name that must not yet exist and its corresponding type. @@ -123,7 +154,7 @@ namespace storm { * @param variableType The type of the variable. * @return The newly declared variable. */ - Variable declareAuxiliaryVariable(std::string const& name, storm::expressions::ExpressionReturnType const& variableType); + Variable declareAuxiliaryVariable(std::string const& name, storm::expressions::Type const& variableType); /*! * Declares a variable with the given name if it does not yet exist. @@ -132,7 +163,7 @@ namespace storm { * @param variableType The type of the variable to declare. * @return The variable. */ - Variable declareOrGetVariable(std::string const& name, storm::expressions::ExpressionReturnType const& variableType); + Variable declareOrGetVariable(std::string const& name, storm::expressions::Type const& variableType); /*! * Declares a variable with the given name if it does not yet exist. @@ -141,7 +172,7 @@ namespace storm { * @param variableType The type of the variable to declare. * @return The variable. */ - Variable declareOrGetAuxiliaryVariable(std::string const& name, storm::expressions::ExpressionReturnType const& variableType); + Variable declareOrGetAuxiliaryVariable(std::string const& name, storm::expressions::Type const& variableType); /*! * Retrieves the expression that represents the variable with the given name. @@ -164,7 +195,7 @@ namespace storm { * @param variableType The type of the variable to declare. * @return The variable. */ - Variable declareFreshVariable(storm::expressions::ExpressionReturnType const& variableType); + Variable declareFreshVariable(storm::expressions::Type const& variableType); /*! * Declares an auxiliary variable with the given type whose name is guaranteed to be unique and not yet in use. @@ -172,14 +203,14 @@ namespace storm { * @param variableType The type of the variable to declare. * @return The variable. */ - Variable declareFreshAuxiliaryVariable(storm::expressions::ExpressionReturnType const& variableType); + 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::ExpressionReturnType const& variableType) const; + uint_fast64_t getNumberOfVariables(storm::expressions::Type const& variableType) const; /*! * Retrieves the number of variables. @@ -214,7 +245,7 @@ namespace storm { * * @return The number of auxiliary variables with the given type. */ - uint_fast64_t getNumberOfAuxiliaryVariables(storm::expressions::ExpressionReturnType const& variableType) const; + uint_fast64_t getNumberOfAuxiliaryVariables(storm::expressions::Type const& variableType) const; /*! * Retrieves the number of auxiliary variables. @@ -258,7 +289,7 @@ namespace storm { * @param index The index of the variable whose name to retrieve. * @return The type of the variable. */ - ExpressionReturnType getVariableType(uint_fast64_t index) const; + Type const& getVariableType(uint_fast64_t index) const; /*! * Retrieves the offset of the variable with the given index within the group of equally typed variables. @@ -305,14 +336,17 @@ namespace storm { // A mapping from all variable indices to their names. std::unordered_map indexToNameMapping; + // A mapping from all variable indices to their types. + std::unordered_map indexToTypeMapping; + // Store counts for variables. - std::vector variableTypeToCountMapping; + std::unordered_map variableTypeToCountMapping; // The number of declared variables. uint_fast64_t numberOfVariables; // Store counts for auxiliary variables. - std::vector auxiliaryVariableTypeToCountMapping; + std::unordered_map auxiliaryVariableTypeToCountMapping; // The number of declared auxiliary variables. uint_fast64_t numberOfAuxiliaryVariables; @@ -321,11 +355,10 @@ namespace storm { uint_fast64_t freshVariableCounter; // A mask that can be used to query whether a variable is an auxiliary variable. - static const uint_fast64_t auxiliaryMask = (1 << 63); - static const uint_fast64_t booleanMask = (1 << 62); - static const uint_fast64_t integerMask = (1 << 61); - static const uint_fast64_t rationalMask = (1 << 60); - static const uint_fast64_t offsetMask = (1 << 60) - 1; + static const uint64_t auxiliaryMask = (1 << 60); + + // A mask that can be used to project a variable index to its offset (with the group of equally typed variables). + static const uint64_t offsetMask = (1 << 60) - 1; }; } } diff --git a/src/storage/expressions/ExpressionReturnType.cpp b/src/storage/expressions/ExpressionReturnType.cpp deleted file mode 100644 index c10810f6c..000000000 --- a/src/storage/expressions/ExpressionReturnType.cpp +++ /dev/null @@ -1,15 +0,0 @@ -#include "src/storage/expressions/ExpressionReturnType.h" - -namespace storm { - namespace expressions { - std::ostream& operator<<(std::ostream& stream, ExpressionReturnType const& enumValue) { - switch (enumValue) { - case ExpressionReturnType::Undefined: stream << "undefined"; break; - case ExpressionReturnType::Bool: stream << "bool"; break; - case ExpressionReturnType::Int: stream << "int"; break; - case ExpressionReturnType::Double: stream << "double"; break; - } - return stream; - } - } -} \ No newline at end of file diff --git a/src/storage/expressions/ExpressionReturnType.h b/src/storage/expressions/ExpressionReturnType.h deleted file mode 100644 index 04dd2b3ee..000000000 --- a/src/storage/expressions/ExpressionReturnType.h +++ /dev/null @@ -1,35 +0,0 @@ -#ifndef STORM_STORAGE_EXPRESSIONS_EXPRESSIONRETURNTYPE_H_ -#define STORM_STORAGE_EXPRESSIONS_EXPRESSIONRETURNTYPE_H_ - -#include - -namespace storm { - namespace expressions { - /*! - * Each node in an expression tree has a uniquely defined type from this enum. - */ - enum class ExpressionReturnType { Undefined = 0, Bool = 1, Int = 2, Double = 3}; - - std::ostream& operator<<(std::ostream& stream, ExpressionReturnType const& enumValue); - } -} - -namespace std { - // Provide a hashing operator, so we can put variables in unordered collections. - template <> - struct hash { - std::size_t operator()(storm::expressions::ExpressionReturnType const& type) const { - return static_cast(type); - } - }; - - // Provide a less operator, so we can put variables in ordered collections. - template <> - struct less { - std::size_t operator()(storm::expressions::ExpressionReturnType const& type1, storm::expressions::ExpressionReturnType const& type2) const { - return static_cast(type1) < static_cast(type2); - } - }; -} - -#endif /* STORM_STORAGE_EXPRESSIONS_EXPRESSIONRETURNTYPE_H_ */ \ No newline at end of file diff --git a/src/storage/expressions/IfThenElseExpression.cpp b/src/storage/expressions/IfThenElseExpression.cpp index 2e20c15b8..090a7cff4 100644 --- a/src/storage/expressions/IfThenElseExpression.cpp +++ b/src/storage/expressions/IfThenElseExpression.cpp @@ -5,7 +5,7 @@ namespace storm { namespace expressions { - IfThenElseExpression::IfThenElseExpression(ExpressionManager const& manager, ExpressionReturnType returnType, std::shared_ptr const& condition, std::shared_ptr const& thenExpression, std::shared_ptr const& elseExpression) : BaseExpression(manager, returnType), condition(condition), thenExpression(thenExpression), elseExpression(elseExpression) { + IfThenElseExpression::IfThenElseExpression(ExpressionManager const& manager, Type const& type, std::shared_ptr const& condition, std::shared_ptr const& thenExpression, std::shared_ptr const& elseExpression) : BaseExpression(manager, type), condition(condition), thenExpression(thenExpression), elseExpression(elseExpression) { // Intentionally left empty. } @@ -85,7 +85,7 @@ namespace storm { if (conditionSimplified.get() == this->condition.get() && thenExpressionSimplified.get() == this->thenExpression.get() && elseExpressionSimplified.get() == this->elseExpression.get()) { return this->shared_from_this(); } else { - return std::shared_ptr(new IfThenElseExpression(this->getManager(), this->getReturnType(), conditionSimplified, thenExpressionSimplified, elseExpressionSimplified)); + return std::shared_ptr(new IfThenElseExpression(this->getManager(), this->getType(), conditionSimplified, thenExpressionSimplified, elseExpressionSimplified)); } } } diff --git a/src/storage/expressions/IfThenElseExpression.h b/src/storage/expressions/IfThenElseExpression.h index 85a90c2b9..2e39a99d9 100644 --- a/src/storage/expressions/IfThenElseExpression.h +++ b/src/storage/expressions/IfThenElseExpression.h @@ -12,11 +12,11 @@ namespace storm { * Creates an if-then-else expression with the given return type, condition and operands. * * @param manager The manager responsible for this expression. - * @param returnType The return type of the expression. + * @param type The return type of the expression. * @param thenExpression The expression evaluated if the condition evaluates true. * @param elseExpression The expression evaluated if the condition evaluates false. */ - IfThenElseExpression(ExpressionManager const& manager, ExpressionReturnType returnType, std::shared_ptr const& condition, std::shared_ptr const& thenExpression, std::shared_ptr const& elseExpression); + IfThenElseExpression(ExpressionManager const& manager, Type const& type, std::shared_ptr const& condition, std::shared_ptr const& thenExpression, std::shared_ptr const& elseExpression); // Instantiate constructors and assignments with their default implementations. IfThenElseExpression(IfThenElseExpression const& other) = default; diff --git a/src/storage/expressions/IntegerLiteralExpression.cpp b/src/storage/expressions/IntegerLiteralExpression.cpp index 36b8fe2bf..bb50f26a3 100644 --- a/src/storage/expressions/IntegerLiteralExpression.cpp +++ b/src/storage/expressions/IntegerLiteralExpression.cpp @@ -1,8 +1,9 @@ #include "src/storage/expressions/IntegerLiteralExpression.h" +#include "src/storage/expressions/ExpressionManager.h" namespace storm { namespace expressions { - IntegerLiteralExpression::IntegerLiteralExpression(ExpressionManager const& manager, int_fast64_t value) : BaseExpression(manager, ExpressionReturnType::Int), value(value) { + IntegerLiteralExpression::IntegerLiteralExpression(ExpressionManager const& manager, int_fast64_t value) : BaseExpression(manager, manager.getIntegerType()), value(value) { // Intentionally left empty. } diff --git a/src/storage/expressions/LinearCoefficientVisitor.h b/src/storage/expressions/LinearCoefficientVisitor.h index faf02414b..2860da273 100644 --- a/src/storage/expressions/LinearCoefficientVisitor.h +++ b/src/storage/expressions/LinearCoefficientVisitor.h @@ -5,7 +5,7 @@ #include "src/storage/expressions/Expression.h" #include "src/storage/expressions/ExpressionVisitor.h" -#include "src/storage/expressions/SimpleValuation.h" +#include "src/storage/expressions/Valuation.h" namespace storm { namespace expressions { @@ -24,7 +24,7 @@ namespace storm { * @return A pair consisting of a mapping from identifiers to their coefficients and the coefficient of * the constant atom. */ - std::pair getLinearCoefficients(Expression const& expression); + std::pair getLinearCoefficients(Expression const& expression); virtual boost::any visit(IfThenElseExpression const& expression) override; virtual boost::any visit(BinaryBooleanFunctionExpression const& expression) override; diff --git a/src/storage/expressions/SimpleValuation.cpp b/src/storage/expressions/SimpleValuation.cpp new file mode 100644 index 000000000..331a0d8ad --- /dev/null +++ b/src/storage/expressions/SimpleValuation.cpp @@ -0,0 +1,78 @@ +#include "src/storage/expressions/SimpleValuation.h" + +#include + +#include "src/storage/expressions/ExpressionManager.h" +#include "src/storage/expressions/Variable.h" + +namespace storm { + namespace expressions { + SimpleValuation::SimpleValuation(ExpressionManager const& manager) : Valuation(manager), booleanValues(nullptr), integerValues(nullptr), rationalValues(nullptr) { + if (manager.getNumberOfBooleanVariables() > 0) { + booleanValues = std::unique_ptr>(new std::vector(manager.getNumberOfBooleanVariables())); + } + if (manager.getNumberOfIntegerVariables() > 0) { + integerValues = std::unique_ptr>(new std::vector(manager.getNumberOfIntegerVariables())); + } + if (manager.getNumberOfRationalVariables() > 0) { + rationalValues = std::unique_ptr>(new std::vector(manager.getNumberOfRationalVariables())); + } + } + + SimpleValuation::SimpleValuation(SimpleValuation const& other) : Valuation(other.getManager()) { + if (other.booleanValues != nullptr) { + booleanValues = std::unique_ptr>(new std::vector(*other.booleanValues)); + } + if (other.integerValues != nullptr) { + integerValues = std::unique_ptr>(new std::vector(*other.integerValues)); + } + if (other.booleanValues != nullptr) { + rationalValues = std::unique_ptr>(new std::vector(*other.rationalValues)); + } + } + + bool SimpleValuation::operator==(SimpleValuation const& other) const { + return this->getManager() == other.getManager() && booleanValues == other.booleanValues && integerValues == other.integerValues && rationalValues == other.rationalValues; + } + + bool SimpleValuation::getBooleanValue(Variable const& booleanVariable) const { + return (*booleanValues)[booleanVariable.getOffset()]; + } + + int_fast64_t SimpleValuation::getIntegerValue(Variable const& integerVariable) const { + return (*integerValues)[integerVariable.getOffset()]; + } + + double SimpleValuation::getRationalValue(Variable const& rationalVariable) const { + return (*rationalValues)[rationalVariable.getOffset()]; + } + + void SimpleValuation::setBooleanValue(Variable const& booleanVariable, bool value) { + (*booleanValues)[booleanVariable.getOffset()] = value; + } + + void SimpleValuation::setIntegerValue(Variable const& integerVariable, int_fast64_t value) { + (*integerValues)[integerVariable.getOffset()] = value; + } + + void SimpleValuation::setRationalValue(Variable const& rationalVariable, double value) { + (*rationalValues)[rationalVariable.getOffset()] = value; + } + + std::size_t SimpleValuationPointerHash::operator()(SimpleValuation* SimpleValuation) const { + size_t seed = 0; + boost::hash_combine(seed, SimpleValuation->booleanValues); + boost::hash_combine(seed, SimpleValuation->integerValues); + boost::hash_combine(seed, SimpleValuation->rationalValues); + return seed; + } + + bool SimpleValuationPointerCompare::operator()(SimpleValuation* SimpleValuation1, SimpleValuation* SimpleValuation2) const { + return *SimpleValuation1 == *SimpleValuation2; + } + + bool SimpleValuationPointerLess::operator()(SimpleValuation* SimpleValuation1, SimpleValuation* SimpleValuation2) const { + return SimpleValuation1->booleanValues < SimpleValuation2->booleanValues || SimpleValuation1->integerValues < SimpleValuation2->integerValues || SimpleValuation1->rationalValues < SimpleValuation2->rationalValues; + } + } +} \ No newline at end of file diff --git a/src/storage/expressions/SimpleValuation.h b/src/storage/expressions/SimpleValuation.h new file mode 100644 index 000000000..3efadd7b4 --- /dev/null +++ b/src/storage/expressions/SimpleValuation.h @@ -0,0 +1,83 @@ +#ifndef STORM_STORAGE_EXPRESSIONS_SIMPLEVALUATION_H_ +#define STORM_STORAGE_EXPRESSIONS_SIMPLEVALUATION_H_ + +#include +#include + +#include "src/storage/expressions/Valuation.h" + +namespace storm { + namespace expressions { + + /*! + * A simple implementation of the valuation interface. + */ + class SimpleValuation : public Valuation { + public: + /*! + * Creates a new valuation over the non-auxiliary variables of the given manager. + */ + SimpleValuation(storm::expressions::ExpressionManager const& manager); + + /*! + * Deep-copies the valuation. + * + * @param other The valuation to copy + */ + SimpleValuation(SimpleValuation const& other); + + /*! + * Checks whether the two valuations are semantically equivalent. + * + * @param other The valuation with which to compare. + * @return True iff the two valuations are semantically equivalent. + */ + bool operator==(SimpleValuation const& other) const; + + // + 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 void setIntegerValue(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; + + private: + // Containers that store the values of the variables of the appropriate type. + std::unique_ptr> booleanValues; + std::unique_ptr> integerValues; + std::unique_ptr> rationalValues; + }; + + /*! + * A helper class that can pe used as the hash functor for data structures that need to hash valuations given + * via pointers. + */ + class SimpleValuationPointerHash { + public: + std::size_t operator()(SimpleValuation* valuation) const; + }; + + /*! + * A helper class that can be used as the comparison functor wrt. equality for data structures that need to + * store pointers to valuations and need to compare the elements wrt. their content (rather than pointer + * equality). + */ + class SimpleValuationPointerCompare { + public: + bool operator()(SimpleValuation* valuation1, SimpleValuation* valuation2) const; + }; + + /*! + * A helper class that can be used as the comparison functor wrt. "<" for data structures that need to + * store pointers to valuations and need to compare the elements wrt. their content (rather than pointer + * equality). + */ + class SimpleValuationPointerLess { + public: + bool operator()(SimpleValuation* valuation1, SimpleValuation* valuation2) const; + }; + } +} + +#endif /* STORM_STORAGE_EXPRESSIONS_SIMPLEVALUATION_H_ */ \ No newline at end of file diff --git a/src/storage/expressions/Type.cpp b/src/storage/expressions/Type.cpp new file mode 100644 index 000000000..bfc2adaff --- /dev/null +++ b/src/storage/expressions/Type.cpp @@ -0,0 +1,156 @@ +#include "src/storage/expressions/Type.h" + +#include "src/storage/expressions/ExpressionManager.h" +#include "src/utility/macros.h" + +namespace storm { + namespace expressions { + + bool BaseType::operator==(BaseType const& other) const { + return this->getMask() == other.getMask(); + } + + uint64_t BooleanType::getMask() const { + return BooleanType::mask; + } + + std::string BooleanType::getStringRepresentation() const { + return "bool"; + } + + uint64_t IntegerType::getMask() const { + return IntegerType::mask; + } + + std::string IntegerType::getStringRepresentation() const { + return "int"; + } + + uint64_t BoundedIntegerType::getMask() const { + return BoundedIntegerType::mask; + } + + std::string BoundedIntegerType::getStringRepresentation() const { + return "int[" + std::to_string(width) + "]"; + } + + std::size_t BoundedIntegerType::getWidth() const { + return width; + } + + bool BoundedIntegerType::operator==(BaseType const& other) const { + return this->getMask() == other.getMask() && this->width == static_cast(other).width; + } + + uint64_t RationalType::getMask() const { + return RationalType::mask; + } + + std::string RationalType::getStringRepresentation() const { + return "rational"; + } + + Type::Type(ExpressionManager const& manager, std::shared_ptr innerType) : manager(manager), innerType(innerType) { + // Intentionally left empty. + } + + bool Type::operator==(Type const& other) const { + return *this->innerType == *other.innerType; + } + + uint64_t Type::getMask() const { + return this->innerType->getMask(); + } + + std::string Type::getStringRepresentation() const { + return this->innerType->getStringRepresentation(); + } + + bool Type::isNumericalType() const { + return this->isIntegralType() || this->isRationalType(); + } + + bool Type::isIntegralType() const { + return this->isUnboundedIntegralType() || this->isBoundedIntegralType(); + } + + bool Type::isBooleanType() const { + return typeid(*this->innerType) == typeid(BooleanType); + } + + bool Type::isUnboundedIntegralType() const { + return typeid(*this->innerType) == typeid(IntegerType); + } + + bool Type::isBoundedIntegralType() const { + return typeid(*this->innerType) == typeid(BoundedIntegerType); + } + + std::size_t Type::getWidth() const { + return dynamic_cast(*this->innerType).getWidth(); + } + + bool Type::isRationalType() const { + return typeid(*this->innerType) == typeid(RationalType); + } + + Type Type::plusMinusTimes(Type const& other) const { + STORM_LOG_ASSERT(this->isNumericalType() && other.isNumericalType(), "Operator requires numerical operands."); + if (this->isRationalType() || other.isRationalType()) { + return manager.getRationalType(); + } + return manager.getIntegerType(); + } + + Type Type::minus() const { + STORM_LOG_ASSERT(this->isNumericalType(), "Operator requires numerical operand."); + return *this; + } + + Type Type::divide(Type const& other) const { + STORM_LOG_ASSERT(this->isNumericalType() && other.isNumericalType(), "Operator requires numerical operands."); + return manager.getRationalType(); + } + + Type Type::logicalConnective(Type const& other) const { + STORM_LOG_ASSERT(this->isBooleanType() && other.isBooleanType(), "Operator requires boolean operands."); + return *this; + } + + Type Type::logicalConnective() const { + STORM_LOG_ASSERT(this->isBooleanType(), "Operator requires boolean operand."); + return *this; + } + + Type Type::numericalComparison(Type const& other) const { + STORM_LOG_ASSERT(this->isNumericalType() && other.isNumericalType(), "Operator requires numerical operands."); + if (this->isRationalType() || other.isRationalType()) { + return manager.getRationalType(); + } + return manager.getIntegerType(); + } + + Type Type::ite(Type const& thenType, Type const& elseType) const { + STORM_LOG_ASSERT(thenType == elseType, "Operator requires equal types."); + return thenType; + } + + Type Type::floorCeil() const { + STORM_LOG_ASSERT(this->isRationalType(), "Operator requires rational operand."); + return manager.getIntegerType(); + } + + Type Type::minimumMaximum(Type const& other) const { + STORM_LOG_ASSERT(this->isNumericalType() && other.isNumericalType(), "Operator requires numerical operands."); + if (this->isRationalType() || other.isRationalType()) { + return manager.getRationalType(); + } + return manager.getIntegerType(); + } + + std::ostream& operator<<(std::ostream& stream, Type const& type) { + stream << type.getStringRepresentation(); + return stream; + } + } +} \ No newline at end of file diff --git a/src/storage/expressions/Type.h b/src/storage/expressions/Type.h new file mode 100644 index 000000000..b8a3f51de --- /dev/null +++ b/src/storage/expressions/Type.h @@ -0,0 +1,224 @@ +#ifndef STORM_STORAGE_EXPRESSIONS_EXPRESSIONRETURNTYPE_H_ +#define STORM_STORAGE_EXPRESSIONS_EXPRESSIONRETURNTYPE_H_ + +#include +#include +#include + +#include "src/storage/expressions/OperatorType.h" + +namespace storm { + namespace expressions { + // Forward-declare expression manager class. + class ExpressionManager; + + class BaseType { + public: + /*! + * Retrieves the mask that is associated with this type. + * + * @return The mask associated with this type. + */ + virtual uint64_t getMask() const = 0; + + /*! + * Checks whether two types are actually the same. + * + * @param other The type to compare with. + * @return True iff the types are the same. + */ + virtual bool operator==(BaseType const& other) const; + + /*! + * Returns a string representation of the type. + * + * @return A string representation of the type. + */ + virtual std::string getStringRepresentation() const = 0; + }; + + class BooleanType : public BaseType { + public: + virtual uint64_t getMask() const override; + virtual std::string getStringRepresentation() const override; + + private: + static const uint64_t mask = (1 << 61); + }; + + class IntegerType : public BaseType { + public: + virtual uint64_t getMask() const override; + virtual std::string getStringRepresentation() const override; + + private: + static const uint64_t mask = (1 << 62); + }; + + class BoundedIntegerType : public BaseType { + public: + /*! + * Creates a new bounded integer type with the given bit width. + * + * @param width The bit width of the type. + */ + BoundedIntegerType(std::size_t width); + + /*! + * Retrieves the bit width of the bounded type. + * + * @return The bit width of the bounded type. + */ + std::size_t getWidth() const; + + virtual uint64_t getMask() const override; + + virtual bool operator==(BaseType const& other) const override; + + virtual std::string getStringRepresentation() const override; + + private: + static const uint64_t mask = (1 << 61) | (1 << 62); + + // The bit width of the type. + std::size_t width; + }; + + class RationalType : public BaseType { + public: + virtual uint64_t getMask() const override; + + virtual std::string getStringRepresentation() const override; + + private: + static const uint64_t mask = (1 << 63); + }; + + class ErrorType : public BaseType { + public: + virtual uint64_t getMask() const override; + + virtual std::string getStringRepresentation() const override; + + private: + static const uint64_t mask = 0; + }; + + class Type { + public: + Type(ExpressionManager const& manager, std::shared_ptr innerType); + + /*! + * Checks whether two types are the same. + * + * @other The type to compare with. + * @return True iff the types are the same. + */ + bool operator==(Type const& other) const; + + /*! + * Retrieves the bit mask of the type. + * + * @return The bit mask of the type. + */ + uint64_t getMask() const; + + /*! + * Retrieves a string representation of the type. + * + * @return A string representation of the type. + */ + std::string getStringRepresentation() const; + + /*! + * Checks whether this type is a numerical type. + * + * @return True iff the type is a numerical one. + */ + bool isNumericalType() const; + + /*! + * Checks whether this type is an integral type. + * + * @return True iff the type is a integral one. + */ + bool isIntegralType() const; + + /*! + * Checks whether this type is a boolean type. + * + * @return True iff the type is a boolean one. + */ + bool isBooleanType() const; + + /*! + * Checks whether this type is an unbounded integral type. + * + * @return True iff the type is a unbounded integral one. + */ + bool isUnboundedIntegralType() const; + + /*! + * Checks whether this type is a bounded integral type. + * + * @return True iff the type is a bounded integral one. + */ + bool isBoundedIntegralType() const; + + /*! + * Retrieves the bit width of the type, provided that it is a bounded integral type. + * + * @return The bit width of the bounded integral type. + */ + std::size_t getWidth() const; + + /*! + * Checks whether this type is a rational type. + * + * @return True iff the type is a rational one. + */ + bool isRationalType() const; + + // Functions that, given the input types, produce the output type of the corresponding function application. + Type plusMinusTimes(Type const& other) const; + Type minus() const; + Type divide(Type const& other) const; + Type logicalConnective(Type const& other) const; + Type logicalConnective() const; + Type numericalComparison(Type const& other) const; + Type ite(Type const& thenType, Type const& elseType) const; + Type floorCeil() const; + Type minimumMaximum(Type const& other) const; + + private: + // The manager responsible for the type. + ExpressionManager const& manager; + + // The encapsulated type. + std::shared_ptr innerType; + }; + + std::ostream& operator<<(std::ostream& stream, Type const& type); + + } +} + +namespace std { + // Provide a hashing operator, so we can put types in unordered collections. + template <> + struct hash { + std::size_t operator()(storm::expressions::Type const& type) const { + return std::hash()(type.getMask()); + } + }; + + // Provide a less operator, so we can put types in ordered collections. + template <> + struct less { + std::size_t operator()(storm::expressions::Type const& type1, storm::expressions::Type const& type2) const { + return type1.getMask() < type2.getMask(); + } + }; +} + +#endif /* STORM_STORAGE_EXPRESSIONS_EXPRESSIONRETURNTYPE_H_ */ \ No newline at end of file diff --git a/src/storage/expressions/UnaryBooleanFunctionExpression.cpp b/src/storage/expressions/UnaryBooleanFunctionExpression.cpp index 74b96a36c..70347080c 100644 --- a/src/storage/expressions/UnaryBooleanFunctionExpression.cpp +++ b/src/storage/expressions/UnaryBooleanFunctionExpression.cpp @@ -5,7 +5,7 @@ namespace storm { namespace expressions { - UnaryBooleanFunctionExpression::UnaryBooleanFunctionExpression(ExpressionManager const& manager, ExpressionReturnType returnType, std::shared_ptr const& operand, OperatorType operatorType) : UnaryExpression(manager, returnType, operand), operatorType(operatorType) { + UnaryBooleanFunctionExpression::UnaryBooleanFunctionExpression(ExpressionManager const& manager, Type const& type, std::shared_ptr const& operand, OperatorType operatorType) : UnaryExpression(manager, type, operand), operatorType(operatorType) { // Intentionally left empty. } @@ -20,7 +20,7 @@ namespace storm { } bool UnaryBooleanFunctionExpression::evaluateAsBool(Valuation const* valuation) const { - STORM_LOG_THROW(this->hasBooleanReturnType(), storm::exceptions::InvalidTypeException, "Unable to evaluate expression as boolean."); + STORM_LOG_THROW(this->hasBooleanType(), storm::exceptions::InvalidTypeException, "Unable to evaluate expression as boolean."); bool operandEvaluated = this->getOperand()->evaluateAsBool(valuation); switch (this->getOperatorType()) { @@ -32,16 +32,16 @@ namespace storm { std::shared_ptr operandSimplified = this->getOperand()->simplify(); switch (this->getOperatorType()) { case OperatorType::Not: if (operandSimplified->isTrue()) { - return std::shared_ptr(new BooleanLiteralExpression(false)); + return std::shared_ptr(new BooleanLiteralExpression(this->getManager(), false)); } else { - return std::shared_ptr(new BooleanLiteralExpression(true)); + return std::shared_ptr(new BooleanLiteralExpression(this->getManager(), true)); } } if (operandSimplified.get() == this->getOperand().get()) { return this->shared_from_this(); } else { - return std::shared_ptr(new UnaryBooleanFunctionExpression(this->getReturnType(), operandSimplified, this->getOperatorType())); + return std::shared_ptr(new UnaryBooleanFunctionExpression(this->getManager(), this->getType(), operandSimplified, this->getOperatorType())); } } diff --git a/src/storage/expressions/UnaryBooleanFunctionExpression.h b/src/storage/expressions/UnaryBooleanFunctionExpression.h index 3cf7c0b55..7502521e0 100644 --- a/src/storage/expressions/UnaryBooleanFunctionExpression.h +++ b/src/storage/expressions/UnaryBooleanFunctionExpression.h @@ -17,11 +17,11 @@ namespace storm { * Creates a unary boolean function expression with the given return type, operand and operator. * * @param manager The manager responsible for this expression. - * @param returnType The return type of the expression. + * @param type The return type of the expression. * @param operand The operand of the expression. * @param operatorType The operator of the expression. */ - UnaryBooleanFunctionExpression(ExpressionManager const& manager, ExpressionReturnType returnType, std::shared_ptr const& operand, OperatorType operatorType); + UnaryBooleanFunctionExpression(ExpressionManager const& manager, Type const& type, std::shared_ptr const& operand, OperatorType operatorType); // Instantiate constructors and assignments with their default implementations. UnaryBooleanFunctionExpression(UnaryBooleanFunctionExpression const& other) = default; diff --git a/src/storage/expressions/UnaryExpression.cpp b/src/storage/expressions/UnaryExpression.cpp index 57abeeedc..c51ef0703 100644 --- a/src/storage/expressions/UnaryExpression.cpp +++ b/src/storage/expressions/UnaryExpression.cpp @@ -5,7 +5,7 @@ namespace storm { namespace expressions { - UnaryExpression::UnaryExpression(ExpressionManager const& manager, ExpressionReturnType returnType, std::shared_ptr const& operand) : BaseExpression(manager, returnType), operand(operand) { + UnaryExpression::UnaryExpression(ExpressionManager const& manager, Type const& type, std::shared_ptr const& operand) : BaseExpression(manager, type), operand(operand) { // Intentionally left empty. } diff --git a/src/storage/expressions/UnaryExpression.h b/src/storage/expressions/UnaryExpression.h index 60b770622..fa5b54649 100644 --- a/src/storage/expressions/UnaryExpression.h +++ b/src/storage/expressions/UnaryExpression.h @@ -12,10 +12,10 @@ namespace storm { * Creates a unary expression with the given return type and operand. * * @param manager The manager responsible for this expression. - * @param returnType The return type of the expression. + * @param type The return type of the expression. * @param operand The operand of the unary expression. */ - UnaryExpression(ExpressionManager const& manager, ExpressionReturnType returnType, std::shared_ptr const& operand); + UnaryExpression(ExpressionManager const& manager, Type const& type, std::shared_ptr const& operand); // Instantiate constructors and assignments with their default implementations. UnaryExpression(UnaryExpression const& other); diff --git a/src/storage/expressions/UnaryNumericalFunctionExpression.cpp b/src/storage/expressions/UnaryNumericalFunctionExpression.cpp index 6237db107..86c743a4a 100644 --- a/src/storage/expressions/UnaryNumericalFunctionExpression.cpp +++ b/src/storage/expressions/UnaryNumericalFunctionExpression.cpp @@ -6,7 +6,7 @@ namespace storm { namespace expressions { - UnaryNumericalFunctionExpression::UnaryNumericalFunctionExpression(ExpressionManager const& manager, ExpressionReturnType returnType, std::shared_ptr const& operand, OperatorType operatorType) : UnaryExpression(manager, returnType, operand), operatorType(operatorType) { + UnaryNumericalFunctionExpression::UnaryNumericalFunctionExpression(ExpressionManager const& manager, Type const& type, std::shared_ptr const& operand, OperatorType operatorType) : UnaryExpression(manager, type, operand), operatorType(operatorType) { // Intentionally left empty. } @@ -23,7 +23,7 @@ namespace storm { } int_fast64_t UnaryNumericalFunctionExpression::evaluateAsInt(Valuation const* valuation) const { - STORM_LOG_THROW(this->hasIntegralReturnType(), storm::exceptions::InvalidTypeException, "Unable to evaluate expression as integer."); + STORM_LOG_THROW(this->hasIntegralType(), storm::exceptions::InvalidTypeException, "Unable to evaluate expression as integer."); int_fast64_t operandEvaluated = this->getOperand()->evaluateAsInt(valuation); switch (this->getOperatorType()) { @@ -34,7 +34,7 @@ namespace storm { } double UnaryNumericalFunctionExpression::evaluateAsDouble(Valuation const* valuation) const { - STORM_LOG_THROW(this->hasNumericalReturnType(), storm::exceptions::InvalidTypeException, "Unable to evaluate expression as double."); + STORM_LOG_THROW(this->hasNumericalType(), storm::exceptions::InvalidTypeException, "Unable to evaluate expression as double."); double operandEvaluated = this->getOperand()->evaluateAsDouble(valuation); switch (this->getOperatorType()) { @@ -50,7 +50,7 @@ namespace storm { if (operandSimplified.get() == this->getOperand().get()) { return this->shared_from_this(); } else { - return std::shared_ptr(new UnaryNumericalFunctionExpression(this->getReturnType(), operandSimplified, this->getOperatorType())); + return std::shared_ptr(new UnaryNumericalFunctionExpression(this->getManager(), this->getType(), operandSimplified, this->getOperatorType())); } } diff --git a/src/storage/expressions/UnaryNumericalFunctionExpression.h b/src/storage/expressions/UnaryNumericalFunctionExpression.h index b4aac426e..3b79d223d 100644 --- a/src/storage/expressions/UnaryNumericalFunctionExpression.h +++ b/src/storage/expressions/UnaryNumericalFunctionExpression.h @@ -17,11 +17,11 @@ namespace storm { * Creates a unary numerical function expression with the given return type, operand and operator. * * @param manager The manager responsible for this expression. - * @param returnType The return type of the expression. + * @param type The return type of the expression. * @param operand The operand of the expression. * @param operatorType The operator of the expression. */ - UnaryNumericalFunctionExpression(ExpressionManager const& manager, ExpressionReturnType returnType, std::shared_ptr const& operand, OperatorType operatorType); + UnaryNumericalFunctionExpression(ExpressionManager const& manager, Type const& type, std::shared_ptr const& operand, OperatorType operatorType); // Instantiate constructors and assignments with their default implementations. UnaryNumericalFunctionExpression(UnaryNumericalFunctionExpression const& other) = default; diff --git a/src/storage/expressions/Valuation.cpp b/src/storage/expressions/Valuation.cpp index a875b358f..831e49066 100644 --- a/src/storage/expressions/Valuation.cpp +++ b/src/storage/expressions/Valuation.cpp @@ -1,82 +1,10 @@ #include "src/storage/expressions/Valuation.h" - -#include - #include "src/storage/expressions/ExpressionManager.h" -#include "src/storage/expressions/Variable.h" namespace storm { namespace expressions { - Valuation::Valuation(ExpressionManager const& manager) : manager(manager), booleanValues(nullptr), integerValues(nullptr), rationalValues(nullptr) { - if (manager.getNumberOfBooleanVariables() > 0) { - booleanValues = std::unique_ptr>(new std::vector(manager.getNumberOfBooleanVariables())); - } - if (manager.getNumberOfIntegerVariables() > 0) { - integerValues = std::unique_ptr>(new std::vector(manager.getNumberOfIntegerVariables())); - } - if (manager.getNumberOfRationalVariables() > 0) { - rationalValues = std::unique_ptr>(new std::vector(manager.getNumberOfRationalVariables())); - } - } - - Valuation::Valuation(Valuation const& other) : manager(other.manager) { - if (other.booleanValues != nullptr) { - booleanValues = std::unique_ptr>(new std::vector(*other.booleanValues)); - } - if (other.integerValues != nullptr) { - integerValues = std::unique_ptr>(new std::vector(*other.integerValues)); - } - if (other.booleanValues != nullptr) { - rationalValues = std::unique_ptr>(new std::vector(*other.rationalValues)); - } - } - - bool Valuation::operator==(Valuation const& other) const { - return manager == other.manager && booleanValues == other.booleanValues && integerValues == other.integerValues && rationalValues == other.rationalValues; - } - - bool Valuation::getBooleanValue(Variable const& booleanVariable) const { - return (*booleanValues)[booleanVariable.getOffset()]; - } - - int_fast64_t Valuation::getIntegerValue(Variable const& integerVariable) const { - return (*integerValues)[integerVariable.getOffset()]; - } - - double Valuation::getRationalValue(Variable const& rationalVariable) const { - return (*rationalValues)[rationalVariable.getOffset()]; - } - - void Valuation::setBooleanValue(Variable const& booleanVariable, bool value) { - (*booleanValues)[booleanVariable.getOffset()] = value; - } - - void Valuation::setIntegerValue(Variable const& integerVariable, int_fast64_t value) { - (*integerValues)[integerVariable.getOffset()] = value; - } - - void Valuation::setRationalValue(Variable const& rationalVariable, double value) { - (*rationalValues)[rationalVariable.getOffset()] = value; - } - ExpressionManager const& Valuation::getManager() const { return manager; } - - std::size_t ValuationPointerHash::operator()(Valuation* valuation) const { - size_t seed = 0; - boost::hash_combine(seed, valuation->booleanValues); - boost::hash_combine(seed, valuation->integerValues); - boost::hash_combine(seed, valuation->rationalValues); - return seed; - } - - bool ValuationPointerCompare::operator()(Valuation* valuation1, Valuation* valuation2) const { - return *valuation1 == *valuation2; - } - - bool ValuationPointerLess::operator()(Valuation* valuation1, Valuation* valuation2) const { - return valuation1->booleanValues < valuation2->booleanValues || valuation1->integerValues < valuation2->integerValues || valuation1->rationalValues < valuation2->rationalValues; - } } } \ No newline at end of file diff --git a/src/storage/expressions/Valuation.h b/src/storage/expressions/Valuation.h index 2d56ae106..034df3a28 100644 --- a/src/storage/expressions/Valuation.h +++ b/src/storage/expressions/Valuation.h @@ -10,7 +10,7 @@ namespace storm { class Variable; /*! - * A class to store a valuation of variables. This is, for example, used for evaluating expressions. + * The base class of all valuations of variables. This is, for example, used for evaluating expressions. */ class Valuation { public: @@ -26,28 +26,13 @@ namespace storm { */ Valuation(ExpressionManager const& manager); - /*! - * Deep-copies the valuation. - * - * @param other The valuation to copy - */ - Valuation(Valuation const& other); - - /*! - * Checks whether the two valuations are semantically equivalent. - * - * @param other The valuation with which to compare. - * @return True iff the two valuations are semantically equivalent. - */ - bool operator==(Valuation const& other) const; - /*! * Retrieves the value of the given boolean variable. * * @param booleanVariable The boolean variable whose value to retrieve. * @return The value of the boolean variable. */ - bool getBooleanValue(Variable const& booleanVariable) const; + virtual bool getBooleanValue(Variable const& booleanVariable) const = 0; /*! * Sets the value of the given boolean variable to the provided value. @@ -55,7 +40,7 @@ namespace storm { * @param booleanVariable The variable whose value to set. * @param value The new value of the variable. */ - void setBooleanValue(Variable const& booleanVariable, bool value); + virtual void setBooleanValue(Variable const& booleanVariable, bool value) = 0; /*! * Retrieves the value of the given integer variable. @@ -63,7 +48,7 @@ namespace storm { * @param integerVariable The integer variable whose value to retrieve. * @return The value of the integer variable. */ - int_fast64_t getIntegerValue(Variable const& integerVariable) const; + virtual int_fast64_t getIntegerValue(Variable const& integerVariable) const = 0; /*! * Sets the value of the given boolean variable to the provided value. @@ -71,7 +56,7 @@ namespace storm { * @param integerVariable The variable whose value to set. * @param value The new value of the variable. */ - void setIntegerValue(Variable const& integerVariable, int_fast64_t value); + virtual void setIntegerValue(Variable const& integerVariable, int_fast64_t value) = 0; /*! * Retrieves the value of the given rational variable. @@ -79,7 +64,7 @@ namespace storm { * @param rationalVariable The rational variable whose value to retrieve. * @return The value of the rational variable. */ - double getRationalValue(Variable const& rationalVariable) const; + virtual double getRationalValue(Variable const& rationalVariable) const = 0; /*! * Sets the value of the given boolean variable to the provided value. @@ -87,7 +72,7 @@ namespace storm { * @param integerVariable The variable whose value to set. * @param value The new value of the variable. */ - void setRationalValue(Variable const& rationalVariable, double value); + virtual void setRationalValue(Variable const& rationalVariable, double value) = 0; /*! * Retrieves the manager responsible for the variables of this valuation. @@ -99,40 +84,6 @@ namespace storm { private: // The manager responsible for the variables of this valuation. ExpressionManager const& manager; - - // Containers that store the values of the variables of the appropriate type. - std::unique_ptr> booleanValues; - std::unique_ptr> integerValues; - std::unique_ptr> rationalValues; - }; - - /*! - * A helper class that can pe used as the hash functor for data structures that need to hash valuations given - * via pointers. - */ - class ValuationPointerHash { - public: - std::size_t operator()(Valuation* valuation) const; - }; - - /*! - * A helper class that can be used as the comparison functor wrt. equality for data structures that need to - * store pointers to valuations and need to compare the elements wrt. their content (rather than pointer - * equality). - */ - class ValuationPointerCompare { - public: - bool operator()(Valuation* valuation1, Valuation* valuation2) const; - }; - - /*! - * A helper class that can be used as the comparison functor wrt. "<" for data structures that need to - * store pointers to valuations and need to compare the elements wrt. their content (rather than pointer - * equality). - */ - class ValuationPointerLess { - public: - bool operator()(Valuation* valuation1, Valuation* valuation2) const; }; } } diff --git a/src/storage/expressions/Variable.cpp b/src/storage/expressions/Variable.cpp index 67683dfaa..2c6b5780e 100644 --- a/src/storage/expressions/Variable.cpp +++ b/src/storage/expressions/Variable.cpp @@ -27,7 +27,7 @@ namespace storm { return manager.getVariableName(index); } - ExpressionReturnType Variable::getType() const { + Type const& Variable::getType() const { return manager.getVariableType(index); } @@ -36,19 +36,19 @@ namespace storm { } bool Variable::hasBooleanType() const { - return this->getType() == ExpressionReturnType::Bool; + return this->getType().isBooleanType(); } bool Variable::hasIntegralType() const { - return this->getType() == ExpressionReturnType::Int; + return this->getType().isIntegralType(); } bool Variable::hasRationalType() const { - return this->getType() == ExpressionReturnType::Double; + return this->getType().isRationalType(); } bool Variable::hasNumericType() const { - return this->getType() == ExpressionReturnType::Int || this->getType() == ExpressionReturnType::Double; + return this->getType().isNumericalType(); } } } \ No newline at end of file diff --git a/src/storage/expressions/Variable.h b/src/storage/expressions/Variable.h index 10325877d..51e3c13b0 100644 --- a/src/storage/expressions/Variable.h +++ b/src/storage/expressions/Variable.h @@ -5,7 +5,7 @@ #include #include "src/utility/OsDetection.h" -#include "src/storage/expressions/ExpressionReturnType.h" +#include "src/storage/expressions/Type.h" #include "src/storage/expressions/Expression.h" namespace storm { @@ -51,7 +51,7 @@ namespace storm { * * @return The type of the variable. */ - ExpressionReturnType getType() const; + Type const& getType() const; /*! * Retrieves an expression that represents the variable.