Add more parts about MiniZinc

.latexmkrc

···
 @default_files = ('dekker_thesis.tex');
 
 $pdf_mode = 5;
+$dvi_mode = $postscript_mode = 0;
 $bibtex_use = 2;
 $out_dir = 'build';
 

assets/glossary.tex

···
   description={},
 }
 
+\newglossaryentry{array}{
+  name={array},
+  description={},
+}
+
 \newglossaryentry{gls-cbls}{
   name={constraint-based local search},
   description={},
 }
 
+\newglossaryentry{comprehension}{
+  name={comprehension},
+  description={},
+}
+
+\newglossaryentry{conditional}{
+  name={conditional},
+  description={},
+}
 
 \newglossaryentry{constraint}{
   name={constraint},
···
   description={},
 }
 
+\newglossaryentry{generator}{
+  name={generator},
+  description={},
+}
+
 \newglossaryentry{global}{
   name={global constraint},
   description={},
···
   description={},
 }
 
+\newglossaryentry{let}{
+  name={let expression},
+  description={},
+}
+
 \newglossaryentry{linear-programming}{
   name={linear programming},
   description={},
···
   description={},
 }
 
+\newglossaryentry{operator}{
+  name={operators},
+  description={},
+}
+
+\newglossaryentry{optional}{
+  name={optional},
+  description={},
+}
+
 \newglossaryentry{restart}{
   name={restart},
   description={},
···
   name={term rewriting},
   description={},
 }
+
+\newglossaryentry{zinc}{
+  name={Zinc},
+  description={},
+}

assets/shorthands.tex

···
 \newcommand{\minisearch}{\gls{minisearch}\xspace{}}
 \newcommand{\minizinc}{\gls{minizinc}\xspace{}}
 \newcommand{\nanozinc}{\gls{nanozinc}\xspace{}}
+\newcommand{\zinc}{\gls{zinc}\xspace{}}
 \newcommand{\cml}{\gls{constraint-modelling} language\xspace{}}
 \newcommand{\cmls}{\gls{constraint-modelling} languages\xspace{}}
 

chapters/2_background.tex

···
 In a constraint model, instead of specifying the manner in which we can find the
 solution, we give a concise description of the problem. We describe what we
 already know, the \glspl{parameter}, what we wish to know, the \glspl{variable},
-and the relationships that should exists between them, the \glspl{constraint}.
+and the relationships that should exist between them, the \glspl{constraint}.
 
 This type of combinatorial problem is typically called a \gls{csp}. Many \cmls\
 also support the modelling of \gls{cop}, where a \gls{csp} is augmented with an
···
 \autocite{nethercote-2007-minizinc}. Its expressive language and extensive
 library of constraints allow users to easily model complex problems.
 
-Let us introduce the language by modelling the problem from
-\cref{ex:back-knapsack}. A \minizinc\ model encoding this problem is shown in
-\cref{lst:back-mzn-knapsack}.
-
 \begin{listing}
   \mznfile{assets/mzn/back_knapsack.mzn}
   \caption{\label{lst:back-mzn-knapsack} A \minizinc\ model describing a 0-1 knapsack
     problem}
 \end{listing}
 
-The model starts with the declaration of the \glspl{parameter}.
-\Lref{line:back:knap:toys} declares an enumerated type that represents all
-possible toys, \(T\) in the mathematical model in the example.
-\Lref{line:back:knap:joy,line:back:knap:space} declare arrays mapping from toys
-to integer values, these represent the functional mappings \(joy\) and
-\(space\). Finally, \lref{line:back:knap:left} declares an integer
-\gls{parameter} to represent the car capacity as an equivalent to \(C\).
+\begin{example}%
+\label{ex:back-mzn-knapsack}
 
