From a73574a99f50ccefdc011e58661e31478072e484 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Wed, 27 Jun 2018 15:37:10 +0200
Subject: [PATCH] added functionality to translate a polytope to an expression

---
 src/storm/storage/geometry/NativePolytope.h | 21 +++++++++++++--------
 src/storm/storage/geometry/Polytope.cpp     | 15 +++++++++++++++
 src/storm/storage/geometry/Polytope.h       | 13 +++++++++++++
 3 files changed, 41 insertions(+), 8 deletions(-)

diff --git a/src/storm/storage/geometry/NativePolytope.h b/src/storm/storage/geometry/NativePolytope.h
index 11931a7d8..e5ef64d8d 100644
--- a/src/storm/storage/geometry/NativePolytope.h
+++ b/src/storm/storage/geometry/NativePolytope.h
@@ -2,7 +2,6 @@
 #define STORM_STORAGE_GEOMETRY_NATIVEPOLYTOPE_H_
 
 #include "storm/storage/geometry/Polytope.h"
-#include "storm/storage/expressions/Expressions.h"
 #include "storm/adapters/EigenAdapter.h"
 
 namespace storm {
@@ -125,8 +124,20 @@ namespace storm {
                  */
                 virtual std::pair<Point, bool> optimize(Point const& direction) const override;
 
-                virtual bool isNativePolytope() const override;
+                /*!
+                 * declares one variable for each dimension and returns the obtained variables.
+                 * @param manager The expression manager that keeps track of the variables
+                 * @param namePrefix The prefix that is prepanded to the variable index
+                 */
+                virtual std::vector<storm::expressions::Variable> declareVariables(storm::expressions::ExpressionManager& manager, std::string const& namePrefix) const override;
+
+                /*!
+                 * returns the constrains defined by this polytope as an expression over the given variables
+                 */
+                virtual std::vector<storm::expressions::Expression> getConstraints(storm::expressions::ExpressionManager const& manager, std::vector<storm::expressions::Variable> const& variables) const override;
                 
+
+                virtual bool isNativePolytope() const override;
             private:
 
                 // returns the vertices of this polytope as EigenVectors
@@ -136,12 +147,6 @@ namespace storm {
                 std::pair<EigenVector, bool> optimize(EigenVector const& direction) const;
 
 
-                // declares one variable for each constraint and returns the obtained variables.
-                std::vector<storm::expressions::Variable> declareVariables(storm::expressions::ExpressionManager& manager, std::string const& namePrefix) const;
-
-                // returns the constrains defined by this polytope as an expresseion
-                std::vector<storm::expressions::Expression> getConstraints(storm::expressions::ExpressionManager const& manager, std::vector<storm::expressions::Variable> const& variables) const;
-
 
                 //Stores whether the polytope is empty or not
                 mutable EmptyStatus emptyStatus;
diff --git a/src/storm/storage/geometry/Polytope.cpp b/src/storm/storage/geometry/Polytope.cpp
index 756abbfd0..83af2b3f7 100644
--- a/src/storm/storage/geometry/Polytope.cpp
+++ b/src/storm/storage/geometry/Polytope.cpp
@@ -182,6 +182,21 @@ namespace storm {
                 return createDownwardClosure(this->getVertices());
             }
             
+            template <typename ValueType>
+            std::vector<storm::expressions::Variable> Polytope<ValueType>::declareVariables(storm::expressions::ExpressionManager& manager, std::string const& namePrefix) const {
+                STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Functionality not implemented for this polytope implementation.");
+                std::vector<storm::expressions::Variable> result;
+                return result;
+            }
+
+            template <typename ValueType>
+            std::vector<storm::expressions::Expression> Polytope<ValueType>::getConstraints(storm::expressions::ExpressionManager const& manager, std::vector<storm::expressions::Variable> const& variables) const {
+                STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Functionality not implemented for this polytope implementation.");
+                std::vector<storm::expressions::Expression> result;
+                return result;
+            }
+
+            
             template <typename ValueType>
             template <typename TargetType>
             std::shared_ptr<Polytope<TargetType>> Polytope<ValueType>::convertNumberRepresentation() const {
diff --git a/src/storm/storage/geometry/Polytope.h b/src/storm/storage/geometry/Polytope.h
index 5d7ff858a..5c0822486 100644
--- a/src/storm/storage/geometry/Polytope.h
+++ b/src/storm/storage/geometry/Polytope.h
@@ -7,6 +7,7 @@
 
 #include "storm/storage/geometry/Halfspace.h"
 #include "storm/storage/BitVector.h"
+#include "storm/storage/expressions/Expressions.h"
 
 namespace storm {
     namespace storage {
@@ -137,6 +138,18 @@ namespace storm {
                  */
                 virtual std::pair<Point, bool> optimize(Point const& direction) const = 0;
                 
+                /*!
+                 * Declares one variable for each dimension and returns the obtained variables.
+                 * @param manager The expression manager that keeps track of the variables
+                 * @param namePrefix The prefix that is prepanded to the variable index
+                 */
+                virtual std::vector<storm::expressions::Variable> declareVariables(storm::expressions::ExpressionManager& manager, std::string const& namePrefix) const;
+
+                /*!
+                 * Returns the constrains defined by this polytope as an expression over the given variables
+                 */
+                virtual std::vector<storm::expressions::Expression> getConstraints(storm::expressions::ExpressionManager const& manager, std::vector<storm::expressions::Variable> const& variables) const;
+                
                 /*!
                  * converts the intern number representation of the polytope to the given target type
                  */