/usr/share/mozart/doc/system/node22.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 | <!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">
<HTML><HEAD><TITLE>5.8 Symbolic 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="node21.html#section.fd.arithmetic"><< Prev</A></TD><TD><A href="node14.html">- Up -</A></TD><TD><A href="node23.html#section.fd.bool">Next >></A></TD></TR></TABLE><DIV id="section.fd.nonlinear"><H2><A name="section.fd.nonlinear">5.8 Symbolic Propagators</A></H2><P>The following propagators do domain propagation or amplify the store by constraints <CODE>X<SPAN class="keyword">::</SPAN>Spec</CODE>, where <CODE>Spec</CODE> may also contain holes. </P><DL><DT><A name="label182"></A> <CODE>distinct</CODE></DT><DD><BLOCKQUOTE class="synopsis"><P></P><BLOCKQUOTE class="code"><CODE>{FD<SPAN class="keyword">.</SPAN>distinct </CODE><CODE>*<I>Dv</I></CODE><CODE>}</CODE></BLOCKQUOTE><P></P></BLOCKQUOTE></DD><DD><P>All elements in <CODE><I>Dv</I></CODE> are pairwise distinct. If one element becomes determined, the remaining elements are constrained to be different from it. If two variables become equal, the propagator fails, e. g. <CODE>{FD<SPAN class="keyword">.</SPAN>distinct [A A B]}</CODE> will fail even if <CODE>A</CODE> is not determined. </P></DD><DT><A name="label184"></A> <CODE>distinctB</CODE></DT><DD><BLOCKQUOTE class="synopsis"><P></P><BLOCKQUOTE class="code"><CODE>{FD<SPAN class="keyword">.</SPAN>distinctB </CODE><CODE>*<I>Dv</I></CODE><CODE>}</CODE></BLOCKQUOTE><P></P></BLOCKQUOTE></DD><DD><P>All elements in <CODE><I>Dv</I></CODE> are pairwise distinct. Uses bounds propagation, but does not use value propagation as <CODE>FD<SPAN class="keyword">.</SPAN>distinct</CODE>. Also fails, if two variables are equal. Currently uses the quadratic algorithm for propagation by Puget described in <A href="bib.html#puget.98">[Pug98]</A>. </P></DD><DT><A name="label186"></A> <CODE>distinctD</CODE></DT><DD><BLOCKQUOTE class="synopsis"><P></P><BLOCKQUOTE class="code"><CODE>{FD<SPAN class="keyword">.</SPAN>distinctD </CODE><CODE>*<I>Dv</I></CODE><CODE>}</CODE></BLOCKQUOTE><P></P></BLOCKQUOTE></DD><DD><P>All elements in <CODE><I>Dv</I></CODE> are pairwise distinct. Uses full domain propagation. Also fails, if two variables are equal. Is based on Régin's algorithm <A href="bib.html#regin.94">[Rég94]</A>. </P></DD><DT><A name="label188"></A> <CODE>distinctOffset</CODE></DT><DD><BLOCKQUOTE class="synopsis"><P></P><BLOCKQUOTE class="code"><CODE>{FD<SPAN class="keyword">.</SPAN>distinctOffset </CODE><CODE>*<I>Dv</I></CODE><CODE> </CODE><CODE>+<I>Iv</I></CODE><CODE>}</CODE></BLOCKQUOTE><P></P></BLOCKQUOTE></DD><DD><P>All sums <IMG alt="{\tt D}_i+{\tt I}_i" src="latex81.png"> are pairwise distinct, i. e. for all <IMG alt="i\neq j" src="latex82.png"> holds <IMG alt="{\tt D}_i+{I}_i \neq {\tt D}_j + {\tt I}_j" src="latex83.png">. If one <IMG alt="{\tt D}_i" src="latex84.png"> becomes determined, the remaining elements <IMG alt="{\tt D}_j" src="latex85.png"> are constrained to be different from <IMG alt="{\tt D}_i+{\tt I}_i-{\tt I}_j" src="latex86.png">. </P></DD><DT><A name="label190"></A> <CODE>distinct2</CODE></DT><DD><BLOCKQUOTE class="synopsis"><P></P><BLOCKQUOTE class="code"><CODE>{FD<SPAN class="keyword">.</SPAN>distinct2 </CODE><CODE>*<I>Dv1</I></CODE><CODE> </CODE><CODE>+<I>Iv1</I></CODE><CODE> </CODE><CODE>*<I>Dv2</I></CODE><CODE> </CODE><CODE>+<I>Iv2</I></CODE><CODE>}</CODE></BLOCKQUOTE><P></P></BLOCKQUOTE></DD><DD><P>Assume that all arguments are tuples of width <I>n</I>. Then the propagator's operational semantics is defined as follows. </P><BLOCKQUOTE class="code"><CODE><SPAN class="keyword">or</SPAN> Dv1<SPAN class="keyword">.</SPAN></CODE><CODE><I>i</I></CODE><CODE> <SPAN class="keyword">+</SPAN> IV1<SPAN class="keyword">.</SPAN></CODE><CODE><I>i</I></CODE><CODE> <SPAN class="keyword">=<:</SPAN> Dv1<SPAN class="keyword">.</SPAN></CODE><CODE><I>j</I></CODE><CODE> <BR><SPAN class="keyword">[]</SPAN> Dv1<SPAN class="keyword">.</SPAN></CODE><CODE><I>j</I></CODE><CODE> <SPAN class="keyword">+</SPAN> IV1<SPAN class="keyword">.</SPAN></CODE><CODE><I>j</I></CODE><CODE> <SPAN class="keyword">=<:</SPAN> Dv1<SPAN class="keyword">.</SPAN></CODE><CODE><I>i</I></CODE><CODE> <BR><SPAN class="keyword">[]</SPAN> Dv2<SPAN class="keyword">.</SPAN></CODE><CODE><I>i</I></CODE><CODE> <SPAN class="keyword">+</SPAN> IV2<SPAN class="keyword">.</SPAN></CODE><CODE><I>i</I></CODE><CODE> <SPAN class="keyword">=<:</SPAN> Dv2<SPAN class="keyword">.</SPAN></CODE><CODE><I>j</I></CODE><CODE> <BR><SPAN class="keyword">[]</SPAN> Dv2<SPAN class="keyword">.</SPAN></CODE><CODE><I>j</I></CODE><CODE> <SPAN class="keyword">+</SPAN> IV2<SPAN class="keyword">.</SPAN></CODE><CODE><I>j</I></CODE><CODE> <SPAN class="keyword">=<:</SPAN> Dv2<SPAN class="keyword">.</SPAN></CODE><CODE><I>i</I></CODE><CODE> <BR><SPAN class="keyword">end</SPAN></CODE></BLOCKQUOTE><P> This propagator may be used to express that a number of rectangles must not overlap in the two-dimensional space. In this case <CODE><I>Dv1</I></CODE> and <CODE><I>Dv2</I></CODE> may denote the x-coordinates and y-coordinates of the lower left corner of the rectangles, respectively. <CODE><I>Iv1</I></CODE> and <CODE><I>Iv2</I></CODE> may denote the widths and heights of the rectangles, respectively. </P></DD><DT><CODE>atMost</CODE><A name="label192"></A></DT><DD><BLOCKQUOTE class="synopsis"><P><CODE>{FD<SPAN class="keyword">.</SPAN>atMost </CODE><CODE>*<I>D</I></CODE><CODE> </CODE><CODE>*<I>Dv</I></CODE><CODE> </CODE><CODE>+<I>I</I></CODE><CODE>}</CODE></P></BLOCKQUOTE></DD><DT><CODE>atLeast</CODE><A name="label194"></A></DT><DD><BLOCKQUOTE class="synopsis"><P><CODE>{FD<SPAN class="keyword">.</SPAN>atLeast </CODE><CODE>*<I>D</I></CODE><CODE> </CODE><CODE>*<I>Dv</I></CODE><CODE> </CODE><CODE>+<I>I</I></CODE><CODE>}</CODE></P></BLOCKQUOTE></DD><DT><CODE>exactly</CODE><A name="label196"></A></DT><DD><BLOCKQUOTE class="synopsis"><P><CODE>{FD<SPAN class="keyword">.</SPAN>exactly </CODE><CODE>*<I>D</I></CODE><CODE> </CODE><CODE>*<I>Dv</I></CODE><CODE> </CODE><CODE>+<I>I</I></CODE><CODE>}</CODE></P></BLOCKQUOTE></DD><DD><P>At most, at least, exactly <CODE><I>D</I></CODE> elements of <CODE><I>Dv</I></CODE> are equal to <CODE><I>I</I></CODE>. The operational semantics is defined as follows. Let <CODE>VFoldL</CODE> be either <CODE>FoldL</CODE> or <CODE>Record<SPAN class="keyword">.</SPAN>foldL</CODE> depending on the type of <CODE><I>Dv</I></CODE> and </P><BLOCKQUOTE class="code"><CODE>S = {VFoldL Dv <SPAN class="keyword">fun</SPAN>{<SPAN class="functionname">$</SPAN> In D1} {FD<SPAN class="keyword">.</SPAN>plus In D1<SPAN class="keyword">=:</SPAN>I} <SPAN class="keyword">end</SPAN> 0}</CODE></BLOCKQUOTE><P> The propagator <CODE>FD<SPAN class="keyword">.</SPAN>atMost</CODE>, <CODE>FD<SPAN class="keyword">.</SPAN>atLeast</CODE> and <CODE>FD<SPAN class="keyword">.</SPAN>exactly</CODE> are defined by <CODE><I>D</I></CODE><CODE><SPAN class="keyword">>=:</SPAN>S</CODE>, <CODE><I>D</I></CODE><CODE><SPAN class="keyword">=<:</SPAN>S</CODE> and <CODE><I>D</I></CODE><CODE><SPAN class="keyword">=:</SPAN>S</CODE>, respectively. </P></DD><DT><A name="label198"></A> <CODE>element</CODE></DT><DD><BLOCKQUOTE class="synopsis"><P></P><BLOCKQUOTE class="code"><CODE>{FD<SPAN class="keyword">.</SPAN>element </CODE><CODE>*<I>D1</I></CODE><CODE> </CODE><CODE>+<I>Iv</I></CODE><CODE> </CODE><CODE>*<I>D2</I></CODE><CODE>}</CODE></BLOCKQUOTE><P></P></BLOCKQUOTE></DD><DD><P>The <CODE><I>D1</I></CODE>-th element of <CODE><I>Iv</I></CODE> is <CODE><I>D2</I></CODE>. </P><P>It propagates as follows. For each integer <I>i</I> in the domain of <CODE><I>D1</I></CODE>, the <I>i</I>-th element of <CODE><I>Iv</I></CODE> is in the domain of <CODE><I>D2</I></CODE>; and no other values. For each value <I>j</I> in the domain of <CODE><I>D2</I></CODE>, all positions where <I>j</I> occurs in <CODE><I>Is</I></CODE> are in the domain of <CODE><I>D1</I></CODE>; and no other values. For example, </P><BLOCKQUOTE class="code"><CODE>{FD<SPAN class="keyword">.</SPAN>int [1 3] X} {FD<SPAN class="keyword">.</SPAN>element X [5 6 7 8] Y}</CODE></BLOCKQUOTE><P> will constrain <CODE>Y</CODE> to <IMG alt="\{5,7\}" src="latex87.png">. <CODE><I>D1</I></CODE> is constrained to be greater than 0. </P></DD></DL><P></P></DIV><TABLE align="center" border="0" cellpadding="6" cellspacing="6" class="nav"><TR bgcolor="#DDDDDD"><TD><A href="node21.html#section.fd.arithmetic"><< Prev</A></TD><TD><A href="node14.html">- Up -</A></TD><TD><A href="node23.html#section.fd.bool">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>
|