-The model then declares its \glspl{variable}. \Lref{line:back:knap:sel} declares
-the main \gls{variable} \mzninline{selection}, which represents the selection of
-toys to be packed. \(S\) in our earlier model. We also declare the variable
-\mzninline{total_joy}, on \lref{line:back:knap:tj}, which is functionally
-defined to be the summation of all the joy for the toy picked in our selection.
+  Let us introduce the language by modelling the problem from
+  \cref{ex:back-knapsack}. A \minizinc\ model encoding this problem is shown in
+  \cref{lst:back-mzn-knapsack}.
+
+  The model starts with the declaration of the \glspl{parameter}.
+  \Lref{line:back:knap:toys} declares an enumerated type that represents all
+  possible toys, \(T\) in the mathematical model in the example.
+  \Lref{line:back:knap:joy,line:back:knap:space} declare arrays mapping from
+  toys to integer values, these represent the functional mappings \(joy\) and
+  \(space\). Finally, \lref{line:back:knap:left} declares an integer
+  \gls{parameter} to represent the car capacity as an equivalent to \(C\).
+
+  The model then declares its \glspl{variable}. \Lref{line:back:knap:sel}
+  declares the main \gls{variable} \mzninline{selection}, which represents the
+  selection of toys to be packed. \(S\) in our earlier model. We also declare
+  the variable \mzninline{total_joy}, on \lref{line:back:knap:tj}, which is
+  functionally defined to be the summation of all the joy for the toy picked in
+  our selection.
 
-Finally, the model contains a constraint, on \lref{line:back:knap:con}, to
-ensure we do not exceed the given capacity and states the goal for the solver:
-to maximise the value of the variable \mzninline{total_joy}.
+  Finally, the model contains a constraint, on \lref{line:back:knap:con}, to
+  ensure we do not exceed the given capacity and states the goal for the solver:
+  to maximise the value of the variable \mzninline{total_joy}.
+\end{example}
 
 One might note that, although more textual and explicit, the \minizinc\ model
 definition is very similar to our earlier mathematical definition.
···
   \glspl{parameter} and as \glspl{variable}. \minizinc\ is allows all these
   types to be contained in arrays. Unlike other languages, arrays can have a
   user defined index set. Although the index can start at any value the set is
-  forced to be a range. \minizinc\ also has an annotation type, annotations can be either a declared name or a function call. These annotations can be attached to \minizinc\ expressions, declarations, or constraints. }
+  forced to be a range. \minizinc\ also has an annotation type, annotations can
+  be either a declared name or a function call. These annotations can be
+  attached to \minizinc\ expressions, declarations, or constraints. }
+
+\jip{This should explain array types}
 
 \subsection{MiniZinc Expressions}%
 \label{subsec:back-mzn-expr}
 
+One of the powers of the \minizinc\ language is the extensive expression
+language that it offers to help modellers create models that are intuitive to
+read, but are transformed to fit the structure best suited to the chosen
+\gls{solver}. We will now briefly discussed the most important \minizinc\
+expressions and the general methods employed when flattening them. For a
+detailed overview of all \minizinc\ you can consult the full syntactic structure
+of the \minizinc\ expressions in \minizinc\ 2.5.5 can be found in
+\cref{sec:mzn-grammar-expressions}. Nethercote et al.\ and Mariott et al.\ offer
+a detailed discussion of the expression language of \minizinc\ and its
+predecessor \zinc\ respectively
+\autocite*{nethercote-2007-minizinc,marriott-2008-zinc}.
 
-\paragraph{Global Constraints}
-\paragraph{Operators}
-\paragraph{Conditional Expressions}
-\paragraph{Array Operations}
-\paragraph{Set Operations}
-\paragraph{Generator Expressions}
-\paragraph{Let Expressions}
+\Glspl{global} are the basic building blocks in the \minizinc\ language. These
+expressions capture common (complex) relations between variables. \Glspl{global}
+in the \minizinc\ language are used as function calls. An example of a
+\gls{global} is
+
+\begin{mzn}
+predicate knapsack(
+  array [int] of int: w,
+  array [int] of int: p,
+  array [int] of var int: x,
+  var int: W,
+  var int: P,
+);
+\end{mzn}
+
+This \gls{global} expresses the knapsack relationship, where the
+\glspl{parameter} \mzninline{w} are the weights of the items, \mzninline{p} are
+the profit for each items, the \glspl{variable} in \mzninline{x} represent the
+amount of time the items are present in the knapsack, and \mzninline{W} and
+\mzninline{P}, repectively, represent the weight and profit of the knapsack.
+
+Note that the usage of this \gls{global} might have simplified the \minizinc\
+model in \cref{ex:back-mzn-knapsack}:
+
+\begin{mzn}
+  constraint knapsack(toy_space, toy_joy, set2bool(selection), total_joy, space);
+\end{mzn}
+
+The usage of this \gls{global} has the additional benefit that the knapsack
+structure of the problem is then known to the \gls{solver} which might implement
+special handling of the relationship.
+
+Although \minizinc\ contains a extensive library of \glspl{global}, many
+problems contain constraints that aren't covered by a \gls{global}. There are
+many other expression forms in \minizinc\ that can help modellers express a
+constraint.
 
