[doc] updated CtcInverse manual page for contraction on boxes

doc/manual/manual/contractors/analytic/ctcinverse.rst

@@ -92,7 +92,9 @@ To represent the vectors :math:`\mathbf{x}\in\mathbb{R}^n` consistent with the c
       :end-before: [ctcinv-1-end]
       :dedent: 0
 
-The contractor can be used as an operator to contract a 2d box :math:`[\mathbf{x}]`. It can also be involved in a paver in order to reveal the constraint:
+The contractor can be used as an operator to contract a :math:`n`-d box :math:`[\mathbf{x}]`.
+
+Note that the contraction may be fast but not minimal, depending on your analytic expression. Therefore, you can also combine a ``CtcInverse`` with a ``CtcFixpoint`` to apply the contraction procedure repeatedly until a fixpoint is reached on the same box. The following code corresponds to a contraction revealed in the next figure, which shows contraction cases in blue and their fixpoint counterparts in red.
 
 .. tabs::
 
@@ -120,14 +122,10 @@ The contractor can be used as an operator to contract a 2d box :math:`[\mathbf{x
       :end-before: [ctcinv-2-end]
       :dedent: 0
 
-Which produces the following output:
-
-.. figure:: ./himmelblau_50.png
+.. figure:: ./himmelblau_boxes.png
   :width: 400px
 
-  Outer approximation of the solution set for :math:`f(\mathbf{x})\in[50,50]`. This paving result reveals three connected subsets approximated with outer boxes. Blue parts are guaranteed not to contain solutions.
-
-We recall that for thick solution sets, one should prefer the use of the ``SepInverse`` separator in order to get both outer and inner approximations. For instance, the solution set associated with :math:`f(\mathbf{x})\leqslant 50` corresponds to:
+As any other contractor, a ``CtcInverse`` can also be involved in a paver in order to reveal the constraint set:
 
 .. tabs::
 
@@ -155,6 +153,41 @@ We recall that for thick solution sets, one should prefer the use of the ``SepIn
       :end-before: [ctcinv-3-end]
       :dedent: 0
 
+Which produces the following output:
+
+.. figure:: ./himmelblau_50.png
+  :width: 400px
+
+  Outer approximation of the solution set for :math:`f(\mathbf{x})\in[50,50]`. This paving result reveals three connected subsets approximated with outer boxes. Blue parts are guaranteed not to contain solutions.
+
+We recall that for thick solution sets, one should prefer the use of the ``SepInverse`` separator in order to get both outer and inner approximations. For instance, the solution set associated with :math:`f(\mathbf{x})\leqslant 50` corresponds to:
+
+.. tabs::
+
+  .. group-tab:: Python
+
+    .. literalinclude:: src.py
+      :language: py
+      :start-after: [ctcinv-4-beg]
+      :end-before: [ctcinv-4-end]
+      :dedent: 4
+
+  .. group-tab:: C++
+
+    .. literalinclude:: src.cpp
+      :language: c++
+      :start-after: [ctcinv-4-beg]
+      :end-before: [ctcinv-4-end]
+      :dedent: 4
+
+  .. group-tab:: Matlab
+
+    .. literalinclude:: src.m
+      :language: matlab
+      :start-after: [ctcinv-4-beg]
+      :end-before: [ctcinv-4-end]
+      :dedent: 0
+
 
 .. figure:: ./himmelblau_50_inner.png
   :width: 400px
@@ -176,24 +209,24 @@ can be easily approximated by the following union of contractors:
 
     .. literalinclude:: src.py
       :language: py
-      :start-after: [ctcinv-4-beg]
-      :end-before: [ctcinv-4-end]
+      :start-after: [ctcinv-5-beg]
+      :end-before: [ctcinv-5-end]
       :dedent: 4
 
   .. group-tab:: C++
 
     .. literalinclude:: src.cpp
       :language: c++
-      :start-after: [ctcinv-4-beg]
-      :end-before: [ctcinv-4-end]
+      :start-after: [ctcinv-5-beg]
+      :end-before: [ctcinv-5-end]
       :dedent: 4
 
   .. group-tab:: Matlab
 
     .. literalinclude:: src.m
       :language: matlab
-      :start-after: [ctcinv-4-beg]
-      :end-before: [ctcinv-4-end]
+      :start-after: [ctcinv-5-beg]
+      :end-before: [ctcinv-5-end]
       :dedent: 0
 
 .. figure:: ./himmelblau_50_150_250.png
@@ -323,24 +356,24 @@ When the constraint is a complement constraint :math:`\mathbf{f}(\mathbf{x})\not
 
     .. literalinclude:: src.py
       :language: py
