p-floats.tex.in

% -*- mode: LaTeX; -*- 
\chapter{Propagators for float constraints}
\label{chap:p:floats}

This chapter shows how to implement propagators for constraints
over float variables. We assume that you have worked through the
chapters on implementing integer propagators, as most of the
techniques readily carry over and are not explained again
here.

\paragraph{Overview.}

\mbox{}\autoref{sec:p:floats:example} demonstrates a propagator
that implements a ternary linear constraint. Float views and
their related concepts are summarized in
\autoref{sec:p:floats:propagation}.


\section{A simple example}
\label{sec:p:floats:example}

\begin{figure}
\insertlitcode{linear}
\caption{A constraint and propagator for ternary linear}
\label{fig:p:floats:linear}
\end{figure}

\autoref{fig:p:floats:linear} shows a propagator for the
ternary linear constraint
$\mathtt{x}_0+\mathtt{x}_1+\mathtt{x}_2=0$ for three float
variables $\mathtt{x}_0$, $\mathtt{x}_1$, and $\mathtt{x}_2$.

As you can see, propagators for float constraints follow exactly
the same structure as propagators for integer or Boolean
constraints. The same propagator patterns can be used (see
\autoref{sec:p:started:patterns}). The appropriate views and
propagation conditions are defined in the namespace
\gecoderef[namespace]{Gecode::Float}.

\paragraph{Operations on float views.}

\begin{figure}
\begin{center}
\begin{tabular}{ll}
\multicolumn{2}{c}{\textbf{access operations}}\\
\?min()? & return lower bound (a float number)\\
\?max()? & return upper bound (a float number)\\
\?size()? & return width of domain (a float number)\\
\?assigned()? & whether view is assigned\\
\?in(n)? & whether float number \?n? is contained in domain\\
\?in(n)? & whether float value \?n? is contained in domain\\
\\
\multicolumn{2}{c}{\textbf{modification operations}}\\
\?eq(home,n)? & restrict values to be equal to \?n?\\
\?lq(home,n)? & restrict values to be less or equal than \?n?\\
\?gq(home,n)? & restrict values to be greater or equal than \?n?\\
\end{tabular}
\end{center}
\caption{Most important float view operations}
\label{fig:p:float:view}
\end{figure}

The most important operations on float views for programming
propagators are summarized in \autoref{fig:p:float:view}, the
full information can be found in
\gecoderef[class]{Float::FloatView}. The lack of operations such
as \?gr()? (for greater), \?le()? (for less), and \?nq()? (for
disequality) is due to the fact that domains are closed
intervals, see \autoref{sec:m:float:val} and
\autoref{tip:m:float:weak}.

\paragraph{Creating a rounding object.}

\begin{figure}
\begin{center}
\begin{tabular}{|l|l|c|}
\hline
\multicolumn{1}{|c|}{function} &
\multicolumn{1}{c|}{meaning}&default\\
\hline
\hline
\?add_down(x,y)?, \?add_up(x,y)? & l/u bound of
$\mathtt{x}+\mathtt{y}$
&\YES\\
\?sub_down(x,y)?, \?sub_up(x,y)? &
l/u bound of $\mathtt{x} - \mathtt{y}$
&\YES\\
\?mul_down(x,y)?, \?mul_up(x,y)? 
& l/u bound of $\mathtt{x} \times \mathtt{y}$
&\YES\\
\?div_down(x,y)?, \?div_up(x,y)? 
& l/u bound of $\mathtt{x} / \mathtt{y}$
&\YES\\\hline
\?sqrt_down(x)?, \?sqrt_up(x)? 
& l/u bound of $\sqrt{\mathtt{x}}$
&\YES\\\hline
\texttt{int}\?_down(x)? & next downward-rounded integer of $\mathtt{x}$
&\YES\\
\texttt{int}\?_up(x)? & next upward-rounded integer of $\mathtt{x}$
&\YES\\\hline
\?exp_down(x)?, \?exp_up(x)? 
& l/u bound of $\exp(\mathtt{x})$
&\\
\?log_down(x)?, \?log_up(x)? 
& l/u bound of $\log(\mathtt{x})$
&\\\hline
\?sin_down(x)?, \?sin_up(x)? 
& l/u bound of $\sin(\mathtt{x})$
&\\
\?cos_down(x)?, \?cos_up(x)? 
& l/u bound of $\cos(\mathtt{x})$
&\\
\?tan_down(x)?, \?tan_up(x)? 
& l/u bound of $\tan(\mathtt{x})$
&\\\hline
\?asin_down(x)?, \?asin_up(x)? 
& l/u bound of $\arcsin(\mathtt{x})$
&\\
\?acos_down(x)?, \?acos_up(x)? 
& l/u bound of $\arccos(\mathtt{x})$
&\\
\?atan_down(x)?, \?atan_up(x)? 
& l/u bound of $\arctan(\mathtt{x})$
&\\\hline
\?sinh_down(x)?, \?sinh_up(x)? 
& l/u bound of $\sinh(\mathtt{x})$
&\\
\?cosh_down(x)?, \?cosh_up(x)? 
& l/u bound of $\cosh(\mathtt{x})$
&\\
\?tanh_down(x)?, \?tanh_up(x)? 
& l/u bound of $\tanh(\mathtt{x})$
&\\\hline
\?asinh_down(x)?, \?asinh_up(x)? 
& l/u bound of $\arcsinh(\mathtt{x})$
&\\
\?acosh_down(x)?, \?acosh_up(x)? 
& l/u bound of $\arccosh(\mathtt{x})$
&\\
\?atanh_down(x)?, \?atanh_up(x)? 
& l/u bound of $\arctanh(\mathtt{x})$
&\\\hline
\end{tabular}
\end{center}
\caption[Rounding operations on float numbers]{Rounding
  operations on float numbers 
  (\?x? and \?y? are float numbers)}
