/usr/share/mozart/doc/system/node23.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.9 0/1 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="node22.html#section.fd.nonlinear"><< Prev</A></TD><TD><A href="node14.html">- Up -</A></TD><TD><A href="node24.html#section.fd.reified">Next >></A></TD></TR></TABLE><DIV id="section.fd.bool"><H2><A name="section.fd.bool">5.9 0/1 Propagators</A></H2><P>Using the mapping from <CODE>0</CODE> and <CODE>1</CODE> to the truth values <A name="label199"></A><EM>false</EM> and <A name="label200"></A><EM>true</EM>, respectively, logical connectives between finite domain integers are defined. If at most one argument is a free variable, it will be constrained to a finite domain integer in <IMG alt="\{0,1\}" src="latex88.png">. Such a finite domain integer is also called a 0/1-integer. The propagators exploit equality and may also post equality between variables.</P><P>The operational semantics is detailed only for <CODE>FD<SPAN class="keyword">.</SPAN>conj</CODE>. For the remaining propagators, the operational semantics is defined accordingly, exploiting as much information as possible (including coreferences). </P><DL><DT><A name="label202"></A> <CODE>conj</CODE></DT><DD><BLOCKQUOTE class="synopsis"><P></P><BLOCKQUOTE class="code"><CODE>{FD<SPAN class="keyword">.</SPAN>conj </CODE><CODE>$<I>D1</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><CODE><I>D3</I></CODE> is the conjunction of <CODE><I>D1</I></CODE> and <CODE><I>D2</I></CODE>. The operational semantics can be described by the following code </P><BLOCKQUOTE class="code"><CODE>[D1 D2 D3] <SPAN class="keyword">:::</SPAN> 0<SPAN class="keyword">#</SPAN>1<BR><SPAN class="keyword">cond</SPAN> D1=0 <SPAN class="keyword">then</SPAN> D3=0 <BR><SPAN class="keyword">[]</SPAN> D1=1 <SPAN class="keyword">then</SPAN> D2=D3 <BR><SPAN class="keyword">[]</SPAN> D2=0 <SPAN class="keyword">then</SPAN> D3=0 <BR><SPAN class="keyword">[]</SPAN> D2=1 <SPAN class="keyword">then</SPAN> D1=D3 <BR><SPAN class="keyword">[]</SPAN> D3=1 <SPAN class="keyword">then</SPAN> D1=1 D2=1 <BR><SPAN class="keyword">[]</SPAN> D1=D2 <SPAN class="keyword">then</SPAN> D1=D3 <BR><SPAN class="keyword">end</SPAN></CODE></BLOCKQUOTE><P> </P></DD><DT><A name="label204"></A> <CODE>disj</CODE></DT><DD><BLOCKQUOTE class="synopsis"><P></P><BLOCKQUOTE class="code"><CODE>{FD<SPAN class="keyword">.</SPAN>disj </CODE><CODE>$<I>D1</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><CODE><I>D3</I></CODE> is the disjunction of <CODE><I>D1</I></CODE> and <CODE><I>D2</I></CODE>. </P></DD><DT><A name="label206"></A> <CODE>exor</CODE></DT><DD><BLOCKQUOTE class="synopsis"><P></P><BLOCKQUOTE class="code"><CODE>{FD<SPAN class="keyword">.</SPAN>exor </CODE><CODE>$<I>D1</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><CODE><I>D3</I></CODE> is the exclusive disjunction of <CODE><I>D1</I></CODE> and <CODE><I>D2</I></CODE>. </P></DD><DT><A name="label208"></A> <CODE>nega</CODE></DT><DD><BLOCKQUOTE class="synopsis"><P></P><BLOCKQUOTE class="code"><CODE>{FD<SPAN class="keyword">.</SPAN>nega </CODE><CODE>$<I>D1</I></CODE><CODE> </CODE><CODE>$<I>D2</I></CODE><CODE>}</CODE></BLOCKQUOTE><P></P></BLOCKQUOTE></DD><DD><P><CODE><I>D2</I></CODE> is the negation of <CODE><I>D1</I></CODE>. </P></DD><DT><A name="label210"></A> <CODE>impl</CODE></DT><DD><BLOCKQUOTE class="synopsis"><P></P><BLOCKQUOTE class="code"><CODE>{FD<SPAN class="keyword">.</SPAN>impl </CODE><CODE>$<I>D1</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><CODE><I>D3</I></CODE> is the implication of <CODE><I>D2</I></CODE> by <CODE><I>D1</I></CODE> (``<IMG alt="{\tt D1}\rightarrow{\tt D2}" src="latex89.png">''). </P></DD><DT><A name="label212"></A> <CODE>equi</CODE></DT><DD><BLOCKQUOTE class="synopsis"><P></P><BLOCKQUOTE class="code"><CODE>{FD<SPAN class="keyword">.</SPAN>equi </CODE><CODE>$<I>D1</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><CODE><I>D3</I></CODE> is the equivalence of <CODE><I>D1</I></CODE> by <CODE><I>D2</I></CODE> (``<IMG alt="{\tt D1}\leftrightarrow{\tt D2}" src="latex90.png">''). </P></DD></DL><P></P></DIV><TABLE align="center" border="0" cellpadding="6" cellspacing="6" class="nav"><TR bgcolor="#DDDDDD"><TD><A href="node22.html#section.fd.nonlinear"><< Prev</A></TD><TD><A href="node14.html">- Up -</A></TD><TD><A href="node24.html#section.fd.reified">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>
|