+\Gls{operator} symbols in \minizinc\ are used as short hands for \minizinc\
+functions that can be used to transform or combine other expressions. For
+example the constraint
+
+\begin{mzn}
+constraint not (a + b < c);
+\end{mzn}
+
+contains the infix \glspl{operator} \mzninline{+} and \mzninline{<}, and the
+prefix \gls{operator} \mzninline{not}.
+
+These \glspl{operator} will be evaluated using the addition, less-than
+comparison, and Boolean negation functions respectively. Although the
+\gls{operator} syntax for \glspl{variable} and \glspl{parameter} is the same,
+different (overloaded) versions of these functions will be used during
+flattening. For \glspl{parameter} types the result of the function can be
+directly computed, but when flattening these functions with \glspl{variable}
+types a new variable for its result must be introduced and a constraints
+enforcing the functional relationship.
+
+The choice between different expressions can often be expressed using a
+\gls{conditional} expression, sometimes better known as an ``if-then-else''
+expressions. You could, for example, force that the absolute value of
+\mzninline{a} is bigger than \mzninline{b} using the constraint
+
+\begin{mzn}
+  constraint if b >= 0 then a > b else b < a endif;
+\end{mzn}
+
+In \minizinc\ the result of an \gls{conditional} expression is, however, not
+contained to Boolean types. The condition in the expression, the ``if'', must be
+of a Boolean type, but as long as the different sides of the \gls{conditional}
+expression are the same type it is a valid conditional expression. This can be
+used to, for example, define an absolute value function for integer
+\gls{parameter}:
+
+\begin{mzn}
+  function int: abs(int: a) =
+    if a >= 0 then a else -a endif;
+\end{mzn}
+
+When the condition does not contain any \glspl{variable}, then the flattening of
+a \gls{conditional} expression will result in one of the side of the
+expressions. If, however, the condition does contain a \glspl{variable}, then
+the result of the condition cannot be defined during the flattening. Instead,
+the expression will introduce a new variable for the result of the expression
+and a constraint to enforce the functional relationship. In \minizinc\ special
+\mzninline{if_then_else} \glspl{global} are available to implement this
+relationship.
+
+For the selection of an element from an \gls{array}, instead of between
+different expressions, the \minizinc\ language uses an \gls{array} access syntax
+similar to most other languages. The expression \mzninline{a[i]} selects the
+element with index \mzninline{i} from the array \mzninline{a}. Note this is not
+necessarily the \(\mzninline{i}^{\text{th}}\) element because \minizinc\ allows
+modellers to provide a custom index set.
+
+Like the previous expressions, the selector \mzninline{i} can be both a
+\gls{parameter} or a \gls{variable}. If the expression is a \gls{variable}, then
+the expression is flattened as being an \mzninline{element} function. Otherwise,
+the flattening will replace the \gls{array} access expression by the element
+referenced by expression.
+
+\Gls{array} \glspl{comprehension} are expressions can be used to compose
+\gls{array} objects. This allows modellers to create \glspl{array} that are not
+given directly as input to the model or are a declared collection of variables.
+
+\Gls{generator} expressions, \mzninline{[E | G where F]}, consist of three
+parts:
+
+\begin{description}
+  \item[\mzninline{G}] The generator expression which assigns the values of
+  collections to identifiers,
+  \item[\mzninline{F}] an optional filtering condition, which has to evaluate to
+    \mzninline{true} for the iteration to be included in the array,
+  \item[\mzninline{E}] and the expression that is evaluation for each iteration
+    when the filtering condition succeeds.
+\end{description}
+
+The following example composes a array that contains the doubled even values of
+an \gls{array} \mzninline{x}.
+
+\begin{minizinc}
+  [ xi * 2 | xi in x where x mod 2 == 0]
+\end{minizinc}
+
+The evaluated expression will be added to the new array. This means that the
+type of the array will primarily depend on the type of the expression. However,
+in recent versions of \minizinc\ both the collections over which we iterate and
+the filtering condition could have a  \gls{variable} type. Since we then cannot
+decise during flattening if an element is present in the array, the elements
+will be made of an \gls{optional} type. This means that the solver still will
+decide if the element is present in the array or if it takes a special
+``absent'' value (\mzninline{<>}).
+
+Finally, \glspl{let} are the primary scoping mechanism in the \minizinc\
+language, together with function definitions. A \gls{let} allows a modeller to
+provide a list of definitions, flattened in order, that can be used in its
+resulting definition. There are three main purposes for \glspl{let}:
+
+\begin{enumerate}
+  \item To name an intermediate expression so it can be used multiple times (or
+  to simplify the expression). For example, the constraint 
+
+  \begin{mzn}
+    constraint let { var int: tmp = x div 2; } in tmp mod 2 == 0 \/ tmp = 0;
+  \end{mzn}
+
+  constrains that half of \mzninline{x} is even or zero.
+
+  \item To introduce a scoped \gls{variable}. For example, the constraint
+
+  \begin{mzn}
+    let {var -2..2: slack;} in x + slack = y;
+  \end{mzn}
+
+  constrains that \mzninline{x} and \mzninline{y} are at most two apart.
+
+  \item To constrain the resulting expression. For example, the following function
+
+  \begin{mzn}
+    function var int: int_times(var int: x, var int: y) =
+      let {
+        var int: z;
+        constraint pred_int_times(x, y, z);
+      } in z;
+  \end{mzn}
+
+  returns a new \gls{variable} \mzninline{z} that is constrained to be the
+  multiplication of \mzninline{x} and \mzninline{y} by the relational
+  multiplication constraint \mzninline{pred_int_times}.
+\end{enumerate}
+
+An important detail in flattening \glspl{let} is that any variables that are
+introduced might need to be renamed in the resulting solver level model.
+Different from top-level definitions, the variables declared in \glspl{let} can
+be flattened multiple times when used in loops, function definitions (that are
+called multiple times), and \gls{array} \glspl{comprehension}. In these cases the
+flattener must assign any variables in the \gls{let} a new name and use this
+name in any subsequent definitions and in the resulting expression.
 
 \subsection{Handling Undefined Expressions}%
 \label{subsec:back-mzn-partial}
 
