diff --git a/src/storm/storage/geometry/Polytope.cpp b/src/storm/storage/geometry/Polytope.cpp index a89b7247e..e7befab70 100644 --- a/src/storm/storage/geometry/Polytope.cpp +++ b/src/storm/storage/geometry/Polytope.cpp @@ -47,35 +47,47 @@ namespace storm { template std::shared_ptr> Polytope::createDownwardClosure(std::vector 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 + std::shared_ptr> Polytope::createSelectiveDownwardClosure(std::vector 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> 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 auxiliaryPoints = points; - auxiliaryPoints.reserve(auxiliaryPoints.size()*(1+dimensions)); - for(auto const& point : points) { - for(uint_fast64_t dim=0; dim(); } } std::vector> 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()); + // 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()); } - if(allGreaterZero){ + if (allGreaterEqZero){ halfspaces.push_back(std::move(h)); } } diff --git a/src/storm/storage/geometry/Polytope.h b/src/storm/storage/geometry/Polytope.h index d467af99d..06b6f26ae 100644 --- a/src/storm/storage/geometry/Polytope.h +++ b/src/storm/storage/geometry/Polytope.h @@ -6,6 +6,7 @@ #include #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> createDownwardClosure(std::vector 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> createSelectiveDownwardClosure(std::vector const& points, storm::storage::BitVector const& selectedDimensions); + /*! * Returns the vertices of this polytope. */