\label{fig:p:floats:rounding}
\end{figure}

The propagation rules of the \?Linear? propagator will require
that it can be controlled whether to round downwards or upwards
in a floating point operation on a float number. Access to
operations with explicit rounding control is provided by an
object of class \gecoderef[class]{Float::Rounding}. The creation
of an object of this class initializes the underlying floating
point unit such that it performs exact rounding in the required
direction. Note, that explicit rounding is only required if
rounding provided by operations on float values is not
sufficient.

\mbox{}\autoref{fig:p:floats:rounding} lists the supported
operations with explicit rounding, where the \?_down()? variants
round downwards and the \?_up()? variants round upwards. The
functions marked as default are always supported, the others are
only supported if Gecode has been built accordingly, see
\autoref{m:float:mpfr}.

Hence, the first thing that the \?propagate()? function of the
\?Linear? propagator does is to create a rounding object \?r? as
follows:
\insertlitcode{linear:create rounding object}

\paragraph{Pruning lower and upper bounds.}

The propagation rules for \?Linear? are quite
straightforward. As $\mathtt{x}_0+\mathtt{x}_1+\mathtt{x}_2=0$ we
can isolate $\mathtt{x}_0$ ($\mathtt{x}_1$ and $\mathtt{x}_2$ are
of course analogous):
$$
\mathtt{x}_0=-\mathtt{x}_1-\mathtt{x}_2
$$
The upper bound of $\mathtt{x}_0$ can be constrained following:
\begin{eqnarray*}
\mathtt{x}_0&\leq&\max\left(-\mathtt{x}_1-\mathtt{x}_2\right)\\
            &=&-\min\left(\mathtt{x}_1+\mathtt{x}_2\right)\\
            &=&-\min\left(\min(\mathtt{x}_1)+\min(\mathtt{x}_2)\right)
\end{eqnarray*}
and, accordingly, the lower bound of $\mathtt{x}_0$ can be
constrained following:
\begin{eqnarray*}
\mathtt{x}_0&\geq&\min\left(-\mathtt{x}_1-\mathtt{x}_2\right)\\
            &=&-\max\left(\mathtt{x}_1+\mathtt{x}_2\right)\\
            &=&-\max\left(\max(\mathtt{x}_1)+\max(\mathtt{x}_2\right))
\end{eqnarray*}

The equations can be translated directly into
update operations, where $\min$ corresponds to rounding
downwards:
\insertlitcode{linear:prune upper bounds}
and $\max$ corresponds to rounding upwards:
\insertlitcode{linear:prune lower bounds}



\section{Modification events, propagation conditions, views,
   and advisors}
\label{sec:p:floats:propagation}

This section summarizes how these concepts are
specialized for float variables and propagators.

\paragraph{Modification events and propagation conditions.}

