added Z3LPSolver

src/storm/solver/Z3LPSolver.cpp

@@ -0,0 +1,306 @@
+#include "storm/solver/Z3LpSolver.h"
+
+#include <numeric>
+
+#include "storm/storage/expressions/LinearCoefficientVisitor.h"
+
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/modules/DebugSettings.h"
+
+#include "storm/utility/macros.h"
+#include "storm/utility/constants.h"
+#include "storm/storage/expressions/Expression.h"
+#include "storm/storage/expressions/ExpressionManager.h"
+
+#include "storm/exceptions/InvalidStateException.h"
+#include "storm/exceptions/InvalidAccessException.h"
+#include "storm/exceptions/InvalidArgumentException.h"
+#include "storm/exceptions/NotImplementedException.h"
+#include "storm/exceptions/ExpressionEvaluationException.h"
+
+
+namespace storm {
+    namespace solver {
+        
+#ifdef STORM_HAVE_Z3
+        Z3LpSolver::Z3LpSolver(std::string const& name, OptimizationDirection const& optDir) : LpSolver(optDir), z3CheckResult(z3::unknown), z3Handle(0) {
+            STORM_LOG_WARN_COND(name != "", "Z3 does not support names for solvers");
+            z3::config config;
+            config.set("model", true);
+            context = std::unique_ptr<z3::context>(new z3::context(config));
+            solver = std::unique_ptr<z3::optimize>(new z3::optimize(*context));
+            expressionAdapter = std::unique_ptr<storm::adapters::Z3ExpressionAdapter>(new storm::adapters::Z3ExpressionAdapter(*this->manager, *context));
+            optimizationFunction = this->getManager().rational(storm::utility::zero<double>());
+        }
+        
+        Z3LpSolver::Z3LpSolver(std::string const& name) : Z3LpSolver(name, OptimizationDirection::Minimize) {
+            // Intentionally left empty.
+        }
+        
+        Z3LpSolver::Z3LpSolver(OptimizationDirection const& optDir) : Z3LpSolver("", optDir) {
+            // Intentionally left empty.
+        }
+        
+        Z3LpSolver::Z3LpSolver() : Z3LpSolver("", OptimizationDirection::Minimize) {
+            // Intentionally left empty.
+        }
+        
+        Z3LpSolver::~Z3LpSolver() {
+            // Intentionally left empty.
+        }
+        
+        void Z3LpSolver::update() const {
+            // Since the model changed, we erase the optimality flag and reset the current model.
+            this->z3Model.reset(nullptr);
+            this->currentModelHasBeenOptimized = false;
+        }
+        
+        storm::expressions::Variable Z3LpSolver::addBoundedContinuousVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient) {
+            storm::expressions::Variable newVariable = this->manager->declareVariable(name, 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;
+        }
+        
+        storm::expressions::Variable Z3LpSolver::addLowerBoundedContinuousVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient) {
+            storm::expressions::Variable newVariable = this->manager->declareVariable(name, manager->getRationalType());
+            solver->add(expressionAdapter->translateExpression(newVariable.getExpression() >= this->manager->rational(lowerBound)));
+            optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable;
+            return newVariable;
+        }
+
+        storm::expressions::Variable Z3LpSolver::addUpperBoundedContinuousVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient) {
+            storm::expressions::Variable newVariable = this->manager->declareVariable(name, manager->getRationalType());
+            solver->add(expressionAdapter->translateExpression(newVariable.getExpression() <= this->manager->rational(upperBound)));
+            optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable;
+            return newVariable;
+        }
+
+        storm::expressions::Variable Z3LpSolver::addUnboundedContinuousVariable(std::string const& name, double objectiveFunctionCoefficient) {
+            storm::expressions::Variable newVariable = this->manager->declareVariable(name, manager->getRationalType());
+            optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable;
+            return newVariable;
+        }
+        
+        storm::expressions::Variable Z3LpSolver::addBoundedIntegerVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient) {
+            storm::expressions::Variable newVariable = this->manager->declareVariable(name, 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;
+        }
+        
+        storm::expressions::Variable Z3LpSolver::addLowerBoundedIntegerVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient) {
+            storm::expressions::Variable newVariable = this->manager->declareVariable(name, manager->getIntegerType());
+            solver->add(expressionAdapter->translateExpression(newVariable.getExpression() >= this->manager->rational(lowerBound)));
+            optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable;
+            return newVariable;
+        }
+        
+        storm::expressions::Variable Z3LpSolver::addUpperBoundedIntegerVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient) {
+            storm::expressions::Variable newVariable = this->manager->declareVariable(name, manager->getIntegerType());
+            solver->add(expressionAdapter->translateExpression(newVariable.getExpression() <= this->manager->rational(upperBound)));
+            optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable;
+            return newVariable;
+        }
+        
+        storm::expressions::Variable Z3LpSolver::addUnboundedIntegerVariable(std::string const& name, double objectiveFunctionCoefficient) {
+            storm::expressions::Variable newVariable = this->manager->declareVariable(name, manager->getIntegerType());
+            optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable;
+            return newVariable;
+        }
+        
+        storm::expressions::Variable Z3LpSolver::addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient) {
+            storm::expressions::Variable newVariable = this->manager->declareVariable(name, manager->getBooleanType());
+            optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable;
+            return newVariable;
+        }
+
+        void Z3LpSolver::addConstraint(std::string const& name, storm::expressions::Expression const& constraint) {            
+            STORM_LOG_THROW(constraint.isRelationalExpression(), storm::exceptions::InvalidArgumentException, "Illegal constraint is not a relational expression.");
+            STORM_LOG_THROW(constraint.getOperator() != storm::expressions::OperatorType::NotEqual, storm::exceptions::InvalidArgumentException, "Illegal constraint uses inequality operator.");
+            STORM_LOG_WARN_COND(name != "", "Z3 does not support names for constraints");
+            solver->add(expressionAdapter->translateExpression(constraint));
+        }
+        
+        void Z3LpSolver::optimize() const {
+            // First incorporate all recent changes.
+            this->update();
+
+            // Invoke push() as we want to be able to erase the current optimization function after checking
+            solver->push();
+
+            // Solve the optimization problem depending on the optimization direction
+            z3Handle = this->getOptimizationDirection() == OptimizationDirection::Minimize ? solver->minimize(expressionAdapter->translateExpression(optimizationFunction)) :  solver->maximize(expressionAdapter->translateExpression(optimizationFunction));
+            z3CheckResult = solver->check();
+            STORM_LOG_THROW(z3CheckResult != z3::unknown, storm::exceptions::InvalidStateException, "Unable to solve LP problem with Z3: Check result is unknown.");
+
+            this->currentModelHasBeenOptimized = true;
+            solver->pop(); // removes current optimization function
+
+        }
+        
+        bool Z3LpSolver::isInfeasible() const {
+            STORM_LOG_THROW(this->currentModelHasBeenOptimized, storm::exceptions::InvalidStateException, "Illegal call to Z3LpSolver::isInfeasible: model has not been optimized.");
+            return z3CheckResult == z3::unsat;
+        }
+        
+        bool Z3LpSolver::isUnbounded() const {
+            STORM_LOG_THROW(this->currentModelHasBeenOptimized, storm::exceptions::InvalidStateException, "Illegal call to Z3LpSolver::isInfeasible: model has not been optimized.");
+            z3::expr expr = solver->upper(z3Handle);
+            STORM_LOG_THROW(expr.is_app(), storm::exceptions::ExpressionEvaluationException, "Failed to convert Z3 expression. Encountered unknown expression type.");
+            return expr.decl().decl_kind() != Z3_OP_ANUM;
+        }
+        
+        bool Z3LpSolver::isOptimal() const {
+            return !this->isInfeasible() && !this->isUnbounded();
+        }
+
+
+        storm::expressions::Expression Z3LpSolver::getValue(storm::expressions::Variable const& variable) const {
+            STORM_LOG_ASSERT(variable.getManager() == this->getManager(), "Requested variable is managed by a different manager.");
+            if (!this->isOptimal()) {
+                STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get Z3 solution from infeasible model.");
+                STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException, "Unable to get Z3 solution from unbounded model.");
+                STORM_LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to get Z3 solution from unoptimized model.");
+            }
+            if(!this->z3Model) {
+                z3Model = std::unique_ptr<z3::model>(new z3::model(solver->get_model()));
+            }
+            z3::expr z3Var = this->expressionAdapter->translateExpression(variable);
+			return this->expressionAdapter->translateExpression(z3Model->eval(z3Var, true));
+        }
+
+        double Z3LpSolver::getContinuousValue(storm::expressions::Variable const& variable) const {
+            return getValue(variable).evaluateAsDouble();
+        }
+        
+        int_fast64_t Z3LpSolver::getIntegerValue(storm::expressions::Variable const& variable) const {
+            return getValue(variable).evaluateAsInt();
+        }
+        
+        bool Z3LpSolver::getBinaryValue(storm::expressions::Variable const& variable) const {
+           return getValue(variable).evaluateAsBool();
+        }
+        
+        double Z3LpSolver::getObjectiveValue() const {
+            if (!this->isOptimal()) {
+                STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get Z3 solution from infeasible model.");
+                STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException, "Unable to get Z3 solution from unbounded model.");
+                STORM_LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to get Z3 solution from unoptimized model.");
+            }
+            z3::expr expr = solver->upper(z3Handle);
+            STORM_LOG_THROW(expr == solver->lower(z3Handle), storm::exceptions::InvalidAccessException, "Lower and Upper Approximation of z3LPSolver result do not match."); // TODO: make this an assertion
+            return this->expressionAdapter->translateExpression(expr).evaluateAsDouble();
+        }
+        
+        void Z3LpSolver::writeModelToFile(std::string const& filename) const {
+                STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::NotImplementedException, "Exporting LP Problems to a file is not implemented for z3.");
+        }
+
+#else 
+            Z3LpSolver::Z3LpSolver(std::string const&, OptimizationDirection const&) {
+                throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support. Please choose a version of support with Z3 support.";
+            }
+            
+            Z3LpSolver::Z3LpSolver(std::string const&) {
+                throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support. Please choose a version of support with Z3 support.";
+            }
+            
+            Z3LpSolver::Z3LpSolver(OptimizationDirection const&) {
+                throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support. Please choose a version of support with Z3 support.";
+            }
+            
+            Z3LpSolver::Z3LpSolver() {
+                throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support. Please choose a version of support with Z3 support.";
+            }
+            
+            Z3LpSolver::~Z3LpSolver() { 
+            
+            }
+            
+            storm::expressions::Variable Z3LpSolver::addBoundedContinuousVariable(std::string const&, double, double, double) {
+                throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support. Please choose a version of support with Z3 support.";
+            }
+            
+            storm::expressions::Variable Z3LpSolver::addLowerBoundedContinuousVariable(std::string const&, double, double ) {
+                throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support. Please choose a version of support with Z3 support.";            }
+            
+            storm::expressions::Variable Z3LpSolver::addUpperBoundedContinuousVariable(std::string const&, double, double ) {
+                throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support. Please choose a version of support with Z3 support.";
+            }
+            
+            storm::expressions::Variable Z3LpSolver::addUnboundedContinuousVariable(std::string const&, double ) {
+                throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support. Please choose a version of support with Z3 support.";
+            }
+            
+            storm::expressions::Variable Z3LpSolver::addBoundedIntegerVariable(std::string const&, double, double, double) {
+                throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support. Please choose a version of support with Z3 support.";
+            }
+            
+            storm::expressions::Variable Z3LpSolver::addLowerBoundedIntegerVariable(std::string const&, double, double) {
+                throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support. Please choose a version of support with Z3 support.";
+            }
+            
+            storm::expressions::Variable Z3LpSolver::addUpperBoundedIntegerVariable(std::string const&, double, double) {
+                throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support. Please choose a version of support with Z3 support.";
+            }
+            
+            storm::expressions::Variable Z3LpSolver::addUnboundedIntegerVariable(std::string const&, double) {
+                throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support. Please choose a version of support with Z3 support.";
+            }
+            
+            storm::expressions::Variable Z3LpSolver::addBinaryVariable(std::string const&, double) {
+                throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support. Please choose a version of support with Z3 support.";
+            }
+            
+            void Z3LpSolver::update() const {
+                throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support. Please choose a version of support with Z3 support.";
+            }
+            
+            void Z3LpSolver::addConstraint(std::string const&, storm::expressions::Expression const&) {
+                throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support. Please choose a version of support with Z3 support.";
+            }
+            
+            void Z3LpSolver::optimize() const {
+                throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support. Please choose a version of support with Z3 support.";
+            }
+            
+            bool Z3LpSolver::isInfeasible() const {
+                throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support. Please choose a version of support with Z3 support.";
+            }
+            
+            bool Z3LpSolver::isUnbounded() const {
+                throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support. Please choose a version of support with Z3 support.";
+            }
+            
+            bool Z3LpSolver::isOptimal() const {
+                throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support. Please choose a version of support with Z3 support.";
+            }
+            
+            double Z3LpSolver::getContinuousValue(storm::expressions::Variable const&) const {
+                throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support. Please choose a version of support with Z3 support.";
+            }
+            
+            int_fast64_t Z3LpSolver::getIntegerValue(storm::expressions::Variable const&) const {
+                throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support. Please choose a version of support with Z3 support.";
+            }
+            
+            bool Z3LpSolver::getBinaryValue(storm::expressions::Variable const&) const {
+                throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support. Please choose a version of support with Z3 support.";
+            }
+            
+            double Z3LpSolver::getObjectiveValue() const {
+                throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support. Please choose a version of support with Z3 support.";
+            }
+            
+            void Z3LpSolver::writeModelToFile(std::string const&) const {
+                throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support. Please choose a version of support with Z3 support.";
+            }
+
+            void Z3LpSolver::toggleOutput(bool) const {
+                throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support. Please choose a version of support with Z3 support.";
+            }
+
+#endif        
+    }
+}

