/usr/share/mozart/doc/cpitut/node4.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>1.3 Replacing a Propagator</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="node3.html#u_getting_started"><< Prev</A></TD><TD><A href="node1.html">- Up -</A></TD><TD><A href="node5.html#u_nesting">Next >></A></TD></TR></TABLE><DIV id="u_replacing"><H2><A name="u_replacing">1.3 Replacing a Propagator</A></H2><P>There are situations when a propagator should be replaced by another one. The replacing propagator must have the same declarative semantics, but should provide a more efficient implementation for a particular situation. </P><P>Consider the following situation: First a propagator <IMG alt="x+y=z" src="latex1.png"> was imposed. At a later point in time the constraint <IMG alt="x=y" src="latex26.png"> is told to the constraint store. The equality constraint allows to replace <IMG alt="x+y=z" src="latex1.png"> by <IMG alt="2x=z" src="latex27.png">. The rules below show how <IMG alt="x+y=z" src="latex1.png"> can be replaced by another (equality) constraint, if two variables are set equal. </P><P></P><DIV id="u_replace.rule1"><P class="margin"></P><P> Rule 1: <IMG alt="x+y=z \;\wedge\; x=y \;\rightarrow\; z=2x" src="latex28.png"> </P></DIV><DIV id="u_replace.rule2"><P class="margin"></P><P> Rule 2: <IMG alt="x+y=z \;\wedge\; x=z \;\rightarrow\; y=0" src="latex29.png"> </P></DIV><DIV id="u_replace.rule3"><P class="margin"></P><P> Rule 3: <IMG alt="x+y=z \;\wedge\; y=z \;\rightarrow\; x=0" src="latex30.png"> </P></DIV><P>Such simplifications can be implemented by replacing a propagator by another one. The C<SPAN class="allcaps">PI</SPAN> provides for that purpose in <CODE>OZ_Propagator</CODE> a group of member functions <CODE>replaceBy</CODE>. This section demonstrates how to realise the above simplifications using the example of the previous section. </P><DIV id="u_replace.twice"><H3><A name="u_replace.twice">1.3.1 A Twice Propagator</A></H3><P>The implementation of the simplification rule <IMG alt="x+y=z \wedge x=y \rightarrow 2x=z" src="latex31.png"> requires a propagator for the constraint <IMG alt="2x=z" src="latex27.png">. The following code defines the class <CODE>TwiceProp</CODE>. </P><BLOCKQUOTE class="linenumbers"><PRE><SPAN class="keyword">class</SPAN> <SPAN class="type">TwiceProp</SPAN> : <SPAN class="keyword">public</SPAN> <SPAN class="type">OZ_Propagator</SPAN> {<BR><SPAN class="keyword">private</SPAN>:<BR> <SPAN class="keyword">static</SPAN> <SPAN class="type">OZ_PropagatorProfile</SPAN> <SPAN class="variablename">profile</SPAN>;<BR> <SPAN class="type">OZ_Term</SPAN> <SPAN class="variablename">_x</SPAN>, <SPAN class="variablename">_z</SPAN>;<BR><SPAN class="keyword">public</SPAN>:<BR> <SPAN class="functionname">TwiceProp</SPAN>(<SPAN class="type">OZ_Term</SPAN> <SPAN class="variablename">a</SPAN>, <SPAN class="type">OZ_Term</SPAN> <SPAN class="variablename">b</SPAN>) <BR> : _x(a), _z(b) {}<BR> <SPAN class="keyword">virtual</SPAN> <SPAN class="type">OZ_Return</SPAN> <SPAN class="functionname">propagate</SPAN>(<SPAN class="type">void</SPAN>);<BR> <BR> <SPAN class="keyword">virtual</SPAN> <SPAN class="type">size_t</SPAN> <SPAN class="functionname">sizeOf</SPAN>(<SPAN class="type">void</SPAN>) { <BR> <SPAN class="keyword">return</SPAN> <SPAN class="keyword">sizeof</SPAN>(TwiceProp); <BR> }<BR> <SPAN class="keyword">virtual</SPAN> <SPAN class="type">void</SPAN> <SPAN class="functionname">gCollect</SPAN>(<SPAN class="type">void</SPAN>) { <BR> OZ_gCollectTerm(_x); <BR> OZ_gCollectTerm(_z); <BR> } <BR> <SPAN class="keyword">virtual</SPAN> <SPAN class="type">void</SPAN> <SPAN class="functionname">sClone</SPAN>(<SPAN class="type">void</SPAN>) { <BR> OZ_sCloneTerm(_x); <BR> OZ_sCloneTerm(_z); <BR> } <BR> <SPAN class="keyword">virtual</SPAN> <SPAN class="type">OZ_Term</SPAN> <SPAN class="functionname">getParameters</SPAN>(<SPAN class="type">void</SPAN>) <SPAN class="keyword">const</SPAN> {<BR> <SPAN class="keyword">return</SPAN> OZ_cons(_x, <BR> OZ_cons(_z,<BR> OZ_nil()));<BR> }<BR> <SPAN class="keyword">virtual</SPAN> <SPAN class="type">OZ_PropagatorProfile</SPAN> *<SPAN class="functionname">getProfile</SPAN>(<SPAN class="type">void</SPAN>) <SPAN class="keyword">const</SPAN> { <BR> <SPAN class="keyword">return</SPAN> &profile;<BR> }<BR>};<BR> <BR><SPAN class="type">OZ_PropagatorProfile</SPAN> <SPAN class="reference">TwiceProp</SPAN>::<SPAN class="variablename">profile</SPAN>;<BR></PRE></BLOCKQUOTE><P> </P><P>The member function <CODE>propagate()</CODE> mainly consists of a <CODE><SPAN class="keyword">for</SPAN></CODE>-loop collecting in auxiliary variables the values <IMG alt="v_x" src="latex32.png"> and <IMG alt="v_z" src="latex24.png"> satisfying the relation <IMG alt="2v_x=v_z" src="latex33.png">. </P><P></P><BLOCKQUOTE class="linenumbers"><PRE><SPAN class="type">OZ_Return</SPAN> <SPAN class="reference">TwiceProp</SPAN>::<SPAN class="functionname">propagate</SPAN>(<SPAN class="type">void</SPAN>)<BR>{<BR> <SPAN class="type">OZ_FDIntVar</SPAN> <SPAN class="variablename">x</SPAN>(_x), z(_z);<BR> <BR> <SPAN class="type">OZ_FiniteDomain</SPAN> <SPAN class="variablename">x_aux</SPAN>(fd_empty), <SPAN class="variablename">z_aux</SPAN>(fd_empty);<BR> <BR> <SPAN class="keyword">for</SPAN> (<SPAN class="type">int</SPAN> <SPAN class="variablename">i</SPAN> = x->getMinElem(); i != -1; <BR> i = x->getNextLargerElem(i)) {<BR> <SPAN class="type">int</SPAN> <SPAN class="variablename">i2</SPAN> = 2 * i;<BR> <SPAN class="keyword">if</SPAN> (z->isIn(i2)) {<BR> x_aux += i; z_aux += i2;<BR> }<BR> }<BR> <BR> FailOnEmpty(*x &= x_aux);<BR> FailOnEmpty(*z &= z_aux);<BR> <BR> <SPAN class="keyword">return</SPAN> (x.leave() | z.leave())<BR> ? OZ_SLEEP : OZ_ENTAILED;<BR> <BR><SPAN class="reference">failure</SPAN>: <BR> x.fail(); z.fail();<BR> <SPAN class="keyword">return</SPAN> OZ_FAILED;<BR>}<BR> <BR></PRE></BLOCKQUOTE><P></P><P></P></DIV><DIV id="u_replace.equality"><H3><A name="u_replace.equality">1.3.2 Equality Detection and Replacement</A></H3><P>Imposing equality on variables is done by unification. A propagator is <EM>always</EM> resumed if at least one variable of its parameters is unified with another variable. The class <CODE>OZ_Propagator</CODE> provides for a member function <CODE>mayBeEqualVars()</CODE>, which returns 1 in case the propagator is resumed because at least one of its parameters was involved in a unification. Otherwise it returns 0. </P><P>To detect if the addition propagator is resumed because of a unification the following macro is defined. First, it checks if the propagator's parameters were involved in some unification. If that is the case, all possible combinations of equated variables are tested. The C<SPAN class="allcaps">PI</SPAN> function <CODE>OZ_isEqualVars()</CODE> is provided for that purpose. It takes two heap references and returns 1 if they refer to the same variable. In case equal variables are detected the execution branches to a <CODE>return</CODE> statement, which returns the value produced by executing the function passed as argument of the macro. </P><P></P><BLOCKQUOTE class="linenumbers"><PRE>#define <SPAN class="functionname">ReplaceOnUnify</SPAN>(<SPAN class="variablename">EQ01</SPAN>, <SPAN class="variablename">EQ02</SPAN>, <SPAN class="variablename">EQ12</SPAN>) \<BR> <SPAN class="keyword">if</SPAN> (mayBeEqualVars()) { \<BR> <SPAN class="keyword">if</SPAN> (OZ_isEqualVars(_x, _y)) { \<BR> <SPAN class="keyword">return</SPAN> (EQ01); \<BR> } \<BR> <SPAN class="keyword">if</SPAN> (OZ_isEqualVars(_x, _z)) { \<BR> <SPAN class="keyword">return</SPAN> (EQ02); \<BR> } \<BR> <SPAN class="keyword">if</SPAN> (OZ_isEqualVars(_y, _z)) { \<BR> <SPAN class="keyword">return</SPAN> (EQ12); \<BR> } \<BR> }<BR></PRE></BLOCKQUOTE><P> </P><P>The macro is inserted as first statement in the code of the addition propagator. The member functions <CODE>replaceBy()</CODE> and <CODE>replaceByInt()</CODE> provided by <CODE>OZ_Propagator</CODE> replace the addition propagator according to their arguments by another propagator or a basic constraint. </P><P></P><BLOCKQUOTE class="linenumbers"><PRE><SPAN class="type">OZ_Return</SPAN> <SPAN class="reference">AddProp</SPAN>::<SPAN class="functionname">propagate</SPAN>(<SPAN class="type">void</SPAN>)<BR>{<BR></PRE></BLOCKQUOTE><P> </P><BLOCKQUOTE class="linenumbers"><PRE> ReplaceOnUnify(replaceBy(<SPAN class="keyword">new</SPAN> <SPAN class="type">TwiceProp</SPAN>(_x, _z)),<BR> replaceByInt(_y, 0),<BR> replaceByInt(_x, 0));<BR></PRE></BLOCKQUOTE><P> </P><P>The first argument of the macro causes the addition propagator to be replaced by the twice propagator, which implements reduction rule 1 <A href="node4.html#u_replace.rule1">*</A>. The member function <CODE>replaceBy()</CODE> expects a pointer to a propagator which is generated by applying the <CODE>new</CODE> operator to the constructor of the class <CODE>TwiceProp</CODE>. The second and third macro argument realize the simplification rules 2 <A href="node4.html#u_replace.rule2">*</A> and 3 <A href="node4.html#u_replace.rule3">*</A> by imposing the constraint <IMG alt="y=0" src="latex34.png"> resp. <IMG alt="x=0" src="latex35.png">. </P></DIV><DIV id="u_replace.benefits"><H3><A name="u_replace.benefits">1.3.3 Benefits of Replacing Propagators</A></H3><P>In most of the cases when propagators are replaced the execution becomes faster without obtaining a stronger propagation simply by the fact that redundant computation is avoided. The example of this section provides for even better propagation by imposing a stronger constraint. This can be observed when running the following Oz code. Of course, the updated module has to be loaded before. </P><BLOCKQUOTE class="linenumbers"><PRE><SPAN class="keyword">declare</SPAN> X Y Z <SPAN class="keyword">in</SPAN> <BR>{Browse [X Y Z]} % <SPAN class="comment">[X Y Z]<BR></SPAN> <BR>X <SPAN class="keyword">::</SPAN> [1 3 5 7 9] % <SPAN class="comment">[X{1 3 5 7 9}<BR></SPAN>Y <SPAN class="keyword">::</SPAN> [1 3 5 7 9] % <SPAN class="comment">Y{1 3 5 7 9}<BR></SPAN>Z <SPAN class="keyword">::</SPAN> 0<SPAN class="keyword">#</SPAN>10 % <SPAN class="comment">Z{0#10}]<BR></SPAN> <BR>{FD_PROP<SPAN class="keyword">.</SPAN>add X Y Z} % <SPAN class="comment">[X{1 3 5 7 9} Y{1 3 5 7 9}<BR></SPAN> % <SPAN class="comment">Z{2 4 6 8 10}]<BR></SPAN>X = Y % <SPAN class="comment">[Y{1 3 5} Y{1 3 5} Z{2 6 10}]<BR></SPAN> <BR></PRE></BLOCKQUOTE><P> </P><P>Note that the constraint <IMG alt="x=y" src="latex26.png"> causes <IMG alt="x+y=z" src="latex1.png"> to be replaced by <IMG alt="2x=z" src="latex27.png">, so that the domain of <IMG alt="x" src="latex4.png"> and <IMG alt="y" src="latex5.png"> is further constrained to <IMG alt="\{1,3,5\}" src="latex36.png">, which is not the case for the propagator implemented in <A href="node3.html#u_getting_started">Section 1.2</A>. </P></DIV></DIV><TABLE align="center" border="0" cellpadding="6" cellspacing="6" class="nav"><TR bgcolor="#DDDDDD"><TD><A href="node3.html#u_getting_started"><< Prev</A></TD><TD><A href="node1.html">- Up -</A></TD><TD><A href="node5.html#u_nesting">Next >></A></TD></TR></TABLE><HR><ADDRESS><A href="http://www.ps.uni-sb.de/~tmueller/">Tobias Müller</A><BR><SPAN class="version">Version 1.4.0 (20110908185330)</SPAN></ADDRESS></BODY></HTML>
|