Work on aggregation in rewriting chapter

assets/shorthands.tex

@@ -17,6 +17,7 @@
 \newcommand{\microzinc}{\gls{microzinc}\xspace{}}
 \newcommand{\minisearch}{\gls{minisearch}\xspace{}}
 \newcommand{\minizinc}{\gls{minizinc}\xspace{}}
+\newcommand{\model}{\gls{model}\xspace{}}
 \newcommand{\nanozinc}{\gls{nanozinc}\xspace{}}
 \newcommand{\parameters}{\glspl{parameter}\xspace{}}
 \newcommand{\parameter}{\gls{parameter}\xspace{}}

chapters/2_background.tex

@@ -1351,9 +1351,12 @@ It, however, will not perform more complex \gls{propagation}, like the \gls{prop
 
 Complex \minizinc\ expression can sometimes result in the creation of many new variables that represent intermediate results.
 This is in particular true for linear and boolean equations that are generally written using \minizinc\ operators.
-For example the evaluation of the linear constraint \mzninline{x + 2*y <= z} could result in the following \flatzinc:
 
-\begin{nzn}
+\begin{example}%
+\label{ex:back-agg}
+	For example the evaluation of the linear constraint \mzninline{x + 2*y <= z} could result in the following \flatzinc:
+
+	\begin{nzn}
 		var int: x;
 		var int: y;
 		var int: z;
@@ -1362,16 +1365,18 @@ For example the evaluation of the linear constraint \mzninline{x + 2*y <= z} cou
 		constraint int_times(y, 2, i1);
 		constraint int_plus(x, i1, i2);
 		constraint int_le(i2, z);
-\end{nzn}
+	\end{nzn}
 
-This \flatzinc\ model is correct, but, at least for pure \gls{cp} solvers, the existence of the intermediate variables is likely to have a negative impact on the \solver{}'s performance.
-These \solvers{} would likely perform better had they directly received the equivalent linear \constraint{}:
+	This \flatzinc\ model is correct, but, at least for pure \gls{cp} solvers, the existence of the intermediate variables is likely to have a negative impact on the \solver{}'s performance.
+	These \solvers{} would likely perform better had they directly received the equivalent linear \constraint{}:
 
-\begin{mzn}
+	\begin{mzn}
 		constraint int_lin_le([1,2,-1], [x,y,z], 0)
-\end{mzn}
+	\end{mzn}
 
-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 \constraint{} directly represents the initial \constraint{} in the \model{} without the use of \glspl{ivar}.
+	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.
+\end{example}
 
 This can be resolved using the \gls{aggregation}.
 When we aggregate constraints we collect multiple \minizinc\ expressions, that would each have been separately translated, and combine them into a singular structure that eliminates the need for intermediate \variables{}.
@@ -1419,11 +1424,11 @@ All other not yet flattened constraints, that could change the relevant \glspl{d
 Note that this heuristic does not guarantee that \variables{} have their tightest possible \gls{domain}.
 One delayed \constraint{} can still influence the \glspl{domain} of \variables{} used by other delayed \constraints{}.
 
-Delaying the rewriting of constraints might, however, interfere with the constraint aggregation.
-Since aggregation is eagerly performed only when a \constraint{} is first encountered, it cannot aggregate any constraints that follow from delayed values.
+Delaying the rewriting of constraints might, however, interfere with the  \gls{aggregation}.
+Since \gls{aggregation} is eagerly performed only when a \constraint{} is first encountered, it cannot aggregate any constraints that follow from delayed values.
 For example, if when aggregating Boolean clauses comes across an expression that needs to be reified, then a new Boolean \variable{} is created and the reified \constraint{} is delayed.
 The problem is, however, that if the definition of this reified constraint turn out to be in terms of Boolean clauses as well, then this definition could have been aggregated as well.
-Because the flattener does not revisit the aggregation of variables, this does not happen.
+Because the flattener does not revisit \gls{aggregation}, this does not happen.
 
 \subsection{FlatZinc Optimisation}%
 \label{subsec:back-fzn-optimisation}

chapters/3_rewriting.tex

@@ -670,38 +670,38 @@ This allows us to disable the \gls{cse} when it is guaranteed to be unnecessary.
 \subsection{Constraint Aggregation}%
 \label{subsec:rew-aggregation}
 
-Complex \minizinc\ expression can sometimes result in the creation of many new variables that represent intermediate results.
-This is in particular true for linear and boolean equations that are generally written using \minizinc\ operators.
-For example the evaluation of the linear constraint \mzninline{x + 2*y <= z} will result in the following \nanozinc:
+In our new system it is still possible to support \gls{aggregation}.
+We aggregate \constraints{} by combining \constraints{} connected through functional definitions, eliminating the need for \glspl{ivar}.
+To aggregate a certain kind of \constraint{}, it is marked as a \gls{native} \constraint{}.
+These \constraints will now be kept as temporary functional definitions in the \nanozinc{} program.
+These functional definitions are kept in the \nanozinc{} program until a top-level (relational) \constraint{} is posted that uses these definitions.
+Once this happens, the interpreter will employ dedicated \gls{aggregation} logic to visit the functional definitions and combine their constraints.
+The top-level \gls{constraint} is then replaced by the combined \gls{constraint}.
+When the \glspl{ivar} become unused, they will be removed using the normal mechanisms.
 
-\begin{nzn}
+\begin{example} For example, let us reconsider the linear constraint from \cref{ex:back-agg}: \mzninline{x + 2*y <= z}.
+	The constraint will result in the following \nanozinc{}:
+
+	\begin{nzn}
 		var int: x;
 		var int: y;
 		var int: z;
 		var int: i1;
-	↳ constraint int_times(y, 2);
+		↳ constraint '*'(y, 2);
 		var int: i2;
-	↳ constraint int_plus(x, i1);
-	constraint int_le(i2, z);
-\end{nzn}
+		↳ constraint '+'(x, i1);
+		constraint '<='(i2, z);
+	\end{nzn}
 
-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.
+	\mzninline{*} and \mzninline{+} were marked as \gls{native} \constraints{} as they can be aggregated into a linear \constraint{}.
+	Their functional definitions are put in place in the \nanozinc{}, and then a top-level \mzninline{<=} \constraint{} is created.
+	The \interpreter{} will then recursively visit the arguments of the \constraints{}.
+	The \constraints{} are then combined into a single linear \constraint{}:
 
-This can be resolved using the \gls{aggregation}.
-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, Boolean logic can be combined into clauses, and counting constraints can be combined into global cardinality constraints.
-
-In \nanozinc{}, we are able to aggregate constraints during partial evaluation.
-To aggregate a certain kind of constraint, the \solver{} must support 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) \gls{constraint} is posted that uses the temporary functional definitions as one of its arguments, the interpreter will employ dedicated \gls{aggregation} logic to visit the functional definitions and combine their constraints.
-The top-level \gls{constraint} is then replaced by the combined \gls{constraint}.
-When the intermediate variables become unused, they will be removed using the normal mechanisms.
-
-\jip{TODO:\ Aggregation is also part of the background. How can we make this more
-	specific to how it works in \nanozinc{}.}
+	\begin{mzn}
+		constraint int_lin_le([1,2,-1], [x,y,z], 0)
+	\end{mzn}
+\end{example}
 
 \section{Experiments}\label{sec:rew-experiments}