From 93c03fff3f94d8c68e24dfcbe745a669e32cb871 Mon Sep 17 00:00:00 2001 From: David_Korzeniewski Date: Wed, 25 Jun 2014 10:44:35 +0200 Subject: [PATCH] Fixed order of checks in Z3ExpressionAdapter, fixed missing override of isVariable in VariableExpression, removed unnecessary exception in Z3SmtSolver model generation Former-commit-id: ca5f876655762309afaa98af8341aa7520872308 --- src/adapters/Z3ExpressionAdapter.h | 28 +++++++++++++++++-- src/solver/Z3SmtSolver.cpp | 3 -- .../expressions/VariableExpression.cpp | 4 +++ src/storage/expressions/VariableExpression.h | 1 + .../adapter/Z3ExpressionAdapterTest.cpp | 8 +++--- test/functional/solver/Z3SmtSolverTest.cpp | 8 +++--- 6 files changed, 39 insertions(+), 13 deletions(-) diff --git a/src/adapters/Z3ExpressionAdapter.h b/src/adapters/Z3ExpressionAdapter.h index 493007bb7..5a59c6cd7 100644 --- a/src/adapters/Z3ExpressionAdapter.h +++ b/src/adapters/Z3ExpressionAdapter.h @@ -102,6 +102,11 @@ namespace storm { } storm::expressions::Expression translateExpression(z3::expr const& expr) { + //std::cout << std::boolalpha << expr.is_var() << std::endl; + //std::cout << std::boolalpha << expr.is_app() << std::endl; + //std::cout << expr.decl().decl_kind() << std::endl; + + /* if (expr.is_bool() && expr.is_const()) { switch (Z3_get_bool_value(expr.ctx(), expr)) { case Z3_L_FALSE: @@ -128,7 +133,8 @@ namespace storm { } else { LOG_THROW(false, 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()) { + } else */ + if (expr.is_app()) { switch (expr.decl().decl_kind()) { case Z3_OP_TRUE: return storm::expressions::Expression::createTrue(); @@ -192,8 +198,26 @@ namespace storm { 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_ANUM: + //Arithmetic numeral + 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(false, 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(false, 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."); + } + } case Z3_OP_UNINTERPRETED: - //this should be a variable... + //storm only supports uninterpreted constant functions 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()); diff --git a/src/solver/Z3SmtSolver.cpp b/src/solver/Z3SmtSolver.cpp index eea1b5c1d..9dbe3a9b7 100644 --- a/src/solver/Z3SmtSolver.cpp +++ b/src/solver/Z3SmtSolver.cpp @@ -162,9 +162,6 @@ namespace storm { } - - - LOG_THROW(false, storm::exceptions::NotImplementedException, "Model generation is not implemented in this Z3 solver interface."); #else LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support."); #endif diff --git a/src/storage/expressions/VariableExpression.cpp b/src/storage/expressions/VariableExpression.cpp index e28bbc7cd..a9f714569 100644 --- a/src/storage/expressions/VariableExpression.cpp +++ b/src/storage/expressions/VariableExpression.cpp @@ -48,6 +48,10 @@ namespace storm { bool VariableExpression::containsVariables() const { return true; } + + bool VariableExpression::isVariable() const { + return true; + } std::set VariableExpression::getVariables() const { return {this->getVariableName()}; diff --git a/src/storage/expressions/VariableExpression.h b/src/storage/expressions/VariableExpression.h index 439cd3155..dda150495 100644 --- a/src/storage/expressions/VariableExpression.h +++ b/src/storage/expressions/VariableExpression.h @@ -31,6 +31,7 @@ namespace storm { virtual double evaluateAsDouble(Valuation const* valuation = nullptr) const override; virtual std::string const& getIdentifier() const override; virtual bool containsVariables() const override; + virtual bool isVariable() const override; virtual std::set getVariables() const override; virtual std::map getVariablesAndTypes() const override; virtual std::shared_ptr simplify() const override; diff --git a/test/functional/adapter/Z3ExpressionAdapterTest.cpp b/test/functional/adapter/Z3ExpressionAdapterTest.cpp index 618d86faa..ce7abc105 100644 --- a/test/functional/adapter/Z3ExpressionAdapterTest.cpp +++ b/test/functional/adapter/Z3ExpressionAdapterTest.cpp @@ -171,17 +171,17 @@ TEST(Z3ExpressionAdapter, Z3ToStormBasic) { z3::expr z3True = ctx.bool_val(true); storm::expressions::Expression exprTrue; - ASSERT_NO_THROW(exprTrue = adapter.translateExpression(z3True)); + exprTrue = adapter.translateExpression(z3True); ASSERT_TRUE(exprTrue.isTrue()); z3::expr z3False = ctx.bool_val(false); storm::expressions::Expression exprFalse; - ASSERT_NO_THROW(exprFalse = adapter.translateExpression(z3False)); + exprFalse = adapter.translateExpression(z3False); ASSERT_TRUE(exprFalse.isFalse()); z3::expr z3Conjunction = (ctx.bool_const("x") && ctx.bool_const("y")); storm::expressions::Expression exprConjunction; - ASSERT_NO_THROW(exprConjunction = adapter.translateExpression(z3Conjunction)); + (exprConjunction = adapter.translateExpression(z3Conjunction)); ASSERT_EQ(storm::expressions::OperatorType::And, exprConjunction.getOperator()); ASSERT_TRUE(exprConjunction.getOperand(0).isVariable()); ASSERT_EQ("x", exprConjunction.getOperand(0).getIdentifier()); @@ -190,7 +190,7 @@ TEST(Z3ExpressionAdapter, Z3ToStormBasic) { z3::expr z3Nor = !(ctx.bool_const("x") || ctx.bool_const("y")); storm::expressions::Expression exprNor; - ASSERT_NO_THROW(exprNor = adapter.translateExpression(z3Nor)); + (exprNor = adapter.translateExpression(z3Nor)); ASSERT_EQ(storm::expressions::OperatorType::Not, exprNor.getOperator()); ASSERT_EQ(storm::expressions::OperatorType::Or, exprNor.getOperand(0).getOperator()); ASSERT_TRUE(exprNor.getOperand(0).getOperand(0).isVariable()); diff --git a/test/functional/solver/Z3SmtSolverTest.cpp b/test/functional/solver/Z3SmtSolverTest.cpp index 61a082a45..e33a2be4f 100644 --- a/test/functional/solver/Z3SmtSolverTest.cpp +++ b/test/functional/solver/Z3SmtSolverTest.cpp @@ -174,13 +174,13 @@ TEST(Z3SmtSolver, GenerateModel) { && c == (a * b) && b + a > c; - ASSERT_NO_THROW(s.assertExpression(exprFormula)); - ASSERT_NO_THROW(result = s.check()); + (s.assertExpression(exprFormula)); + (result = s.check()); ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT); storm::expressions::SimpleValuation model; - ASSERT_NO_THROW(model = s.getModel()); + (model = s.getModel()); int_fast64_t a_eval; - ASSERT_NO_THROW(a_eval = model.getIntegerValue("a")); + (a_eval = model.getIntegerValue("a")); ASSERT_EQ(1, a_eval); #else