-Some expressions in the \cmls\ do not always have a well defined result.
+Some expressions in the \cmls\ do not always have a well-defined result.
 Examples of such expressions in \minizinc\ are:
 
 \begin{itemize}
   \item Division (or modulus) when the divisor is zero: \\ \mzninline{x div 0 =
-        @??@}
+  @??@}
 
   \item Array access when the index is outside of the given index set: \\
-        \mzninline{array1d(1..3, [1,2,3])[0] = @??@}
+  \mzninline{array1d(1..3, [1,2,3])[0] = @??@}
 
-  \item Finding the minimum or maximum or an empty set: \\ \mzninline{min({}) =
-        @??@}
+  \item Finding the minimum or maximum or an empty set: \\ \mzninline{min({})
+  =@??@}
 
-  \item Computing the square root of a negative value: \\ \mzninline{sqrt(-1) = @??@}
+  \item Computing the square root of a negative value: \\ \mzninline{sqrt(-1) =
+  @??@}
 
 \end{itemize}
 
 The existence of undefined expressions can cause confusion in \cmls. There is
-both the question what happens when a undefined expressions is evaluated and at
-what point during the process undefined values will be resolved, during
+both the question of what happens when an undefined expression is evaluated and
+at what point during the process undefined values will be resolved, during
 flattening or at solving time.
 
 Frisch and Stuckey define three semantic models to deal with the undefinedness
···
 
 \begin{description}
 
-  \item[Strict] \cmls\ employing a ``strict'' undefinedness semantic do not allow any undefined behaviour during the evaluation of the constraint model. If during the flattening or solving process an expression is found to be undefined, then any expressions in which it is used is also marked as undefined. In the end, this means that the occurrence of a single undefined expression will mark the full model as undefined.
+  \item[Strict] \cmls\ employing a ``strict'' undefinedness semantic do not
+    allow any undefined behaviour during the evaluation of the constraint model.
+    If during the flattening or solving process an expression is found to be
+    undefined, then any expressions in which it is used is also marked as
+    undefined. In the end, this means that the occurrence of a single undefined
+    expression will mark the full model as undefined.
 
