diff --git a/chapters/2_background.tex b/chapters/2_background.tex index 6aa6063..dbe9200 100644 --- a/chapters/2_background.tex +++ b/chapters/2_background.tex @@ -1244,6 +1244,7 @@ Because the evaluation of a \minizinc{} expression cannot have any side effects, 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 \cmls\ \autocite{rendl-2009-enhanced-tailoring}. \begin{example} +\label{ex:back-cse} For instance, in the constraint \begin{mzn} @@ -1273,7 +1274,7 @@ Some expressions only become syntactically equal during evaluation, as in the fo 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. \end{example} -A straightforward approach to ensure that the same instantiation of a function To ensure that syntactically equal expressions are only evaluated once the \minizinc\ compiler through the use of memorisation. +To ensure that the same instantiation of a function are only evaluated once, the \minizinc\ compiler uses memorisation. After the flattening of an expression, the instantiated expression and its result are stored in a lookup table, the \gls{cse} table. Then before any consequent expression is flattened the \gls{cse} table is consulted. If an equivalent expression is found, then the accompanying result is used; otherwise, the evaluation proceeds as normal. diff --git a/chapters/3_rewriting.tex b/chapters/3_rewriting.tex index 8364530..a844c9a 100644 --- a/chapters/3_rewriting.tex +++ b/chapters/3_rewriting.tex @@ -616,59 +616,41 @@ This crucial optimisation enables rewriting in multiple \emph{phases}. For example, a model targeted at a \gls{mip} solver is rewritten into Boolean and reified constraints, whose definitions are annotated to be delayed. The \nanozinc\ model can then be fully simplified by \gls{propagation}, before the Boolean and reified constraints are rewritten into lower-level linear primitives suitable for \gls{mip}. -\subsection{Common Sub-expression Elimination}\label{sec:4-cse} +\subsection{Common Sub-expression Elimination}% +\label{sec:rew-cse} -\jip{Adjust with the background section. Just needs to talk about \microzinc{} optimisation.} +\Gls{cse} is a crucial technique to avoid duplications in a \gls{model}. +In our architecture \gls{cse} is performed on two levels. -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 \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}. +The \microzinc{} \gls{interpreter} performs \gls{cse} through memorisation. +It maintains a table that maps a function identifier and the call arguments to its result for each call instruction that is executed. +Before it executes a call instruction, it searches the table for an entry with identical function identifier and call arguments. +Since functions in \microzinc\ are guaranteed to be pure and total, whenever the table search succeeds, the result can be used instead of executing the call instruction. -For instance, in the constraint - -\begin{mzn} -(abs(x)*2 >= 20) \/ (abs(x)+5 >= 15) -\end{mzn} - -the expression \mzninline{abs(x)} is evaluated twice. -Since functions in \microzinc\ are guaranteed to be pure and total, any expressions that are syntactically equal can be detected by a static compiler analysis before evaluation even begins, and hoisted into a let expression: - -\begin{mzn} -constraint let { var int: y = abs(x) } in - (y*2 >= 20) \/ (y+5 >= 15) -\end{mzn} - -However, some expressions only become syntactically equal during evaluation, as in the following example. +Earlier in the process, however, the \minizinc{} to \microzinc{} \gls{compiler} can perform a more traditional form of \gls{cse}. \begin{example} - Consider the fragment: + For instance, let us reconsider the \minizinc{} fragment from \cref{ex:back-cse} \begin{mzn} - function var float: pythagoras(var float: a, var float: b) = - let { - var float: x = pow(a, 2); - var float: y = pow(b, 2); - } in sqrt(x + y); - constraint pythagoras(i, i) >= 5; + (abs(x)*2 >= 20) \/ (abs(x)+5 >= 15) \end{mzn} - 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 \gls{cse} table. - Then before any consequent 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. + It is important that \gls{cse}the expression \mzninline{abs(x)} is evaluated twice. + Since functions in \microzinc\ are guaranteed to be pure and total, any expressions that are syntactically equal can be detected by a static compiler analysis before evaluation even begins, and hoisted into a let expression: + + \begin{mzn} + constraint let { var int: y = abs(x) } in + (y*2 >= 20) \/ (y+5 >= 15) + \end{mzn} - 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 \gls{cse} table and replaced by the earlier stored result: \mzninline{y = x}. \end{example} -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 sub-expressions before evaluation begins. -However, since the static analysis is cheap and can potentially avoid many dynamic table look-ups, it is valuable to combine both approaches. +As such, the compiler can enforce sharing of common sub-expressions before evaluation begins. +It is worth noting that, although the \gls{cse} approach based on memorisation would also covers the static example above, this method can potentially avoid many dynamic table look-ups. +Since the static analysis is cheap, it is valuable to combine both approaches. The static approach can be further improved by \emph{inlining} function calls, since that may expose more calls as being syntactically equal. -\jip{TODO:\ \gls{cse} will be discussed in the background. How can we make this - more specific to how it works in \nanozinc{}.} - \jip{Comment Peter: details or implementation -- interaction with reference counting??} \paragraph{Reification}