/usr/share/mozart/doc/system/node21.html is in mozart-doc 1.4.0-8ubuntu1.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 | <!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">
<HTML><HEAD><TITLE>5.7 Generic Propagators</TITLE><LINK href="ozdoc.css" rel="stylesheet" type="text/css"></HEAD><BODY><TABLE align="center" border="0" cellpadding="6" cellspacing="6" class="nav"><TR bgcolor="#DDDDDD"><TD><A href="node20.html#section.fd.watching"><< Prev</A></TD><TD><A href="node14.html">- Up -</A></TD><TD><A href="node22.html#section.fd.nonlinear">Next >></A></TD></TR></TABLE><DIV id="section.fd.arithmetic"><H2><A name="section.fd.arithmetic">5.7 Generic Propagators</A></H2><P>The generic propagators <CODE>FD<SPAN class="keyword">.</SPAN>sum</CODE>, <CODE>FD<SPAN class="keyword">.</SPAN>sumC</CODE> and <CODE>FD<SPAN class="keyword">.</SPAN>sumCN</CODE> do interval propagation. The propagators <CODE>FD<SPAN class="keyword">.</SPAN>sumAC</CODE> and <CODE>FD<SPAN class="keyword">.</SPAN>sumACN</CODE> do interval propagation but may also cut holes into domains. For example, </P><BLOCKQUOTE class="code"><CODE>{FD<SPAN class="keyword">.</SPAN>dom 0<SPAN class="keyword">#</SPAN>10 [X Y]}<BR>{FD<SPAN class="keyword">.</SPAN>sumAC [1 <SPAN class="keyword">~</SPAN>1] [X Y] <SPAN class="string">'>:'</SPAN> 8}</CODE></BLOCKQUOTE><P> will reduce the domains of <CODE>X</CODE> and <CODE>Y</CODE> to <IMG alt="\{0,1,9,10\}" src="latex24.png">. Except for propagators <CODE>FD<SPAN class="keyword">.</SPAN>sumCN</CODE> and <CODE>FD<SPAN class="keyword">.</SPAN>sumACN</CODE>, equality is exploited, e. g. <CODE>{FD<SPAN class="keyword">.</SPAN>sumC [2 3] [A A] <SPAN class="string">'=:'</SPAN> 10}</CODE> is equivalent to <CODE>{FD<SPAN class="keyword">.</SPAN>sumC [5] [A] <SPAN class="string">'=:'</SPAN> 10}</CODE>. </P><P class="margin"><IMG alt="\underline{x}" src="latex29.png">,<IMG alt="\overline{x}" src="latex30.png"></P><P> Let <I>S</I> denote the current constraint store and <I>x</I> a finite domain integer.<IMG alt="\underline{x}" src="latex29.png"> denotes the largest integer such that <IMG alt="S \models x \geq \underline{x}" src="latex31.png"> holds. Analogously, <IMG alt="\overline{x}" src="latex30.png"> denotes the smallest integer such that <IMG alt="S \models x \leq \overline{x}" src="latex32.png"> holds. </P><P class="margin"><IMG alt="\lfloor n \rfloor$, $\lceil n \rceil" src="latex33.png"></P><P> Let <I>n</I> denote a real number. <IMG alt="\lfloor n \rfloor" src="latex34.png"> denotes the largest integer which is equal or smaller than <I>n</I>. Analogously, <IMG alt="\lceil n \rceil" src="latex35.png"> denotes the smallest integer which is equal or larger than <I>n</I>. </P><DL><DT><A name="label168"></A> <CODE>sum</CODE></DT><DD><BLOCKQUOTE class="synopsis"><P></P><BLOCKQUOTE class="code"><CODE>{FD<SPAN class="keyword">.</SPAN>sum </CODE><CODE>*<I>Dv</I></CODE><CODE> </CODE><CODE>+<I>A</I></CODE><CODE> </CODE><CODE>*<I>D</I></CODE><CODE>}</CODE></BLOCKQUOTE><P></P></BLOCKQUOTE></DD><DD><P>creates a propagator for </P><P><IMG alt="1*{\tt D}_1+\ldots+1*{\tt D}_n+(-1)*{\tt D}\;\sim_{{\tt A}}\;0" src="latex36.png"></P><P>For the operational semantics see <CODE>FD<SPAN class="keyword">.</SPAN>sumC</CODE>. For the relation symbol <CODE><SPAN class="string">'\\=:'</SPAN></CODE>, the propagator waits until at most one non-determined variable is left. Then the appropriate value is discarded from the variable's domain. For the other relations, the propagator does interval propagation. </P></DD><DT><A name="label170"></A> <CODE>sumC</CODE></DT><DD><BLOCKQUOTE class="synopsis"><P></P><BLOCKQUOTE class="code"><CODE>{FD<SPAN class="keyword">.</SPAN>sumC </CODE><CODE>+<I>Iv</I></CODE><CODE> </CODE><CODE>*<I>Dv</I></CODE><CODE> </CODE><CODE>+<I>A</I></CODE><CODE> </CODE><CODE>*<I>D</I></CODE><CODE>}</CODE></BLOCKQUOTE><P></P></BLOCKQUOTE></DD><DD><P>creates a propagator for the scalar product of the vectors <CODE><I>Iv</I></CODE> and <CODE><I>Dv</I></CODE>: </P><P><IMG alt="{\tt I}_1*{\tt D}_1+\ldots+{\tt I}_n*{\tt D}_n+(-1)*{\tt D}\;\sim_{{\tt A}}\;0" src="latex37.png"></P><P> Let <IMG alt="{\tt D}_{n+1}" src="latex38.png"> be <CODE><I>D</I></CODE> and <IMG alt="{\tt I}_{n+1}" src="latex39.png"> be -1. Then, the operational semantics is defined as follows. For each product <IMG alt="{\tt I}_k*{\tt D}_k" src="latex40.png">, an isolation (projection) is computed:</P><P><IMG alt=" {\tt I}_k*{\tt D}_k \;\sim_{{\tt A}}\; \underbrace{- \sum_{i = 1, i \neq k}^{n+1}
{\tt I}_i * {\tt D}_i}_{{\mbox{\sl RHS}}_k}." src="latex41.png"></P><P>For the right hand side <IMG alt="{\mbox{\sl RHS}}_k" src="latex42.png">, the upper <IMG alt="\overline{\mbox{\mbox{\sl RHS}}_k}" src="latex43.png"> and lower limit <IMG alt="\underline{\mbox{\mbox{\sl RHS}}_k}" src="latex44.png"> are defined as follows.</P><P><IMG alt=" ~$~
\begin{eqnarray*}
\overline{\mbox{\mbox{\sl RHS}}_k} \ =\
-\sum_{i =1, i\neq k, {\tt I}_i > 0}^{n+1} {\tt I}_i *
\underline{{\tt D}}_i \;-\;
\sum_{i =1, i\neq k, {\tt I}_i < 0}^{n+1} {\tt I}_i *
\overline{{\tt D}}_i
\\
\underline{\mbox{\mbox{\sl RHS}}_k} \ = \
-\sum_{i =1, i\neq k, {\tt I}_i > 0}^{n+1} {\tt I}_i *
\overline{{\tt D}}_i \;-\;
\sum_{i =1, i\neq k, {\tt I}_i < 0}^{n+1} {\tt I}_i *
\underline{{\tt D}}_i
\end{eqnarray*}
~$~" src="latex45.png"></P><P>These values are used to narrow the domain of <IMG alt="{\tt D}_k" src="latex46.png"> until a fixed point is reached. We describe the propagation for the different possible values of <CODE>A</CODE>. </P><DL><DT><CODE><SPAN class="string">'=<:'</SPAN></CODE></DT><DD><P>Narrowing is done according to the following inequalities.</P><P><IMG alt="{\tt D}_k \leq \left \lfloor \frac{\overline{{\mbox{\sl RHS}}_k}}{{\tt I}_k}
\right \rfloor \quad
\mbox{ if\ } {\tt I}_k > 0" src="latex47.png"></P><P><IMG alt="{\tt D}_k \geq \left \lceil \frac{\overline{{\mbox{\sl RHS}}_k}}{{\tt I}_k} \right \rceil \quad
\mbox{ if\ } {\tt I}_k < 0" src="latex48.png"></P><P>Here <IMG alt="x\leq n" src="latex49.png"> denotes the basic constraint <IMG alt="x \in
\{0,\ldots,n\}" src="latex50.png"> and <IMG alt="x \geq n" src="latex51.png"> denotes the basic constraint <IMG alt="x \in
\{n,\ldots,\codeinline{oz}{FD.sup}\}" src="latex52.png">. </P><P>The propagator ceases to exist, if the following condition holds. </P><P><IMG alt="\sum_{i =1, {\tt I}_i > 0}^{n+1} {\tt I}_i *
\overline{{\tt D}}_i \;+\;
\sum_{i =1, {\tt I}_i < 0}^{n+1} {\tt I}_i *
\underline{{\tt D}}_i
\leq 0" src="latex53.png"></P><P>As an example consider </P><BLOCKQUOTE class="code"><CODE>X <SPAN class="keyword">-</SPAN> Y <SPAN class="keyword">=<:</SPAN> Z <SPAN class="keyword">-</SPAN> V</CODE></BLOCKQUOTE><P> We have the following narrowing.</P><P><IMG alt="\codeinline{oz}{X} \leq \overline{\codeinline{oz}{Z}} - \underline{\codeinline{oz}{V}} + \overline{\codeinline{oz}{Y}}
\quad \quad
\codeinline{oz}{Y} \geq \underline{\codeinline{oz}{X}} - \overline{\codeinline{oz}{Z}} + \overline{\codeinline{oz}{V}}
\quad \quad
\codeinline{oz}{Z} \geq \underline{\codeinline{oz}{X}} - \overline{\codeinline{oz}{Y}} + \underline{\codeinline{oz}{V}}
\quad\quad
\codeinline{oz}{V} \leq \overline{\codeinline{oz}{Z}} - \underline{\codeinline{oz}{X}} + \overline{\codeinline{oz}{Y}}" src="latex54.png"></P><P>The propagator ceases to exist if <IMG alt="\overline{\codeinline{oz}{X}} - \underline{\codeinline{oz}{Y}}
\leq \underline{\codeinline{oz}{Z}} - \overline{\codeinline{oz}{V}}" src="latex55.png"> holds. </P></DD><DT><CODE><SPAN class="string">'>=:'</SPAN></CODE></DT><DD><P>This case can be reduced to <CODE><SPAN class="keyword">=<:</SPAN></CODE> due to the observation that </P><P><IMG alt="{\tt I}_1*{\tt D}_1+\ldots+{\tt I}_n*{\tt D}_n+(-1)*{\tt D}\;\geq\;0" src="latex56.png"></P><P>is equivalent to </P><P><IMG alt="(-{\tt I}_1)*{\tt D}_1+\ldots+(-{\tt I}_n)*{\tt D}_n+1*{\tt D}\;\leq\;0" src="latex57.png"></P><P>Alternatively, <IMG alt="\underline{\mbox{\mbox{\sl RHS}}_k}" src="latex44.png"> can be used for the definition. </P></DD><DT><CODE><SPAN class="string">'<:'</SPAN></CODE> </DT><DD><P>Analogous to <CODE><SPAN class="string">'=<:'</SPAN></CODE></P></DD><DT><CODE><SPAN class="string">'>:'</SPAN></CODE> </DT><DD><P>Analogous to <CODE><SPAN class="string">'>=:'</SPAN></CODE></P></DD><DT><CODE><SPAN class="string">'=:'</SPAN></CODE></DT><DD><P>In this case, the operational semantics is defined by conjunction of the formulas given for <CODE><SPAN class="keyword">=<:</SPAN></CODE> and <CODE><SPAN class="keyword">>=:</SPAN></CODE>. Furthermore, coreferences are realized in that, e. g. the propagator <CODE>3<SPAN class="keyword">*</SPAN>X<SPAN class="keyword">=:</SPAN>3<SPAN class="keyword">*</SPAN>Y</CODE> tells the basic constraint <CODE>X=Y</CODE>. </P></DD><DT><CODE><SPAN class="string">'\\=:'</SPAN></CODE></DT><DD><P>In this case, the propagator waits until at most one non-determined variable is left, say <IMG alt="{\tt D}_k" src="latex46.png">. Then, <IMG alt="{\mbox{\sl RHS}}_k" src="latex42.png"> denotes a unique integer value which is discarded from the domain of <IMG alt="{\tt D}_k" src="latex46.png">.</P></DD></DL><P></P><P>Additional propagation is achieved through the realization of coreferences, i. e. equality between variables. If the store <CODE><I>S</I></CODE> entails (without loss of generality) <IMG alt="{\tt D}_1 = {\tt D}_2" src="latex58.png">, the generic propagator evolves into:</P><P><IMG alt="({\tt I}_1 + {\tt I}_2) * {\tt D}_2 + \ldots +
{\tt I}_n*{\tt D}_n+(-1)*{\tt D}\;\sim_{{\tt A}}\;0 " src="latex59.png"></P><P></P></DD><DT><A name="label172"></A> <CODE>sumCN</CODE></DT><DD><BLOCKQUOTE class="synopsis"><P></P><BLOCKQUOTE class="code"><CODE>{FD<SPAN class="keyword">.</SPAN>sumCN </CODE><CODE>+<I>Iv</I></CODE><CODE> </CODE><CODE>*<I>Dvv</I></CODE><CODE> </CODE><CODE>+<I>A</I></CODE><CODE> </CODE><CODE>*<I>D</I></CODE><CODE>}</CODE></BLOCKQUOTE><P></P></BLOCKQUOTE></DD><DD><P>creates a propagator for </P><P><IMG alt="{\tt I}_1*{\tt D}_{11}*\ldots*{\tt D}_{1m_1}+\ldots+{\tt I}_n*{\tt D}_{n1}*\ldots*{\tt D}_{nm_n}+
(-1)*{\tt D}\;\sim_{{\tt A}}\;0" src="latex60.png"></P><P> Let <IMG alt="{\tt D}_{(n+1)1}" src="latex61.png"> be <CODE><I>D</I></CODE>, <IMG alt="{\tt I}_{n+1}" src="latex39.png"> be -1, and <IMG alt="m_{n+1}" src="latex62.png"> be 1. Then, the operational semantics is defined as follows. For <IMG alt="k, 1
\leq k \leq n+1" src="latex63.png">, an isolation (projection) is computed:</P><P><IMG alt="{\tt I}_{k}*{\tt D}_{k1}*\ldots*{\tt D}_{km_k} \;\sim_{{\tt A}}\; \underbrace{- {\sum_{i = 1, i \neq k}^{n+1}
{\tt I}_i * \prod_{j=1}^{m_i}{\tt D}_{ij}}}_{{\mbox{\sl RHS}}_k}" src="latex64.png"></P><P> For the right hand side <IMG alt="{\mbox{\sl RHS}}_k" src="latex42.png">, the upper <IMG alt="\overline{\mbox{\mbox{\sl RHS}}_k}" src="latex43.png"> and lower limit <IMG alt="\underline{\mbox{\mbox{\sl RHS}}_k}" src="latex44.png"> are defined as follows.</P><P><IMG alt="~$~
\begin{eqnarray*}
\overline{\mbox{\mbox{\sl RHS}}_k} \ =\
-\sum_{i =1, i\neq k, {\tt I}_i > 0}^{n+1} {\tt I}_i *
\prod_{j=1}^{m_i}\underline{{\tt D}}_{ij} \;-\;
\sum_{i =1, i\neq k, {\tt I}_i < 0}^{n+1} {\tt I}_i *
\prod_{j=1}^{m_i}\overline{{\tt D}}_{ij}
\\
\underline{\mbox{\mbox{\sl RHS}}_k} \ = \
-\sum_{i =1, i\neq k, {\tt I}_i > 0}^{n+1} {\tt I}_i *
\prod_{j=1}^{m_i}\overline{{\tt D}}_{ij} \;-\;
\sum_{i =1, i\neq k, {\tt I}_i < 0}^{n+1} {\tt I}_i *
\prod_{j=1}^{m_i}\underline{{\tt D}}_{ij}
\end{eqnarray*}
~$~" src="latex65.png"></P><P>These values are used to narrow the domain of <IMG alt="{\tt D}_{kl}, 1 \leq l
\leq m_k," src="latex66.png"> until a fixed point is reached. We describe the propagation for the different possible values of <CODE>A</CODE>. </P><DL><DT><CODE><SPAN class="string">'=<:'</SPAN></CODE></DT><DD><P>The narrowing is done according to the following inequalities.</P><P><IMG alt="{\tt D}_{kl} \leq \left \lfloor \frac{\overline{\mbox{\sl RHS}}_k}{{\tt I}_k * \prod_{j=1,
j\neq l}^{m_k} \underline{{\tt D}}_{kj}} \right \rfloor \quad
\mbox{ if\ } {\tt I}_k > 0" src="latex67.png"></P><P></P><P><IMG alt="{\tt D}_{kl} \geq \left \lceil \frac{\overline{\mbox{\sl RHS}}_k}{{\tt I}_k * \prod_{j=0,
j\neq l}^{m_k} \overline{{\tt D}}_{kj}} \right \rceil \quad
\mbox{ if\ } {\tt I}_k < 0" src="latex68.png"></P><P> Here <IMG alt="x\leq n" src="latex49.png"> denotes the basic constraint <IMG alt="x \in
\{0,\ldots,n\}" src="latex50.png"> and <IMG alt="x \geq n" src="latex51.png"> denotes the basic constraint <IMG alt="x \in
\{n,\ldots,\codeinline{oz}{FD.sup}\}" src="latex52.png">. </P><P>The propagator ceases to exist, if the following condition holds. </P><P><IMG alt="\sum_{i =1, {\tt I}_i > 0}^{n+1} {\tt I}_i *
\prod_{j=1}^{m_i}\overline{{\tt D}}_{ij} +
\sum_{i =1, {\tt I}_{i} < 0}^{n+1} {\tt I}_i *
\prod_{j=1}^{m_i}\underline{{\tt D}}_i
\leq 0" src="latex69.png"></P><P> As an example consider </P><BLOCKQUOTE class="code"><CODE>3<SPAN class="keyword">*</SPAN>X<SPAN class="keyword">*</SPAN>Y <SPAN class="keyword">-</SPAN> Z <SPAN class="keyword">=<:</SPAN> A</CODE></BLOCKQUOTE><P> We have the following formulas.</P><P><IMG alt="\codeinline{oz}{X} \leq \left\lfloor \frac{\overline{\codeinline{oz}{A}} +
\overline{\codeinline{oz}{Z}}}{3*\underline{\codeinline{oz}{Y}}} \right\rfloor
\quad \quad
\codeinline{oz}{Y} \leq \left\lfloor \frac{\overline{\codeinline{oz}{A}} +
\overline{\codeinline{oz}{Z}}}{3*\underline{\codeinline{oz}{X}}} \right\rfloor
\quad \quad
\codeinline{oz}{Z} \geq \underline{\codeinline{oz}{X}} *\overline{\codeinline{oz}{Y}} - \overline{\codeinline{oz}{A}}
\quad \quad
\codeinline{oz}{A} \geq \underline{\codeinline{oz}{X}} *\overline{\codeinline{oz}{Y}} - \overline{\codeinline{oz}{Z}}" src="latex70.png"></P><P>The propagator ceases to exist if <IMG alt="3*\overline{\codeinline{oz}{X}}*\overline{\codeinline{oz}{Y}} -
\underline{\codeinline{oz}{Z}} \leq \underline{\codeinline{oz}{A}}" src="latex71.png"> holds. </P></DD><DT><CODE><SPAN class="string">'>=:'</SPAN></CODE></DT><DD><P>This case can be reduced to <CODE><SPAN class="string">'=<:'</SPAN></CODE> due to the observation that </P><P><IMG alt="{\tt I}_1*{\tt D}_{11}*\ldots*{\tt D}_{1k_1}+\ldots+{\tt I}_n*{\tt D}_{n1}*\ldots*{\tt D}_{nk_n}+(-1)*{\tt D}_{(n+1)1}\;\leq\;0" src="latex72.png"></P><P>is equivalent to </P><P><IMG alt="(-{\tt I}_1)*{\tt D}_{11}*\ldots*{\tt D}_{1k_1}+\ldots+(-{\tt I}_n)*{\tt D}_{n1}*\ldots*{\tt D}_{nk_n}+1*{\tt D}_{(n+1)1}\;\geq\;0" src="latex73.png"></P><P>Alternatively, <IMG alt="\underline{\mbox{\mbox{\sl RHS}}_k}" src="latex44.png"> can be used for the definition. </P></DD><DT><CODE><SPAN class="string">'<:'</SPAN></CODE></DT><DD><P>Analogous to <CODE><SPAN class="string">'=<:'</SPAN></CODE></P></DD><DT><CODE><SPAN class="string">'>:'</SPAN></CODE></DT><DD><P>Analogous to <CODE><SPAN class="string">'>=:'</SPAN></CODE></P></DD><DT><CODE><SPAN class="string">'=:'</SPAN></CODE></DT><DD><P>In this case, the operational semantics is defined by conjunction of the formulas given for <CODE><SPAN class="string">'=<:'</SPAN></CODE> and <CODE><SPAN class="string">'>=:'</SPAN></CODE>.</P></DD><DT><CODE><SPAN class="string">'\\=:'</SPAN></CODE></DT><DD><P>In this case, the propagator waits until at most one non-determined variable is left, say <IMG alt="D_{kl}" src="latex74.png">. Then, <IMG alt="{\mbox{\sl RHS}}_k" src="latex42.png"> denotes a unique integer, and if </P><P><IMG alt="\frac{{\mbox{\sl RHS}}_k}{{\tt I}_k * \prod_{j=1,
j\neq l}^{m_k} {{\tt D}}_{kj}} " src="latex75.png"></P><P> denotes an integer value, this value is discarded from the domain of <IMG alt="{\tt D}_{kl}" src="latex76.png">.</P></DD></DL><P> Coreferences are not exploited for nonlinear generic constraints. The only exception is the expression </P><BLOCKQUOTE class="code"><CODE>X <SPAN class="keyword">*</SPAN> X <SPAN class="keyword">=:</SPAN> Y</CODE></BLOCKQUOTE><P> which has the same operational semantics as <CODE>{FD<SPAN class="keyword">.</SPAN>times X X Y}</CODE> (but note that the occurring variables are not automatically constrained to finite domain integers). </P></DD><DT><A name="label174"></A> <CODE>sumAC</CODE></DT><DD><BLOCKQUOTE class="synopsis"><P></P><BLOCKQUOTE class="code"><CODE>{FD<SPAN class="keyword">.</SPAN>sumAC </CODE><CODE>+<I>Iv</I></CODE><CODE> </CODE><CODE>*<I>Dv</I></CODE><CODE> </CODE><CODE>+<I>A</I></CODE><CODE> </CODE><CODE>*<I>D</I></CODE><CODE>}</CODE></BLOCKQUOTE><P></P></BLOCKQUOTE></DD><DD><P>creates a propagator for the absolute value of the scalar product of the vectors <CODE><I>Iv</I></CODE> and <CODE><I>Dv</I></CODE>: </P><P><IMG alt="|{\tt Iv} * {\tt Dv}| = |{\tt I}_1*{\tt D}_1 + \ldots +
{\tt I}_n*{\tt D}_n|\;\sim_{{\tt A}}\;{\tt D}" src="latex77.png"></P><P> The operational semantics is as follows. If <CODE><I>A</I></CODE> is <CODE><SPAN class="string">'<:'</SPAN></CODE>, <CODE><SPAN class="string">'=<:'</SPAN></CODE> or <CODE><SPAN class="string">'\\=:'</SPAN></CODE>, the following definition holds. </P><P><IMG alt=" {\tt Iv} * {\tt Dv} \sim_{{\tt A}} D \;\wedge\; (-{\tt Iv})*{\tt Dv}
\sim_{{\tt A}} D" src="latex78.png"></P><P> If <CODE><I>A</I></CODE> is <CODE><SPAN class="string">'>:'</SPAN></CODE>, <CODE><SPAN class="string">'>=:'</SPAN></CODE> or <CODE><SPAN class="string">'=:'</SPAN></CODE>, the following definition holds. </P><P><IMG alt="{\tt Iv} * {\tt Dv} \sim_{{\tt A}} D \;\vee\; (-{\tt Iv})*{\tt Dv}
\sim_{{\tt A}} D" src="latex79.png"></P><P>where the disjunction is realized by constructive disjunction. </P></DD><DT><A name="label176"></A> <CODE>sumACN</CODE></DT><DD><BLOCKQUOTE class="synopsis"><P></P><BLOCKQUOTE class="code"><CODE>{FD<SPAN class="keyword">.</SPAN>sumACN </CODE><CODE>+<I>Iv</I></CODE><CODE> </CODE><CODE>*<I>Dvv</I></CODE><CODE> </CODE><CODE>+<I>A</I></CODE><CODE> </CODE><CODE>*<I>D</I></CODE><CODE>}</CODE></BLOCKQUOTE><P></P></BLOCKQUOTE></DD><DD><P>creates a propagator for </P><P><IMG alt="|{\tt I}_1*{\tt D}_{11}*\ldots*{\tt D}_{1k_1}+\ldots+{\tt I}_n*{\tt D}_{n1}*\ldots*{\tt D}_{nk_n}|\;\sim_{{\tt A}}\;{\tt D}" src="latex80.png"></P><P></P><P>The operational semantics is defined analogously to <CODE>FD<SPAN class="keyword">.</SPAN>sumAC</CODE>. </P></DD><DT><A name="label178"></A> <CODE>sumD</CODE></DT><DD><BLOCKQUOTE class="synopsis"><P></P><BLOCKQUOTE class="code"><CODE>{FD<SPAN class="keyword">.</SPAN>sumD </CODE><CODE>*<I>Dv</I></CODE><CODE> </CODE><CODE>+<I>A</I></CODE><CODE> </CODE><CODE>*<I>D</I></CODE><CODE>}</CODE></BLOCKQUOTE><P></P></BLOCKQUOTE></DD><DD><P>creates a propagator analogous to <CODE>FD<SPAN class="keyword">.</SPAN>sum</CODE> but performs <EM>domain-consistent</EM> propagation. Note that only equality (<CODE><I>A</I></CODE> is <CODE><SPAN class="string">'=:'</SPAN></CODE>) and disequality (<CODE><I>A</I></CODE> is <CODE><SPAN class="string">'\\=:'</SPAN></CODE>) are supported, as for inequalities domain and bounds propagation are equivalent. </P></DD><DT><A name="label180"></A> <CODE>sumCD</CODE></DT><DD><BLOCKQUOTE class="synopsis"><P></P><BLOCKQUOTE class="code"><CODE>{FD<SPAN class="keyword">.</SPAN>sumCD </CODE><CODE>+<I>Iv</I></CODE><CODE> </CODE><CODE>*<I>Dv</I></CODE><CODE> </CODE><CODE>+<I>A</I></CODE><CODE> </CODE><CODE>*<I>D</I></CODE><CODE>}</CODE></BLOCKQUOTE><P></P></BLOCKQUOTE></DD><DD><P>creates a propagator analogous to <CODE>FD<SPAN class="keyword">.</SPAN>sumC</CODE> but performs <EM>domain-consistent</EM> propagation. Note that only equality (<CODE><I>A</I></CODE> is <CODE><SPAN class="string">'=:'</SPAN></CODE>) and disequality (<CODE><I>A</I></CODE> is <CODE><SPAN class="string">'\\=:'</SPAN></CODE>) are supported, as for inequalities domain and bounds propagation are equivalent.</P></DD></DL><P></P></DIV><TABLE align="center" border="0" cellpadding="6" cellspacing="6" class="nav"><TR bgcolor="#DDDDDD"><TD><A href="node20.html#section.fd.watching"><< Prev</A></TD><TD><A href="node14.html">- Up -</A></TD><TD><A href="node22.html#section.fd.nonlinear">Next >></A></TD></TR></TABLE><HR><ADDRESS><A href="http://www.ps.uni-sb.de/~duchier/">Denys Duchier</A>, <A href="http://www.ps.uni-sb.de/~kornstae/">Leif Kornstaedt</A>, <A href="http://www.ps.uni-sb.de/~homik/">Martin Homik</A>, <A href="http://www.ps.uni-sb.de/~tmueller/">Tobias Müller</A>, <A href="http://www.ps.uni-sb.de/~schulte/">Christian Schulte</A> and <A href="http://www.info.ucl.ac.be/~pvr">Peter Van Roy</A><BR><SPAN class="version">Version 1.4.0 (20110908185330)</SPAN></ADDRESS></BODY></HTML>
|