-  \item[Kleene] The ``Kleene'' semantic treat undefined expressions as expressions for which not enough information is available. This if a expressions contains undefined sub-expression, it will only be marked as undefined if the value of the subexpression is required to compute its result. Take for example the expression \mzninline{false -> E}. Here, when \mzninline{E} is undefined the result of the expression can still be said to be \mzninline{true}, since the value of \mzninline{E} does not influence the result of the expression. However, if we take the expression \mzninline{true /\ E}, then when \mzninline{E} is undefined the overall expression is also undefined since the value of the expression cannot be determined.
+  \item[Kleene] The ``Kleene'' semantic treat undefined expressions as
+    expressions for which not enough information is available. This if an
+    expression contains undefined sub-expression, it will only be marked as
+    undefined if the value of the sub-expression is required to compute its
+    result. Take for example the expression \mzninline{false -> E}. Here, when
+    \mzninline{E} is undefined the result of the expression can still be said to
+    be \mzninline{true}, since the value of \mzninline{E} does not influence the
+    result of the expression. However, if we take the expression \mzninline{true
+    /\ E}, then when \mzninline{E} is undefined the overall expression is also
+    undefined since the value of the expression cannot be determined.
 
-  \item[Relational] The ``relational'' semantic follows from the fact that all expressions in \cmls\ will eventually become part of a relational constraint. So even though a (functional) expression in itself might not have a well-defined result, we can still decide whether its surrounding relationship holds. For example, the expression \mzninline{x div 0} is undefined, but the relationship \mzninline{int_div(x,0,y)} can be said to be \mzninline{false}. It can be said that the relational semantic will make the closest relational expression that contains an undefined expression \mzninline{false}.
+  \item[Relational] The ``relational'' semantic follows from the fact that all
+    expressions in \cmls\ will eventually become part of a relational
+    constraint. So even though a (functional) expression in itself might not
+    have a well-defined result, we can still decide whether its surrounding
+    relationship holds. For example, the expression \mzninline{x div 0} is
+    undefined, but the relationship \mzninline{int_div(x,0,y)} can be said to be
+    \mzninline{false}. It can be said that the relational semantic will make the
+    closest relational expression that contains an undefined expression
+    \mzninline{false}.
 
 \end{description}
 
···
 the users of constraint modelling languages. This is why the \minizinc\ uses
 relational semantics during its evaluation.
 
-For example, one might might deal with a zero divisor using a disjunction:
+For example, one might deal with a zero divisor using a disjunction:
 
 \begin{mzn}
   constraint d == 0 \/ a div d < 3;
···
 
 In this case we expect the undefinedness of the division to be contained within
 the second part of the disjunction. This corresponds to ``relational''
-semantics. \jip{TODO:\@ This also corresponds to Kleene semantics, maybe I should
-  use a different example}
+semantics. \jip{TODO:\@ This also corresponds to Kleene semantics, maybe I
+should use a different example}
 
 Frisch and Stuckey also show that different \glspl{solver} often employ
-different semantical models \autocite*{frisch-2009-undefinedness}. It is
+different semantics \autocite*{frisch-2009-undefinedness}. It is
 therefore important that, during the flattening process, any potentially
 undefined expression gets replaced by an equivalent model that is still valid
 under a strict semantic. Essentially eliminating the existence of undefined

chapters/3_rewriting.tex

···
 
 In this chapter, we revisit the rewriting of high-level \cmls\ into solver-level
 constraint models. We describe a new \textbf{systematic view of the execution of
-  \minizinc{}} and build on this to propose a new tool chain. We show how this
+\minizinc{}} and build on this to propose a new tool chain. We show how this
 tool chain allows us to:
 
 \begin{itemize}
···
 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.
+\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
···
 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:
+2*y <= z} will result in the following \nanozinc:
 
 \begin{nzn}
   var int: x;
···
 additional burden to have intermediate values that have to be given a value in
 the solution.
 
-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,
-Boolean logic can be combined into clauses, and counting constraints can be
-combined into global cardinality constraints.
+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, 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 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 \gls{aggregation} logic to visit
-the functional definitions and combine their constraints. The top-level
+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.
···
 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.
+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\