diff --git a/src/adapters/HyproAdapter.h b/src/adapters/HyproAdapter.h index d63553583..33ca968eb 100644 --- a/src/adapters/HyproAdapter.h +++ b/src/adapters/HyproAdapter.h @@ -6,9 +6,10 @@ #ifdef STORM_HAVE_HYPRO -#include -//#include -#include +#include +#include +#include +#include #include "src/adapters/CarlAdapter.h" #include "src/storage/geometry/HalfSpace.h" @@ -33,12 +34,14 @@ namespace storm { template hypro::Halfspace toHypro(storm::storage::geometry::Halfspace const& h){ - return hypro::Halfspace(toHypro(h.normalVector()), h.offset()); + T offset = h.offset(); + return hypro::Halfspace(toHypro(h.normalVector()), std::move(offset)); } template - hypro::Halfspace fromHypro(hypro::Halfspace const& h){ - return storm::storage::geometry::Halfspace(fromHypro(h.normal()), h.offset()); + storm::storage::geometry::Halfspace fromHypro(hypro::Halfspace const& h){ + T offset = h.offset(); + return storm::storage::geometry::Halfspace(fromHypro(h.normal()), std::move(offset)); } } diff --git a/src/storage/geometry/Halfspace.h b/src/storage/geometry/Halfspace.h index 4317df726..7ebd599cc 100644 --- a/src/storage/geometry/Halfspace.h +++ b/src/storage/geometry/Halfspace.h @@ -2,6 +2,8 @@ #define STORM_STORAGE_GEOMETRY_HALFSPACE_H_ #include +#include +#include "src/utility/constants.h" #include "src/utility/vector.h" namespace storm { @@ -25,18 +27,29 @@ namespace storm { //Intentionally left empty } + /* + * Returns true iff the given point is contained in this halfspace, i.e., normalVector*point <= offset holds. + */ bool contains(std::vector const& point) { - return storm::utility::vector::multiplyVectors(point, normalVector()) <= offset(); + return storm::utility::vector::dotProduct(point, normalVector()) <= offset(); } - std::string toString() { + /* + * Returns a string representation of this Halfspace. + * If the given flag is true, the occurring numbers are converted to double before printing to increase readability + */ + std::string toString(bool numbersAsDouble = false) const { std::stringstream stream; stream << "("; for(auto it = normalVector().begin(); it != normalVector().end(); ++it){ if(it != normalVector().begin()){ stream << ", "; } - stream << *it; + if(numbersAsDouble) { + stream << std::setw(10) << storm::utility::convertNumber(*it); + } else { + stream << std::setw(10) << *it; + } } stream << ") * x <= " << offset(); return stream.str(); diff --git a/src/storage/geometry/Hyperrectangle.h b/src/storage/geometry/Hyperrectangle.h new file mode 100644 index 000000000..2afdf242e --- /dev/null +++ b/src/storage/geometry/Hyperrectangle.h @@ -0,0 +1,77 @@ +#ifndef STORM_STORAGE_GEOMETRY_HYPERRECTANGLE_H_ +#define STORM_STORAGE_GEOMETRY_HYPERRECTANGLE_H_ + +#include +#include + +#include "src/utility/macros.h" +#include "src/storage/geometry/Polytope.h" +#include "src/storage/geometry/Halfspace.h" +#include "src/exceptions/InvalidArgumentException" + +namespace storm { + namespace storage { + namespace geometry { + + /* + * This class represents a hyperrectangle, i.e., the intersection of finitely many intervals + */ + + template + class Hyperrectangle { + + public: + + Hyperrectangle(std::vector const& lowerBounds, std::vector const& upperBounds) : mLowerBounds(lowerBounds), mUpperBounds(upperBounds) { + STORM_LOG_THROW(lowerBounds.size() == upperBounds.size(), storm::exceptions::InvalidArgumentException, "Tried to construct a hyperrectangle but the number of given lower bounds does not equal the number of given upper bounds."); + } + + Hyperrectangle(std::vector&& lowerBounds, std::vector&& upperBounds) : mLowerBounds(lowerBounds), mUpperBounds(upperBounds) { + STORM_LOG_THROW(lowerBounds.size() == upperBounds.size(), storm::exceptions::InvalidArgumentException, "Tried to construct a hyperrectangle but the number of given lower bounds does not equal the number of given upper bounds."); + } + + std::vector const& lowerBounds() const { + return mLowerBounds; + } + + std::vector& lowerBounds(){ + return mLowerBounds; + } + + std::vector const& upperBounds() const { + return mUpperBounds; + } + + std::vector& upperBounds(){ + return mUpperBounds; + } + + std::shared_ptr> asPolytope() const { + STORM_LOG_THROW(lowerBounds.size() == upperBounds.size(), storm::exceptions::InvalidArgumentException, "Tried to construct a polytope form a hyperrectangle but the numbers of given lower and upper bounds do not match."); + std::vector> halfspaces; + halfspaces.reserve(2*lowerBounds.size()); + for(uint_fast64_t i = 0; i direction(lowerBounds.size(), storm::utility::zero()); + direction[i] = -storm::utility::one(); + ValueType offset = -lowerBounds()[i]; + halfspaces.emplace_back(std::move(direction), std::move(offset)); + + direction = std::vector(lowerBounds.size(), storm::utility::zero()); + direction[i] = storm::utility::one(); + offset = upperBounds()[i]; + halfspaces.emplace_back(std::move(direction), std::move(offset)); + } + return Polytope::create(halfspaces); + } + + private: + + std::vector mLowerBounds; + std::vector mUpperBounds; + + }; + } + } +} + +#endif /* STORM_STORAGE_GEOMETRY_HYPERRECTANGLE_H_ */ diff --git a/src/storage/geometry/HyproPolytope.cpp b/src/storage/geometry/HyproPolytope.cpp new file mode 100644 index 000000000..b5959c8e3 --- /dev/null +++ b/src/storage/geometry/HyproPolytope.cpp @@ -0,0 +1,195 @@ +#include "src/storage/geometry/HyproPolytope.h" + +#include "src/utility/macros.h" +#include "src/exceptions/InvalidArgumentException.h" +#include "src/exceptions/UnexpectedException.h" + +namespace storm { + namespace storage { + namespace geometry { + + template + HyproPolytope::HyproPolytope(std::vector> const& halfspaces) { + if(halfspaces.empty()){ + internPolytope = HyproPolytopeType(); + } else { + std::vector> hyproHalfspaces; + hyproHalfspaces.reserve(halfspaces.size()); + for(auto& h : halfspaces) { + hyproHalfspaces.emplace_back(storm::adapters::toHypro(h)); + } + internPolytope = HyproPolytopeType(std::move(hyproHalfspaces)); + } + } + + template + HyproPolytope::HyproPolytope(std::vector const& points) { + if(points.empty()){ + internPolytope = HyproPolytopeType::Empty(); + } else { + std::vector> hyproPoints; + hyproPoints.reserve(points.size()); + for(auto const& p : points){ + hyproPoints.emplace_back(storm::adapters::toHypro(p)); + } + internPolytope = HyproPolytopeType(std::move(hyproPoints)); + } + } + + template + std::shared_ptr> HyproPolytope::create(boost::optional>> const& halfspaces, + boost::optional> const& points) { + if(halfspaces) { + STORM_LOG_WARN_COND(!points, "Creating a HyproPolytope where halfspaces AND points are given. The points will be ignored."); + return std::make_shared>(*halfspaces); + } else if(points) { + return std::make_shared>(*points); + } + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Creating a HyproPolytope but no representation was given."); + return nullptr; + } + + template + HyproPolytope::HyproPolytope(HyproPolytope const& other) : internPolytope(other.internPolytope) { + // Intentionally left empty + } + + template + HyproPolytope::HyproPolytope(HyproPolytope&& other) : internPolytope(std::move(other.internPolytope)) { + // Intentionally left empty + } + + template + HyproPolytope::HyproPolytope(HyproPolytopeType const& p) : internPolytope(p) { + // Intentionally left empty + } + + template + HyproPolytope::HyproPolytope(HyproPolytopeType&& p) : internPolytope(p) { + // Intentionally left empty + } + + template + HyproPolytope::~HyproPolytope() { + // Intentionally left empty + } + + template + std::vector::Point> HyproPolytope::getVertices() const { + std::vector> hyproVertices = internPolytope.vertices(); + std::vector result; + result.reserve(hyproVertices.size()); + for(auto const& p : hyproVertices) { + result.push_back(storm::adapters::fromHypro(p.rawCoordinates())); + } + return result; + } + + template + std::vector> HyproPolytope::getHalfspaces() const { + std::vector> hyproHalfspaces = internPolytope.constraints(); + std::vector> result; + result.reserve(hyproHalfspaces.size()); + for(auto const& h : hyproHalfspaces) { + result.push_back(storm::adapters::fromHypro(h)); + } + return result; + } + + template + bool HyproPolytope::isEmpty() const { + return internPolytope.empty(); + } + + template + bool HyproPolytope::isUniversal() const { + return internPolytope.constraints().empty(); + } + + template + bool HyproPolytope::contains(Point const& point) const{ + return internPolytope.contains(storm::adapters::toHypro(point)); + } + + template + bool HyproPolytope::contains(std::shared_ptr> const& other) const { + STORM_LOG_THROW(other->isHyproPolytope(), storm::exceptions::InvalidArgumentException, "Invoked operation between a HyproPolytope and a different polytope implementation. This is not supported"); + return internPolytope.contains(other->asHyproPolytope().internPolytope); + } + + template + std::shared_ptr> HyproPolytope::intersection(std::shared_ptr> const& rhs) const{ + STORM_LOG_THROW(rhs->isHyproPolytope(), storm::exceptions::InvalidArgumentException, "Invoked operation between a HyproPolytope and a different polytope implementation. This is not supported"); + return std::make_shared>(internPolytope.intersect(rhs->asHyproPolytope().internPolytope)); + } + + template + std::shared_ptr> HyproPolytope::intersection(Halfspace const& halfspace) const{ + HyproPolytopeType result(internPolytope); + result.insert(storm::adapters::toHypro(halfspace)); + return std::make_shared>(std::move(result)); + } + + template + std::shared_ptr> HyproPolytope::convexUnion(std::shared_ptr> const& rhs) const{ + STORM_LOG_THROW(rhs->isHyproPolytope(), storm::exceptions::InvalidArgumentException, "Invoked operation between a HyproPolytope and a different polytope implementation. This is not supported"); + return std::make_shared>(internPolytope.unite(rhs->asHyproPolytope().internPolytope)); + } + + template + std::shared_ptr> HyproPolytope::minkowskiSum(std::shared_ptr> const& rhs) const{ + STORM_LOG_THROW(rhs->isHyproPolytope(), storm::exceptions::InvalidArgumentException, "Invoked operation between a HyproPolytope and a different polytope implementation. This is not supported"); + return std::make_shared>(internPolytope.minkowskiSum(rhs->asHyproPolytope().internPolytope)); + } + + template + std::shared_ptr> HyproPolytope::downwardClosure(boost::optional const& upperBounds) const { + if(this->isUniversal() || this->isEmpty()) { + // In these cases, the polytope does not change, i.e., we return a copy of this + return std::make_shared>(internPolytope); + } + // Only keep the halfspaces where all entries of the normal vector are non-negative + std::vector> halfspaces; + for(auto& h : internPolytope.constraints()){ + if((h.normal().array() >= storm::utility::zero()).all()){ + halfspaces.push_back(h); + } + } + // Add Halfspaces to bound the polytope in each (positive) direction + for(uint_fast64_t dim = 0; dim < internPolytope.dimension(); ++dim){ + hypro::vector_t direction = hypro::vector_t::Zero(dim); + direction(dim) = storm::utility::one(); + if(upperBounds){ + ValueType upperBound = (*upperBounds)[dim]; + halfspaces.emplace_back(std::move(direction), std::move(upperBound)); + } else { + // Compute max{x_dim | x \in P } + hypro::EvaluationResult evalRes = internPolytope.evaluate(direction); + switch (evalRes.errorCode) { + case hypro::SOLUTION::FEAS: + halfspaces.emplace_back(std::move(direction), std::move(evalRes.supportValue)); + break; + case hypro::SOLUTION::INFTY: + // if this polytope is not bounded in the current direction, no halfspace needs to be added + break; + default: + // there should never be an infeasible solution as we already excluded the empty polytope. + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unexpected eror code for Polytope evaluation"); + break; + } + } + } + return std::make_shared>(HyproPolytopeType(std::move(halfspaces))); + } + + template + bool HyproPolytope::isHyproPolytope() const { + return true; + } + +#ifdef STORM_HAVE_CARL + template class HyproPolytope; +#endif + } + } +} diff --git a/src/storage/geometry/HyproPolytope.h b/src/storage/geometry/HyproPolytope.h new file mode 100644 index 000000000..c17dfd775 --- /dev/null +++ b/src/storage/geometry/HyproPolytope.h @@ -0,0 +1,124 @@ +#ifndef STORM_STORAGE_GEOMETRY_HYPROPOLYTOPE_H_ +#define STORM_STORAGE_GEOMETRY_HYPROPOLYTOPE_H_ + +#include "src/storage/geometry/Polytope.h" +#include "src/adapters/HyproAdapter.h" + +#ifdef STORM_HAVE_HYPRO + +namespace storm { + namespace storage { + namespace geometry { + + template + class HyproPolytope : public Polytope { + public: + + typedef typename Polytope::Point Point; + typedef hypro::HPolytope HyproPolytopeType; + + /*! + * Creates a HyproPolytope from the given halfspaces or points. + * If both representations are given, one of them might be ignored + */ + static std::shared_ptr> create(boost::optional>> const& halfspaces, + boost::optional> const& points); + + /*! + * Creates a HyproPolytope from the given halfspaces + * The resulting polytope is defined as the intersection of the halfspaces. + */ + HyproPolytope(std::vector> const& halfspaces); + + /*! + * Creates a HyproPolytope from the given points. + * The resulting polytope is defined as the convex hull of the points' + */ + HyproPolytope(std::vector const& points); + + /*! + * Copy and move constructors + */ + HyproPolytope(HyproPolytope const& other); + HyproPolytope(HyproPolytope&& other); + + /*! + * Construction from a plain hypro polytope + */ + HyproPolytope(HyproPolytopeType const& polytope); + HyproPolytope(HyproPolytopeType&& polytope); + + ~HyproPolytope(); + + /*! + * Returns the vertices of this polytope. + */ + virtual std::vector getVertices() const override; + + /*! + * Returns the halfspaces of this polytope. + */ + virtual std::vector> getHalfspaces() const override; + + + /*! + * Returns whether this polytope is the empty set. + */ + virtual bool isEmpty() const override; + + /*! + * Returns whether this polytope is universal (i.e., equals R^n). + */ + virtual bool isUniversal() const override; + + /*! + * Returns true iff the given point is inside of the polytope. + */ + virtual bool contains(Point const& point) const override; + + /*! + * Returns true iff the given polytope is a subset of this polytope. + */ + virtual bool contains(std::shared_ptr> const& other) const override; + + /*! + * Intersects this polytope with rhs and returns the result. + */ + virtual std::shared_ptr> intersection(std::shared_ptr> const& rhs) const override; + virtual std::shared_ptr> intersection(Halfspace const& halfspace) const override; + + /*! + * Returns the convex union of this polytope and rhs. + */ + virtual std::shared_ptr> convexUnion(std::shared_ptr> const& rhs) const override; + + /*! + * Returns the minkowskiSum of this polytope and rhs. + */ + virtual std::shared_ptr> minkowskiSum(std::shared_ptr> const& rhs) const override; + + /*! + * Returns the downward closure of this, i.e., the set { x | ex. y \in P : x<=y} where P is this Polytope. + * Put differently, the resulting polytope corresponds to this polytope, where + * 1. a vector y with y_i=max{x_i | x \in P} is computed and for each i, a halfspace with offset y_i and + * normal vector n (where n_i = 1 and the remaining entries are 0) is inserted. + * 2. all halfspaces where the normal vector has at least one negative entry are removed + * + * @param upperBounds If given, this vector is considered for y (hence, max{x_i | x i \in P does not need to be computed) + */ + virtual std::shared_ptr> downwardClosure(boost::optional const& upperBounds = boost::none) const override; + + virtual bool isHyproPolytope() const override; + + private: + + HyproPolytopeType internPolytope; + }; + + } + } +} + +#endif /* STORM_HAVE_HYPRO */ + +#endif /* STORM_STORAGE_GEOMETRY_HYPROPOLYTOPE_H_ */ diff --git a/src/storage/geometry/Polytope.cpp b/src/storage/geometry/Polytope.cpp index aaac1507d..1e6718a34 100644 --- a/src/storage/geometry/Polytope.cpp +++ b/src/storage/geometry/Polytope.cpp @@ -1,7 +1,10 @@ #include "src/storage/geometry/Polytope.h" -#include "src/utility/macros.h" +#include + #include "src/adapters/HyproAdapter.h" +#include "src/storage/geometry/HyproPolytope.h" +#include "src/utility/macros.h" #include "src/exceptions/NotImplementedException.h" namespace storm { @@ -9,83 +12,128 @@ namespace storm { namespace geometry { template - std::shared_ptr> Polytope::create(std::vector> const& halfspaces){ - return create(halfspaces, boost::none, false); + std::shared_ptr> Polytope::create(std::vector> const& halfspaces) { + return create(halfspaces, boost::none); } template - std::shared_ptr> Polytope::create(std::vector const& points){ - return create(boost::none, points, false); + std::shared_ptr> Polytope::create(std::vector const& points) { + return create(boost::none, points); } template - std::shared_ptr> Polytope::createDownwardClosure(std::vector> const& halfspaces){ - return create(halfspaces, boost::none, false); + std::shared_ptr> Polytope::create(boost::optional>> const& halfspaces, + boost::optional> const& points) { +#ifdef STORM_HAVE_HYPRO + return HyproPolytope::create(halfspaces, points); +#endif + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "No polytope implementation specified."); + return nullptr; } + //Protected default constructor template - std::shared_ptr> Polytope::createDownwardClosure(std::vector const& points){ - return create(boost::none, points, true); + Polytope::Polytope() { + // Intentionally left empty } template - std::shared_ptr> Polytope::create(boost::optional>> const& halfspaces, - boost::optional> const& points, - bool downwardClosure) { - -#ifdef STORM_HAVE_HYPRO - std::cout << "HyPro available!!" << std::endl; - // return std::make_shared(HyproPolytope(halfspaces, points, downwardClosure)); -#endif - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "No polytope implementation specified."); - return nullptr; + Polytope::~Polytope() { + // Intentionally left empty } template - std::vector::Point> Polytope::getVertices(){ + std::vector::Point> Polytope::getVertices() const{ STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Functionality not implemented."); + return std::vector(); } template - std::vector> Polytope::getHalfspaces(){ + std::vector> Polytope::getHalfspaces() const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Functionality not implemented."); + return std::vector>(); } template - bool Polytope::contains(Point const& point) const{ + bool Polytope::isEmpty() const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Functionality not implemented."); + return false; } template - std::shared_ptr> Polytope::intersect(std::shared_ptr> const& rhs) const{ + bool Polytope::isUniversal() const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Functionality not implemented."); + return false; } + template - std::shared_ptr> Polytope::intersect(Halfspace const& rhs) const{ + bool Polytope::contains(Point const& point) const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Functionality not implemented."); + return false; } template - std::shared_ptr> Polytope::convexUnion(std::shared_ptr> const& rhs) const{ + bool Polytope::contains(std::shared_ptr> const& other) const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Functionality not implemented."); + return false; } + template - std::shared_ptr> Polytope::convexUnion(Point const& rhs) const{ + std::shared_ptr> Polytope::intersection(std::shared_ptr> const& rhs) const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Functionality not implemented."); + return nullptr; } template - std::shared_ptr> Polytope::bloat(Point const& point1, Point const& point2) const{ + std::shared_ptr> Polytope::intersection(Halfspace const& halfspace) const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Functionality not implemented."); + return nullptr; } + template + std::shared_ptr> Polytope::convexUnion(std::shared_ptr> const& rhs) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Functionality not implemented."); + return nullptr; + } + + template + std::shared_ptr> Polytope::minkowskiSum(std::shared_ptr> const& rhs) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Functionality not implemented."); + return nullptr; + } template - std::string Polytope::toString() const{ + std::shared_ptr> Polytope::downwardClosure(boost::optional const& upperBounds) const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Functionality not implemented."); + return nullptr; + } + + template + std::string Polytope::toString(bool numbersAsDouble) const { + auto halfspaces = this->getHalfspaces(); + std::stringstream stream; + stream << "Polytope with " << halfspaces.size() << " Halfspaces" << (halfspaces.empty() ? "" : ":") << std::endl; + for (auto const& h : halfspaces) { + stream << "| " << h.toString(numbersAsDouble) << std::endl; + } + return stream.str(); + } + + template + bool Polytope::isHyproPolytope() const { + return false; + } + + template + HyproPolytope const& Polytope::asHyproPolytope() const { + return dynamic_cast const&>(*this); + } + + template + HyproPolytope& Polytope::asHyproPolytope() { + return dynamic_cast&>(*this); } - template class Polytope; #ifdef STORM_HAVE_CARL template class Polytope; #endif diff --git a/src/storage/geometry/Polytope.h b/src/storage/geometry/Polytope.h index 6e082dd0f..6fc84151c 100644 --- a/src/storage/geometry/Polytope.h +++ b/src/storage/geometry/Polytope.h @@ -11,17 +11,21 @@ namespace storm { namespace storage { namespace geometry { + // Forward declaration + template + class HyproPolytope; + template class Polytope { public: typedef std::vector Point; - - Polytope() = delete; //Use create methods to assemble a polytope + + ~Polytope(); /*! * Creates a polytope from the given halfspaces. - * If the given vector of halfspaces is empty, the resulting polytope is universal (i.e., equals |R^n). + * If the given vector of halfspaces is empty, the resulting polytope is universal (i.e., equals R^n). */ static std::shared_ptr> create(std::vector> const& halfspaces); @@ -32,71 +36,85 @@ namespace storm { static std::shared_ptr> create(std::vector const& points); /*! - * Creates a polytope P from the given halfspaces - * and returns the downward closure of P, i.e., the set { x | ex. y \in P: x<=y} - * If the vector of halfspaces is empty, the resulting polytope will be universal. + * Returns the vertices of this polytope. */ - static std::shared_ptr> createDownwardClosure(std::vector> const& halfspaces); + virtual std::vector getVertices() const; /*! - * Creates a polytope P from the given points (i.e., the convex hull of the points) - * and returns the downward closure of P, i.e., the set { x | ex. y \in P: x<=y} - * If the vector of points is empty, the resulting polytope be empty. + * Returns the halfspaces of this polytope. */ - static std::shared_ptr> createDownwardClosure(std::vector const& points); - + virtual std::vector> getHalfspaces() const; + /*! - * Returns the vertices of this polytope. + * Returns whether this polytope is the empty set. */ - virtual std::vector getVertices(); + virtual bool isEmpty() const; /*! - * Returns the halfspaces of this polytope. + * Returns whether this polytope is universal (i.e., equals R^n). */ - virtual std::vector> getHalfspaces(); + virtual bool isUniversal() const; /*! * Returns true iff the given point is inside of the polytope. */ virtual bool contains(Point const& point) const; + /*! + * Returns true iff the given polytope is a subset of this polytope. + */ + virtual bool contains(std::shared_ptr> const& other) const; + /*! * Intersects this polytope with rhs and returns the result. */ - virtual std::shared_ptr> intersect(std::shared_ptr> const& rhs) const; - virtual std::shared_ptr> intersect(Halfspace const& rhs) const; + virtual std::shared_ptr> intersection(std::shared_ptr> const& rhs) const; + virtual std::shared_ptr> intersection(Halfspace const& halfspace) const; /*! * Returns the convex union of this polytope and rhs. */ virtual std::shared_ptr> convexUnion(std::shared_ptr> const& rhs) const; - virtual std::shared_ptr> convexUnion(Point const& rhs) const; + + /*! + * Returns the minkowskiSum of this polytope and rhs. + */ + virtual std::shared_ptr> minkowskiSum(std::shared_ptr> const& rhs) const; /*! - * Bloats the polytope - * The resulting polytope is (possibly an overapproximation of) the minkowski sum of this polytope and the - * hyperrectangle given by point1 and point2. + * Returns the downward closure of this, i.e., the set { x | ex. y \in P : x<=y} where P is this Polytope. + * Put differently, the resulting polytope corresponds to this polytope, where + * 1. a vector y with y_i=max{x_i | x \in P} is computed and for each i, a halfspace with offset y_i and + * normal vector n (where n_i = 1 and the remaining entries are 0) is inserted. + * 2. all halfspaces where the normal vector has at least one negative entry are removed + * + * @param upperBounds If given, this vector is considered for y (hence, max{x_i | x i \in P does not need to be computed) */ - virtual std::shared_ptr> bloat(Point const& point1, Point const& point2) const; - + virtual std::shared_ptr> downwardClosure(boost::optional const& upperBounds = boost::none) const; /* * Returns a string representation of this polytope. + * If the given flag is true, the occurring numbers are converted to double before printing to increase readability */ - virtual std::string toString() const; + virtual std::string toString(bool numbersAsDouble = false) const; + + virtual bool isHyproPolytope() const; + + HyproPolytope& asHyproPolytope(); + HyproPolytope const& asHyproPolytope() const; + + protected: + + Polytope(); + private: /*! * Creates a polytope from the given halfspaces or vertices. - * if the given flag is true, the downward closure will be created. */ static std::shared_ptr> create(boost::optional>> const& halfspaces, - boost::optional> const& points, - bool downwardClosure); + boost::optional> const& points); - Polytope(boost::optional>> const& halfspaces, - boost::optional> const& points, - bool downwardClosure); };