From 99d9a9710d0ccbff0bc4064ec5be1900ff23a561 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 6 Jan 2015 17:56:07 +0100 Subject: [PATCH] Further steps to make everything work again. Former-commit-id: 3f45a49dabbda57a14b9019d554cdf277ab88666 --- src/adapters/MathsatExpressionAdapter.h | 38 +- src/adapters/Z3ExpressionAdapter.h | 59 +-- .../SparseMarkovAutomatonCslModelChecker.h | 23 +- src/parser/ExpressionParser.cpp | 14 +- src/solver/LpSolver.h | 10 + src/storage/dd/CuddDdManager.cpp | 42 ++- src/storage/expressions/BaseExpression.cpp | 4 + src/storage/expressions/BaseExpression.h | 12 +- src/storage/expressions/BinaryExpression.cpp | 8 +- src/storage/expressions/BinaryExpression.h | 2 +- .../expressions/BooleanLiteralExpression.cpp | 4 +- .../expressions/BooleanLiteralExpression.h | 2 +- .../expressions/DoubleLiteralExpression.cpp | 4 +- .../expressions/DoubleLiteralExpression.h | 2 +- src/storage/expressions/Expression.cpp | 181 ++++----- src/storage/expressions/Expression.h | 116 +++--- src/storage/expressions/ExpressionManager.cpp | 12 + src/storage/expressions/ExpressionManager.h | 27 ++ .../expressions/IfThenElseExpression.cpp | 11 +- .../expressions/IfThenElseExpression.h | 2 +- .../expressions/IntegerLiteralExpression.cpp | 4 +- .../expressions/IntegerLiteralExpression.h | 2 +- src/storage/expressions/SimpleValuation.cpp | 4 + src/storage/expressions/SimpleValuation.h | 5 + src/storage/expressions/Type.cpp | 5 + src/storage/expressions/UnaryExpression.cpp | 4 +- src/storage/expressions/UnaryExpression.h | 2 +- .../expressions/VariableExpression.cpp | 4 +- src/storage/expressions/VariableExpression.h | 2 +- src/storage/prism/Program.cpp | 171 ++++----- .../adapter/MathsatExpressionAdapterTest.cpp | 80 ++-- .../adapter/Z3ExpressionAdapterTest.cpp | 54 ++- test/functional/solver/GlpkLpSolverTest.cpp | 171 +++++---- test/functional/solver/GurobiLpSolverTest.cpp | 201 +++++----- .../solver/MathSatSmtSolverTest.cpp | 173 +++++---- test/functional/solver/Z3SmtSolverTest.cpp | 328 ++++++++--------- test/functional/storage/CuddDdTest.cpp | 252 ++++++------- test/functional/storage/ExpressionTest.cpp | 346 +++++++++--------- 38 files changed, 1302 insertions(+), 1079 deletions(-) diff --git a/src/adapters/MathsatExpressionAdapter.h b/src/adapters/MathsatExpressionAdapter.h index b9f5c3d4d..94b1e1e9e 100644 --- a/src/adapters/MathsatExpressionAdapter.h +++ b/src/adapters/MathsatExpressionAdapter.h @@ -9,6 +9,7 @@ #include "mathsat.h" #endif +#include "storage/expressions/ExpressionManager.h" #include "storage/expressions/Expressions.h" #include "storage/expressions/ExpressionVisitor.h" #include "src/utility/macros.h" @@ -68,7 +69,13 @@ namespace storm { * @return An equivalent term for MathSAT. */ msat_term translateExpression(storm::expressions::Variable const& variable) { - return msat_make_constant(env, variableToDeclarationMapping[variable]); + STORM_LOG_ASSERT(variable.getManager() == this->manager, "Invalid expression for solver."); + + auto const& variableExpressionPair = variableToDeclarationMapping.find(variable); + if (variableExpressionPair != variableToDeclarationMapping.end()) { + return msat_make_constant(env, createVariable(variable)); + } + return msat_make_constant(env, variableExpressionPair->second); } /*! @@ -204,7 +211,7 @@ namespace storm { } virtual boost::any visit(expressions::VariableExpression const& expression) override { - return msat_make_constant(env, variableToDeclarationMapping[expression.getVariable()]); + return translateExpression(expression.getVariable()); } storm::expressions::Expression translateExpression(msat_term const& term) { @@ -213,7 +220,7 @@ namespace storm { } else if (msat_term_is_or(env, term)) { return translateExpression(msat_term_get_arg(term, 0)) || translateExpression(msat_term_get_arg(term, 1)); } else if (msat_term_is_iff(env, term)) { - return translateExpression(msat_term_get_arg(term, 0)).iff(translateExpression(msat_term_get_arg(term, 1))); + return storm::expressions::iff(translateExpression(msat_term_get_arg(term, 0)), translateExpression(msat_term_get_arg(term, 1))); } else if (msat_term_is_not(env, term)) { return !translateExpression(msat_term_get_arg(term, 0)); } else if (msat_term_is_plus(env, term)) { @@ -250,12 +257,35 @@ namespace storm { } private: + /*! + * Creates a MathSAT variable for the provided variable. + * + * @param variable The variable for which to create a MathSAT counterpart. + */ + msat_decl createVariable(storm::expressions::Variable const& variable) { + msat_decl msatDeclaration; + if (variable.getType().isBooleanType()) { + msatDeclaration = msat_declare_function(env, variable.getName().c_str(), msat_get_bool_type(env)); + } else if (variable.getType().isUnboundedIntegralType()) { + msatDeclaration = msat_declare_function(env, variable.getName().c_str(), msat_get_integer_type(env)); + } else if (variable.getType().isBoundedIntegralType()) { + msatDeclaration = msat_declare_function(env, variable.getName().c_str(), msat_get_bv_type(env, variable.getType().getWidth())); + } else if (variable.getType().isRationalType()) { + msatDeclaration = msat_declare_function(env, variable.getName().c_str(), msat_get_rational_type(env)); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Encountered variable '" << variable.getName() << "' with unknown type while trying to create solver variables."); + } + variableToDeclarationMapping.insert(std::make_pair(variable, msatDeclaration)); + declarationToVariableMapping.insert(std::make_pair(msatDeclaration, variable)); + return msatDeclaration; + } + // The expression manager to use. storm::expressions::ExpressionManager& manager; // The MathSAT environment used. msat_env& env; - + // A mapping of variable names to their declaration in the MathSAT environment. std::unordered_map variableToDeclarationMapping; diff --git a/src/adapters/Z3ExpressionAdapter.h b/src/adapters/Z3ExpressionAdapter.h index 045261d05..bee1b42da 100644 --- a/src/adapters/Z3ExpressionAdapter.h +++ b/src/adapters/Z3ExpressionAdapter.h @@ -31,23 +31,7 @@ namespace storm { * 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(), variableToExpressionMapping() { - // Here, we need to create the mapping from all variables known to the manager to their z3 counterparts. - for (auto const& variableTypePair : manager) { - 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)); - } + // Intentionally left empty. } /*! @@ -57,8 +41,9 @@ namespace storm { * @return An equivalent expression for Z3. */ z3::expr translateExpression(storm::expressions::Expression const& expression) { + STORM_LOG_ASSERT(expression.getManager() == this->manager, "Invalid expression for solver."); z3::expr result = boost::any_cast(expression.getBaseExpression().accept(*this)); - + for (z3::expr const& assertion : additionalAssertions) { result = result && assertion; } @@ -74,8 +59,12 @@ namespace storm { * @return An equivalent expression for Z3. */ z3::expr translateExpression(storm::expressions::Variable const& variable) { + STORM_LOG_ASSERT(variable.getManager() == this->manager, "Invalid expression for solver."); + auto const& variableExpressionPair = variableToExpressionMapping.find(variable); - STORM_LOG_ASSERT(variableExpressionPair != variableToExpressionMapping.end(), "Unable to find variable."); + if (variableExpressionPair != variableToExpressionMapping.end()) { + return createVariable(variable); + } return variableExpressionPair->second; } @@ -101,7 +90,7 @@ namespace storm { case Z3_OP_EQ: return this->translateExpression(expr.arg(0)) == this->translateExpression(expr.arg(1)); case Z3_OP_ITE: - return this->translateExpression(expr.arg(0)).ite(this->translateExpression(expr.arg(1)), this->translateExpression(expr.arg(2))); + return storm::expressions::ite(this->translateExpression(expr.arg(0)), this->translateExpression(expr.arg(1)), this->translateExpression(expr.arg(2))); case Z3_OP_AND: { unsigned args = expr.num_args(); STORM_LOG_THROW(args != 0, storm::exceptions::ExpressionEvaluationException, "Failed to convert Z3 expression. 0-ary AND is assumed to be an error."); @@ -129,13 +118,13 @@ namespace storm { } } case Z3_OP_IFF: - return this->translateExpression(expr.arg(0)).iff(this->translateExpression(expr.arg(1))); + return storm::expressions::iff(this->translateExpression(expr.arg(0)), this->translateExpression(expr.arg(1))); case Z3_OP_XOR: return this->translateExpression(expr.arg(0)) ^ this->translateExpression(expr.arg(1)); case Z3_OP_NOT: return !this->translateExpression(expr.arg(0)); case Z3_OP_IMPLIES: - return this->translateExpression(expr.arg(0)).implies(this->translateExpression(expr.arg(1))); + return storm::expressions::implies(this->translateExpression(expr.arg(0)), this->translateExpression(expr.arg(1))); case Z3_OP_LE: return this->translateExpression(expr.arg(0)) <= this->translateExpression(expr.arg(1)); case Z3_OP_GE: @@ -307,10 +296,34 @@ namespace storm { } virtual boost::any visit(storm::expressions::VariableExpression const& expression) override { - return variableToExpressionMapping.at(expression.getVariable()); + return this->translateExpression(expression.getVariable()); } private: + /*! + * Creates a Z3 variable for the provided variable. + * + * @param variable The variable for which to create a Z3 counterpart. + */ + z3::expr createVariable(storm::expressions::Variable const& variable) { + z3::expr z3Variable(context); + if (variable.getType().isBooleanType()) { + z3Variable = context.bool_const(variable.getName().c_str()); + } else if (variable.getType().isUnboundedIntegralType()) { + z3Variable = context.int_const(variable.getName().c_str()); + } else if (variable.getType().isBoundedIntegralType()) { + z3Variable = context.bv_const(variable.getName().c_str(), variable.getType().getWidth()); + } else if (variable.getType().isRationalType()) { + z3Variable = context.real_const(variable.getName().c_str()); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Encountered variable '" << variable.getName() << "' with unknown type while trying to create solver variables."); + } + variableToExpressionMapping.insert(std::make_pair(variable, z3Variable)); + declarationToVariableMapping.insert(std::make_pair(z3Variable.decl(), variable)); + return z3Variable; + } + + // The manager that can be used to build expressions. storm::expressions::ExpressionManager& manager; diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h index 80ba611aa..a5518b58e 100644 --- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h +++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h @@ -476,13 +476,12 @@ namespace storm { solver->setModelSense(min ? storm::solver::LpSolver::ModelSense::Maximize : storm::solver::LpSolver::ModelSense::Minimize); // First, we need to create the variables for the problem. - std::map stateToVariableNameMap; + std::map stateToVariableMap; for (auto const& stateChoicesPair : mec) { std::string variableName = "x" + std::to_string(stateChoicesPair.first); - stateToVariableNameMap[stateChoicesPair.first] = variableName; - solver->addUnboundedContinuousVariable(variableName); + stateToVariableMap[stateChoicesPair.first] = solver->addUnboundedContinuousVariable(variableName); } - solver->addUnboundedContinuousVariable("k", 1); + storm::expressions::Variable k = solver->addUnboundedContinuousVariable("k", 1); solver->update(); // Now we encode the problem as constraints. @@ -491,14 +490,14 @@ namespace storm { // Now, based on the type of the state, create a suitable constraint. if (markovianStates.get(state)) { - storm::expressions::Expression constraint = storm::expressions::Expression::createDoubleVariable(stateToVariableNameMap.at(state)); + storm::expressions::Expression constraint = stateToVariableMap.at(state); for (auto element : transitionMatrix.getRow(nondeterministicChoiceIndices[state])) { - constraint = constraint - storm::expressions::Expression::createDoubleVariable(stateToVariableNameMap.at(element.getColumn())) * storm::expressions::Expression::createDoubleLiteral(element.getValue()); + constraint = constraint - stateToVariableMap.at(element.getColumn()) * solver->getConstant(element.getValue()); } - constraint = constraint + storm::expressions::Expression::createDoubleLiteral(storm::utility::constantOne() / exitRates[state]) * storm::expressions::Expression::createDoubleVariable("k"); - storm::expressions::Expression rightHandSide = goalStates.get(state) ? storm::expressions::Expression::createDoubleLiteral(storm::utility::constantOne() / exitRates[state]) : storm::expressions::Expression::createDoubleLiteral(storm::utility::constantZero()); + constraint = constraint + solver->getConstant(storm::utility::constantOne() / exitRates[state]) * k; + storm::expressions::Expression rightHandSide = goalStates.get(state) ? solver->getConstant(storm::utility::constantOne() / exitRates[state]) : solver->getConstant(0); if (min) { constraint = constraint <= rightHandSide; } else { @@ -509,13 +508,13 @@ namespace storm { // For probabilistic states, we want to add the constraint x_s <= sum P(s, a, s') * x_s' where a is the current action // and the sum ranges over all states s'. for (auto choice : stateChoicesPair.second) { - storm::expressions::Expression constraint = storm::expressions::Expression::createDoubleVariable(stateToVariableNameMap.at(state)); + storm::expressions::Expression constraint = stateToVariableMap.at(state); for (auto element : transitionMatrix.getRow(choice)) { - constraint = constraint - storm::expressions::Expression::createDoubleVariable(stateToVariableNameMap.at(element.getColumn())) * storm::expressions::Expression::createDoubleLiteral(element.getValue()); + constraint = constraint - stateToVariableMap.at(element.getColumn()) * solver->getConstant(element.getValue()); } - storm::expressions::Expression rightHandSide = storm::expressions::Expression::createDoubleLiteral(storm::utility::constantZero()); + storm::expressions::Expression rightHandSide = solver->getConstant(storm::utility::constantZero()); if (min) { constraint = constraint <= rightHandSide; } else { @@ -527,7 +526,7 @@ namespace storm { } solver->optimize(); - return solver->getContinuousValue("k"); + return solver->getContinuousValue(k); } /*! diff --git a/src/parser/ExpressionParser.cpp b/src/parser/ExpressionParser.cpp index 19ff25040..8733a4d83 100644 --- a/src/parser/ExpressionParser.cpp +++ b/src/parser/ExpressionParser.cpp @@ -93,7 +93,7 @@ namespace storm { storm::expressions::Expression ExpressionParser::createIteExpression(storm::expressions::Expression e1, storm::expressions::Expression e2, storm::expressions::Expression e3) const { if (this->createExpressions) { try { - return e1.ite(e2, e3); + return storm::expressions::ite(e1, e2, e3); } catch (storm::exceptions::InvalidTypeException const& e) { STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what()); } @@ -106,7 +106,7 @@ namespace storm { try { switch (operatorType) { case storm::expressions::OperatorType::Or: return e1 || e2; break; - case storm::expressions::OperatorType::Implies: return e1.implies(e2); break; + case storm::expressions::OperatorType::Implies: return storm::expressions::implies(e1, e2); break; default: STORM_LOG_ASSERT(false, "Invalid operation."); break; } } catch (storm::exceptions::InvalidTypeException const& e) { @@ -151,7 +151,7 @@ namespace storm { if (this->createExpressions) { try { switch (operatorType) { - case storm::expressions::OperatorType::Equal: return e1.hasBooleanReturnType() && e2.hasBooleanReturnType() ? e1.iff(e2) : e1 == e2; break; + case storm::expressions::OperatorType::Equal: return e1.hasBooleanType() && e2.hasBooleanType() ? storm::expressions::iff(e1, e2) : e1 == e2; break; case storm::expressions::OperatorType::NotEqual: return e1 != e2; break; default: STORM_LOG_ASSERT(false, "Invalid operation."); break; } @@ -250,8 +250,8 @@ namespace storm { if (this->createExpressions) { try { switch (operatorType) { - case storm::expressions::OperatorType::Min: return storm::expressions::Expression::minimum(e1, e2); break; - case storm::expressions::OperatorType::Max: return storm::expressions::Expression::maximum(e1, e2); break; + case storm::expressions::OperatorType::Min: return storm::expressions::minimum(e1, e2); break; + case storm::expressions::OperatorType::Max: return storm::expressions::maximum(e1, e2); break; default: STORM_LOG_ASSERT(false, "Invalid operation."); break; } } catch (storm::exceptions::InvalidTypeException const& e) { @@ -265,8 +265,8 @@ namespace storm { if (this->createExpressions) { try { switch (operatorType) { - case storm::expressions::OperatorType::Floor: return e1.floor(); break; - case storm::expressions::OperatorType::Ceil: return e1.ceil(); break; + case storm::expressions::OperatorType::Floor: return storm::expressions::floor(e1); break; + case storm::expressions::OperatorType::Ceil: return storm::expressions::ceil(e1); break; default: STORM_LOG_ASSERT(false, "Invalid operation."); break; } } catch (storm::exceptions::InvalidTypeException const& e) { diff --git a/src/solver/LpSolver.h b/src/solver/LpSolver.h index e83411cbb..46fd327fe 100644 --- a/src/solver/LpSolver.h +++ b/src/solver/LpSolver.h @@ -133,6 +133,16 @@ namespace storm { */ virtual storm::expressions::Variable addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient = 0) = 0; + /*! + * Retrieves an expression that characterizes the given constant value. + * + * @param value The value of the constant. + * @return The resulting expression. + */ + storm::expressions::Expression getConstant(double value) const { + return manager->rational(value); + } + /*! * Updates the model to make the variables that have been declared since the last call to update * usable. diff --git a/src/storage/dd/CuddDdManager.cpp b/src/storage/dd/CuddDdManager.cpp index 217903852..2a689ab13 100644 --- a/src/storage/dd/CuddDdManager.cpp +++ b/src/storage/dd/CuddDdManager.cpp @@ -198,26 +198,54 @@ namespace storm { std::vector DdManager::getDdVariableNames() const { // First, we initialize a list DD variables and their names. - std::vector> variableNamePairs; - for (auto const& nameMetaVariablePair : this->metaVariableMap) { - DdMetaVariable const& metaVariable = nameMetaVariablePair.second; + std::vector> variablePairs; + for (auto const& variablePair : this->metaVariableMap) { + DdMetaVariable const& metaVariable = variablePair.second; // If the meta variable is of type bool, we don't need to suffix it with the bit number. if (metaVariable.getType() == DdMetaVariable::MetaVariableType::Bool) { - variableNamePairs.emplace_back(metaVariable.getDdVariables().front().getCuddAdd(), metaVariable.getName()); + variablePairs.emplace_back(metaVariable.getDdVariables().front().getCuddAdd(), variablePair.first.getName()); } else { // For integer-valued meta variables, we, however, have to add the suffix. for (uint_fast64_t variableIndex = 0; variableIndex < metaVariable.getNumberOfDdVariables(); ++variableIndex) { - variableNamePairs.emplace_back(metaVariable.getDdVariables()[variableIndex].getCuddAdd(), metaVariable.getName() + "." + std::to_string(variableIndex)); + variablePairs.emplace_back(metaVariable.getDdVariables()[variableIndex].getCuddAdd(), variablePair.first.getName() + '.' + std::to_string(variableIndex)); } } } // Then, we sort this list according to the indices of the ADDs. - std::sort(variableNamePairs.begin(), variableNamePairs.end(), [](std::pair const& a, std::pair const& b) { return a.first.NodeReadIndex() < b.first.NodeReadIndex(); }); + std::sort(variablePairs.begin(), variablePairs.end(), [](std::pair const& a, std::pair const& b) { return a.first.NodeReadIndex() < b.first.NodeReadIndex(); }); // Now, we project the sorted vector to its second component. std::vector result; - for (auto const& element : variableNamePairs) { + for (auto const& element : variablePairs) { + result.push_back(element.second); + } + + return result; + } + + std::vector DdManager::getDdVariables() const { + // First, we initialize a list DD variables and their names. + std::vector> variablePairs; + for (auto const& variablePair : this->metaVariableMap) { + DdMetaVariable const& metaVariable = variablePair.second; + // If the meta variable is of type bool, we don't need to suffix it with the bit number. + if (metaVariable.getType() == DdMetaVariable::MetaVariableType::Bool) { + variablePairs.emplace_back(metaVariable.getDdVariables().front().getCuddAdd(), variablePair.first); + } else { + // For integer-valued meta variables, we, however, have to add the suffix. + for (uint_fast64_t variableIndex = 0; variableIndex < metaVariable.getNumberOfDdVariables(); ++variableIndex) { + variablePairs.emplace_back(metaVariable.getDdVariables()[variableIndex].getCuddAdd(), variablePair); + } + } + } + + // Then, we sort this list according to the indices of the ADDs. + std::sort(variablePairs.begin(), variablePairs.end(), [](std::pair const& a, std::pair const& b) { return a.first.NodeReadIndex() < b.first.NodeReadIndex(); }); + + // Now, we project the sorted vector to its second component. + std::vector result; + for (auto const& element : variablePairs) { result.push_back(element.second); } diff --git a/src/storage/expressions/BaseExpression.cpp b/src/storage/expressions/BaseExpression.cpp index 5685edd11..af5d5d96e 100644 --- a/src/storage/expressions/BaseExpression.cpp +++ b/src/storage/expressions/BaseExpression.cpp @@ -26,6 +26,10 @@ namespace storm { return this->getType().isBooleanType(); } + bool BaseExpression::hasRationalType() const { + return this->getType().isRationalType(); + } + int_fast64_t BaseExpression::evaluateAsInt(Valuation const* valuation) const { STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Unable to evaluate expression as integer."); } diff --git a/src/storage/expressions/BaseExpression.h b/src/storage/expressions/BaseExpression.h index 301cd861f..df30292cb 100644 --- a/src/storage/expressions/BaseExpression.h +++ b/src/storage/expressions/BaseExpression.h @@ -18,6 +18,7 @@ namespace storm { namespace expressions { // Forward-declare expression manager. class ExpressionManager; + class Variable; /*! * The base class of all expression classes. @@ -148,9 +149,9 @@ namespace storm { /*! * Retrieves the set of all variables that appear in the expression. * - * @return The set of all variables that appear in the expression. + * @param The set into which all variables in this expresson are inserted. */ - virtual std::set getVariables() const = 0; + virtual void gatherVariables(std::set& variables) const = 0; /*! * Simplifies the expression according to some simple rules. @@ -187,6 +188,13 @@ namespace storm { */ bool hasBooleanType() const; + /*! + * Retrieves whether the expression has a rational return type. + * + * @return True iff the expression has a rational return type. + */ + bool hasRationalType() const; + /*! * Retrieves a shared pointer to this expression. * diff --git a/src/storage/expressions/BinaryExpression.cpp b/src/storage/expressions/BinaryExpression.cpp index c03e7b718..c0976e56f 100644 --- a/src/storage/expressions/BinaryExpression.cpp +++ b/src/storage/expressions/BinaryExpression.cpp @@ -17,11 +17,9 @@ namespace storm { return this->getFirstOperand()->containsVariables() || this->getSecondOperand()->containsVariables(); } - std::set BinaryExpression::getVariables() const { - std::set firstVariableSet = this->getFirstOperand()->getVariables(); - std::set secondVariableSet = this->getSecondOperand()->getVariables(); - firstVariableSet.insert(secondVariableSet.begin(), secondVariableSet.end()); - return firstVariableSet; + void BinaryExpression::gatherVariables(std::set& variables) const { + this->getFirstOperand()->gatherVariables(variables); + this->getSecondOperand()->gatherVariables(variables); } std::shared_ptr const& BinaryExpression::getFirstOperand() const { diff --git a/src/storage/expressions/BinaryExpression.h b/src/storage/expressions/BinaryExpression.h index 69a61ab99..344a50182 100644 --- a/src/storage/expressions/BinaryExpression.h +++ b/src/storage/expressions/BinaryExpression.h @@ -35,7 +35,7 @@ namespace storm { virtual bool containsVariables() const override; virtual uint_fast64_t getArity() const override; virtual std::shared_ptr getOperand(uint_fast64_t operandIndex) const override; - virtual std::set getVariables() const override; + virtual void gatherVariables(std::set& variables) const override; /*! * Retrieves the first operand of the expression. diff --git a/src/storage/expressions/BooleanLiteralExpression.cpp b/src/storage/expressions/BooleanLiteralExpression.cpp index 195dc7aae..9847e4bb3 100644 --- a/src/storage/expressions/BooleanLiteralExpression.cpp +++ b/src/storage/expressions/BooleanLiteralExpression.cpp @@ -23,8 +23,8 @@ namespace storm { return this->getValue() == false; } - std::set BooleanLiteralExpression::getVariables() const { - return std::set(); + void BooleanLiteralExpression::gatherVariables(std::set& variables) const { + return; } std::shared_ptr BooleanLiteralExpression::simplify() const { diff --git a/src/storage/expressions/BooleanLiteralExpression.h b/src/storage/expressions/BooleanLiteralExpression.h index f382fed62..cb8f694e6 100644 --- a/src/storage/expressions/BooleanLiteralExpression.h +++ b/src/storage/expressions/BooleanLiteralExpression.h @@ -30,7 +30,7 @@ namespace storm { virtual bool isLiteral() const override; virtual bool isTrue() const override; virtual bool isFalse() const override; - virtual std::set getVariables() const override; + virtual void gatherVariables(std::set& variables) const override; virtual std::shared_ptr simplify() const override; virtual boost::any accept(ExpressionVisitor& visitor) const override; diff --git a/src/storage/expressions/DoubleLiteralExpression.cpp b/src/storage/expressions/DoubleLiteralExpression.cpp index 23bf0fc39..be878f0b2 100644 --- a/src/storage/expressions/DoubleLiteralExpression.cpp +++ b/src/storage/expressions/DoubleLiteralExpression.cpp @@ -15,8 +15,8 @@ namespace storm { return true; } - std::set DoubleLiteralExpression::getVariables() const { - return std::set(); + void DoubleLiteralExpression::gatherVariables(std::set& variables) const { + return; } std::shared_ptr DoubleLiteralExpression::simplify() const { diff --git a/src/storage/expressions/DoubleLiteralExpression.h b/src/storage/expressions/DoubleLiteralExpression.h index 9630dab9f..cb3114e2d 100644 --- a/src/storage/expressions/DoubleLiteralExpression.h +++ b/src/storage/expressions/DoubleLiteralExpression.h @@ -28,7 +28,7 @@ namespace storm { // Override base class methods. virtual double evaluateAsDouble(Valuation const* valuation = nullptr) const override; virtual bool isLiteral() const override; - virtual std::set getVariables() const override; + virtual void gatherVariables(std::set& variables) const override; virtual std::shared_ptr simplify() const override; virtual boost::any accept(ExpressionVisitor& visitor) const override; diff --git a/src/storage/expressions/Expression.cpp b/src/storage/expressions/Expression.cpp index 68d63df1c..7c46235bc 100644 --- a/src/storage/expressions/Expression.cpp +++ b/src/storage/expressions/Expression.cpp @@ -11,6 +11,17 @@ namespace storm { namespace expressions { + /*! + * Checks whether the two expressions share the same expression manager. + * + * @param a The first expression. + * @param b The second expression. + * @return True iff the expressions share the same manager. + */ + static void assertSameManager(BaseExpression const& a, BaseExpression const& b) { + STORM_LOG_THROW(a.getManager() == b.getManager(), storm::exceptions::InvalidArgumentException, "Expressions are managed by different manager."); + } + Expression::Expression(std::shared_ptr const& expressionPtr) : expressionPtr(expressionPtr) { // Intentionally left empty. } @@ -83,8 +94,10 @@ namespace storm { return this->getBaseExpression().isFalse(); } - std::set Expression::getVariables() const { - return this->getBaseExpression().getVariables(); + std::set Expression::getVariables() const { + std::set result; + this->getBaseExpression().gatherVariables(result); + return result; } bool Expression::isRelationalExpression() const { @@ -117,142 +130,142 @@ namespace storm { return this->getBaseExpression().getType(); } - bool Expression::hasNumericalReturnType() const { + bool Expression::hasNumericalType() const { return this->getBaseExpression().hasNumericalType(); } - bool Expression::hasBooleanReturnType() const { + bool Expression::hasRationalType() const { + return this->getBaseExpression().hasRationalType(); + } + + bool Expression::hasBooleanType() const { return this->getBaseExpression().hasBooleanType(); } - bool Expression::hasIntegralReturnType() const { + bool Expression::hasIntegralType() const { return this->getBaseExpression().hasIntegralType(); } - - Expression Expression::operator+(Expression const& other) const { - assertSameManager(this->getBaseExpression(), other.getBaseExpression()); - 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 { - assertSameManager(this->getBaseExpression(), other.getBaseExpression()); - return Expression(std::shared_ptr(new BinaryNumericalFunctionExpression(this->getBaseExpression().getManager(), this->getType().plusMinusTimes(other.getType()), this->getBaseExpressionPointer(), other.getBaseExpressionPointer(), BinaryNumericalFunctionExpression::OperatorType::Minus))); + boost::any Expression::accept(ExpressionVisitor& visitor) const { + return this->getBaseExpression().accept(visitor); } - Expression Expression::operator-() const { - return Expression(std::shared_ptr(new UnaryNumericalFunctionExpression(this->getBaseExpression().getManager(), this->getType(), this->getBaseExpressionPointer(), UnaryNumericalFunctionExpression::OperatorType::Minus))); + std::ostream& operator<<(std::ostream& stream, Expression const& expression) { + stream << expression.getBaseExpression(); + return stream; } - Expression Expression::operator*(Expression const& other) const { - assertSameManager(this->getBaseExpression(), other.getBaseExpression()); - return Expression(std::shared_ptr(new BinaryNumericalFunctionExpression(this->getBaseExpression().getManager(), this->getType().plusMinusTimes(other.getType()), this->getBaseExpressionPointer(), other.getBaseExpressionPointer(), BinaryNumericalFunctionExpression::OperatorType::Times))); + Expression operator+(Expression const& first, Expression const& second) { + assertSameManager(first.getBaseExpression(), second.getBaseExpression()); + return Expression(std::shared_ptr(new BinaryNumericalFunctionExpression(first.getManager(), first.getType().plusMinusTimes(second.getType()), first.getBaseExpressionPointer(), second.getBaseExpressionPointer(), BinaryNumericalFunctionExpression::OperatorType::Plus))); } - Expression Expression::operator/(Expression const& other) const { - assertSameManager(this->getBaseExpression(), other.getBaseExpression()); - return Expression(std::shared_ptr(new BinaryNumericalFunctionExpression(this->getBaseExpression().getManager(), this->getType().divide(other.getType()), this->getBaseExpressionPointer(), other.getBaseExpressionPointer(), BinaryNumericalFunctionExpression::OperatorType::Divide))); + Expression operator-(Expression const& first, Expression const& second) { + assertSameManager(first.getBaseExpression(), second.getBaseExpression()); + return Expression(std::shared_ptr(new BinaryNumericalFunctionExpression(first.getBaseExpression().getManager(), first.getType().plusMinusTimes(second.getType()), first.getBaseExpressionPointer(), second.getBaseExpressionPointer(), BinaryNumericalFunctionExpression::OperatorType::Minus))); } - Expression Expression::operator^(Expression const& other) const { - assertSameManager(this->getBaseExpression(), other.getBaseExpression()); - return Expression(std::shared_ptr(new BinaryNumericalFunctionExpression(this->getBaseExpression().getManager(), this->getType().power(other.getType()), this->getBaseExpressionPointer(), other.getBaseExpressionPointer(), BinaryNumericalFunctionExpression::OperatorType::Power))); + Expression operator-(Expression const& first) { + return Expression(std::shared_ptr(new UnaryNumericalFunctionExpression(first.getBaseExpression().getManager(), first.getType(), first.getBaseExpressionPointer(), UnaryNumericalFunctionExpression::OperatorType::Minus))); } - Expression Expression::operator&&(Expression const& other) const { - assertSameManager(this->getBaseExpression(), other.getBaseExpression()); - return Expression(std::shared_ptr(new BinaryBooleanFunctionExpression(this->getBaseExpression().getManager(), this->getType().logicalConnective(other.getType()), this->getBaseExpressionPointer(), other.getBaseExpressionPointer(), BinaryBooleanFunctionExpression::OperatorType::And))); + Expression operator*(Expression const& first, Expression const& second) { + assertSameManager(first.getBaseExpression(), second.getBaseExpression()); + return Expression(std::shared_ptr(new BinaryNumericalFunctionExpression(first.getBaseExpression().getManager(), first.getType().plusMinusTimes(second.getType()), first.getBaseExpressionPointer(), second.getBaseExpressionPointer(), BinaryNumericalFunctionExpression::OperatorType::Times))); } - Expression Expression::operator||(Expression const& other) const { - assertSameManager(this->getBaseExpression(), other.getBaseExpression()); - return Expression(std::shared_ptr(new BinaryBooleanFunctionExpression(this->getBaseExpression().getManager(), this->getType().logicalConnective(other.getType()), this->getBaseExpressionPointer(), other.getBaseExpressionPointer(), BinaryBooleanFunctionExpression::OperatorType::Or))); + Expression operator/(Expression const& first, Expression const& second) { + assertSameManager(first.getBaseExpression(), second.getBaseExpression()); + return Expression(std::shared_ptr(new BinaryNumericalFunctionExpression(first.getBaseExpression().getManager(), first.getType().divide(second.getType()), first.getBaseExpressionPointer(), second.getBaseExpressionPointer(), BinaryNumericalFunctionExpression::OperatorType::Divide))); } - Expression Expression::operator!() const { - return Expression(std::shared_ptr(new UnaryBooleanFunctionExpression(this->getBaseExpression().getManager(), this->getType().logicalConnective(), this->getBaseExpressionPointer(), UnaryBooleanFunctionExpression::OperatorType::Not))); + Expression operator^(Expression const& first, Expression const& second) { + assertSameManager(first.getBaseExpression(), second.getBaseExpression()); + return Expression(std::shared_ptr(new BinaryNumericalFunctionExpression(first.getBaseExpression().getManager(), first.getType().power(second.getType()), first.getBaseExpressionPointer(), second.getBaseExpressionPointer(), BinaryNumericalFunctionExpression::OperatorType::Power))); } - Expression Expression::operator==(Expression const& other) const { - assertSameManager(this->getBaseExpression(), other.getBaseExpression()); - return Expression(std::shared_ptr(new BinaryRelationExpression(this->getBaseExpression().getManager(), this->getType().numericalComparison(other.getType()), this->getBaseExpressionPointer(), other.getBaseExpressionPointer(), BinaryRelationExpression::RelationType::Equal))); + Expression operator&&(Expression const& first, Expression const& second) { + assertSameManager(first.getBaseExpression(), second.getBaseExpression()); + return Expression(std::shared_ptr(new BinaryBooleanFunctionExpression(first.getBaseExpression().getManager(), first.getType().logicalConnective(second.getType()), first.getBaseExpressionPointer(), second.getBaseExpressionPointer(), BinaryBooleanFunctionExpression::OperatorType::And))); } - Expression Expression::operator!=(Expression const& other) const { - assertSameManager(this->getBaseExpression(), other.getBaseExpression()); - if (this->hasNumericalReturnType() && other.hasNumericalReturnType()) { - return Expression(std::shared_ptr(new BinaryRelationExpression(this->getBaseExpression().getManager(), this->getType().numericalComparison(other.getType()), this->getBaseExpressionPointer(), other.getBaseExpressionPointer(), BinaryRelationExpression::RelationType::NotEqual))); - } else { - return Expression(std::shared_ptr(new BinaryBooleanFunctionExpression(this->getBaseExpression().getManager(), this->getType().logicalConnective(other.getType()), this->getBaseExpressionPointer(), other.getBaseExpressionPointer(), BinaryBooleanFunctionExpression::OperatorType::Xor))); - } + Expression operator||(Expression const& first, Expression const& second) { + assertSameManager(first.getBaseExpression(), second.getBaseExpression()); + return Expression(std::shared_ptr(new BinaryBooleanFunctionExpression(first.getBaseExpression().getManager(), first.getType().logicalConnective(second.getType()), first.getBaseExpressionPointer(), second.getBaseExpressionPointer(), BinaryBooleanFunctionExpression::OperatorType::Or))); } - Expression Expression::operator>(Expression const& other) const { - assertSameManager(this->getBaseExpression(), other.getBaseExpression()); - return Expression(std::shared_ptr(new BinaryRelationExpression(this->getBaseExpression().getManager(), this->getType().numericalComparison(other.getType()), this->getBaseExpressionPointer(), other.getBaseExpressionPointer(), BinaryRelationExpression::RelationType::Greater))); + Expression operator!(Expression const& first) { + return Expression(std::shared_ptr(new UnaryBooleanFunctionExpression(first.getBaseExpression().getManager(), first.getType().logicalConnective(), first.getBaseExpressionPointer(), UnaryBooleanFunctionExpression::OperatorType::Not))); } - Expression Expression::operator>=(Expression const& other) const { - assertSameManager(this->getBaseExpression(), other.getBaseExpression()); - return Expression(std::shared_ptr(new BinaryRelationExpression(this->getBaseExpression().getManager(), this->getType().numericalComparison(other.getType()), this->getBaseExpressionPointer(), other.getBaseExpressionPointer(), BinaryRelationExpression::RelationType::GreaterOrEqual))); + Expression operator==(Expression const& first, Expression const& second) { + assertSameManager(first.getBaseExpression(), second.getBaseExpression()); + return Expression(std::shared_ptr(new BinaryRelationExpression(first.getBaseExpression().getManager(), first.getType().numericalComparison(second.getType()), first.getBaseExpressionPointer(), second.getBaseExpressionPointer(), BinaryRelationExpression::RelationType::Equal))); } - Expression Expression::operator<(Expression const& other) const { - assertSameManager(this->getBaseExpression(), other.getBaseExpression()); - return Expression(std::shared_ptr(new BinaryRelationExpression(this->getBaseExpression().getManager(), this->getType().numericalComparison(other.getType()), this->getBaseExpressionPointer(), other.getBaseExpressionPointer(), BinaryRelationExpression::RelationType::Less))); + Expression operator!=(Expression const& first, Expression const& second) { + assertSameManager(first.getBaseExpression(), second.getBaseExpression()); + if (first.hasNumericalType() && second.hasNumericalType()) { + return Expression(std::shared_ptr(new BinaryRelationExpression(first.getBaseExpression().getManager(), first.getType().numericalComparison(second.getType()), first.getBaseExpressionPointer(), second.getBaseExpressionPointer(), BinaryRelationExpression::RelationType::NotEqual))); + } else { + return Expression(std::shared_ptr(new BinaryBooleanFunctionExpression(first.getBaseExpression().getManager(), first.getType().logicalConnective(second.getType()), first.getBaseExpressionPointer(), second.getBaseExpressionPointer(), BinaryBooleanFunctionExpression::OperatorType::Xor))); + } } - Expression Expression::operator<=(Expression const& other) const { - assertSameManager(this->getBaseExpression(), other.getBaseExpression()); - return Expression(std::shared_ptr(new BinaryRelationExpression(this->getBaseExpression().getManager(), this->getType().numericalComparison(other.getType()), this->getBaseExpressionPointer(), other.getBaseExpressionPointer(), BinaryRelationExpression::RelationType::LessOrEqual))); + Expression operator>(Expression const& first, Expression const& second) { + assertSameManager(first.getBaseExpression(), second.getBaseExpression()); + return Expression(std::shared_ptr(new BinaryRelationExpression(first.getBaseExpression().getManager(), first.getType().numericalComparison(second.getType()), first.getBaseExpressionPointer(), second.getBaseExpressionPointer(), BinaryRelationExpression::RelationType::Greater))); } - Expression Expression::minimum(Expression const& lhs, Expression const& rhs) { - assertSameManager(lhs.getBaseExpression(), rhs.getBaseExpression()); - return Expression(std::shared_ptr(new BinaryNumericalFunctionExpression(lhs.getBaseExpression().getManager(), lhs.getType().minimumMaximum(rhs.getType()), lhs.getBaseExpressionPointer(), rhs.getBaseExpressionPointer(), BinaryNumericalFunctionExpression::OperatorType::Min))); + Expression operator>=(Expression const& first, Expression const& second) { + assertSameManager(first.getBaseExpression(), second.getBaseExpression()); + return Expression(std::shared_ptr(new BinaryRelationExpression(first.getBaseExpression().getManager(), first.getType().numericalComparison(second.getType()), first.getBaseExpressionPointer(), second.getBaseExpressionPointer(), BinaryRelationExpression::RelationType::GreaterOrEqual))); } - Expression Expression::maximum(Expression const& lhs, Expression const& rhs) { - assertSameManager(lhs.getBaseExpression(), rhs.getBaseExpression()); - return Expression(std::shared_ptr(new BinaryNumericalFunctionExpression(lhs.getBaseExpression().getManager(), lhs.getType().minimumMaximum(rhs.getType()), lhs.getBaseExpressionPointer(), rhs.getBaseExpressionPointer(), BinaryNumericalFunctionExpression::OperatorType::Max))); + Expression operator<(Expression const& first, Expression const& second) { + assertSameManager(first.getBaseExpression(), second.getBaseExpression()); + return Expression(std::shared_ptr(new BinaryRelationExpression(first.getBaseExpression().getManager(), first.getType().numericalComparison(second.getType()), first.getBaseExpressionPointer(), second.getBaseExpressionPointer(), BinaryRelationExpression::RelationType::Less))); } - Expression Expression::ite(Expression const& thenExpression, Expression const& elseExpression) { - assertSameManager(this->getBaseExpression(), thenExpression.getBaseExpression()); - assertSameManager(thenExpression.getBaseExpression(), elseExpression.getBaseExpression()); - return Expression(std::shared_ptr(new IfThenElseExpression(this->getBaseExpression().getManager(), this->getType().ite(thenExpression.getType(), elseExpression.getType()), this->getBaseExpressionPointer(), thenExpression.getBaseExpressionPointer(), elseExpression.getBaseExpressionPointer()))); + Expression operator<=(Expression const& first, Expression const& second) { + assertSameManager(first.getBaseExpression(), second.getBaseExpression()); + return Expression(std::shared_ptr(new BinaryRelationExpression(first.getBaseExpression().getManager(), first.getType().numericalComparison(second.getType()), first.getBaseExpressionPointer(), second.getBaseExpressionPointer(), BinaryRelationExpression::RelationType::LessOrEqual))); } - - Expression Expression::implies(Expression const& other) const { - assertSameManager(this->getBaseExpression(), other.getBaseExpression()); - return Expression(std::shared_ptr(new BinaryBooleanFunctionExpression(this->getBaseExpression().getManager(), this->getType().logicalConnective(other.getType()), this->getBaseExpressionPointer(), other.getBaseExpressionPointer(), BinaryBooleanFunctionExpression::OperatorType::Implies))); + + Expression minimum(Expression const& first, Expression const& second) { + assertSameManager(first.getBaseExpression(), second.getBaseExpression()); + return Expression(std::shared_ptr(new BinaryNumericalFunctionExpression(first.getBaseExpression().getManager(), first.getType().minimumMaximum(second.getType()), first.getBaseExpressionPointer(), second.getBaseExpressionPointer(), BinaryNumericalFunctionExpression::OperatorType::Min))); } - Expression Expression::iff(Expression const& other) const { - assertSameManager(this->getBaseExpression(), other.getBaseExpression()); - return Expression(std::shared_ptr(new BinaryBooleanFunctionExpression(this->getBaseExpression().getManager(), this->getType().logicalConnective(other.getType()), this->getBaseExpressionPointer(), other.getBaseExpressionPointer(), BinaryBooleanFunctionExpression::OperatorType::Iff))); + Expression maximum(Expression const& first, Expression const& second) { + assertSameManager(first.getBaseExpression(), second.getBaseExpression()); + return Expression(std::shared_ptr(new BinaryNumericalFunctionExpression(first.getBaseExpression().getManager(), first.getType().minimumMaximum(second.getType()), first.getBaseExpressionPointer(), second.getBaseExpressionPointer(), BinaryNumericalFunctionExpression::OperatorType::Max))); } - Expression Expression::floor() const { - STORM_LOG_THROW(this->hasNumericalReturnType(), storm::exceptions::InvalidTypeException, "Operator 'floor' requires numerical operand."); - return Expression(std::shared_ptr(new UnaryNumericalFunctionExpression(this->getBaseExpression().getManager(), this->getType().floorCeil(), this->getBaseExpressionPointer(), UnaryNumericalFunctionExpression::OperatorType::Floor))); + Expression ite(Expression const& condition, Expression const& thenExpression, Expression const& elseExpression) { + assertSameManager(condition.getBaseExpression(), thenExpression.getBaseExpression()); + assertSameManager(thenExpression.getBaseExpression(), elseExpression.getBaseExpression()); + return Expression(std::shared_ptr(new IfThenElseExpression(condition.getBaseExpression().getManager(), condition.getType().ite(thenExpression.getType(), elseExpression.getType()), condition.getBaseExpressionPointer(), thenExpression.getBaseExpressionPointer(), elseExpression.getBaseExpressionPointer()))); } - Expression Expression::ceil() const { - STORM_LOG_THROW(this->hasNumericalReturnType(), storm::exceptions::InvalidTypeException, "Operator 'ceil' requires numerical operand."); - return Expression(std::shared_ptr(new UnaryNumericalFunctionExpression(this->getBaseExpression().getManager(), this->getType().floorCeil(), this->getBaseExpressionPointer(), UnaryNumericalFunctionExpression::OperatorType::Ceil))); + Expression implies(Expression const& first, Expression const& second) { + assertSameManager(first.getBaseExpression(), second.getBaseExpression()); + return Expression(std::shared_ptr(new BinaryBooleanFunctionExpression(first.getBaseExpression().getManager(), first.getType().logicalConnective(second.getType()), first.getBaseExpressionPointer(), second.getBaseExpressionPointer(), BinaryBooleanFunctionExpression::OperatorType::Implies))); } - boost::any Expression::accept(ExpressionVisitor& visitor) const { - return this->getBaseExpression().accept(visitor); + Expression iff(Expression const& first, Expression const& second) { + assertSameManager(first.getBaseExpression(), second.getBaseExpression()); + return Expression(std::shared_ptr(new BinaryBooleanFunctionExpression(first.getBaseExpression().getManager(), first.getType().logicalConnective(second.getType()), first.getBaseExpressionPointer(), second.getBaseExpressionPointer(), BinaryBooleanFunctionExpression::OperatorType::Iff))); } - void Expression::assertSameManager(BaseExpression const& a, BaseExpression const& b) { - STORM_LOG_THROW(a.getManager() == b.getManager(), storm::exceptions::InvalidArgumentException, "Expressions are managed by different manager."); + Expression floor(Expression const& first) { + STORM_LOG_THROW(first.hasNumericalType(), storm::exceptions::InvalidTypeException, "Operator 'floor' requires numerical operand."); + return Expression(std::shared_ptr(new UnaryNumericalFunctionExpression(first.getBaseExpression().getManager(), first.getType().floorCeil(), first.getBaseExpressionPointer(), UnaryNumericalFunctionExpression::OperatorType::Floor))); } - std::ostream& operator<<(std::ostream& stream, Expression const& expression) { - stream << expression.getBaseExpression(); - return stream; + Expression ceil(Expression const& first) { + STORM_LOG_THROW(first.hasNumericalType(), storm::exceptions::InvalidTypeException, "Operator 'ceil' requires numerical operand."); + return Expression(std::shared_ptr(new UnaryNumericalFunctionExpression(first.getBaseExpression().getManager(), first.getType().floorCeil(), first.getBaseExpressionPointer(), UnaryNumericalFunctionExpression::OperatorType::Ceil))); } } } diff --git a/src/storage/expressions/Expression.h b/src/storage/expressions/Expression.h index eef3cde9f..943440090 100644 --- a/src/storage/expressions/Expression.h +++ b/src/storage/expressions/Expression.h @@ -21,8 +21,39 @@ namespace storm { friend class Variable; template friend class SubstitutionVisitor; + friend Expression operator+(Expression const& first, Expression const& second); + friend Expression operator-(Expression const& first, Expression const& second); + friend Expression operator-(Expression const& first); + friend Expression operator*(Expression const& first, Expression const& second); + friend Expression operator/(Expression const& first, Expression const& second); + friend Expression operator^(Expression const& first, Expression const& second); + friend Expression operator&&(Expression const& first, Expression const& second); + friend Expression operator||(Expression const& first, Expression const& second); + friend Expression operator!(Expression const& first); + friend Expression operator==(Expression const& first, Expression const& second); + friend Expression operator!=(Expression const& first, Expression const& second); + friend Expression operator>(Expression const& first, Expression const& second); + friend Expression operator>=(Expression const& first, Expression const& second); + friend Expression operator<(Expression const& first, Expression const& second); + friend Expression operator<=(Expression const& first, Expression const& second); + friend Expression ite(Expression const& condition, Expression const& thenExpression, Expression const& elseExpression); + friend Expression implies(Expression const& first, Expression const& second); + friend Expression iff(Expression const& first, Expression const& second); + friend Expression floor(Expression const& first); + friend Expression ceil(Expression const& first); + friend Expression minimum(Expression const& first, Expression const& second); + friend Expression maximum(Expression const& first, Expression const& second); + + Expression() = default; + /*! + * Creates an expression representing the given variable. + * + * @param variable The variable to represent. + */ + Expression(Variable const& variable); + // Instantiate constructors and assignments with their default implementations. Expression(Expression const& other) = default; Expression& operator=(Expression const& other) = default; @@ -31,33 +62,6 @@ namespace storm { Expression& operator=(Expression&&) = default; #endif - // Provide operator overloads to conveniently construct new expressions from other expressions. - Expression operator+(Expression const& other) const; - Expression operator-(Expression const& other) const; - Expression operator-() const; - Expression operator*(Expression const& other) const; - Expression operator/(Expression const& other) const; - Expression operator^(Expression const& other) const; - Expression operator&&(Expression const& other) const; - Expression operator||(Expression const& other) const; - Expression operator!() const; - Expression operator==(Expression const& other) const; - Expression operator!=(Expression const& other) const; - Expression operator>(Expression const& other) const; - Expression operator>=(Expression const& other) const; - Expression operator<(Expression const& other) const; - Expression operator<=(Expression const& other) const; - - Expression ite(Expression const& thenExpression, Expression const& elseExpression); - Expression implies(Expression const& other) const; - Expression iff(Expression const& other) const; - - Expression floor() const; - Expression ceil() const; - - static Expression minimum(Expression const& lhs, Expression const& rhs); - static Expression maximum(Expression const& lhs, Expression const& rhs); - /*! * Substitutes all occurrences of the variables according to the given map. Note that this substitution is * done simultaneously, i.e., variables appearing in the expressions that were "plugged in" are not @@ -207,7 +211,7 @@ namespace storm { * * @return The set of all variables that appear in the expression. */ - std::set getVariables() const; + std::set getVariables() const; /*! * Retrieves the base expression underlying this expression object. Note that prior to calling this, the @@ -243,21 +247,28 @@ namespace storm { * * @return True iff the expression has a numerical return type. */ - bool hasNumericalReturnType() const; + bool hasNumericalType() const; + + /*! + * Retrieves whether the expression has a rational return type. + * + * @return True iff the expression has a rational return type. + */ + bool hasRationalType() const; /*! * Retrieves whether the expression has a boolean return type. * * @return True iff the expression has a boolean return type. */ - bool hasBooleanReturnType() const; + bool hasBooleanType() const; /*! * Retrieves whether the expression has an integral return type. * * @return True iff the expression has a integral return type. */ - bool hasIntegralReturnType() const; + bool hasIntegralType() const; /*! * Accepts the given visitor. @@ -275,29 +286,38 @@ namespace storm { * @param expressionPtr A pointer to the underlying base expression. */ Expression(std::shared_ptr const& expressionPtr); - - /*! - * Creates an expression representing the given variable. - * - * @param variable The variable to represent. - */ - Expression(Variable const& variable); - - /*! - * Checks whether the two expressions share the same expression manager. - * - * @param a The first expression. - * @param b The second expression. - * @return True iff the expressions share the same manager. - */ - static void assertSameManager(BaseExpression const& a, BaseExpression const& b); - + // A pointer to the underlying base expression. std::shared_ptr expressionPtr; // A pointer to the responsible manager. std::shared_ptr manager; }; + + // Provide operator overloads to conveniently construct new expressions from other expressions. + Expression operator+(Expression const& first, Expression const& second); + Expression operator-(Expression const& first, Expression const& second); + Expression operator-(Expression const& first); + Expression operator*(Expression const& first, Expression const& second); + Expression operator/(Expression const& first, Expression const& second); + Expression operator^(Expression const& first, Expression const& second); + Expression operator&&(Expression const& first, Expression const& second); + Expression operator||(Expression const& first, Expression const& second); + Expression operator!(Expression const& first); + Expression operator==(Expression const& first, Expression const& second); + Expression operator!=(Expression const& first, Expression const& second); + Expression operator>(Expression const& first, Expression const& second); + Expression operator>=(Expression const& first, Expression const& second); + Expression operator<(Expression const& first, Expression const& second); + Expression operator<=(Expression const& first, Expression const& second); + Expression ite(Expression const& condition, Expression const& thenExpression, Expression const& elseExpression); + Expression implies(Expression const& first, Expression const& second); + Expression iff(Expression const& first, Expression const& second); + Expression floor(Expression const& first); + Expression ceil(Expression const& first); + Expression minimum(Expression const& first, Expression const& second); + Expression maximum(Expression const& first, Expression const& second); + } } diff --git a/src/storage/expressions/ExpressionManager.cpp b/src/storage/expressions/ExpressionManager.cpp index 32c1cf8f6..bd5459ad8 100644 --- a/src/storage/expressions/ExpressionManager.cpp +++ b/src/storage/expressions/ExpressionManager.cpp @@ -100,6 +100,18 @@ namespace storm { STORM_LOG_THROW(!variableExists(name), storm::exceptions::InvalidArgumentException, "Variable with name '" << name << "' already exists."); return declareOrGetVariable(name, variableType); } + + Variable ExpressionManager::declareBooleanVariable(std::string const& name) { + return this->declareVariable(name, this->getBooleanType()); + } + + Variable ExpressionManager::declareIntegerVariable(std::string const& name) { + return this->declareVariable(name, this->getIntegerType()); + } + + Variable ExpressionManager::declareRationalVariable(std::string const& name) { + return this->declareVariable(name, this->getRationalType()); + } 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."); diff --git a/src/storage/expressions/ExpressionManager.h b/src/storage/expressions/ExpressionManager.h index bb313ff9c..2c89315b2 100644 --- a/src/storage/expressions/ExpressionManager.h +++ b/src/storage/expressions/ExpressionManager.h @@ -147,6 +147,33 @@ namespace storm { * @return The newly declared variable. */ Variable declareVariable(std::string const& name, storm::expressions::Type const& variableType); + + /*! + * Declares a new boolean 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. + * + * @param name The name of the variable. + * @return The newly declared variable. + */ + Variable declareBooleanVariable(std::string const& name); + + /*! + * Declares a new integer 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. + * + * @param name The name of the variable. + * @return The newly declared variable. + */ + Variable declareIntegerVariable(std::string const& name); + + /*! + * Declares a new rational variable with a name that must not yet exist and its corresponding type. Note that + * the name must not start with two underscores since these variables are reserved for internal use only. + * + * @param name The name of the variable. + * @return The newly declared variable. + */ + Variable declareRationalVariable(std::string const& name); /*! * Declares an auxiliary variable with a name that must not yet exist and its corresponding type. diff --git a/src/storage/expressions/IfThenElseExpression.cpp b/src/storage/expressions/IfThenElseExpression.cpp index 090a7cff4..f3e65a94f 100644 --- a/src/storage/expressions/IfThenElseExpression.cpp +++ b/src/storage/expressions/IfThenElseExpression.cpp @@ -63,13 +63,10 @@ namespace storm { } } - std::set IfThenElseExpression::getVariables() const { - std::set result = this->condition->getVariables(); - std::set tmp = this->thenExpression->getVariables(); - result.insert(tmp.begin(), tmp.end()); - tmp = this->elseExpression->getVariables(); - result.insert(tmp.begin(), tmp.end()); - return result; + void IfThenElseExpression::gatherVariables(std::set& variables) const { + this->condition->gatherVariables(variables); + this->thenExpression->gatherVariables(variables); + this->elseExpression->gatherVariables(variables); } std::shared_ptr IfThenElseExpression::simplify() const { diff --git a/src/storage/expressions/IfThenElseExpression.h b/src/storage/expressions/IfThenElseExpression.h index 2e39a99d9..45c6b7e21 100644 --- a/src/storage/expressions/IfThenElseExpression.h +++ b/src/storage/expressions/IfThenElseExpression.h @@ -36,7 +36,7 @@ namespace storm { virtual bool evaluateAsBool(Valuation const* valuation = nullptr) const override; virtual int_fast64_t evaluateAsInt(Valuation const* valuation = nullptr) const override; virtual double evaluateAsDouble(Valuation const* valuation = nullptr) const override; - virtual std::set getVariables() const override; + virtual void gatherVariables(std::set& variables) const override; virtual std::shared_ptr simplify() const override; virtual boost::any accept(ExpressionVisitor& visitor) const override; diff --git a/src/storage/expressions/IntegerLiteralExpression.cpp b/src/storage/expressions/IntegerLiteralExpression.cpp index bb50f26a3..f1050f70a 100644 --- a/src/storage/expressions/IntegerLiteralExpression.cpp +++ b/src/storage/expressions/IntegerLiteralExpression.cpp @@ -19,8 +19,8 @@ namespace storm { return true; } - std::set IntegerLiteralExpression::getVariables() const { - return std::set(); + void IntegerLiteralExpression::gatherVariables(std::set& variables) const { + return; } std::shared_ptr IntegerLiteralExpression::simplify() const { diff --git a/src/storage/expressions/IntegerLiteralExpression.h b/src/storage/expressions/IntegerLiteralExpression.h index 348ea06ed..61cbd351c 100644 --- a/src/storage/expressions/IntegerLiteralExpression.h +++ b/src/storage/expressions/IntegerLiteralExpression.h @@ -29,7 +29,7 @@ namespace storm { virtual int_fast64_t evaluateAsInt(Valuation const* valuation = nullptr) const override; virtual double evaluateAsDouble(Valuation const* valuation = nullptr) const override; virtual bool isLiteral() const override; - virtual std::set getVariables() const override; + virtual void gatherVariables(std::set& variables) const override; virtual std::shared_ptr simplify() const override; virtual boost::any accept(ExpressionVisitor& visitor) const override; diff --git a/src/storage/expressions/SimpleValuation.cpp b/src/storage/expressions/SimpleValuation.cpp index a79dcef6f..34ff6aae6 100644 --- a/src/storage/expressions/SimpleValuation.cpp +++ b/src/storage/expressions/SimpleValuation.cpp @@ -7,6 +7,10 @@ namespace storm { namespace expressions { + SimpleValuation::SimpleValuation() : Valuation(nullptr) { + // Intentionally left empty. + } + SimpleValuation::SimpleValuation(std::shared_ptr const& manager) : Valuation(manager), booleanValues(nullptr), integerValues(nullptr), rationalValues(nullptr) { if (this->getManager().getNumberOfBooleanVariables() > 0) { booleanValues = std::unique_ptr>(new std::vector(this->getManager().getNumberOfBooleanVariables())); diff --git a/src/storage/expressions/SimpleValuation.h b/src/storage/expressions/SimpleValuation.h index 2d8fff7a3..3e19fea8d 100644 --- a/src/storage/expressions/SimpleValuation.h +++ b/src/storage/expressions/SimpleValuation.h @@ -17,6 +17,11 @@ namespace storm { friend class SimpleValuationPointerHash; friend class SimpleValuationPointerLess; + /*! + * Creates an empty simple valuation that is associated to no manager and has no variables. + */ + SimpleValuation(); + /*! * Creates a new valuation over the non-auxiliary variables of the given manager. * diff --git a/src/storage/expressions/Type.cpp b/src/storage/expressions/Type.cpp index f9d0e4713..fcc683cd2 100644 --- a/src/storage/expressions/Type.cpp +++ b/src/storage/expressions/Type.cpp @@ -26,6 +26,11 @@ namespace storm { return "int"; } + BoundedIntegerType::BoundedIntegerType(std::size_t width) : width(width) { + // Intentionally left empty. + } + + uint64_t BoundedIntegerType::getMask() const { return BoundedIntegerType::mask; } diff --git a/src/storage/expressions/UnaryExpression.cpp b/src/storage/expressions/UnaryExpression.cpp index c51ef0703..1223368fd 100644 --- a/src/storage/expressions/UnaryExpression.cpp +++ b/src/storage/expressions/UnaryExpression.cpp @@ -17,8 +17,8 @@ namespace storm { return this->getOperand()->containsVariables(); } - std::set UnaryExpression::getVariables() const { - return this->getOperand()->getVariables(); + void UnaryExpression::gatherVariables(std::set& variables) const { + return; } std::shared_ptr const& UnaryExpression::getOperand() const { diff --git a/src/storage/expressions/UnaryExpression.h b/src/storage/expressions/UnaryExpression.h index fa5b54649..793077545 100644 --- a/src/storage/expressions/UnaryExpression.h +++ b/src/storage/expressions/UnaryExpression.h @@ -31,7 +31,7 @@ namespace storm { virtual bool containsVariables() const override; virtual uint_fast64_t getArity() const override; virtual std::shared_ptr getOperand(uint_fast64_t operandIndex) const override; - virtual std::set getVariables() const override; + virtual void gatherVariables(std::set& variables) const override; /*! * Retrieves the operand of the unary expression. diff --git a/src/storage/expressions/VariableExpression.cpp b/src/storage/expressions/VariableExpression.cpp index 19cdb8cd3..350abb8b9 100644 --- a/src/storage/expressions/VariableExpression.cpp +++ b/src/storage/expressions/VariableExpression.cpp @@ -53,8 +53,8 @@ namespace storm { return true; } - std::set VariableExpression::getVariables() const { - return {this->getVariableName()}; + void VariableExpression::gatherVariables(std::set& variables) const { + variables.insert(this->getVariable()); } std::shared_ptr VariableExpression::simplify() const { diff --git a/src/storage/expressions/VariableExpression.h b/src/storage/expressions/VariableExpression.h index 505900ebc..35cc6efab 100644 --- a/src/storage/expressions/VariableExpression.h +++ b/src/storage/expressions/VariableExpression.h @@ -33,7 +33,7 @@ namespace storm { virtual std::string const& getIdentifier() const override; virtual bool containsVariables() const override; virtual bool isVariable() const override; - virtual std::set getVariables() const override; + virtual void gatherVariables(std::set& variables) const override; virtual std::shared_ptr simplify() const override; virtual boost::any accept(ExpressionVisitor& visitor) const override; diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index a405d601b..ea7fcc3a1 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -20,14 +20,14 @@ namespace storm { storm::expressions::Expression newInitialExpression = manager->boolean(true); for (auto const& booleanVariable : this->getGlobalBooleanVariables()) { - newInitialExpression = newInitialExpression && booleanVariable.getExpression().iff(booleanVariable.getInitialValueExpression()); + newInitialExpression = newInitialExpression && storm::expressions::iff(booleanVariable.getExpression(), booleanVariable.getInitialValueExpression()); } for (auto const& integerVariable : this->getGlobalIntegerVariables()) { newInitialExpression = newInitialExpression && integerVariable.getExpression() == integerVariable.getInitialValueExpression(); } for (auto const& module : this->getModules()) { for (auto const& booleanVariable : module.getBooleanVariables()) { - newInitialExpression = newInitialExpression && booleanVariable.getExpression().iff(booleanVariable.getInitialValueExpression()); + newInitialExpression = newInitialExpression && storm::expressions::iff(booleanVariable.getExpression(), booleanVariable.getInitialValueExpression()); } for (auto const& integerVariable : module.getIntegerVariables()) { newInitialExpression = newInitialExpression && integerVariable.getExpression() == integerVariable.getInitialValueExpression(); @@ -345,151 +345,137 @@ namespace storm { void Program::checkValidity() const { // Start by checking the constant declarations. - std::set allIdentifiers; - std::set globalIdentifiers; - std::set constantNames; + std::set all; + std::set global; + std::set constants; for (auto const& constant : this->getConstants()) { - // Check for duplicate identifiers. - STORM_LOG_THROW(allIdentifiers.find(constant.getName()) == allIdentifiers.end(), storm::exceptions::WrongFormatException, "Error in " << constant.getFilename() << ", line " << constant.getLineNumber() << ": duplicate identifier '" << constant.getName() << "'."); - // Check defining expressions of defined constants. if (constant.isDefined()) { - std::set containedIdentifiers = constant.getExpression().getVariables(); - bool isValid = std::includes(constantNames.begin(), constantNames.end(), containedIdentifiers.begin(), containedIdentifiers.end()); + std::set containedVariables = constant.getExpression().getVariables(); + bool isValid = std::includes(constants.begin(), constants.end(), containedVariables.begin(), containedVariables.end()); STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << constant.getFilename() << ", line " << constant.getLineNumber() << ": defining expression refers to unknown identifiers."); } // Record the new identifier for future checks. - constantNames.insert(constant.getName()); - allIdentifiers.insert(constant.getName()); - globalIdentifiers.insert(constant.getName()); + constants.insert(constant.getExpressionVariable()); + all.insert(constant.getExpressionVariable()); + global.insert(constant.getExpressionVariable()); } // Now we check the variable declarations. We start with the global variables. - std::set variableNames; + std::set variables; for (auto const& variable : this->getGlobalBooleanVariables()) { - // Check for duplicate identifiers. - STORM_LOG_THROW(allIdentifiers.find(variable.getName()) == allIdentifiers.end(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": duplicate identifier '" << variable.getName() << "'."); - // Check the initial value of the variable. - std::set containedIdentifiers = variable.getInitialValueExpression().getVariables(); - bool isValid = std::includes(constantNames.begin(), constantNames.end(), containedIdentifiers.begin(), containedIdentifiers.end()); + std::set containedVariables = variable.getInitialValueExpression().getVariables(); + bool isValid = std::includes(constants.begin(), constants.end(), containedVariables.begin(), containedVariables.end()); STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants."); // Record the new identifier for future checks. - variableNames.insert(variable.getName()); - allIdentifiers.insert(variable.getName()); - globalIdentifiers.insert(variable.getName()); + variables.insert(variable.getExpressionVariable()); + all.insert(variable.getExpressionVariable()); + global.insert(variable.getExpressionVariable()); } for (auto const& variable : this->getGlobalIntegerVariables()) { - // Check for duplicate identifiers. - STORM_LOG_THROW(allIdentifiers.find(variable.getName()) == allIdentifiers.end(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": duplicate identifier '" << variable.getName() << "'."); - // Check that bound expressions of the range. - std::set containedIdentifiers = variable.getLowerBoundExpression().getVariables(); - bool isValid = std::includes(constantNames.begin(), constantNames.end(), containedIdentifiers.begin(), containedIdentifiers.end()); + std::set containedVariables = variable.getLowerBoundExpression().getVariables(); + bool isValid = std::includes(constants.begin(), constants.end(), containedVariables.begin(), containedVariables.end()); STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": lower bound expression refers to unknown constants."); - containedIdentifiers = variable.getLowerBoundExpression().getVariables(); - isValid = std::includes(constantNames.begin(), constantNames.end(), containedIdentifiers.begin(), containedIdentifiers.end()); + containedVariables = variable.getLowerBoundExpression().getVariables(); + isValid = std::includes(constants.begin(), constants.end(), containedVariables.begin(), containedVariables.end()); STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": upper bound expression refers to unknown constants."); // Check the initial value of the variable. - containedIdentifiers = variable.getInitialValueExpression().getVariables(); - isValid = std::includes(constantNames.begin(), constantNames.end(), containedIdentifiers.begin(), containedIdentifiers.end()); + containedVariables = variable.getInitialValueExpression().getVariables(); + isValid = std::includes(constants.begin(), constants.end(), containedVariables.begin(), containedVariables.end()); STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants."); // Record the new identifier for future checks. - variableNames.insert(variable.getName()); - allIdentifiers.insert(variable.getName()); - globalIdentifiers.insert(variable.getName()); + variables.insert(variable.getExpressionVariable()); + all.insert(variable.getExpressionVariable()); + global.insert(variable.getExpressionVariable()); } // Now go through the variables of the modules. for (auto const& module : this->getModules()) { for (auto const& variable : module.getBooleanVariables()) { - // Check for duplicate identifiers. - STORM_LOG_THROW(allIdentifiers.find(variable.getName()) == allIdentifiers.end(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": duplicate identifier '" << variable.getName() << "'."); - // Check the initial value of the variable. - std::set containedIdentifiers = variable.getInitialValueExpression().getVariables(); - bool isValid = std::includes(constantNames.begin(), constantNames.end(), containedIdentifiers.begin(), containedIdentifiers.end()); + std::set containedVariables = variable.getInitialValueExpression().getVariables(); + bool isValid = std::includes(constants.begin(), constants.end(), containedVariables.begin(), containedVariables.end()); STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants."); // Record the new identifier for future checks. - variableNames.insert(variable.getName()); - allIdentifiers.insert(variable.getName()); + variables.insert(variable.getExpressionVariable()); + all.insert(variable.getExpressionVariable()); } for (auto const& variable : module.getIntegerVariables()) { - // Check for duplicate identifiers. - STORM_LOG_THROW(allIdentifiers.find(variable.getName()) == allIdentifiers.end(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": duplicate identifier '" << variable.getName() << "'."); - // Check that bound expressions of the range. - std::set containedIdentifiers = variable.getLowerBoundExpression().getVariables(); - bool isValid = std::includes(constantNames.begin(), constantNames.end(), containedIdentifiers.begin(), containedIdentifiers.end()); + std::set containedVariables = variable.getLowerBoundExpression().getVariables(); + bool isValid = std::includes(constants.begin(), constants.end(), containedVariables.begin(), containedVariables.end()); STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": lower bound expression refers to unknown constants."); - containedIdentifiers = variable.getLowerBoundExpression().getVariables(); - isValid = std::includes(constantNames.begin(), constantNames.end(), containedIdentifiers.begin(), containedIdentifiers.end()); + containedVariables = variable.getLowerBoundExpression().getVariables(); + isValid = std::includes(constants.begin(), constants.end(), containedVariables.begin(), containedVariables.end()); STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": upper bound expression refers to unknown constants."); // Check the initial value of the variable. - containedIdentifiers = variable.getInitialValueExpression().getVariables(); - isValid = std::includes(constantNames.begin(), constantNames.end(), containedIdentifiers.begin(), containedIdentifiers.end()); + containedVariables = variable.getInitialValueExpression().getVariables(); + isValid = std::includes(constants.begin(), constants.end(), containedVariables.begin(), containedVariables.end()); STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants."); // Record the new identifier for future checks. - variableNames.insert(variable.getName()); - allIdentifiers.insert(variable.getName()); + variables.insert(variable.getExpressionVariable()); + all.insert(variable.getExpressionVariable()); } } // Create the set of valid identifiers for future checks. - std::set variablesAndConstants; - std::set_union(variableNames.begin(), variableNames.end(), constantNames.begin(), constantNames.end(), std::inserter(variablesAndConstants, variablesAndConstants.begin())); + std::set variablesAndConstants; + std::set_union(variables.begin(), variables.end(), constants.begin(), constants.end(), std::inserter(variablesAndConstants, variablesAndConstants.begin())); // Check the commands of the modules. for (auto const& module : this->getModules()) { - std::set legalIdentifiers = globalIdentifiers; + std::set legalVariables = global; for (auto const& variable : module.getBooleanVariables()) { - legalIdentifiers.insert(variable.getName()); + legalVariables.insert(variable.getExpressionVariable()); } for (auto const& variable : module.getIntegerVariables()) { - legalIdentifiers.insert(variable.getName()); + legalVariables.insert(variable.getExpressionVariable()); } for (auto const& command : module.getCommands()) { // Check the guard. - std::set containedIdentifiers = command.getGuardExpression().getVariables(); - bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end()); + std::set containedVariables = command.getGuardExpression().getVariables(); + bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end()); STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": guard refers to unknown identifiers."); - STORM_LOG_THROW(command.getGuardExpression().hasBooleanReturnType(), storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": expression for guard must evaluate to type 'bool'."); + STORM_LOG_THROW(command.getGuardExpression().hasBooleanType(), storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": expression for guard must evaluate to type 'bool'."); // Check all updates. for (auto const& update : command.getUpdates()) { - containedIdentifiers = update.getLikelihoodExpression().getVariables(); - isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end()); + containedVariables = update.getLikelihoodExpression().getVariables(); + isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end()); STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": likelihood expression refers to unknown identifiers."); // Check all assignments. - std::set alreadyAssignedIdentifiers; + std::set alreadyAssignedVariables; for (auto const& assignment : update.getAssignments()) { - if (legalIdentifiers.find(assignment.getVariableName()) == legalIdentifiers.end()) { - if (allIdentifiers.find(assignment.getVariableName()) != allIdentifiers.end()) { + storm::expressions::Variable assignedVariable = manager->getVariable(assignment.getVariableName()); + if (legalVariables.find(assignedVariable) == legalVariables.end()) { + if (all.find(assignedVariable) != all.end()) { STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": assignment illegally refers to variable '" << assignment.getVariableName() << "'."); } else { STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": assignment refers to unknown variable '" << assignment.getVariableName() << "'."); } } - STORM_LOG_THROW(alreadyAssignedIdentifiers.find(assignment.getVariableName()) == alreadyAssignedIdentifiers.end(), storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": duplicate assignment to variable '" << assignment.getVariableName() << "'."); - STORM_LOG_THROW(manager->getVariable(assignment.getVariableName()).getType() == assignment.getExpression().getType(), storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": illegally assigning a value of type '" << assignment.getExpression().getType() << "' to variable '" << assignment.getVariableName() << "' of type '" << manager->getVariable(assignment.getVariableName()).getType() << "'."); + STORM_LOG_THROW(alreadyAssignedVariables.find(assignedVariable) == alreadyAssignedVariables.end(), storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": duplicate assignment to variable '" << assignment.getVariableName() << "'."); + STORM_LOG_THROW(assignedVariable.getType() == assignment.getExpression().getType(), storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": illegally assigning a value of type '" << assignment.getExpression().getType() << "' to variable '" << assignment.getVariableName() << "' of type '" << assignedVariable.getType() << "'."); - containedIdentifiers = assignment.getExpression().getVariables(); - isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end()); + containedVariables = assignment.getExpression().getVariables(); + isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end()); STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": likelihood expression refers to unknown identifiers."); // Add the current variable to the set of assigned variables (of this update). - alreadyAssignedIdentifiers.insert(assignment.getVariableName()); + alreadyAssignedVariables.insert(assignedVariable); } } } @@ -498,57 +484,48 @@ namespace storm { // Now check the reward models. for (auto const& rewardModel : this->getRewardModels()) { for (auto const& stateReward : rewardModel.getStateRewards()) { - std::set containedIdentifiers = stateReward.getStatePredicateExpression().getVariables(); - bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end()); + std::set containedVariables = stateReward.getStatePredicateExpression().getVariables(); + bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end()); STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << stateReward.getFilename() << ", line " << stateReward.getLineNumber() << ": state reward expression refers to unknown identifiers."); - STORM_LOG_THROW(stateReward.getStatePredicateExpression().hasBooleanReturnType(), storm::exceptions::WrongFormatException, "Error in " << stateReward.getFilename() << ", line " << stateReward.getLineNumber() << ": state predicate must evaluate to type 'bool'."); + STORM_LOG_THROW(stateReward.getStatePredicateExpression().hasBooleanType(), storm::exceptions::WrongFormatException, "Error in " << stateReward.getFilename() << ", line " << stateReward.getLineNumber() << ": state predicate must evaluate to type 'bool'."); - containedIdentifiers = stateReward.getRewardValueExpression().getVariables(); - isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end()); + containedVariables = stateReward.getRewardValueExpression().getVariables(); + isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end()); STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << stateReward.getFilename() << ", line " << stateReward.getLineNumber() << ": state reward value expression refers to unknown identifiers."); - STORM_LOG_THROW(stateReward.getRewardValueExpression().hasNumericalReturnType(), storm::exceptions::WrongFormatException, "Error in " << stateReward.getFilename() << ", line " << stateReward.getLineNumber() << ": reward value expression must evaluate to numerical type."); + STORM_LOG_THROW(stateReward.getRewardValueExpression().hasNumericalType(), storm::exceptions::WrongFormatException, "Error in " << stateReward.getFilename() << ", line " << stateReward.getLineNumber() << ": reward value expression must evaluate to numerical type."); } for (auto const& transitionReward : rewardModel.getTransitionRewards()) { - std::set containedIdentifiers = transitionReward.getStatePredicateExpression().getVariables(); - bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end()); + std::set containedVariables = transitionReward.getStatePredicateExpression().getVariables(); + bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end()); STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << transitionReward.getFilename() << ", line " << transitionReward.getLineNumber() << ": state reward expression refers to unknown identifiers."); - STORM_LOG_THROW(transitionReward.getStatePredicateExpression().hasBooleanReturnType(), storm::exceptions::WrongFormatException, "Error in " << transitionReward.getFilename() << ", line " << transitionReward.getLineNumber() << ": state predicate must evaluate to type 'bool'."); + STORM_LOG_THROW(transitionReward.getStatePredicateExpression().hasBooleanType(), storm::exceptions::WrongFormatException, "Error in " << transitionReward.getFilename() << ", line " << transitionReward.getLineNumber() << ": state predicate must evaluate to type 'bool'."); - containedIdentifiers = transitionReward.getRewardValueExpression().getVariables(); - isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end()); + containedVariables = transitionReward.getRewardValueExpression().getVariables(); + isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end()); STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << transitionReward.getFilename() << ", line " << transitionReward.getLineNumber() << ": state reward value expression refers to unknown identifiers."); - STORM_LOG_THROW(transitionReward.getRewardValueExpression().hasNumericalReturnType(), storm::exceptions::WrongFormatException, "Error in " << transitionReward.getFilename() << ", line " << transitionReward.getLineNumber() << ": reward value expression must evaluate to numerical type."); + STORM_LOG_THROW(transitionReward.getRewardValueExpression().hasNumericalType(), storm::exceptions::WrongFormatException, "Error in " << transitionReward.getFilename() << ", line " << transitionReward.getLineNumber() << ": reward value expression must evaluate to numerical type."); } } // Check the initial states expression. - std::set containedIdentifiers = this->getInitialConstruct().getInitialStatesExpression().getVariables(); + std::set containedIdentifiers = this->getInitialConstruct().getInitialStatesExpression().getVariables(); bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end()); STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << this->getInitialConstruct().getFilename() << ", line " << this->getInitialConstruct().getLineNumber() << ": initial expression refers to unknown identifiers."); // Check the labels. for (auto const& label : this->getLabels()) { - // Check for duplicate identifiers. - STORM_LOG_THROW(allIdentifiers.find(label.getName()) == allIdentifiers.end(), storm::exceptions::WrongFormatException, "Error in " << label.getFilename() << ", line " << label.getLineNumber() << ": duplicate identifier '" << label.getName() << "'."); - - std::set containedIdentifiers = label.getStatePredicateExpression().getVariables(); - bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end()); + std::set containedVariables = label.getStatePredicateExpression().getVariables(); + bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end()); STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << label.getFilename() << ", line " << label.getLineNumber() << ": label expression refers to unknown identifiers."); - STORM_LOG_THROW(label.getStatePredicateExpression().hasBooleanReturnType(), storm::exceptions::WrongFormatException, "Error in " << label.getFilename() << ", line " << label.getLineNumber() << ": label predicate must evaluate to type 'bool'."); + STORM_LOG_THROW(label.getStatePredicateExpression().hasBooleanType(), storm::exceptions::WrongFormatException, "Error in " << label.getFilename() << ", line " << label.getLineNumber() << ": label predicate must evaluate to type 'bool'."); } // Check the formulas. for (auto const& formula : this->getFormulas()) { - // Check for duplicate identifiers. - STORM_LOG_THROW(allIdentifiers.find(formula.getName()) == allIdentifiers.end(), storm::exceptions::WrongFormatException, "Error in " << formula.getFilename() << ", line " << formula.getLineNumber() << ": duplicate identifier '" << formula.getName() << "'."); - - std::set containedIdentifiers = formula.getExpression().getVariables(); - bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end()); + std::set containedVariables = formula.getExpression().getVariables(); + bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end()); STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << formula.getFilename() << ", line " << formula.getLineNumber() << ": formula expression refers to unknown identifiers."); - - // Record the new identifier for future checks. - allIdentifiers.insert(formula.getName()); } } diff --git a/test/functional/adapter/MathsatExpressionAdapterTest.cpp b/test/functional/adapter/MathsatExpressionAdapterTest.cpp index b59100a17..154bf0716 100644 --- a/test/functional/adapter/MathsatExpressionAdapterTest.cpp +++ b/test/functional/adapter/MathsatExpressionAdapterTest.cpp @@ -12,10 +12,10 @@ TEST(MathsatExpressionAdapter, StormToMathsatBasic) { ASSERT_FALSE(MSAT_ERROR_ENV(env)); msat_destroy_config(config); - storm::adapters::MathsatExpressionAdapter adapter(env); - storm::adapters::MathsatExpressionAdapter adapter2(env, false); + std::shared_ptr manager(new storm::expressions::ExpressionManager()); + storm::adapters::MathsatExpressionAdapter adapter(*manager, env); - storm::expressions::Expression exprTrue = storm::expressions::Expression::createTrue(); + storm::expressions::Expression exprTrue = manager->boolean(true); msat_term msatTrue = msat_make_true(env); msat_term conjecture; ASSERT_NO_THROW(conjecture = msat_make_not(env, msat_make_iff(env, msatTrue, adapter.translateExpression(exprTrue)))); @@ -23,24 +23,24 @@ TEST(MathsatExpressionAdapter, StormToMathsatBasic) { ASSERT_TRUE(msat_solve(env) == msat_result::MSAT_UNSAT); msat_reset_env(env); - storm::expressions::Expression exprFalse = storm::expressions::Expression::createFalse(); + storm::expressions::Expression exprFalse = manager->boolean(false); msat_term msatFalse = msat_make_false(env); ASSERT_NO_THROW(conjecture = msat_make_not(env, msat_make_iff(env, adapter.translateExpression(exprFalse), msatFalse))); msat_assert_formula(env, conjecture); ASSERT_TRUE(msat_solve(env) == msat_result::MSAT_UNSAT); msat_reset_env(env); - storm::expressions::Expression exprConjunction = (storm::expressions::Expression::createBooleanVariable("x") && storm::expressions::Expression::createBooleanVariable("y")); + storm::expressions::Variable x = manager->declareBooleanVariable("x"); + storm::expressions::Variable y = manager->declareBooleanVariable("y"); + storm::expressions::Expression exprConjunction = x && y; msat_term msatConjunction = msat_make_and(env, msat_make_constant(env, msat_declare_function(env, "x", msat_get_bool_type(env))), msat_make_constant(env, msat_declare_function(env, "y", msat_get_bool_type(env)))); - // Variables not yet created in adapter. - ASSERT_THROW(adapter2.translateExpression(exprConjunction), storm::exceptions::InvalidArgumentException); ASSERT_NO_THROW(conjecture = msat_make_not(env, msat_make_iff(env, adapter.translateExpression(exprConjunction), msatConjunction))); msat_assert_formula(env, conjecture); ASSERT_TRUE(msat_solve(env) == msat_result::MSAT_UNSAT); msat_reset_env(env); - storm::expressions::Expression exprNor = !(storm::expressions::Expression::createBooleanVariable("x") || storm::expressions::Expression::createBooleanVariable("y")); + storm::expressions::Expression exprNor = !(x || y); msat_term msatNor = msat_make_not(env, msat_make_or(env, msat_make_constant(env, msat_declare_function(env, "x", msat_get_bool_type(env))), msat_make_constant(env, msat_declare_function(env, "y", msat_get_bool_type(env))))); ASSERT_NO_THROW(adapter.translateExpression(exprNor)); // Variables already created in adapter. ASSERT_NO_THROW(conjecture = msat_make_not(env, msat_make_iff(env, adapter.translateExpression(exprNor), msatNor))); @@ -55,15 +55,19 @@ TEST(MathsatExpressionAdapter, StormToMathsatInteger) { ASSERT_FALSE(MSAT_ERROR_ENV(env)); msat_destroy_config(config); - storm::adapters::MathsatExpressionAdapter adapter(env); + std::shared_ptr manager(new storm::expressions::ExpressionManager()); + storm::adapters::MathsatExpressionAdapter adapter(*manager, env); - storm::expressions::Expression exprAdd = (storm::expressions::Expression::createIntegerVariable("x") + storm::expressions::Expression::createIntegerVariable("y") < -storm::expressions::Expression::createIntegerVariable("y")); + storm::expressions::Variable x = manager->declareIntegerVariable("x"); + storm::expressions::Variable y = manager->declareIntegerVariable("y"); + + storm::expressions::Expression exprAdd = x + y < -y; msat_decl xDecl = msat_declare_function(env, "x", msat_get_integer_type(env)); - msat_term x = msat_make_constant(env, xDecl); + msat_term xVar = msat_make_constant(env, xDecl); msat_decl yDecl = msat_declare_function(env, "y", msat_get_integer_type(env)); - msat_term y = msat_make_constant(env, yDecl); - msat_term minusY = msat_make_times(env, msat_make_number(env, "-1"), y); - msat_term msatAdd = msat_make_plus(env, x, y); + msat_term yVar = msat_make_constant(env, yDecl); + msat_term minusY = msat_make_times(env, msat_make_number(env, "-1"), yVar); + msat_term msatAdd = msat_make_plus(env, xVar, yVar); msat_term msatLess = msat_make_and(env, msat_make_leq(env, msatAdd, minusY), msat_make_not(env, msat_make_equal(env, msatAdd, minusY))); msat_term conjecture; ASSERT_NO_THROW(conjecture = msat_make_not(env, msat_make_iff(env, adapter.translateExpression(exprAdd), msatLess))); @@ -71,9 +75,9 @@ TEST(MathsatExpressionAdapter, StormToMathsatInteger) { ASSERT_TRUE(msat_solve(env) == msat_result::MSAT_UNSAT); msat_reset_env(env); - storm::expressions::Expression exprMult = !(storm::expressions::Expression::createIntegerVariable("x") * storm::expressions::Expression::createIntegerVariable("y") == storm::expressions::Expression::createIntegerVariable("y")); - msat_term msatTimes = msat_make_times(env, x, y); - msat_term msatNotEqual = msat_make_not(env, msat_make_equal(env, msatTimes, y)); + storm::expressions::Expression exprMult = !(x * y == y); + msat_term msatTimes = msat_make_times(env, xVar, yVar); + msat_term msatNotEqual = msat_make_not(env, msat_make_equal(env, msatTimes, yVar)); ASSERT_NO_THROW(conjecture = msat_make_not(env, msat_make_iff(env, adapter.translateExpression(exprMult), msatNotEqual))); msat_assert_formula(env, conjecture); ASSERT_TRUE(msat_solve(env) == msat_result::MSAT_UNSAT); @@ -86,15 +90,19 @@ TEST(MathsatExpressionAdapter, StormToMathsatReal) { ASSERT_FALSE(MSAT_ERROR_ENV(env)); msat_destroy_config(config); - storm::adapters::MathsatExpressionAdapter adapter(env); + std::shared_ptr manager(new storm::expressions::ExpressionManager()); + storm::adapters::MathsatExpressionAdapter adapter(*manager, env); - storm::expressions::Expression exprAdd = (storm::expressions::Expression::createDoubleVariable("x") + storm::expressions::Expression::createDoubleVariable("y") < -storm::expressions::Expression::createDoubleVariable("y")); + storm::expressions::Variable x = manager->declareRationalVariable("x"); + storm::expressions::Variable y = manager->declareRationalVariable("y"); + + storm::expressions::Expression exprAdd = x + y < -y; msat_decl xDecl = msat_declare_function(env, "x", msat_get_rational_type(env)); - msat_term x = msat_make_constant(env, xDecl); + msat_term xVar = msat_make_constant(env, xDecl); msat_decl yDecl = msat_declare_function(env, "y", msat_get_rational_type(env)); - msat_term y = msat_make_constant(env, yDecl); - msat_term minusY = msat_make_times(env, msat_make_number(env, "-1"), y); - msat_term msatAdd = msat_make_plus(env, x, y); + msat_term yVar = msat_make_constant(env, yDecl); + msat_term minusY = msat_make_times(env, msat_make_number(env, "-1"), yVar); + msat_term msatAdd = msat_make_plus(env, xVar, yVar); msat_term msatLess = msat_make_and(env, msat_make_leq(env, msatAdd, minusY), msat_make_not(env, msat_make_equal(env, msatAdd, minusY))); msat_term conjecture; ASSERT_NO_THROW(conjecture = msat_make_not(env, msat_make_iff(env, adapter.translateExpression(exprAdd), msatLess))); @@ -102,9 +110,9 @@ TEST(MathsatExpressionAdapter, StormToMathsatReal) { ASSERT_TRUE(msat_solve(env) == msat_result::MSAT_UNSAT); msat_reset_env(env); - storm::expressions::Expression exprMult = !(storm::expressions::Expression::createDoubleVariable("x") * storm::expressions::Expression::createDoubleVariable("y") == storm::expressions::Expression::createDoubleVariable("y")); - msat_term msatTimes = msat_make_times(env, x, y); - msat_term msatNotEqual = msat_make_not(env, msat_make_equal(env, msatTimes, y)); + storm::expressions::Expression exprMult = !(x * y == y); + msat_term msatTimes = msat_make_times(env, xVar, yVar); + msat_term msatNotEqual = msat_make_not(env, msat_make_equal(env, msatTimes, yVar)); ASSERT_NO_THROW(conjecture = msat_make_not(env, msat_make_iff(env, adapter.translateExpression(exprMult), msatNotEqual))); msat_assert_formula(env, conjecture); ASSERT_TRUE(msat_solve(env) == msat_result::MSAT_UNSAT); @@ -117,13 +125,16 @@ TEST(MathsatExpressionAdapter, StormToMathsatFloorCeil) { ASSERT_FALSE(MSAT_ERROR_ENV(env)); msat_destroy_config(config); - storm::adapters::MathsatExpressionAdapter adapter(env); + std::shared_ptr manager(new storm::expressions::ExpressionManager()); + storm::adapters::MathsatExpressionAdapter adapter(*manager, env); - storm::expressions::Expression exprFloor = ((storm::expressions::Expression::createDoubleVariable("d").floor()) == storm::expressions::Expression::createIntegerVariable("i") && storm::expressions::Expression::createDoubleVariable("d") > storm::expressions::Expression::createDoubleLiteral(4.1) && storm::expressions::Expression::createDoubleVariable("d") < storm::expressions::Expression::createDoubleLiteral(4.991)); + storm::expressions::Variable d = manager->declareRationalVariable("d"); + storm::expressions::Variable i = manager->declareIntegerVariable("d"); + storm::expressions::Expression exprFloor = storm::expressions::floor(d) == i && d > manager->rational(4.1) && d < manager->rational(4.991); msat_decl iDecl = msat_declare_function(env, "i", msat_get_integer_type(env)); - msat_term i = msat_make_constant(env, iDecl); - msat_term msatEqualsFour = msat_make_equal(env, msat_make_number(env, "4"), i); + msat_term iVar = msat_make_constant(env, iDecl); + msat_term msatEqualsFour = msat_make_equal(env, msat_make_number(env, "4"), iVar); msat_term conjecture; msat_term translatedExpr = adapter.translateExpression(exprFloor); msat_term msatIff = msat_make_iff(env, translatedExpr, msatEqualsFour); @@ -140,8 +151,8 @@ TEST(MathsatExpressionAdapter, StormToMathsatFloorCeil) { ASSERT_TRUE(msat_solve(env) == msat_result::MSAT_UNSAT); msat_reset_env(env); - storm::expressions::Expression exprCeil = ((storm::expressions::Expression::createDoubleVariable("d").ceil()) == storm::expressions::Expression::createIntegerVariable("i") && storm::expressions::Expression::createDoubleVariable("d") > storm::expressions::Expression::createDoubleLiteral(4.1) && storm::expressions::Expression::createDoubleVariable("d") < storm::expressions::Expression::createDoubleLiteral(4.991)); - msat_term msatEqualsFive = msat_make_equal(env, msat_make_number(env, "5"), i); + storm::expressions::Expression exprCeil = storm::expressions::ceil(d) == i && d > manager->rational(4.1) && d < manager->rational(4.991); + msat_term msatEqualsFive = msat_make_equal(env, msat_make_number(env, "5"), iVar); ASSERT_NO_THROW(conjecture = msat_make_not(env, msat_make_iff(env, adapter.translateExpression(exprFloor), msatEqualsFive))); msat_assert_formula(env, conjecture); @@ -162,7 +173,10 @@ TEST(MathsatExpressionAdapter, MathsatToStormBasic) { unsigned args = 2; - storm::adapters::MathsatExpressionAdapter adapter(env); + std::shared_ptr manager(new storm::expressions::ExpressionManager()); + manager->declareBooleanVariable("x"); + manager->declareBooleanVariable("y"); + storm::adapters::MathsatExpressionAdapter adapter(*manager, env); msat_term msatTrue = msat_make_true(env); storm::expressions::Expression exprTrue; diff --git a/test/functional/adapter/Z3ExpressionAdapterTest.cpp b/test/functional/adapter/Z3ExpressionAdapterTest.cpp index 49d1959ed..ba3cc656f 100644 --- a/test/functional/adapter/Z3ExpressionAdapterTest.cpp +++ b/test/functional/adapter/Z3ExpressionAdapterTest.cpp @@ -1,6 +1,9 @@ #include "gtest/gtest.h" #include "storm-config.h" +#include +#include "src/storage/expressions/ExpressionManager.h" + #ifdef STORM_HAVE_Z3 #include "z3++.h" #include "src/adapters/Z3ExpressionAdapter.h" @@ -11,34 +14,34 @@ TEST(Z3ExpressionAdapter, StormToZ3Basic) { z3::solver s(ctx); z3::expr conjecture = ctx.bool_val(false); - storm::adapters::Z3ExpressionAdapter adapter(ctx); - storm::adapters::Z3ExpressionAdapter adapter2(ctx, false); + std::shared_ptr manager(new storm::expressions::ExpressionManager()); + storm::adapters::Z3ExpressionAdapter adapter(*manager, ctx); - storm::expressions::Expression exprTrue = storm::expressions::Expression::createTrue(); + storm::expressions::Expression exprTrue = manager->boolean(true); z3::expr z3True = ctx.bool_val(true); ASSERT_NO_THROW(conjecture = !z3::expr(ctx, Z3_mk_iff(ctx, adapter.translateExpression(exprTrue), z3True))); s.add(conjecture); ASSERT_TRUE(s.check() == z3::unsat); s.reset(); - storm::expressions::Expression exprFalse = storm::expressions::Expression::createFalse(); + storm::expressions::Expression exprFalse = manager->boolean(false); z3::expr z3False = ctx.bool_val(false); ASSERT_NO_THROW(conjecture = !z3::expr(ctx, Z3_mk_iff(ctx, adapter.translateExpression(exprFalse), z3False))); s.add(conjecture); ASSERT_TRUE(s.check() == z3::unsat); s.reset(); - storm::expressions::Expression exprConjunction = (storm::expressions::Expression::createBooleanVariable("x") && storm::expressions::Expression::createBooleanVariable("y")); + storm::expressions::Variable x = manager->declareBooleanVariable("x"); + storm::expressions::Variable y = manager->declareBooleanVariable("y"); + storm::expressions::Expression exprConjunction = x && y; z3::expr z3Conjunction = (ctx.bool_const("x") && ctx.bool_const("y")); - // Variables not yet created in adapter. - ASSERT_THROW( adapter2.translateExpression(exprConjunction), storm::exceptions::InvalidArgumentException ); ASSERT_NO_THROW(conjecture = !z3::expr(ctx, Z3_mk_iff(ctx, adapter.translateExpression(exprConjunction), z3Conjunction))); s.add(conjecture); ASSERT_TRUE(s.check() == z3::unsat); s.reset(); - storm::expressions::Expression exprNor = !(storm::expressions::Expression::createBooleanVariable("x") || storm::expressions::Expression::createBooleanVariable("y")); + storm::expressions::Expression exprNor = !(x || y); z3::expr z3Nor = !(ctx.bool_const("x") || ctx.bool_const("y")); ASSERT_NO_THROW(adapter.translateExpression(exprNor)); // Variables already created in adapter. ASSERT_NO_THROW(conjecture = !z3::expr(ctx, Z3_mk_iff(ctx, adapter.translateExpression(exprNor), z3Nor))); @@ -52,16 +55,20 @@ TEST(Z3ExpressionAdapter, StormToZ3Integer) { z3::solver s(ctx); z3::expr conjecture = ctx.bool_val(false); - storm::adapters::Z3ExpressionAdapter adapter(ctx, true); + std::shared_ptr manager(new storm::expressions::ExpressionManager()); + storm::adapters::Z3ExpressionAdapter adapter(*manager, ctx); - storm::expressions::Expression exprAdd = (storm::expressions::Expression::createIntegerVariable("x") + storm::expressions::Expression::createIntegerVariable("y") < -storm::expressions::Expression::createIntegerVariable("y")); + storm::expressions::Variable x = manager->declareIntegerVariable("x"); + storm::expressions::Variable y = manager->declareIntegerVariable("y"); + + storm::expressions::Expression exprAdd = x + y < -y; z3::expr z3Add = (ctx.int_const("x") + ctx.int_const("y") < -ctx.int_const("y")); ASSERT_NO_THROW(conjecture = !z3::expr(ctx, Z3_mk_iff(ctx, adapter.translateExpression(exprAdd), z3Add))); s.add(conjecture); ASSERT_TRUE(s.check() == z3::unsat); s.reset(); - storm::expressions::Expression exprMult = !(storm::expressions::Expression::createIntegerVariable("x") * storm::expressions::Expression::createIntegerVariable("y") == storm::expressions::Expression::createIntegerVariable("y")); + storm::expressions::Expression exprMult = !(x * y == y); z3::expr z3Mult = !(ctx.int_const("x") * ctx.int_const("y") == ctx.int_const("y")); ASSERT_NO_THROW(conjecture = !z3::expr(ctx, Z3_mk_iff(ctx, adapter.translateExpression(exprMult), z3Mult))); s.add(conjecture); @@ -74,16 +81,20 @@ TEST(Z3ExpressionAdapter, StormToZ3Real) { z3::solver s(ctx); z3::expr conjecture = ctx.bool_val(false); - storm::adapters::Z3ExpressionAdapter adapter(ctx); + std::shared_ptr manager(new storm::expressions::ExpressionManager()); + storm::adapters::Z3ExpressionAdapter adapter(*manager, ctx); - storm::expressions::Expression exprAdd = (storm::expressions::Expression::createDoubleVariable("x") + storm::expressions::Expression::createDoubleVariable("y") < -storm::expressions::Expression::createDoubleVariable("y")); + storm::expressions::Variable x = manager->declareRationalVariable("x"); + storm::expressions::Variable y = manager->declareRationalVariable("y"); + + storm::expressions::Expression exprAdd = x + y < -y; z3::expr z3Add = (ctx.real_const("x") + ctx.real_const("y") < -ctx.real_const("y")); ASSERT_NO_THROW(conjecture = !z3::expr(ctx, Z3_mk_iff(ctx, adapter.translateExpression(exprAdd), z3Add))); s.add(conjecture); ASSERT_TRUE(s.check() == z3::unsat); s.reset(); - storm::expressions::Expression exprMult = !(storm::expressions::Expression::createDoubleVariable("x") * storm::expressions::Expression::createDoubleVariable("y") == storm::expressions::Expression::createDoubleVariable("y")); + storm::expressions::Expression exprMult = !(x * y == y); z3::expr z3Mult = !(ctx.real_const("x") * ctx.real_const("y") == ctx.real_const("y")); ASSERT_NO_THROW(conjecture = !z3::expr(ctx, Z3_mk_iff(ctx, adapter.translateExpression(exprMult), z3Mult))); s.add(conjecture); @@ -96,9 +107,13 @@ TEST(Z3ExpressionAdapter, StormToZ3FloorCeil) { z3::solver s(ctx); z3::expr conjecture = ctx.bool_val(false); - storm::adapters::Z3ExpressionAdapter adapter(ctx); + std::shared_ptr manager(new storm::expressions::ExpressionManager()); + storm::adapters::Z3ExpressionAdapter adapter(*manager, ctx); - storm::expressions::Expression exprFloor = ((storm::expressions::Expression::createDoubleVariable("d").floor()) == storm::expressions::Expression::createIntegerVariable("i") && storm::expressions::Expression::createDoubleVariable("d") > storm::expressions::Expression::createDoubleLiteral(4.1) && storm::expressions::Expression::createDoubleVariable("d") < storm::expressions::Expression::createDoubleLiteral(4.991)); + storm::expressions::Variable d = manager->declareRationalVariable("d"); + storm::expressions::Variable i = manager->declareIntegerVariable("d"); + + storm::expressions::Expression exprFloor = storm::expressions::floor(d) == i && d > manager->rational(4.1) && d < manager->rational(4.991); z3::expr z3Floor = ctx.int_val(4) == ctx.int_const("i"); ASSERT_NO_THROW(conjecture = !z3::expr(ctx, Z3_mk_iff(ctx, adapter.translateExpression(exprFloor), z3Floor))); @@ -114,7 +129,7 @@ TEST(Z3ExpressionAdapter, StormToZ3FloorCeil) { ASSERT_TRUE(s.check() == z3::unsat); s.reset(); - storm::expressions::Expression exprCeil = ((storm::expressions::Expression::createDoubleVariable("d").ceil()) == storm::expressions::Expression::createIntegerVariable("i") && storm::expressions::Expression::createDoubleVariable("d") > storm::expressions::Expression::createDoubleLiteral(4.1) && storm::expressions::Expression::createDoubleVariable("d") < storm::expressions::Expression::createDoubleLiteral(4.991)); + storm::expressions::Expression exprCeil = storm::expressions::ceil(d) == i && d > manager->rational(4.1) && d < manager->rational(4.991); z3::expr z3Ceil = ctx.int_val(5) == ctx.int_const("i"); ASSERT_NO_THROW(conjecture = !z3::expr(ctx, Z3_mk_iff(ctx, adapter.translateExpression(exprCeil), z3Ceil))); @@ -134,7 +149,10 @@ TEST(Z3ExpressionAdapter, Z3ToStormBasic) { z3::context ctx; unsigned args = 2; - storm::adapters::Z3ExpressionAdapter adapter(ctx); + std::shared_ptr manager(new storm::expressions::ExpressionManager()); + manager->declareBooleanVariable("x"); + manager->declareBooleanVariable("y"); + storm::adapters::Z3ExpressionAdapter adapter(*manager, ctx); z3::expr z3True = ctx.bool_val(true); storm::expressions::Expression exprTrue; diff --git a/test/functional/solver/GlpkLpSolverTest.cpp b/test/functional/solver/GlpkLpSolverTest.cpp index 31c134172..ab3511d83 100644 --- a/test/functional/solver/GlpkLpSolverTest.cpp +++ b/test/functional/solver/GlpkLpSolverTest.cpp @@ -9,15 +9,17 @@ TEST(GlpkLpSolver, LPOptimizeMax) { storm::solver::GlpkLpSolver solver(storm::solver::LpSolver::ModelSense::Maximize); - ASSERT_NO_THROW(solver.addBoundedContinuousVariable("x", 0, 1, -1)); - ASSERT_NO_THROW(solver.addLowerBoundedContinuousVariable("y", 0, 2)); - ASSERT_NO_THROW(solver.addLowerBoundedContinuousVariable("z", 0, 1)); + storm::expressions::Variable x; + storm::expressions::Variable y; + storm::expressions::Variable z; + ASSERT_NO_THROW(x = solver.addBoundedContinuousVariable("x", 0, 1, -1)); + ASSERT_NO_THROW(y = solver.addLowerBoundedContinuousVariable("y", 0, 2)); + ASSERT_NO_THROW(z = solver.addLowerBoundedContinuousVariable("z", 0, 1)); ASSERT_NO_THROW(solver.update()); - - solver.addConstraint("", storm::expressions::Expression::createDoubleVariable("x") + storm::expressions::Expression::createDoubleVariable("y") + storm::expressions::Expression::createDoubleVariable("z") <= storm::expressions::Expression::createDoubleLiteral(12)); - ASSERT_NO_THROW(solver.addConstraint("", storm::expressions::Expression::createDoubleVariable("x") + storm::expressions::Expression::createDoubleVariable("y") + storm::expressions::Expression::createDoubleVariable("z") <= storm::expressions::Expression::createDoubleLiteral(12))); - ASSERT_NO_THROW(solver.addConstraint("", storm::expressions::Expression::createDoubleLiteral(0.5) * storm::expressions::Expression::createDoubleVariable("y") + storm::expressions::Expression::createDoubleVariable("z") - storm::expressions::Expression::createDoubleVariable("x") == storm::expressions::Expression::createDoubleLiteral(5))); - ASSERT_NO_THROW(solver.addConstraint("", storm::expressions::Expression::createDoubleVariable("y") - storm::expressions::Expression::createDoubleVariable("x") <= storm::expressions::Expression::createDoubleLiteral(5.5))); + + ASSERT_NO_THROW(solver.addConstraint("", x + y + z <= solver.getConstant(12))); + ASSERT_NO_THROW(solver.addConstraint("", solver.getConstant(0.5) * y + z - x == solver.getConstant(5))); + ASSERT_NO_THROW(solver.addConstraint("", y - x <= solver.getConstant(5.5))); ASSERT_NO_THROW(solver.update()); ASSERT_NO_THROW(solver.optimize()); @@ -25,13 +27,13 @@ TEST(GlpkLpSolver, LPOptimizeMax) { ASSERT_FALSE(solver.isUnbounded()); ASSERT_FALSE(solver.isInfeasible()); double xValue = 0; - ASSERT_NO_THROW(xValue = solver.getContinuousValue("x")); + ASSERT_NO_THROW(xValue = solver.getContinuousValue(x)); ASSERT_LT(std::abs(xValue - 1), storm::settings::generalSettings().getPrecision()); double yValue = 0; - ASSERT_NO_THROW(yValue = solver.getContinuousValue("y")); + ASSERT_NO_THROW(yValue = solver.getContinuousValue(y)); ASSERT_LT(std::abs(yValue - 6.5), storm::settings::generalSettings().getPrecision()); double zValue = 0; - ASSERT_NO_THROW(zValue = solver.getContinuousValue("z")); + ASSERT_NO_THROW(zValue = solver.getContinuousValue(z)); ASSERT_LT(std::abs(zValue - 2.75), storm::settings::generalSettings().getPrecision()); double objectiveValue = 0; ASSERT_NO_THROW(objectiveValue = solver.getObjectiveValue()); @@ -40,14 +42,17 @@ TEST(GlpkLpSolver, LPOptimizeMax) { TEST(GlpkLpSolver, LPOptimizeMin) { storm::solver::GlpkLpSolver solver(storm::solver::LpSolver::ModelSense::Minimize); - ASSERT_NO_THROW(solver.addBoundedContinuousVariable("x", 0, 1, -1)); - ASSERT_NO_THROW(solver.addLowerBoundedContinuousVariable("y", 0, 2)); - ASSERT_NO_THROW(solver.addBoundedContinuousVariable("z", 1, 5.7, -1)); + storm::expressions::Variable x; + storm::expressions::Variable y; + storm::expressions::Variable z; + ASSERT_NO_THROW(x = solver.addBoundedContinuousVariable("x", 0, 1, -1)); + ASSERT_NO_THROW(y = solver.addLowerBoundedContinuousVariable("y", 0, 2)); + ASSERT_NO_THROW(z = solver.addBoundedContinuousVariable("z", 1, 5.7, -1)); ASSERT_NO_THROW(solver.update()); - ASSERT_NO_THROW(solver.addConstraint("", storm::expressions::Expression::createDoubleVariable("x") + storm::expressions::Expression::createDoubleVariable("y") + storm::expressions::Expression::createDoubleVariable("z") <= storm::expressions::Expression::createDoubleLiteral(12))); - ASSERT_NO_THROW(solver.addConstraint("", storm::expressions::Expression::createDoubleLiteral(0.5) * storm::expressions::Expression::createDoubleVariable("y") + storm::expressions::Expression::createDoubleVariable("z") - storm::expressions::Expression::createDoubleVariable("x") <= storm::expressions::Expression::createDoubleLiteral(5))); - ASSERT_NO_THROW(solver.addConstraint("", storm::expressions::Expression::createDoubleVariable("y") - storm::expressions::Expression::createDoubleVariable("x") <= storm::expressions::Expression::createDoubleLiteral(5.5))); + ASSERT_NO_THROW(solver.addConstraint("", x + y + z <= solver.getConstant(12))); + ASSERT_NO_THROW(solver.addConstraint("", solver.getConstant(0.5) * y + z - x == solver.getConstant(5))); + ASSERT_NO_THROW(solver.addConstraint("", y - x <= solver.getConstant(5.5))); ASSERT_NO_THROW(solver.update()); ASSERT_NO_THROW(solver.optimize()); @@ -55,13 +60,13 @@ TEST(GlpkLpSolver, LPOptimizeMin) { ASSERT_FALSE(solver.isUnbounded()); ASSERT_FALSE(solver.isInfeasible()); double xValue = 0; - ASSERT_NO_THROW(xValue = solver.getContinuousValue("x")); + ASSERT_NO_THROW(xValue = solver.getContinuousValue(x)); ASSERT_LT(std::abs(xValue - 1), storm::settings::generalSettings().getPrecision()); double yValue = 0; - ASSERT_NO_THROW(yValue = solver.getContinuousValue("y")); + ASSERT_NO_THROW(yValue = solver.getContinuousValue(y)); ASSERT_LT(std::abs(yValue - 0), storm::settings::generalSettings().getPrecision()); double zValue = 0; - ASSERT_NO_THROW(zValue = solver.getContinuousValue("z")); + ASSERT_NO_THROW(zValue = solver.getContinuousValue(z)); ASSERT_LT(std::abs(zValue - 5.7), storm::settings::generalSettings().getPrecision()); double objectiveValue = 0; ASSERT_NO_THROW(objectiveValue = solver.getObjectiveValue()); @@ -70,14 +75,17 @@ TEST(GlpkLpSolver, LPOptimizeMin) { TEST(GlpkLpSolver, MILPOptimizeMax) { storm::solver::GlpkLpSolver solver(storm::solver::LpSolver::ModelSense::Maximize); - ASSERT_NO_THROW(solver.addBinaryVariable("x", -1)); - ASSERT_NO_THROW(solver.addLowerBoundedIntegerVariable("y", 0, 2)); - ASSERT_NO_THROW(solver.addLowerBoundedContinuousVariable("z", 0, 1)); + storm::expressions::Variable x; + storm::expressions::Variable y; + storm::expressions::Variable z; + ASSERT_NO_THROW(x = solver.addBinaryVariable("x", -1)); + ASSERT_NO_THROW(y = solver.addLowerBoundedIntegerVariable("y", 0, 2)); + ASSERT_NO_THROW(z = solver.addLowerBoundedContinuousVariable("z", 0, 1)); ASSERT_NO_THROW(solver.update()); - ASSERT_NO_THROW(solver.addConstraint("", storm::expressions::Expression::createDoubleVariable("x") + storm::expressions::Expression::createDoubleVariable("y") + storm::expressions::Expression::createDoubleVariable("z") <= storm::expressions::Expression::createDoubleLiteral(12))); - ASSERT_NO_THROW(solver.addConstraint("", storm::expressions::Expression::createDoubleLiteral(0.5) * storm::expressions::Expression::createDoubleVariable("y") + storm::expressions::Expression::createDoubleVariable("z") - storm::expressions::Expression::createDoubleVariable("x") == storm::expressions::Expression::createDoubleLiteral(5))); - ASSERT_NO_THROW(solver.addConstraint("", storm::expressions::Expression::createDoubleVariable("y") - storm::expressions::Expression::createDoubleVariable("x") <= storm::expressions::Expression::createDoubleLiteral(5.5))); + ASSERT_NO_THROW(solver.addConstraint("", x + y + z <= solver.getConstant(12))); + ASSERT_NO_THROW(solver.addConstraint("", solver.getConstant(0.5) * y + z - x == solver.getConstant(5))); + ASSERT_NO_THROW(solver.addConstraint("", y - x <= solver.getConstant(5.5))); ASSERT_NO_THROW(solver.update()); ASSERT_NO_THROW(solver.optimize()); @@ -85,13 +93,13 @@ TEST(GlpkLpSolver, MILPOptimizeMax) { ASSERT_FALSE(solver.isUnbounded()); ASSERT_FALSE(solver.isInfeasible()); bool xValue = false; - ASSERT_NO_THROW(xValue = solver.getBinaryValue("x")); + ASSERT_NO_THROW(xValue = solver.getBinaryValue(x)); ASSERT_EQ(true, xValue); int_fast64_t yValue = 0; - ASSERT_NO_THROW(yValue = solver.getIntegerValue("y")); + ASSERT_NO_THROW(yValue = solver.getIntegerValue(y)); ASSERT_EQ(6, yValue); double zValue = 0; - ASSERT_NO_THROW(zValue = solver.getContinuousValue("z")); + ASSERT_NO_THROW(zValue = solver.getContinuousValue(z)); ASSERT_LT(std::abs(zValue - 3), storm::settings::generalSettings().getPrecision()); double objectiveValue = 0; ASSERT_NO_THROW(objectiveValue = solver.getObjectiveValue()); @@ -100,14 +108,17 @@ TEST(GlpkLpSolver, MILPOptimizeMax) { TEST(GlpkLpSolver, MILPOptimizeMin) { storm::solver::GlpkLpSolver solver(storm::solver::LpSolver::ModelSense::Minimize); - ASSERT_NO_THROW(solver.addBinaryVariable("x", -1)); - ASSERT_NO_THROW(solver.addLowerBoundedIntegerVariable("y", 0, 2)); - ASSERT_NO_THROW(solver.addBoundedContinuousVariable("z", 0, 5, -1)); + storm::expressions::Variable x; + storm::expressions::Variable y; + storm::expressions::Variable z; + ASSERT_NO_THROW(x = solver.addBinaryVariable("x", -1)); + ASSERT_NO_THROW(y = solver.addLowerBoundedIntegerVariable("y", 0, 2)); + ASSERT_NO_THROW(z = solver.addBoundedContinuousVariable("z", 0, 5, -1)); ASSERT_NO_THROW(solver.update()); - ASSERT_NO_THROW(solver.addConstraint("", storm::expressions::Expression::createDoubleVariable("x") + storm::expressions::Expression::createDoubleVariable("y") + storm::expressions::Expression::createDoubleVariable("z") <= storm::expressions::Expression::createDoubleLiteral(12))); - ASSERT_NO_THROW(solver.addConstraint("", storm::expressions::Expression::createDoubleLiteral(0.5) * storm::expressions::Expression::createDoubleVariable("y") + storm::expressions::Expression::createDoubleVariable("z") - storm::expressions::Expression::createDoubleVariable("x") <= storm::expressions::Expression::createDoubleLiteral(5))); - ASSERT_NO_THROW(solver.addConstraint("", storm::expressions::Expression::createDoubleVariable("y") - storm::expressions::Expression::createDoubleVariable("x") <= storm::expressions::Expression::createDoubleLiteral(5.5))); + ASSERT_NO_THROW(solver.addConstraint("", x + y + z <= solver.getConstant(12))); + ASSERT_NO_THROW(solver.addConstraint("", solver.getConstant(0.5) * y + z - x == solver.getConstant(5))); + ASSERT_NO_THROW(solver.addConstraint("", y - x <= solver.getConstant(5.5))); ASSERT_NO_THROW(solver.update()); ASSERT_NO_THROW(solver.optimize()); @@ -115,13 +126,13 @@ TEST(GlpkLpSolver, MILPOptimizeMin) { ASSERT_FALSE(solver.isUnbounded()); ASSERT_FALSE(solver.isInfeasible()); bool xValue = false; - ASSERT_NO_THROW(xValue = solver.getBinaryValue("x")); + ASSERT_NO_THROW(xValue = solver.getBinaryValue(x)); ASSERT_EQ(true, xValue); int_fast64_t yValue = 0; - ASSERT_NO_THROW(yValue = solver.getIntegerValue("y")); + ASSERT_NO_THROW(yValue = solver.getIntegerValue(y)); ASSERT_EQ(0, yValue); double zValue = 0; - ASSERT_NO_THROW(zValue = solver.getContinuousValue("z")); + ASSERT_NO_THROW(zValue = solver.getContinuousValue(z)); ASSERT_LT(std::abs(zValue - 5), storm::settings::generalSettings().getPrecision()); double objectiveValue = 0; ASSERT_NO_THROW(objectiveValue = solver.getObjectiveValue()); @@ -130,15 +141,18 @@ TEST(GlpkLpSolver, MILPOptimizeMin) { TEST(GlpkLpSolver, LPInfeasible) { storm::solver::GlpkLpSolver solver(storm::solver::LpSolver::ModelSense::Maximize); - ASSERT_NO_THROW(solver.addBoundedContinuousVariable("x", 0, 1, -1)); - ASSERT_NO_THROW(solver.addLowerBoundedContinuousVariable("y", 0, 2)); - ASSERT_NO_THROW(solver.addLowerBoundedContinuousVariable("z", 0, 1)); + storm::expressions::Variable x; + storm::expressions::Variable y; + storm::expressions::Variable z; + ASSERT_NO_THROW(x = solver.addBoundedContinuousVariable("x", 0, 1, -1)); + ASSERT_NO_THROW(y = solver.addLowerBoundedContinuousVariable("y", 0, 2)); + ASSERT_NO_THROW(z = solver.addLowerBoundedContinuousVariable("z", 0, 1)); ASSERT_NO_THROW(solver.update()); - ASSERT_NO_THROW(solver.addConstraint("", storm::expressions::Expression::createDoubleVariable("x") + storm::expressions::Expression::createDoubleVariable("y") + storm::expressions::Expression::createDoubleVariable("z") <= storm::expressions::Expression::createDoubleLiteral(12))); - ASSERT_NO_THROW(solver.addConstraint("", storm::expressions::Expression::createDoubleLiteral(0.5) * storm::expressions::Expression::createDoubleVariable("y") + storm::expressions::Expression::createDoubleVariable("z") - storm::expressions::Expression::createDoubleVariable("x") == storm::expressions::Expression::createDoubleLiteral(5))); - ASSERT_NO_THROW(solver.addConstraint("", storm::expressions::Expression::createDoubleVariable("y") - storm::expressions::Expression::createDoubleVariable("x") <= storm::expressions::Expression::createDoubleLiteral(5.5))); - ASSERT_NO_THROW(solver.addConstraint("", storm::expressions::Expression::createDoubleVariable("y") > storm::expressions::Expression::createDoubleLiteral(7))); + ASSERT_NO_THROW(solver.addConstraint("", x + y + z <= solver.getConstant(12))); + ASSERT_NO_THROW(solver.addConstraint("", solver.getConstant(0.5) * y + z - x == solver.getConstant(5))); + ASSERT_NO_THROW(solver.addConstraint("", y - x <= solver.getConstant(5.5))); + ASSERT_NO_THROW(solver.addConstraint("", y > solver.getConstant(7))); ASSERT_NO_THROW(solver.update()); ASSERT_NO_THROW(solver.optimize()); @@ -146,26 +160,29 @@ TEST(GlpkLpSolver, LPInfeasible) { ASSERT_FALSE(solver.isUnbounded()); ASSERT_TRUE(solver.isInfeasible()); double xValue = 0; - ASSERT_THROW(xValue = solver.getContinuousValue("x"), storm::exceptions::InvalidAccessException); + ASSERT_THROW(xValue = solver.getContinuousValue(x), storm::exceptions::InvalidAccessException); double yValue = 0; - ASSERT_THROW(yValue = solver.getContinuousValue("y"), storm::exceptions::InvalidAccessException); + ASSERT_THROW(yValue = solver.getContinuousValue(y), storm::exceptions::InvalidAccessException); double zValue = 0; - ASSERT_THROW(zValue = solver.getContinuousValue("z"), storm::exceptions::InvalidAccessException); + ASSERT_THROW(zValue = solver.getContinuousValue(z), storm::exceptions::InvalidAccessException); double objectiveValue = 0; ASSERT_THROW(objectiveValue = solver.getObjectiveValue(), storm::exceptions::InvalidAccessException); } TEST(GlpkLpSolver, MILPInfeasible) { storm::solver::GlpkLpSolver solver(storm::solver::LpSolver::ModelSense::Maximize); - ASSERT_NO_THROW(solver.addBinaryVariable("x", -1)); - ASSERT_NO_THROW(solver.addLowerBoundedContinuousVariable("y", 0, 2)); - ASSERT_NO_THROW(solver.addLowerBoundedContinuousVariable("z", 0, 1)); + storm::expressions::Variable x; + storm::expressions::Variable y; + storm::expressions::Variable z; + ASSERT_NO_THROW(x = solver.addBinaryVariable("x", -1)); + ASSERT_NO_THROW(y = solver.addLowerBoundedContinuousVariable("y", 0, 2)); + ASSERT_NO_THROW(z = solver.addLowerBoundedContinuousVariable("z", 0, 1)); ASSERT_NO_THROW(solver.update()); - ASSERT_NO_THROW(solver.addConstraint("", storm::expressions::Expression::createDoubleVariable("x") + storm::expressions::Expression::createDoubleVariable("y") + storm::expressions::Expression::createDoubleVariable("z") <= storm::expressions::Expression::createDoubleLiteral(12))); - ASSERT_NO_THROW(solver.addConstraint("", storm::expressions::Expression::createDoubleLiteral(0.5) * storm::expressions::Expression::createDoubleVariable("y") + storm::expressions::Expression::createDoubleVariable("z") - storm::expressions::Expression::createDoubleVariable("x") == storm::expressions::Expression::createDoubleLiteral(5))); - ASSERT_NO_THROW(solver.addConstraint("", storm::expressions::Expression::createDoubleVariable("y") - storm::expressions::Expression::createDoubleVariable("x") <= storm::expressions::Expression::createDoubleLiteral(5.5))); - ASSERT_NO_THROW(solver.addConstraint("", storm::expressions::Expression::createDoubleVariable("y") > storm::expressions::Expression::createDoubleLiteral(7))); + ASSERT_NO_THROW(solver.addConstraint("", x + y + z <= solver.getConstant(12))); + ASSERT_NO_THROW(solver.addConstraint("", solver.getConstant(0.5) * y + z - x == solver.getConstant(5))); + ASSERT_NO_THROW(solver.addConstraint("", y - x <= solver.getConstant(5.5))); + ASSERT_NO_THROW(solver.addConstraint("", y > solver.getConstant(7))); ASSERT_NO_THROW(solver.update()); ASSERT_NO_THROW(solver.optimize()); @@ -173,24 +190,27 @@ TEST(GlpkLpSolver, MILPInfeasible) { ASSERT_FALSE(solver.isUnbounded()); ASSERT_TRUE(solver.isInfeasible()); bool xValue = false; - ASSERT_THROW(xValue = solver.getBinaryValue("x"), storm::exceptions::InvalidAccessException); + ASSERT_THROW(xValue = solver.getBinaryValue(x), storm::exceptions::InvalidAccessException); int_fast64_t yValue = 0; - ASSERT_THROW(yValue = solver.getIntegerValue("y"), storm::exceptions::InvalidAccessException); + ASSERT_THROW(yValue = solver.getIntegerValue(y), storm::exceptions::InvalidAccessException); double zValue = 0; - ASSERT_THROW(zValue = solver.getContinuousValue("z"), storm::exceptions::InvalidAccessException); + ASSERT_THROW(zValue = solver.getContinuousValue(z), storm::exceptions::InvalidAccessException); double objectiveValue = 0; ASSERT_THROW(objectiveValue = solver.getObjectiveValue(), storm::exceptions::InvalidAccessException); } TEST(GlpkLpSolver, LPUnbounded) { storm::solver::GlpkLpSolver solver(storm::solver::LpSolver::ModelSense::Maximize); - ASSERT_NO_THROW(solver.addBoundedContinuousVariable("x", 0, 1, -1)); - ASSERT_NO_THROW(solver.addLowerBoundedContinuousVariable("y", 0, 2)); - ASSERT_NO_THROW(solver.addLowerBoundedContinuousVariable("z", 0, 1)); + storm::expressions::Variable x; + storm::expressions::Variable y; + storm::expressions::Variable z; + ASSERT_NO_THROW(x = solver.addBoundedContinuousVariable("x", 0, 1, -1)); + ASSERT_NO_THROW(y = solver.addLowerBoundedContinuousVariable("y", 0, 2)); + ASSERT_NO_THROW(z = solver.addLowerBoundedContinuousVariable("z", 0, 1)); ASSERT_NO_THROW(solver.update()); - ASSERT_NO_THROW(solver.addConstraint("", storm::expressions::Expression::createDoubleVariable("x") + storm::expressions::Expression::createDoubleVariable("y") - storm::expressions::Expression::createDoubleVariable("z") <= storm::expressions::Expression::createDoubleLiteral(12))); - ASSERT_NO_THROW(solver.addConstraint("", storm::expressions::Expression::createDoubleVariable("y") - storm::expressions::Expression::createDoubleVariable("x") <= storm::expressions::Expression::createDoubleLiteral(5.5))); + ASSERT_NO_THROW(solver.addConstraint("", x + y - z <= solver.getConstant(12))); + ASSERT_NO_THROW(solver.addConstraint("", y - x <= solver.getConstant(5.5))); ASSERT_NO_THROW(solver.update()); ASSERT_NO_THROW(solver.optimize()); @@ -198,24 +218,27 @@ TEST(GlpkLpSolver, LPUnbounded) { ASSERT_TRUE(solver.isUnbounded()); ASSERT_FALSE(solver.isInfeasible()); double xValue = 0; - ASSERT_THROW(xValue = solver.getContinuousValue("x"), storm::exceptions::InvalidAccessException); + ASSERT_THROW(xValue = solver.getContinuousValue(x), storm::exceptions::InvalidAccessException); double yValue = 0; - ASSERT_THROW(yValue = solver.getContinuousValue("y"), storm::exceptions::InvalidAccessException); + ASSERT_THROW(yValue = solver.getContinuousValue(y), storm::exceptions::InvalidAccessException); double zValue = 0; - ASSERT_THROW(zValue = solver.getContinuousValue("z"), storm::exceptions::InvalidAccessException); + ASSERT_THROW(zValue = solver.getContinuousValue(z), storm::exceptions::InvalidAccessException); double objectiveValue = 0; ASSERT_THROW(objectiveValue = solver.getObjectiveValue(), storm::exceptions::InvalidAccessException); } TEST(GlpkLpSolver, MILPUnbounded) { storm::solver::GlpkLpSolver solver(storm::solver::LpSolver::ModelSense::Maximize); - ASSERT_NO_THROW(solver.addBinaryVariable("x", -1)); - ASSERT_NO_THROW(solver.addLowerBoundedContinuousVariable("y", 0, 2)); - ASSERT_NO_THROW(solver.addLowerBoundedContinuousVariable("z", 0, 1)); + storm::expressions::Variable x; + storm::expressions::Variable y; + storm::expressions::Variable z; + ASSERT_NO_THROW(x = solver.addBinaryVariable("x", -1)); + ASSERT_NO_THROW(y = solver.addLowerBoundedContinuousVariable("y", 0, 2)); + ASSERT_NO_THROW(z = solver.addLowerBoundedContinuousVariable("z", 0, 1)); ASSERT_NO_THROW(solver.update()); - ASSERT_NO_THROW(solver.addConstraint("", storm::expressions::Expression::createDoubleVariable("x") + storm::expressions::Expression::createDoubleVariable("y") - storm::expressions::Expression::createDoubleVariable("z") <= storm::expressions::Expression::createDoubleLiteral(12))); - ASSERT_NO_THROW(solver.addConstraint("", storm::expressions::Expression::createDoubleVariable("y") - storm::expressions::Expression::createDoubleVariable("x") <= storm::expressions::Expression::createDoubleLiteral(5.5))); + ASSERT_NO_THROW(solver.addConstraint("", x + y - z <= solver.getConstant(12))); + ASSERT_NO_THROW(solver.addConstraint("", y - x <= solver.getConstant(5.5))); ASSERT_NO_THROW(solver.update()); ASSERT_NO_THROW(solver.optimize()); @@ -223,11 +246,11 @@ TEST(GlpkLpSolver, MILPUnbounded) { ASSERT_TRUE(solver.isUnbounded()); ASSERT_FALSE(solver.isInfeasible()); bool xValue = false; - ASSERT_THROW(xValue = solver.getBinaryValue("x"), storm::exceptions::InvalidAccessException); + ASSERT_THROW(xValue = solver.getBinaryValue(x), storm::exceptions::InvalidAccessException); int_fast64_t yValue = 0; - ASSERT_THROW(yValue = solver.getIntegerValue("y"), storm::exceptions::InvalidAccessException); + ASSERT_THROW(yValue = solver.getIntegerValue(y), storm::exceptions::InvalidAccessException); double zValue = 0; - ASSERT_THROW(zValue = solver.getContinuousValue("z"), storm::exceptions::InvalidAccessException); + ASSERT_THROW(zValue = solver.getContinuousValue(z), storm::exceptions::InvalidAccessException); double objectiveValue = 0; ASSERT_THROW(objectiveValue = solver.getObjectiveValue(), storm::exceptions::InvalidAccessException); } diff --git a/test/functional/solver/GurobiLpSolverTest.cpp b/test/functional/solver/GurobiLpSolverTest.cpp index e71ad3711..083ed19bc 100644 --- a/test/functional/solver/GurobiLpSolverTest.cpp +++ b/test/functional/solver/GurobiLpSolverTest.cpp @@ -9,28 +9,31 @@ TEST(GurobiLpSolver, LPOptimizeMax) { storm::solver::GurobiLpSolver solver(storm::solver::LpSolver::ModelSense::Maximize); - ASSERT_NO_THROW(solver.addBoundedContinuousVariable("x", 0, 1, -1)); - ASSERT_NO_THROW(solver.addLowerBoundedContinuousVariable("y", 0, 2)); - ASSERT_NO_THROW(solver.addLowerBoundedContinuousVariable("z", 0, 1)); + storm::expressions::Variable x; + storm::expressions::Variable y; + storm::expressions::Variable z; + ASSERT_NO_THROW(x = solver.addBoundedContinuousVariable("x", 0, 1, -1)); + ASSERT_NO_THROW(y = solver.addLowerBoundedContinuousVariable("y", 0, 2)); + ASSERT_NO_THROW(z = solver.addLowerBoundedContinuousVariable("z", 0, 1)); ASSERT_NO_THROW(solver.update()); - ASSERT_NO_THROW(solver.addConstraint("", storm::expressions::Expression::createDoubleVariable("x") + storm::expressions::Expression::createDoubleVariable("y") + storm::expressions::Expression::createDoubleVariable("z") <= storm::expressions::Expression::createDoubleLiteral(12))); - ASSERT_NO_THROW(solver.addConstraint("", storm::expressions::Expression::createDoubleLiteral(0.5) * storm::expressions::Expression::createDoubleVariable("y") + storm::expressions::Expression::createDoubleVariable("z") - storm::expressions::Expression::createDoubleVariable("x") == storm::expressions::Expression::createDoubleLiteral(5))); - ASSERT_NO_THROW(solver.addConstraint("", storm::expressions::Expression::createDoubleVariable("y") - storm::expressions::Expression::createDoubleVariable("x") <= storm::expressions::Expression::createDoubleLiteral(5.5))); + ASSERT_NO_THROW(solver.addConstraint("", x + y + z <= solver.getConstant(12))); + ASSERT_NO_THROW(solver.addConstraint("", solver.getConstant(0.5) * y + z - x == solver.getConstant(5))); + ASSERT_NO_THROW(solver.addConstraint("", y - x <= solver.getConstant(5.5))); ASSERT_NO_THROW(solver.update()); - + ASSERT_NO_THROW(solver.optimize()); ASSERT_TRUE(solver.isOptimal()); ASSERT_FALSE(solver.isUnbounded()); ASSERT_FALSE(solver.isInfeasible()); double xValue = 0; - ASSERT_NO_THROW(xValue = solver.getContinuousValue("x")); + ASSERT_NO_THROW(xValue = solver.getContinuousValue(x)); ASSERT_LT(std::abs(xValue - 1), storm::settings::generalSettings().getPrecision()); double yValue = 0; - ASSERT_NO_THROW(yValue = solver.getContinuousValue("y")); + ASSERT_NO_THROW(yValue = solver.getContinuousValue(y)); ASSERT_LT(std::abs(yValue - 6.5), storm::settings::generalSettings().getPrecision()); double zValue = 0; - ASSERT_NO_THROW(zValue = solver.getContinuousValue("z")); + ASSERT_NO_THROW(zValue = solver.getContinuousValue(z)); ASSERT_LT(std::abs(zValue - 2.75), storm::settings::generalSettings().getPrecision()); double objectiveValue = 0; ASSERT_NO_THROW(objectiveValue = solver.getObjectiveValue()); @@ -39,28 +42,31 @@ TEST(GurobiLpSolver, LPOptimizeMax) { TEST(GurobiLpSolver, LPOptimizeMin) { storm::solver::GurobiLpSolver solver(storm::solver::LpSolver::ModelSense::Minimize); - ASSERT_NO_THROW(solver.addBoundedContinuousVariable("x", 0, 1, -1)); - ASSERT_NO_THROW(solver.addLowerBoundedIntegerVariable("y", 0, 2)); - ASSERT_NO_THROW(solver.addBoundedContinuousVariable("z", 1, 5.7, -1)); + storm::expressions::Variable x; + storm::expressions::Variable y; + storm::expressions::Variable z; + ASSERT_NO_THROW(x = solver.addBoundedContinuousVariable("x", 0, 1, -1)); + ASSERT_NO_THROW(y = solver.addLowerBoundedContinuousVariable("y", 0, 2)); + ASSERT_NO_THROW(z = solver.addBoundedContinuousVariable("z", 1, 5.7, -1)); ASSERT_NO_THROW(solver.update()); - - ASSERT_NO_THROW(solver.addConstraint("", storm::expressions::Expression::createDoubleVariable("x") + storm::expressions::Expression::createDoubleVariable("y") + storm::expressions::Expression::createDoubleVariable("z") <= storm::expressions::Expression::createDoubleLiteral(12))); - ASSERT_NO_THROW(solver.addConstraint("", storm::expressions::Expression::createDoubleLiteral(0.5) * storm::expressions::Expression::createDoubleVariable("y") + storm::expressions::Expression::createDoubleVariable("z") - storm::expressions::Expression::createDoubleVariable("x") <= storm::expressions::Expression::createDoubleLiteral(5))); - ASSERT_NO_THROW(solver.addConstraint("", storm::expressions::Expression::createDoubleVariable("y") - storm::expressions::Expression::createDoubleVariable("x") <= storm::expressions::Expression::createDoubleLiteral(5.5))); + + ASSERT_NO_THROW(solver.addConstraint("", x + y + z <= solver.getConstant(12))); + ASSERT_NO_THROW(solver.addConstraint("", solver.getConstant(0.5) * y + z - x == solver.getConstant(5))); + ASSERT_NO_THROW(solver.addConstraint("", y - x <= solver.getConstant(5.5))); ASSERT_NO_THROW(solver.update()); - + ASSERT_NO_THROW(solver.optimize()); ASSERT_TRUE(solver.isOptimal()); ASSERT_FALSE(solver.isUnbounded()); ASSERT_FALSE(solver.isInfeasible()); double xValue = 0; - ASSERT_NO_THROW(xValue = solver.getContinuousValue("x")); + ASSERT_NO_THROW(xValue = solver.getContinuousValue(x)); ASSERT_LT(std::abs(xValue - 1), storm::settings::generalSettings().getPrecision()); double yValue = 0; - ASSERT_NO_THROW(yValue = solver.getContinuousValue("y")); + ASSERT_NO_THROW(yValue = solver.getContinuousValue(y)); ASSERT_LT(std::abs(yValue - 0), storm::settings::generalSettings().getPrecision()); double zValue = 0; - ASSERT_NO_THROW(zValue = solver.getContinuousValue("z")); + ASSERT_NO_THROW(zValue = solver.getContinuousValue(z)); ASSERT_LT(std::abs(zValue - 5.7), storm::settings::generalSettings().getPrecision()); double objectiveValue = 0; ASSERT_NO_THROW(objectiveValue = solver.getObjectiveValue()); @@ -69,28 +75,31 @@ TEST(GurobiLpSolver, LPOptimizeMin) { TEST(GurobiLpSolver, MILPOptimizeMax) { storm::solver::GurobiLpSolver solver(storm::solver::LpSolver::ModelSense::Maximize); - ASSERT_NO_THROW(solver.addBinaryVariable("x", -1)); - ASSERT_NO_THROW(solver.addLowerBoundedIntegerVariable("y", 0, 2)); - ASSERT_NO_THROW(solver.addLowerBoundedContinuousVariable("z", 0, 1)); + storm::expressions::Variable x; + storm::expressions::Variable y; + storm::expressions::Variable z; + ASSERT_NO_THROW(x = solver.addBinaryVariable("x", -1)); + ASSERT_NO_THROW(y = solver.addLowerBoundedIntegerVariable("y", 0, 2)); + ASSERT_NO_THROW(z = solver.addLowerBoundedContinuousVariable("z", 0, 1)); ASSERT_NO_THROW(solver.update()); - - ASSERT_NO_THROW(solver.addConstraint("", storm::expressions::Expression::createDoubleVariable("x") + storm::expressions::Expression::createDoubleVariable("y") + storm::expressions::Expression::createDoubleVariable("z") <= storm::expressions::Expression::createDoubleLiteral(12))); - ASSERT_NO_THROW(solver.addConstraint("", storm::expressions::Expression::createDoubleLiteral(0.5) * storm::expressions::Expression::createDoubleVariable("y") + storm::expressions::Expression::createDoubleVariable("z") - storm::expressions::Expression::createDoubleVariable("x") == storm::expressions::Expression::createDoubleLiteral(5))); - ASSERT_NO_THROW(solver.addConstraint("", storm::expressions::Expression::createDoubleVariable("y") - storm::expressions::Expression::createDoubleVariable("x") <= storm::expressions::Expression::createDoubleLiteral(5.5))); + + ASSERT_NO_THROW(solver.addConstraint("", x + y + z <= solver.getConstant(12))); + ASSERT_NO_THROW(solver.addConstraint("", solver.getConstant(0.5) * y + z - x == solver.getConstant(5))); + ASSERT_NO_THROW(solver.addConstraint("", y - x <= solver.getConstant(5.5))); ASSERT_NO_THROW(solver.update()); - + ASSERT_NO_THROW(solver.optimize()); ASSERT_TRUE(solver.isOptimal()); ASSERT_FALSE(solver.isUnbounded()); ASSERT_FALSE(solver.isInfeasible()); bool xValue = false; - ASSERT_NO_THROW(xValue = solver.getBinaryValue("x")); + ASSERT_NO_THROW(xValue = solver.getBinaryValue(x)); ASSERT_EQ(true, xValue); int_fast64_t yValue = 0; - ASSERT_NO_THROW(yValue = solver.getIntegerValue("y")); + ASSERT_NO_THROW(yValue = solver.getIntegerValue(y)); ASSERT_EQ(6, yValue); double zValue = 0; - ASSERT_NO_THROW(zValue = solver.getContinuousValue("z")); + ASSERT_NO_THROW(zValue = solver.getContinuousValue(z)); ASSERT_LT(std::abs(zValue - 3), storm::settings::generalSettings().getPrecision()); double objectiveValue = 0; ASSERT_NO_THROW(objectiveValue = solver.getObjectiveValue()); @@ -99,28 +108,31 @@ TEST(GurobiLpSolver, MILPOptimizeMax) { TEST(GurobiLpSolver, MILPOptimizeMin) { storm::solver::GurobiLpSolver solver(storm::solver::LpSolver::ModelSense::Minimize); - ASSERT_NO_THROW(solver.addBinaryVariable("x", -1)); - ASSERT_NO_THROW(solver.addLowerBoundedIntegerVariable("y", 0, 2)); - ASSERT_NO_THROW(solver.addBoundedContinuousVariable("z", 0, 5, -1)); + storm::expressions::Variable x; + storm::expressions::Variable y; + storm::expressions::Variable z; + ASSERT_NO_THROW(x = solver.addBinaryVariable("x", -1)); + ASSERT_NO_THROW(y = solver.addLowerBoundedIntegerVariable("y", 0, 2)); + ASSERT_NO_THROW(z = solver.addBoundedContinuousVariable("z", 0, 5, -1)); ASSERT_NO_THROW(solver.update()); - - ASSERT_NO_THROW(solver.addConstraint("", storm::expressions::Expression::createDoubleVariable("x") + storm::expressions::Expression::createDoubleVariable("y") + storm::expressions::Expression::createDoubleVariable("z") <= storm::expressions::Expression::createDoubleLiteral(12))); - ASSERT_NO_THROW(solver.addConstraint("", storm::expressions::Expression::createDoubleLiteral(0.5) * storm::expressions::Expression::createDoubleVariable("y") + storm::expressions::Expression::createDoubleVariable("z") - storm::expressions::Expression::createDoubleVariable("x") <= storm::expressions::Expression::createDoubleLiteral(5))); - ASSERT_NO_THROW(solver.addConstraint("", storm::expressions::Expression::createDoubleVariable("y") - storm::expressions::Expression::createDoubleVariable("x") <= storm::expressions::Expression::createDoubleLiteral(5.5))); + + ASSERT_NO_THROW(solver.addConstraint("", x + y + z <= solver.getConstant(12))); + ASSERT_NO_THROW(solver.addConstraint("", solver.getConstant(0.5) * y + z - x == solver.getConstant(5))); + ASSERT_NO_THROW(solver.addConstraint("", y - x <= solver.getConstant(5.5))); ASSERT_NO_THROW(solver.update()); - + ASSERT_NO_THROW(solver.optimize()); ASSERT_TRUE(solver.isOptimal()); ASSERT_FALSE(solver.isUnbounded()); ASSERT_FALSE(solver.isInfeasible()); bool xValue = false; - ASSERT_NO_THROW(xValue = solver.getBinaryValue("x")); + ASSERT_NO_THROW(xValue = solver.getBinaryValue(x)); ASSERT_EQ(true, xValue); int_fast64_t yValue = 0; - ASSERT_NO_THROW(yValue = solver.getIntegerValue("y")); + ASSERT_NO_THROW(yValue = solver.getIntegerValue(y)); ASSERT_EQ(0, yValue); double zValue = 0; - ASSERT_NO_THROW(zValue = solver.getContinuousValue("z")); + ASSERT_NO_THROW(zValue = solver.getContinuousValue(z)); ASSERT_LT(std::abs(zValue - 5), storm::settings::generalSettings().getPrecision()); double objectiveValue = 0; ASSERT_NO_THROW(objectiveValue = solver.getObjectiveValue()); @@ -129,103 +141,116 @@ TEST(GurobiLpSolver, MILPOptimizeMin) { TEST(GurobiLpSolver, LPInfeasible) { storm::solver::GurobiLpSolver solver(storm::solver::LpSolver::ModelSense::Maximize); - ASSERT_NO_THROW(solver.addBoundedContinuousVariable("x", 0, 1, -1)); - ASSERT_NO_THROW(solver.addLowerBoundedContinuousVariable("y", 0, 2)); - ASSERT_NO_THROW(solver.addLowerBoundedContinuousVariable("z", 0, 1)); + storm::expressions::Variable x; + storm::expressions::Variable y; + storm::expressions::Variable z; + ASSERT_NO_THROW(x = solver.addBoundedContinuousVariable("x", 0, 1, -1)); + ASSERT_NO_THROW(y = solver.addLowerBoundedContinuousVariable("y", 0, 2)); + ASSERT_NO_THROW(z = solver.addLowerBoundedContinuousVariable("z", 0, 1)); ASSERT_NO_THROW(solver.update()); - - ASSERT_NO_THROW(solver.addConstraint("", storm::expressions::Expression::createDoubleVariable("x") + storm::expressions::Expression::createDoubleVariable("y") + storm::expressions::Expression::createDoubleVariable("z") <= storm::expressions::Expression::createDoubleLiteral(12))); - ASSERT_NO_THROW(solver.addConstraint("", storm::expressions::Expression::createDoubleLiteral(0.5) * storm::expressions::Expression::createDoubleVariable("y") + storm::expressions::Expression::createDoubleVariable("z") - storm::expressions::Expression::createDoubleVariable("x") == storm::expressions::Expression::createDoubleLiteral(5))); - ASSERT_NO_THROW(solver.addConstraint("", storm::expressions::Expression::createDoubleVariable("y") - storm::expressions::Expression::createDoubleVariable("x") <= storm::expressions::Expression::createDoubleLiteral(5.5))); - ASSERT_NO_THROW(solver.addConstraint("", storm::expressions::Expression::createDoubleVariable("y") > storm::expressions::Expression::createDoubleLiteral(7))); + + ASSERT_NO_THROW(solver.addConstraint("", x + y + z <= solver.getConstant(12))); + ASSERT_NO_THROW(solver.addConstraint("", solver.getConstant(0.5) * y + z - x == solver.getConstant(5))); + ASSERT_NO_THROW(solver.addConstraint("", y - x <= solver.getConstant(5.5))); + ASSERT_NO_THROW(solver.addConstraint("", y > solver.getConstant(7))); ASSERT_NO_THROW(solver.update()); - + ASSERT_NO_THROW(solver.optimize()); ASSERT_FALSE(solver.isOptimal()); ASSERT_FALSE(solver.isUnbounded()); ASSERT_TRUE(solver.isInfeasible()); double xValue = 0; - ASSERT_THROW(xValue = solver.getContinuousValue("x"), storm::exceptions::InvalidAccessException); + ASSERT_THROW(xValue = solver.getContinuousValue(x), storm::exceptions::InvalidAccessException); double yValue = 0; - ASSERT_THROW(yValue = solver.getContinuousValue("y"), storm::exceptions::InvalidAccessException); + ASSERT_THROW(yValue = solver.getContinuousValue(y), storm::exceptions::InvalidAccessException); double zValue = 0; - ASSERT_THROW(zValue = solver.getContinuousValue("z"), storm::exceptions::InvalidAccessException); + ASSERT_THROW(zValue = solver.getContinuousValue(z), storm::exceptions::InvalidAccessException); double objectiveValue = 0; ASSERT_THROW(objectiveValue = solver.getObjectiveValue(), storm::exceptions::InvalidAccessException); } TEST(GurobiLpSolver, MILPInfeasible) { storm::solver::GurobiLpSolver solver(storm::solver::LpSolver::ModelSense::Maximize); - ASSERT_NO_THROW(solver.addBinaryVariable("x", -1)); - ASSERT_NO_THROW(solver.addLowerBoundedContinuousVariable("y", 0, 2)); - ASSERT_NO_THROW(solver.addLowerBoundedContinuousVariable("z", 0, 1)); + storm::expressions::Variable x; + storm::expressions::Variable y; + storm::expressions::Variable z; + ASSERT_NO_THROW(x = solver.addBoundedContinuousVariable("x", 0, 1, -1)); + ASSERT_NO_THROW(y = solver.addLowerBoundedContinuousVariable("y", 0, 2)); + ASSERT_NO_THROW(z = solver.addLowerBoundedContinuousVariable("z", 0, 1)); ASSERT_NO_THROW(solver.update()); - - ASSERT_NO_THROW(solver.addConstraint("", storm::expressions::Expression::createDoubleVariable("x") + storm::expressions::Expression::createDoubleVariable("y") + storm::expressions::Expression::createDoubleVariable("z") <= storm::expressions::Expression::createDoubleLiteral(12))); - ASSERT_NO_THROW(solver.addConstraint("", storm::expressions::Expression::createDoubleLiteral(0.5) * storm::expressions::Expression::createDoubleVariable("y") + storm::expressions::Expression::createDoubleVariable("z") - storm::expressions::Expression::createDoubleVariable("x") == storm::expressions::Expression::createDoubleLiteral(5))); - ASSERT_NO_THROW(solver.addConstraint("", storm::expressions::Expression::createDoubleVariable("y") - storm::expressions::Expression::createDoubleVariable("x") <= storm::expressions::Expression::createDoubleLiteral(5.5))); - ASSERT_NO_THROW(solver.addConstraint("", storm::expressions::Expression::createDoubleVariable("y") > storm::expressions::Expression::createDoubleLiteral(7))); + + ASSERT_NO_THROW(solver.addConstraint("", x + y + z <= solver.getConstant(12))); + ASSERT_NO_THROW(solver.addConstraint("", solver.getConstant(0.5) * y + z - x == solver.getConstant(5))); + ASSERT_NO_THROW(solver.addConstraint("", y - x <= solver.getConstant(5.5))); + ASSERT_NO_THROW(solver.addConstraint("", y > solver.getConstant(7))); ASSERT_NO_THROW(solver.update()); - + ASSERT_NO_THROW(solver.optimize()); ASSERT_FALSE(solver.isOptimal()); ASSERT_FALSE(solver.isUnbounded()); ASSERT_TRUE(solver.isInfeasible()); - bool xValue = false; - ASSERT_THROW(xValue = solver.getBinaryValue("x"), storm::exceptions::InvalidAccessException); - int_fast64_t yValue = 0; - ASSERT_THROW(yValue = solver.getIntegerValue("y"), storm::exceptions::InvalidAccessException); + double xValue = 0; + ASSERT_THROW(xValue = solver.getContinuousValue(x), storm::exceptions::InvalidAccessException); + double yValue = 0; + ASSERT_THROW(yValue = solver.getContinuousValue(y), storm::exceptions::InvalidAccessException); double zValue = 0; - ASSERT_THROW(zValue = solver.getContinuousValue("z"), storm::exceptions::InvalidAccessException); + ASSERT_THROW(zValue = solver.getContinuousValue(z), storm::exceptions::InvalidAccessException); double objectiveValue = 0; ASSERT_THROW(objectiveValue = solver.getObjectiveValue(), storm::exceptions::InvalidAccessException); } TEST(GurobiLpSolver, LPUnbounded) { storm::solver::GurobiLpSolver solver(storm::solver::LpSolver::ModelSense::Maximize); - ASSERT_NO_THROW(solver.addBoundedContinuousVariable("x", 0, 1, -1)); - ASSERT_NO_THROW(solver.addLowerBoundedContinuousVariable("y", 0, 2)); - ASSERT_NO_THROW(solver.addLowerBoundedContinuousVariable("z", 0, 1)); + storm::expressions::Variable x; + storm::expressions::Variable y; + storm::expressions::Variable z; + ASSERT_NO_THROW(x = solver.addBoundedContinuousVariable("x", 0, 1, -1)); + ASSERT_NO_THROW(y = solver.addLowerBoundedContinuousVariable("y", 0, 2)); + ASSERT_NO_THROW(z = solver.addLowerBoundedContinuousVariable("z", 0, 1)); ASSERT_NO_THROW(solver.update()); - - ASSERT_NO_THROW(solver.addConstraint("", storm::expressions::Expression::createDoubleVariable("x") + storm::expressions::Expression::createDoubleVariable("y") - storm::expressions::Expression::createDoubleVariable("z") <= storm::expressions::Expression::createDoubleLiteral(12))); - ASSERT_NO_THROW(solver.addConstraint("", storm::expressions::Expression::createDoubleVariable("y") - storm::expressions::Expression::createDoubleVariable("x") <= storm::expressions::Expression::createDoubleLiteral(5.5))); + + ASSERT_NO_THROW(solver.addConstraint("", x + y - z <= solver.getConstant(12))); + ASSERT_NO_THROW(solver.addConstraint("", y - x <= solver.getConstant(5.5))); ASSERT_NO_THROW(solver.update()); - + ASSERT_NO_THROW(solver.optimize()); ASSERT_FALSE(solver.isOptimal()); ASSERT_TRUE(solver.isUnbounded()); ASSERT_FALSE(solver.isInfeasible()); double xValue = 0; - ASSERT_THROW(xValue = solver.getContinuousValue("x"), storm::exceptions::InvalidAccessException); + ASSERT_THROW(xValue = solver.getContinuousValue(x), storm::exceptions::InvalidAccessException); double yValue = 0; - ASSERT_THROW(yValue = solver.getContinuousValue("y"), storm::exceptions::InvalidAccessException); + ASSERT_THROW(yValue = solver.getContinuousValue(y), storm::exceptions::InvalidAccessException); double zValue = 0; - ASSERT_THROW(zValue = solver.getContinuousValue("z"), storm::exceptions::InvalidAccessException); + ASSERT_THROW(zValue = solver.getContinuousValue(z), storm::exceptions::InvalidAccessException); double objectiveValue = 0; ASSERT_THROW(objectiveValue = solver.getObjectiveValue(), storm::exceptions::InvalidAccessException); } TEST(GurobiLpSolver, MILPUnbounded) { storm::solver::GurobiLpSolver solver(storm::solver::LpSolver::ModelSense::Maximize); - ASSERT_NO_THROW(solver.addBinaryVariable("x", -1)); - ASSERT_NO_THROW(solver.addLowerBoundedContinuousVariable("y", 0, 2)); - ASSERT_NO_THROW(solver.addLowerBoundedContinuousVariable("z", 0, 1)); + storm::expressions::Variable x; + storm::expressions::Variable y; + storm::expressions::Variable z; + ASSERT_NO_THROW(x = solver.addBinaryVariable("x", -1)); + ASSERT_NO_THROW(y = solver.addLowerBoundedContinuousVariable("y", 0, 2)); + ASSERT_NO_THROW(z = solver.addLowerBoundedContinuousVariable("z", 0, 1)); + ASSERT_NO_THROW(solver.update()); + + ASSERT_NO_THROW(solver.addConstraint("", x + y - z <= solver.getConstant(12))); + ASSERT_NO_THROW(solver.addConstraint("", y - x <= solver.getConstant(5.5))); ASSERT_NO_THROW(solver.update()); - - ASSERT_NO_THROW(solver.addConstraint("", storm::expressions::Expression::createDoubleVariable("x") + storm::expressions::Expression::createDoubleVariable("y") - storm::expressions::Expression::createDoubleVariable("z") <= storm::expressions::Expression::createDoubleLiteral(12))); - ASSERT_NO_THROW(solver.addConstraint("", storm::expressions::Expression::createDoubleVariable("y") - storm::expressions::Expression::createDoubleVariable("x") <= storm::expressions::Expression::createDoubleLiteral(5.5))); ASSERT_NO_THROW(solver.optimize()); ASSERT_FALSE(solver.isOptimal()); ASSERT_TRUE(solver.isUnbounded()); ASSERT_FALSE(solver.isInfeasible()); bool xValue = false; - ASSERT_THROW(xValue = solver.getBinaryValue("x"), storm::exceptions::InvalidAccessException); + ASSERT_THROW(xValue = solver.getBinaryValue(x), storm::exceptions::InvalidAccessException); int_fast64_t yValue = 0; - ASSERT_THROW(yValue = solver.getIntegerValue("y"), storm::exceptions::InvalidAccessException); + ASSERT_THROW(yValue = solver.getIntegerValue(y), storm::exceptions::InvalidAccessException); double zValue = 0; - ASSERT_THROW(zValue = solver.getContinuousValue("z"), storm::exceptions::InvalidAccessException); + ASSERT_THROW(zValue = solver.getContinuousValue(z), storm::exceptions::InvalidAccessException); double objectiveValue = 0; ASSERT_THROW(objectiveValue = solver.getObjectiveValue(), storm::exceptions::InvalidAccessException); } diff --git a/test/functional/solver/MathSatSmtSolverTest.cpp b/test/functional/solver/MathSatSmtSolverTest.cpp index 2efdbc4fc..52cb38ee2 100644 --- a/test/functional/solver/MathSatSmtSolverTest.cpp +++ b/test/functional/solver/MathSatSmtSolverTest.cpp @@ -5,24 +5,26 @@ #include "src/solver/MathsatSmtSolver.h" TEST(MathsatSmtSolver, CheckSat) { - storm::solver::MathsatSmtSolver s; + std::shared_ptr manager(new storm::expressions::ExpressionManager()); + + storm::expressions::Variable x = manager->declareBooleanVariable("x"); + storm::expressions::Variable y = manager->declareBooleanVariable("y"); + + storm::solver::MathsatSmtSolver s(*manager); storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::Unknown; - storm::expressions::Expression exprDeMorgan = !(storm::expressions::Expression::createBooleanVariable("x") && storm::expressions::Expression::createBooleanVariable("y")).iff((!storm::expressions::Expression::createBooleanVariable("x") || !storm::expressions::Expression::createBooleanVariable("y"))); + storm::expressions::Expression exprDeMorgan = storm::expressions::iff(!(x && y), !x || !y); ASSERT_NO_THROW(s.add(exprDeMorgan)); ASSERT_NO_THROW(result = s.check()); ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat); ASSERT_NO_THROW(s.reset()); - storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a"); - storm::expressions::Expression b = storm::expressions::Expression::createIntegerVariable("b"); - storm::expressions::Expression c = storm::expressions::Expression::createIntegerVariable("c"); - storm::expressions::Expression exprFormula = a >= storm::expressions::Expression::createIntegerLiteral(0) - && a < storm::expressions::Expression::createIntegerLiteral(5) - && b > storm::expressions::Expression::createIntegerLiteral(7) - && c == (a * b) - && b + a > c; + storm::expressions::Variable a = manager->declareIntegerVariable("a"); + storm::expressions::Variable b = manager->declareIntegerVariable("b"); + storm::expressions::Variable c = manager->declareIntegerVariable("c"); + + storm::expressions::Expression exprFormula = a >= manager->integer(0) && a < manager->integer(5) && b > manager->integer(7) && c == (a * b) && b + a > c; ASSERT_NO_THROW(s.add(exprFormula)); ASSERT_NO_THROW(result = s.check()); @@ -31,24 +33,26 @@ TEST(MathsatSmtSolver, CheckSat) { } TEST(MathsatSmtSolver, CheckUnsat) { - storm::solver::MathsatSmtSolver s; + std::shared_ptr manager(new storm::expressions::ExpressionManager()); + + storm::expressions::Variable x = manager->declareBooleanVariable("x"); + storm::expressions::Variable y = manager->declareBooleanVariable("y"); + + storm::solver::MathsatSmtSolver s(*manager); storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::Unknown; - storm::expressions::Expression exprDeMorgan = !(storm::expressions::Expression::createBooleanVariable("x") && storm::expressions::Expression::createBooleanVariable("y")).iff( (!storm::expressions::Expression::createBooleanVariable("x") || !storm::expressions::Expression::createBooleanVariable("y"))); + storm::expressions::Expression exprDeMorgan = storm::expressions::iff(!(x && y), !x || !y); ASSERT_NO_THROW(s.add(!exprDeMorgan)); ASSERT_NO_THROW(result = s.check()); ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat); ASSERT_NO_THROW(s.reset()); - storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a"); - storm::expressions::Expression b = storm::expressions::Expression::createIntegerVariable("b"); - storm::expressions::Expression c = storm::expressions::Expression::createIntegerVariable("c"); - storm::expressions::Expression exprFormula = a >= storm::expressions::Expression::createIntegerLiteral(2) - && a < storm::expressions::Expression::createIntegerLiteral(5) - && b > storm::expressions::Expression::createIntegerLiteral(7) - && c == (a + b + storm::expressions::Expression::createIntegerLiteral(1)) - && b + a > c; + storm::expressions::Variable a = manager->declareIntegerVariable("a"); + storm::expressions::Variable b = manager->declareIntegerVariable("b"); + storm::expressions::Variable c = manager->declareIntegerVariable("c"); + + storm::expressions::Expression exprFormula = a >= manager->rational(2) && a < manager->integer(5) && b > manager->integer(7) && c == (a + b + manager->integer(1)) && b + a > c; ASSERT_NO_THROW(s.add(exprFormula)); ASSERT_NO_THROW(result = s.check()); @@ -56,12 +60,14 @@ TEST(MathsatSmtSolver, CheckUnsat) { } TEST(MathsatSmtSolver, Backtracking) { - storm::solver::MathsatSmtSolver s; + std::shared_ptr manager(new storm::expressions::ExpressionManager()); + + storm::solver::MathsatSmtSolver s(*manager); storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::Unknown; - storm::expressions::Expression expr1 = storm::expressions::Expression::createTrue(); - storm::expressions::Expression expr2 = storm::expressions::Expression::createFalse(); - storm::expressions::Expression expr3 = storm::expressions::Expression::createFalse(); + storm::expressions::Expression expr1 = manager->boolean(true); + storm::expressions::Expression expr2 = manager->boolean(false); + storm::expressions::Expression expr3 = manager->boolean(false); ASSERT_NO_THROW(s.add(expr1)); ASSERT_NO_THROW(result = s.check()); @@ -86,15 +92,11 @@ TEST(MathsatSmtSolver, Backtracking) { ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat); ASSERT_NO_THROW(s.reset()); - storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a"); - storm::expressions::Expression b = storm::expressions::Expression::createIntegerVariable("b"); - storm::expressions::Expression c = storm::expressions::Expression::createIntegerVariable("c"); - storm::expressions::Expression exprFormula = a >= storm::expressions::Expression::createIntegerLiteral(0) - && a < storm::expressions::Expression::createIntegerLiteral(5) - && b > storm::expressions::Expression::createIntegerLiteral(7) - && c == (a + b - storm::expressions::Expression::createIntegerLiteral(1)) - && b + a > c; - storm::expressions::Expression exprFormula2 = c > a + b + storm::expressions::Expression::createIntegerLiteral(1); + storm::expressions::Variable a = manager->declareIntegerVariable("a"); + storm::expressions::Variable b = manager->declareIntegerVariable("b"); + storm::expressions::Variable c = manager->declareIntegerVariable("c"); + storm::expressions::Expression exprFormula = a >= manager->integer(0) && a < manager->integer(5) && b > manager->integer(7) && c == (a + b - manager->integer(1)) && b + a > c; + storm::expressions::Expression exprFormula2 = c > a + b + manager->integer(1); ASSERT_NO_THROW(s.add(exprFormula)); ASSERT_NO_THROW(result = s.check()); @@ -109,19 +111,17 @@ TEST(MathsatSmtSolver, Backtracking) { } TEST(MathsatSmtSolver, Assumptions) { - storm::solver::MathsatSmtSolver s; + std::shared_ptr manager(new storm::expressions::ExpressionManager()); + + storm::solver::MathsatSmtSolver s(*manager); storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::Unknown; - storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a"); - storm::expressions::Expression b = storm::expressions::Expression::createIntegerVariable("b"); - storm::expressions::Expression c = storm::expressions::Expression::createIntegerVariable("c"); - storm::expressions::Expression exprFormula = a >= storm::expressions::Expression::createIntegerLiteral(0) - && a < storm::expressions::Expression::createIntegerLiteral(5) - && b > storm::expressions::Expression::createIntegerLiteral(7) - && c == (a + b - storm::expressions::Expression::createIntegerLiteral(1)) - && b + a > c; - storm::expressions::Expression f2 = storm::expressions::Expression::createBooleanVariable("f2"); - storm::expressions::Expression exprFormula2 = f2.implies(c > a + b + storm::expressions::Expression::createIntegerLiteral(1)); + storm::expressions::Variable a = manager->declareIntegerVariable("a"); + storm::expressions::Variable b = manager->declareIntegerVariable("b"); + storm::expressions::Variable c = manager->declareIntegerVariable("c"); + storm::expressions::Expression exprFormula = a >= manager->integer(0) && a < manager->integer(5) && b > manager->integer(7) && c == a + b - manager->integer(1) && b + a > c; + storm::expressions::Variable f2 = manager->declareBooleanVariable("f2"); + storm::expressions::Expression exprFormula2 = storm::expressions::implies(f2, c > a + b + manager->integer(1)); ASSERT_NO_THROW(s.add(exprFormula)); ASSERT_NO_THROW(result = s.check()); @@ -138,40 +138,40 @@ TEST(MathsatSmtSolver, Assumptions) { } TEST(MathsatSmtSolver, GenerateModel) { - storm::solver::MathsatSmtSolver s; + std::shared_ptr manager(new storm::expressions::ExpressionManager()); + + storm::solver::MathsatSmtSolver s(*manager); storm::solver::SmtSolver::CheckResult result; - storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a"); - storm::expressions::Expression b = storm::expressions::Expression::createIntegerVariable("b"); - storm::expressions::Expression c = storm::expressions::Expression::createIntegerVariable("c"); - storm::expressions::Expression exprFormula = a > storm::expressions::Expression::createIntegerLiteral(0) - && a < storm::expressions::Expression::createIntegerLiteral(5) - && b > storm::expressions::Expression::createIntegerLiteral(7) - && c == (a + b - storm::expressions::Expression::createIntegerLiteral(1)) - && b + a > c; + storm::expressions::Variable a = manager->declareIntegerVariable("a"); + storm::expressions::Variable b = manager->declareIntegerVariable("b"); + storm::expressions::Variable c = manager->declareIntegerVariable("c"); + storm::expressions::Expression exprFormula = a > manager->integer(0) && a < manager->integer(5) && b > manager->integer(7) && c == a + b - manager->integer(1) && b + a > c; s.add(exprFormula); result = s.check(); ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat); std::shared_ptr model = s.getModel(); - int_fast64_t aEval = model->getIntegerValue("a"); - int_fast64_t bEval = model->getIntegerValue("b"); - int_fast64_t cEval = model->getIntegerValue("c"); + int_fast64_t aEval = model->getIntegerValue(a); + int_fast64_t bEval = model->getIntegerValue(b); + int_fast64_t cEval = model->getIntegerValue(c); ASSERT_TRUE(cEval == aEval + bEval - 1); } TEST(MathsatSmtSolver, AllSat) { - storm::solver::MathsatSmtSolver s; + std::shared_ptr manager(new storm::expressions::ExpressionManager()); + + storm::solver::MathsatSmtSolver s(*manager); storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::Unknown; - storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a"); - storm::expressions::Expression b = storm::expressions::Expression::createIntegerVariable("b"); - storm::expressions::Expression x = storm::expressions::Expression::createBooleanVariable("x"); - storm::expressions::Expression y = storm::expressions::Expression::createBooleanVariable("y"); - storm::expressions::Expression z = storm::expressions::Expression::createBooleanVariable("z"); - storm::expressions::Expression exprFormula1 = x.implies(a > storm::expressions::Expression::createIntegerLiteral(5)); - storm::expressions::Expression exprFormula2 = y.implies(a < storm::expressions::Expression::createIntegerLiteral(5)); - storm::expressions::Expression exprFormula3 = z.implies(b < storm::expressions::Expression::createIntegerLiteral(5)); + storm::expressions::Variable a = manager->declareIntegerVariable("a"); + storm::expressions::Variable b = manager->declareIntegerVariable("b"); + storm::expressions::Variable x = manager->declareBooleanVariable("x"); + storm::expressions::Variable y = manager->declareBooleanVariable("y"); + storm::expressions::Variable z = manager->declareBooleanVariable("z"); + storm::expressions::Expression exprFormula1 = storm::expressions::implies(x, a > manager->integer(5)); + storm::expressions::Expression exprFormula2 = storm::expressions::implies(y, a < manager->integer(5)); + storm::expressions::Expression exprFormula3 = storm::expressions::implies(z, b < manager->integer(5)); s.add(exprFormula1); s.add(exprFormula2); @@ -181,33 +181,26 @@ TEST(MathsatSmtSolver, AllSat) { ASSERT_TRUE(valuations.size() == 3); for (int i = 0; i < valuations.size(); ++i) { - ASSERT_EQ(valuations[i].getNumberOfIdentifiers(), 2); - ASSERT_TRUE(valuations[i].containsBooleanIdentifier("x")); - ASSERT_TRUE(valuations[i].containsBooleanIdentifier("y")); - } - for (int i = 0; i < valuations.size(); ++i) { - ASSERT_FALSE(valuations[i].getBooleanValue("x") && valuations[i].getBooleanValue("y")); + ASSERT_FALSE(valuations[i].getBooleanValue(x) && valuations[i].getBooleanValue(y)); for (int j = i+1; j < valuations.size(); ++j) { - ASSERT_TRUE((valuations[i].getBooleanValue("x") != valuations[j].getBooleanValue("x")) || (valuations[i].getBooleanValue("y") != valuations[j].getBooleanValue("y"))); + ASSERT_TRUE((valuations[i].getBooleanValue(x) != valuations[j].getBooleanValue(x)) || (valuations[i].getBooleanValue(y) != valuations[j].getBooleanValue(y))); } } } TEST(MathsatSmtSolver, UnsatAssumptions) { - storm::solver::MathsatSmtSolver s(storm::solver::MathsatSmtSolver::Options(false, true, false)); + std::shared_ptr manager(new storm::expressions::ExpressionManager()); + + storm::solver::MathsatSmtSolver s(*manager, storm::solver::MathsatSmtSolver::Options(false, true, false)); storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::Unknown; - storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a"); - storm::expressions::Expression b = storm::expressions::Expression::createIntegerVariable("b"); - storm::expressions::Expression c = storm::expressions::Expression::createIntegerVariable("c"); - storm::expressions::Expression exprFormula = a >= storm::expressions::Expression::createIntegerLiteral(0) - && a < storm::expressions::Expression::createIntegerLiteral(5) - && b > storm::expressions::Expression::createIntegerLiteral(7) - && c == (a + b - storm::expressions::Expression::createIntegerLiteral(1)) - && b + a > c; - storm::expressions::Expression f2 = storm::expressions::Expression::createBooleanVariable("f2"); - storm::expressions::Expression exprFormula2 = f2.implies(c > a + b + storm::expressions::Expression::createIntegerLiteral(1)); + storm::expressions::Variable a = manager->declareIntegerVariable("a"); + storm::expressions::Variable b = manager->declareIntegerVariable("b"); + storm::expressions::Variable c = manager->declareIntegerVariable("c"); + storm::expressions::Expression exprFormula = a >= manager->integer(0) && a < manager->integer(5) && b > manager->integer(7) && c == a + b - manager->integer(1) && b + a > c; + storm::expressions::Variable f2 = manager->declareBooleanVariable("f2"); + storm::expressions::Expression exprFormula2 = storm::expressions::implies(f2, c > a + b + manager->integer(1)); s.add(exprFormula); s.add(exprFormula2); @@ -220,12 +213,14 @@ TEST(MathsatSmtSolver, UnsatAssumptions) { } TEST(MathsatSmtSolver, InterpolationTest) { - storm::solver::MathsatSmtSolver s(storm::solver::MathsatSmtSolver::Options(false, false, true)); + std::shared_ptr manager(new storm::expressions::ExpressionManager()); + + storm::solver::MathsatSmtSolver s(*manager, storm::solver::MathsatSmtSolver::Options(false, false, true)); storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::Unknown; - storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a"); - storm::expressions::Expression b = storm::expressions::Expression::createIntegerVariable("b"); - storm::expressions::Expression c = storm::expressions::Expression::createIntegerVariable("c"); + storm::expressions::Variable a = manager->declareIntegerVariable("a"); + storm::expressions::Variable b = manager->declareIntegerVariable("b"); + storm::expressions::Variable c = manager->declareIntegerVariable("c"); storm::expressions::Expression exprFormula = a > b; storm::expressions::Expression exprFormula2 = b > c; storm::expressions::Expression exprFormula3 = c > a; @@ -243,9 +238,9 @@ TEST(MathsatSmtSolver, InterpolationTest) { storm::expressions::Expression interpol; ASSERT_NO_THROW(interpol = s.getInterpolant({0, 1})); - storm::solver::MathsatSmtSolver s2; + storm::solver::MathsatSmtSolver s2(*manager); - ASSERT_NO_THROW(s2.add(!(exprFormula && exprFormula2).implies(interpol))); + ASSERT_NO_THROW(s2.add(storm::expressions::implies(!(exprFormula && exprFormula2), interpol))); ASSERT_NO_THROW(result = s2.check()); ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat); diff --git a/test/functional/solver/Z3SmtSolverTest.cpp b/test/functional/solver/Z3SmtSolverTest.cpp index 7b05af248..4e2b1b63c 100644 --- a/test/functional/solver/Z3SmtSolverTest.cpp +++ b/test/functional/solver/Z3SmtSolverTest.cpp @@ -3,27 +3,28 @@ #ifdef STORM_HAVE_Z3 #include "src/solver/Z3SmtSolver.h" -#include "src/settings/SettingsManager.h" TEST(Z3SmtSolver, CheckSat) { - storm::solver::Z3SmtSolver s; + std::shared_ptr manager(new storm::expressions::ExpressionManager()); + + storm::expressions::Variable x = manager->declareBooleanVariable("x"); + storm::expressions::Variable y = manager->declareBooleanVariable("y"); + + storm::solver::Z3SmtSolver s(*manager); storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::Unknown; - storm::expressions::Expression exprDeMorgan = !(storm::expressions::Expression::createBooleanVariable("x") && storm::expressions::Expression::createBooleanVariable("y")).iff((!storm::expressions::Expression::createBooleanVariable("x") || !storm::expressions::Expression::createBooleanVariable("y"))); + storm::expressions::Expression exprDeMorgan = storm::expressions::iff(!(x && y), !x || !y); ASSERT_NO_THROW(s.add(exprDeMorgan)); ASSERT_NO_THROW(result = s.check()); ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat); ASSERT_NO_THROW(s.reset()); - storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a"); - storm::expressions::Expression b = storm::expressions::Expression::createIntegerVariable("b"); - storm::expressions::Expression c = storm::expressions::Expression::createIntegerVariable("c"); - storm::expressions::Expression exprFormula = a >= storm::expressions::Expression::createIntegerLiteral(0) - && a < storm::expressions::Expression::createIntegerLiteral(5) - && b > storm::expressions::Expression::createIntegerLiteral(7) - && c == (a * b) - && b + a > c; + storm::expressions::Variable a = manager->declareIntegerVariable("a"); + storm::expressions::Variable b = manager->declareIntegerVariable("b"); + storm::expressions::Variable c = manager->declareIntegerVariable("c"); + + storm::expressions::Expression exprFormula = a >= manager->integer(0) && a < manager->integer(5) && b > manager->integer(7) && c == (a * b) && b + a > c; ASSERT_NO_THROW(s.add(exprFormula)); ASSERT_NO_THROW(result = s.check()); @@ -32,194 +33,183 @@ TEST(Z3SmtSolver, CheckSat) { } TEST(Z3SmtSolver, CheckUnsat) { - storm::solver::Z3SmtSolver s; + std::shared_ptr manager(new storm::expressions::ExpressionManager()); + + storm::expressions::Variable x = manager->declareBooleanVariable("x"); + storm::expressions::Variable y = manager->declareBooleanVariable("y"); + + storm::solver::Z3SmtSolver s(*manager); storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::Unknown; - storm::expressions::Expression exprDeMorgan = !(storm::expressions::Expression::createBooleanVariable("x") && storm::expressions::Expression::createBooleanVariable("y")).iff( (!storm::expressions::Expression::createBooleanVariable("x") || !storm::expressions::Expression::createBooleanVariable("y"))); + storm::expressions::Expression exprDeMorgan = storm::expressions::iff(!(x && y), !x || !y); ASSERT_NO_THROW(s.add(!exprDeMorgan)); ASSERT_NO_THROW(result = s.check()); ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat); ASSERT_NO_THROW(s.reset()); + storm::expressions::Variable a = manager->declareIntegerVariable("a"); + storm::expressions::Variable b = manager->declareIntegerVariable("b"); + storm::expressions::Variable c = manager->declareIntegerVariable("c"); - storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a"); - storm::expressions::Expression b = storm::expressions::Expression::createIntegerVariable("b"); - storm::expressions::Expression c = storm::expressions::Expression::createIntegerVariable("c"); - storm::expressions::Expression exprFormula = a >= storm::expressions::Expression::createIntegerLiteral(2) - && a < storm::expressions::Expression::createIntegerLiteral(5) - && b > storm::expressions::Expression::createIntegerLiteral(7) - && c == (a * b) - && b + a > c; + storm::expressions::Expression exprFormula = a >= manager->rational(2) && a < manager->integer(5) && b > manager->integer(7) && c == (a + b + manager->integer(1)) && b + a > c; ASSERT_NO_THROW(s.add(exprFormula)); ASSERT_NO_THROW(result = s.check()); ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat); } - TEST(Z3SmtSolver, Backtracking) { - storm::solver::Z3SmtSolver s; - storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::Unknown; - - storm::expressions::Expression expr1 = storm::expressions::Expression::createTrue(); - storm::expressions::Expression expr2 = storm::expressions::Expression::createFalse(); - storm::expressions::Expression expr3 = storm::expressions::Expression::createFalse(); - - ASSERT_NO_THROW(s.add(expr1)); - ASSERT_NO_THROW(result = s.check()); - ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat); - ASSERT_NO_THROW(s.push()); - ASSERT_NO_THROW(s.add(expr2)); - ASSERT_NO_THROW(result = s.check()); - ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat); - ASSERT_NO_THROW(s.pop()); - ASSERT_NO_THROW(result = s.check()); - ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat); - ASSERT_NO_THROW(s.push()); - ASSERT_NO_THROW(s.add(expr2)); - ASSERT_NO_THROW(result = s.check()); - ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat); - ASSERT_NO_THROW(s.push()); - ASSERT_NO_THROW(s.add(expr3)); - ASSERT_NO_THROW(result = s.check()); - ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat); - ASSERT_NO_THROW(s.pop(2)); - ASSERT_NO_THROW(result = s.check()); - ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat); - ASSERT_NO_THROW(s.reset()); - - - storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a"); - storm::expressions::Expression b = storm::expressions::Expression::createIntegerVariable("b"); - storm::expressions::Expression c = storm::expressions::Expression::createIntegerVariable("c"); - storm::expressions::Expression exprFormula = a >= storm::expressions::Expression::createIntegerLiteral(0) - && a < storm::expressions::Expression::createIntegerLiteral(5) - && b > storm::expressions::Expression::createIntegerLiteral(7) - && c == (a * b) - && b + a > c; - storm::expressions::Expression exprFormula2 = a >= storm::expressions::Expression::createIntegerLiteral(2); - - ASSERT_NO_THROW(s.add(exprFormula)); - ASSERT_NO_THROW(result = s.check()); - ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat); - ASSERT_NO_THROW(s.push()); - ASSERT_NO_THROW(s.add(exprFormula2)); - ASSERT_NO_THROW(result = s.check()); - ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat); - ASSERT_NO_THROW(s.pop()); - ASSERT_NO_THROW(result = s.check()); - ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat); + std::shared_ptr manager(new storm::expressions::ExpressionManager()); + + storm::solver::Z3SmtSolver s(*manager); + storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::Unknown; + + storm::expressions::Expression expr1 = manager->boolean(true); + storm::expressions::Expression expr2 = manager->boolean(false); + storm::expressions::Expression expr3 = manager->boolean(false); + + ASSERT_NO_THROW(s.add(expr1)); + ASSERT_NO_THROW(result = s.check()); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat); + ASSERT_NO_THROW(s.push()); + ASSERT_NO_THROW(s.add(expr2)); + ASSERT_NO_THROW(result = s.check()); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat); + ASSERT_NO_THROW(s.pop()); + ASSERT_NO_THROW(result = s.check()); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat); + ASSERT_NO_THROW(s.push()); + ASSERT_NO_THROW(s.add(expr2)); + ASSERT_NO_THROW(result = s.check()); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat); + ASSERT_NO_THROW(s.push()); + ASSERT_NO_THROW(s.add(expr3)); + ASSERT_NO_THROW(result = s.check()); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat); + ASSERT_NO_THROW(s.pop(2)); + ASSERT_NO_THROW(result = s.check()); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat); + ASSERT_NO_THROW(s.reset()); + + storm::expressions::Variable a = manager->declareIntegerVariable("a"); + storm::expressions::Variable b = manager->declareIntegerVariable("b"); + storm::expressions::Variable c = manager->declareIntegerVariable("c"); + storm::expressions::Expression exprFormula = a >= manager->integer(0) && a < manager->integer(5) && b > manager->integer(7) && c == (a + b - manager->integer(1)) && b + a > c; + storm::expressions::Expression exprFormula2 = c > a + b + manager->integer(1); + + ASSERT_NO_THROW(s.add(exprFormula)); + ASSERT_NO_THROW(result = s.check()); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat); + ASSERT_NO_THROW(s.push()); + ASSERT_NO_THROW(s.add(exprFormula2)); + ASSERT_NO_THROW(result = s.check()); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat); + ASSERT_NO_THROW(s.pop()); + ASSERT_NO_THROW(result = s.check()); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat); } TEST(Z3SmtSolver, Assumptions) { - storm::solver::Z3SmtSolver s; - storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::Unknown; - - storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a"); - storm::expressions::Expression b = storm::expressions::Expression::createIntegerVariable("b"); - storm::expressions::Expression c = storm::expressions::Expression::createIntegerVariable("c"); - storm::expressions::Expression exprFormula = a >= storm::expressions::Expression::createIntegerLiteral(0) - && a < storm::expressions::Expression::createIntegerLiteral(5) - && b > storm::expressions::Expression::createIntegerLiteral(7) - && c == (a * b) - && b + a > c; - storm::expressions::Expression f2 = storm::expressions::Expression::createBooleanVariable("f2"); - storm::expressions::Expression exprFormula2 = f2.implies(a >= storm::expressions::Expression::createIntegerLiteral(2)); - - ASSERT_NO_THROW(s.add(exprFormula)); - ASSERT_NO_THROW(result = s.check()); - ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat); - ASSERT_NO_THROW(s.add(exprFormula2)); - ASSERT_NO_THROW(result = s.check()); - ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat); - ASSERT_NO_THROW(result = s.checkWithAssumptions({f2})); - ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat); - ASSERT_NO_THROW(result = s.check()); - ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat); - ASSERT_NO_THROW(result = s.checkWithAssumptions({ !f2 })); - ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat); + std::shared_ptr manager(new storm::expressions::ExpressionManager()); + + storm::solver::Z3SmtSolver s(*manager); + storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::Unknown; + + storm::expressions::Variable a = manager->declareIntegerVariable("a"); + storm::expressions::Variable b = manager->declareIntegerVariable("b"); + storm::expressions::Variable c = manager->declareIntegerVariable("c"); + storm::expressions::Expression exprFormula = a >= manager->integer(0) && a < manager->integer(5) && b > manager->integer(7) && c == a + b - manager->integer(1) && b + a > c; + storm::expressions::Variable f2 = manager->declareBooleanVariable("f2"); + storm::expressions::Expression exprFormula2 = storm::expressions::implies(f2, c > a + b + manager->integer(1)); + + ASSERT_NO_THROW(s.add(exprFormula)); + ASSERT_NO_THROW(result = s.check()); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat); + ASSERT_NO_THROW(s.add(exprFormula2)); + ASSERT_NO_THROW(result = s.check()); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat); + ASSERT_NO_THROW(result = s.checkWithAssumptions({f2})); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat); + ASSERT_NO_THROW(result = s.check()); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat); + ASSERT_NO_THROW(result = s.checkWithAssumptions({ !f2 })); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat); } TEST(Z3SmtSolver, GenerateModel) { - storm::solver::Z3SmtSolver s; - storm::solver::SmtSolver::CheckResult result; - - storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a"); - storm::expressions::Expression b = storm::expressions::Expression::createIntegerVariable("b"); - storm::expressions::Expression c = storm::expressions::Expression::createIntegerVariable("c"); - storm::expressions::Expression exprFormula = a > storm::expressions::Expression::createIntegerLiteral(0) - && a < storm::expressions::Expression::createIntegerLiteral(5) - && b > storm::expressions::Expression::createIntegerLiteral(7) - && c == (a * b) - && b + a > c; - - s.add(exprFormula); - result = s.check(); - ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat); + std::shared_ptr manager(new storm::expressions::ExpressionManager()); + + storm::solver::Z3SmtSolver s(*manager); + storm::solver::SmtSolver::CheckResult result; + + storm::expressions::Variable a = manager->declareIntegerVariable("a"); + storm::expressions::Variable b = manager->declareIntegerVariable("b"); + storm::expressions::Variable c = manager->declareIntegerVariable("c"); + storm::expressions::Expression exprFormula = a > manager->integer(0) && a < manager->integer(5) && b > manager->integer(7) && c == a + b - manager->integer(1) && b + a > c; + + s.add(exprFormula); + result = s.check(); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat); std::shared_ptr model = s.getModel(); - int_fast64_t aEval = model->getIntegerValue("a"); - ASSERT_EQ(1, aEval); + int_fast64_t aEval = model->getIntegerValue(a); + int_fast64_t bEval = model->getIntegerValue(b); + int_fast64_t cEval = model->getIntegerValue(c); + ASSERT_TRUE(cEval == aEval + bEval - 1); } - TEST(Z3SmtSolver, AllSat) { - storm::solver::Z3SmtSolver s; - storm::solver::SmtSolver::CheckResult result; - - storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a"); - storm::expressions::Expression b = storm::expressions::Expression::createIntegerVariable("b"); - storm::expressions::Expression x = storm::expressions::Expression::createBooleanVariable("x"); - storm::expressions::Expression y = storm::expressions::Expression::createBooleanVariable("y"); - storm::expressions::Expression z = storm::expressions::Expression::createBooleanVariable("z"); - storm::expressions::Expression exprFormula1 = x.implies(a > storm::expressions::Expression::createIntegerLiteral(5)); - storm::expressions::Expression exprFormula2 = y.implies(a < storm::expressions::Expression::createIntegerLiteral(5)); - storm::expressions::Expression exprFormula3 = z.implies(b < storm::expressions::Expression::createIntegerLiteral(5)); - - s.add(exprFormula1); - s.add(exprFormula2); - s.add(exprFormula3); - - std::vector valuations = s.allSat({x,y}); - - ASSERT_TRUE(valuations.size() == 3); - for (int i = 0; i < valuations.size(); ++i) { - ASSERT_EQ(valuations[i].getNumberOfIdentifiers(), 2); - ASSERT_TRUE(valuations[i].containsBooleanIdentifier("x")); - ASSERT_TRUE(valuations[i].containsBooleanIdentifier("y")); - } - for (int i = 0; i < valuations.size(); ++i) { - ASSERT_FALSE(valuations[i].getBooleanValue("x") && valuations[i].getBooleanValue("y")); + std::shared_ptr manager(new storm::expressions::ExpressionManager()); + + storm::solver::Z3SmtSolver s(*manager); + storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::Unknown; + + storm::expressions::Variable a = manager->declareIntegerVariable("a"); + storm::expressions::Variable b = manager->declareIntegerVariable("b"); + storm::expressions::Variable x = manager->declareBooleanVariable("x"); + storm::expressions::Variable y = manager->declareBooleanVariable("y"); + storm::expressions::Variable z = manager->declareBooleanVariable("z"); + storm::expressions::Expression exprFormula1 = storm::expressions::implies(x, a > manager->integer(5)); + storm::expressions::Expression exprFormula2 = storm::expressions::implies(y, a < manager->integer(5)); + storm::expressions::Expression exprFormula3 = storm::expressions::implies(z, b < manager->integer(5)); + + s.add(exprFormula1); + s.add(exprFormula2); + s.add(exprFormula3); + + std::vector valuations = s.allSat({x,y}); + + ASSERT_TRUE(valuations.size() == 3); + for (int i = 0; i < valuations.size(); ++i) { + ASSERT_FALSE(valuations[i].getBooleanValue(x) && valuations[i].getBooleanValue(y)); - for (int j = i+1; j < valuations.size(); ++j) { - ASSERT_TRUE((valuations[i].getBooleanValue("x") != valuations[j].getBooleanValue("x")) || (valuations[i].getBooleanValue("y") != valuations[j].getBooleanValue("y"))); - } - } + for (int j = i+1; j < valuations.size(); ++j) { + ASSERT_TRUE((valuations[i].getBooleanValue(x) != valuations[j].getBooleanValue(x)) || (valuations[i].getBooleanValue(y) != valuations[j].getBooleanValue(y))); + } + } } TEST(Z3SmtSolver, UnsatAssumptions) { - storm::solver::Z3SmtSolver s; - storm::solver::SmtSolver::CheckResult result; - - storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a"); - storm::expressions::Expression b = storm::expressions::Expression::createIntegerVariable("b"); - storm::expressions::Expression c = storm::expressions::Expression::createIntegerVariable("c"); - storm::expressions::Expression exprFormula = a >= storm::expressions::Expression::createIntegerLiteral(0) - && a < storm::expressions::Expression::createIntegerLiteral(5) - && b > storm::expressions::Expression::createIntegerLiteral(7) - && c == (a * b) - && b + a > c; - storm::expressions::Expression f2 = storm::expressions::Expression::createBooleanVariable("f2"); - storm::expressions::Expression exprFormula2 = f2.implies(a >= storm::expressions::Expression::createIntegerLiteral(2)); - - s.add(exprFormula); - s.add(exprFormula2); - result = s.checkWithAssumptions({ f2 }); - ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat); - std::vector unsatCore = s.getUnsatAssumptions(); - ASSERT_EQ(unsatCore.size(), 1); - ASSERT_TRUE(unsatCore[0].isVariable()); - ASSERT_STREQ("f2", unsatCore[0].getIdentifier().c_str()); + std::shared_ptr manager(new storm::expressions::ExpressionManager()); + + storm::solver::Z3SmtSolver s(*manager); + storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::Unknown; + + storm::expressions::Variable a = manager->declareIntegerVariable("a"); + storm::expressions::Variable b = manager->declareIntegerVariable("b"); + storm::expressions::Variable c = manager->declareIntegerVariable("c"); + storm::expressions::Expression exprFormula = a >= manager->integer(0) && a < manager->integer(5) && b > manager->integer(7) && c == a + b - manager->integer(1) && b + a > c; + storm::expressions::Variable f2 = manager->declareBooleanVariable("f2"); + storm::expressions::Expression exprFormula2 = storm::expressions::implies(f2, c > a + b + manager->integer(1)); + + s.add(exprFormula); + s.add(exprFormula2); + result = s.checkWithAssumptions({ f2 }); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat); + std::vector unsatCore = s.getUnsatAssumptions(); + ASSERT_EQ(unsatCore.size(), 1); + ASSERT_TRUE(unsatCore[0].isVariable()); + ASSERT_STREQ("f2", unsatCore[0].getIdentifier().c_str()); } #endif \ No newline at end of file diff --git a/test/functional/storage/CuddDdTest.cpp b/test/functional/storage/CuddDdTest.cpp index e95348625..52760783c 100644 --- a/test/functional/storage/CuddDdTest.cpp +++ b/test/functional/storage/CuddDdTest.cpp @@ -55,12 +55,12 @@ TEST(CuddDdManager, AddGetMetaVariableTest) { TEST(CuddDdManager, EncodingTest) { std::shared_ptr> manager(new storm::dd::DdManager()); - manager->addMetaVariable("x", 1, 9); + std::pair x = manager->addMetaVariable("x", 1, 9); storm::dd::Dd encoding; - ASSERT_THROW(encoding = manager->getEncoding("x", 0), storm::exceptions::InvalidArgumentException); - ASSERT_THROW(encoding = manager->getEncoding("x", 10), storm::exceptions::InvalidArgumentException); - ASSERT_NO_THROW(encoding = manager->getEncoding("x", 4)); + ASSERT_THROW(encoding = manager->getEncoding(x.first, 0), storm::exceptions::InvalidArgumentException); + ASSERT_THROW(encoding = manager->getEncoding(x.first, 10), storm::exceptions::InvalidArgumentException); + ASSERT_NO_THROW(encoding = manager->getEncoding(x.first, 4)); EXPECT_EQ(1, encoding.getNonZeroCount()); EXPECT_EQ(6, encoding.getNodeCount()); EXPECT_EQ(2, encoding.getLeafCount()); @@ -68,11 +68,11 @@ TEST(CuddDdManager, EncodingTest) { TEST(CuddDdManager, RangeTest) { std::shared_ptr> manager(new storm::dd::DdManager()); - ASSERT_NO_THROW(manager->addMetaVariable("x", 1, 9)); + std::pair x; + ASSERT_NO_THROW(x = manager->addMetaVariable("x", 1, 9)); storm::dd::Dd range; - ASSERT_THROW(range = manager->getRange("y"), storm::exceptions::InvalidArgumentException); - ASSERT_NO_THROW(range = manager->getRange("x")); + ASSERT_NO_THROW(range = manager->getRange(x.first)); EXPECT_EQ(9, range.getNonZeroCount()); EXPECT_EQ(2, range.getLeafCount()); @@ -81,11 +81,10 @@ TEST(CuddDdManager, RangeTest) { TEST(CuddDdManager, IdentityTest) { std::shared_ptr> manager(new storm::dd::DdManager()); - manager->addMetaVariable("x", 1, 9); + std::pair x = manager->addMetaVariable("x", 1, 9); storm::dd::Dd range; - ASSERT_THROW(range = manager->getIdentity("y"), storm::exceptions::InvalidArgumentException); - ASSERT_NO_THROW(range = manager->getIdentity("x")); + ASSERT_NO_THROW(range = manager->getIdentity(x.first)); EXPECT_EQ(9, range.getNonZeroCount()); EXPECT_EQ(10, range.getLeafCount()); @@ -94,7 +93,7 @@ TEST(CuddDdManager, IdentityTest) { TEST(CuddDd, OperatorTest) { std::shared_ptr> manager(new storm::dd::DdManager()); - manager->addMetaVariable("x", 1, 9); + std::pair x = manager->addMetaVariable("x", 1, 9); EXPECT_TRUE(manager->getZero() == manager->getZero()); EXPECT_FALSE(manager->getZero() == manager->getOne()); @@ -136,7 +135,7 @@ TEST(CuddDd, OperatorTest) { dd3 = dd1 || dd2; EXPECT_TRUE(dd3 == manager->getOne()); - dd1 = manager->getIdentity("x"); + dd1 = manager->getIdentity(x.first); dd2 = manager->getConstant(5); dd3 = dd1.equals(dd2); @@ -157,18 +156,18 @@ TEST(CuddDd, OperatorTest) { dd3 = dd1.greaterOrEqual(dd2); EXPECT_EQ(5, dd3.getNonZeroCount()); - dd3 = (manager->getEncoding("x", 2)).ite(dd2, dd1); + dd3 = (manager->getEncoding(x.first, 2)).ite(dd2, dd1); dd4 = dd3.less(dd2); EXPECT_EQ(10, dd4.getNonZeroCount()); dd4 = dd3.minimum(dd1); - dd4 *= manager->getEncoding("x", 2); - dd4 = dd4.sumAbstract({"x"}); + dd4 *= manager->getEncoding(x.first, 2); + dd4 = dd4.sumAbstract({x.first}); EXPECT_EQ(2, dd4.getValue()); dd4 = dd3.maximum(dd1); - dd4 *= manager->getEncoding("x", 2); - dd4 = dd4.sumAbstract({"x"}); + dd4 *= manager->getEncoding(x.first, 2); + dd4 = dd4.sumAbstract({x.first}); EXPECT_EQ(5, dd4.getValue()); dd1 = manager->getConstant(0.01); @@ -179,45 +178,45 @@ TEST(CuddDd, OperatorTest) { TEST(CuddDd, AbstractionTest) { std::shared_ptr> manager(new storm::dd::DdManager()); - manager->addMetaVariable("x", 1, 9); + std::pair x = manager->addMetaVariable("x", 1, 9); storm::dd::Dd dd1; storm::dd::Dd dd2; storm::dd::Dd dd3; - dd1 = manager->getIdentity("x"); + dd1 = manager->getIdentity(x.first); dd2 = manager->getConstant(5); dd3 = dd1.equals(dd2); EXPECT_EQ(1, dd3.getNonZeroCount()); - ASSERT_THROW(dd3 = dd3.existsAbstract({"x'"}), storm::exceptions::InvalidArgumentException); - ASSERT_NO_THROW(dd3 = dd3.existsAbstract({"x"})); + ASSERT_THROW(dd3 = dd3.existsAbstract({x.second}), storm::exceptions::InvalidArgumentException); + ASSERT_NO_THROW(dd3 = dd3.existsAbstract({x.first})); EXPECT_EQ(1, dd3.getNonZeroCount()); EXPECT_EQ(1, dd3.getMax()); dd3 = dd1.equals(dd2); dd3 *= manager->getConstant(3); EXPECT_EQ(1, dd3.getNonZeroCount()); - ASSERT_THROW(dd3 = dd3.existsAbstract({"x'"}), storm::exceptions::InvalidArgumentException); - ASSERT_NO_THROW(dd3 = dd3.existsAbstract({"x"})); + ASSERT_THROW(dd3 = dd3.existsAbstract({x.second}), storm::exceptions::InvalidArgumentException); + ASSERT_NO_THROW(dd3 = dd3.existsAbstract({x.first})); EXPECT_TRUE(dd3 == manager->getZero()); dd3 = dd1.equals(dd2); dd3 *= manager->getConstant(3); - ASSERT_THROW(dd3 = dd3.sumAbstract({"x'"}), storm::exceptions::InvalidArgumentException); - ASSERT_NO_THROW(dd3 = dd3.sumAbstract({"x"})); + ASSERT_THROW(dd3 = dd3.sumAbstract({x.second}), storm::exceptions::InvalidArgumentException); + ASSERT_NO_THROW(dd3 = dd3.sumAbstract({x.first})); EXPECT_EQ(1, dd3.getNonZeroCount()); EXPECT_EQ(3, dd3.getMax()); dd3 = dd1.equals(dd2); dd3 *= manager->getConstant(3); - ASSERT_THROW(dd3 = dd3.minAbstract({"x'"}), storm::exceptions::InvalidArgumentException); - ASSERT_NO_THROW(dd3 = dd3.minAbstract({"x"})); + ASSERT_THROW(dd3 = dd3.minAbstract({x.second}), storm::exceptions::InvalidArgumentException); + ASSERT_NO_THROW(dd3 = dd3.minAbstract({x.first})); EXPECT_EQ(0, dd3.getNonZeroCount()); EXPECT_EQ(0, dd3.getMax()); dd3 = dd1.equals(dd2); dd3 *= manager->getConstant(3); - ASSERT_THROW(dd3 = dd3.maxAbstract({"x'"}), storm::exceptions::InvalidArgumentException); - ASSERT_NO_THROW(dd3 = dd3.maxAbstract({"x"})); + ASSERT_THROW(dd3 = dd3.maxAbstract({x.second}), storm::exceptions::InvalidArgumentException); + ASSERT_NO_THROW(dd3 = dd3.maxAbstract({x.first})); EXPECT_EQ(1, dd3.getNonZeroCount()); EXPECT_EQ(3, dd3.getMax()); } @@ -225,55 +224,55 @@ TEST(CuddDd, AbstractionTest) { TEST(CuddDd, SwapTest) { std::shared_ptr> manager(new storm::dd::DdManager()); - manager->addMetaVariable("x", 1, 9); - manager->addMetaVariable("z", 2, 8); + std::pair x = manager->addMetaVariable("x", 1, 9); + std::pair z = manager->addMetaVariable("z", 2, 8); storm::dd::Dd dd1; storm::dd::Dd dd2; - dd1 = manager->getIdentity("x"); - ASSERT_THROW(dd1.swapVariables({std::make_pair("x", "z")}), storm::exceptions::InvalidArgumentException); - ASSERT_NO_THROW(dd1.swapVariables({std::make_pair("x", "x'")})); - EXPECT_TRUE(dd1 == manager->getIdentity("x'")); + dd1 = manager->getIdentity(x.first); + ASSERT_THROW(dd1.swapVariables({std::make_pair(x.first, z.first)}), storm::exceptions::InvalidArgumentException); + ASSERT_NO_THROW(dd1.swapVariables({std::make_pair(x.first, x.second)})); + EXPECT_TRUE(dd1 == manager->getIdentity(x.second)); } TEST(CuddDd, MultiplyMatrixTest) { std::shared_ptr> manager(new storm::dd::DdManager()); - manager->addMetaVariable("x", 1, 9); + std::pair x = manager->addMetaVariable("x", 1, 9); - storm::dd::Dd dd1 = manager->getIdentity("x").equals(manager->getIdentity("x'")); - storm::dd::Dd dd2 = manager->getRange("x'"); + storm::dd::Dd dd1 = manager->getIdentity(x.first).equals(manager->getIdentity(x.second)); + storm::dd::Dd dd2 = manager->getRange(x.second); storm::dd::Dd dd3; dd1 *= manager->getConstant(2); - ASSERT_NO_THROW(dd3 = dd1.multiplyMatrix(dd2, {"x'"})); - ASSERT_NO_THROW(dd3.swapVariables({std::make_pair("x", "x'")})); + ASSERT_NO_THROW(dd3 = dd1.multiplyMatrix(dd2, {x.second})); + ASSERT_NO_THROW(dd3.swapVariables({std::make_pair(x.first, x.second)})); EXPECT_TRUE(dd3 == dd2 * manager->getConstant(2)); } TEST(CuddDd, GetSetValueTest) { std::shared_ptr> manager(new storm::dd::DdManager()); - manager->addMetaVariable("x", 1, 9); + std::pair x = manager->addMetaVariable("x", 1, 9); storm::dd::Dd dd1 = manager->getOne(); - ASSERT_NO_THROW(dd1.setValue("x", 4, 2)); + ASSERT_NO_THROW(dd1.setValue(x.first, 4, 2)); EXPECT_EQ(2, dd1.getLeafCount()); - std::map metaVariableToValueMap; - metaVariableToValueMap.emplace("x", 1); + std::map metaVariableToValueMap; + metaVariableToValueMap.emplace(x.first, 1); EXPECT_EQ(1, dd1.getValue(metaVariableToValueMap)); metaVariableToValueMap.clear(); - metaVariableToValueMap.emplace("x", 4); + metaVariableToValueMap.emplace(x.first, 4); EXPECT_EQ(2, dd1.getValue(metaVariableToValueMap)); } TEST(CuddDd, ForwardIteratorTest) { std::shared_ptr> manager(new storm::dd::DdManager()); - manager->addMetaVariable("x", 1, 9); - manager->addMetaVariable("y", 0, 3); + std::pair x = manager->addMetaVariable("x", 1, 9); + std::pair y = manager->addMetaVariable("y", 0, 3); storm::dd::Dd dd; - ASSERT_NO_THROW(dd = manager->getRange("x")); + ASSERT_NO_THROW(dd = manager->getRange(x.first)); storm::dd::DdForwardIterator it, ite; ASSERT_NO_THROW(it = dd.begin()); @@ -287,7 +286,7 @@ TEST(CuddDd, ForwardIteratorTest) { } EXPECT_EQ(9, numberOfValuations); - dd = manager->getRange("x"); + dd = manager->getRange(x.first); dd = dd.ite(manager->getOne(), manager->getOne()); ASSERT_NO_THROW(it = dd.begin()); ASSERT_NO_THROW(ite = dd.end()); @@ -310,80 +309,81 @@ TEST(CuddDd, ForwardIteratorTest) { EXPECT_EQ(1, numberOfValuations); } -TEST(CuddDd, ToExpressionTest) { - std::shared_ptr> manager(new storm::dd::DdManager()); - manager->addMetaVariable("x", 1, 9); - - storm::dd::Dd dd; - ASSERT_NO_THROW(dd = manager->getIdentity("x")); - - storm::expressions::Expression ddAsExpression; - ASSERT_NO_THROW(ddAsExpression = dd.toExpression()); - - storm::expressions::SimpleValuation valuation; - for (std::size_t bit = 0; bit < manager->getMetaVariable("x").getNumberOfDdVariables(); ++bit) { - valuation.addBooleanIdentifier("x." + std::to_string(bit)); - } - - storm::dd::DdMetaVariable const& metaVariable = manager->getMetaVariable("x"); - - for (auto valuationValuePair : dd) { - for (std::size_t i = 0; i < metaVariable.getNumberOfDdVariables(); ++i) { - // Check if the i-th bit is set or not and modify the valuation accordingly. - if (((valuationValuePair.first.getIntegerValue("x") - metaVariable.getLow()) & (1ull << (metaVariable.getNumberOfDdVariables() - i - 1))) != 0) { - valuation.setBooleanValue("x." + std::to_string(i), true); - } else { - valuation.setBooleanValue("x." + std::to_string(i), false); - } - } - - // At this point, the constructed valuation should make the expression obtained from the DD evaluate to the very - // same value as the current value obtained from the DD. - EXPECT_EQ(valuationValuePair.second, ddAsExpression.evaluateAsDouble(&valuation)); - } - - storm::expressions::Expression mintermExpression = dd.getMintermExpression(); - - // Check whether all minterms are covered. - for (auto valuationValuePair : dd) { - for (std::size_t i = 0; i < metaVariable.getNumberOfDdVariables(); ++i) { - // Check if the i-th bit is set or not and modify the valuation accordingly. - if (((valuationValuePair.first.getIntegerValue("x") - metaVariable.getLow()) & (1ull << (metaVariable.getNumberOfDdVariables() - i - 1))) != 0) { - valuation.setBooleanValue("x." + std::to_string(i), true); - } else { - valuation.setBooleanValue("x." + std::to_string(i), false); - } - } - - // At this point, the constructed valuation should make the expression obtained from the DD evaluate to the very - // same value as the current value obtained from the DD. - EXPECT_TRUE(mintermExpression.evaluateAsBool(&valuation)); - } - - // Now check no additional minterms are covered. - dd = !dd; - for (auto valuationValuePair : dd) { - for (std::size_t i = 0; i < metaVariable.getNumberOfDdVariables(); ++i) { - // Check if the i-th bit is set or not and modify the valuation accordingly. - if (((valuationValuePair.first.getIntegerValue("x") - metaVariable.getLow()) & (1ull << (metaVariable.getNumberOfDdVariables() - i - 1))) != 0) { - valuation.setBooleanValue("x." + std::to_string(i), true); - } else { - valuation.setBooleanValue("x." + std::to_string(i), false); - } - } - - // At this point, the constructed valuation should make the expression obtained from the DD evaluate to the very - // same value as the current value obtained from the DD. - EXPECT_FALSE(mintermExpression.evaluateAsBool(&valuation)); - } -} +// FIXME: make toExpression work again and then fix this test. +//TEST(CuddDd, ToExpressionTest) { +// std::shared_ptr> manager(new storm::dd::DdManager()); +// std::pair x = manager->addMetaVariable("x", 1, 9); +// +// storm::dd::Dd dd; +// ASSERT_NO_THROW(dd = manager->getIdentity(x.first)); +// +// storm::expressions::Expression ddAsExpression; +// ASSERT_NO_THROW(ddAsExpression = dd.toExpression()); +// +// storm::expressions::SimpleValuation valuation; +// for (std::size_t bit = 0; bit < manager->getMetaVariable(x.first).getNumberOfDdVariables(); ++bit) { +// valuation.addBooleanIdentifier("x." + std::to_string(bit)); +// } +// +// storm::dd::DdMetaVariable const& metaVariable = manager->getMetaVariable("x"); +// +// for (auto valuationValuePair : dd) { +// for (std::size_t i = 0; i < metaVariable.getNumberOfDdVariables(); ++i) { +// // Check if the i-th bit is set or not and modify the valuation accordingly. +// if (((valuationValuePair.first.getIntegerValue("x") - metaVariable.getLow()) & (1ull << (metaVariable.getNumberOfDdVariables() - i - 1))) != 0) { +// valuation.setBooleanValue("x." + std::to_string(i), true); +// } else { +// valuation.setBooleanValue("x." + std::to_string(i), false); +// } +// } +// +// // At this point, the constructed valuation should make the expression obtained from the DD evaluate to the very +// // same value as the current value obtained from the DD. +// EXPECT_EQ(valuationValuePair.second, ddAsExpression.evaluateAsDouble(&valuation)); +// } +// +// storm::expressions::Expression mintermExpression = dd.getMintermExpression(); +// +// // Check whether all minterms are covered. +// for (auto valuationValuePair : dd) { +// for (std::size_t i = 0; i < metaVariable.getNumberOfDdVariables(); ++i) { +// // Check if the i-th bit is set or not and modify the valuation accordingly. +// if (((valuationValuePair.first.getIntegerValue("x") - metaVariable.getLow()) & (1ull << (metaVariable.getNumberOfDdVariables() - i - 1))) != 0) { +// valuation.setBooleanValue("x." + std::to_string(i), true); +// } else { +// valuation.setBooleanValue("x." + std::to_string(i), false); +// } +// } +// +// // At this point, the constructed valuation should make the expression obtained from the DD evaluate to the very +// // same value as the current value obtained from the DD. +// EXPECT_TRUE(mintermExpression.evaluateAsBool(&valuation)); +// } +// +// // Now check no additional minterms are covered. +// dd = !dd; +// for (auto valuationValuePair : dd) { +// for (std::size_t i = 0; i < metaVariable.getNumberOfDdVariables(); ++i) { +// // Check if the i-th bit is set or not and modify the valuation accordingly. +// if (((valuationValuePair.first.getIntegerValue("x") - metaVariable.getLow()) & (1ull << (metaVariable.getNumberOfDdVariables() - i - 1))) != 0) { +// valuation.setBooleanValue("x." + std::to_string(i), true); +// } else { +// valuation.setBooleanValue("x." + std::to_string(i), false); +// } +// } +// +// // At this point, the constructed valuation should make the expression obtained from the DD evaluate to the very +// // same value as the current value obtained from the DD. +// EXPECT_FALSE(mintermExpression.evaluateAsBool(&valuation)); +// } +//} TEST(CuddDd, OddTest) { std::shared_ptr> manager(new storm::dd::DdManager()); - manager->addMetaVariable("a"); - manager->addMetaVariable("x", 1, 9); + std::pair a = manager->addMetaVariable("a"); + std::pair x = manager->addMetaVariable("x", 1, 9); - storm::dd::Dd dd = manager->getIdentity("x"); + storm::dd::Dd dd = manager->getIdentity(x.first); storm::dd::Odd odd; ASSERT_NO_THROW(odd = storm::dd::Odd(dd)); EXPECT_EQ(9, odd.getTotalOffset()); @@ -397,25 +397,25 @@ TEST(CuddDd, OddTest) { } // Create a non-trivial matrix. - dd = manager->getIdentity("x").equals(manager->getIdentity("x'")) * manager->getRange("x"); - dd += manager->getEncoding("x", 1) * manager->getRange("x'") + manager->getEncoding("x'", 1) * manager->getRange("x"); + dd = manager->getIdentity(x.first).equals(manager->getIdentity(x.second)) * manager->getRange(x.first); + dd += manager->getEncoding(x.first, 1) * manager->getRange(x.second) + manager->getEncoding(x.second, 1) * manager->getRange(x.first); // Create the ODDs. storm::dd::Odd rowOdd; - ASSERT_NO_THROW(rowOdd = storm::dd::Odd(manager->getRange("x"))); + ASSERT_NO_THROW(rowOdd = storm::dd::Odd(manager->getRange(x.first))); storm::dd::Odd columnOdd; - ASSERT_NO_THROW(columnOdd = storm::dd::Odd(manager->getRange("x'"))); + ASSERT_NO_THROW(columnOdd = storm::dd::Odd(manager->getRange(x.second))); // Try to translate the matrix. storm::storage::SparseMatrix matrix; - ASSERT_NO_THROW(matrix = dd.toMatrix({"x"}, {"x'"}, rowOdd, columnOdd)); + ASSERT_NO_THROW(matrix = dd.toMatrix({x.first}, {x.second}, rowOdd, columnOdd)); EXPECT_EQ(9, matrix.getRowCount()); EXPECT_EQ(9, matrix.getColumnCount()); EXPECT_EQ(25, matrix.getNonzeroEntryCount()); - dd = manager->getRange("x") * manager->getRange("x'") * manager->getEncoding("a", 0).ite(dd, dd + manager->getConstant(1)); - ASSERT_NO_THROW(matrix = dd.toMatrix({"x"}, {"x'"}, {"a"}, rowOdd, columnOdd)); + dd = manager->getRange(x.first) * manager->getRange(x.second) * manager->getEncoding(a.first, 0).ite(dd, dd + manager->getConstant(1)); + ASSERT_NO_THROW(matrix = dd.toMatrix({x.first}, {x.second}, {a.first}, rowOdd, columnOdd)); EXPECT_EQ(18, matrix.getRowCount()); EXPECT_EQ(9, matrix.getRowGroupCount()); EXPECT_EQ(9, matrix.getColumnCount()); diff --git a/test/functional/storage/ExpressionTest.cpp b/test/functional/storage/ExpressionTest.cpp index 642456995..9e45105c0 100644 --- a/test/functional/storage/ExpressionTest.cpp +++ b/test/functional/storage/ExpressionTest.cpp @@ -3,287 +3,296 @@ #include "gtest/gtest.h" #include "src/storage/expressions/Expression.h" +#include "src/storage/expressions/ExpressionManager.h" #include "src/storage/expressions/LinearityCheckVisitor.h" #include "src/storage/expressions/SimpleValuation.h" #include "src/exceptions/InvalidTypeException.h" TEST(Expression, FactoryMethodTest) { - EXPECT_NO_THROW(storm::expressions::Expression::createBooleanLiteral(true)); - EXPECT_NO_THROW(storm::expressions::Expression::createTrue()); - EXPECT_NO_THROW(storm::expressions::Expression::createFalse()); - EXPECT_NO_THROW(storm::expressions::Expression::createIntegerLiteral(3)); - EXPECT_NO_THROW(storm::expressions::Expression::createDoubleLiteral(3.14)); - EXPECT_NO_THROW(storm::expressions::Expression::createBooleanVariable("x")); - EXPECT_NO_THROW(storm::expressions::Expression::createIntegerVariable("y")); - EXPECT_NO_THROW(storm::expressions::Expression::createDoubleVariable("z")); + std::shared_ptr manager(new storm::expressions::ExpressionManager()); + EXPECT_NO_THROW(manager->boolean(true)); + EXPECT_NO_THROW(manager->boolean(false)); + EXPECT_NO_THROW(manager->integer(3)); + EXPECT_NO_THROW(manager->rational(3.14)); + EXPECT_NO_THROW(manager->declareBooleanVariable("x")); + EXPECT_NO_THROW(manager->declareIntegerVariable("y")); + EXPECT_NO_THROW(manager->declareRationalVariable("z")); } TEST(Expression, AccessorTest) { + std::shared_ptr manager(new storm::expressions::ExpressionManager()); + storm::expressions::Expression trueExpression; storm::expressions::Expression falseExpression; storm::expressions::Expression threeExpression; storm::expressions::Expression piExpression; storm::expressions::Expression boolVarExpression; storm::expressions::Expression intVarExpression; - storm::expressions::Expression doubleVarExpression; + storm::expressions::Expression rationalVarExpression; - ASSERT_NO_THROW(trueExpression = storm::expressions::Expression::createTrue()); - ASSERT_NO_THROW(falseExpression = storm::expressions::Expression::createFalse()); - ASSERT_NO_THROW(threeExpression = storm::expressions::Expression::createIntegerLiteral(3)); - ASSERT_NO_THROW(piExpression = storm::expressions::Expression::createDoubleLiteral(3.14)); - ASSERT_NO_THROW(boolVarExpression = storm::expressions::Expression::createBooleanVariable("x")); - ASSERT_NO_THROW(intVarExpression = storm::expressions::Expression::createIntegerVariable("y")); - ASSERT_NO_THROW(doubleVarExpression = storm::expressions::Expression::createDoubleVariable("z")); + ASSERT_NO_THROW(trueExpression = manager->boolean(true)); + ASSERT_NO_THROW(falseExpression = manager->boolean(false)); + ASSERT_NO_THROW(threeExpression = manager->integer(3)); + ASSERT_NO_THROW(piExpression = manager->rational(3.14)); + ASSERT_NO_THROW(boolVarExpression = manager->declareBooleanVariable("x")); + ASSERT_NO_THROW(intVarExpression = manager->declareIntegerVariable("y")); + ASSERT_NO_THROW(rationalVarExpression = manager->declareRationalVariable("z")); - EXPECT_TRUE(trueExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); + EXPECT_TRUE(trueExpression.hasBooleanType()); EXPECT_TRUE(trueExpression.isLiteral()); EXPECT_TRUE(trueExpression.isTrue()); EXPECT_FALSE(trueExpression.isFalse()); - EXPECT_TRUE(trueExpression.getVariables() == std::set()); + EXPECT_TRUE(trueExpression.getVariables() == std::set()); - EXPECT_TRUE(falseExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); + EXPECT_TRUE(falseExpression.hasBooleanType()); EXPECT_TRUE(falseExpression.isLiteral()); EXPECT_FALSE(falseExpression.isTrue()); EXPECT_TRUE(falseExpression.isFalse()); - EXPECT_TRUE(falseExpression.getVariables() == std::set()); + EXPECT_TRUE(falseExpression.getVariables() == std::set()); - EXPECT_TRUE(threeExpression.getReturnType() == storm::expressions::ExpressionReturnType::Int); + EXPECT_TRUE(threeExpression.hasIntegralType()); EXPECT_TRUE(threeExpression.isLiteral()); EXPECT_FALSE(threeExpression.isTrue()); EXPECT_FALSE(threeExpression.isFalse()); - EXPECT_TRUE(threeExpression.getVariables() == std::set()); + EXPECT_TRUE(threeExpression.getVariables() == std::set()); - EXPECT_TRUE(piExpression.getReturnType() == storm::expressions::ExpressionReturnType::Double); + EXPECT_TRUE(piExpression.hasRationalType()); EXPECT_TRUE(piExpression.isLiteral()); EXPECT_FALSE(piExpression.isTrue()); EXPECT_FALSE(piExpression.isFalse()); - EXPECT_TRUE(piExpression.getVariables() == std::set()); + EXPECT_TRUE(piExpression.getVariables() == std::set()); - EXPECT_TRUE(boolVarExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); + EXPECT_TRUE(boolVarExpression.hasBooleanType()); EXPECT_FALSE(boolVarExpression.isLiteral()); EXPECT_FALSE(boolVarExpression.isTrue()); EXPECT_FALSE(boolVarExpression.isFalse()); - EXPECT_TRUE(boolVarExpression.getVariables() == std::set({"x"})); + EXPECT_TRUE(boolVarExpression.getVariables() == std::set({manager->getVariable("x")})); - EXPECT_TRUE(intVarExpression.getReturnType() == storm::expressions::ExpressionReturnType::Int); + EXPECT_TRUE(intVarExpression.hasIntegralType()); EXPECT_FALSE(intVarExpression.isLiteral()); EXPECT_FALSE(intVarExpression.isTrue()); EXPECT_FALSE(intVarExpression.isFalse()); - EXPECT_TRUE(intVarExpression.getVariables() == std::set({"y"})); + EXPECT_TRUE(intVarExpression.getVariables() == std::set({manager->getVariable("y")})); - EXPECT_TRUE(doubleVarExpression.getReturnType() == storm::expressions::ExpressionReturnType::Double); - EXPECT_FALSE(doubleVarExpression.isLiteral()); - EXPECT_FALSE(doubleVarExpression.isTrue()); - EXPECT_FALSE(doubleVarExpression.isFalse()); - EXPECT_TRUE(doubleVarExpression.getVariables() == std::set({"z"})); + EXPECT_TRUE(rationalVarExpression.hasRationalType()); + EXPECT_FALSE(rationalVarExpression.isLiteral()); + EXPECT_FALSE(rationalVarExpression.isTrue()); + EXPECT_FALSE(rationalVarExpression.isFalse()); + EXPECT_TRUE(rationalVarExpression.getVariables() == std::set({manager->getVariable("z")})); } TEST(Expression, OperatorTest) { + std::shared_ptr manager(new storm::expressions::ExpressionManager()); + storm::expressions::Expression trueExpression; storm::expressions::Expression falseExpression; storm::expressions::Expression threeExpression; storm::expressions::Expression piExpression; storm::expressions::Expression boolVarExpression; storm::expressions::Expression intVarExpression; - storm::expressions::Expression doubleVarExpression; + storm::expressions::Expression rationalVarExpression; - ASSERT_NO_THROW(trueExpression = storm::expressions::Expression::createTrue()); - ASSERT_NO_THROW(falseExpression = storm::expressions::Expression::createFalse()); - ASSERT_NO_THROW(threeExpression = storm::expressions::Expression::createIntegerLiteral(3)); - ASSERT_NO_THROW(piExpression = storm::expressions::Expression::createDoubleLiteral(3.14)); - ASSERT_NO_THROW(boolVarExpression = storm::expressions::Expression::createBooleanVariable("x")); - ASSERT_NO_THROW(intVarExpression = storm::expressions::Expression::createIntegerVariable("y")); - ASSERT_NO_THROW(doubleVarExpression = storm::expressions::Expression::createDoubleVariable("z")); + ASSERT_NO_THROW(trueExpression = manager->boolean(true)); + ASSERT_NO_THROW(falseExpression = manager->boolean(false)); + ASSERT_NO_THROW(threeExpression = manager->integer(3)); + ASSERT_NO_THROW(piExpression = manager->rational(3.14)); + ASSERT_NO_THROW(boolVarExpression = manager->declareBooleanVariable("x")); + ASSERT_NO_THROW(intVarExpression = manager->declareIntegerVariable("y")); + ASSERT_NO_THROW(rationalVarExpression = manager->declareRationalVariable("z")); storm::expressions::Expression tempExpression; - ASSERT_THROW(tempExpression = trueExpression.ite(falseExpression, piExpression), storm::exceptions::InvalidTypeException); - ASSERT_NO_THROW(tempExpression = boolVarExpression.ite(threeExpression, doubleVarExpression)); - EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Double); - ASSERT_NO_THROW(tempExpression = boolVarExpression.ite(threeExpression, intVarExpression)); - EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Int); - ASSERT_NO_THROW(tempExpression = boolVarExpression.ite(trueExpression, falseExpression)); - EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); + ASSERT_THROW(tempExpression = storm::expressions::ite(trueExpression, falseExpression, piExpression), storm::exceptions::InvalidTypeException); + ASSERT_NO_THROW(tempExpression = storm::expressions::ite(boolVarExpression, threeExpression, rationalVarExpression)); + EXPECT_TRUE(tempExpression.hasRationalType()); + ASSERT_NO_THROW(tempExpression = storm::expressions::ite(boolVarExpression, threeExpression, intVarExpression)); + EXPECT_TRUE(tempExpression.hasIntegralType()); + ASSERT_NO_THROW(tempExpression = storm::expressions::ite(boolVarExpression, trueExpression, falseExpression)); + EXPECT_TRUE(tempExpression.hasBooleanType()); ASSERT_THROW(tempExpression = trueExpression + piExpression, storm::exceptions::InvalidTypeException); ASSERT_NO_THROW(tempExpression = threeExpression + threeExpression); - EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Int); + EXPECT_TRUE(tempExpression.hasIntegralType()); ASSERT_NO_THROW(tempExpression = threeExpression + piExpression); - EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Double); - ASSERT_NO_THROW(tempExpression = doubleVarExpression + doubleVarExpression); - EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Double); + EXPECT_TRUE(tempExpression.hasRationalType()); + ASSERT_NO_THROW(tempExpression = rationalVarExpression + rationalVarExpression); + EXPECT_TRUE(tempExpression.hasRationalType()); ASSERT_THROW(tempExpression = trueExpression - piExpression, storm::exceptions::InvalidTypeException); ASSERT_NO_THROW(tempExpression = threeExpression - threeExpression); - EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Int); + EXPECT_TRUE(tempExpression.hasIntegralType()); ASSERT_NO_THROW(tempExpression = threeExpression - piExpression); - EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Double); - ASSERT_NO_THROW(tempExpression = doubleVarExpression - doubleVarExpression); - EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Double); + EXPECT_TRUE(tempExpression.hasRationalType()); + ASSERT_NO_THROW(tempExpression = rationalVarExpression - rationalVarExpression); + EXPECT_TRUE(tempExpression.hasRationalType()); ASSERT_THROW(tempExpression = -trueExpression, storm::exceptions::InvalidTypeException); ASSERT_NO_THROW(tempExpression = -threeExpression); - EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Int); + EXPECT_TRUE(tempExpression.hasIntegralType()); ASSERT_NO_THROW(tempExpression = -piExpression); - EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Double); - ASSERT_NO_THROW(tempExpression = -doubleVarExpression); - EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Double); + EXPECT_TRUE(tempExpression.hasRationalType()); + ASSERT_NO_THROW(tempExpression = -rationalVarExpression); + EXPECT_TRUE(tempExpression.hasRationalType()); ASSERT_THROW(tempExpression = trueExpression * piExpression, storm::exceptions::InvalidTypeException); ASSERT_NO_THROW(tempExpression = threeExpression * threeExpression); - EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Int); + EXPECT_TRUE(tempExpression.hasIntegralType()); ASSERT_NO_THROW(tempExpression = threeExpression * piExpression); - EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Double); + EXPECT_TRUE(tempExpression.hasRationalType()); ASSERT_NO_THROW(tempExpression = intVarExpression * intVarExpression); - EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Int); + EXPECT_TRUE(tempExpression.hasIntegralType()); ASSERT_THROW(tempExpression = trueExpression / piExpression, storm::exceptions::InvalidTypeException); ASSERT_NO_THROW(tempExpression = threeExpression / threeExpression); - EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Int); + EXPECT_TRUE(tempExpression.hasIntegralType()); ASSERT_NO_THROW(tempExpression = threeExpression / piExpression); - EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Double); - ASSERT_NO_THROW(tempExpression = doubleVarExpression / intVarExpression); - EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Double); + EXPECT_TRUE(tempExpression.hasRationalType()); + ASSERT_NO_THROW(tempExpression = rationalVarExpression / intVarExpression); + EXPECT_TRUE(tempExpression.hasRationalType()); ASSERT_THROW(tempExpression = trueExpression && piExpression, storm::exceptions::InvalidTypeException); ASSERT_NO_THROW(tempExpression = trueExpression && falseExpression); - EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); + EXPECT_TRUE(tempExpression.hasBooleanType()); ASSERT_NO_THROW(tempExpression = boolVarExpression && boolVarExpression); - EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); + EXPECT_TRUE(tempExpression.hasBooleanType()); ASSERT_THROW(tempExpression = trueExpression || piExpression, storm::exceptions::InvalidTypeException); ASSERT_NO_THROW(tempExpression = trueExpression || falseExpression); - EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); + EXPECT_TRUE(tempExpression.hasBooleanType()); ASSERT_NO_THROW(tempExpression = boolVarExpression || boolVarExpression); - EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); + EXPECT_TRUE(tempExpression.hasBooleanType()); ASSERT_THROW(tempExpression = !threeExpression, storm::exceptions::InvalidTypeException); ASSERT_NO_THROW(tempExpression = !trueExpression); - EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); + EXPECT_TRUE(tempExpression.hasBooleanType()); ASSERT_NO_THROW(tempExpression = !boolVarExpression); - EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); + EXPECT_TRUE(tempExpression.hasBooleanType()); ASSERT_THROW(tempExpression = trueExpression == piExpression, storm::exceptions::InvalidTypeException); ASSERT_NO_THROW(tempExpression = threeExpression == threeExpression); - EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); - ASSERT_NO_THROW(tempExpression = intVarExpression == doubleVarExpression); - EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); + EXPECT_TRUE(tempExpression.hasBooleanType()); + ASSERT_NO_THROW(tempExpression = intVarExpression == rationalVarExpression); + EXPECT_TRUE(tempExpression.hasBooleanType()); ASSERT_THROW(tempExpression = trueExpression != piExpression, storm::exceptions::InvalidTypeException); ASSERT_NO_THROW(tempExpression = threeExpression != threeExpression); - EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); - ASSERT_NO_THROW(tempExpression = intVarExpression != doubleVarExpression); - EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); + EXPECT_TRUE(tempExpression.hasBooleanType()); + ASSERT_NO_THROW(tempExpression = intVarExpression != rationalVarExpression); + EXPECT_TRUE(tempExpression.hasBooleanType()); ASSERT_THROW(tempExpression = trueExpression > piExpression, storm::exceptions::InvalidTypeException); ASSERT_NO_THROW(tempExpression = threeExpression > threeExpression); - EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); - ASSERT_NO_THROW(tempExpression = intVarExpression > doubleVarExpression); - EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); + EXPECT_TRUE(tempExpression.hasBooleanType()); + ASSERT_NO_THROW(tempExpression = intVarExpression > rationalVarExpression); + EXPECT_TRUE(tempExpression.hasBooleanType()); ASSERT_THROW(tempExpression = trueExpression >= piExpression, storm::exceptions::InvalidTypeException); ASSERT_NO_THROW(tempExpression = threeExpression >= threeExpression); - EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); - ASSERT_NO_THROW(tempExpression = intVarExpression >= doubleVarExpression); - EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); + EXPECT_TRUE(tempExpression.hasBooleanType()); + ASSERT_NO_THROW(tempExpression = intVarExpression >= rationalVarExpression); + EXPECT_TRUE(tempExpression.hasBooleanType()); ASSERT_THROW(tempExpression = trueExpression < piExpression, storm::exceptions::InvalidTypeException); ASSERT_NO_THROW(tempExpression = threeExpression < threeExpression); - EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); - ASSERT_NO_THROW(tempExpression = intVarExpression < doubleVarExpression); - EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); + EXPECT_TRUE(tempExpression.hasBooleanType()); + ASSERT_NO_THROW(tempExpression = intVarExpression < rationalVarExpression); + EXPECT_TRUE(tempExpression.hasBooleanType()); ASSERT_THROW(tempExpression = trueExpression <= piExpression, storm::exceptions::InvalidTypeException); ASSERT_NO_THROW(tempExpression = threeExpression <= threeExpression); - EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); - ASSERT_NO_THROW(tempExpression = intVarExpression <= doubleVarExpression); - EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); - - ASSERT_THROW(tempExpression = storm::expressions::Expression::minimum(trueExpression, piExpression), storm::exceptions::InvalidTypeException); - ASSERT_NO_THROW(tempExpression = storm::expressions::Expression::minimum(threeExpression, threeExpression)); - EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Int); - ASSERT_NO_THROW(tempExpression = storm::expressions::Expression::minimum(intVarExpression, doubleVarExpression)); - EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Double); + EXPECT_TRUE(tempExpression.hasBooleanType()); + ASSERT_NO_THROW(tempExpression = intVarExpression <= rationalVarExpression); + EXPECT_TRUE(tempExpression.hasBooleanType()); + + ASSERT_THROW(tempExpression = storm::expressions::minimum(trueExpression, piExpression), storm::exceptions::InvalidTypeException); + ASSERT_NO_THROW(tempExpression = storm::expressions::minimum(threeExpression, threeExpression)); + EXPECT_TRUE(tempExpression.hasIntegralType()); + ASSERT_NO_THROW(tempExpression = storm::expressions::minimum(intVarExpression, rationalVarExpression)); + EXPECT_TRUE(tempExpression.hasRationalType()); - ASSERT_THROW(tempExpression = storm::expressions::Expression::maximum(trueExpression, piExpression), storm::exceptions::InvalidTypeException); - ASSERT_NO_THROW(tempExpression = storm::expressions::Expression::maximum(threeExpression, threeExpression)); - EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Int); - ASSERT_NO_THROW(tempExpression = storm::expressions::Expression::maximum(intVarExpression, doubleVarExpression)); - EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Double); - - ASSERT_THROW(tempExpression = trueExpression.implies(piExpression), storm::exceptions::InvalidTypeException); - ASSERT_NO_THROW(tempExpression = trueExpression.implies(falseExpression)); - EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); - ASSERT_NO_THROW(tempExpression = boolVarExpression.implies(boolVarExpression)); - EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); - - ASSERT_THROW(tempExpression = trueExpression.iff(piExpression), storm::exceptions::InvalidTypeException); - ASSERT_NO_THROW(tempExpression = trueExpression.iff(falseExpression)); - EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); - ASSERT_NO_THROW(tempExpression = boolVarExpression.iff(boolVarExpression)); - EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); + ASSERT_THROW(tempExpression = storm::expressions::maximum(trueExpression, piExpression), storm::exceptions::InvalidTypeException); + ASSERT_NO_THROW(tempExpression = storm::expressions::maximum(threeExpression, threeExpression)); + EXPECT_TRUE(tempExpression.hasIntegralType()); + ASSERT_NO_THROW(tempExpression = storm::expressions::maximum(intVarExpression, rationalVarExpression)); + EXPECT_TRUE(tempExpression.hasRationalType()); + + ASSERT_THROW(tempExpression = storm::expressions::implies(trueExpression, piExpression), storm::exceptions::InvalidTypeException); + ASSERT_NO_THROW(tempExpression = storm::expressions::implies(trueExpression, falseExpression)); + EXPECT_TRUE(tempExpression.hasBooleanType()); + ASSERT_NO_THROW(tempExpression = storm::expressions::implies(boolVarExpression, boolVarExpression)); + EXPECT_TRUE(tempExpression.hasBooleanType()); + + ASSERT_THROW(tempExpression = storm::expressions::iff(trueExpression, piExpression), storm::exceptions::InvalidTypeException); + ASSERT_NO_THROW(tempExpression = storm::expressions::iff(trueExpression, falseExpression)); + EXPECT_TRUE(tempExpression.hasBooleanType()); + ASSERT_NO_THROW(tempExpression = storm::expressions::iff(boolVarExpression, boolVarExpression)); + EXPECT_TRUE(tempExpression.hasBooleanType()); ASSERT_THROW(tempExpression = trueExpression != piExpression, storm::exceptions::InvalidTypeException); ASSERT_NO_THROW(tempExpression = trueExpression != falseExpression); - EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); + EXPECT_TRUE(tempExpression.hasBooleanType()); ASSERT_NO_THROW(tempExpression = boolVarExpression != boolVarExpression); - EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); + EXPECT_TRUE(tempExpression.hasBooleanType()); - ASSERT_THROW(tempExpression = trueExpression.floor(), storm::exceptions::InvalidTypeException); - ASSERT_NO_THROW(tempExpression = threeExpression.floor()); - EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Int); - ASSERT_NO_THROW(tempExpression = doubleVarExpression.floor()); - EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Int); + ASSERT_THROW(tempExpression = storm::expressions::floor(trueExpression), storm::exceptions::InvalidTypeException); + ASSERT_NO_THROW(tempExpression = storm::expressions::floor(threeExpression)); + EXPECT_TRUE(tempExpression.hasIntegralType()); + ASSERT_NO_THROW(tempExpression = storm::expressions::floor(rationalVarExpression)); + EXPECT_TRUE(tempExpression.hasIntegralType()); - ASSERT_THROW(tempExpression = trueExpression.ceil(), storm::exceptions::InvalidTypeException); - ASSERT_NO_THROW(tempExpression = threeExpression.ceil()); - EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Int); - ASSERT_NO_THROW(tempExpression = doubleVarExpression.ceil()); - EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Int); + ASSERT_THROW(tempExpression = storm::expressions::ceil(trueExpression), storm::exceptions::InvalidTypeException); + ASSERT_NO_THROW(tempExpression = storm::expressions::ceil(threeExpression)); + EXPECT_TRUE(tempExpression.hasIntegralType()); + ASSERT_NO_THROW(tempExpression = storm::expressions::ceil(rationalVarExpression)); + EXPECT_TRUE(tempExpression.hasIntegralType()); ASSERT_THROW(tempExpression = trueExpression ^ piExpression, storm::exceptions::InvalidTypeException); ASSERT_NO_THROW(tempExpression = threeExpression ^ threeExpression); - EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Int); - ASSERT_NO_THROW(tempExpression = intVarExpression ^ doubleVarExpression); - EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Double); + EXPECT_TRUE(tempExpression.hasIntegralType()); + ASSERT_NO_THROW(tempExpression = intVarExpression ^ rationalVarExpression); + EXPECT_TRUE(tempExpression.hasRationalType()); } TEST(Expression, SubstitutionTest) { + std::shared_ptr manager(new storm::expressions::ExpressionManager()); + storm::expressions::Expression trueExpression; storm::expressions::Expression falseExpression; storm::expressions::Expression threeExpression; storm::expressions::Expression piExpression; storm::expressions::Expression boolVarExpression; storm::expressions::Expression intVarExpression; - storm::expressions::Expression doubleVarExpression; + storm::expressions::Expression rationalVarExpression; - ASSERT_NO_THROW(trueExpression = storm::expressions::Expression::createTrue()); - ASSERT_NO_THROW(falseExpression = storm::expressions::Expression::createFalse()); - ASSERT_NO_THROW(threeExpression = storm::expressions::Expression::createIntegerLiteral(3)); - ASSERT_NO_THROW(piExpression = storm::expressions::Expression::createDoubleLiteral(3.14)); - ASSERT_NO_THROW(boolVarExpression = storm::expressions::Expression::createBooleanVariable("x")); - ASSERT_NO_THROW(intVarExpression = storm::expressions::Expression::createIntegerVariable("y")); - ASSERT_NO_THROW(doubleVarExpression = storm::expressions::Expression::createDoubleVariable("z")); + ASSERT_NO_THROW(trueExpression = manager->boolean(true)); + ASSERT_NO_THROW(falseExpression = manager->boolean(false)); + ASSERT_NO_THROW(threeExpression = manager->integer(3)); + ASSERT_NO_THROW(piExpression = manager->rational(3.14)); + ASSERT_NO_THROW(boolVarExpression = manager->declareBooleanVariable("x")); + ASSERT_NO_THROW(intVarExpression = manager->declareIntegerVariable("y")); + ASSERT_NO_THROW(rationalVarExpression = manager->declareRationalVariable("z")); storm::expressions::Expression tempExpression; ASSERT_NO_THROW(tempExpression = (intVarExpression < threeExpression || boolVarExpression) && boolVarExpression); - std::map substution = { std::make_pair("y", doubleVarExpression), std::make_pair("x", storm::expressions::Expression::createTrue()), std::make_pair("a", storm::expressions::Expression::createTrue()) }; + std::map substution = { std::make_pair(manager->getVariable("y"), rationalVarExpression), std::make_pair(manager->getVariable("x"), manager->boolean(true)) }; storm::expressions::Expression substitutedExpression; ASSERT_NO_THROW(substitutedExpression = tempExpression.substitute(substution)); EXPECT_TRUE(substitutedExpression.simplify().isTrue()); } TEST(Expression, SimplificationTest) { + std::shared_ptr manager(new storm::expressions::ExpressionManager()); + storm::expressions::Expression trueExpression; storm::expressions::Expression falseExpression; storm::expressions::Expression threeExpression; storm::expressions::Expression intVarExpression; - ASSERT_NO_THROW(trueExpression = storm::expressions::Expression::createTrue()); - ASSERT_NO_THROW(falseExpression = storm::expressions::Expression::createFalse()); - ASSERT_NO_THROW(threeExpression = storm::expressions::Expression::createIntegerLiteral(3)); - ASSERT_NO_THROW(intVarExpression = storm::expressions::Expression::createIntegerVariable("y")); + ASSERT_NO_THROW(trueExpression = manager->boolean(true)); + ASSERT_NO_THROW(falseExpression = manager->boolean(false)); + ASSERT_NO_THROW(threeExpression = manager->integer(3)); + ASSERT_NO_THROW(intVarExpression = manager->declareIntegerVariable("y")); storm::expressions::Expression tempExpression; storm::expressions::Expression simplifiedExpression; @@ -298,61 +307,60 @@ TEST(Expression, SimplificationTest) { } TEST(Expression, SimpleEvaluationTest) { + std::shared_ptr manager(new storm::expressions::ExpressionManager()); + storm::expressions::Expression trueExpression; storm::expressions::Expression falseExpression; storm::expressions::Expression threeExpression; storm::expressions::Expression piExpression; storm::expressions::Expression boolVarExpression; storm::expressions::Expression intVarExpression; - storm::expressions::Expression doubleVarExpression; + storm::expressions::Expression rationalVarExpression; - ASSERT_NO_THROW(trueExpression = storm::expressions::Expression::createTrue()); - ASSERT_NO_THROW(falseExpression = storm::expressions::Expression::createFalse()); - ASSERT_NO_THROW(threeExpression = storm::expressions::Expression::createIntegerLiteral(3)); - ASSERT_NO_THROW(piExpression = storm::expressions::Expression::createDoubleLiteral(3.14)); - ASSERT_NO_THROW(boolVarExpression = storm::expressions::Expression::createBooleanVariable("x")); - ASSERT_NO_THROW(intVarExpression = storm::expressions::Expression::createIntegerVariable("y")); - ASSERT_NO_THROW(doubleVarExpression = storm::expressions::Expression::createDoubleVariable("z")); + ASSERT_NO_THROW(trueExpression = manager->boolean(true)); + ASSERT_NO_THROW(falseExpression = manager->boolean(false)); + ASSERT_NO_THROW(threeExpression = manager->integer(3)); + ASSERT_NO_THROW(piExpression = manager->rational(3.14)); + ASSERT_NO_THROW(boolVarExpression = manager->declareBooleanVariable("x")); + ASSERT_NO_THROW(intVarExpression = manager->declareIntegerVariable("y")); + ASSERT_NO_THROW(rationalVarExpression = manager->declareRationalVariable("z")); storm::expressions::Expression tempExpression; ASSERT_NO_THROW(tempExpression = (intVarExpression < threeExpression || boolVarExpression) && boolVarExpression); - ASSERT_NO_THROW(storm::expressions::SimpleValuation valuation); - storm::expressions::SimpleValuation valuation; - ASSERT_NO_THROW(valuation.addBooleanIdentifier("x")); - ASSERT_NO_THROW(valuation.addBooleanIdentifier("a")); - ASSERT_NO_THROW(valuation.addIntegerIdentifier("y")); - ASSERT_NO_THROW(valuation.addIntegerIdentifier("b")); - ASSERT_NO_THROW(valuation.addDoubleIdentifier("z")); - ASSERT_NO_THROW(valuation.addDoubleIdentifier("c")); + ASSERT_NO_THROW(storm::expressions::SimpleValuation valuation(manager)); + storm::expressions::SimpleValuation valuation(manager); + ASSERT_NO_THROW(valuation.setBooleanValue(manager->getVariable("x"), false)); + ASSERT_NO_THROW(valuation.setIntegerValue(manager->getVariable("y"), 0)); + ASSERT_NO_THROW(valuation.setRationalValue(manager->getVariable("z"), 0)); ASSERT_THROW(tempExpression.evaluateAsDouble(&valuation), storm::exceptions::InvalidTypeException); ASSERT_THROW(tempExpression.evaluateAsInt(&valuation), storm::exceptions::InvalidTypeException); EXPECT_FALSE(tempExpression.evaluateAsBool(&valuation)); - ASSERT_NO_THROW(valuation.setBooleanValue("a", true)); - EXPECT_FALSE(tempExpression.evaluateAsBool(&valuation)); - ASSERT_NO_THROW(valuation.setIntegerValue("y", 3)); + ASSERT_NO_THROW(valuation.setIntegerValue(manager->getVariable("y"), 3)); EXPECT_FALSE(tempExpression.evaluateAsBool(&valuation)); - ASSERT_NO_THROW(tempExpression = ((intVarExpression < threeExpression).ite(trueExpression, falseExpression))); + ASSERT_NO_THROW(tempExpression = storm::expressions::ite(intVarExpression < threeExpression, trueExpression, falseExpression)); ASSERT_THROW(tempExpression.evaluateAsDouble(&valuation), storm::exceptions::InvalidTypeException); ASSERT_THROW(tempExpression.evaluateAsInt(&valuation), storm::exceptions::InvalidTypeException); EXPECT_FALSE(tempExpression.evaluateAsBool(&valuation)); } TEST(Expression, VisitorTest) { + std::shared_ptr manager(new storm::expressions::ExpressionManager()); + storm::expressions::Expression threeExpression; storm::expressions::Expression piExpression; storm::expressions::Expression intVarExpression; - storm::expressions::Expression doubleVarExpression; - - ASSERT_NO_THROW(threeExpression = storm::expressions::Expression::createIntegerLiteral(3)); - ASSERT_NO_THROW(piExpression = storm::expressions::Expression::createDoubleLiteral(3.14)); - ASSERT_NO_THROW(intVarExpression = storm::expressions::Expression::createIntegerVariable("y")); - ASSERT_NO_THROW(doubleVarExpression = storm::expressions::Expression::createDoubleVariable("z")); + storm::expressions::Expression rationalVarExpression; - storm::expressions::Expression tempExpression = intVarExpression + doubleVarExpression * threeExpression; + ASSERT_NO_THROW(threeExpression = manager->integer(3)); + ASSERT_NO_THROW(piExpression = manager->rational(3.14)); + ASSERT_NO_THROW(intVarExpression = manager->declareIntegerVariable("y")); + ASSERT_NO_THROW(rationalVarExpression = manager->declareRationalVariable("z")); + + storm::expressions::Expression tempExpression = intVarExpression + rationalVarExpression * threeExpression; storm::expressions::LinearityCheckVisitor visitor; EXPECT_TRUE(visitor.check(tempExpression)); } \ No newline at end of file