added possibility to compute the 'downward closure' of a polytope only with respect to a set of dimensions

src/storm/storage/geometry/Polytope.cpp

@@ -47,35 +47,47 @@ namespace storm {
             
             template <typename ValueType>
             std::shared_ptr<Polytope<ValueType>> Polytope<ValueType>::createDownwardClosure(std::vector<Point> const& points) {
-                if(points.empty()) {
+                if (points.empty()) {
                     // In this case, the downwardclosure is empty
                     return createEmptyPolytope();
                 }
-                uint_fast64_t const dimensions = points.front().size();
+                // Reduce this call to a more general method
+                storm::storage::BitVector dimensions(points.front().size(), true);
+                return createSelectiveDownwardClosure(points, dimensions);
+            }
+            
+            template <typename ValueType>
+            std::shared_ptr<Polytope<ValueType>> Polytope<ValueType>::createSelectiveDownwardClosure(std::vector<Point> const& points, storm::storage::BitVector const& selectedDimensions) {
+                if (points.empty()) {
+                    // In this case, the downwardclosure is empty
+                    return createEmptyPolytope();
+                }
+                if (selectedDimensions.empty()) {
+                    return create(points);
+                }
+                assert(points.front().size() == selectedDimensions.size());
+                uint64_t dimensions = selectedDimensions.size();
+                
                 std::vector<Halfspace<ValueType>> halfspaces;
                 // We build the convex hull of the given points.
-                // However, auxiliary points (that will always be in the downward closure) are added.
+                // However, auxiliary points (that will always be in the selective downward closure) are added.
                 // Then, the halfspaces of the resulting polytope are a superset of the halfspaces of the downward closure.
                 std::vector<Point> auxiliaryPoints = points;
-                auxiliaryPoints.reserve(auxiliaryPoints.size()*(1+dimensions));
-                for(auto const& point : points) {
-                    for(uint_fast64_t dim=0; dim<dimensions; ++dim) {
+                auxiliaryPoints.reserve(auxiliaryPoints.size() * (1 + selectedDimensions.getNumberOfSetBits()));
+                for (auto const& point : points) {
+                    for (auto const& dim : selectedDimensions) {
                         auxiliaryPoints.push_back(point);
                         auxiliaryPoints.back()[dim] -= storm::utility::one<ValueType>();
                     }
                 }
                 std::vector<Halfspace<ValueType>> auxiliaryHalfspaces = create(auxiliaryPoints)->getHalfspaces();
-                // The downward closure is obtained by selecting the halfspaces for which the normal vector is non-negative (coordinate wise).
-                // Note that due to the auxiliary points, the polytope is never degenerated and thus there is always one unique halfspace-representation which is necessary:
-                // Consider, e.g., the convex hull of two points (1,0,0) and (0,1,1).
-                // There are multiple halfspace-representations for this set. In particular, there is one where all but one normalVectors have negative entries.
-                // However, the downward closure of this set can only be represented with 5 halfspaces.
-                for(auto& h : auxiliaryHalfspaces){
-                    bool allGreaterZero = true;
-                    for(auto const& value : h.normalVector()) {
-                        allGreaterZero &= (value >= storm::utility::zero<ValueType>());
-                    }
-                    if(allGreaterZero){
+                // The downward closure is obtained by erasing the halfspaces for which the normal vector is negative for one of the selected dimensions.
+                for (auto& h : auxiliaryHalfspaces) {
+                    bool allGreaterEqZero = true;
+                    for (auto const& dim : selectedDimensions) {
+                        allGreaterEqZero &= (h.normalVector()[dim] >= storm::utility::zero<ValueType>());
+                    }
+                    if (allGreaterEqZero){
                         halfspaces.push_back(std::move(h));
                     }
                 }

src/storm/storage/geometry/Polytope.h

@@ -6,6 +6,7 @@
 #include <boost/optional.hpp>
 
 #include "storm/storage/geometry/Halfspace.h"
+#include "storm/storage/BitVector.h"
 
 namespace storm {
     namespace storage {
@@ -43,10 +44,17 @@ namespace storm {
                 
                 /*!
                  * Creates the downward closure of the given points (i.e., the set { x | ex. y \in conv(points) : x<=y }
-                 * If the vector of points is empty, the resulting polytope be empty.
+                 * If the vector of points is empty, the resulting polytope is empty.
                  */
                 static std::shared_ptr<Polytope<ValueType>> createDownwardClosure(std::vector<Point> const& points);
                 
+                /*!
+                 * Creates the downward closure of the given points but only with respect to the selected dimensions,
+                 * (i.e., the set { x | ex. y \in conv(points) : (x_i<=y_i if i in selectedDim) and (x_i==y_i if i not in selectedDim }
+                 * If the vector of points is empty, the resulting polytope is empty.
+                 */
+                static std::shared_ptr<Polytope<ValueType>> createSelectiveDownwardClosure(std::vector<Point> const& points, storm::storage::BitVector const& selectedDimensions);
+                
                 /*!
                  * Returns the vertices of this polytope.
                  */