From 71731e8003841bb38cd02cb7e1f1d8222b7b55e6 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Thu, 23 May 2019 18:55:29 +0200
Subject: [PATCH] Z3LpSolver: Fixed incremental support.

---
 src/storm/solver/Z3LpSolver.cpp | 66 ++++++++++++++++++++++++++++-----
 src/storm/solver/Z3LpSolver.h   |  3 ++
 2 files changed, 59 insertions(+), 10 deletions(-)

diff --git a/src/storm/solver/Z3LpSolver.cpp b/src/storm/solver/Z3LpSolver.cpp
index 16c04bd57..a43388c67 100644
--- a/src/storm/solver/Z3LpSolver.cpp
+++ b/src/storm/solver/Z3LpSolver.cpp
@@ -25,7 +25,7 @@ namespace storm {
 #ifdef STORM_HAVE_Z3_OPTIMIZE
         
         template<typename ValueType>
-        Z3LpSolver<ValueType>::Z3LpSolver(std::string const& name, OptimizationDirection const& optDir) : LpSolver<ValueType>(optDir) {
+        Z3LpSolver<ValueType>::Z3LpSolver(std::string const& name, OptimizationDirection const& optDir) : LpSolver<ValueType>(optDir), isIncremental(false) {
             z3::config config;
             config.set("model", true);
             context = std::unique_ptr<z3::context>(new z3::context(config));
@@ -64,7 +64,12 @@ namespace storm {
         
         template<typename ValueType>
         storm::expressions::Variable Z3LpSolver<ValueType>::addBoundedContinuousVariable(std::string const& name, ValueType lowerBound, ValueType upperBound, ValueType objectiveFunctionCoefficient) {
-            storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getRationalType());
+            storm::expressions::Variable newVariable;
+            if (isIncremental) {
+                newVariable = this->manager->declareOrGetVariable(name, this->manager->getRationalType());
+            } else {
+                newVariable = this->manager->declareVariable(name, this->manager->getRationalType());
+            }
             solver->add(expressionAdapter->translateExpression((newVariable.getExpression() >= this->manager->rational(lowerBound)) && (newVariable.getExpression() <= this->manager->rational(upperBound))));
             optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable;
             return newVariable;
@@ -72,7 +77,12 @@ namespace storm {
         
         template<typename ValueType>
         storm::expressions::Variable Z3LpSolver<ValueType>::addLowerBoundedContinuousVariable(std::string const& name, ValueType lowerBound, ValueType objectiveFunctionCoefficient) {
-            storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getRationalType());
+            storm::expressions::Variable newVariable;
+            if (isIncremental) {
+                newVariable = this->manager->declareOrGetVariable(name, this->manager->getRationalType());
+            } else {
+                newVariable = this->manager->declareVariable(name, this->manager->getRationalType());
+            }
             solver->add(expressionAdapter->translateExpression(newVariable.getExpression() >= this->manager->rational(lowerBound)));
             optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable;
             return newVariable;
@@ -80,7 +90,12 @@ namespace storm {
 
         template<typename ValueType>
         storm::expressions::Variable Z3LpSolver<ValueType>::addUpperBoundedContinuousVariable(std::string const& name, ValueType upperBound, ValueType objectiveFunctionCoefficient) {
-            storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getRationalType());
+            storm::expressions::Variable newVariable;
+            if (isIncremental) {
+                newVariable = this->manager->declareOrGetVariable(name, this->manager->getRationalType());
+            } else {
+                newVariable = this->manager->declareVariable(name, this->manager->getRationalType());
+            }
             solver->add(expressionAdapter->translateExpression(newVariable.getExpression() <= this->manager->rational(upperBound)));
             optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable;
             return newVariable;
@@ -88,14 +103,24 @@ namespace storm {
 
         template<typename ValueType>
         storm::expressions::Variable Z3LpSolver<ValueType>::addUnboundedContinuousVariable(std::string const& name, ValueType objectiveFunctionCoefficient) {
-            storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getRationalType());
+            storm::expressions::Variable newVariable;
+            if (isIncremental) {
+                newVariable = this->manager->declareOrGetVariable(name, this->manager->getRationalType());
+            } else {
+                newVariable = this->manager->declareVariable(name, this->manager->getRationalType());
+            }
             optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable;
             return newVariable;
         }
         
         template<typename ValueType>
         storm::expressions::Variable Z3LpSolver<ValueType>::addBoundedIntegerVariable(std::string const& name, ValueType lowerBound, ValueType upperBound, ValueType objectiveFunctionCoefficient) {
-            storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getIntegerType());
+            storm::expressions::Variable newVariable;
+            if (isIncremental) {
+                newVariable = this->manager->declareOrGetVariable(name, this->manager->getIntegerType());
+            } else {
+                newVariable = this->manager->declareVariable(name, this->manager->getIntegerType());
+            }
             solver->add(expressionAdapter->translateExpression((newVariable.getExpression() >= this->manager->rational(lowerBound)) && (newVariable.getExpression() <= this->manager->rational(upperBound))));
             optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable;
             return newVariable;
@@ -103,7 +128,12 @@ namespace storm {
         
         template<typename ValueType>
         storm::expressions::Variable Z3LpSolver<ValueType>::addLowerBoundedIntegerVariable(std::string const& name, ValueType lowerBound, ValueType objectiveFunctionCoefficient) {
-            storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getIntegerType());
+            storm::expressions::Variable newVariable;
+            if (isIncremental) {
+                newVariable = this->manager->declareOrGetVariable(name, this->manager->getIntegerType());
+            } else {
+                newVariable = this->manager->declareVariable(name, this->manager->getIntegerType());
+            }
             solver->add(expressionAdapter->translateExpression(newVariable.getExpression() >= this->manager->rational(lowerBound)));
             optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable;
             return newVariable;
@@ -111,7 +141,12 @@ namespace storm {
         
         template<typename ValueType>
         storm::expressions::Variable Z3LpSolver<ValueType>::addUpperBoundedIntegerVariable(std::string const& name, ValueType upperBound, ValueType objectiveFunctionCoefficient) {
-            storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getIntegerType());
+            storm::expressions::Variable newVariable;
+            if (isIncremental) {
+                newVariable = this->manager->declareOrGetVariable(name, this->manager->getIntegerType());
+            } else {
+                newVariable = this->manager->declareVariable(name, this->manager->getIntegerType());
+            }
             solver->add(expressionAdapter->translateExpression(newVariable.getExpression() <= this->manager->rational(upperBound)));
             optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable;
             return newVariable;
@@ -119,14 +154,24 @@ namespace storm {
         
         template<typename ValueType>
         storm::expressions::Variable Z3LpSolver<ValueType>::addUnboundedIntegerVariable(std::string const& name, ValueType objectiveFunctionCoefficient) {
-            storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getIntegerType());
+            storm::expressions::Variable newVariable;
+            if (isIncremental) {
+                newVariable = this->manager->declareOrGetVariable(name, this->manager->getIntegerType());
+            } else {
+                newVariable = this->manager->declareVariable(name, this->manager->getIntegerType());
+            }
             optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable;
             return newVariable;
         }
         
         template<typename ValueType>
         storm::expressions::Variable Z3LpSolver<ValueType>::addBinaryVariable(std::string const& name, ValueType objectiveFunctionCoefficient) {
-            storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getIntegerType());
+            storm::expressions::Variable newVariable;
+            if (isIncremental) {
+                newVariable = this->manager->declareOrGetVariable(name, this->manager->getIntegerType());
+            } else {
+                newVariable = this->manager->declareVariable(name, this->manager->getIntegerType());
+            }
             solver->add(expressionAdapter->translateExpression((newVariable.getExpression() >= this->manager->rational(storm::utility::zero<storm::RationalNumber>())) && (newVariable.getExpression() <= this->manager->rational(storm::utility::one<storm::RationalNumber>()))));
             optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable;
             return newVariable;
@@ -266,6 +311,7 @@ namespace storm {
         template<typename ValueType>
         void Z3LpSolver<ValueType>::pop()  {
             solver->pop();
+            isIncremental = true;
         }
 
 #else
diff --git a/src/storm/solver/Z3LpSolver.h b/src/storm/solver/Z3LpSolver.h
index a1877091c..ece5951f0 100644
--- a/src/storm/solver/Z3LpSolver.h
+++ b/src/storm/solver/Z3LpSolver.h
@@ -116,6 +116,9 @@ namespace storm {
             mutable bool lastCheckUnbounded;
             mutable std::unique_ptr<z3::expr> lastCheckObjectiveValue;
             mutable std::unique_ptr<z3::model> lastCheckModel;
+            
+            // Stores whether this solver is used in an incremental way (with push() and pop())
+            bool isIncremental;
 
             // An expression adapter that is used for translating the expression into Z3's format.
             std::unique_ptr<storm::adapters::Z3ExpressionAdapter> expressionAdapter;