Dekker1/dekker-phd-thesis
Archived
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Add correct index references for CSE

Browse Source
This commit is contained in:
Jip J. Dekker 2021-04-09 16:47:50 +10:00
parent cda3338543
commit bbe7ecb848
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
1 changed files with 25 additions and 25 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

50
chapters/4_rewriting.tex
View File

@ -164,7 +164,7 @@ The translation from \minizinc\ to \microzinc\ involves the following steps:
\mzninline{int_plus(x,y)}. As mentioned above, more complex rules for
rewriting conditionals with variables, such as \mzninline{if x then A
else B endif} and \mzninline{A[x]} where \mzninline{x} is a variable,
are also replaced by function calls (\eg \mzninline{if_then_else([x,
are also replaced by function calls (\eg\ \mzninline{if_then_else([x,
true], [A, B])} and \mzninline{element(a, x)} respectively).
\item Replace optional variables into non-optional forms. As shown by Mears et
@ -908,17 +908,17 @@ can then be fully simplified by constraint propagation, before the Boolean and
reified constraints are rewritten into lower-level linear primitives suitable
for MIP\@.
\subsection{Common Subexpression Elimination}\label{sec:4-cse}
\subsection{\titlecap{\glsentrytext{gls-cse}}}\label{sec:4-cse}
The simplifications introduced above remove definitions from the model when we
can detect that they are no longer needed. In some cases, it is even possible to
not generate definitions in the first place through the use of common
subexpression elimination (CSE). This simplification is a well understood
technique that originates from compiler optimisation \autocite{cocke-1970-cse}
and has proven to be very effective in discrete optimisation
not generate definitions in the first place through the use of
\glsaccesslong{cse}. This simplification is a well understood technique that
originates from compiler optimisation \autocite{cocke-1970-cse} and has proven
to be very effective in discrete optimisation
\autocite{marinov-2005-sat-optimisations, araya-2008-cse-numcsp}, including
during the evaluation of constraint modelling languages such as
\minizinc\ \autocite{rendl-2009-enhanced-tailoring}.
during the evaluation of constraint modelling languages such as \minizinc\
\autocite{rendl-2009-enhanced-tailoring}.
For instance, in the constraint\\
\mzninline{(abs(x)*2 >= 20) \/ (abs(x)+5 >= 15)}\\
@ -949,22 +949,22 @@ in the following example.
Although the expressions \mzninline{pow(a, 2)} and \mzninline{pow(b, 2)} are
not syntactically equal, the function call \mzninline{pythagoras(i,i)} using
the same variable for \mzninline{a} and \mzninline{b} makes them equivalent.
A straightforward approach to ensure that the same instantiation of a
function is only evaluated once is through memorisation. After the evaluation
of a \microzinc\ call, the instantiated call and its result are stored in a
lookup table, the CSE table. Before a call is evaluated the CSE table is
the same variable for \mzninline{a} and \mzninline{b} makes them equivalent. A
straightforward approach to ensure that the same instantiation of a function
is only evaluated once is through memorisation. After the evaluation of a
\microzinc\ call, the instantiated call and its result are stored in a lookup
table, the \gls{cse} table. Before a call is evaluated the \gls{cse} table is
consulted. If the call is found, then the accompanying result is used;
otherwise, the evaluation proceeds as normal.
In our example, the evaluation of \mzninline{pythagoras(i, i)} would proceed
as normal to evaluate \mzninline{x = pow(i, 2)}. However, the expression
defining \mzninline{y}, \mzninline{pow(i, 2)}, will be found in the CSE table
and replaced by the earlier stored result: \mzninline{y = x}.
defining \mzninline{y}, \mzninline{pow(i, 2)}, will be found in the \gls{cse}
table and replaced by the earlier stored result: \mzninline{y = x}.
\end{example}
It is worth noting that the CSE approach based on memorisation also covers the
static example above, where the compiler can enforce sharing of common
It is worth noting that the \gls{cse} approach based on memorisation also covers
the static example above, where the compiler can enforce sharing of common
subexpressions before evaluation begins. However, since the static analysis is
cheap and can potentially avoid many dynamic table lookups, it is valuable to
combine both approaches. The static approach can be further improved by
@ -991,17 +991,17 @@ detect that a reified constraint is in fact not required.
If a constraint is present in the root context, it means that it must hold
globally. If the same constraint is used in a reified context, it can therefore
be replaced with the constant \mzninline{true}, avoiding the need for
reification (or in fact any evaluation). We can harness CSE to store the
reification (or in fact any evaluation). We can harness \gls{cse} to store the
evaluation context when a constraint is added, and detect when the same
constraint is used in both contexts. Whenever a lookup in the CSE table is
constraint is used in both contexts. Whenever a lookup in the \gls{cse} table is
successful, action can be taken depending on both the current and stored
evaluation context. If the stored expression was in root context, the constant
\mzninline{true} can be used, independent of the current context. If the stored
expression was in reified context and the current context is reified, the
stored result variable can be used. If the stored expression was in reified
context and the current context is root context, then the previous result can
be replaced by the constant \mzninline{true} (and all its dependencies removed)
and the evaluation will proceed as normal with the root context constraint.
expression was in reified context and the current context is reified, the stored
result variable can be used. If the stored expression was in reified context and
the current context is root context, then the previous result can be replaced by
the constant \mzninline{true} (and all its dependencies removed) and the
evaluation will proceed as normal with the root context constraint.
\begin{example}
Consider the fragment:
@ -1016,7 +1016,7 @@ and the evaluation will proceed as normal with the root context constraint.
\mzninline{q(x)} for the original call. Suppose processing the second
constraint we discover \mzninline{t(x,y)} is \mzninline{true}, setting
\mzninline{b1}. When we process \mzninline{q(x)} in the call
\mzninline{t(x,y)} we find it is the root context. So CSE needs to set
\mzninline{t(x,y)} we find it is the root context. So \gls{cse} needs to set
\mzninline{b0} to \mzninline{true}.
\end{example}