-      :start-after: [ctcinv-5-beg]
-      :end-before: [ctcinv-5-end]
+      :start-after: [ctcinv-6-beg]
+      :end-before: [ctcinv-6-end]
       :dedent: 4
 
   .. group-tab:: C++
 
     .. literalinclude:: src.cpp
       :language: c++
-      :start-after: [ctcinv-5-beg]
-      :end-before: [ctcinv-5-end]
+      :start-after: [ctcinv-6-beg]
+      :end-before: [ctcinv-6-end]
       :dedent: 4
 
   .. group-tab:: Matlab
 
     .. literalinclude:: src.m
       :language: matlab
-      :start-after: [ctcinv-5-beg]
-      :end-before: [ctcinv-5-end]
+      :start-after: [ctcinv-6-beg]
+      :end-before: [ctcinv-6-end]
       :dedent: 0
 
 
@@ -358,24 +391,24 @@ The underlying analytic function can be accessed through ``.fnc()`` (useful for
 
     .. literalinclude:: src.py
       :language: py
-      :start-after: [ctcinv-6-beg]
-      :end-before: [ctcinv-6-end]
+      :start-after: [ctcinv-7-beg]
+      :end-before: [ctcinv-7-end]
       :dedent: 4
 
   .. group-tab:: C++
 
     .. literalinclude:: src.cpp
       :language: c++
-      :start-after: [ctcinv-6-beg]
-      :end-before: [ctcinv-6-end]
+      :start-after: [ctcinv-7-beg]
+      :end-before: [ctcinv-7-end]
       :dedent: 4
 
   .. group-tab:: Matlab
 
     .. literalinclude:: src.m
       :language: matlab
-      :start-after: [ctcinv-6-beg]
-      :end-before: [ctcinv-6-end]
+      :start-after: [ctcinv-7-beg]
+      :end-before: [ctcinv-7-end]
       :dedent: 0
 
 Centered form option

doc/manual/manual/contractors/analytic/src.cpp

@@ -9,6 +9,7 @@
 
 #include <catch2/catch_test_macros.hpp>
 #include <codac2_CtcInverse.h>
+#include <codac2_CtcFixpoint.h>
 #include <codac2_SepInverse.h>
 #include <codac2_CtcInverseNotIn.h>
 #include <codac2_Approx.h>
@@ -29,22 +30,36 @@ TEST_CASE("CtcInverse - manual")
     // [ctcinv-1-end]
 
     // [ctcinv-2-beg]
-    DefaultFigure::pave({{-6,6},{-6,6}}, c, 1e-2);
+    IntervalVector z({{0,3.5},{0,1}});
+    DefaultFigure::draw_box(z, {Color::blue(),Color::blue(.1)}); // prior to contraction
+    c.contract(z);
+    DefaultFigure::draw_box(z, {Color::blue(),Color::white()}); // after one CtcInverse contraction
+    // z == [ [1.84, 3.5] ; [0, 1] ]
+
+    // Combining CtcInverse with a CtcFixpoint:
+    CtcFixpoint cfix(c);
+    c.contract(z);
+    DefaultFigure::draw_box(z, Color::red()); // after a fixed point contraction
+    // z == [ [1.84, 2.483] ; [0, 1] ]
     // [ctcinv-2-end]
 
     // [ctcinv-3-beg]
-    SepInverse s(f, {0,50});
-    DefaultFigure::pave({{-6,6},{-6,6}}, s, 1e-2);
+    DefaultFigure::pave({{-6,6},{-6,6}}, c, 1e-2);
     // [ctcinv-3-end]
 
     // [ctcinv-4-beg]
+    SepInverse s(f, {0,50});
+    DefaultFigure::pave({{-6,6},{-6,6}}, s, 1e-2);
+    // [ctcinv-4-end]
+
+    // [ctcinv-5-beg]
     auto cu = CtcInverse(f,50) | CtcInverse(f,150) | CtcInverse(f,250);
     DefaultFigure::pave({{-6,6},{-6,6}}, cu, 1e-2);
-    // [ctcinv-4-end]
+    // [ctcinv-5-end]
   }
 
   {
-    // [ctcinv-5-beg]
+    // [ctcinv-6-beg]
     VectorVar x(2);
     AnalyticFunction f({x}, x[0]);
 
@@ -54,19 +69,19 @@ TEST_CASE("CtcInverse - manual")
     IntervalVector y({{0.5,3},{-1,1}});
     c.contract(y); // {{1,3},{-1,1}}
     // Only the first component is constrained by the not-in condition
-    // [ctcinv-5-end]
+    // [ctcinv-6-end]
 
     CHECK(y == IntervalVector({{1,3},{-1,1}}));
   }
 
   {
-    // [ctcinv-6-beg]
+    // [ctcinv-7-beg]
     VectorVar x(2);
     AnalyticFunction f({x}, x[0]-x[1]);
     CtcInverse c(f, 0);
     // c.fnc().input_size() == 2
     // c.fnc().output_size() == 1
-    // [ctcinv-6-end]
+    // [ctcinv-7-end]
 
     CHECK(c.fnc().input_size() == 2);
     CHECK(c.fnc().output_size() == 1);

doc/manual/manual/contractors/analytic/src.m

@@ -17,20 +17,34 @@
 % [ctcinv-1-end]
 
 % [ctcinv-2-beg]
-DefaultFigure().pave(IntervalVector({{-6,6},{-6,6}}), c, 1e-2);
+z = IntervalVector({{0.0,3.5},{0.0,1.0}});
+DefaultFigure().draw_box(z, StyleProperties({Color().blue(),Color().blue(.1)})); % prior to contraction
+z = c.contract(z);
+DefaultFigure().draw_box(z, StyleProperties({Color().blue(),Color().white()})); % after one CtcInverse contraction
+% z == [ [1.84, 3.5] ; [0, 1] ]
+
+% Combining CtcInverse with a CtcFixpoint:
+cfix = CtcFixpoint(c);
+z = c.contract(z);
+DefaultFigure().draw_box(z, Color().red()); % after a fixed point contraction
+% z == [ [1.84, 2.483] ; [0, 1] ]
 % [ctcinv-2-end]
 
 % [ctcinv-3-beg]
-s = SepInverse(f, Interval(0,50));
-DefaultFigure().pave(IntervalVector({{-6,6},{-6,6}}), s, 1e-2);
+DefaultFigure().pave(IntervalVector({{-6,6},{-6,6}}), c, 1e-2);
 % [ctcinv-3-end]
 
 % [ctcinv-4-beg]
-cu = CtcUnion(CtcUnion(CtcInverse(f,50), CtcInverse(f,150)), CtcInverse(f,250));
-DefaultFigure().pave(IntervalVector({{-6,6},{-6,6}}), cu, 1e-2)
+s = SepInverse(f, Interval(0,50));
+DefaultFigure().pave(IntervalVector({{-6,6},{-6,6}}), s, 1e-2);
 % [ctcinv-4-end]
 
 % [ctcinv-5-beg]
+cu = CtcUnion(CtcUnion(CtcInverse(f,50), CtcInverse(f,150)), CtcInverse(f,250));
+DefaultFigure().pave(IntervalVector({{-6,6},{-6,6}}), cu, 1e-2)
+% [ctcinv-5-end]
+
+% [ctcinv-6-beg]
 x = VectorVar(2);
 f = AnalyticFunction({x}, x(1));
 
@@ -40,14 +54,14 @@
 y = IntervalVector({{0.5,3},{-1,1}});
 c.contract(y); % [[1,3],[-1,1]]
 % Only the first component is constrained by the not-in condition
-% [ctcinv-5-end]
+% [ctcinv-6-end]
 
 assert(y==IntervalVector({{1,3},{-1,1}}));
 
-% [ctcinv-6-beg]
+% [ctcinv-7-beg]
 x = VectorVar(2);
 f = AnalyticFunction({x}, x(1)-x(2));
 c = CtcInverse(f, 0);
 assert(c.fnc().input_size() == 2);
 assert(c.fnc().output_size() == 1);
-% [ctcinv-6-end]
+% [ctcinv-7-end]

doc/manual/manual/contractors/analytic/src.py

@@ -24,21 +24,67 @@ def tests_CtcInverse_manual(test):
     c = CtcInverse(f, 50)
     # [ctcinv-1-end]
 
+
+    # # Generates the documentation figure:
+
+    # sty = PavingStyle(
+    #   [Color.black(),Color.black()],
+    #   [Color.none(),Color.none()],
+    #   [Color.none(),Color.none()])
+
+    # l = [
+    #   IntervalVector([[0,3],[2,4]]),
+    #   IntervalVector([[0,3.5],[0,1]]),
+    #   IntervalVector([[-2,-1],[0,3]]),
+    #   IntervalVector([[0,2],[-3,-2]]),
+    #   IntervalVector([[-5,-1],[-4.5,-1]]),
+    #   IntervalVector([[3,4],[-3.5,-0.5]])
+    # ]
+
+    # fig = Figure2D("My figure", GraphicOutput.VIBES | GraphicOutput.IPE)
+    # fig.set_axes(axis(0,[-6,6]), axis(1,[-6,6]))
+
+    # for xi in l:
+    #   fig.draw_box(xi, [Color.blue(),Color.blue(0.1)])
+    #   c1 = CtcFixpoint(c)
+    #   xi = c.contract(xi)
+    #   fig.draw_box(xi, [Color.blue(),Color.white()])
+    #   c1 = CtcFixpoint(c,0)
+    #   xi = c1.contract(xi)
+    #   fig.draw_box(xi, [Color.red(),Color.none()])
+
+    # fig.pave([[-6,6],[-6,6]], c, 5e-3, sty)
+
+
     # [ctcinv-2-beg]
-    DefaultFigure.pave([[-6,6],[-6,6]], c, 1e-2)
+    z = IntervalVector([[0,3.5],[0,1]])
+    DefaultFigure.draw_box(z, [Color.blue(),Color.blue(.1)]) # prior to contraction
+    z = c.contract(z)
+    DefaultFigure.draw_box(z, [Color.blue(),Color.white()]) # after one CtcInverse contraction
+    # z == [ [1.84, 3.5] ; [0, 1] ]
+
+    # Combining CtcInverse with a CtcFixpoint:
+    cfix = CtcFixpoint(c)
+    z = c.contract(z)
+    DefaultFigure.draw_box(z, Color.red()) # after a fixed point contraction
+    # z == [ [1.84, 2.483] ; [0, 1] ]
     # [ctcinv-2-end]
 
     # [ctcinv-3-beg]
-    s = SepInverse(f, [0,50])
-    DefaultFigure.pave([[-6,6],[-6,6]], s, 1e-2)
+    DefaultFigure.pave([[-6,6],[-6,6]], c, 1e-2)
     # [ctcinv-3-end]
 
     # [ctcinv-4-beg]
-    cu = CtcInverse(f,50) | CtcInverse(f,150) | CtcInverse(f,250)
-    DefaultFigure.pave([[-6,6],[-6,6]], cu, 1e-2)
+    s = SepInverse(f, [0,50])
+    DefaultFigure.pave([[-6,6],[-6,6]], s, 1e-2)
     # [ctcinv-4-end]
 
     # [ctcinv-5-beg]
+    cu = CtcInverse(f,50) | CtcInverse(f,150) | CtcInverse(f,250)
+    DefaultFigure.pave([[-6,6],[-6,6]], cu, 1e-2)
+    # [ctcinv-5-end]
+
+    # [ctcinv-6-beg]
     x = VectorVar(2)
     f = AnalyticFunction([x], x[0])
 
@@ -48,17 +94,17 @@ def tests_CtcInverse_manual(test):
     y = IntervalVector([[0.5,3],[-1,1]])
     c.contract(y) # [[1,3],[-1,1]]
     # Only the first component is constrained by the not-in condition
-    # [ctcinv-5-end]
+    # [ctcinv-6-end]
 
     test.assertTrue(y == IntervalVector([[1,3],[-1,1]]))
 
-    # [ctcinv-6-beg]
+    # [ctcinv-7-beg]
     x = VectorVar(2)
     f = AnalyticFunction([x], x[0]-x[1])
     c = CtcInverse(f, 0)
     assert c.fnc().input_size() == 2
     assert c.fnc().output_size() == 1
-    # [ctcinv-6-end]
+    # [ctcinv-7-end]
 
 if __name__ ==  '__main__':
   unittest.main()