Add section on Aggregation

assets/glossary.tex

@@ -9,6 +9,10 @@
 %     program that implements that API},
 % }
 
+\newglossaryentry{aggregation}{
+  name={aggregation},
+  description={},
+}
 
 \newglossaryentry{gls-cbls}{
   name={constraint-based local search},

chapters/1_introduction.tex

@@ -23,7 +23,7 @@ model can be used with any of these solvers, which is achieved through the use
 of solver-specific libraries of constraint definitions. In \minizinc, these
 solver libraries are written in the same language.
 
-\minizinc\ turned out to be much more expressive than expected, so more
+As such, \minizinc\ turned out to be much more expressive than expected, so more
 and more preprocessing and model transformation has been added to both the core
 \minizinc\ library, and users' models. And in addition to one-shot solving,
 \minizinc\ is frequently used as the basis of a larger meta-optimisation tool

chapters/4_rewriting.tex

@@ -755,7 +755,7 @@ by garbage collection in the interpreter. Since our prototype interpreter uses
 reference counting, it already accurately tracks the liveness of each
 identifier.
 
-\subsection{Constraint propagation}
+\subsection{Constraint Propagation}
 
 Another way that variables can become unused is if a constraint can be detected
 to be true based on its semantics, and the known domains of the variables. For
@@ -767,7 +767,7 @@ model without changing satisfiability. This, in turn, may result in
 their auxiliary definitions, if any).
 
 This is a simple form of \gls{propagation}, the main inference method used in
-constraint solvers \autocite{schulte-2008-propagation}. Constraint propagation,
+constraint solvers \autocite{schulte-2008-propagation}. \gls{propagation},
 in general, can not only detect when constraints are trivially true (or false),
 but also tighten variable domains. For instance, given the constraint
 \mzninline{x>y}, with initial domains \mzninline{x in 1..10, y in 1..10}, would
@@ -782,7 +782,7 @@ the \mzninline{abs} function. We therefore need to track whether a variable
 domain has been enforced through external constraints, or is the consequence of
 its own definition. We omit the details of this mechanism for space reasons.
 
-A further effect of constraint propagation is the replacement of constraints by
+A further effect of \gls{propagation} is the replacement of constraints by
 simpler versions. A constraint \mzninline{x=y+z}, where the domain of
 \mzninline{z} has been tightened to the singleton \mzninline{0..0}, can be
 rewritten to \mzninline{x=y}. Propagating the effect of one constraint can thus
@@ -792,12 +792,12 @@ run all propagation rules or algorithms until they reach a fix-point.
 The \nanozinc\ interpreter applies propagation rules for the most important
 constraints, such as linear and Boolean constraints, which can lead to
 significant reductions in generated code size. It has been shown previously that
-applying full constraint propagation during compilation can be beneficial
+applying full \gls{propagation} during compilation can be beneficial
 \autocite{leo-2015-multipass}, in particular when the target solver requires
 complicated reformulations (such as linearisation for MIP solvers
 \autocite{belov-2016-linearisation}).
 
-Returning to the example above, constraint propagation (and other model
+Returning to the example above, \gls{propagation} (and other model
 simplifications) can result in \emph{equality constraints} \mzninline{x=y} being
 introduced. For certain types of target solvers, in particular those based on
 constraint programming, equality constraints can lead to exponentially larger
@@ -850,8 +850,8 @@ equalities to the target constraint solver.
 \paragraph{Implementation}
 
 Rewriting a function call that has a \microzinc\ definition and rewriting a
-constraint due to propagation are very similar. The interpreter therefore simply
-interleaves both forms of rewriting. Efficient constraint propagation engines
+constraint due to \gls{propagation} are very similar. The interpreter therefore simply
+interleaves both forms of rewriting. Efficient \gls{propagation} engines
 ``wake up'' a constraint only when one of its variables has received an update
 (\ie\ when its domain has been shrunk). To enable this, the interpreter needs
 to keep a data structure linking variables to the constraints where they appear
@@ -860,7 +860,7 @@ arguments). These links do not take part in the reference counting.
 
 \subsection{Delayed Rewriting}
 
-Adding constraint propagation and simplification into the rewriting system means
+Adding \gls{propagation} and simplification into the rewriting system means
 that the system becomes non-confluent, and some orders of execution may produce
 ``better'', \ie\ more compact or more efficient, \nanozinc.
 
@@ -888,7 +888,7 @@ that the system becomes non-confluent, and some orders of execution may produce
 For MIP solvers, it is quite important to enforce \emph{tight} bounds in order
 to improve efficiency and sometimes even numerical stability. It would therefore
 be useful to rewrite the \mzninline{lq_zero_if_b} predicate only after all the
-constraint propagation has been performed, in order to take advantage of the
+\gls{propagation} has been performed, in order to take advantage of the
 tightest possible bounds. On the other hand, evaluating a predicate may also
 \emph{impose} new bounds on variables, so it is not always clear which order of
 evaluation is best.
