Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 10 additions & 6 deletions doc/manual/index.rst
Original file line number Diff line number Diff line change
Expand Up @@ -214,11 +214,15 @@ User manual
* The class SetMembershipFunction
* Extension to custom expressions

* :ref:`sec-domains-tubes`
* :ref:`sec-domains-tubes-tdomain`
* :ref:`sec-domains-tubes-slicedtube`
* The Trajectory classes
* Increasing performances using views
* :ref:`sec-tubes-trajectories`
* :ref:`sec-trajectories-sampledtraj`
* :ref:`sec-trajectories-analytictraj`
* :ref:`sec-trajectories-operations`
* :ref:`sec-trajectories-io`
* :ref:`sec-tubes-tdomain`
* :ref:`sec-tubes-slice`
* :ref:`sec-tubes-slicedtube`
* :ref:`sec-tubes-examples`

* Contractors
* What are contractors?
Expand Down Expand Up @@ -354,7 +358,7 @@ User manual
* Related papers
* Contributors
* How to cite Codac
:ref:`sec-ref-codac-logos`
* :ref:`sec-ref-codac-logos`


How-to guides
Expand Down
7 changes: 7 additions & 0 deletions doc/manual/manual/cn/index.rst
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
Contractor Networks
===================

.. toctree::

What is a CN? <http://codac.io>
The ContractorNetwork class <http://codac.io>
9 changes: 9 additions & 0 deletions doc/manual/manual/contractors/basic/index.rst
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
Basic contractors
=================

.. toctree::

CtcIdentity <http://codac.io>
CtcEmpty <http://codac.io>
CtcLazy <http://codac.io>
CtcFixpoint <http://codac.io>
1 change: 1 addition & 0 deletions doc/manual/manual/contractors/index.rst
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
.. _sec-ctc:

Contractors, separators
=======================

Expand Down
8 changes: 8 additions & 0 deletions doc/manual/manual/contractors/linear/index.rst
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
Linear contractors
==================

.. toctree::

CtcGaussElim <http://codac.io>
CtcGaussSeidel <http://codac.io>
CtcLinearPrecond <http://codac.io>
188 changes: 188 additions & 0 deletions doc/manual/manual/contractors/set/ctcunion.rst
Original file line number Diff line number Diff line change
@@ -0,0 +1,188 @@
.. _sec-ctc-set-ctcunion:
.. _sec-sep-set-sepunion:

Union: CtcUnion and SepUnion
============================

Main author: `Simon Rohou <https://www.simon-rohou.fr/research/>`_


``CtcUnion`` and ``SepUnion`` implement the logical union/disjunction counterpart of
``CtcInter`` and ``SepInter``:

.. list-table::
:header-rows: 1
:widths: 20 35 45

* - Class
- Combines
- Meaning
* - ``CtcUnion``
- contractors
- disjunction of constraints, obtained by joining the contracted branches
* - ``SepUnion``
- separators
- separator associated with the union of the represented sets

Both classes can be constructed explicitly or with the ``|`` operator.


CtcUnion: disjunction of contractors
------------------------------------

For box contractors, ``CtcUnion`` applies every stored contractor independently to the
same input box and returns a box enclosing the union of the resulting branches:

.. math::

\mathcal{C}_{\mathrm{union}}([\mathbf{x}])
=
\operatorname{hull}\!\left(
\bigcup_{i=1}^{n}\mathcal{C}_i([\mathbf{x}])
\right),

where :math:`\operatorname{hull}` denotes the smallest box containing the union.

This evaluation differs from ``CtcInter``: the branches are **not** applied
sequentially. Each contractor receives the original input domain.

.. note::

The exact union of several boxes is generally not a box. ``CtcUnion`` therefore
returns a box enclosure of this union. This enclosure may contain points that do not
belong to any individual branch.

The usual construction uses ``|`` or the ``CtcUnion`` constructor.

.. tabs::

.. group-tab:: Python

.. literalinclude:: src.py
:language: py
:start-after: [union-ctc-1-beg]
:end-before: [union-ctc-1-end]
:dedent: 4

.. group-tab:: C++

.. literalinclude:: src.cpp
:language: c++
:start-after: [union-ctc-1-beg]
:end-before: [union-ctc-1-end]
:dedent: 2

Applying it to a box gives the hull of the contracted branches:

.. tabs::

.. group-tab:: Python

.. literalinclude:: src.py
:language: py
:start-after: [union-ctc-2-beg]
:end-before: [union-ctc-2-end]
:dedent: 4

.. group-tab:: C++

.. literalinclude:: src.cpp
:language: c++
:start-after: [union-ctc-2-beg]
:end-before: [union-ctc-2-end]
:dedent: 2

For the two boxes used here, the exact union is not itself a box. Its interval hull is

.. math::

[-12,10]\times[-2,4].


SepUnion: union of represented sets
-----------------------------------

``SepUnion`` is the separator counterpart. If separators
:math:`\mathcal{S}_1,\ldots,\mathcal{S}_n` are associated with sets
:math:`\mathbb{S}_1,\ldots,\mathbb{S}_n`, then ``SepUnion`` is associated with

