From fd24a2586c0d47909178b5a300d5b9b989e84613 Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 22 Feb 2017 18:52:24 +0100 Subject: [PATCH] added implementation for Z3LpSolver::getValue() when z3_optimize is not available --- src/storm/solver/Z3LpSolver.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/storm/solver/Z3LpSolver.cpp b/src/storm/solver/Z3LpSolver.cpp index e49845eef..45ffbd7be 100644 --- a/src/storm/solver/Z3LpSolver.cpp +++ b/src/storm/solver/Z3LpSolver.cpp @@ -188,7 +188,7 @@ namespace storm { z3::expr z3Var = this->expressionAdapter->translateExpression(variable); return this->expressionAdapter->translateExpression(lastCheckModel->eval(z3Var, true)); } - + double Z3LpSolver::getContinuousValue(storm::expressions::Variable const& variable) const { storm::expressions::Expression value = getValue(variable); if(value.getBaseExpression().isIntegerLiteralExpression()) { @@ -398,6 +398,10 @@ namespace storm { bool Z3LpSolver::isOptimal() const { throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; } + + storm::expressions::Expression Z3LpSolver::getValue(storm::expressions::Variable const& variable) const { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; + } double Z3LpSolver::getContinuousValue(storm::expressions::Variable const&) const { throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";