Work on CSE in rewriting chapter

assets/shorthands.tex

@@ -9,9 +9,11 @@
 \newcommand{\Cmls}{\Glspl{cml}}
 \newcommand{\cmls}{\glspl{cml}}
 \newcommand{\cml}{\gls{cml}}
+\newcommand{\compiler}{\glspl{compiler}\xspace{}}
 \newcommand{\constraints}{\glspl{constraint}\xspace{}}
 \newcommand{\constraint}{\gls{constraint}\xspace{}}
 \newcommand{\flatzinc}{\gls{flatzinc}\xspace{}}
+\newcommand{\interpreter}{\gls{interpreter}\xspace{}}
 \newcommand{\microzinc}{\gls{microzinc}\xspace{}}
 \newcommand{\minisearch}{\gls{minisearch}\xspace{}}
 \newcommand{\minizinc}{\gls{minizinc}\xspace{}}

chapters/3_rewriting.tex

@@ -467,7 +467,7 @@ Consider now the case where a variable in \nanozinc\ is only used in its own aux
 
 	The constraint \mzninline{abs(x) > y} is now used in a disjunction.
 	This means that instead of enforcing the constraint globally, the model needs to reason about whether the constraint holds or not.
-	This is called \gls{reification} (we will come back to this in \cref{sec:4-cse}).
+	This is called \gls{reification} (we will come back to this in \cref{sec:rew-cse}).
 	Following the rewriting rules, the generated \nanozinc\ code will look very similar to the code generated in \cref{ex:4-absnzn}, but with an additional \mzninline{bool_or} constraint for the disjunction, which uses a variable \mzninline{b} that will be introduced for \mzninline{abs(x) > y}:
 
 	\begin{nzn}
@@ -622,12 +622,12 @@ The \nanozinc\ model can then be fully simplified by \gls{propagation}, before t
 \Gls{cse} is a crucial technique to avoid duplications in a \gls{model}.
 In our architecture \gls{cse} is performed on two levels.
 
-The \microzinc{} \gls{interpreter} performs \gls{cse} through memorisation.
+The \microzinc{} \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.
 
-Earlier in the process, however, the \minizinc{} to \microzinc{} \gls{compiler} can perform a more traditional form of \gls{cse}.
+Earlier in the process, however, the \minizinc{} to \microzinc{} \compiler{} can perform form of \gls{cse} such as it is performed in many other programming languages.
 
 \begin{example}
 	For instance, let us reconsider the \minizinc{} fragment from \cref{ex:back-cse}
@@ -636,12 +636,12 @@ Earlier in the process, however, the \minizinc{} to \microzinc{} \gls{compiler}
 		(abs(x)*2 >= 20) \/ (abs(x)+5 >= 15)
 	\end{mzn}
 
-	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:
+	In this case a static \gls{compiler} analysis could detect that the same syntactical expression, \mzninline{abs(x)}, occurs twice.
+	Since these expressions are guaranteed to have equivalent result, this analysis could then be able to hoist into a let expression.
 
 	\begin{mzn}
 		constraint let { var int: y = abs(x) } in
-		(y*2 >= 20) \/ (y+5 >= 15)
+			(y*2 >= 20) \/ (y+5 >= 15)
 	\end{mzn}
 
 \end{example}
@@ -651,50 +651,21 @@ It is worth noting that, although the \gls{cse} approach based on memorisation w
 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{Comment Peter: details or implementation -- interaction with reference counting??}
+\paragraph{Implementation} In the implementation of our \microzinc{} \interpreter{}, \gls{cse} directly interacts with the reference counting mechanism.
+It is clear that a new reference must created when an entry of the \gls{cse} is reused in \nanozinc{}, but the entries of the table themselves are also essentially references.
+However, when a variable is no longer referenced in the \nanozinc{}, we still expect it to be removed, even if it is still part of the \gls{cse} table.
+As such, we treat \gls{cse} entries as \emph{weak} references.
+They reference an object, but do not affect its liveness (\ie{} increase its reference count).
+If an entry is found in the \gls{cse} table with a reference count of zero, it is removed from the table and its contents are not used.
 