@@ -897,18 +897,18 @@ In our \microzinc/\nanozinc\ system, we allow predicates and functions to be
 \emph{annotated} as potential candidates for \emph{delayed rewriting}. Any
 annotated constraint is handled by the (CallPrimitive) rule rather than the
 (Call) rule, which means that it is simply added as a call into the \nanozinc\
-code, without evaluating its body. When propagation reaches a fix-point, all
-annotations are removed from the current \nanozinc\ program, and evaluation
+code, without evaluating its body. When \gls{propagation} reaches a fix-point,
+all annotations are removed from the current \nanozinc\ program, and evaluation
 resumes with the predicate bodies.
 
 This crucial optimisation enables rewriting in multiple \emph{phases}. For
 example, a model targeted at a 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 constraint propagation, before the Boolean and
+can then be fully simplified by \gls{propagation}, before the Boolean and
 reified constraints are rewritten into lower-level linear primitives suitable
 for MIP\@.
 
-\subsection{\titlecap{\glsentrytext{gls-cse}}}\label{sec:4-cse}
+\subsection{Common Subexpression Elimination}\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
@@ -931,10 +931,10 @@ evaluation even begins, and hoisted into a let expression:
 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:
 
@@ -971,6 +971,10 @@ 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}
+
 \paragraph{Reification}
 
 Many constraint modelling languages, including \minizinc, not only enable
@@ -1025,8 +1029,10 @@ 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}
 
-\subsection{Constraint \titlecap{\glsentrytext{aggregation}}}%
+\subsection{Constraint Aggregation}%
 \label{subsec:rew-aggregation}
 
 Complex \minizinc\ expression can sometimes result in the creation of many new
@@ -1054,7 +1060,7 @@ directly. 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 aggregation of constraints. When we aggregate
+This can be resolved using the \gls{aggregation} of constraints. When we aggregate
 constraints we combine constraints connected through functional definitions into
 one or multiple constraints eliminating the need for intermediate variables. For
 example, the arithmetic definitions can be combined into linear constraints,
@@ -1066,14 +1072,14 @@ aggregate a certain kind of constraint, the solver must the constraint as a
 solver-level primitive. These constraints will now be kept as temporary
 functional definitions in the \nanozinc\ program. Once a top-level (relational)
 constraint is posted that uses the temporary functional definitions as one of
-its arguments, the interpreter will employ dedicated aggregation logic to visit
+its arguments, the interpreter will employ dedicated \gls{aggregation} logic to visit
 the functional definitions and combine their constraints. The top-level
 constraint constraint is then replaced by the combined constraint. When the
 intermediate variables become unused, they will be removed using the normal
 mechanisms.
 
-\jip{TODO: Add the example of aggregating the previous example from the
-  \nanozinc\ to the linear expression.}
+\jip{TODO: Aggregation is also part of the background. How can we make this more
+  specific to how it works in \nanozinc}
 
 \section{Experiments}\label{sec:4-experiments}
 
@@ -1157,18 +1163,20 @@ eliminate all unused variables and constraints: we track all constraints that
 are introduced only to define a variable. This means we can keep an accurate
 count of when a variable becomes unused by counting only the references to a
 variable in constraints that do not help define it. Then, we discuss the use of
-constraint propagation during the partial evaluation of the \nanozinc\ program.
-This technique can help shrink the domains of the decision variable or even
-combine variables known to be equal. When a redefinition of a constraint
-requires the introspection into the current domain of a variable, it is often
-important to have the tightest possible domain. Hence, we discuss how in
-choosing the the next \nanozinc\ constraint to rewrite, the interpreter can
-sometimes delay the rewriting of certain constraints to ensure the most amount
-of information is available. The final optimisation technique, \gls{cse},
-ensures that we do not create or evaluate the same constraint or function twice
-and reuse variables where possible.
-
-\jip{todo: Aggregation}
+\gls{propagation} during the partial evaluation of the \nanozinc\ program. This
+technique can help shrink the domains of the decision variable or even combine
+variables known to be equal. When a redefinition of a constraint requires the
+introspection into the current domain of a variable, it is often important to
+have the tightest possible domain. Hence, we discuss how in choosing the the
+next \nanozinc\ constraint to rewrite, the interpreter can sometimes delay the
+rewriting of certain constraints to ensure the most amount of information is
+available. \Gls{cse}, our next optimisation technique, ensures that we do not
+create or evaluate the same constraint or function twice and reuse variables
+where possible. Finally, the last optimisation technique we discuss is the use
+of constraint \gls{aggregation}. The use of \gls{aggregation} ensures that individual
+functional constraints can be collected and combined into an aggregated form.
+This allows us to avoid the existence of intermediate variables in some cases.
+This optimisation is very important for \gls{mip} solvers.
 
 Finally, we test the described system using a experimental implementation. We
 compare this experimental implementation against the current \minizinc\