\begin{figure}
\begin{center}
\begin{tabular}{ll}
\multicolumn{2}{c}{\textbf{float modification events}}\\
\?Float::ME_FLOAT_NONE? & the view has not been changed\\
\?Float::ME_FLOAT_FAILED? & the domain has become empty\\
\?Float::ME_FLOAT_VAL? & the view has been assigned\\
\?Float::ME_FLOAT_BND? & the bounds have changed (the domain has changed)\\
\\
\multicolumn{2}{c}{\textbf{float propagation conditions}}\\
\?Float::PC_FLOAT_VAL? & schedule when the view is assigned\\
\?Float::PC_FLOAT_BND? & schedule when the domain changes\\
\?Float::PC_FLOAT_NONE? & do not schedule\\
\end{tabular}
\end{center}
\caption{Float modification events and propagation conditions}
\label{fig:p:floats:propagation_conditions}
\end{figure}

The modification events and propagation conditions for float
propagators (see
\autoref{fig:p:floats:propagation_conditions}) capture
how the variable domain of a float view can change.


\paragraph{Float variable views.}

In addition to the basic \gecoderef[class]{Float::FloatView} class,
there are two other float views:
\gecoderef[class]{Float::MinusView}, and
\gecoderef[class]{Float::ScaleView}. The two latter views are
defined similarly to minus view for integers (see
\autoref{sec:p:views:int:minus}) and scale views for integers
(see \autoref{sec:p:views:int:constantscale}).

\paragraph{Advisors for float propagators.}

Advisors for float constraints get informed about the domain
modifications using a float delta of class
\gecoderef[class]{Float::FloatDelta}. 

Float deltas are also represented by a minimum and maximum
float number and hence also constitute a closed interval (like float
values and float variables). That means that a float delta
cannot describe exactly which values have been removed. For example,
assume that \?x? is a float view and that the domain of \?x? is
$\range{-1.0}{1.0}$. Then, executing
\begin{code}
GECODE_ME_CHECK(x.lq(home,0.0));
\end{code}
will generate a float delta \?d? such that \?x.min(d)? returns
\?0.0? and \?x.max(d)? returns \?1.0? even though the domain of \?x?
is now $\range{-1.0}{0.0}$ and still includes $0.0$.


\begin{litcode}{linear}{schulte}
#include <gecode/float.hh>
using namespace Gecode;
  
class Linear
  : public TernaryPropagator<Float::FloatView,Float::PC_FLOAT_BND> {
public:
  Linear(Home home, Float::FloatView x0, Float::FloatView x1,
                    Float::FloatView x2)
    : TernaryPropagator<Float::FloatView,Float::PC_FLOAT_BND>
        (home,x0,x1,x2) {}
  \begin{litblock}{anonymous}
  static ExecStatus post(Home home, Float::FloatView x0, Float::FloatView x1,
                         Float::FloatView x2) {
    (void) new (home) Linear(home,x0,x1,x2);
    return ES_OK;
  }
  Linear(Space& home, Linear& p)
    : TernaryPropagator<Float::FloatView,Float::PC_FLOAT_BND>(home,p) {}
  virtual Propagator* copy(Space& home) {
    return new (home) Linear(home,*this);
  }
  \end{litblock}
  virtual ExecStatus propagate(Space& home, const ModEventDelta&)  {
    using namespace Float;
    \begin{litblock}{create rounding object}
    Rounding r;
    \end{litblock}
    \begin{litblock}{prune upper bounds}
    GECODE_ME_CHECK(x0.lq(home,-r.add_down(x1.min(),x2.min())));
    GECODE_ME_CHECK(x1.lq(home,-r.add_down(x0.min(),x2.min())));
    GECODE_ME_CHECK(x2.lq(home,-r.add_down(x0.min(),x1.min())));
    \end{litblock}
    \begin{litblock}{prune lower bounds}
    GECODE_ME_CHECK(x0.gq(home,-r.add_up(x1.max(),x2.max())));
    GECODE_ME_CHECK(x1.gq(home,-r.add_up(x0.max(),x2.max())));
    GECODE_ME_CHECK(x2.gq(home,-r.add_up(x0.max(),x1.max())));
    \end{litblock}
    return (x0.assigned() && x1.assigned()) ?
      home.ES_SUBSUMED(*this) : ES_NOFIX;
  }
};

void linear(Home home, FloatVar x0, FloatVar x1, FloatVar x2) {
  GECODE_POST;
  GECODE_ES_FAIL(Linear::post(home,x0,x1,x2));
}
\end{litcode}