-\paragraph{Reification}
-
-\jip{Adjust with information in the background section. Is there anything specific to the \microzinc{}/\nanozinc{} system?}
-
-Many constraint modelling languages, including \minizinc{}, not only enable \constraints{} to be globally enforced, but typically also support \constraints{} to be \emph{reified} into a Boolean variable.
-Reification means that a variable \mzninline{b} is constrained to be true if and only if a corresponding constraint \mzninline{c(...)
-} holds.
-We have already seen reification in \cref{ex:4-absreif}: the truth of constraint \mzninline{abs(x) > y} was bound to a Boolean variable \mzninline{b1}, which was then used in a disjunction.
-We say that the same constraint can be used in \emph{root context} as well as in a \emph{reified context}.
-In \minizinc{}, almost all constraints can be used in both contexts.
-However, reified constraints are often defined in the library in terms of complicated decompositions into simpler constraints, or require specialised algorithms in the target solvers.
-In either case, it can be very beneficial for the efficiency of the generated \nanozinc\ program if we can 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 \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 \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, then the constant \mzninline{true} can be used, independent of the current context.
-Otherwise, if the stored expression was in reified context and the current context is reified, then the stored result variable can be used.
-Finally, 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:
-
-	\begin{mzn}
-		function var bool: p(var int: x, var int: y) = q(x) /\ r(y);
-		constraint b0 <-> q(x);
-		constraint b1 <-> t(x,y);
-		constraint b1 <-> p(x,y);
-	\end{mzn}
-
-	If we process the top-level constraints in order we create a reified call to \mzninline{q(x)} for the original call.
-	Suppose processing the second constraint we discover \mzninline{t(x,y)} is \mzninline{true}, fixing \mzninline{b1}.
-	When we then process \mzninline{q(x)} in instantiation of the call \mzninline{p(x,y)}, we find it is the root context.
-	So \gls{cse} needs to set \mzninline{b0} to \mzninline{true}.
-\end{example}
-
-\minizinc{} distinguishes not only between root and reified contexts, but in addition recognises constraints in \emph{positive} contexts, also known as \emph{half-reified} \autocite{feydy-2011-half-reif}.
-A full explanation and discussion of half-reification can be found in \cref{ch:half-reif}.
-
-\jip{TODO:\ Reification should also be discussed in the background. How can we
-	make this more specific to how it works in \nanozinc{}.}
+The usage of a \gls{cse} table can be costly.
+It requires a lot of memory and the time to find entries can be significant in the overall process.
+This is aggravated by the fact that \minizinc{} has many places where a function's body only contains a single call to a function that is not used anywhere else.
+Although this structure offers flexibility when defining \minizinc{} libraries.
+It results in many \gls{cse} entries that differ only by their function identifier.
+Therefore, we have added an additional flag to our call instruction.
+This flag controls whether the call is subject \gls{cse}.
+This allows us to disable the \gls{cse} when it is guaranteed to be unnecessary.
 
 \subsection{Constraint Aggregation}%
 \label{subsec:rew-aggregation}
@@ -714,8 +685,8 @@ For example the evaluation of the linear constraint \mzninline{x + 2*y <= z} wil
 	constraint int_le(i2, z);
 \end{nzn}
 
-These \nanozinc\ definitions are correct, but, at least for \gls{mip} solvers \jip{this was wrong}, the existence of the intermediate variables is likely to have a negative impact on the \gls{solver}'s performance.
-These \glspl{solver} would likely perform better had they received the linear constraint \mzninline{int_lin_le([1,2,-1],  [x,y,z], 0)} directly, which corresponds to \mzninline{1*x + 2*y - z <= 0}.
+These \nanozinc\ definitions are correct, but, for many \gls{cp} solvers the existence of the intermediate variables is likely to have a negative impact on the \solver{}'s performance.
+These \solver{} would likely perform better had they received the linear constraint \mzninline{int_lin_le([1,2,-1],  [x,y,z], 0)}, which directly corresponds to \mzninline{1*x + 2*y - z <= 0}.
 Since many solvers support linear constraints, it is often an additional burden to have intermediate values that have to be given a value in the solution.
 
 This can be resolved using the \gls{aggregation}.

chapters/4_half_reif.tex

@@ -6,6 +6,50 @@
 
 \input{chapters/4_half_reif_preamble}
 
+
+\paragraph{Reification - Text from rewriting}
+
+\jip{Adjust with information in the background section. Is there anything specific to the \microzinc{}/\nanozinc{} system?}
+
+Many constraint modelling languages, including \minizinc{}, not only enable \constraints{} to be globally enforced, but typically also support \constraints{} to be \emph{reified} into a Boolean variable.
+Reification means that a variable \mzninline{b} is constrained to be true if and only if a corresponding constraint \mzninline{c(...)
+} holds.
+We have already seen reification in \cref{ex:4-absreif}: the truth of constraint \mzninline{abs(x) > y} was bound to a Boolean variable \mzninline{b1}, which was then used in a disjunction.
+We say that the same constraint can be used in \emph{root context} as well as in a \emph{reified context}.
+In \minizinc{}, almost all constraints can be used in both contexts.
+However, reified constraints are often defined in the library in terms of complicated decompositions into simpler constraints, or require specialised algorithms in the target solvers.
+In either case, it can be very beneficial for the efficiency of the generated \nanozinc\ program if we can 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 \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 \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, then the constant \mzninline{true} can be used, independent of the current context.
+Otherwise, if the stored expression was in reified context and the current context is reified, then the stored result variable can be used.
+Finally, 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:
+
+	\begin{mzn}
+		function var bool: p(var int: x, var int: y) = q(x) /\ r(y);
+		constraint b0 <-> q(x);
+		constraint b1 <-> t(x,y);
+		constraint b1 <-> p(x,y);
+	\end{mzn}
+
+	If we process the top-level constraints in order we create a reified call to \mzninline{q(x)} for the original call.
+	Suppose processing the second constraint we discover \mzninline{t(x,y)} is \mzninline{true}, fixing \mzninline{b1}.
+	When we then process \mzninline{q(x)} in instantiation of the call \mzninline{p(x,y)}, we find it is the root context.
+	So \gls{cse} needs to set \mzninline{b0} to \mzninline{true}.
+\end{example}
+
+\minizinc{} distinguishes not only between root and reified contexts, but in addition recognises constraints in \emph{positive} contexts, also known as \emph{half-reified} \autocite{feydy-2011-half-reif}.
+A full explanation and discussion of half-reification can be found in \cref{ch:half-reif}.
+
+\jip{TODO:\ Reification should also be discussed in the background. How can we
+	make this more specific to how it works in \nanozinc{}.}
+
 \section{An Introduction to Half Reification}
 \label{sec:half-intro}