src/storm/solver/Z3LPSolver.h

@@ -0,0 +1,134 @@
+#ifndef STORM_SOLVER_Z3LPSOLVER
+#define STORM_SOLVER_Z3LPSOLVER
+
+#include <map>
+#include "storm/solver/LpSolver.h"
+// To detect whether the usage of Z3 is possible, this include is neccessary.
+#include "storm-config.h"
+#include "storm/storage/expressions/Expressions.h"
+#include "storm/adapters/Z3ExpressionAdapter.h"
+
+
+#ifdef STORM_HAVE_Z3
+    #include "z3++.h"
+    #include "z3.h"
+#endif
+
+
+namespace storm {
+    namespace solver {
+
+        /*!
+         * A class that implements the LpSolver interface using Z3.
+         */
+        class Z3LpSolver : public LpSolver {
+        public:
+            /*!
+             * Constructs a solver with the given name and optimization direction
+             *
+             * @param name The name of the LP problem.
+             * @param optDir A value indicating whether the value of the objective function is to be minimized or
+             * maximized.
+             */
+            Z3LpSolver(std::string const& name, OptimizationDirection const& optDir);
+            
+            /*!
+             * Constructs a solver with the given name. By default the objective function is assumed to be minimized,
+             * but this may be altered later using a call to setOptimizationDirection.
+             *
+             * @param name The name of the LP problem.
+             */
+            Z3LpSolver(std::string const& name);
+            
+            /*!
+             * Constructs a solver without a name and the given optimization direction.
+             *
+             * @param optDir A value indicating whether the value of the objective function is to be minimized or
+             * maximized.
+             */
+            Z3LpSolver(OptimizationDirection const& optDir);
+            
+            /*!
+             * Constructs a solver without a name. By default the objective function is assumed to be minimized,
+             * but this may be altered later using a call to setModelSense.
+             */
+            Z3LpSolver();
+            
+            /*!
+             * Destructs a solver by freeing the pointers to Z3's structures.
+             */
+            virtual ~Z3LpSolver();
+            
+            // Methods to add continuous variables.
+            virtual storm::expressions::Variable addBoundedContinuousVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient = 0) override;
+            virtual storm::expressions::Variable addLowerBoundedContinuousVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient = 0) override;
+            virtual storm::expressions::Variable addUpperBoundedContinuousVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient = 0) override;
+            virtual storm::expressions::Variable addUnboundedContinuousVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override;
+            
+            // Methods to add integer variables.
+            virtual storm::expressions::Variable addBoundedIntegerVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient = 0) override;
+            virtual storm::expressions::Variable addLowerBoundedIntegerVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient = 0) override;
+            virtual storm::expressions::Variable addUpperBoundedIntegerVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient = 0) override;
+            virtual storm::expressions::Variable addUnboundedIntegerVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override;
+            
+            // Methods to add binary variables.
+            virtual storm::expressions::Variable addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override;
+            
+            // Methods to incorporate recent changes.
+            virtual void update() const override;
+            
+            // Methods to add constraints
+            virtual void addConstraint(std::string const& name, storm::expressions::Expression const& constraint) override;
+            
+            // Methods to optimize and retrieve optimality status.
+            virtual void optimize() const override;
+            virtual bool isInfeasible() const override;
+            virtual bool isUnbounded() const override;
+            virtual bool isOptimal() const override;
+            
+            // Methods to retrieve values of variables and the objective function in the optimal solutions.
+            virtual double getContinuousValue(storm::expressions::Variable const& name) const override;
+            virtual int_fast64_t getIntegerValue(storm::expressions::Variable const& name) const override;
+            virtual bool getBinaryValue(storm::expressions::Variable const& name) const override;
+            virtual double getObjectiveValue() const override;
+            
+            // Methods to print the LP problem to a file.
+            virtual void writeModelToFile(std::string const& filename) const override;
+
+        private:
+             virtual storm::expressions::Expression getValue(storm::expressions::Variable const& name) const;
+
+
+#ifdef STORM_HAVE_Z3
+
+            // The context used by the solver.
+            std::unique_ptr<z3::context> context;
+
+            // The actual solver object.
+            std::unique_ptr<z3::optimize> solver;
+
+            // The result of the most recent check
+            mutable z3::check_result z3CheckResult;
+
+            // The handle for the most recent optimization call
+            mutable z3::optimize::handle z3Handle;
+
+            // The model for the most recent optimization call
+            mutable std::unique_ptr<z3::model> z3Model;
+
+            // An expression adapter that is used for translating the expression into Z3's format.
+            std::unique_ptr<storm::adapters::Z3ExpressionAdapter> expressionAdapter;
+
+            // The function that is to be optimized
+            storm::expressions::Expression optimizationFunction;
+
+#endif
+
+            // The name of the solver
+            std::string name;
+        };
+
+    }
+}
+
+#endif /* STORM_SOLVER_Z3LPSOLVER */

