<Section id="u_replacing">

<Title/Replacing a Propagator/
<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>
Consider the following situation: First a propagator <Math/x+y=z/ was
imposed. At a later point in time the constraint <Math/x=y/ is told to the
constraint store. The equality constraint allows to replace <Math/x+y=z/ by
<Math/2x=z/. The rules below show how <Math/x+y=z/ can be replaced by another
(equality) constraint, if two variables are set equal.

<p>
<!--
\begin{eqnarray}
x+y=z \;\wedge\; x=y  \;\rightarrow\;  z=2x \label{rule_r1} \\
x+y=z \;\wedge\; x=z  \;\rightarrow\;  y=0  \label{rule_r2} \\
x+y=z \;\wedge\; y=z  \;\rightarrow\;  x=0  \label{rule_r3}
\end{eqnarray}
-->

<para id="u_replace.rule1"><title//
Rule 1: <Math/x+y=z \;\wedge\; x=y  \;\rightarrow\;  z=2x/

<para id="u_replace.rule2"><title//
Rule 2: <Math/x+y=z \;\wedge\; x=z  \;\rightarrow\;  y=0/

<para id="u_replace.rule3"><title//
Rule 3: <Math/x+y=z \;\wedge\; y=z  \;\rightarrow\;  x=0/

<p>
Such simplifications can be implemented by replacing a propagator by
another one. The &cpi provides for that purpose in <<OZ_Propagator>> a
group of member functions <<replaceBy>>. This section demonstrates
how to realise the above simplifications using the example of the
previous section.

<SubSection id="u_replace.twice">
<Title/A Twice Propagator/
<p>
The implementation of the simplification rule 
<Math/x+y=z \wedge x=y \rightarrow 2x=z/ requires a propagator for the 
constraint
<Math/2x=z/. The following code defines the class <<TwiceProp>>.

<Code.Extern display proglang=cc to="programs/ex_b.2.cc" class=linenumbers>

<p>
The member function <<propagate()>> mainly consists of a
<<for>>-loop collecting in auxiliary variables the values <Math/v_x/ and
<Math/v_z/ satisfying the relation <Math/2v_x=v_z/.

<p>
<Code.Extern display proglang=cc to="programs/ex_b.3.cc" class=linenumbers>
<p>

<Subsection id = "u_replace.equality">
<Title/Equality Detection and Replacement/
<p>
Imposing equality on variables is done by unification. A propagator is
<Em/always/ resumed if at least one variable of its parameters is
unified with another variable. The class <<OZ_Propagator>> provides
for a member function <<mayBeEqualVars()>>, which returns <Math/1/ in case
the propagator is resumed because at least one of its parameters was
involved in a unification. Otherwise it returns <Math/0/.

<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 
&cpi function <<OZ_isEqualVars()>> is provided for that purpose. It takes
two heap references and returns <Math/1/ if they refer to the same
variable. In case equal variables are detected the execution branches to
a <<return>> statement, which returns the value produced by executing
the function passed as argument of the macro.

<p>
<Code.Extern display proglang=cc to="programs/ex_b.3b.cc" class=linenumbers>

<p>
The macro is inserted as first statement in the code of the addition
propagator. The member functions <<replaceBy()>> and
<<replaceByInt()>> provided by <<OZ_Propagator>> replace the addition
propagator according to their arguments by another propagator or a basic
constraint.

<p>
<Code.Extern display proglang=cc to="programs/ex_a.3a.cc" class=linenumbers>
<Code.Extern display proglang=cc to="programs/ex_b.3a.cc" class=linenumbers>

<p>
The first argument of the macro causes the addition propagator to be
replaced by the twice propagator, which implements reduction rule 1
<ptr to="u_replace.rule1">.  The member function <<replaceBy()>>
expects a pointer to a propagator which is generated by applying the
<<new>> operator to the constructor of the class <<TwiceProp>>. The
second and third macro argument realize the simplification rules 2
<ptr to="u_replace.rule2"> and 3 <ptr to="u_replace.rule3"> by
imposing the constraint <Math/y=0/ &resp <Math/x=0/.


<SubSection id="u_replace.benefits">
<Title/Benefits of Replacing Propagators/

<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.

<Code.Extern display to="programs/ex_b.2.oz" class=linenumbers>

<p>
Note that the constraint <Math/x=y/ causes <Math/x+y=z/ to be replaced
by <Math/2x=z/,
so that the domain of <Math/x/ and <Math/y/ is further constrained to 
<Math/\{1,3,5\}/,
which is not the case for the propagator implemented in
<ptr to="u_getting_started">.