.. math::

\mathbb{S}_{\mathrm{union}}
=
\mathbb{S}_1 \cup \cdots \cup \mathbb{S}_n.

Construction follows the same syntax as for ``CtcUnion``:

.. tabs::

.. group-tab:: Python

.. literalinclude:: src.py
:language: py
:start-after: [union-sep-1-beg]
:end-before: [union-sep-1-end]
:dedent: 4

.. group-tab:: C++

.. literalinclude:: src.cpp
:language: c++
:start-after: [union-sep-1-beg]
:end-before: [union-sep-1-end]
:dedent: 2


Building a union incrementally
------------------------------

Both classes support ``|=`` and ``nb()``.

For ``CtcUnion``, a union may be created from the dimension only. Before a branch is
added, it represents the empty disjunction: contracting a box with it returns the empty
domain. Adding contractors with ``|=`` then builds the disjunction incrementally.

.. tabs::

.. group-tab:: Python

.. literalinclude:: src.py
:language: py
:start-after: [union-ctc-3-beg]
:end-before: [union-ctc-3-end]
:dedent: 4

.. group-tab:: C++

.. literalinclude:: src.cpp
:language: c++
:start-after: [union-ctc-3-beg]
:end-before: [union-ctc-3-end]
:dedent: 2

``SepUnion`` currently has no constructor taking only a dimension, so incremental
construction starts from an existing separator:

.. tabs::

.. group-tab:: Python

.. literalinclude:: src.py
:language: py
:start-after: [union-sep-2-beg]
:end-before: [union-sep-2-end]
:dedent: 4

.. group-tab:: C++

.. literalinclude:: src.cpp
:language: c++
:start-after: [union-sep-2-beg]
:end-before: [union-sep-2-end]
:dedent: 2


.. admonition:: Technical documentation

See the `C++ API documentation of CtcUnion <../../api/html/classcodac2_1_1_ctc_union.html>`_
and the `C++ API documentation of SepUnion <../../api/html/classcodac2_1_1_sep_union.html>`_.
14 changes: 14 additions & 0 deletions doc/manual/manual/contractors/temporal/index.rst
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
Temporal contractors
====================

.. toctree::

Using static contractors on tubes <http://codac.io>
CtcDeriv <http://codac.io>
CtcEval <http://codac.io>
CtcDelay <http://codac.io>
CtcLinobs <http://codac.io>
CtcLohner <http://codac.io>
CtcPicard <http://codac.io>
CtcChain <http://codac.io>
CtcDiffInclusion <http://codac.io>
7 changes: 7 additions & 0 deletions doc/manual/manual/extensions/ibex/index.rst
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
Interface with the IBEX library
===============================

.. toctree::

Installing the codac-ibex extension <http://codac.io>
How to use <http://codac.io>
6 changes: 6 additions & 0 deletions doc/manual/manual/extensions/unsupported/index.rst
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
Unsupported features of Codac
=============================

.. toctree::

Installing the codac-unsupported extension <http://codac.io>
2 changes: 2 additions & 0 deletions doc/manual/manual/functions/analytic/analytic_operators.rst
Original file line number Diff line number Diff line change
Expand Up @@ -350,6 +350,8 @@ Temporal operations for involving trajectories or tubes in analytic expressions
);


For a detailed example using ``SampledTraj.as_function()`` and information on pointwise ``AnalyticFunction.traj_eval(...)``, see :ref:`sec-trajectories-operations`.

Direct use of operators
^^^^^^^^^^^^^^^^^^^^^^^

Expand Down
6 changes: 2 additions & 4 deletions doc/manual/manual/functions/analytic/index.rst
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,5 @@ Analytic inclusion functions

.. toctree::

analytic_functions.rst
analytic_operators.rst
Extension to custom expressions
Temporal functions
analytic_functions.rst
analytic_operators.rst
10 changes: 5 additions & 5 deletions doc/manual/manual/functions/index.rst
Original file line number Diff line number Diff line change
Expand Up @@ -4,9 +4,9 @@ Inclusion functions
===================

.. toctree::
:maxdepth: 1

analytic/analytic_functions.rst
analytic/analytic_operators.rst
parallelepiped/parallelepiped_eval.rst
peibos/peibos.rst
.. Set-membership functions
analytic/analytic_functions.rst
analytic/analytic_operators.rst
parallelepiped/parallelepiped_eval.rst
peibos/peibos.rst
7 changes: 7 additions & 0 deletions doc/manual/manual/functions/setmembership/index.rst
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
Set-membership functions
========================

.. toctree::

The class SetMembershipFunction <http://codac.io>
Extension to custom expressions <http://codac.io>
2 changes: 2 additions & 0 deletions doc/manual/manual/intervals/Interval_class.rst
Original file line number Diff line number Diff line change
Expand Up @@ -257,6 +257,8 @@ For instance, ``x < y`` returns:
- ``BoolInterval.UNKNOWN`` otherwise.


.. _sec-intervals-class-un-bin-ary:

Unary and binary functions
--------------------------

Expand Down
Loading
Loading