/usr/share/mozart/doc/system/node8.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>3 Constraints-Specific Type Structure and Modes</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="index.html">- Up -</A></TD><TD><A href="node9.html#chapter.search">Next >></A></TD></TR></TABLE><DIV id="chapter.types_modes_constr"><H1><A name="chapter.types_modes_constr">3 Constraints-Specific Type Structure and Modes</A></H1><P>This section presents those types and modes which are specific for the constraint extensions. </P><H2><A name="label43">3.1 Type Structure</A></H2><P>There are two additional secondary types. </P><P class="margin">Vector</P><P> A vector is a record with a label different from <CODE><SPAN class="string">'|'</SPAN></CODE> or a list. The elements of the list or the fields of the record are called the elements of the vector. A finite domain vector is a vector all of whose elements are finite domain integers. </P><P class="margin">Specification of Sets of Integers</P><P> A specification of sets of integers <CODE>Spec</CODE> is used in cointext of finite domain and finite set constraints. It is recursively defined as follows. </P><BLOCKQUOTE><TABLE border="0" cellpadding="0" cellspacing="0"><TR valign="top"><TD><I>Spec</I></TD><TD align="center"> ::= </TD><TD><I>simpl_spec</I></TD></TR><TR valign="top"><TD></TD><TD align="center"> | </TD><TD>compl(<I>simpl_spec</I>)</TD></TR></TABLE></BLOCKQUOTE><P></P><BLOCKQUOTE><TABLE border="0" cellpadding="0" cellspacing="0"><TR valign="top"><TD><I>simpl_spec</I></TD><TD align="center"> ::= </TD><TD><I>range_descr</I></TD></TR><TR valign="top"><TD></TD><TD align="center"> | </TD><TD>[<I>range_descr</I>+]</TD></TR><TR valign="top"><TD></TD><TD align="center"> | </TD><TD><CODE>nil</CODE></TD></TR></TABLE></BLOCKQUOTE><P></P><BLOCKQUOTE><TABLE border="0" cellpadding="0" cellspacing="0"><TR valign="top"><TD><I>range_descr</I></TD><TD align="center"> ::= </TD><TD><I>integer</I></TD></TR><TR valign="top"><TD></TD><TD align="center"> | </TD><TD><I>integer</I><CODE><SPAN class="keyword">#</SPAN></CODE><I>integer</I></TD></TR></TABLE></BLOCKQUOTE><P></P><BLOCKQUOTE><TABLE border="0" cellpadding="0" cellspacing="0"><TR valign="top"><TD><I>integer</I></TD><TD align="center"> ::= </TD><TD><CODE>FD<SPAN class="keyword">.</SPAN>inf</CODE>,...,<CODE>FD<SPAN class="keyword">.</SPAN>sup</CODE></TD></TR><TR valign="top"><TD></TD><TD align="center"> | </TD><TD><CODE>FS<SPAN class="keyword">.</SPAN>inf</CODE>,...,<CODE>FS<SPAN class="keyword">.</SPAN>sup</CODE></TD></TR></TABLE></BLOCKQUOTE><P></P><P>A specification of sets of integers denotes a set of integers which is either the union of integer singletons <IMG alt="i" src="latex1.png"> and integer intervals <IMG alt="i\#i" src="latex2.png">, or the complement <CODE>compl(<SPAN class="keyword">...</SPAN>)</CODE> of such a set relative to <IMG alt="\{\mbox{\tt FD.inf},\ldots,\mbox{\tt FD.sup}\}" src="latex3.png"> resp. <IMG alt="\{\mbox{\tt FS.inf},\ldots,\mbox{\tt FS.sup}\}" src="latex4.png">. Note that an empty set is specified by <CODE>nil</CODE>. </P><P>In context of finite domain constraints for example, <CODE>2<SPAN class="keyword">#</SPAN>5</CODE> denotes the set <IMG alt="\{2,\ldots,5\}" src="latex5.png">, the specification <CODE>[1 10<SPAN class="keyword">#</SPAN>20]</CODE> denotes the set <IMG alt="\{1,10,\ldots,20\}" src="latex6.png">, and <CODE>compl(2<SPAN class="keyword">#</SPAN>5)</CODE> denotes <IMG alt="\{0,1,6,\ldots,\mbox{\tt FD.sup}\}" src="latex7.png">. </P><P>The value of <CODE>FD<SPAN class="keyword">.</SPAN>inf</CODE> and <CODE>FS<SPAN class="keyword">.</SPAN>inf</CODE> is 0 and the value of <CODE>FD<SPAN class="keyword">.</SPAN>sup</CODE> and <CODE>FS<SPAN class="keyword">.</SPAN>sup</CODE> is 134217726. These values are implementation-dependent. </P><P class="margin">Weight Specifications</P><P> Weight specifications <CODE>SpecW</CODE> occur in conjunction with set constraints (see <A href="node42.html#section.fs.distribution">Section 7.9</A>) and are defined as follows. </P><BLOCKQUOTE><TABLE border="0" cellpadding="0" cellspacing="0"><TR valign="top"><TD><I>SpecW</I></TD><TD align="center"> ::= </TD><TD><CODE>nil</CODE></TD></TR><TR valign="top"><TD></TD><TD align="center"> | </TD><TD>[<I>ElemDescr</I>]+</TD></TR></TABLE></BLOCKQUOTE><P></P><BLOCKQUOTE><TABLE border="0" cellpadding="0" cellspacing="0"><TR valign="top"><TD><I>ElemDescr</I></TD><TD align="center"> ::= </TD><TD><I>Int</I><CODE><SPAN class="keyword">#</SPAN></CODE><I>Int</I></TD></TR><TR valign="top"><TD></TD><TD align="center"> | </TD><TD><CODE>(</CODE><I>Int</I><CODE><SPAN class="keyword">#</SPAN></CODE><I>Int</I><CODE>)<SPAN class="keyword">#</SPAN></CODE><I>Int</I></TD></TR><TR valign="top"><TD></TD><TD align="center"> | </TD><TD><CODE>default<SPAN class="keyword">#</SPAN></CODE><I>Int</I></TD></TR></TABLE></BLOCKQUOTE><P></P><H2><A name="label44">3.2 Signatures</A></H2><DIV class="unnumbered" id="sec:type-abbrev-ps"><H3><A name="sec:type-abbrev-ps">Types</A></H3><P>The additional type abbreviations are listed in Figure <A href="node8.html#type-abbrev-ps">Figure 3.1</A>. </P><DIV id="type-abbrev-ps"><HR><P><A name="type-abbrev-ps"></A></P><TABLE align="center" bgcolor="#f0f0e0"><TR valign="top"><TH><P>Abbreviation</P></TH><TH><P>Type</P></TH></TR><TR valign="top"><TD><P><I>D</I></P></TD><TD><P>finite domain integer</P></TD></TR><TR valign="top"><TD><P><I>M</I></P></TD><TD><P>finite set of integers</P></TD></TR><TR valign="top"><TD><P><I>Xr</I></P></TD><TD><P>records of type <I>X</I></P></TD></TR><TR valign="top"><TD><P><I>Xt</I></P></TD><TD><P>tuples of type <I>X</I></P></TD></TR><TR valign="top"><TD><P><I>Xv</I></P></TD><TD><P>vectors of type <I>X</I></P></TD></TR><TR valign="top"><TD><P><I>Xvv</I></P></TD><TD><P>vectors of vectors of type <I>X</I></P></TD></TR><TR valign="top"><TD><P><I>Xrr</I></P></TD><TD><P>records of records of type <I>X</I></P></TD></TR></TABLE><P class="caption"><STRONG>Figure 3.1:</STRONG> Type Abbreviations</P><HR></DIV><P> </P></DIV><DIV class="unnumbered" id="modes-ps"><H3><A name="modes-ps">Modes</A></H3><P>Given a constraint store, every variable is in exactly one of the following three states. It is <EM>free</EM> if the store knows nothing about the variable apart from equalities, <EM>determined</EM> if the store knows the top-level constructor, and <EM>kinded</EM> if the variable is neither free nor determined. Variables which are either determined or kinded are called <EM>constrained</EM>. </P><P>The base language does not allow to constrain a variable without determining it. Most procedures of the base language wait until their arguments are determined. </P><P class="margin">Input Modes <CODE>*<I></I></CODE>, <CODE>+<I></I></CODE></P><P> In the constraint extension, a variable can be constrained before it becomes determined. Accordingly, the constraint extensions use additional input modes <CODE>*<I></I></CODE> and <CODE>$<I></I></CODE> which synchronize more weakly than <CODE>+<I></I></CODE>. The application of a procedure <CODE>P</CODE> waits until its inputs (<CODE>+<I></I></CODE>, <CODE>*<I></I></CODE>) are determined or constrained, respectively. If the input arguments are well-typed, <CODE>P</CODE> returns outputs of the specified types. Ill-typed input arguments produce a runtime type error (on completion of <CODE>P</CODE>). </P><P class="margin">Propagators</P><P> Note that it is perfectly possible that an input argument is constrained further. This is the case for many propagators, which have the following typical moding. </P><BLOCKQUOTE class="code"><CODE>{P </CODE><CODE>*<I>X</I></CODE><CODE> </CODE><CODE>*<I>Y</I></CODE><CODE> </CODE><CODE>*<I>Z</I></CODE><CODE>}</CODE></BLOCKQUOTE><P> Note also that modes only partially specify the synchronisation behavior of a procedure. </P><P class="margin">Nestable Input Mode <CODE>$<I></I></CODE></P><P> The mode <CODE>$<I></I></CODE> slightly weakens <CODE>*<I></I></CODE> to allow for nesting of propagators. When <IMG alt="n" src="latex8.png"> arguments of a propagator have input mode <CODE>$<I></I></CODE>, then this propagator waits until <IMG alt="n-1" src="latex9.png"> of them are constrained and then it constrains the remaining <IMG alt="n" src="latex8.png">th argument according to its type. </P></DIV><H3><A name="label45">3.2.1 Notational Conventions</A></H3><P>Notational conventions are explained in context of finite domain constraints but apply of course for finite set constraints too. </P><P class="margin">Specification Input</P><P> The signature </P><BLOCKQUOTE class="code"><CODE>{FD<SPAN class="keyword">.</SPAN>int </CODE><CODE>+<I>Spec</I></CODE><CODE> </CODE><CODE>?<I>D</I></CODE><CODE>}</CODE></BLOCKQUOTE><P> specifies that an application of <CODE>FD<SPAN class="keyword">.</SPAN>int</CODE> waits until <CODE>+<I>Spec</I></CODE> is <EM>ground</EM>, i. e., contains no free variables. Arguments of the form <CODE>+<I>Spec</I></CODE> never occur. The signature </P><BLOCKQUOTE class="code"><CODE>{FD<SPAN class="keyword">.</SPAN>distinct </CODE><CODE>*<I>Dv</I></CODE><CODE>}</CODE></BLOCKQUOTE><P> specifies that an application of <CODE>FD<SPAN class="keyword">.</SPAN>distinct</CODE> waits until its argument <CODE>Dv</CODE> is determined and all its elements are constrained to finite domain integers. Analogously, <CODE>+<I>Iv</I></CODE> specifies that the application waits until <CODE>Iv</CODE> and all its elements are determined. The scheme </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> specifies that the application waits until <CODE>*<I>Dvv</I></CODE> and all its elements are determined, and until their elements are constrained to finite domain integers. </P><P class="margin">Generic Propagators</P><P> For some procedures like that for generic propagators, an atom occurring as an argument denotes a relation symbol. For example, </P><BLOCKQUOTE class="code"><CODE>{FD<SPAN class="keyword">.</SPAN>sum [X Y Z] <SPAN class="string">'=:'</SPAN> D}</CODE></BLOCKQUOTE><P> denotes the constraint </P><BLOCKQUOTE><P><IMG alt="X + Y + Z = D" src="latex10.png"></P></BLOCKQUOTE><P> If <IMG alt="A" src="latex11.png"> is the atomic argument, <IMG alt="\sim_A" src="latex12.png"> is the corresponding arithmetic relation. For <IMG alt="A" src="latex11.png"> the atoms <CODE><SPAN class="string">'=:'</SPAN></CODE>, <CODE><SPAN class="string">'>:'</SPAN></CODE>, <CODE><SPAN class="string">'>=:'</SPAN></CODE>, <CODE><SPAN class="string">'<:'</SPAN></CODE>, <CODE><SPAN class="string">'=<:'</SPAN></CODE>, and <CODE><SPAN class="string">'\\=:'</SPAN></CODE> are allowed. The relations are <IMG alt="=" src="latex13.png">, <IMG alt=">" src="latex14.png">, <IMG alt="\geq" src="latex15.png">, <IMG alt="<" src="latex16.png">, <IMG alt="\leq" src="latex17.png">, and <IMG alt="\neq" src="latex18.png">, respectively. </P></DIV><TABLE align="center" border="0" cellpadding="6" cellspacing="6" class="nav"><TR bgcolor="#DDDDDD"><TD><A href="index.html">- Up -</A></TD><TD><A href="node9.html#chapter.search">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>
|