diff --git a/src/adapters/Z3ExpressionAdapter.h b/src/adapters/Z3ExpressionAdapter.h
index bd722a553..493007bb7 100644
--- a/src/adapters/Z3ExpressionAdapter.h
+++ b/src/adapters/Z3ExpressionAdapter.h
@@ -65,7 +65,7 @@ namespace storm {
variables = expression.getVariablesAndTypes();
}
catch (storm::exceptions::InvalidTypeException* e) {
- LOG_THROW(true, storm::exceptions::InvalidTypeException, "Encountered variable with ambigious type while trying to autocreate solver variables: " << e);
+ LOG_THROW(false, storm::exceptions::InvalidTypeException, "Encountered variable with ambigious type while trying to autocreate solver variables: " << e);
}
for (auto variableAndType : variables) {
@@ -82,7 +82,7 @@ namespace storm {
this->variableToExpressionMap.insert(std::make_pair(variableAndType.first, context.real_const(variableAndType.first.c_str())));
break;
default:
- LOG_THROW(true, storm::exceptions::InvalidTypeException, "Encountered variable with unknown type while trying to autocreate solver variables: " << variableAndType.first);
+ LOG_THROW(false, storm::exceptions::InvalidTypeException, "Encountered variable with unknown type while trying to autocreate solver variables: " << variableAndType.first);
break;
}
}
@@ -110,7 +110,7 @@ namespace storm {
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.");
+ LOG_THROW(false, 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()) {
@@ -118,7 +118,7 @@ namespace storm {
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.");
+ 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;
@@ -126,7 +126,7 @@ namespace storm {
if (Z3_get_numeral_rational_int64(expr.ctx(), expr, &num, &den)) {
return storm::expressions::Expression::createDoubleLiteral(static_cast<double>(num) / static_cast<double>(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.");
+ 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()) {
switch (expr.decl().decl_kind()) {
@@ -140,7 +140,7 @@ namespace storm {
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.");
+ 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 {
@@ -153,7 +153,7 @@ namespace storm {
}
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.");
+ 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 {
@@ -194,7 +194,7 @@ namespace storm {
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.");
+ 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()) {
@@ -202,15 +202,15 @@ namespace storm {
} 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.");
+ LOG_THROW(false, 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() <<".");
+ LOG_THROW(false, 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.");
+ LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Failed to convert Z3 expression. Encountered unknown expression type.");
}
}
diff --git a/src/solver/Z3SmtSolver.cpp b/src/solver/Z3SmtSolver.cpp
index ffa627ca1..eea1b5c1d 100644
--- a/src/solver/Z3SmtSolver.cpp
+++ b/src/solver/Z3SmtSolver.cpp
@@ -8,6 +8,7 @@ namespace storm {
: m_context()
, m_solver(m_context)
, m_adapter(m_context, {})
+ , lastResult(CheckResult::UNKNOWN)
#endif
{
//intentionally left empty
@@ -19,7 +20,7 @@ namespace storm {
#ifdef STORM_HAVE_Z3
this->m_solver.push();
#else
- LOG_THROW(true, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
+ LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
#endif
}
@@ -28,7 +29,7 @@ namespace storm {
#ifdef STORM_HAVE_Z3
this->m_solver.pop();
#else
- LOG_THROW(true, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
+ LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
#endif
}
@@ -37,7 +38,7 @@ namespace storm {
#ifdef STORM_HAVE_Z3
this->m_solver.pop((unsigned int)n);
#else
- LOG_THROW(true, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
+ LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
#endif
}
@@ -46,7 +47,7 @@ namespace storm {
#ifdef STORM_HAVE_Z3
this->m_solver.reset();
#else
- LOG_THROW(true, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
+ LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
#endif
}
@@ -55,25 +56,27 @@ namespace storm {
#ifdef STORM_HAVE_Z3
this->m_solver.add(m_adapter.translateExpression(e, true));
#else
- LOG_THROW(true, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
+ LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
#endif
}
SmtSolver::CheckResult Z3SmtSolver::check()
{
#ifdef STORM_HAVE_Z3
- switch (this->m_solver.check())
- {
+ switch (this->m_solver.check()) {
case z3::sat:
- return SmtSolver::CheckResult::SAT;
+ this->lastResult = SmtSolver::CheckResult::SAT;
+ break;
case z3::unsat:
- return SmtSolver::CheckResult::UNSAT;
+ this->lastResult = SmtSolver::CheckResult::UNSAT;
+ break;
default:
+ this->lastResult = SmtSolver::CheckResult::UNKNOWN;
break;
}
- return SmtSolver::CheckResult::UNKNOWN;
+ return this->lastResult;
#else
- LOG_THROW(true, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
+ LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
#endif
}
@@ -86,18 +89,20 @@ namespace storm {
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;
+ switch (this->m_solver.check(z3Assumptions)) {
+ case z3::sat:
+ this->lastResult = SmtSolver::CheckResult::SAT;
+ break;
+ case z3::unsat:
+ this->lastResult = SmtSolver::CheckResult::UNSAT;
+ break;
+ default:
+ this->lastResult = SmtSolver::CheckResult::UNKNOWN;
+ break;
}
- return SmtSolver::CheckResult::UNKNOWN;
+ return this->lastResult;
#else
- LOG_THROW(true, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
+ LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
#endif
}
@@ -110,45 +115,76 @@ namespace storm {
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;
+ switch (this->m_solver.check(z3Assumptions)) {
+ case z3::sat:
+ this->lastResult = SmtSolver::CheckResult::SAT;
+ break;
+ case z3::unsat:
+ this->lastResult = SmtSolver::CheckResult::UNSAT;
+ break;
+ default:
+ this->lastResult = SmtSolver::CheckResult::UNKNOWN;
+ break;
}
- return SmtSolver::CheckResult::UNKNOWN;
+ return this->lastResult;
#else
- LOG_THROW(true, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
+ LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
#endif
}
storm::expressions::SimpleValuation Z3SmtSolver::getModel()
{
#ifdef STORM_HAVE_Z3
- LOG_THROW(true, storm::exceptions::NotImplementedException, "Model generation is not implemented in this Z3 solver interface.");
+
+ LOG_THROW(this->lastResult == SmtSolver::CheckResult::SAT, storm::exceptions::InvalidStateException, "Requested Model but last check result was not SAT.");
+
+ z3::model m = this->m_solver.get_model();
+ storm::expressions::SimpleValuation stormModel;
+
+ for (unsigned i = 0; i < m.num_consts(); ++i) {
+ z3::func_decl var_i = m.get_const_decl(i);
+ storm::expressions::Expression var_i_interp = this->m_adapter.translateExpression(m.get_const_interp(var_i));
+
+ switch (var_i_interp.getReturnType()) {
+ case storm::expressions::ExpressionReturnType::Bool:
+ stormModel.addBooleanIdentifier(var_i.name().str(), var_i_interp.evaluateAsBool());
+ break;
+ case storm::expressions::ExpressionReturnType::Int:
+ stormModel.addIntegerIdentifier(var_i.name().str(), var_i_interp.evaluateAsInt());
+ break;
+ case storm::expressions::ExpressionReturnType::Double:
+ stormModel.addDoubleIdentifier(var_i.name().str(), var_i_interp.evaluateAsDouble());
+ break;
+ default:
+ LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Variable interpretation in model is not of type bool, int or double.")
+ break;
+ }
+
+ }
+
+
+
+ LOG_THROW(false, storm::exceptions::NotImplementedException, "Model generation is not implemented in this Z3 solver interface.");
#else
- LOG_THROW(true, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
+ LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
#endif
}
std::set<storm::expressions::SimpleValuation> Z3SmtSolver::solveAndDiversify(std::set<storm::expressions::SimpleValuation> diversifyers)
{
#ifdef STORM_HAVE_Z3
- LOG_THROW(true, storm::exceptions::NotImplementedException, "Model generation is not implemented in this Z3 solver interface.");
+ LOG_THROW(false, storm::exceptions::NotImplementedException, "Model generation is not implemented in this Z3 solver interface.");
#else
- LOG_THROW(true, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
+ LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
#endif
}
uint_fast64_t Z3SmtSolver::solveAndDiversify(std::set<storm::expressions::SimpleValuation> diversifyers, std::function<bool(storm::expressions::Valuation&) > callback)
{
#ifdef STORM_HAVE_Z3
- LOG_THROW(true, storm::exceptions::NotImplementedException, "Model generation is not implemented in this Z3 solver interface.");
+ LOG_THROW(false, storm::exceptions::NotImplementedException, "Model generation is not implemented in this Z3 solver interface.");
#else
- LOG_THROW(true, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
+ LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
#endif
}
diff --git a/src/solver/Z3SmtSolver.h b/src/solver/Z3SmtSolver.h
index 916b69b91..672eba271 100644
--- a/src/solver/Z3SmtSolver.h
+++ b/src/solver/Z3SmtSolver.h
@@ -43,6 +43,8 @@ namespace storm {
z3::context m_context;
z3::solver m_solver;
storm::adapters::Z3ExpressionAdapter m_adapter;
+
+ CheckResult lastResult;
#endif
};
}
diff --git a/test/functional/adapter/Z3ExpressionAdapterTest.cpp b/test/functional/adapter/Z3ExpressionAdapterTest.cpp
index b31dd0f7b..618d86faa 100644
--- a/test/functional/adapter/Z3ExpressionAdapterTest.cpp
+++ b/test/functional/adapter/Z3ExpressionAdapterTest.cpp
@@ -161,3 +161,44 @@ TEST(Z3ExpressionAdapter, StormToZ3FloorCeil) {
#endif
}
+TEST(Z3ExpressionAdapter, Z3ToStormBasic) {
+#ifdef STORM_HAVE_Z3
+ z3::context ctx;
+
+ unsigned args = 2;
+
+ storm::adapters::Z3ExpressionAdapter adapter(ctx, {});
+
+ z3::expr z3True = ctx.bool_val(true);
+ storm::expressions::Expression exprTrue;
+ ASSERT_NO_THROW(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));
+ 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));
+ ASSERT_EQ(storm::expressions::OperatorType::And, exprConjunction.getOperator());
+ ASSERT_TRUE(exprConjunction.getOperand(0).isVariable());
+ ASSERT_EQ("x", exprConjunction.getOperand(0).getIdentifier());
+ ASSERT_TRUE(exprConjunction.getOperand(1).isVariable());
+ ASSERT_EQ("y", exprConjunction.getOperand(1).getIdentifier());
+
+ z3::expr z3Nor = !(ctx.bool_const("x") || ctx.bool_const("y"));
+ storm::expressions::Expression exprNor;
+ ASSERT_NO_THROW(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());
+ ASSERT_EQ("x", exprNor.getOperand(0).getOperand(0).getIdentifier());
+ ASSERT_TRUE(exprNor.getOperand(0).getOperand(1).isVariable());
+ ASSERT_EQ("y", exprNor.getOperand(0).getOperand(1).getIdentifier());
+
+#else
+ ASSERT_TRUE(false) << "StoRM built without Z3 support.";
+#endif
+}
\ No newline at end of file
diff --git a/test/functional/solver/Z3SmtSolverTest.cpp b/test/functional/solver/Z3SmtSolverTest.cpp
index 5560af25d..61a082a45 100644
--- a/test/functional/solver/Z3SmtSolverTest.cpp
+++ b/test/functional/solver/Z3SmtSolverTest.cpp
@@ -126,7 +126,6 @@ TEST(Z3SmtSolver, Backtracking) {
#endif
}
-
TEST(Z3SmtSolver, Assumptions) {
#ifdef STORM_HAVE_Z3
storm::solver::Z3SmtSolver s;
@@ -160,3 +159,31 @@ TEST(Z3SmtSolver, Assumptions) {
ASSERT_TRUE(false) << "StoRM built without Z3 support.";
#endif
}
+
+TEST(Z3SmtSolver, GenerateModel) {
+#ifdef STORM_HAVE_Z3
+ storm::solver::Z3SmtSolver s;
+ storm::solver::Z3SmtSolver::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;
+
+ ASSERT_NO_THROW(s.assertExpression(exprFormula));
+ ASSERT_NO_THROW(result = s.check());
+ ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT);
+ storm::expressions::SimpleValuation model;
+ ASSERT_NO_THROW(model = s.getModel());
+ int_fast64_t a_eval;
+ ASSERT_NO_THROW(a_eval = model.getIntegerValue("a"));
+ ASSERT_EQ(1, a_eval);
+
+#else
+ ASSERT_TRUE(false) << "StoRM built without Z3 support.";
+#endif
+}
\ No newline at end of file