diff --git a/src/adapters/Z3ExpressionAdapter.h b/src/adapters/Z3ExpressionAdapter.h index 09bc1dac4..8237fbce6 100644 --- a/src/adapters/Z3ExpressionAdapter.h +++ b/src/adapters/Z3ExpressionAdapter.h @@ -10,13 +10,17 @@ #include -#include "src/ir/expressions/ExpressionVisitor.h" -#include "src/ir/expressions/Expressions.h" +#include "z3++.h" +#include "z3.h" + +#include "src/storage/expressions/Expressions.h" +#include "src/exceptions/ExpressionEvaluationException.h" +#include "src/exceptions/NotImplementedException.h" namespace storm { namespace adapters { - class Z3ExpressionAdapter : public storm::ir::expressions::ExpressionVisitor { + class Z3ExpressionAdapter : public storm::expressions::ExpressionVisitor { public: /*! * Creates a Z3ExpressionAdapter over the given Z3 context. @@ -25,7 +29,12 @@ namespace storm { * the lifetime of the context as long as the instance of this adapter is used. * @param variableToExpressionMap A mapping from variable names to their corresponding Z3 expressions. */ - Z3ExpressionAdapter(z3::context& context, std::map const& variableToExpressionMap) : context(context), stack(), variableToExpressionMap(variableToExpressionMap) { + Z3ExpressionAdapter(z3::context& context, std::map const& variableToExpressionMap) + : context(context) + , stack() + , variableToExpressionMap(variableToExpressionMap) + , additionalVariableCounter(0) + , additionalAssertions() { // Intentionally left empty. } @@ -35,71 +44,86 @@ namespace storm { * @param expression The expression to translate. * @return An equivalent expression for Z3. */ - z3::expr translateExpression(std::unique_ptr const& expression) { - expression->accept(this); + z3::expr translateExpression(storm::expressions::Expression const& expression) { + expression.getBaseExpression().accept(this); z3::expr result = stack.top(); stack.pop(); + + while (!additionalAssertions.empty()) { + result = result && additionalAssertions.top(); + additionalAssertions.pop(); + } + return result; } - virtual void visit(ir::expressions::BinaryBooleanFunctionExpression* expression) { - expression->getLeft()->accept(this); - expression->getRight()->accept(this); + virtual void visit(storm::expressions::BinaryBooleanFunctionExpression const* expression) override { + expression->getFirstOperand()->accept(this); + expression->getSecondOperand()->accept(this); - z3::expr rightResult = stack.top(); + const z3::expr rightResult = stack.top(); stack.pop(); - z3::expr leftResult = stack.top(); + const z3::expr leftResult = stack.top(); stack.pop(); - switch(expression->getFunctionType()) { - case storm::ir::expressions::BinaryBooleanFunctionExpression::AND: + switch(expression->getOperatorType()) { + case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::And: stack.push(leftResult && rightResult); break; - case storm::ir::expressions::BinaryBooleanFunctionExpression::OR: + case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Or: stack.push(leftResult || rightResult); - break; + break; + case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Xor: + stack.push(z3::expr(context, Z3_mk_xor(context, leftResult, rightResult))); + break; + case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Implies: + stack.push(z3::expr(context, Z3_mk_implies(context, leftResult, rightResult))); + break; + case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Iff: + stack.push(z3::expr(context, Z3_mk_iff(context, leftResult, rightResult))); + break; default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " - << "Unknown boolean binary operator: '" << expression->getFunctionType() << "' in expression " << expression->toString() << "."; + << "Unknown boolean binary operator: '" << expression->getOperatorType() << "' in expression " << expression << "."; } } - virtual void visit(ir::expressions::BinaryNumericalFunctionExpression* expression) { - expression->getLeft()->accept(this); - expression->getRight()->accept(this); + virtual void visit(storm::expressions::BinaryNumericalFunctionExpression const* expression) override { + expression->getFirstOperand()->accept(this); + expression->getSecondOperand()->accept(this); z3::expr rightResult = stack.top(); stack.pop(); z3::expr leftResult = stack.top(); stack.pop(); - switch(expression->getFunctionType()) { - case storm::ir::expressions::BinaryNumericalFunctionExpression::PLUS: + switch(expression->getOperatorType()) { + case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Plus: stack.push(leftResult + rightResult); break; - case storm::ir::expressions::BinaryNumericalFunctionExpression::MINUS: + case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Minus: stack.push(leftResult - rightResult); break; - case storm::ir::expressions::BinaryNumericalFunctionExpression::TIMES: + case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Times: stack.push(leftResult * rightResult); break; - case storm::ir::expressions::BinaryNumericalFunctionExpression::DIVIDE: + case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Divide: stack.push(leftResult / rightResult); break; - case storm::ir::expressions::BinaryNumericalFunctionExpression::MIN: + case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Min: stack.push(ite(leftResult <= rightResult, leftResult, rightResult)); break; - case storm::ir::expressions::BinaryNumericalFunctionExpression::MAX: + case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Max: stack.push(ite(leftResult >= rightResult, leftResult, rightResult)); break; default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " - << "Unknown numerical binary operator: '" << expression->getFunctionType() << "' in expression " << expression->toString() << "."; + << "Unknown numerical binary operator: '" << expression->getOperatorType() << "' in expression " << expression << "."; } } - virtual void visit(ir::expressions::BinaryRelationExpression* expression) { - expression->getLeft()->accept(this); - expression->getRight()->accept(this); + virtual void visit(storm::expressions::BinaryRelationExpression const* expression) override { + expression->getFirstOperand()->accept(this); + expression->getSecondOperand()->accept(this); z3::expr rightResult = stack.top(); stack.pop(); @@ -107,109 +131,122 @@ namespace storm { stack.pop(); switch(expression->getRelationType()) { - case storm::ir::expressions::BinaryRelationExpression::EQUAL: + case storm::expressions::BinaryRelationExpression::RelationType::Equal: stack.push(leftResult == rightResult); break; - case storm::ir::expressions::BinaryRelationExpression::NOT_EQUAL: + case storm::expressions::BinaryRelationExpression::RelationType::NotEqual: stack.push(leftResult != rightResult); break; - case storm::ir::expressions::BinaryRelationExpression::LESS: + case storm::expressions::BinaryRelationExpression::RelationType::Less: stack.push(leftResult < rightResult); break; - case storm::ir::expressions::BinaryRelationExpression::LESS_OR_EQUAL: + case storm::expressions::BinaryRelationExpression::RelationType::LessOrEqual: stack.push(leftResult <= rightResult); break; - case storm::ir::expressions::BinaryRelationExpression::GREATER: + case storm::expressions::BinaryRelationExpression::RelationType::Greater: stack.push(leftResult > rightResult); break; - case storm::ir::expressions::BinaryRelationExpression::GREATER_OR_EQUAL: + case storm::expressions::BinaryRelationExpression::RelationType::GreaterOrEqual: stack.push(leftResult >= rightResult); break; default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " - << "Unknown boolean binary operator: '" << expression->getRelationType() << "' in expression " << expression->toString() << "."; + << "Unknown boolean binary operator: '" << expression->getRelationType() << "' in expression " << expression << "."; } } - virtual void visit(ir::expressions::BooleanConstantExpression* expression) { - if (!expression->isDefined()) { - throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " - << ". Boolean constant '" << expression->getConstantName() << "' is undefined."; - } - - stack.push(context.bool_val(expression->getValue())); + virtual void visit(storm::expressions::BooleanConstantExpression const* expression) override { + throw storm::exceptions::NotImplementedException() << "BooleanConstantExpression is not supported by Z3ExpressionAdapter."; } - virtual void visit(ir::expressions::BooleanLiteralExpression* expression) { - stack.push(context.bool_val(expression->getValueAsBool(nullptr))); + virtual void visit(storm::expressions::BooleanLiteralExpression const* expression) override { + stack.push(context.bool_val(expression->evaluateAsBool())); } - virtual void visit(ir::expressions::DoubleConstantExpression* expression) { - if (!expression->isDefined()) { - throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " - << ". Double constant '" << expression->getConstantName() << "' is undefined."; - } - - std::stringstream fractionStream; - fractionStream << expression->getValue(); - stack.push(context.real_val(fractionStream.str().c_str())); + virtual void visit(storm::expressions::DoubleConstantExpression const* expression) override { + throw storm::exceptions::NotImplementedException() << "DoubleConstantExpression is not supported by Z3ExpressionAdapter."; } - virtual void visit(ir::expressions::DoubleLiteralExpression* expression) { + virtual void visit(storm::expressions::DoubleLiteralExpression const* expression) override { std::stringstream fractionStream; - fractionStream << expression->getValueAsDouble(nullptr); + fractionStream << expression->evaluateAsDouble(); stack.push(context.real_val(fractionStream.str().c_str())); } - virtual void visit(ir::expressions::IntegerConstantExpression* expression) { - if (!expression->isDefined()) { - throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " - << ". Integer constant '" << expression->getConstantName() << "' is undefined."; - } - - stack.push(context.int_val(static_cast(expression->getValue()))); + virtual void visit(storm::expressions::IntegerConstantExpression const* expression) override { + throw storm::exceptions::NotImplementedException() << "IntegerConstantExpression is not supported by Z3ExpressionAdapter."; } - virtual void visit(ir::expressions::IntegerLiteralExpression* expression) { - stack.push(context.int_val(static_cast(expression->getValueAsInt(nullptr)))); + virtual void visit(storm::expressions::IntegerLiteralExpression const* expression) override { + stack.push(context.int_val(static_cast(expression->evaluateAsInt()))); } - virtual void visit(ir::expressions::UnaryBooleanFunctionExpression* expression) { - expression->getChild()->accept(this); + virtual void visit(storm::expressions::UnaryBooleanFunctionExpression const* expression) override { + expression->getOperand()->accept(this); z3::expr childResult = stack.top(); stack.pop(); - switch (expression->getFunctionType()) { - case storm::ir::expressions::UnaryBooleanFunctionExpression::NOT: + switch (expression->getOperatorType()) { + case storm::expressions::UnaryBooleanFunctionExpression::OperatorType::Not: stack.push(!childResult); break; default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " - << "Unknown boolean binary operator: '" << expression->getFunctionType() << "' in expression " << expression->toString() << "."; + << "Unknown boolean binary operator: '" << expression->getOperatorType() << "' in expression " << expression << "."; } } - virtual void visit(ir::expressions::UnaryNumericalFunctionExpression* expression) { - expression->getChild()->accept(this); + virtual void visit(storm::expressions::UnaryNumericalFunctionExpression const* expression) override { + expression->getOperand()->accept(this); z3::expr childResult = stack.top(); stack.pop(); - switch(expression->getFunctionType()) { - case storm::ir::expressions::UnaryNumericalFunctionExpression::MINUS: + switch(expression->getOperatorType()) { + case storm::expressions::UnaryNumericalFunctionExpression::OperatorType::Minus: stack.push(0 - childResult); - break; + break; + case storm::expressions::UnaryNumericalFunctionExpression::OperatorType::Floor: { + z3::expr floorVariable = context.int_const(("__floor_" + std::to_string(additionalVariableCounter++)).c_str()); + additionalAssertions.push(z3::expr(context, Z3_mk_int2real(context, floorVariable)) <= childResult < (z3::expr(context, Z3_mk_int2real(context, floorVariable)) + 1)); + throw storm::exceptions::NotImplementedException() << "Unary numerical function 'floor' is not supported by Z3ExpressionAdapter."; + break; + } + case storm::expressions::UnaryNumericalFunctionExpression::OperatorType::Ceil:{ + z3::expr ceilVariable = context.int_const(("__floor_" + std::to_string(additionalVariableCounter++)).c_str()); + additionalAssertions.push(z3::expr(context, Z3_mk_int2real(context, ceilVariable)) - 1 <= childResult < z3::expr(context, Z3_mk_int2real(context, ceilVariable))); + throw storm::exceptions::NotImplementedException() << "Unary numerical function 'floor' is not supported by Z3ExpressionAdapter."; + break; + } default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " - << "Unknown numerical unary operator: '" << expression->getFunctionType() << "'."; + << "Unknown numerical unary operator: '" << expression->getOperatorType() << "'."; } } + + virtual void visit(storm::expressions::IfThenElseExpression const* expression) override { + expression->getCondition()->accept(this); + expression->getThenExpression()->accept(this); + expression->getElseExpression()->accept(this); + + z3::expr conditionResult = stack.top(); + stack.pop(); + z3::expr thenResult = stack.top(); + stack.pop(); + z3::expr elseResult = stack.top(); + stack.pop(); + + stack.push(z3::expr(context, Z3_mk_ite(context, conditionResult, thenResult, elseResult))); + } - virtual void visit(ir::expressions::VariableExpression* expression) { + virtual void visit(storm::expressions::VariableExpression const* expression) override { stack.push(variableToExpressionMap.at(expression->getVariableName())); } - + private: z3::context& context; std::stack stack; + std::stack additionalAssertions; + uint_fast64_t additionalVariableCounter; + std::map variableToExpressionMap; }; diff --git a/src/solver/SmtSolver.h b/src/solver/SmtSolver.h index 9c9dbce80..d71fece46 100644 --- a/src/solver/SmtSolver.h +++ b/src/solver/SmtSolver.h @@ -31,7 +31,7 @@ namespace storm { InterpolantComputation = 0x04 }; //! possible check results - enum class CheckResult {SAT, UNSAT, UNKNOWN}; + enum class CheckResult { SAT, UNSAT, UNKNOWN }; public: /*! * Constructs a new smt solver with the given options. @@ -42,6 +42,9 @@ namespace storm { SmtSolver(Options options = Options::ModelGeneration) {}; virtual ~SmtSolver() {}; + SmtSolver(const SmtSolver&) = delete; + SmtSolver(const SmtSolver&&) {}; + //! pushes a backtrackingpoint in the solver virtual void push() = 0; //! pops a backtrackingpoint in the solver