This file is indexed.

/usr/share/mozart/doc/system/node25.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
<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">
<HTML><HEAD><TITLE>5.11 Miscellaneous 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="node24.html#section.fd.reified">&lt;&lt; Prev</A></TD><TD><A href="node14.html">- Up -</A></TD><TD><A href="node26.html#section.fd.distribution">Next &gt;&gt;</A></TD></TR></TABLE><DIV id="section.fd.misc"><H2><A name="section.fd.misc">5.11 Miscellaneous Propagators</A></H2><P></P><DL><DT><A name="label232"></A> <CODE>plus</CODE></DT><DD><BLOCKQUOTE class="synopsis"><P></P><BLOCKQUOTE class="code"><CODE>{FD<SPAN class="keyword">.</SPAN>plus&nbsp;</CODE><CODE>$<I>D1</I></CODE><CODE>&nbsp;</CODE><CODE>$<I>D2</I></CODE><CODE>&nbsp;</CODE><CODE>$<I>D3</I></CODE><CODE>}</CODE></BLOCKQUOTE><P></P></BLOCKQUOTE></DD><DD><P><CODE><I>D3</I></CODE> is the sum of <CODE><I>D1</I></CODE> and <CODE><I>D2</I></CODE>. The propagator constrains its arguments as <CODE><I>D1</I></CODE><CODE><SPAN class="keyword">+</SPAN></CODE><CODE><I>D2</I></CODE><CODE><SPAN class="keyword">=:</SPAN></CODE><CODE><I>D3</I></CODE>. </P></DD><DT><A name="label234"></A> <CODE>plusD</CODE></DT><DD><BLOCKQUOTE class="synopsis"><P></P><BLOCKQUOTE class="code"><CODE>{FD<SPAN class="keyword">.</SPAN>plusD&nbsp;</CODE><CODE>$<I>D1</I></CODE><CODE>&nbsp;</CODE><CODE>$<I>D2</I></CODE><CODE>&nbsp;</CODE><CODE>$<I>D3</I></CODE><CODE>}</CODE></BLOCKQUOTE><P></P></BLOCKQUOTE></DD><DD><P><CODE><I>D3</I></CODE> is the sum of <CODE><I>D1</I></CODE> and <CODE><I>D2</I></CODE>. The propagator constrains its arguments as <CODE><I>D1</I></CODE><CODE><SPAN class="keyword">+</SPAN></CODE><CODE><I>D2</I></CODE><CODE><SPAN class="keyword">=:</SPAN></CODE><CODE><I>D3</I></CODE>.</P><P>Does domain propagation, which can be very expensive. </P></DD><DT><A name="label236"></A> <CODE>minus</CODE></DT><DD><BLOCKQUOTE class="synopsis"><P></P><BLOCKQUOTE class="code"><CODE>{FD<SPAN class="keyword">.</SPAN>minus&nbsp;</CODE><CODE>$<I>D1</I></CODE><CODE>&nbsp;</CODE><CODE>$<I>D2</I></CODE><CODE>&nbsp;</CODE><CODE>$<I>D3</I></CODE><CODE>}</CODE></BLOCKQUOTE><P></P></BLOCKQUOTE></DD><DD><P><CODE><I>D3</I></CODE> is the difference between <CODE><I>D1</I></CODE> and <CODE><I>D2</I></CODE>. The propagator constrains its arguments as <CODE><I>D1</I></CODE><CODE><SPAN class="keyword">-</SPAN></CODE><CODE><I>D2</I></CODE><CODE><SPAN class="keyword">=:</SPAN></CODE><CODE><I>D3</I></CODE>. </P></DD><DT><A name="label238"></A> <CODE>minusD</CODE></DT><DD><BLOCKQUOTE class="synopsis"><P></P><BLOCKQUOTE class="code"><CODE>{FD<SPAN class="keyword">.</SPAN>minusD&nbsp;</CODE><CODE>$<I>D1</I></CODE><CODE>&nbsp;</CODE><CODE>$<I>D2</I></CODE><CODE>&nbsp;</CODE><CODE>$<I>D3</I></CODE><CODE>}</CODE></BLOCKQUOTE><P></P></BLOCKQUOTE></DD><DD><P><CODE><I>D3</I></CODE> is the difference between <CODE><I>D1</I></CODE> and <CODE><I>D2</I></CODE>. The propagator constrains its arguments as <CODE><I>D1</I></CODE><CODE><SPAN class="keyword">-</SPAN></CODE><CODE><I>D2</I></CODE><CODE><SPAN class="keyword">=:</SPAN></CODE><CODE><I>D3</I></CODE>.</P><P>Does domain propagation, which can be very expensive. </P></DD><DT><A name="label240"></A> <CODE>times</CODE></DT><DD><BLOCKQUOTE class="synopsis"><P></P><BLOCKQUOTE class="code"><CODE>{FD<SPAN class="keyword">.</SPAN>times&nbsp;</CODE><CODE>$<I>D1</I></CODE><CODE>&nbsp;</CODE><CODE>$<I>D2</I></CODE><CODE>&nbsp;</CODE><CODE>$<I>D3</I></CODE><CODE>}</CODE></BLOCKQUOTE><P></P></BLOCKQUOTE></DD><DD><P><CODE><I>D3</I></CODE> is the product of <CODE><I>D1</I></CODE> and <CODE><I>D2</I></CODE>. Coreferences are exploited. If the store entails <CODE>D1&nbsp;=&nbsp;D3</CODE>, the propagator ceases to exist and the constraint <CODE>D2=1</CODE> is imposed. If the store entails <CODE>D2&nbsp;=&nbsp;D3</CODE>, the propagator ceases to exist and the constraint <CODE>D1=1</CODE> is imposed. If the store entails <CODE>D1&nbsp;=&nbsp;D2</CODE>, the propagator ceases to exist and a propagator is imposed instead, which constrains the variables <CODE>D1</CODE> and <CODE>D2</CODE> as follows. </P><P><IMG alt="\underline{{\tt D1}}^2 \leq {\tt D3} \leq \overline{{\tt D1}}^2 \quad\quad
\lceil \sqrt{\underline{{\tt D3}}} \rceil \leq {\tt D1} \leq \lfloor
\sqrt{\overline{{\tt D3}}} \rfloor" src="latex94.png"></P><P>For notation see&nbsp;<A href="node21.html#section.fd.arithmetic">Section&nbsp;5.7</A>n. </P></DD><DT><A name="label242"></A> <CODE>timesD</CODE></DT><DD><BLOCKQUOTE class="synopsis"><P></P><BLOCKQUOTE class="code"><CODE>{FD<SPAN class="keyword">.</SPAN>timesD&nbsp;</CODE><CODE>$<I>D1</I></CODE><CODE>&nbsp;</CODE><CODE>$<I>D2</I></CODE><CODE>&nbsp;</CODE><CODE>$<I>D3</I></CODE><CODE>}</CODE></BLOCKQUOTE><P></P></BLOCKQUOTE></DD><DD><P><CODE><I>D3</I></CODE> is the product of <CODE><I>D1</I></CODE> and <CODE><I>D2</I></CODE>. </P><P>Does domain propagation, which can be very expensive. </P></DD><DT><A name="label244"></A> <CODE>power</CODE></DT><DD><BLOCKQUOTE class="synopsis"><P></P><BLOCKQUOTE class="code"><CODE>{FD<SPAN class="keyword">.</SPAN>power&nbsp;</CODE><CODE>$<I>D1</I></CODE><CODE>&nbsp;</CODE><CODE>+<I>I</I></CODE><CODE>&nbsp;</CODE><CODE>$<I>D2</I></CODE><CODE>}</CODE></BLOCKQUOTE><P></P></BLOCKQUOTE></DD><DD><P><CODE>$<I>D2</I></CODE> is the result of <CODE><I>D1</I></CODE> raised to the power of <CODE><I>I</I></CODE>, i.&nbsp;e. <IMG alt="{\tt D1}^{{\tt I}} = {\tt D2}" src="latex95.png">. The propagator constrains the variables <CODE>D1</CODE> and <CODE>D2</CODE> as follows. </P><P><IMG alt="\underline{{\tt D1}}^{{\tt I}} \leq {\tt D2} \leq \overline{{\tt D1}}^{{\tt I}}
\quad\quad 
\lceil \sqrt[{\tt D2}]{\underline{{\tt D1}}} \rceil \leq {\tt D2} \leq \lfloor
\sqrt[{\tt D2}]{\overline{{\tt D1}}} \rfloor" src="latex96.png"></P><P>For notation see &nbsp;<A href="node21.html#section.fd.arithmetic">Section&nbsp;5.7</A>. </P></DD><DT><A name="label246"></A> <CODE>divI</CODE></DT><DD><BLOCKQUOTE class="synopsis"><P></P><BLOCKQUOTE class="code"><CODE>{FD<SPAN class="keyword">.</SPAN>divI&nbsp;</CODE><CODE>$<I>D1</I></CODE><CODE>&nbsp;</CODE><CODE>+<I>I</I></CODE><CODE>&nbsp;</CODE><CODE>$<I>D2</I></CODE><CODE>}</CODE></BLOCKQUOTE><P></P></BLOCKQUOTE></DD><DD><P><CODE><I>D2</I></CODE> is the result of the integer division of <CODE>D1</CODE> by <CODE>I</CODE>. </P><P>A domain bound is discarded from the domain of one variable, if there is no value between the lower and upper bound of the domain of the other variable, such that the constraint holds. Additionally, if <IMG alt="{\tt D1}={\tt D2}" src="latex97.png">, the propagator is replaced by <CODE>I=1</CODE>. </P></DD><DT><CODE>modI</CODE></DT><DD><BLOCKQUOTE class="synopsis"><P><A name="label248"></A> </P><BLOCKQUOTE class="code"><CODE>{FD<SPAN class="keyword">.</SPAN>modI&nbsp;</CODE><CODE>$<I>D1</I></CODE><CODE>&nbsp;</CODE><CODE>+<I>I</I></CODE><CODE>&nbsp;</CODE><CODE>$<I>D2</I></CODE><CODE>}</CODE></BLOCKQUOTE><P></P></BLOCKQUOTE></DD><DD><P><CODE><I>D2</I></CODE> is the result of <CODE>D1</CODE> modulus <CODE>I</CODE>. </P><P>A domain bound is discarded from the domain of one variable, if there is no value between the lower and upper bound of the domain of the other variable, such that the constraint holds. Additionally, if <IMG alt="{\tt D1}={\tt D2}" src="latex97.png">, the propagator is replaced by <CODE>D1<SPAN class="keyword">&lt;:</SPAN>I</CODE>. If the current upper bound of <CODE><I>D1</I></CODE> is less than <CODE><I>I</I></CODE>, the propagator is replaced by <CODE>D1=D2</CODE>. </P></DD><DT><A name="label250"></A> <CODE>divD</CODE></DT><DD><BLOCKQUOTE class="synopsis"><P></P><BLOCKQUOTE class="code"><CODE>{FD<SPAN class="keyword">.</SPAN>divD&nbsp;</CODE><CODE>$<I>D1</I></CODE><CODE>&nbsp;</CODE><CODE>+<I>I</I></CODE><CODE>&nbsp;</CODE><CODE>$<I>D2</I></CODE><CODE>}</CODE></BLOCKQUOTE><P></P></BLOCKQUOTE></DD><DD><P><CODE><I>D2</I></CODE> is the result of the integer division of <CODE>D1</CODE> by <CODE>I</CODE>. </P><P>Does domain propagation, which can be very expensive. </P></DD><DT><A name="label252"></A> <CODE>modD</CODE></DT><DD><BLOCKQUOTE class="synopsis"><P></P><BLOCKQUOTE class="code"><CODE>{FD<SPAN class="keyword">.</SPAN>modD&nbsp;</CODE><CODE>$<I>D1</I></CODE><CODE>&nbsp;</CODE><CODE>+<I>I</I></CODE><CODE>&nbsp;</CODE><CODE>$<I>D2</I></CODE><CODE>}</CODE></BLOCKQUOTE><P></P></BLOCKQUOTE></DD><DD><P><CODE><I>D2</I></CODE> is the result of <CODE>D1</CODE> modulus <CODE>I</CODE>. </P><P>Does domain propagation, which can be very expensive. </P></DD><DT><A name="label254"></A> <CODE>max</CODE></DT><DD><BLOCKQUOTE class="synopsis"><P></P><BLOCKQUOTE class="code"><CODE>{FD<SPAN class="keyword">.</SPAN>max&nbsp;</CODE><CODE>$<I>D1</I></CODE><CODE>&nbsp;</CODE><CODE>$<I>D2</I></CODE><CODE>&nbsp;</CODE><CODE>$<I>D3</I></CODE><CODE>}</CODE></BLOCKQUOTE><P></P></BLOCKQUOTE></DD><DD><P><CODE><I>D3</I></CODE> is the maximum of <CODE><I>D1</I></CODE> and <CODE><I>D2</I></CODE>. </P><P>Its operational semantics is defined through </P><BLOCKQUOTE class="code"><CODE>D3<SPAN class="keyword">&gt;=:</SPAN>D1&nbsp;&nbsp;&nbsp;D3<SPAN class="keyword">&gt;=:</SPAN>D2<BR>condis&nbsp;D3<SPAN class="keyword">=&lt;:</SPAN>D1<BR><SPAN class="keyword">[]</SPAN>&nbsp;D3<SPAN class="keyword">=&lt;:</SPAN>D2<BR><SPAN class="keyword">end</SPAN>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<BR><SPAN class="keyword">if</SPAN>&nbsp;D1=D2&nbsp;<SPAN class="keyword">then</SPAN>&nbsp;D3=D1<BR><SPAN class="keyword">else</SPAN>&nbsp;<SPAN class="keyword">skip</SPAN>&nbsp;<BR><SPAN class="keyword">end</SPAN>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;</CODE></BLOCKQUOTE><P> </P></DD><DT><A name="label256"></A> <CODE>min</CODE></DT><DD><BLOCKQUOTE class="synopsis"><P></P><BLOCKQUOTE class="code"><CODE>{FD<SPAN class="keyword">.</SPAN>min&nbsp;</CODE><CODE>$<I>D1</I></CODE><CODE>&nbsp;</CODE><CODE>$<I>D2</I></CODE><CODE>&nbsp;</CODE><CODE>$<I>D3</I></CODE><CODE>}</CODE></BLOCKQUOTE><P></P></BLOCKQUOTE></DD><DD><P><CODE><I>D3</I></CODE> is the minimum of <CODE><I>D1</I></CODE> and <CODE><I>D2</I></CODE>. Its operational semantics is defined through </P><BLOCKQUOTE class="code"><CODE>D3<SPAN class="keyword">=&lt;:</SPAN>D1&nbsp;&nbsp;&nbsp;D3<SPAN class="keyword">=&lt;:</SPAN>D2<BR>condis&nbsp;D3<SPAN class="keyword">&gt;=:</SPAN>D1<BR><SPAN class="keyword">[]</SPAN>&nbsp;D3<SPAN class="keyword">&gt;=:</SPAN>D2<BR><SPAN class="keyword">end</SPAN>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<BR><SPAN class="keyword">if</SPAN>&nbsp;D1=D2&nbsp;<SPAN class="keyword">then</SPAN>&nbsp;D3=D1<BR><SPAN class="keyword">else</SPAN>&nbsp;<SPAN class="keyword">skip</SPAN>&nbsp;<BR><SPAN class="keyword">end</SPAN>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;</CODE></BLOCKQUOTE><P> </P></DD><DT><A name="label258"></A> <CODE>distance</CODE></DT><DD id="page.distance"><BLOCKQUOTE class="synopsis"><P></P><BLOCKQUOTE class="code"><CODE>{FD<SPAN class="keyword">.</SPAN>distance&nbsp;</CODE><CODE>*<I>D1</I></CODE><CODE>&nbsp;</CODE><CODE>*<I>D2</I></CODE><CODE>&nbsp;</CODE><CODE>+<I>A</I></CODE><CODE>&nbsp;</CODE><CODE>*<I>D3</I></CODE><CODE>}</CODE></BLOCKQUOTE><P></P></BLOCKQUOTE></DD><DD><P>creates a propagator for <IMG alt="|~{\tt D1}-{\tt D2}~|\;\sim_{{\tt A}}\;{\tt D3}" src="latex98.png">. May cut holes into domains. For example, </P><BLOCKQUOTE class="code"><CODE>{FD<SPAN class="keyword">.</SPAN>dom&nbsp;0<SPAN class="keyword">#</SPAN>10&nbsp;[X&nbsp;Y]}<BR>{FD<SPAN class="keyword">.</SPAN>distance&nbsp;X&nbsp;Y&nbsp;<SPAN class="string">'&gt;:'</SPAN>&nbsp;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">.</P><P>The propagator is equivalent to <CODE>{FD<SPAN class="keyword">.</SPAN>sumAC&nbsp;[1&nbsp;<SPAN class="keyword">~</SPAN>1]&nbsp;[D1&nbsp;D2]&nbsp;A&nbsp;D3}</CODE> but is more efficient. </P></DD><DT><A name="label260"></A> <CODE>less</CODE></DT><DD><BLOCKQUOTE class="synopsis"><P></P><BLOCKQUOTE class="code"><CODE>{FD<SPAN class="keyword">.</SPAN>less&nbsp;</CODE><CODE>*<I>D1</I></CODE><CODE>&nbsp;</CODE><CODE>*<I>D2</I></CODE><CODE>}</CODE></BLOCKQUOTE><P></P></BLOCKQUOTE></DD><DD><P>Equivalent to <CODE><I>D1</I></CODE><CODE><SPAN class="keyword">&lt;:</SPAN></CODE><CODE><I>D2</I></CODE>. </P></DD><DT><A name="label262"></A> <CODE>lesseq</CODE></DT><DD><BLOCKQUOTE class="synopsis"><P></P><BLOCKQUOTE class="code"><CODE>{FD<SPAN class="keyword">.</SPAN>lesseq&nbsp;</CODE><CODE>*<I>D1</I></CODE><CODE>&nbsp;</CODE><CODE>*<I>D2</I></CODE><CODE>}</CODE></BLOCKQUOTE><P></P></BLOCKQUOTE></DD><DD><P>Equivalent to <CODE><I>D1</I></CODE> <CODE><SPAN class="keyword">=&lt;:</SPAN></CODE> <CODE><I>D2</I></CODE>. </P></DD><DT><A name="label264"></A> <CODE>greater</CODE></DT><DD><BLOCKQUOTE class="synopsis"><P></P><BLOCKQUOTE class="code"><CODE>{FD<SPAN class="keyword">.</SPAN>greater&nbsp;</CODE><CODE>*<I>D1</I></CODE><CODE>&nbsp;</CODE><CODE>*<I>D2</I></CODE><CODE>}</CODE></BLOCKQUOTE><P></P></BLOCKQUOTE></DD><DD><P>Equivalent to <CODE><I>D1</I></CODE><CODE><SPAN class="keyword">&gt;:</SPAN></CODE><CODE><I>D2</I></CODE>. </P></DD><DT><A name="label266"></A> <CODE>greatereq</CODE></DT><DD><BLOCKQUOTE class="synopsis"><P></P><BLOCKQUOTE class="code"><CODE>{FD<SPAN class="keyword">.</SPAN>greatereq&nbsp;</CODE><CODE>*<I>D1</I></CODE><CODE>&nbsp;</CODE><CODE>*<I>D2</I></CODE><CODE>}</CODE></BLOCKQUOTE><P></P></BLOCKQUOTE></DD><DD><P>Equivalent to <CODE><I>D1</I></CODE><CODE><SPAN class="keyword">&gt;=:</SPAN></CODE><CODE><I>D2</I></CODE>. </P></DD><DT id="ref_disjoint"><A name="label268"></A> <CODE>disjoint</CODE></DT><DD><BLOCKQUOTE class="synopsis"><P></P><BLOCKQUOTE class="code"><CODE>{FD<SPAN class="keyword">.</SPAN>disjoint&nbsp;</CODE><CODE>*<I>D1</I></CODE><CODE>&nbsp;</CODE><CODE>+<I>I1</I></CODE><CODE>&nbsp;</CODE><CODE>*<I>D2</I></CODE><CODE>&nbsp;</CODE><CODE>+<I>I2</I></CODE><CODE>}</CODE></BLOCKQUOTE><P></P></BLOCKQUOTE></DD><DD><P>creates a propagator for <IMG alt="{\tt D1}+{\tt I1}\leq{\tt D2} \;\vee\; {\tt D2}+{\tt I2}\leq{\tt D1}" src="latex99.png">. May cut holes into domains. For example, </P><BLOCKQUOTE class="code"><CODE>{FD<SPAN class="keyword">.</SPAN>dom&nbsp;0<SPAN class="keyword">#</SPAN>10&nbsp;[X&nbsp;Y]}<BR>{FD<SPAN class="keyword">.</SPAN>disjoint&nbsp;X&nbsp;9&nbsp;Y&nbsp;9}</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">.</P><P>Its operational semantics is defined through </P><BLOCKQUOTE class="code"><CODE>condis&nbsp;D1&nbsp;<SPAN class="keyword">+</SPAN>&nbsp;I1&nbsp;<SPAN class="keyword">=&lt;:</SPAN>&nbsp;D2<BR><SPAN class="keyword">[]</SPAN>&nbsp;D2&nbsp;<SPAN class="keyword">+</SPAN>&nbsp;I2&nbsp;<SPAN class="keyword">=&lt;:</SPAN>&nbsp;D1<BR><SPAN class="keyword">end</SPAN></CODE></BLOCKQUOTE><P> </P></DD><DT><A name="label270"></A> <CODE>disjointC</CODE></DT><DD><BLOCKQUOTE class="synopsis"><P></P><BLOCKQUOTE class="code"><CODE>{FD<SPAN class="keyword">.</SPAN>disjointC&nbsp;</CODE><CODE>*<I>D1</I></CODE><CODE>&nbsp;</CODE><CODE>+<I>I1</I></CODE><CODE>&nbsp;</CODE><CODE>*<I>D2</I></CODE><CODE>&nbsp;</CODE><CODE>+<I>I2</I></CODE><CODE>&nbsp;</CODE><CODE><I>D3</I></CODE><CODE>}</CODE></BLOCKQUOTE><P></P></BLOCKQUOTE></DD><DD><P>creates a propagator for </P><P><IMG alt="(({\tt D1}+{\tt I1}\leq{\tt D2} \wedge {\tt D3}=0) \;\vee\;({\tt D2}+{\tt I2}\leq{\tt D1} \wedge {\tt D3}=1)) \;\wedge\; ({\tt D3}\in\{0,1\})." src="latex100.png"></P><P>Its operational semantics is defined through </P><BLOCKQUOTE class="code"><CODE>condis&nbsp;D1&nbsp;<SPAN class="keyword">+</SPAN>&nbsp;I1&nbsp;<SPAN class="keyword">=&lt;:</SPAN>&nbsp;D2&nbsp;&nbsp;&nbsp;&nbsp;<BR>&nbsp;&nbsp;&nbsp;D3&nbsp;<SPAN class="keyword">=:</SPAN>&nbsp;0<BR><SPAN class="keyword">[]</SPAN>&nbsp;D2&nbsp;<SPAN class="keyword">+</SPAN>&nbsp;I2&nbsp;<SPAN class="keyword">=&lt;:</SPAN>&nbsp;D1<BR>&nbsp;&nbsp;&nbsp;D3&nbsp;<SPAN class="keyword">=:</SPAN>&nbsp;1<BR><SPAN class="keyword">end</SPAN></CODE></BLOCKQUOTE><P> </P></DD><DT id="ref_tasksoverlap"><A name="label272"></A> <CODE>tasksOverlap</CODE></DT><DD><BLOCKQUOTE class="synopsis"><P></P><BLOCKQUOTE class="code"><CODE>{FD<SPAN class="keyword">.</SPAN>tasksOverlap&nbsp;</CODE><CODE>*<I>D1</I></CODE><CODE>&nbsp;</CODE><CODE>+<I>I1</I></CODE><CODE>&nbsp;</CODE><CODE>*<I>D2</I></CODE><CODE>&nbsp;</CODE><CODE>+<I>I2</I></CODE><CODE>&nbsp;</CODE><CODE><I>D3</I></CODE><CODE>}</CODE></BLOCKQUOTE><P></P></BLOCKQUOTE></DD><DD><P>creates a propagator for </P><P><IMG alt="(({\tt D1}+{\tt I1}>{\tt D2} \;\wedge\; {\tt D2}+{\tt I2}>{\tt D1} \;\wedge \; {\tt D3}=1) \;\vee\; ({\tt D1}+{\tt I1}\leq{\tt D2} \;\wedge\; {\tt D3}=0) \;\vee\;({\tt D2}+{\tt I2}\leq{\tt D1} \;\wedge\; {\tt D3}=0)) \;\wedge\; ({\tt D3}\in\{0,1\})" src="latex101.png">. </P><P>Its operational semantics is defined through </P><BLOCKQUOTE class="code"><CODE>condis<BR>&nbsp;&nbsp;&nbsp;D1&nbsp;<SPAN class="keyword">+</SPAN>&nbsp;I1&nbsp;<SPAN class="keyword">&gt;:</SPAN>&nbsp;D2&nbsp;&nbsp;&nbsp;&nbsp;<BR>&nbsp;&nbsp;&nbsp;D2&nbsp;<SPAN class="keyword">+</SPAN>&nbsp;I2&nbsp;<SPAN class="keyword">&gt;:</SPAN>&nbsp;D1<BR>&nbsp;&nbsp;&nbsp;D3&nbsp;<SPAN class="keyword">=:</SPAN>&nbsp;1<BR><SPAN class="keyword">[]</SPAN>&nbsp;&nbsp;<BR>&nbsp;&nbsp;&nbsp;D1&nbsp;<SPAN class="keyword">+</SPAN>&nbsp;I1&nbsp;<SPAN class="keyword">=&lt;:</SPAN>&nbsp;D2&nbsp;&nbsp;&nbsp;&nbsp;<BR>&nbsp;&nbsp;&nbsp;D3&nbsp;<SPAN class="keyword">=:</SPAN>&nbsp;0<BR><SPAN class="keyword">[]</SPAN>&nbsp;&nbsp;<BR>&nbsp;&nbsp;&nbsp;D2&nbsp;<SPAN class="keyword">+</SPAN>&nbsp;I2&nbsp;<SPAN class="keyword">=&lt;:</SPAN>&nbsp;D1<BR>&nbsp;&nbsp;&nbsp;D3&nbsp;<SPAN class="keyword">=:</SPAN>&nbsp;0<BR><SPAN class="keyword">end</SPAN></CODE></BLOCKQUOTE><P></P></DD></DL><P> Note that the disjunction is <A href="node16.html#section.fd.condis">constructive</A>. Informally, in case <CODE>D3</CODE> is 0 the propagator behaves like <CODE>FD<SPAN class="keyword">.</SPAN>disjoint</CODE>, i.e., in context of task scheduling two tasks must not overlap. Otherwise, if <CODE>D3</CODE> is 1, the two tasks must overlap. This propagator is used in applications which shall be able to deal with overlapping tasks. </P></DIV><TABLE align="center" border="0" cellpadding="6" cellspacing="6" class="nav"><TR bgcolor="#DDDDDD"><TD><A href="node24.html#section.fd.reified">&lt;&lt; Prev</A></TD><TD><A href="node14.html">- Up -</A></TD><TD><A href="node26.html#section.fd.distribution">Next &gt;&gt;</A></TD></TR></TABLE><HR><ADDRESS><A href="http://www.ps.uni-sb.de/~duchier/">Denys&nbsp;Duchier</A>, <A href="http://www.ps.uni-sb.de/~kornstae/">Leif&nbsp;Kornstaedt</A>, <A href="http://www.ps.uni-sb.de/~homik/">Martin&nbsp;Homik</A>, <A href="http://www.ps.uni-sb.de/~tmueller/">Tobias&nbsp;Müller</A>, <A href="http://www.ps.uni-sb.de/~schulte/">Christian&nbsp;Schulte</A> and&nbsp;<A href="http://www.info.ucl.ac.be/~pvr">Peter&nbsp;Van Roy</A><BR><SPAN class="version">Version 1.4.0 (20110908185330)</SPAN></ADDRESS></BODY></HTML>