diff --git a/src/storage/geometry/HyproPolytope.cpp b/src/storage/geometry/HyproPolytope.cpp index d085e7d09..0def7ae64 100644 --- a/src/storage/geometry/HyproPolytope.cpp +++ b/src/storage/geometry/HyproPolytope.cpp @@ -1,4 +1,6 @@ #include "src/storage/geometry/HyproPolytope.h" +# +#ifdef STORM_HAVE_HYPRO #include "src/utility/macros.h" #include "src/exceptions/InvalidArgumentException.h" @@ -114,13 +116,13 @@ namespace storm { 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); + return internPolytope.contains(dynamic_cast const&>(*other).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)); + return std::make_shared>(internPolytope.intersect(dynamic_cast const&>(*rhs).internPolytope)); } template @@ -133,13 +135,13 @@ namespace storm { 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)); + return std::make_shared>(internPolytope.unite(dynamic_cast const&>(*rhs).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)); + return std::make_shared>(internPolytope.minkowskiSum(dynamic_cast const&>(*rhs).internPolytope)); } template @@ -190,6 +192,8 @@ namespace storm { #ifdef STORM_HAVE_CARL template class HyproPolytope; #endif + // Note that hypro's polytopes only support exact arithmetic } } } +#endif diff --git a/src/storage/geometry/Polytope.cpp b/src/storage/geometry/Polytope.cpp index 1e6718a34..791eb6d86 100644 --- a/src/storage/geometry/Polytope.cpp +++ b/src/storage/geometry/Polytope.cpp @@ -2,6 +2,7 @@ #include +#include "src/adapters/CarlAdapter.h" #include "src/adapters/HyproAdapter.h" #include "src/storage/geometry/HyproPolytope.h" #include "src/utility/macros.h" @@ -21,17 +22,26 @@ namespace storm { return create(boost::none, points); } - template - std::shared_ptr> Polytope::create(boost::optional>> const& halfspaces, +#ifdef STORM_HAVE_CARL + template <> + std::shared_ptr> Polytope::create(boost::optional>> const& halfspaces, boost::optional> const& points) { #ifdef STORM_HAVE_HYPRO - return HyproPolytope::create(halfspaces, points); + return HyproPolytope::create(halfspaces, points); #endif STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "No polytope implementation specified."); return nullptr; } +#endif + + template + std::shared_ptr> Polytope::create(boost::optional>> const& halfspaces, + boost::optional> const& points) { + //Note: hypro polytopes (currently) do not work with non-exact arithmetic (e.g., double) + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "No polytope implementation specified."); + return nullptr; + } - //Protected default constructor template Polytope::Polytope() { // Intentionally left empty @@ -124,19 +134,11 @@ namespace storm { return false; } - template - HyproPolytope const& Polytope::asHyproPolytope() const { - return dynamic_cast const&>(*this); - } - - template - HyproPolytope& Polytope::asHyproPolytope() { - return dynamic_cast&>(*this); - } - #ifdef STORM_HAVE_CARL template class Polytope; #endif + template class Polytope; + // Note that HyproPolytopes only support exact arithmetic } } } diff --git a/src/storage/geometry/Polytope.h b/src/storage/geometry/Polytope.h index 6fc84151c..be113c934 100644 --- a/src/storage/geometry/Polytope.h +++ b/src/storage/geometry/Polytope.h @@ -11,10 +11,6 @@ namespace storm { namespace storage { namespace geometry { - // Forward declaration - template - class HyproPolytope; - template class Polytope { public: @@ -101,9 +97,6 @@ namespace storm { virtual bool isHyproPolytope() const; - HyproPolytope& asHyproPolytope(); - HyproPolytope const& asHyproPolytope() const; - protected: Polytope(); diff --git a/src/utility/constants.cpp b/src/utility/constants.cpp index c3184c194..a47e8f02e 100644 --- a/src/utility/constants.cpp +++ b/src/utility/constants.cpp @@ -131,16 +131,6 @@ namespace storm { value.simplify(); return std::move(value); } - - template<> - double convertNumber(RationalNumber const& number){ - return carl::toDouble(number); - } - - template<> - RationalNumber convertNumber(double const& number){ - return carl::rationalize(number); - } #endif @@ -255,9 +245,6 @@ namespace storm { template RationalNumber one(); template RationalNumber zero(); - template double convertNumber(RationalNumber const& number); - template RationalNumber convertNumber(double const& number); - template bool isOne(Interval const& value); template bool isZero(Interval const& value); template bool isConstant(Interval const& value); diff --git a/src/utility/constants.h b/src/utility/constants.h index 80222b74f..4c6d75768 100644 --- a/src/utility/constants.h +++ b/src/utility/constants.h @@ -12,6 +12,8 @@ #include #include +#include "src/adapters/CarlAdapter.h" + namespace storm { // Forward-declare MatrixEntry class. @@ -52,8 +54,14 @@ namespace storm { storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); template - TargetType convertNumber(SourceType const& number); + TargetType convertNumber(SourceType const& number) { +#ifdef STORM_HAVE_CARL + return carl::convert(number); +#else + return static_cast(number); +#endif + } } } -#endif /* STORM_UTILITY_CONSTANTS_H_ */ \ No newline at end of file +#endif /* STORM_UTILITY_CONSTANTS_H_ */