src/test/solver/Z3LpSolverTest.cpp

@@ -0,0 +1,249 @@
+#include "gtest/gtest.h"
+#include "storm-config.h"
+
+#ifdef STORM_HAVE_Z3
+#include "storm/storage/expressions/Variable.h"
+#include "storm/solver/Z3LpSolver.h"
+#include "storm/exceptions/InvalidStateException.h"
+#include "storm/exceptions/InvalidAccessException.h"
+#include "storm/settings/SettingsManager.h"
+
+#include "storm/settings/modules/GeneralSettings.h"
+
+#include "storm/storage/expressions/Expressions.h"
+#include "storm/solver/OptimizationDirection.h"
+
+#include <cmath>
+
+TEST(Z3LpSolver, LPOptimizeMax) {
+    storm::solver::Z3LpSolver solver(storm::OptimizationDirection::Maximize);
+    storm::expressions::Variable x;
+    storm::expressions::Variable y;
+    storm::expressions::Variable z;
+    ASSERT_NO_THROW(x = solver.addBoundedContinuousVariable("x", 0, 1, -1));
+    ASSERT_NO_THROW(y = solver.addLowerBoundedContinuousVariable("y", 0, 2));
+    ASSERT_NO_THROW(z = solver.addLowerBoundedContinuousVariable("z", 0, 1));
+    ASSERT_NO_THROW(solver.update());
+    
+    ASSERT_NO_THROW(solver.addConstraint("", x + y + z <= solver.getConstant(12)));
+    ASSERT_NO_THROW(solver.addConstraint("", solver.getConstant(0.5) * y + z - x == solver.getConstant(5)));
+    ASSERT_NO_THROW(solver.addConstraint("", y - x <= solver.getConstant(5.5)));
+    ASSERT_NO_THROW(solver.update());
+    
+    ASSERT_NO_THROW(solver.optimize());
+    ASSERT_TRUE(solver.isOptimal());
+    ASSERT_FALSE(solver.isUnbounded());
+    ASSERT_FALSE(solver.isInfeasible());
+    double xValue = 0;
+    ASSERT_NO_THROW(xValue = solver.getContinuousValue(x));
+    ASSERT_LT(std::fabs(xValue - 1), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+    double yValue = 0;
+    ASSERT_NO_THROW(yValue = solver.getContinuousValue(y));
+    ASSERT_LT(std::fabs(yValue - 6.5), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+    double zValue = 0;
+    ASSERT_NO_THROW(zValue = solver.getContinuousValue(z));
+    ASSERT_LT(std::fabs(zValue - 2.75), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+    double objectiveValue = 0;
+    ASSERT_NO_THROW(objectiveValue = solver.getObjectiveValue());
+    ASSERT_LT(std::fabs(objectiveValue - 14.75), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+}
+
+TEST(Z3LpSolver, LPOptimizeMin) {
+    storm::solver::Z3LpSolver solver(storm::OptimizationDirection::Minimize);
+    storm::expressions::Variable x;
+    storm::expressions::Variable y;
+    storm::expressions::Variable z;
+    ASSERT_NO_THROW(x = solver.addBoundedContinuousVariable("x", 0, 1, -1));
+    ASSERT_NO_THROW(y = solver.addLowerBoundedContinuousVariable("y", 0, 2));
+    ASSERT_NO_THROW(z = solver.addBoundedContinuousVariable("z", 1, 5.7, -1));
+    ASSERT_NO_THROW(solver.update());
+
+    ASSERT_NO_THROW(solver.addConstraint("", x + y + z <= solver.getConstant(12)));
+    ASSERT_NO_THROW(solver.addConstraint("", solver.getConstant(0.5) * y + z - x <= solver.getConstant(5)));
+    ASSERT_NO_THROW(solver.addConstraint("", y - x <= solver.getConstant(5.5)));
+    ASSERT_NO_THROW(solver.update());
+
+    ASSERT_NO_THROW(solver.optimize());
+    ASSERT_TRUE(solver.isOptimal());
+    ASSERT_FALSE(solver.isUnbounded());
+    ASSERT_FALSE(solver.isInfeasible());
+    double xValue = 0;
+    ASSERT_NO_THROW(xValue = solver.getContinuousValue(x));
+    ASSERT_LT(std::fabs(xValue - 1), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+    double yValue = 0;
+    ASSERT_NO_THROW(yValue = solver.getContinuousValue(y));
+    ASSERT_LT(std::fabs(yValue - 0), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+    double zValue = 0;
+    ASSERT_NO_THROW(zValue = solver.getContinuousValue(z));
+    ASSERT_LT(std::fabs(zValue - 5.7), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+    double objectiveValue = 0;
+    ASSERT_NO_THROW(objectiveValue = solver.getObjectiveValue());
+    ASSERT_LT(std::fabs(objectiveValue - (-6.7)), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+}
+
+TEST(Z3LpSolver, MILPOptimizeMax) {
+    storm::solver::Z3LpSolver solver(storm::OptimizationDirection::Maximize);
+    storm::expressions::Variable x;
+    storm::expressions::Variable y;
+    storm::expressions::Variable z;
+    ASSERT_NO_THROW(x = solver.addBinaryVariable("x", -1));
+    ASSERT_NO_THROW(y = solver.addLowerBoundedIntegerVariable("y", 0, 2));
+    ASSERT_NO_THROW(z = solver.addLowerBoundedContinuousVariable("z", 0, 1));
+    ASSERT_NO_THROW(solver.update());
+
+    ASSERT_NO_THROW(solver.addConstraint("", x + y + z <= solver.getConstant(12)));
+    ASSERT_NO_THROW(solver.addConstraint("", solver.getConstant(0.5) * y + z - x == solver.getConstant(5)));
+    ASSERT_NO_THROW(solver.addConstraint("", y - x <= solver.getConstant(5.5)));
+    ASSERT_NO_THROW(solver.update());
+
+    ASSERT_NO_THROW(solver.optimize());
+    ASSERT_TRUE(solver.isOptimal());
+    ASSERT_FALSE(solver.isUnbounded());
+    ASSERT_FALSE(solver.isInfeasible());
+    bool xValue = false;
+    ASSERT_NO_THROW(xValue = solver.getBinaryValue(x));
+    ASSERT_EQ(true, xValue);
+    int_fast64_t yValue = 0;
+    ASSERT_NO_THROW(yValue = solver.getIntegerValue(y));
+    ASSERT_EQ(6, yValue);
+    double zValue = 0;
+    ASSERT_NO_THROW(zValue = solver.getContinuousValue(z));
+    ASSERT_LT(std::fabs(zValue - 3), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+    double objectiveValue = 0;
+    ASSERT_NO_THROW(objectiveValue = solver.getObjectiveValue());
+    ASSERT_LT(std::fabs(objectiveValue - 14), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+}
+
+TEST(Z3LpSolver, MILPOptimizeMin) {
+    storm::solver::Z3LpSolver solver(storm::OptimizationDirection::Minimize);
+    storm::expressions::Variable x;
+    storm::expressions::Variable y;
+    storm::expressions::Variable z;
+    ASSERT_NO_THROW(x = solver.addBinaryVariable("x", -1));
+    ASSERT_NO_THROW(y = solver.addLowerBoundedIntegerVariable("y", 0, 2));
+    ASSERT_NO_THROW(z = solver.addBoundedContinuousVariable("z", 0, 5, -1));
+    ASSERT_NO_THROW(solver.update());
+
+    ASSERT_NO_THROW(solver.addConstraint("", x + y + z <= solver.getConstant(12)));
+    ASSERT_NO_THROW(solver.addConstraint("", solver.getConstant(0.5) * y + z - x <= solver.getConstant(5)));
+    ASSERT_NO_THROW(solver.addConstraint("", y - x <= solver.getConstant(5.5)));
+    ASSERT_NO_THROW(solver.update());
+
+    ASSERT_NO_THROW(solver.optimize());
+    ASSERT_TRUE(solver.isOptimal());
+    ASSERT_FALSE(solver.isUnbounded());
+    ASSERT_FALSE(solver.isInfeasible());
+    bool xValue = false;
+    ASSERT_NO_THROW(xValue = solver.getBinaryValue(x));
+    ASSERT_EQ(true, xValue);
+    int_fast64_t yValue = 0;
+    ASSERT_NO_THROW(yValue = solver.getIntegerValue(y));
+    ASSERT_EQ(0, yValue);
+    double zValue = 0;
+    ASSERT_NO_THROW(zValue = solver.getContinuousValue(z));
+    ASSERT_LT(std::fabs(zValue - 5), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+    double objectiveValue = 0;
+    ASSERT_NO_THROW(objectiveValue = solver.getObjectiveValue());
+    ASSERT_LT(std::fabs(objectiveValue - (-6)), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+}
+
+TEST(Z3LpSolver, LPInfeasible) {
+    storm::solver::Z3LpSolver solver(storm::OptimizationDirection::Maximize);
+    storm::expressions::Variable x;
+    storm::expressions::Variable y;
+    storm::expressions::Variable z;
+    ASSERT_NO_THROW(x = solver.addBoundedContinuousVariable("x", 0, 1, -1));
+    ASSERT_NO_THROW(y = solver.addLowerBoundedContinuousVariable("y", 0, 2));
+    ASSERT_NO_THROW(z = solver.addLowerBoundedContinuousVariable("z", 0, 1));
+    ASSERT_NO_THROW(solver.update());
+
+    ASSERT_NO_THROW(solver.addConstraint("", x + y + z <= solver.getConstant(12)));
+    ASSERT_NO_THROW(solver.addConstraint("", solver.getConstant(0.5) * y + z - x == solver.getConstant(5)));
+    ASSERT_NO_THROW(solver.addConstraint("", y - x <= solver.getConstant(5.5)));
+    ASSERT_NO_THROW(solver.addConstraint("", y > solver.getConstant(7)));
+    ASSERT_NO_THROW(solver.update());
+
+    ASSERT_NO_THROW(solver.optimize());
+    ASSERT_FALSE(solver.isOptimal());
+    ASSERT_FALSE(solver.isUnbounded());
+    ASSERT_TRUE(solver.isInfeasible());
+    ASSERT_THROW(solver.getContinuousValue(x), storm::exceptions::InvalidAccessException);
+    ASSERT_THROW(solver.getContinuousValue(y), storm::exceptions::InvalidAccessException);
+    ASSERT_THROW(solver.getContinuousValue(z), storm::exceptions::InvalidAccessException);
+    ASSERT_THROW(solver.getObjectiveValue(), storm::exceptions::InvalidAccessException);
+}
+
+TEST(Z3LpSolver, MILPInfeasible) {
+    storm::solver::Z3LpSolver solver(storm::OptimizationDirection::Maximize);
+    storm::expressions::Variable x;
+    storm::expressions::Variable y;
+    storm::expressions::Variable z;
+    ASSERT_NO_THROW(x = solver.addBinaryVariable("x", -1));
+    ASSERT_NO_THROW(y = solver.addLowerBoundedContinuousVariable("y", 0, 2));
+    ASSERT_NO_THROW(z = solver.addLowerBoundedContinuousVariable("z", 0, 1));
+    ASSERT_NO_THROW(solver.update());
+
+    ASSERT_NO_THROW(solver.addConstraint("", x + y + z <= solver.getConstant(12)));
+    ASSERT_NO_THROW(solver.addConstraint("", solver.getConstant(0.5) * y + z - x == solver.getConstant(5)));
+    ASSERT_NO_THROW(solver.addConstraint("", y - x <= solver.getConstant(5.5)));
+    ASSERT_NO_THROW(solver.addConstraint("", y > solver.getConstant(7)));
+    ASSERT_NO_THROW(solver.update());
+
+    ASSERT_NO_THROW(solver.optimize());
+    ASSERT_FALSE(solver.isOptimal());
+    ASSERT_FALSE(solver.isUnbounded());
+    ASSERT_TRUE(solver.isInfeasible());
+    ASSERT_THROW(solver.getBinaryValue(x), storm::exceptions::InvalidAccessException);
+    ASSERT_THROW(solver.getIntegerValue(y), storm::exceptions::InvalidAccessException);
+    ASSERT_THROW(solver.getContinuousValue(z), storm::exceptions::InvalidAccessException);
+    ASSERT_THROW(solver.getObjectiveValue(), storm::exceptions::InvalidAccessException);
+}
+
+TEST(Z3LpSolver, LPUnbounded) {
+    storm::solver::Z3LpSolver solver(storm::OptimizationDirection::Maximize);
+    storm::expressions::Variable x;
+    storm::expressions::Variable y;
+    storm::expressions::Variable z;
+    ASSERT_NO_THROW(x = solver.addBoundedContinuousVariable("x", 0, 1, -1));
+    ASSERT_NO_THROW(y = solver.addLowerBoundedContinuousVariable("y", 0, 2));
+    ASSERT_NO_THROW(z = solver.addLowerBoundedContinuousVariable("z", 0, 1));
+    ASSERT_NO_THROW(solver.update());
+
+    ASSERT_NO_THROW(solver.addConstraint("", x + y - z <= solver.getConstant(12)));
+    ASSERT_NO_THROW(solver.addConstraint("", y - x <= solver.getConstant(5.5)));
+    ASSERT_NO_THROW(solver.update());
+
+    ASSERT_NO_THROW(solver.optimize());
+    ASSERT_FALSE(solver.isOptimal());
+    ASSERT_TRUE(solver.isUnbounded());
+    ASSERT_FALSE(solver.isInfeasible());
+    ASSERT_THROW(solver.getContinuousValue(x), storm::exceptions::InvalidAccessException);
+    ASSERT_THROW(solver.getContinuousValue(y), storm::exceptions::InvalidAccessException);
+    ASSERT_THROW(solver.getContinuousValue(z), storm::exceptions::InvalidAccessException);
+    ASSERT_THROW(solver.getObjectiveValue(), storm::exceptions::InvalidAccessException);
+}
+
+TEST(Z3LpSolver, MILPUnbounded) {
+    storm::solver::Z3LpSolver solver(storm::OptimizationDirection::Maximize);
+    storm::expressions::Variable x;
+    storm::expressions::Variable y;
+    storm::expressions::Variable z;
+    ASSERT_NO_THROW(x = solver.addBinaryVariable("x", -1));
+    ASSERT_NO_THROW(y = solver.addLowerBoundedContinuousVariable("y", 0, 2));
+    ASSERT_NO_THROW(z = solver.addLowerBoundedContinuousVariable("z", 0, 1));
+    ASSERT_NO_THROW(solver.update());
+
+    ASSERT_NO_THROW(solver.addConstraint("", x + y - z <= solver.getConstant(12)));
+    ASSERT_NO_THROW(solver.addConstraint("", y - x <= solver.getConstant(5.5)));
+    ASSERT_NO_THROW(solver.update());
+
+    ASSERT_NO_THROW(solver.optimize());
+    ASSERT_FALSE(solver.isOptimal());
+    ASSERT_TRUE(solver.isUnbounded());
+    ASSERT_FALSE(solver.isInfeasible());
+    ASSERT_THROW(solver.getBinaryValue(x), storm::exceptions::InvalidAccessException);
+    ASSERT_THROW(solver.getIntegerValue(y), storm::exceptions::InvalidAccessException);
+    ASSERT_THROW(solver.getContinuousValue(z), storm::exceptions::InvalidAccessException);
+    ASSERT_THROW(solver.getObjectiveValue(), storm::exceptions::InvalidAccessException);
+}
+#endif