sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Further steps to make everything work again. 

Former-commit-id: 3f45a49dab
main
dehnert 11 years ago
parent
7ec3e8b214
commit
99d9a9710d
38 changed files with 1302 additions and 1079 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 38
      src/adapters/MathsatExpressionAdapter.h
  2. 59
      src/adapters/Z3ExpressionAdapter.h
  3. 23
      src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h
  4. 14
      src/parser/ExpressionParser.cpp
  5. 10
      src/solver/LpSolver.h
  6. 42
      src/storage/dd/CuddDdManager.cpp
  7. 4
      src/storage/expressions/BaseExpression.cpp
  8. 12
      src/storage/expressions/BaseExpression.h
  9. 8
      src/storage/expressions/BinaryExpression.cpp
  10. 2
      src/storage/expressions/BinaryExpression.h
  11. 4
      src/storage/expressions/BooleanLiteralExpression.cpp
  12. 2
      src/storage/expressions/BooleanLiteralExpression.h
  13. 4
      src/storage/expressions/DoubleLiteralExpression.cpp
  14. 2
      src/storage/expressions/DoubleLiteralExpression.h
  15. 181
      src/storage/expressions/Expression.cpp
  16. 116
      src/storage/expressions/Expression.h
  17. 12
      src/storage/expressions/ExpressionManager.cpp
  18. 27
      src/storage/expressions/ExpressionManager.h
  19. 11
      src/storage/expressions/IfThenElseExpression.cpp
  20. 2
      src/storage/expressions/IfThenElseExpression.h
  21. 4
      src/storage/expressions/IntegerLiteralExpression.cpp
  22. 2
      src/storage/expressions/IntegerLiteralExpression.h
  23. 4
      src/storage/expressions/SimpleValuation.cpp
  24. 5
      src/storage/expressions/SimpleValuation.h
  25. 5
      src/storage/expressions/Type.cpp
  26. 4
      src/storage/expressions/UnaryExpression.cpp
  27. 2
      src/storage/expressions/UnaryExpression.h
  28. 4
      src/storage/expressions/VariableExpression.cpp
  29. 2
      src/storage/expressions/VariableExpression.h
  30. 171
      src/storage/prism/Program.cpp
  31. 80
      test/functional/adapter/MathsatExpressionAdapterTest.cpp
  32. 54
      test/functional/adapter/Z3ExpressionAdapterTest.cpp
  33. 171
      test/functional/solver/GlpkLpSolverTest.cpp
  34. 201
      test/functional/solver/GurobiLpSolverTest.cpp
  35. 173
      test/functional/solver/MathSatSmtSolverTest.cpp
  36. 328
      test/functional/solver/Z3SmtSolverTest.cpp
  37. 252
      test/functional/storage/CuddDdTest.cpp
  38. 346
      test/functional/storage/ExpressionTest.cpp

38
src/adapters/MathsatExpressionAdapter.h
View File

@ -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<storm::expressions::Variable, msat_decl> variableToDeclarationMapping;

59
src/adapters/Z3ExpressionAdapter.h
View File

