Browse Source

added implementation for Z3LpSolver::getValue() when z3_optimize is not available

tempestpy_adaptions
TimQu 8 years ago
parent
commit
fd24a2586c
  1. 6
      src/storm/solver/Z3LpSolver.cpp

6
src/storm/solver/Z3LpSolver.cpp

@ -188,7 +188,7 @@ namespace storm {
z3::expr z3Var = this->expressionAdapter->translateExpression(variable); z3::expr z3Var = this->expressionAdapter->translateExpression(variable);
return this->expressionAdapter->translateExpression(lastCheckModel->eval(z3Var, true)); return this->expressionAdapter->translateExpression(lastCheckModel->eval(z3Var, true));
} }
double Z3LpSolver::getContinuousValue(storm::expressions::Variable const& variable) const { double Z3LpSolver::getContinuousValue(storm::expressions::Variable const& variable) const {
storm::expressions::Expression value = getValue(variable); storm::expressions::Expression value = getValue(variable);
if(value.getBaseExpression().isIntegerLiteralExpression()) { if(value.getBaseExpression().isIntegerLiteralExpression()) {
@ -398,6 +398,10 @@ namespace storm {
bool Z3LpSolver::isOptimal() const { 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."; 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 { 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."; 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.";

Loading…
Cancel
Save