diff --git a/src/adapters/Z3ExpressionAdapter.h b/src/adapters/Z3ExpressionAdapter.h index 8d780f218..b7c1781fd 100644 --- a/src/adapters/Z3ExpressionAdapter.h +++ b/src/adapters/Z3ExpressionAdapter.h @@ -99,6 +99,119 @@ namespace storm { return result; } + storm::expressions::Expression translateExpression(z3::expr const& expr) { + if (expr.is_bool() && expr.is_const()) { + switch (Z3_get_bool_value(expr.ctx(), expr)) { + case Z3_L_FALSE: + return storm::expressions::Expression::createFalse(); + case Z3_L_TRUE: + return storm::expressions::Expression::createTrue(); + break; + default: + LOG_THROW(true, storm::exceptions::ExpressionEvaluationException, "Failed to convert Z3 expression. Expression is constant boolean, but value is undefined."); + break; + } + } else if (expr.is_int() && expr.is_const()) { + int_fast64_t value; + if (Z3_get_numeral_int64(expr.ctx(), expr, &value)) { + return storm::expressions::Expression::createIntegerLiteral(value); + } else { + LOG_THROW(true, storm::exceptions::ExpressionEvaluationException, "Failed to convert Z3 expression. Expression is constant integer and value does not fit into 64-bit integer."); + } + } else if (expr.is_real() && expr.is_const()) { + int_fast64_t num; + int_fast64_t den; + if (Z3_get_numeral_rational_int64(expr.ctx(), expr, &num, &den)) { + return storm::expressions::Expression::createDoubleLiteral(static_cast(num) / static_cast(den)); + } else { + LOG_THROW(true, storm::exceptions::ExpressionEvaluationException, "Failed to convert Z3 expression. Expression is constant real and value does not fit into a fraction with 64-bit integer numerator and denominator."); + } + } else if (expr.is_app()) { + switch (expr.decl().decl_kind()) { + case Z3_OP_TRUE: + return storm::expressions::Expression::createTrue(); + case Z3_OP_FALSE: + return storm::expressions::Expression::createFalse(); + 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))); + case Z3_OP_AND: { + unsigned args = expr.num_args(); + LOG_THROW(args == 0, storm::exceptions::ExpressionEvaluationException, "Failed to convert Z3 expression. 0-ary AND is assumed to be an error."); + if (args == 1) { + return this->translateExpression(expr.arg(0)); + } else { + storm::expressions::Expression retVal = this->translateExpression(expr.arg(0)); + for (unsigned i = 1; i < args; i++) { + retVal = retVal && this->translateExpression(expr.arg(i)); + } + return retVal; + } + } + case Z3_OP_OR: { + unsigned args = expr.num_args(); + LOG_THROW(args == 0, storm::exceptions::ExpressionEvaluationException, "Failed to convert Z3 expression. 0-ary OR is assumed to be an error."); + if (args == 1) { + return this->translateExpression(expr.arg(0)); + } else { + storm::expressions::Expression retVal = this->translateExpression(expr.arg(0)); + for (unsigned i = 1; i < args; i++) { + retVal = retVal || this->translateExpression(expr.arg(i)); + } + return retVal; + } + } + case Z3_OP_IFF: + return this->translateExpression(expr.arg(0)).iff(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))); + case Z3_OP_LE: + return this->translateExpression(expr.arg(0)) <= this->translateExpression(expr.arg(1)); + case Z3_OP_GE: + return this->translateExpression(expr.arg(0)) >= this->translateExpression(expr.arg(1)); + case Z3_OP_LT: + return this->translateExpression(expr.arg(0)) < this->translateExpression(expr.arg(1)); + case Z3_OP_GT: + return this->translateExpression(expr.arg(0)) > this->translateExpression(expr.arg(1)); + case Z3_OP_ADD: + return this->translateExpression(expr.arg(0)) + this->translateExpression(expr.arg(1)); + case Z3_OP_SUB: + return this->translateExpression(expr.arg(0)) - this->translateExpression(expr.arg(1)); + case Z3_OP_UMINUS: + return -this->translateExpression(expr.arg(0)); + case Z3_OP_MUL: + return this->translateExpression(expr.arg(0)) * this->translateExpression(expr.arg(1)); + case Z3_OP_DIV: + return this->translateExpression(expr.arg(0)) / this->translateExpression(expr.arg(1)); + case Z3_OP_IDIV: + return this->translateExpression(expr.arg(0)) / this->translateExpression(expr.arg(1)); + case Z3_OP_UNINTERPRETED: + //this should be a variable... + LOG_THROW(!expr.is_const(), storm::exceptions::ExpressionEvaluationException, "Failed to convert Z3 expression. Encountered non constant uninterpreted function."); + if (expr.is_bool()) { + return storm::expressions::Expression::createBooleanVariable(expr.decl().name().str()); + } else if (expr.is_int()) { + return storm::expressions::Expression::createIntegerVariable(expr.decl().name().str()); + } else if (expr.is_real()) { + return storm::expressions::Expression::createDoubleVariable(expr.decl().name().str()); + } else { + LOG_THROW(true, storm::exceptions::ExpressionEvaluationException, "Failed to convert Z3 expression. Encountered constant uninterpreted function of unknown sort."); + } + + default: + LOG_THROW(true, storm::exceptions::ExpressionEvaluationException, "Failed to convert Z3 expression. Encountered unhandled Z3_decl_kind " << expr.decl().kind() <<"."); + break; + } + } else { + LOG_THROW(true, storm::exceptions::ExpressionEvaluationException, "Failed to convert Z3 expression. Encountered unknown expression type."); + } + } + virtual void visit(storm::expressions::BinaryBooleanFunctionExpression const* expression) override { expression->getFirstOperand()->accept(this); expression->getSecondOperand()->accept(this); @@ -125,7 +238,7 @@ namespace storm { 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->getOperatorType() << "' in expression " << expression << "."; + << "Unknown boolean binary operator: '" << static_cast(expression->getOperatorType()) << "' in expression " << expression << "."; } } @@ -159,7 +272,7 @@ namespace storm { stack.push(ite(leftResult >= rightResult, leftResult, rightResult)); break; default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " - << "Unknown numerical binary operator: '" << expression->getOperatorType() << "' in expression " << expression << "."; + << "Unknown numerical binary operator: '" << static_cast(expression->getOperatorType()) << "' in expression " << expression << "."; } } @@ -192,7 +305,7 @@ namespace storm { stack.push(leftResult >= rightResult); break; default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " - << "Unknown boolean binary operator: '" << expression->getRelationType() << "' in expression " << expression << "."; + << "Unknown boolean binary operator: '" << static_cast(expression->getRelationType()) << "' in expression " << expression << "."; } } @@ -221,7 +334,7 @@ namespace storm { stack.push(!childResult); break; default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " - << "Unknown boolean binary operator: '" << expression->getOperatorType() << "' in expression " << expression << "."; + << "Unknown boolean binary operator: '" << static_cast(expression->getOperatorType()) << "' in expression " << expression << "."; } } @@ -248,7 +361,7 @@ namespace storm { break; } default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " - << "Unknown numerical unary operator: '" << expression->getOperatorType() << "'."; + << "Unknown numerical unary operator: '" << static_cast(expression->getOperatorType()) << "'."; } } diff --git a/src/solver/SmtSolver.h b/src/solver/SmtSolver.h index 296a984b0..4337217c1 100644 --- a/src/solver/SmtSolver.h +++ b/src/solver/SmtSolver.h @@ -71,11 +71,12 @@ namespace storm { //! assert a set of expressions in the solver //! @param es the asserted expressions //! @see assert(storm::expressions::Expression &e) + /* std::hash unavailable for expressions virtual void assertExpression(std::unordered_set &es) { for (storm::expressions::Expression e : es) { this->assertExpression(e); } - } + }*/ //! assert a set of expressions in the solver //! @param es the asserted expressions //! @see assert(storm::expressions::Expression &e) @@ -102,7 +103,9 @@ namespace storm { //! @param es the asserted expressions //! @throws IllegalArgumentTypeException if the return type of one of the expressions is not bool //! @see check() + /* std::hash unavailable for expressions virtual CheckResult checkWithAssumptions(std::unordered_set &assumptions) = 0; + */ //! check satisfiability of the conjunction of the currently asserted expressions and the provided assumptions //! @param es the asserted expressions //! @throws IllegalArgumentTypeException if the return type of one of the expressions is not bool diff --git a/src/solver/Z3SmtSolver.cpp b/src/solver/Z3SmtSolver.cpp index 33495a9fa..f108e7e7d 100644 --- a/src/solver/Z3SmtSolver.cpp +++ b/src/solver/Z3SmtSolver.cpp @@ -23,7 +23,7 @@ namespace storm { void Z3SmtSolver::pop(uint_fast64_t n) { - this->m_solver.pop(n); + this->m_solver.pop((unsigned int)n); } void Z3SmtSolver::reset() @@ -68,25 +68,6 @@ namespace storm { } } - SmtSolver::CheckResult Z3SmtSolver::checkWithAssumptions(std::unordered_set &assumptions) - { - z3::expr_vector z3Assumptions(this->m_context); - - for (storm::expressions::Expression assumption : assumptions) { - z3Assumptions.push_back(this->m_adapter.translateExpression(assumption)); - } - - switch (this->m_solver.check(z3Assumptions)) - { - case z3::sat: - return SmtSolver::CheckResult::SAT; - case z3::unsat: - return SmtSolver::CheckResult::UNSAT; - default: - break; - } - } - SmtSolver::CheckResult Z3SmtSolver::checkWithAssumptions(std::initializer_list &assumptions) { z3::expr_vector z3Assumptions(this->m_context); diff --git a/src/solver/Z3SmtSolver.h b/src/solver/Z3SmtSolver.h index c9f81447d..7fdf21307 100644 --- a/src/solver/Z3SmtSolver.h +++ b/src/solver/Z3SmtSolver.h @@ -28,8 +28,6 @@ namespace storm { virtual CheckResult checkWithAssumptions(std::set &assumptions); - virtual CheckResult checkWithAssumptions(std::unordered_set &assumptions); - virtual CheckResult checkWithAssumptions(std::initializer_list &assumptions); virtual storm::expressions::SimpleValuation getModel(); diff --git a/src/storage/expressions/Expression.cpp b/src/storage/expressions/Expression.cpp index 09810bb31..347d9a778 100644 --- a/src/storage/expressions/Expression.cpp +++ b/src/storage/expressions/Expression.cpp @@ -100,7 +100,7 @@ namespace storm { return this->getBaseExpression().getVariables(); } - std::map Expression::getVariablesAndTypes(bool validate = true) const { + std::map Expression::getVariablesAndTypes(bool validate) const { if (validate) { std::map result = this->getBaseExpression().getVariablesAndTypes(); this->check(result); @@ -125,10 +125,6 @@ namespace storm { return LinearityCheckVisitor().check(*this); } - std::set Expression::getVariables() const { - return this->getBaseExpression().getVariables(); - } - BaseExpression const& Expression::getBaseExpression() const { return *this->expressionPtr; }