@ -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<z3::expr>(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;

23
src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h
View File

@ -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<uint_fast64_t, std::string> stateToVariableNameMap;
std::map<uint_fast64_t, storm::expressions::Variable> 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<ValueType>() / exitRates[state]) * storm::expressions::Expression::createDoubleVariable("k");
storm::expressions::Expression rightHandSide = goalStates.get(state) ? storm::expressions::Expression::createDoubleLiteral(storm::utility::constantOne<ValueType>() / exitRates[state]) : storm::expressions::Expression::createDoubleLiteral(storm::utility::constantZero<ValueType>());
constraint = constraint + solver->getConstant(storm::utility::constantOne<ValueType>() / exitRates[state]) * k;
storm::expressions::Expression rightHandSide = goalStates.get(state) ? solver->getConstant(storm::utility::constantOne<ValueType>() / 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<ValueType>());
storm::expressions::Expression rightHandSide = solver->getConstant(storm::utility::constantZero<ValueType>());
if (min) {
constraint = constraint <= rightHandSide;
} else {
@ -527,7 +526,7 @@ namespace storm {
}
solver->optimize();
return solver->getContinuousValue("k");
return solver->getContinuousValue(k);
}
/*!

14
src/parser/ExpressionParser.cpp
View File

@ -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) {

10
src/solver/LpSolver.h
View File

@ -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 <code>update</code>
* usable.

42
src/storage/dd/CuddDdManager.cpp
View File

@ -198,26 +198,54 @@ namespace storm {
std::vector<std::string> DdManager<DdType::CUDD>::getDdVariableNames() const {
// First, we initialize a list DD variables and their names.
std::vector<std::pair<ADD, std::string>> variableNamePairs;
for (auto const& nameMetaVariablePair : this->metaVariableMap) {
DdMetaVariable<DdType::CUDD> const& metaVariable = nameMetaVariablePair.second;
std::vector<std::pair<ADD, std::string>> variablePairs;
for (auto const& variablePair : this->metaVariableMap) {
DdMetaVariable<DdType::CUDD> 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<storm::dd::DdType::CUDD>::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<ADD, std::string> const& a, std::pair<ADD, std::string> const& b) { return a.first.NodeReadIndex() < b.first.NodeReadIndex(); });
std::sort(variablePairs.begin(), variablePairs.end(), [](std::pair<ADD, std::string> const& a, std::pair<ADD, std::string> const& b) { return a.first.NodeReadIndex() < b.first.NodeReadIndex(); });
// Now, we project the sorted vector to its second component.
std::vector<std::string> result;
for (auto const& element : variableNamePairs) {
for (auto const& element : variablePairs) {
result.push_back(element.second);
}
return result;
}
std::vector<storm::expressions::Variable> DdManager<DdType::CUDD>::getDdVariables() const {
// First, we initialize a list DD variables and their names.
std::vector<std::pair<ADD, storm::expressions::Variable>> variablePairs;
for (auto const& variablePair : this->metaVariableMap) {
DdMetaVariable<DdType::CUDD> 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<storm::dd::DdType::CUDD>::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<ADD, std::string> const& a, std::pair<ADD, std::string> const& b) { return a.first.NodeReadIndex() < b.first.NodeReadIndex(); });
// Now, we project the sorted vector to its second component.
std::vector<storm::expressions::Variable> result;
for (auto const& element : variablePairs) {
result.push_back(element.second);
}

4
src/storage/expressions/BaseExpression.cpp
View File

@ -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.");
}

12
src/storage/expressions/BaseExpression.h
View File

@ -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<std::string> getVariables() const = 0;
virtual void gatherVariables(std::set<storm::expressions::Variable>& 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.
*

8
src/storage/expressions/BinaryExpression.cpp
View File

@ -17,11 +17,9 @@ namespace storm {
return this->getFirstOperand()->containsVariables() || this->getSecondOperand()->containsVariables();
}
std::set<std::string> BinaryExpression::getVariables() const {
std::set<std::string> firstVariableSet = this->getFirstOperand()->getVariables();
std::set<std::string> secondVariableSet = this->getSecondOperand()->getVariables();
firstVariableSet.insert(secondVariableSet.begin(), secondVariableSet.end());
return firstVariableSet;
void BinaryExpression::gatherVariables(std::set<storm::expressions::Variable>& variables) const {
this->getFirstOperand()->gatherVariables(variables);
this->getSecondOperand()->gatherVariables(variables);
}
std::shared_ptr<BaseExpression const> const& BinaryExpression::getFirstOperand() const {

2
src/storage/expressions/BinaryExpression.h
View File

@ -35,7 +35,7 @@ namespace storm {
virtual bool containsVariables() const override;
virtual uint_fast64_t getArity() const override;
virtual std::shared_ptr<BaseExpression const> getOperand(uint_fast64_t operandIndex) const override;
virtual std::set<std::string> getVariables() const override;
virtual void gatherVariables(std::set<storm::expressions::Variable>& variables) const override;
/*!
* Retrieves the first operand of the expression.

4
src/storage/expressions/BooleanLiteralExpression.cpp
View File

@ -23,8 +23,8 @@ namespace storm {
return this->getValue() == false;
}
std::set<std::string> BooleanLiteralExpression::getVariables() const {
return std::set<std::string>();
void BooleanLiteralExpression::gatherVariables(std::set<storm::expressions::Variable>& variables) const {
return;
}
std::shared_ptr<BaseExpression const> BooleanLiteralExpression::simplify() const {

2
src/storage/expressions/BooleanLiteralExpression.h
View File

@ -30,7 +30,7 @@ namespace storm {
virtual bool isLiteral() const override;
virtual bool isTrue() const override;
virtual bool isFalse() const override;
virtual std::set<std::string> getVariables() const override;
virtual void gatherVariables(std::set<storm::expressions::Variable>& variables) const override;
virtual std::shared_ptr<BaseExpression const> simplify() const override;
virtual boost::any accept(ExpressionVisitor& visitor) const override;

4
src/storage/expressions/DoubleLiteralExpression.cpp
View File

@ -15,8 +15,8 @@ namespace storm {
return true;
}
std::set<std::string> DoubleLiteralExpression::getVariables() const {
return std::set<std::string>();
void DoubleLiteralExpression::gatherVariables(std::set<storm::expressions::Variable>& variables) const {
return;
}
std::shared_ptr<BaseExpression const> DoubleLiteralExpression::simplify() const {

2
src/storage/expressions/DoubleLiteralExpression.h
View File

@ -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<std::string> getVariables() const override;
virtual void gatherVariables(std::set<storm::expressions::Variable>& variables) const override;
virtual std::shared_ptr<BaseExpression const> simplify() const override;
virtual boost::any accept(ExpressionVisitor& visitor) const override;

181
src/storage/expressions/Expression.cpp
View File

@ -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<BaseExpression const> const& expressionPtr) : expressionPtr(expressionPtr) {
// Intentionally left empty.
}
@ -83,8 +94,10 @@ namespace storm {
return this->getBaseExpression().isFalse();
}
std::set<std::string> Expression::getVariables() const {
return this->getBaseExpression().getVariables();
std::set<storm::expressions::Variable> Expression::getVariables() const {
std::set<storm::expressions::Variable> 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<BaseExpression>(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<BaseExpression>(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<BaseExpression>(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<BaseExpression>(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<BaseExpression>(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<BaseExpression>(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<BaseExpression>(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<BaseExpression>(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<BaseExpression>(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<BaseExpression>(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<BaseExpression>(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<BaseExpression>(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<BaseExpression>(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<BaseExpression>(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<BaseExpression>(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<BaseExpression>(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<BaseExpression>(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<BaseExpression>(new BinaryRelationExpression(this->getBaseExpression().getManager(), this->getType().numericalComparison(other.getType()), this->getBaseExpressionPointer(), other.getBaseExpressionPointer(), BinaryRelationExpression::RelationType::NotEqual)));
} else {
return Expression(std::shared_ptr<BaseExpression>(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<BaseExpression>(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<BaseExpression>(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<BaseExpression>(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<BaseExpression>(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<BaseExpression>(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<BaseExpression>(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<BaseExpression>(new BinaryRelationExpression(first.getBaseExpression().getManager(), first.getType().numericalComparison(second.getType()), first.getBaseExpressionPointer(), second.getBaseExpressionPointer(), BinaryRelationExpression::RelationType::NotEqual)));
} else {
return Expression(std::shared_ptr<BaseExpression>(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<BaseExpression>(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<BaseExpression>(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<BaseExpression>(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<BaseExpression>(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<BaseExpression>(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<BaseExpression>(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<BaseExpression>(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<BaseExpression>(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<BaseExpression>(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<BaseExpression>(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<BaseExpression>(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<BaseExpression>(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<BaseExpression>(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<BaseExpression>(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<BaseExpression>(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<BaseExpression>(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<BaseExpression>(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<BaseExpression>(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<BaseExpression>(new UnaryNumericalFunctionExpression(first.getBaseExpression().getManager(), first.getType().floorCeil(), first.getBaseExpressionPointer(), UnaryNumericalFunctionExpression::OperatorType::Ceil)));
}
}
}

116
src/storage/expressions/Expression.h
View File

@ -21,8 +21,39 @@ namespace storm {
friend class Variable;
template<typename MapType> 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<std::string> getVariables() const;
std::set<storm::expressions::Variable> 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<BaseExpression const> 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<BaseExpression const> expressionPtr;
// A pointer to the responsible manager.
std::shared_ptr<ExpressionManager> 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);
}
}

12
src/storage/expressions/ExpressionManager.cpp
View File

@ -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.");

27
src/storage/expressions/ExpressionManager.h
View File

@ -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.

11
src/storage/expressions/IfThenElseExpression.cpp
View File

@ -63,13 +63,10 @@ namespace storm {
}
}
std::set<std::string> IfThenElseExpression::getVariables() const {
std::set<std::string> result = this->condition->getVariables();
std::set<std::string> 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<storm::expressions::Variable>& variables) const {
this->condition->gatherVariables(variables);
this->thenExpression->gatherVariables(variables);
this->elseExpression->gatherVariables(variables);
}
std::shared_ptr<BaseExpression const> IfThenElseExpression::simplify() const {

2
src/storage/expressions/IfThenElseExpression.h
View File

@ -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<std::string> getVariables() const override;
virtual void gatherVariables(std::set<storm::expressions::Variable>& variables) const override;
virtual std::shared_ptr<BaseExpression const> simplify() const override;
virtual boost::any accept(ExpressionVisitor& visitor) const override;

4
src/storage/expressions/IntegerLiteralExpression.cpp
View File

@ -19,8 +19,8 @@ namespace storm {
return true;
}
std::set<std::string> IntegerLiteralExpression::getVariables() const {
return std::set<std::string>();
void IntegerLiteralExpression::gatherVariables(std::set<storm::expressions::Variable>& variables) const {
return;
}
std::shared_ptr<BaseExpression const> IntegerLiteralExpression::simplify() const {

2
src/storage/expressions/IntegerLiteralExpression.h
View File

@ -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<std::string> getVariables() const override;
virtual void gatherVariables(std::set<storm::expressions::Variable>& variables) const override;
virtual std::shared_ptr<BaseExpression const> simplify() const override;
virtual boost::any accept(ExpressionVisitor& visitor) const override;

4
src/storage/expressions/SimpleValuation.cpp
View File

@ -7,6 +7,10 @@
namespace storm {
namespace expressions {
SimpleValuation::SimpleValuation() : Valuation(nullptr) {
// Intentionally left empty.
}
SimpleValuation::SimpleValuation(std::shared_ptr<storm::expressions::ExpressionManager const> const& manager) : Valuation(manager), booleanValues(nullptr), integerValues(nullptr), rationalValues(nullptr) {
if (this->getManager().getNumberOfBooleanVariables() > 0) {
booleanValues = std::unique_ptr<std::vector<bool>>(new std::vector<bool>(this->getManager().getNumberOfBooleanVariables()));

5
src/storage/expressions/SimpleValuation.h
View File

@ -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.
*

5
src/storage/expressions/Type.cpp
View File

@ -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;
}

4
src/storage/expressions/UnaryExpression.cpp
View File

@ -17,8 +17,8 @@ namespace storm {
return this->getOperand()->containsVariables();
}
std::set<std::string> UnaryExpression::getVariables() const {
return this->getOperand()->getVariables();
void UnaryExpression::gatherVariables(std::set<storm::expressions::Variable>& variables) const {
return;
}
std::shared_ptr<BaseExpression const> const& UnaryExpression::getOperand() const {

2
src/storage/expressions/UnaryExpression.h
View File

@ -31,7 +31,7 @@ namespace storm {
virtual bool containsVariables() const override;
virtual uint_fast64_t getArity() const override;
virtual std::shared_ptr<BaseExpression const> getOperand(uint_fast64_t operandIndex) const override;
virtual std::set<std::string> getVariables() const override;
virtual void gatherVariables(std::set<storm::expressions::Variable>& variables) const override;
/*!
* Retrieves the operand of the unary expression.

4
src/storage/expressions/VariableExpression.cpp
View File

@ -53,8 +53,8 @@ namespace storm {
return true;
}
std::set<std::string> VariableExpression::getVariables() const {
return {this->getVariableName()};
void VariableExpression::gatherVariables(std::set<storm::expressions::Variable>& variables) const {
variables.insert(this->getVariable());
}
std::shared_ptr<BaseExpression const> VariableExpression::simplify() const {

2
src/storage/expressions/VariableExpression.h
View File

@ -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<std::string> getVariables() const override;
virtual void gatherVariables(std::set<storm::expressions::Variable>& variables) const override;
virtual std::shared_ptr<BaseExpression const> simplify() const override;
virtual boost::any accept(ExpressionVisitor& visitor) const override;

171
src/storage/prism/Program.cpp
View File

@ -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<std::string> allIdentifiers;
std::set<std::string> globalIdentifiers;
std::set<std::string> constantNames;
std::set<storm::expressions::Variable> all;
std::set<storm::expressions::Variable> global;
std::set<storm::expressions::Variable> 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<std::string> containedIdentifiers = constant.getExpression().getVariables();
bool isValid = std::includes(constantNames.begin(), constantNames.end(), containedIdentifiers.begin(), containedIdentifiers.end());
std::set<storm::expressions::Variable> 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<std::string> variableNames;
std::set<storm::expressions::Variable> 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<std::string> containedIdentifiers = variable.getInitialValueExpression().getVariables();
bool isValid = std::includes(constantNames.begin(), constantNames.end(), containedIdentifiers.begin(), containedIdentifiers.end());
std::set<storm::expressions::Variable> 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<std::string> containedIdentifiers = variable.getLowerBoundExpression().getVariables();
bool isValid = std::includes(constantNames.begin(), constantNames.end(), containedIdentifiers.begin(), containedIdentifiers.end());
std::set<storm::expressions::Variable> 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<std::string> containedIdentifiers = variable.getInitialValueExpression().getVariables();
bool isValid = std::includes(constantNames.begin(), constantNames.end(), containedIdentifiers.begin(), containedIdentifiers.end());
std::set<storm::expressions::Variable> 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<std::string> containedIdentifiers = variable.getLowerBoundExpression().getVariables();
bool isValid = std::includes(constantNames.begin(), constantNames.end(), containedIdentifiers.begin(), containedIdentifiers.end());
std::set<storm::expressions::Variable> 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<std::string> variablesAndConstants;
std::set_union(variableNames.begin(), variableNames.end(), constantNames.begin(), constantNames.end(), std::inserter(variablesAndConstants, variablesAndConstants.begin()));
std::set<storm::expressions::Variable> 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<std::string> legalIdentifiers = globalIdentifiers;
std::set<storm::expressions::Variable> 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<std::string> containedIdentifiers = command.getGuardExpression().getVariables();
bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end());
std::set<storm::expressions::Variable> 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<std::string> alreadyAssignedIdentifiers;
std::set<storm::expressions::Variable> 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<std::string> containedIdentifiers = stateReward.getStatePredicateExpression().getVariables();
bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end());
std::set<storm::expressions::Variable> 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<std::string> containedIdentifiers = transitionReward.getStatePredicateExpression().getVariables();
bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end());
std::set<storm::expressions::Variable> 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<std::string> containedIdentifiers = this->getInitialConstruct().getInitialStatesExpression().getVariables();
std::set<storm::expressions::Variable> 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<std::string> containedIdentifiers = label.getStatePredicateExpression().getVariables();
bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end());
std::set<storm::expressions::Variable> 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<std::string> containedIdentifiers = formula.getExpression().getVariables();
bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end());
std::set<storm::expressions::Variable> 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());
}
}

80
test/functional/adapter/MathsatExpressionAdapterTest.cpp
View File

@ -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<storm::expressions::ExpressionManager> 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<storm::expressions::ExpressionManager> 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<storm::expressions::ExpressionManager> 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<storm::expressions::ExpressionManager> 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<storm::expressions::ExpressionManager> 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;

54
test/functional/adapter/Z3ExpressionAdapterTest.cpp
View File

@ -1,6 +1,9 @@
#include "gtest/gtest.h"
#include "storm-config.h"
#include <memory>
#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<storm::expressions::ExpressionManager> 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<storm::expressions::ExpressionManager> 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<storm::expressions::ExpressionManager> 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<storm::expressions::ExpressionManager> 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<storm::expressions::ExpressionManager> 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;

171
test/functional/solver/GlpkLpSolverTest.cpp
View File

@ -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);
}

201
test/functional/solver/GurobiLpSolverTest.cpp
View File

@ -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);
}

173
test/functional/solver/MathSatSmtSolverTest.cpp
View File

@ -5,24 +5,26 @@
#include "src/solver/MathsatSmtSolver.h"
TEST(MathsatSmtSolver, CheckSat) {
storm::solver::MathsatSmtSolver s;
std::shared_ptr<storm::expressions::ExpressionManager> 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<storm::expressions::ExpressionManager> 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<storm::expressions::ExpressionManager> 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<storm::expressions::ExpressionManager> 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<storm::expressions::ExpressionManager> 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<storm::solver::SmtSolver::ModelReference> 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<storm::expressions::ExpressionManager> 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<storm::expressions::ExpressionManager> 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<storm::expressions::ExpressionManager> 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);

328
test/functional/solver/Z3SmtSolverTest.cpp
View File

@ -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<storm::expressions::ExpressionManager> 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<storm::expressions::ExpressionManager> 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<storm::expressions::ExpressionManager> 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<storm::expressions::ExpressionManager> 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<storm::expressions::ExpressionManager> 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<storm::solver::SmtSolver::ModelReference> 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<storm::expressions::SimpleValuation> 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<storm::expressions::ExpressionManager> 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<storm::expressions::SimpleValuation> 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<storm::expressions::Expression> unsatCore = s.getUnsatAssumptions();
ASSERT_EQ(unsatCore.size(), 1);
ASSERT_TRUE(unsatCore[0].isVariable());
ASSERT_STREQ("f2", unsatCore[0].getIdentifier().c_str());
std::shared_ptr<storm::expressions::ExpressionManager> 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<storm::expressions::Expression> unsatCore = s.getUnsatAssumptions();
ASSERT_EQ(unsatCore.size(), 1);
ASSERT_TRUE(unsatCore[0].isVariable());
ASSERT_STREQ("f2", unsatCore[0].getIdentifier().c_str());
}
#endif

252
test/functional/storage/CuddDdTest.cpp
View File

@ -55,12 +55,12 @@ TEST(CuddDdManager, AddGetMetaVariableTest) {
TEST(CuddDdManager, EncodingTest) {
std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());
manager->addMetaVariable("x", 1, 9);
std::pair<storm::expressions::Variable, storm::expressions::Variable> x = manager->addMetaVariable("x", 1, 9);
storm::dd::Dd<storm::dd::DdType::CUDD> 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<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());
ASSERT_NO_THROW(manager->addMetaVariable("x", 1, 9));
std::pair<storm::expressions::Variable, storm::expressions::Variable> x;
ASSERT_NO_THROW(x = manager->addMetaVariable("x", 1, 9));
storm::dd::Dd<storm::dd::DdType::CUDD> 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<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());
manager->addMetaVariable("x", 1, 9);
std::pair<storm::expressions::Variable, storm::expressions::Variable> x = manager->addMetaVariable("x", 1, 9);
storm::dd::Dd<storm::dd::DdType::CUDD> 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<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());
manager->addMetaVariable("x", 1, 9);
std::pair<storm::expressions::Variable, storm::expressions::Variable> 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<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());
manager->addMetaVariable("x", 1, 9);
std::pair<storm::expressions::Variable, storm::expressions::Variable> x = manager->addMetaVariable("x", 1, 9);
storm::dd::Dd<storm::dd::DdType::CUDD> dd1;
storm::dd::Dd<storm::dd::DdType::CUDD> dd2;
storm::dd::Dd<storm::dd::DdType::CUDD> 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<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());
manager->addMetaVariable("x", 1, 9);
manager->addMetaVariable("z", 2, 8);
std::pair<storm::expressions::Variable, storm::expressions::Variable> x = manager->addMetaVariable("x", 1, 9);
std::pair<storm::expressions::Variable, storm::expressions::Variable> z = manager->addMetaVariable("z", 2, 8);
storm::dd::Dd<storm::dd::DdType::CUDD> dd1;
storm::dd::Dd<storm::dd::DdType::CUDD> 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<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());
manager->addMetaVariable("x", 1, 9);
std::pair<storm::expressions::Variable, storm::expressions::Variable> x = manager->addMetaVariable("x", 1, 9);
storm::dd::Dd<storm::dd::DdType::CUDD> dd1 = manager->getIdentity("x").equals(manager->getIdentity("x'"));
storm::dd::Dd<storm::dd::DdType::CUDD> dd2 = manager->getRange("x'");
storm::dd::Dd<storm::dd::DdType::CUDD> dd1 = manager->getIdentity(x.first).equals(manager->getIdentity(x.second));
storm::dd::Dd<storm::dd::DdType::CUDD> dd2 = manager->getRange(x.second);
storm::dd::Dd<storm::dd::DdType::CUDD> 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<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());
manager->addMetaVariable("x", 1, 9);
std::pair<storm::expressions::Variable, storm::expressions::Variable> x = manager->addMetaVariable("x", 1, 9);
storm::dd::Dd<storm::dd::DdType::CUDD> 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<std::string, int_fast64_t> metaVariableToValueMap;
metaVariableToValueMap.emplace("x", 1);
std::map<storm::expressions::Variable, int_fast64_t> 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<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());
manager->addMetaVariable("x", 1, 9);
manager->addMetaVariable("y", 0, 3);
std::pair<storm::expressions::Variable, storm::expressions::Variable> x = manager->addMetaVariable("x", 1, 9);
std::pair<storm::expressions::Variable, storm::expressions::Variable> y = manager->addMetaVariable("y", 0, 3);
storm::dd::Dd<storm::dd::DdType::CUDD> dd;
ASSERT_NO_THROW(dd = manager->getRange("x"));
ASSERT_NO_THROW(dd = manager->getRange(x.first));
storm::dd::DdForwardIterator<storm::dd::DdType::CUDD> 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<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());
manager->addMetaVariable("x", 1, 9);
storm::dd::Dd<storm::dd::DdType::CUDD> 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<storm::dd::DdType::CUDD> 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<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());
// std::pair<storm::expressions::Variable, storm::expressions::Variable> x = manager->addMetaVariable("x", 1, 9);
//
// storm::dd::Dd<storm::dd::DdType::CUDD> 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<storm::dd::DdType::CUDD> 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<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());
manager->addMetaVariable("a");
manager->addMetaVariable("x", 1, 9);
std::pair<storm::expressions::Variable, storm::expressions::Variable> a = manager->addMetaVariable("a");
std::pair<storm::expressions::Variable, storm::expressions::Variable> x = manager->addMetaVariable("x", 1, 9);
storm::dd::Dd<storm::dd::DdType::CUDD> dd = manager->getIdentity("x");
storm::dd::Dd<storm::dd::DdType::CUDD> dd = manager->getIdentity(x.first);
storm::dd::Odd<storm::dd::DdType::CUDD> odd;
ASSERT_NO_THROW(odd = storm::dd::Odd<storm::dd::DdType::CUDD>(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<storm::dd::DdType::CUDD> rowOdd;
ASSERT_NO_THROW(rowOdd = storm::dd::Odd<storm::dd::DdType::CUDD>(manager->getRange("x")));
ASSERT_NO_THROW(rowOdd = storm::dd::Odd<storm::dd::DdType::CUDD>(manager->getRange(x.first)));
storm::dd::Odd<storm::dd::DdType::CUDD> columnOdd;
ASSERT_NO_THROW(columnOdd = storm::dd::Odd<storm::dd::DdType::CUDD>(manager->getRange("x'")));
ASSERT_NO_THROW(columnOdd = storm::dd::Odd<storm::dd::DdType::CUDD>(manager->getRange(x.second)));
// Try to translate the matrix.
storm::storage::SparseMatrix<double> 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());

346
test/functional/storage/ExpressionTest.cpp
View File

@ -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<storm::expressions::ExpressionManager> 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<storm::expressions::ExpressionManager> 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<std::string>());
EXPECT_TRUE(trueExpression.getVariables() == std::set<storm::expressions::Variable>());
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<std::string>());
EXPECT_TRUE(falseExpression.getVariables() == std::set<storm::expressions::Variable>());
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<std::string>());
EXPECT_TRUE(threeExpression.getVariables() == std::set<storm::expressions::Variable>());
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<std::string>());
EXPECT_TRUE(piExpression.getVariables() == std::set<storm::expressions::Variable>());
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<std::string>({"x"}));
EXPECT_TRUE(boolVarExpression.getVariables() == std::set<storm::expressions::Variable>({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<std::string>({"y"}));
EXPECT_TRUE(intVarExpression.getVariables() == std::set<storm::expressions::Variable>({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<std::string>({"z"}));
EXPECT_TRUE(rationalVarExpression.hasRationalType());
EXPECT_FALSE(rationalVarExpression.isLiteral());
EXPECT_FALSE(rationalVarExpression.isTrue());
EXPECT_FALSE(rationalVarExpression.isFalse());
EXPECT_TRUE(rationalVarExpression.getVariables() == std::set<storm::expressions::Variable>({manager->getVariable("z")}));
}
TEST(Expression, OperatorTest) {
std::shared_ptr<storm::expressions::ExpressionManager> 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<storm::expressions::ExpressionManager> 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<std::string, storm::expressions::Expression> substution = { std::make_pair("y", doubleVarExpression), std::make_pair("x", storm::expressions::Expression::createTrue()), std::make_pair("a", storm::expressions::Expression::createTrue()) };
std::map<storm::expressions::Variable, storm::expressions::Expression> 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<storm::expressions::ExpressionManager> 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<storm::expressions::ExpressionManager> 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<storm::expressions::ExpressionManager> 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));
}
Write Preview
Loading…
Cancel
Save