diff --git a/doc/api/Doxyfile.in b/doc/api/Doxyfile.in index 26b09d2c1..c4c4ed42f 100644 --- a/doc/api/Doxyfile.in +++ b/doc/api/Doxyfile.in @@ -2502,7 +2502,7 @@ HIDE_UNDOC_RELATIONS = YES # set to NO # The default value is: NO. -HAVE_DOT = YES +HAVE_DOT = NO # The DOT_NUM_THREADS specifies the number of dot invocations doxygen is allowed # to run in parallel. When set to 0 doxygen will base this on the number of diff --git a/doc/manual/manual/intervals/Interval_class.rst b/doc/manual/manual/intervals/Interval_class.rst index 48b24989a..39f49a7d7 100644 --- a/doc/manual/manual/intervals/Interval_class.rst +++ b/doc/manual/manual/intervals/Interval_class.rst @@ -243,6 +243,20 @@ All standard arithmetic operations are supported in Codac, both element-wise and z = x / y % [1, 3] +Interval comparisons +-------------------- + +The comparison operators ``<`` and ``>`` are also overloaded for intervals. +They return a :ref:`BoolInterval value ` rather than a classical Boolean, in order to encode the set of feasible truth values when the exact operands are only known within interval bounds. + +For instance, ``x < y`` returns: + +- ``BoolInterval.EMPTY`` if one of the two intervals is empty; +- ``BoolInterval.TRUE`` if :math:`\forall a\in[x],\forall b\in[y],\ a& pysep); void export_SepInter(py::module& m, py::class_& sep); void export_SepInverse(py::module& m, py::class_& sep); void export_SepNot(py::module& m, py::class_& sep); +void export_SepPolarCart(py::module& m, py::class_& pysep); void export_SepPolygon(py::module& m, py::class_& sep); void export_SepProj(py::module& m, py::class_& sep); void export_SepQInter(py::module& m, py::class_& sep); @@ -331,6 +332,7 @@ PYBIND11_MODULE(_core, m) export_SepInter(m,py_sep); export_SepInverse(m,py_sep); export_SepNot(m,py_sep); + export_SepPolarCart(m,py_sep); export_SepPolygon(m,py_sep); export_SepProj(m,py_sep); export_SepQInter(m,py_sep); diff --git a/python/src/core/domains/interval/codac2_py_Interval.cpp b/python/src/core/domains/interval/codac2_py_Interval.cpp index 145e9ad4c..2e92ca484 100644 --- a/python/src/core/domains/interval/codac2_py_Interval.cpp +++ b/python/src/core/domains/interval/codac2_py_Interval.cpp @@ -76,6 +76,14 @@ py::class_ export_Interval(py::module& m) BOOL_INTERVAL_OPERATORNEQ_CONST_INTERVAL_REF_CONST, "x"_a) + .def(py::self < py::self, + BOOLINTERVAL_INTERVAL_OPERATOR__CONST_INTERVAL_REF_CONST, + "x"_a) + + .def(py::self > py::self, + BOOLINTERVAL_INTERVAL_OPERATOR_CONST_INTERVAL_REF_CONST, + "x"_a) + .def("lb", &Interval::lb, DOUBLE_INTERVAL_LB_CONST) diff --git a/python/src/core/separators/codac2_py_SepPolarCart.cpp b/python/src/core/separators/codac2_py_SepPolarCart.cpp new file mode 100644 index 000000000..3ad0fd89d --- /dev/null +++ b/python/src/core/separators/codac2_py_SepPolarCart.cpp @@ -0,0 +1,39 @@ +/** + * Codac binding (core) + * ---------------------------------------------------------------------------- + * \date 2026 + * \author Simon Rohou + * \copyright Copyright 2026 Codac Team + * \license GNU Lesser General Public License (LGPL) + */ + +#include +#include +#include +#include +#include +#include "codac2_py_Sep.h" +#include "codac2_py_SepPolarCart_docs.h" // Generated file from Doxygen XML (doxygen2docstring.py): + +using namespace std; +using namespace codac2; +namespace py = pybind11; +using namespace pybind11::literals; + +void export_SepPolarCart(py::module& m, py::class_& pysep) +{ + py::class_ exported(m, "SepPolarCart", pysep, SEPPOLARCART_MAIN); + exported + + .def(py::init([](const SepBase& s1) { + return std::make_unique(s1.copy()); + }), + SEPPOLARCART_SEPPOLARCART_CONST_S_REF, + "s1"_a) + + .def("separate", &SepPolarCart::separate, + BOXPAIR_SEPPOLARCART_SEPARATE_CONST_INTERVALVECTOR_REF_CONST, + "x"_a) + + ; +} \ No newline at end of file diff --git a/src/core/CMakeLists.txt b/src/core/CMakeLists.txt index d06db4fd8..db02e9526 100644 --- a/src/core/CMakeLists.txt +++ b/src/core/CMakeLists.txt @@ -241,6 +241,8 @@ ${CMAKE_CURRENT_SOURCE_DIR}/separators/codac2_SepInter.h ${CMAKE_CURRENT_SOURCE_DIR}/separators/codac2_SepInverse.h ${CMAKE_CURRENT_SOURCE_DIR}/separators/codac2_SepNot.h + ${CMAKE_CURRENT_SOURCE_DIR}/separators/codac2_SepPolarCart.cpp + ${CMAKE_CURRENT_SOURCE_DIR}/separators/codac2_SepPolarCart.h ${CMAKE_CURRENT_SOURCE_DIR}/separators/codac2_SepPolygon.cpp ${CMAKE_CURRENT_SOURCE_DIR}/separators/codac2_SepPolygon.h ${CMAKE_CURRENT_SOURCE_DIR}/separators/codac2_SepProj.cpp diff --git a/src/core/domains/interval/codac2_Interval.h b/src/core/domains/interval/codac2_Interval.h index 34e082421..09dca1ac5 100644 --- a/src/core/domains/interval/codac2_Interval.h +++ b/src/core/domains/interval/codac2_Interval.h @@ -21,6 +21,7 @@ #include "codac2_Domain.h" #include "codac2_assert.h" #include "codac2_TypeInfo.h" +#include "codac2_BoolInterval.h" namespace codac2 { @@ -160,6 +161,40 @@ namespace codac2 */ bool operator!=(const Interval& x) const; + /** + * \brief Comparison (strict less-than) between this and x + * + * The returned ``BoolInterval`` encloses the truth value of + * \f$ts\f$ for \f$t\in[\mathrm{this}]\f$ and \f$s\in[x]\f$. + * + * \note Returns: + * - ``BoolInterval::EMPTY`` if this or x is empty + * - ``BoolInterval::TRUE`` iff \f$\mathrm{lb}([\mathrm{this}])>\mathrm{ub}([x])\f$ + * - ``BoolInterval::FALSE`` iff \f$\mathrm{lb}([x])\geq\mathrm{ub}([\mathrm{this}])\f$ + * - ``BoolInterval::UNKNOWN`` otherwise + * + * \param x interval to be compared with + * \return interval Boolean result + */ + BoolInterval operator>(const Interval& x) const; + /** * \brief Returns the lower bound of this * diff --git a/src/core/domains/interval/codac2_Interval_impl.h b/src/core/domains/interval/codac2_Interval_impl.h index bcdcef9b8..8e2bd0cfc 100644 --- a/src/core/domains/interval/codac2_Interval_impl.h +++ b/src/core/domains/interval/codac2_Interval_impl.h @@ -107,6 +107,22 @@ namespace codac2 return !(*this == x); } + inline BoolInterval Interval::operator<(const Interval& x) const + { + if(is_empty() || x.is_empty()) + return BoolInterval::EMPTY; + if(this->ub() < x.lb()) + return BoolInterval::TRUE; + if(x.ub() <= this->lb()) + return BoolInterval::FALSE; + return BoolInterval::UNKNOWN; + } + + inline BoolInterval Interval::operator>(const Interval& x) const + { + return x < *this; + } + inline double Interval::lb() const { return gaol::interval::left(); diff --git a/src/core/separators/codac2_SepPolarCart.cpp b/src/core/separators/codac2_SepPolarCart.cpp index dbb726d12..ac011ccc3 100644 --- a/src/core/separators/codac2_SepPolarCart.cpp +++ b/src/core/separators/codac2_SepPolarCart.cpp @@ -1,74 +1,115 @@ /** - * codac2_SepPolarCart.cpp + * \file codac2_SepPolarCart.cpp * ---------------------------------------------------------------------------- * \date 2026 - * \author Benoît Desrochers, (Simon Rohou) + * \author Simon Rohou, from a former implementation of Benoît Desrochers * \copyright Copyright 2026 Codac Team * \license GNU Lesser General Public License (LGPL) */ #include "codac2_SepPolarCart.h" #include "codac2_CtcPolar.h" +#include "codac2_cart_prod.h" +#include "codac2_hull.h" using namespace codac2; -BoxPair SepPolarCart::separate(const IntervalVector& x) const +/** + * Contracts x with the Cartesian projection of the complement of a polar box. + * + * For a polar box [rho]x[theta], the complement is represented as the union + * of four polar boxes: + * - rho <= rho.lb(), with theta in [theta] + * - rho >= rho.ub(), with theta in [theta] + * - theta before theta.lb(), with rho in R+ + * - theta after theta.ub(), with rho in R+ + * + * The angular complement is computed in the 2*pi-wide window centered on [theta]. + */ +IntervalVector contract_polar_box_complement( + const CtcPolar& ctc_polar, + const IntervalVector& x, + const IntervalVector& x_pol) { assert_release(x.size() == 2); + assert_release(x_pol.size() == 2); - CtcPolar ctc_polar; - IntervalVector x_cart(2), x_pol(x); + if(x.is_empty()) + return x; - ctc_polar.contract(x_cart[0], x_cart[1], x_pol[0], x_pol[1]); - auto x_cart_sep = _sep.front()->separate(x_cart); - BoxPair x_polar_sep { x, x }; - ctc_polar.contract(x_cart_sep.inner[0], x_cart_sep.inner[1], x_polar_sep.inner[0], x_polar_sep.inner[1]); - ctc_polar.contract(x_cart_sep.outer[0], x_cart_sep.outer[1], x_polar_sep.outer[0], x_polar_sep.outer[1]); + // Complement of the empty polar box: no point is removed by the inner + // contractor, so the Cartesian box is left unchanged. + if(x_pol.is_empty()) + return x; - return x_polar_sep; -} + const Interval& rho = x_pol[0]; + const Interval& theta = x_pol[1]; + std::list parts; -SepPolarXY::SepPolarXY(Interval rho, Interval theta) : rho(rho), theta(theta), Sep(2) { - rho_m = Interval(0, rho.lb()); - rho_p = Interval(rho.ub(), POS_INFINITY); - double limit = theta.mid() - M_PI; - theta_m = Interval(limit, theta.lb()); - theta_p = Interval(theta.ub(), limit + 2*M_PI); - cmpl = Interval(0, 2*M_PI); -} + auto add_polar_part = [&ctc_polar,&parts](const IntervalVector& x, + const Interval& rho, + const Interval& theta) + { + if(rho.is_empty() || theta.is_empty()) + return; + Interval rho_(rho), theta_(theta); + IntervalVector x_(x); + ctc_polar.contract(x_[0],x_[1],rho_,theta_); + parts.push_back(x_); + }; -void SepPolarXY::contractOut(IntervalVector &x_out){ - Interval th = this->theta; - Interval r = this->rho; - this->ctc.contract(x_out[0], x_out[1], r, th); - if(x_out[0].is_empty() || x_out[1].is_empty()) - x_out.set_empty(); -} + // Radial complement, restricted to the current angular sector. The angular + // outside parts below cover the remaining angles. + if(std::isfinite(rho.lb()) && rho.lb() >= 0) + add_polar_part(x, {0,rho.lb()}, theta); + + if(std::isfinite(rho.ub())) + add_polar_part(x, {rho.ub(),oo}, theta); + // Angular complement. If [theta] already covers at least one full turn, + // there is no angular complement in the 2*pi-periodic sense. + if(std::isfinite(theta.lb()) && std::isfinite(theta.ub()) + && theta.ub() - theta.lb() < 2*PI) + { + double limit = theta.mid()-PI; + add_polar_part(x, {0,oo}, {limit,theta.lb()}); + add_polar_part(x, {0,oo}, {theta.ub(),limit+2*PI}); + } -void SepPolarXY::contractIn(IntervalVector &x_in){ - Interval x1(x_in[0]); Interval y1(x_in[1]); - Interval x2(x_in[0]); Interval y2(x_in[1]); - Interval x3(x_in[0]); Interval y3(x_in[1]); - Interval x4(x_in[0]); Interval y4(x_in[1]); - - Interval ALLREALS1 = Interval::POS_REALS; - Interval ALLREALS2 = Interval::POS_REALS; - Interval cmpl1(cmpl); - Interval cmpl2(cmpl); - Interval theta_m_tmp(theta_m); - Interval theta_p_tmp(theta_p); - Interval rho_m_tmp(rho_m); - Interval rho_p_tmp(rho_p); - - this->ctc.contract(x1, y1, ALLREALS1, theta_m_tmp); - this->ctc.contract(x2, y2, ALLREALS2, theta_p_tmp); - this->ctc.contract(x3, y3, rho_m_tmp, cmpl1); - this->ctc.contract(x4, y4, rho_p_tmp, cmpl2); - x_in[0] &= (x1 | x2 | x3 | x4); - x_in[1] &= (y1 | y2 | y3 | y4); - if(x_in[0].is_empty() || x_in[1].is_empty()) - x_in.set_empty(); + return x & hull(parts); } + +BoxPair SepPolarCart::separate(const IntervalVector& x) const +{ + assert_release(x.size() == 2); + + BoxPair x_cart_sep { x, x }; + + if(x.is_empty()) + return x_cart_sep; + + CtcPolar ctc_polar; + IntervalVector x_cart(x), x_pol(2); + + // Cartesian input -> polar enclosure + ctc_polar.contract(x_cart[0], x_cart[1], x_pol[0], x_pol[1]); + + if(x_cart.is_empty() || x_pol.is_empty()) + return x_cart_sep; + + // Separation in the polar space + const BoxPair x_pol_sep = _sep.front()->separate(x_pol); + + // Outer contraction: keep the Cartesian points whose polar coordinates may + // belong to the polar separator output + IntervalVector copy_x_pol_sep = x_pol_sep.outer.subvector(0,1); + ctc_polar.contract(x_cart_sep.outer[0], x_cart_sep.outer[1], copy_x_pol_sep[0], copy_x_pol_sep[1]); + + // Inner contraction: remove points belonging to the polar set by contracting + // with the complement of the polar outer box + x_cart_sep.inner = contract_polar_box_complement(ctc_polar, x_cart_sep.inner, x_pol_sep.outer); + + return x_cart_sep; +} \ No newline at end of file diff --git a/src/core/separators/codac2_SepPolarCart.h b/src/core/separators/codac2_SepPolarCart.h index 27651702f..e4f6b6e9f 100644 --- a/src/core/separators/codac2_SepPolarCart.h +++ b/src/core/separators/codac2_SepPolarCart.h @@ -2,7 +2,7 @@ * \file codac2_SepPolarCart.h * ---------------------------------------------------------------------------- * \date 2026 - * \author Benoît Desrochers, (Simon Rohou) + * \author Benoît Desrochers, Simon Rohou * \copyright Copyright 2026 Codac Team * \license GNU Lesser General Public License (LGPL) */ @@ -14,7 +14,15 @@ namespace codac2 { - // For separating a Cartesian box from a Sep expressed in polar coordinates + /** + * \class SepPolarCart + * \brief For separating a Cartesian box from a separator expressed in polar + * coordinates \f$(\rho,\theta)\f$. + * + * This separator is the inverse counterpart of SepCartPolar: the wrapped + * separator acts on polar boxes, while this class exposes a separator on + * Cartesian boxes \f$(x,y)\f$. + */ class SepPolarCart : public Sep { public: @@ -33,4 +41,4 @@ namespace codac2 const Collection _sep; }; -} \ No newline at end of file +} diff --git a/tests/core/domains/interval/codac2_tests_Interval.cpp b/tests/core/domains/interval/codac2_tests_Interval.cpp index 7dfe8ba2c..e98d6ca55 100644 --- a/tests/core/domains/interval/codac2_tests_Interval.cpp +++ b/tests/core/domains/interval/codac2_tests_Interval.cpp @@ -281,6 +281,27 @@ TEST_CASE("Interval - other tests") CHECK(Approx(a.second,1e-7) == Interval(2,10)); } +TEST_CASE("Interval - comparison") +{ + CHECK((Interval(0,1) < Interval(2,3)) == BoolInterval::TRUE); + CHECK((Interval(0,1) < Interval(1,2)) == BoolInterval::UNKNOWN); + CHECK((Interval(0,1) < Interval(0,1)) == BoolInterval::UNKNOWN); + CHECK((Interval(2,3) < Interval(0,1)) == BoolInterval::FALSE); + CHECK((Interval(2,3) < Interval(-oo,2)) == BoolInterval::FALSE); + CHECK((Interval(-oo,2) < Interval(3,oo)) == BoolInterval::TRUE); + CHECK((Interval::empty() < Interval(0,1)) == BoolInterval::EMPTY); + CHECK((Interval(0,1) < Interval::empty()) == BoolInterval::EMPTY); + + CHECK((Interval(2,3) > Interval(0,1)) == BoolInterval::TRUE); + CHECK((Interval(1,2) > Interval(0,1)) == BoolInterval::UNKNOWN); + CHECK((Interval(0,1) > Interval(0,1)) == BoolInterval::UNKNOWN); + CHECK((Interval(0,1) > Interval(2,3)) == BoolInterval::FALSE); + CHECK((Interval(-oo,2) > Interval(2,3)) == BoolInterval::FALSE); + CHECK((Interval(3,oo) > Interval(-oo,2)) == BoolInterval::TRUE); + CHECK((Interval::empty() > Interval(0,1)) == BoolInterval::EMPTY); + CHECK((Interval(0,1) > Interval::empty()) == BoolInterval::EMPTY); +} + #if 0 // Tests from the IBEX lib that are not considered in this file: diff --git a/tests/core/domains/interval/codac2_tests_Interval.py b/tests/core/domains/interval/codac2_tests_Interval.py index 858a88932..9a505e469 100644 --- a/tests/core/domains/interval/codac2_tests_Interval.py +++ b/tests/core/domains/interval/codac2_tests_Interval.py @@ -249,6 +249,26 @@ def test_interval(self): b = Interval(1,3) & Interval(6,7) # [b] is empty c = a+b self.assertTrue(c.is_empty()) + + # Comparisons + + self.assertTrue((Interval(0,1) < Interval(2,3)) == BoolInterval.TRUE) + self.assertTrue((Interval(0,1) < Interval(1,2)) == BoolInterval.UNKNOWN) + self.assertTrue((Interval(0,1) < Interval(0,1)) == BoolInterval.UNKNOWN) + self.assertTrue((Interval(2,3) < Interval(0,1)) == BoolInterval.FALSE) + self.assertTrue((Interval(2,3) < Interval(-oo,2)) == BoolInterval.FALSE) + self.assertTrue((Interval(-oo,2) < Interval(3,oo)) == BoolInterval.TRUE) + self.assertTrue((Interval.empty() < Interval(0,1)) == BoolInterval.EMPTY) + self.assertTrue((Interval(0,1) < Interval.empty()) == BoolInterval.EMPTY) + + self.assertTrue((Interval(2,3) > Interval(0,1)) == BoolInterval.TRUE) + self.assertTrue((Interval(1,2) > Interval(0,1)) == BoolInterval.UNKNOWN) + self.assertTrue((Interval(0,1) > Interval(0,1)) == BoolInterval.UNKNOWN) + self.assertTrue((Interval(0,1) > Interval(2,3)) == BoolInterval.FALSE) + self.assertTrue((Interval(-oo,2) > Interval(2,3)) == BoolInterval.FALSE) + self.assertTrue((Interval(3,oo) > Interval(-oo,2)) == BoolInterval.TRUE) + self.assertTrue((Interval.empty() > Interval(0,1)) == BoolInterval.EMPTY) + self.assertTrue((Interval(0,1) > Interval.empty()) == BoolInterval.EMPTY) if __name__ == '__main__': unittest.main() \ No newline at end of file