Work on rewriting chapter

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.

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.
+The \microzinc{} \gls{interpreter} performs \gls{cse} through memorisation.
-In some cases, it is even possible to not generate definitions in the first place through the use of \glsaccesslong{cse}.
+It maintains a table that maps a function identifier and the call arguments to its result for each call instruction that is executed.
-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}.
+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
+Earlier in the process, however, the \minizinc{} to \microzinc{} \gls{compiler} can perform a more traditional form of \gls{cse}.
-
-\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.
 
 \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) =
+		(abs(x)*2 >= 20) \/ (abs(x)+5 >= 15)
-			let {
-				var float: x = pow(a, 2);
-				var float: y = pow(b, 2);
-			} in sqrt(x + y);
-		constraint pythagoras(i, i) >= 5;
 	\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.
+	It is important that \gls{cse}the expression \mzninline{abs(x)} is evaluated twice.
-	A straightforward approach to ensure that the same instantiation of a function is only evaluated once is through memorisation.
+	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:
-	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.
+	\begin{mzn}
-	If the call is found, then the accompanying result is used; otherwise, the evaluation proceeds as normal.
+		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.
+As such, 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.
+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}