/usr/share/mozart/doc/system/node24.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 | <!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">
<HTML><HEAD><TITLE>5.10 Reified Constraints</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="node23.html#section.fd.bool"><< Prev</A></TD><TD><A href="node14.html">- Up -</A></TD><TD><A href="node25.html#section.fd.misc">Next >></A></TD></TR></TABLE><DIV id="section.fd.reified"><H2><A name="section.fd.reified">5.10 Reified Constraints</A></H2><P>Reified constraints reflect the validity of a constraint <I>C</I> into a 0/1-valued finite domain integer. The propagator realizing a reified constraint is called the reification propagator. The reification propagators wait in the same way as their non-reified counterparts. All reification propagators constrain their last argument to a 0/1-valued finite domain integer. </P><P>Let <I>C</I> be a constraint and <I>P</I> the corresponding propagator. Reifying <I>C</I> into a 0/1-valued variable <CODE>D</CODE> is defined by</P><P><IMG alt="(C \leftrightarrow \codeinline{oz}{D}=1) \wedge \codeinline{oz}{D} \in \{0,1\}." src="latex91.png"></P><P>This is implemented by </P><BLOCKQUOTE class="code"><CODE>D<SPAN class="keyword">::</SPAN>0<SPAN class="keyword">#</SPAN>1 <BR><SPAN class="keyword">or</SPAN> </CODE><CODE><I>P</I></CODE><CODE> D=1<BR><SPAN class="keyword">[]</SPAN> P^N D=0<BR><SPAN class="keyword">end</SPAN></CODE></BLOCKQUOTE><P> Here, <IMG alt="P^N" src="latex92.png"> denotes the negation of <I>P</I> (i. e. a propagator for the negation of the denotational semantics of <I>P</I>).</P><P>If <I>P</I> is one of <CODE>{FD<SPAN class="keyword">.</SPAN>reified<SPAN class="keyword">.</SPAN>int Spec X}</CODE> and <CODE>{FD<SPAN class="keyword">.</SPAN>reified<SPAN class="keyword">.</SPAN>dom Spec Xv}</CODE>, then <IMG alt="P^N" src="latex92.png"> denotes <CODE>{FD<SPAN class="keyword">.</SPAN>reified<SPAN class="keyword">.</SPAN>int ComplSpec X}</CODE> and <CODE>{FD<SPAN class="keyword">.</SPAN>reified<SPAN class="keyword">.</SPAN>dom ComplSpec Xv}</CODE>, respectively (where <CODE>ComplSpec = compl(Spec)</CODE> if <CODE>Spec</CODE> is a simple domain specification, and <CODE>ComplSpec = SSpec</CODE> if <CODE>Spec = compl(SSpec)</CODE>).</P><P>For the propagators <I>P</I> wich are parameterized by a relation symbol <I>A</I>, the symbol of the negated relation occurs in <IMG alt="P^N" src="latex92.png">. For instance, if <I>P</I> is <CODE>{FD<SPAN class="keyword">.</SPAN>sum Ds <SPAN class="string">'<:'</SPAN> X Y}</CODE>, then <IMG alt="P^N" src="latex92.png"> is <CODE>{FD<SPAN class="keyword">.</SPAN>sum Ds <SPAN class="string">'>=:'</SPAN> X Y}</CODE>. </P><DL><DT><A name="label214"></A> <CODE>reified<SPAN class="keyword">.</SPAN>int</CODE></DT><DD><BLOCKQUOTE class="synopsis"><P></P><BLOCKQUOTE class="code"><CODE>{FD<SPAN class="keyword">.</SPAN>reified<SPAN class="keyword">.</SPAN>int </CODE><CODE>+<I>Spec</I></CODE><CODE> </CODE><CODE>*<I>D1</I></CODE><CODE> </CODE><CODE><I>D2</I></CODE><CODE>}</CODE></BLOCKQUOTE><P></P></BLOCKQUOTE></DD><DD><P>reifies <CODE>{FD<SPAN class="keyword">.</SPAN>int Spec D1}</CODE> into <CODE><I>D2</I></CODE>. </P></DD><DT><A name="label216"></A> <CODE>reified<SPAN class="keyword">.</SPAN>dom</CODE></DT><DD><BLOCKQUOTE class="synopsis"><P></P><BLOCKQUOTE class="code"><CODE>{FD<SPAN class="keyword">.</SPAN>reified<SPAN class="keyword">.</SPAN>dom </CODE><CODE>+<I>Spec</I></CODE><CODE> </CODE><CODE><I>Dv</I></CODE><CODE> </CODE><CODE><I>D</I></CODE><CODE>}</CODE></BLOCKQUOTE><P></P></BLOCKQUOTE></DD><DD><P>reifies <CODE>{FD<SPAN class="keyword">.</SPAN>dom Spec Dv}</CODE> into <CODE><I>D</I></CODE>. </P></DD><DT><A name="label218"></A> <CODE>reified<SPAN class="keyword">.</SPAN>sum</CODE></DT><DD><BLOCKQUOTE class="synopsis"><P></P><BLOCKQUOTE class="code"><CODE>{FD<SPAN class="keyword">.</SPAN>reified<SPAN class="keyword">.</SPAN>sum </CODE><CODE>*<I>Dv</I></CODE><CODE> </CODE><CODE>+<I>A</I></CODE><CODE> </CODE><CODE>*<I>D1</I></CODE><CODE> </CODE><CODE><I>D2</I></CODE><CODE>}</CODE></BLOCKQUOTE><P></P></BLOCKQUOTE></DD><DD><P>reifies <CODE>{FD<SPAN class="keyword">.</SPAN>sum Dv A D1}</CODE> into <CODE><I>D2</I></CODE>. </P></DD><DT><A name="label220"></A> <CODE>reified<SPAN class="keyword">.</SPAN>sumC</CODE></DT><DD><BLOCKQUOTE class="synopsis"><P></P><BLOCKQUOTE class="code"><CODE>{FD<SPAN class="keyword">.</SPAN>reified<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>D1</I></CODE><CODE> </CODE><CODE><I>D2</I></CODE><CODE>}</CODE></BLOCKQUOTE><P></P></BLOCKQUOTE></DD><DD><P>reifies <CODE>{FD<SPAN class="keyword">.</SPAN>sumC Iv Dv A D1}</CODE> into <CODE><I>D2</I></CODE>. </P></DD><DT><A name="label222"></A> <CODE>reified<SPAN class="keyword">.</SPAN>sumCN</CODE></DT><DD><BLOCKQUOTE class="synopsis"><P></P><BLOCKQUOTE class="code"><CODE>{FD<SPAN class="keyword">.</SPAN>reified<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>D1</I></CODE><CODE> </CODE><CODE><I>D2</I></CODE><CODE>} </CODE></BLOCKQUOTE><P></P></BLOCKQUOTE></DD><DD><P>reifies <CODE>{FD<SPAN class="keyword">.</SPAN>sumCN Iv Dvv A D1}</CODE> into <CODE><I>D2</I></CODE>. </P></DD><DT><A name="label224"></A> <CODE>reified<SPAN class="keyword">.</SPAN>sumAC</CODE></DT><DD><BLOCKQUOTE class="synopsis"><P></P><BLOCKQUOTE class="code"><CODE>{FD<SPAN class="keyword">.</SPAN>reified<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>D1</I></CODE><CODE> </CODE><CODE><I>D2</I></CODE><CODE>}</CODE></BLOCKQUOTE><P></P></BLOCKQUOTE></DD><DD><P>reifies <CODE>{FD<SPAN class="keyword">.</SPAN>sumAC Iv Dv A D1}</CODE> into <CODE><I>D2</I></CODE>. </P></DD><DT><A name="label226"></A> <CODE>reified<SPAN class="keyword">.</SPAN>sumACN</CODE></DT><DD><BLOCKQUOTE class="synopsis"><P></P><BLOCKQUOTE class="code"><CODE>{FD<SPAN class="keyword">.</SPAN>reified<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>D1</I></CODE><CODE> </CODE><CODE><I>D2</I></CODE><CODE>} </CODE></BLOCKQUOTE><P></P></BLOCKQUOTE></DD><DD><P>reifies <CODE>{FD<SPAN class="keyword">.</SPAN>sumACN Iv Dvv A D1}</CODE> into <CODE><I>D2</I></CODE>. </P></DD><DT><A name="label228"></A> <CODE>reified<SPAN class="keyword">.</SPAN>distance</CODE></DT><DD><BLOCKQUOTE class="synopsis"><P></P><BLOCKQUOTE class="code"><CODE>{FD<SPAN class="keyword">.</SPAN>reified<SPAN class="keyword">.</SPAN>distance </CODE><CODE>*<I>D1</I></CODE><CODE> </CODE><CODE>*<I>D2</I></CODE><CODE> </CODE><CODE>+<I>A</I></CODE><CODE> </CODE><CODE>*<I>D3</I></CODE><CODE> </CODE><CODE><I>D4</I></CODE><CODE>}</CODE></BLOCKQUOTE><P></P></BLOCKQUOTE></DD><DD><P>reifies <CODE>{FD<SPAN class="keyword">.</SPAN>distance D1 D2 A D3}</CODE> into <CODE><I>D4</I></CODE>. </P></DD><DT><A name="label230"></A> <CODE>reified<SPAN class="keyword">.</SPAN>card</CODE></DT><DD><BLOCKQUOTE class="synopsis"><P></P><BLOCKQUOTE class="code"><CODE>{FD<SPAN class="keyword">.</SPAN>reified<SPAN class="keyword">.</SPAN>card </CODE><CODE>*<I>D1</I></CODE><CODE> </CODE><CODE>*<I>Dv</I></CODE><CODE> </CODE><CODE>*<I>D2</I></CODE><CODE> </CODE><CODE><I>D3</I></CODE><CODE>}</CODE></BLOCKQUOTE><P></P></BLOCKQUOTE></DD><DD><P><I>Dv</I> is a vector of Boolean variables. <CODE>FD<SPAN class="keyword">.</SPAN>reified<SPAN class="keyword">.</SPAN>card</CODE> creates a propagator for</P><P><IMG alt="(({\tt D1}\leq{\tt D}_1+\ldots+{\tt D}_n\leq{\tt D2}) \leftrightarrow
({\tt D3}=1))\;\wedge\;{\tt D3} \in \{0,1\}." src="latex93.png"></P><P>which reifies into <CODE>D3</CODE> the conjunction </P><BLOCKQUOTE class="code"><CODE>D1 <SPAN class="keyword">=<:</SPAN> D1 <SPAN class="keyword">+</SPAN> <SPAN class="keyword">...</SPAN> <SPAN class="keyword">+</SPAN> Dn<BR>D1 <SPAN class="keyword">+</SPAN> <SPAN class="keyword">...</SPAN> <SPAN class="keyword">+</SPAN> Dn <SPAN class="keyword">=<:</SPAN> D2 </CODE></BLOCKQUOTE><P> </P><P>More specifically, its operational semantics is defined through </P><BLOCKQUOTE class="code"><CODE>D3 <SPAN class="keyword">::</SPAN> 0<SPAN class="keyword">#</SPAN>1<BR><SPAN class="keyword">or</SPAN> D1 <SPAN class="keyword">=<:</SPAN> D1 <SPAN class="keyword">+</SPAN> <SPAN class="keyword">...</SPAN> <SPAN class="keyword">+</SPAN> Dn <BR> D1 <SPAN class="keyword">+</SPAN> <SPAN class="keyword">...</SPAN> <SPAN class="keyword">+</SPAN> Dn <SPAN class="keyword">=<:</SPAN> D2<BR> D3 = 1<BR><SPAN class="keyword">[]</SPAN> <SPAN class="keyword">or</SPAN> D1 <SPAN class="keyword">>:</SPAN> D1 <SPAN class="keyword">+</SPAN> <SPAN class="keyword">...</SPAN> <SPAN class="keyword">+</SPAN> Dn <BR> <SPAN class="keyword">[]</SPAN> D1 <SPAN class="keyword">+</SPAN> <SPAN class="keyword">...</SPAN> <SPAN class="keyword">+</SPAN> Dn <SPAN class="keyword">>:</SPAN> D2<BR> <SPAN class="keyword">end</SPAN> <BR> D3 = 0<BR><SPAN class="keyword">end</SPAN> </CODE></BLOCKQUOTE><P></P></DD></DL><P></P></DIV><TABLE align="center" border="0" cellpadding="6" cellspacing="6" class="nav"><TR bgcolor="#DDDDDD"><TD><A href="node23.html#section.fd.bool"><< Prev</A></TD><TD><A href="node14.html">- Up -</A></TD><TD><A href="node25.html#section.fd.misc">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>
|