diff --git a/assets/shorthands.tex b/assets/shorthands.tex
index 190b3ad..6671b95 100644
--- a/assets/shorthands.tex
+++ b/assets/shorthands.tex
@@ -1,13 +1,23 @@
 \newcommand{\eg}{e.g.,\xspace{}}
 \newcommand{\ie}{i.e.,\xspace{}}
+
+\newcommand{\cmls}{\gls{constraint-modelling} languages\xspace{}}
+\newcommand{\cml}{\gls{constraint-modelling} language\xspace{}}
+\newcommand{\constraints}{\glspl{constraint}\xspace{}}
+\newcommand{\constraint}{\gls{constraint}\xspace{}}
 \newcommand{\flatzinc}{\gls{flatzinc}\xspace{}}
 \newcommand{\microzinc}{\gls{microzinc}\xspace{}}
 \newcommand{\minisearch}{\gls{minisearch}\xspace{}}
 \newcommand{\minizinc}{\gls{minizinc}\xspace{}}
 \newcommand{\nanozinc}{\gls{nanozinc}\xspace{}}
+\newcommand{\parameters}{\glspl{parameter}\xspace{}}
+\newcommand{\parameter}{\gls{parameter}\xspace{}}
+\newcommand{\solvers}{\glspl{solver}\xspace{}}
+\newcommand{\solver}{\gls{solver}\xspace{}}
+\newcommand{\variables}{\glspl{variable}\xspace{}}
+\newcommand{\variable}{\gls{variable}\xspace{}}
 \newcommand{\zinc}{\gls{zinc}\xspace{}}
-\newcommand{\cml}{\gls{constraint-modelling} language\xspace{}}
-\newcommand{\cmls}{\gls{constraint-modelling} languages\xspace{}}
+
 
 \renewcommand{\phi}{\varphi}
 \newcommand{\tuple}[1]{\ensuremath{\langle #1 \rangle}}
diff --git a/chapters/2_background.tex b/chapters/2_background.tex
index 3452d21..e0fda3d 100644
--- a/chapters/2_background.tex
+++ b/chapters/2_background.tex
@@ -19,20 +19,20 @@ that a constraint model actually describes the solution to the problem.
 
 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 exist between them, the \glspl{constraint}.
+already know, the \parameters{}, what we wish to know, the \variables{}, and the
+relationships that should exist between them, the \constraints{}.
 
 This type of combinatorial problem is typically called a \gls{csp}. The goal of
-a \gls{csp} is to find values for the \glspl{variable} that satisfy the
-\glspl{constraint} or prove that no such assignment exists. Many \cmls\ also
-support the modelling of \gls{cop}, where a \gls{csp} is augmented with a
+a \gls{csp} is to find values for the \variables{} that satisfy the
+\constraints{} or prove that no such assignment exists. Many \cmls\ also support
+the modelling of \gls{cop}, where a \gls{csp} is augmented with a
 \gls{objective} \(z\). In this case the goal is to find a solution that
-satisfies all \glspl{constraint} while minimising (or maximising) \(z\).
+satisfies all \constraints{} while minimising (or maximising) \(z\).
 
 Although a constraint model does not contain any instructions to find a suitable
 solution, these models can generally be given to a dedicated solving program, or
-\gls{solver} for short, that can find a solution that fits the requirements of
-the model.
+\solver{} for short, that can find a solution that fits the requirements of the
+model.
 
 \begin{listing}
   \pyfile{assets/py/2_dyn_knapsack.py}
@@ -45,10 +45,10 @@ the model.
 
   Let us consider the following scenario: Packing for a weekend trip, I have to
   decide which toys to bring for my dog, Audrey. We only have a small amount of
-  space left in the car, so we cannot bring all the toys. Since Audrey gets
-  enjoys playing with some toys more than others, we can now try and pick the
-  toys that bring Audrey the most amount of joy, but still fit in the car.
-  The following set of equations describe this knapsack problem as a \gls{cop}:
+  space left in the car, so we cannot bring all the toys. Since Audrey gets enjoys
+  playing with some toys more than others, we can now try and pick the toys that
+  bring Audrey the most amount of joy, but still fit in the car. The following set
+  of equations describe this knapsack problem as a \gls{cop}:
 
   \begin{equation*}
     \text{maximise}~z~\text{subject to}~
@@ -59,20 +59,20 @@ the model.
     \end{cases}
   \end{equation*}
 
-  In these equations \(S\) is set \gls{variable}. It contains the selection of
-  toys that will be packed for the trip. \(z\) is the objective \gls{variable}
-  that is maximised to find the optimal selections of toys to pack. The
-  \gls{parameter} \(T\) is the set of all the toys. The \(joy\) and \(space\)
-  functions are \glspl{parameter} used to map toys, \( t \in T\), to a value
-  depicting the amount of enjoyment and space required respectively. Finally,
-  the \gls{parameter} \(C\) is that depicts the total space that is left in the
-  car before packing the toys.
+  In these equations \(S\) is set \variable{}. It contains the selection of toys
+  that will be packed for the trip. \(z\) is the objective \variable{} that is
+  maximised to find the optimal selections of toys to pack. The \parameter{}
+  \(T\) is the set of all the toys. The \(joy\) and \(space\) functions are
+  \parameters{} used to map toys, \( t \in T\), to a value depicting the amount
+  of enjoyment and space required respectively. Finally, the \parameter{} \(C\)
+  is that depicts the total space that is left in the car before packing the
+  toys.
 
   This constraint model gives an abstract mathematical definition of the
   \gls{cop} that would be easy to adjust to changes in the requirements. To
   solve instances of this problem, however, these instances have to be
-  transformed into input accepted by a \gls{solver}. \cmls{} are designed to
-  allow the modeller to express combinatorial problems similar to the above
+  transformed into input accepted by a \solver{}. \cmls{} are designed to allow
+  the modeller to express combinatorial problems similar to the above
   mathematical definition and generate a definition that can be used by
   dedicated solvers.
 
@@ -110,32 +110,32 @@ library of constraints allow users to easily model complex problems.
   \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}.
+  The model starts with the declaration of the \parameters{}.
   \Lref{line:back:knap:toys} declares an enumerated type that represents all
   possible toys, \(T\) in the mathematical model in the example.
   \Lrefrange{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\).
+  \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 \gls{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.
+  The model then declares its \variables{}. \Lref{line:back:knap:sel} declares
+  the main \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 \gls{variable} \mzninline{total_joy}.
+  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.
 
-Given ground assignments to input \glspl{parameter}, a \minizinc\ model is
-translated (via a process called \emph{flattening}) into a set of
-\glspl{variable} and primitive constraints.
+Given ground assignments to input \parameters{}, a \minizinc\ model is
+translated (via a process called \emph{flattening}) into a set of \variables{}
+and primitive constraints.
 
 Given the assignments
 
@@ -158,8 +158,8 @@ constraint int_lin_eq([63,12,100,-1],[selection_0,selection_1,selection_2,total_
 solve maximize total_joy;
 \end{mzn}
 
-This \emph{flat} problem will be passed to some \gls{solver}, which will attempt
-to determine an assignment to each \gls{variable} \mzninline{solection_i} and
+This \emph{flat} problem will be passed to some \solver{}, which will attempt to
+determine an assignment to each \variable{} \mzninline{solection_i} and
 \mzninline{total_joy} that satisfies all constraints and maximises
 \mzninline{total_joy}, or report that there is no such assignment.
 
@@ -167,19 +167,19 @@ to determine an assignment to each \gls{variable} \mzninline{solection_i} and
 \label{subsec:back-mzn-structure}
 
 As we have seen in \cref{ex:back-mzn-knapsack}, a \minizinc\ model generally
-contains value declarations, both for \glspl{variable} and input
-\glspl{parameter}, \glspl{constraint}, and a solving goal. More complex models
-might also include definitions for custom types, user defined functions, and a
-custom output format. In \minizinc\ these items are not constrained to occur in
-any particular order. We will briefly discuss the most important model items.
-For a detailed overview of the structure of \minizinc\ models you can consult
-the full syntactic structure of \minizinc\ 2.5.5 in \cref{ch:minizinc-grammar}.
+contains value declarations, both for \variables{} and input \parameters{},
+\constraints{}, and a solving goal. More complex models might also include
+definitions for custom types, user defined functions, and a custom output
+format. In \minizinc\ these items are not constrained to occur in any particular
+order. We will briefly discuss the most important model items. For a detailed
+overview of the structure of \minizinc\ models you can consult the full
+syntactic structure of \minizinc\ 2.5.5 in \cref{ch:minizinc-grammar}.
 Nethercote et al.\ and Mariott et al.\ offer a detailed discussion of the
 \minizinc\ and \zinc\ language, its predecessor, respectively
 \autocite*{nethercote-2007-minizinc,marriott-2008-zinc}.
 
 Values in \minizinc\ are declared in the form \mzninline{@\(T\)@: @\(I\)@ =
-@\(E\)@;}. \(T\) is the type of the declared value, \(I\) is a new identifier
+  @\(E\)@;}. \(T\) is the type of the declared value, \(I\) is a new identifier
 used to reference the declared value, and, optionally, the modeller can
 functionally define the value using an expression \(E\). The identifier used in
 a top-level value definition must be unique. Two declarations with the same
@@ -187,11 +187,11 @@ identifier will result in an error during the flattening process.
 
 The main types used in \minizinc\ are Boolean, integer, floating point numbers,
 sets of integers, and (user-defined) enumerated types. These types can be used
-both as normal \glspl{parameter} and as \glspl{variable}. To better structure
-models, \minizinc\ allows collections of these types to be contained in arrays.
-Unlike other languages, arrays can have a user defined index set, which can
-start at any value, but has to be a continuous range. For example, an array
-going from 5 to 10 of new boolean \glspl{variable} might be declared as
+both as normal \parameters{} and as \variables{}. To better structure models,
+\minizinc\ allows collections of these types to be contained in arrays. Unlike
+other languages, arrays can have a user defined index set, which can start at
+any value, but has to be a continuous range. For example, an array going from 5
+to 10 of new boolean \variables{} might be declared as
 
 \begin{mzn}
   array[5..10] of var bool: bs;
@@ -200,25 +200,25 @@ going from 5 to 10 of new boolean \glspl{variable} might be declared as
 The type in a declaration can, however, be more complex when the modeller uses a
 type expression. These expressions constrain a declaration, not just to a
 certain type, but also to a set of value. This set of values is generally
-referred to as the \gls{domain} of a \gls{variable}. In \minizinc\ any
-expression that has a set type can be used as a type expression. For example,
-the following two declarations
+referred to as the \gls{domain} of a \variable{}. In \minizinc\ any expression
+that has a set type can be used as a type expression. For example, the following
+two declarations
 
 \begin{mzn}
   var 3..5: x;
   var {1,3,5}: y;
 \end{mzn}
 
-declare two integer \glspl{variable} that can take the values from three to five and
+declare two integer \variables{} that can take the values from three to five and
 one, three, and five respectively.
 
 If the declaration includes an expression to functionally define the value, then
 the identifier can be used as a name for this expression. If, however, the type
 of the declaration is given as a type expression, then this places an implicit
-\gls{constraint} on the expression, forcing the result of the expression to take
-a value according to the type expression.
+\constraint{} on the expression, forcing the result of the expression to take a
+value according to the type expression.
 
-\gls{constraint} items, \mzninline{constraint @\(E\)@;} contain the top-level
+\constraint{} items, \mzninline{constraint @\(E\)@;} contain the top-level
 constraint of the \minizinc\ model. A constraint item contains only a single
 expression \(E\) of Boolean type. During the flattening of the model the
 expressions in constraints are translated into solver level versions of the same
@@ -227,11 +227,11 @@ are equisatisfiable, meaning they are only satisfied if-and-only-if the original
 expression would have been satisfied.
 
 A \minizinc\ model can contain a single goal item. This item can signal the
-solver to do one of three actions: to find an assignment to the \glspl{variable}
+solver to do one of three actions: to find an assignment to the \variables{}
 that satisfies the constraints, \mzninline{solve satisfy;}, to find an
-assignment to the \glspl{variable} that satisfies the constraints and minimises
-the value of a \gls{variable}, \mzninline{solve minimize x;}, or similarly
-maximises the value of a \gls{variable}, \mzninline{solve maximize x;}.
+assignment to the \variables{} that satisfies the constraints and minimises the
+value of a \variable{}, \mzninline{solve minimize x;}, or similarly maximises
+the value of a \variable{}, \mzninline{solve maximize x;}.
 
 \jip{TODO:\@ add some information about search in \minizinc{}. It's probably
   pretty relevant.}
@@ -251,11 +251,11 @@ integer can be defined as follows.
   function int: square(int: a) = a * a;
 \end{mzn}
 
-Function declarations are also the main way in which \gls{solver} libraries are
+Function declarations are also the main way in which \solver{} libraries are
 defined. During flattening all \minizinc\ expressions are (eventually) rewritten
 to function calls. A solver can then provide its own implementation for these
 functions. It is assumed that the implementation of the functions in the
-\gls{solver} libraries will ultimately be rewritten into fully relational call.
+\solver{} libraries will ultimately be rewritten into fully relational call.
 When a relational constraint is directly supported by a solver the function
 should be declared within an expression body. Any call to such function is
 directly placed in the flattened model.
@@ -266,16 +266,16 @@ directly placed in the flattened model.
 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 discuss the most important \minizinc\
-expressions and the general methods employed when flattening them. A detailed
-overview of 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
+\solver{}. We will now briefly discuss the most important \minizinc\ expressions
+and the general methods employed when flattening them. A detailed overview of
+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}.
 
 \Glspl{global} are the basic building blocks in the \minizinc\ language. These
-expressions capture common (complex) relations between \glspl{variable}.
+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}
@@ -288,11 +288,11 @@ predicate knapsack(
 );
 \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 item, the \glspl{variable} in \mzninline{x} represent the
-amount of time the items are present in the knapsack, and \mzninline{W} and
-\mzninline{P}, respectively, represent the weight and profit of the knapsack.
+This \gls{global} expresses the knapsack relationship, where the \parameters{}
+\mzninline{w} are the weights of the items, \mzninline{p} are the profit for
+each item, the \variables{} in \mzninline{x} represent the amount of time the
+items are present in the knapsack, and \mzninline{W} and \mzninline{P},
+respectively, 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}:
@@ -302,7 +302,7 @@ model in \cref{ex:back-mzn-knapsack}:
 \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
+structure of the problem is then known to the \solver{} which might implement
 special handling of the relationship.
 
 Although \minizinc\ contains an extensive library of \glspl{global}, many
@@ -323,12 +323,12 @@ 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 \gls{variable} for its result must be introduced and a constraint
-enforcing the functional relationship.
+\gls{operator} syntax for \variables{} and \parameters{} is the same, different
+(overloaded) versions of these functions will be used during flattening. For
+\parameters{} types the result of the function can be directly computed, but
+when flattening these functions with \variables{} types a new \variable{} for
+its result must be introduced and a constraint 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''
@@ -344,19 +344,19 @@ 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}:
+\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 \gls{variable}, then the
-result of the condition cannot be defined during the flattening. Instead, the
-expression will introduce a new \gls{variable} for the result of the expression
-and a constraint to enforce the functional relationship. In \minizinc\ special
+When the condition does not contain any \variables{}, 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 \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.
 
@@ -368,15 +368,15 @@ 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
+\parameter{} or a \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
-\glspl{variable}.
+\variables{}.
 
 \Gls{generator} expressions, \mzninline{[E | G where F]}, consist of three
 parts:
@@ -400,7 +400,7 @@ values of an \gls{array} \mzninline{x}.
 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
+the filtering condition could have a \variable{} type. Since we then cannot
 decide during flattening if an element is present in the array, the elements
 will be made of a \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
@@ -421,7 +421,7 @@ resulting definition. There are three main purposes for \glspl{let}:
 
   constrains that half of \mzninline{x} is even or zero.
 
-  \item To introduce a scoped \gls{variable}. For example, the constraint
+  \item To introduce a scoped \variable{}. For example, the constraint
 
   \begin{mzn}
     let {var -2..2: slack;} in x + slack = y;
@@ -440,28 +440,28 @@ resulting definition. There are three main purposes for \glspl{let}:
       } in z;
   \end{mzn}
 
-  returns a new \gls{variable} \mzninline{z} that is constrained to be the
+  returns a new \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 \glspl{variable} that
+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 \glspl{variable} declared in
+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
-\glspl{variable} in the \gls{let} a new name and use this name in any subsequent
+\variables{} in the \gls{let} a new name and use this name in any subsequent
 definitions and in the resulting expression.
 
 \subsection{Reification}%
 \label{subsec:back-reification}
 
-With the rich expression language in \minizinc{}, \glspl{constraint} can consist
+With the rich expression language in \minizinc{}, \constraints{} can consist
 of complex expressions that do not translate to a single constraint at the
-\gls{solver} level. Instead different parts of a complex expression will be
-translated into different \glspl{constraint}. Not all of these constraint will
-be globally enforced by the solver. \Glspl{constraint} stemming for
+\solver{} level. Instead different parts of a complex expression will be
+translated into different \constraints{}. Not all of these constraint will
+be globally enforced by the solver. \constraints{} stemming for
 sub-expressions will typically be \emph{reified} into a Boolean variable.
 \Gls{reification} means that a variable \mzninline{b} is constrained to be true
 if and only if a corresponding constraint \mzninline{c(...)} holds.
@@ -595,44 +595,43 @@ 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}
 
-Frisch and Stuckey also show that different \glspl{solver} often employ
-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
-expressions in the \gls{solver} model.
+Frisch and Stuckey also show that different \solvers{} often employ 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 expressions in the \solver{}
+model.
 
 \section{Solving Constraint Models}%
 \label{sec:back-solving}
 
-There are many prominent techniques to solve a \gls{constraint} model, but none
-of them will solve a \minizinc\ model directly. Instead a \minizinc\ model get
-translated into \glspl{variable} and \glspl{constraint} of the type that the
-solver supports directly.
+There are many prominent techniques to solve a \constraint{} model, but none of
+them will solve a \minizinc\ model directly. Instead a \minizinc\ model get
+translated into \variables{} and \constraints{} of the type that the solver
+supports directly.
 
-\minizinc\ was initially designed as an input language for \gls{cp}
-\glspl{solver}. These \glspl{solver} often support many of the high-level
-\glspl{constraint} that are written in a \minizinc\ model. For \gls{cp} solvers
-the amount of translation required can vary a lot. It depends on which
-\glspl{constraint} the targeted \gls{cp} \gls{solver} are directly supported and
-which \glspl{constraint} have to be decomposed.
+\minizinc\ was initially designed as an input language for \gls{cp} \solvers{}.
+These \glspl{solver} often support many of the high-level \constraints{} that
+are written in a \minizinc\ model. For \gls{cp} solvers the amount of
+translation required can vary a lot. It depends on which \constraints{} the
+targeted \gls{cp} \solver{} are directly supported and which \constraints{} have
+to be decomposed.
 
-Because \gls{cp} \glspl{solver} work on a similar level as the \minizinc\
-language, some of the techniques used in \gls{cp} \glspl{solver} can also be
-used during the transformation from \minizinc\ to \flatzinc{}. The usage of
-these techniques can often help shrink the \glspl{domain} of \glspl{variable}
-and eliminate or simplify \gls{constraint}. \Cref{subsec:back-cp} explains the
-general method employed by \gls{cp} \glspl{solver} to solve a \gls{constraint}
-model.
+Because \gls{cp} \solvers{} work on a similar level as the \minizinc\ language,
+some of the techniques used in \gls{cp} \solvers{} can also be used during the
+transformation from \minizinc\ to \flatzinc{}. The usage of these techniques can
+often help shrink the \glspl{domain} of \variables{} and eliminate or simplify
+\constraint{}. \Cref{subsec:back-cp} explains the general method employed by
+\gls{cp} \solvers{} to solve a \constraint{} model.
 
 Throughout the years \minizinc\ has seen the addition of solvers using other
-approaches to finding solutions to \gls{constraint} models. Although these
-\glspl{solver} bring new classes of problems that can be solved using
-\minizinc{}, they also bring new challenges in to efficiently encode the problem
-for these \glspl{solver}. To understand these challenges in the translations a
-\minizinc\ model into a solver level \gls{constraint} model, the remainder of
-this section will discuss the other dominant technologies used used by
-\minizinc\ \gls{solver} targets and their input language.
+approaches to finding solutions to \constraint{} models. Although these
+\solvers{} bring new classes of problems that can be solved using \minizinc{},
+they also bring new challenges in to efficiently encode the problem for these
+\solvers{}. To understand these challenges in the translations a \minizinc\
+model into a solver level \constraint{} model, the remainder of this section
+will discuss the other dominant technologies used used by \minizinc\ \solver{}
+targets and their input language.
 
 \subsection{Constraint Programming}%
 \label{subsec:back-cp}
@@ -640,7 +639,7 @@ this section will discuss the other dominant technologies used used by
 
 When given a \gls{csp}, one might wonder what the best way is to find a solution
 to the problem. The simplest solution would be to apply ``brute force'': try
-every value in the \gls{domain} all \glspl{variable}. It will not surprise the
+every value in the \gls{domain} all \variables{}. It will not surprise the
 reader that this is an inefficient approach. Given, for example, the constraint
 
 \begin{mzn}
@@ -650,62 +649,62 @@ constraint a + b = 5;
 It is clear that when the value \mzninline{a} is known, then the value of
 \mzninline{b} can be deduced. \gls{cp} is the idea solving \glspl{csp} by
 performing an intelligent search by inferring which which values are still
-feasible for each \gls{variable} \autocite{rossi-2006-cp}.
+feasible for each \variable{} \autocite{rossi-2006-cp}.
 
-To find a solution to a given \gls{csp}, a \gls{cp} \gls{solver} will perform a
-depth first search. At each node, the \gls{solver} will try and eliminate any
+To find a solution to a given \gls{csp}, a \gls{cp} \solver{} will perform a
+depth first search. At each node, the \solver{} will try and eliminate any
 impossible value using a process called \gls{propagation}. For each
-\gls{constraint} the \gls{solver} has a chosen algorithm called a
-\gls{propagator}. Triggered by changes in the \glspl{domain} of its
-\glspl{variable}, the \gls{propagator} will analyse and prune the any values
-that are proven to be inconsistent.
+\constraint{} the \solver{} has a chosen algorithm called a \gls{propagator}.
+Triggered by changes in the \glspl{domain} of its \variables{}, the
+\gls{propagator} will analyse and prune the any values that are proven to be
+inconsistent.
 
 In the best case scenario, \gls{propagation} will eliminate all impossible value
-and all \glspl{variable} have been fixed to a single value. In this case we have
+and all \variables{} have been fixed to a single value. In this case we have
 arrived at a solution. Often, \gls{propagation} alone will not be enough to find
 a solution to the problem. Instead, when no more \glspl{propagator} are
-triggered (we have reached a \gls{fixpoint}), the \gls{solver} has to make a
-search decision. It will fix a \gls{variable} to a value or add a new
-\gls{constraint}. This search decision is an assumption made by the \gls{solver}
-in the hope of finding a solution. If no solution is found using the search
-decision, then it needs to try making the opposite decision: excluding the
-chosen value or adding the opposite constraint.
+triggered (we have reached a \gls{fixpoint}), the \solver{} has to make a search
+decision. It will fix a \variable{} to a value or add a new \constraint{}. This
+search decision is an assumption made by the \solver{} in the hope of finding a
+solution. If no solution is found using the search decision, then it needs to
+try making the opposite decision: excluding the chosen value or adding the
+opposite constraint.
 
 Note that the important difference between values \gls{propagation} and making
 search decisions is that value excluded by a \gls{propagator} are guaranteed to
 not occur in any solution, but values excluded by a search heuristic are merely
-removed locally and might still be part of a solution. A \gls{cp} \gls{solver}
-is only able to prove that the problem is unsatisfiable by exploring the full
+removed locally and might still be part of a solution. A \gls{cp} \solver{} is
+only able to prove that the problem is unsatisfiable by exploring the full
 search space.
 
 \Gls{propagation} is not only used when starting the search, but also after
 making each search decision. This means that some of the \gls{propagation}
-depends on the search decision. Therefore, if the \gls{solver} needs to
-reconsider a search decision, then it must also undo all \gls{domain} changes
-that were caused by \gls{propagation} dependent on that search decision.
+depends on the search decision. Therefore, if the \solver{} needs to reconsider
+a search decision, then it must also undo all \gls{domain} changes that were
+caused by \gls{propagation} dependent on that search decision.
 
-The general most common method in \gls{cp} \glspl{solver} to achieve this is to
-keep track of \gls{domain} changes using a \gls{trail}. For every \gls{domain}
-change that is made during propagation (after the first search decision), the
-reverse change is stored on in a list. Whenever a new search decision is made,
-the current position of the list is tagged. If the \gls{solver} now needs to
-undo a search decision (\ie\ \gls{backtrack}), it can apply all change until it
-reaches the change that is tagged with the search decision. Because all changes
-before the tagged point on the \gls{trail} were made before the search decision
-was made, it is guaranteed that these \gls{domain} changes do not depend on the
+The general most common method in \gls{cp} \solvers{} to achieve this is to keep
+track of \gls{domain} changes using a \gls{trail}. For every \gls{domain} change
+that is made during propagation (after the first search decision), the reverse
+change is stored on in a list. Whenever a new search decision is made, the
+current position of the list is tagged. If the \solver{} now needs to undo a
+search decision (\ie\ \gls{backtrack}), it can apply all change until it reaches
+the change that is tagged with the search decision. Because all changes before
+the tagged point on the \gls{trail} were made before the search decision was
+made, it is guaranteed that these \gls{domain} changes do not depend on the
 search decision. Furthermore, because propagation is performed to a
 \gls{fixpoint}, it is guaranteed that no duplicate propagation is required.
 
-The solving method used by \gls{cp} \glspl{solver} is very flexible. A
-\gls{solver} can support many different types of \glspl{variable}: they can
-range from Boolean, floating point numbers, and integers, to intervals, sets,
-and functions. Similarly, \glspl{solver} do not all have access to the same
-propagators. Therefore, a \gls{csp} modelled for one \gls{solver} might look
-very different to an equivalent \gls{csp} modelled for a different solver.
-Instead, \cmls{}, like \minizinc{}, can serve as a standardised form of input
-for these \glspl{solver}. They allow modellers to use high-level constraints
-that are used directly by the solver when supported or they are automatically
-translated to a collection of equivalent supported constraints otherwise.
+The solving method used by \gls{cp} \solvers{} is very flexible. A \solver{} can
+support many different types of \variables{}: they can range from Boolean,
+floating point numbers, and integers, to intervals, sets, and functions.
+Similarly, \solvers{} do not all have access to the same propagators. Therefore,
+a \gls{csp} modelled for one \solver{} might look very different to an
+equivalent \gls{csp} modelled for a different solver. Instead, \cmls{}, like
+\minizinc{}, can serve as a standardised form of input for these \solvers{}.
+They allow modellers to use high-level constraints that are used directly by the
+solver when supported or they are automatically translated to a collection of
+equivalent supported constraints otherwise.
 
 \begin{example}%
 \label{ex:back-nqueens}
@@ -725,16 +724,15 @@ one queen per diagonal. The problem can be modelled in \minizinc\ as follows.
 
 Since we know that there can only be one queen per column, the decision in the
 model left to make is, for every queen, where in the column the piece is placed.
-The \glspl{constraint} in the model model the remaining rules of the problem: no
-two queen can be placed in the same row, no two queen can be place in the same
+The \constraints{} in the model model the remaining rules of the problem: no two
+queen can be placed in the same row, no two queen can be place in the same
 upward diagonal, and no two queens can be place in the same downward diagonal.
-This model can be directly used in most \gls{cp} \glspl{solver}, since integer
-\glspl{variable} and an \mzninline{all_different} \gls{propagator} are common.
+This model can be directly used in most \gls{cp} \solvers{}, since integer
+\variables{} and an \mzninline{all_different} \gls{propagator} are common.
 
 When solving the problem, initially no values can be eliminated from the
-\glspl{domain} of the \glspl{variable}. The first propagation will happen when
-the first queen is placed on the board. The search space will then look like
-this:
+\glspl{domain} of the \variables{}. The first propagation will happen when the
+first queen is placed on the board. The search space will then look like this:
 
 \jip{insert image of nqueens board with one queen assigned.}
 
@@ -750,8 +748,8 @@ board.
 In \gls{cp} solving there is a trade-off between the amount of time spend
 propagating a constraint and the the amount of search that is otherwise
 required. The golden standard for a \gls{propagator} is to be \gls{domain-con},
-meaning that all values left in the \glspl{domain} of its \glspl{variable} there
-is at least one possible variable assignment that satisfies the constraint.
+meaning that all values left in the \glspl{domain} of its \variables{} there is
+at least one possible variable assignment that satisfies the constraint.
 Designing an algorithm that reaches this level of consistency is, however, an
 easy task and might require high complexity. Instead it can sometimes be better
 to use a propagator with a lower level of consistency. Although it might not
@@ -760,25 +758,24 @@ eliminated might take less time than achieving \gls{domain-con}.
 
 This is, for example, the case for integer linear constraints:
 \[ \sum_{i} c_{i} x_{i} = d\] where \(c_{i}\) and \(d\) are integer
-\glspl{parameter} and \(x_{i}\) are integer \gls{variable}. For these
-constraints, no realistic \gls{domain-con} \gls{propagator} exists. Instead
-\glspl{solver} generally use a \gls{bounds-con} \gls{propagator}, which
-guarantee only that the minimum and maximum values in the \glspl{domain} of the
-\glspl{variable} are used in at least one possible assignment that satisfies the
-constraint.
+\parameters{} and \(x_{i}\) are integer \variable{}. For these constraints, no
+realistic \gls{domain-con} \gls{propagator} exists. Instead \solvers{} generally
+use a \gls{bounds-con} \gls{propagator}, which guarantee only that the minimum
+and maximum values in the \glspl{domain} of the \variables{} are used in at
+least one possible assignment that satisfies the constraint.
 
 Thus far, we have only considered \glspl{csp}. \gls{cp} solving can, however,
 also be used to solve optimisation problems using a method called \gls{bnb}. The
-\gls{cp} \gls{solver} will follow the same method as previously described.
-However, when it find a solution, it does not yet know if this solution is
-optimal. It is merely an incumbent solution. The \gls{solver} must therefore
-resume its search, but it is no longer interested in just any solution, only
-solutions that have a better \gls{objective} value. This is achieved by adding a
-new \gls{propagator} that enforces all solutions to have a better
-\gls{objective} value than the incumbent solution. If the search process finds
-another solution, then the incumbent solution is updated and the search process
-continues. If the search process does not find any other solutions, then it is
-proven that there are no better solutions than the current incumbent solution.
+\gls{cp} \solver{} will follow the same method as previously described. However,
+when it find a solution, it does not yet know if this solution is optimal. It is
+merely an incumbent solution. The \solver{} must therefore resume its search,
+but it is no longer interested in just any solution, only solutions that have a
+better \gls{objective} value. This is achieved by adding a new \gls{propagator}
+that enforces all solutions to have a better \gls{objective} value than the
+incumbent solution. If the search process finds another solution, then the
+incumbent solution is updated and the search process continues. If the search
+process does not find any other solutions, then it is proven that there are no
+better solutions than the current incumbent solution.
 
 \gls{cp} solvers like Chuffed \autocite{chuffed-2021-chuffed}, Choco
 \autocite{prudhomme-2016-choco}, Gecode \autocite{gecode-2021-gecode}, and
@@ -805,8 +802,8 @@ where \(V\) and \(C\) represent the number of variables and number of
 constraints respectively. The vector \(c\) holds the coefficients of the
 objective function and the matrix \(a\) holds the coefficients for the
 constraints. The vectors \(l\) and \(u\) respectively contain the lower and
-upper bounds of the constraints. Finally, the \glspl{variable} of the linear
-program held in the \(x\) vector.
+upper bounds of the constraints. Finally, the \variables{} of the linear program
+held in the \(x\) vector.
 
 For problems that are in the form of a linear program, there are proven methods
 to find the optimal solution. The most prominent method, the simplex method, can
@@ -816,19 +813,19 @@ The same method provides the foundation for a harder problem. In \gls{lp} our
 variables must be continuous. If we require that one or more take a discrete
 value (\(x_{i} \in \mathbb{N}\)), then the problem suddenly becomes much harder.
 The problem is referred to as \gls{mip} (or Integer Programming if \textbf{all}
-\glspl{variable} must take a discrete value).
+\variables{} must take a discrete value).
 
 Unlike \gls{lp}, there is no algorithm that can solve a mixed integer program in
 polynomial time. The general method to solve a mixed integer program is to treat
 it as an linear program and find an optimal solution using the simplex method.
-If the \glspl{variable} in the problem that are required to be discrete already
-have discrete values, then we have found our optimal solution. Otherwise, we
-pick one of the \glspl{variable}. For this \gls{variable} we create a version
-of the linear program where it is less or equal to the value in the solution
-rounded down to the nearest discrete value and a version where it is greater or
-equal to the value in the solution rounded up. Both versions are solved to find
-the best solution. The process is repeated recursively until a discrete solution
-is found.
+If the \variables{} in the problem that are required to be discrete already have
+discrete values, then we have found our optimal solution. Otherwise, we pick one
+of the \variables{}. For this \variable{} we create a version of the linear
+program where it is less or equal to the value in the solution rounded down to
+the nearest discrete value and a version where it is greater or equal to the
+value in the solution rounded up. Both versions are solved to find the best
+solution. The process is repeated recursively until a discrete solution is
+found.
 
 Much of the power of this solving method comes from bounds that can be inferred
 during the process. The solution that the simplex provides an upper bound for
@@ -838,23 +835,22 @@ bound. When the upper bound given by the simplex method is lower that the lower
 bound from an earlier solution, then we know that any discrete solutions
 following from the linear program will be strictly worse than the incumbent.
 
-Over the years \gls{lp} and \gls{mip} \glspl{solver} have developed immensely.
-\Glspl{solver}, such as CBC \autocite{forrest-2020-cbc}, CPLEX
+Over the years \gls{lp} and \gls{mip} \solvers{} have developed immensely.
+\solvers{}, such as CBC \autocite{forrest-2020-cbc}, CPLEX
 \autocite{cplex-2020-cplex}, Gurobi \autocite{gurobi-2021-gurobi}, and SCIP
 \autocite{gamrath-2020-scip}, can solve many complex problems. It is therefore
 often worthwhile to encode problem as an mixed integer program to find a
 solution.
 
 \glspl{csp} can be often be encoded as mixed integer programs. This does,
-however, come with its challenges. Most \glspl{constraint} in a \minizinc\ model
-are not linear equations. The translation of a single \gls{constraint} can
-introduce many linear \glspl{constraint} and even new \glspl{variable}. For
-example, when a \gls{constraint} reasons about the value that a variable will
-take, to encode it we will need to introduce \glspl{indicator-var}. The
-\glspl{indicator-var} \(y_{i}\) for a \gls{variable} \(x\) take the value 1 if
-\(x = i\) and 0 otherwise. \Glspl{constraint} reasoning about the value of \(x\)
-can then be rewritten as linear \glspl{constraint} using the \glspl{variable}
-\(y_{i}\).
+however, come with its challenges. Most \constraints{} in a \minizinc\ model are
+not linear equations. The translation of a single \constraint{} can introduce
+many linear \constraints{} and even new \variables{}. For example, when a
+\constraint{} reasons about the value that a variable will take, to encode it we
+will need to introduce \glspl{indicator-var}. The \glspl{indicator-var}
+\(y_{i}\) for a \variable{} \(x\) take the value 1 if \(x = i\) and 0 otherwise.
+\constraints{} reasoning about the value of \(x\) can then be rewritten as
+linear \constraints{} using the \variables{} \(y_{i}\).
 
 \begin{example}
   Let us again consider the N-Queens problem from \cref{ex:back-nqueens}. The
@@ -873,11 +869,11 @@ can then be rewritten as linear \glspl{constraint} using the \glspl{variable}
 
 
   The encoding of this variable uses only integers. Like the \gls{cp} model,
-  integer \glspl{variable} \(q\) are used to represent where the queen is
-  located in each column. To encode the \mzninline{all_different} constraints,
-  the \glspl{indicator-var} \(y\) are inserted to reason about the value of
-  \(q\). The \cref{line:back-mip-channel} is used to connect the \(q\) and \(y\)
-  \glspl{variable} and make sure that their values correspond.
+  integer \variables{} \(q\) are used to represent where the queen is located in
+  each column. To encode the \mzninline{all_different} constraints, the
+  \glspl{indicator-var} \(y\) are inserted to reason about the value of \(q\).
+  The \cref{line:back-mip-channel} is used to connect the \(q\) and \(y\)
+  \variables{} and make sure that their values correspond.
   \Cref{line:back-mip-row} ensures that only one queen is placed in the same
   row. Finally, \cref{line:back-mip-diag1,line:back-mip-diag2} constrain all
   diagonals to contain only one queen.
@@ -891,8 +887,8 @@ can then be rewritten as linear \glspl{constraint} using the \glspl{variable}
 \gls{sat} was the first problem to be proven to be \gls{np-comp}
 \autocite{cook-1971-sat}. The problem asks if there is an assignment for the
 variables of a given Boolean formula, such that the formula is satisfied. This
-problem can be seen as a restriction of the general \gls{csp} where
-\glspl{variable} can only be of a Boolean type.
+problem can be seen as a restriction of the general \gls{csp} where \variables{}
+can only be of a Boolean type.
 
 There is a field of research dedicated to solving \gls{sat} problems. In this
 field a \gls{sat} problem is generally standardised to be in \gls{cnf}. A
@@ -900,24 +896,25 @@ field a \gls{sat} problem is generally standardised to be in \gls{cnf}. A
 or their negations \(\neg x\). These literals are then used in a conjunction of
 disjunctive clauses: a Boolean formula in the form
 \(\forall_{i \in P} \exists_{b \in C_{i}} b\). To solve the \gls{sat} problem,
-the \gls{solver} has to find an assignment for the \glspl{variable} where at
-least one literal is true in every clause.
+the \solver{} has to find an assignment for the \variables{} where at least one
+literal is true in every clause.
 
 Even though the problem is proven to be hard to solve, a lot of progress has
 been made towards solving even the biggest the most complex \gls{sat} problems
 \autocite{biere-2021-sat}. Modern day \gls{sat} solvers, like Kissat
 \autocite{biere-2021-kissat} and Clasp \autocite{gebser-2012-clasp}, can solve
-instances of the problem with thousands of \glspl{variable} and clauses.
+instances of the problem with thousands of \variables{} and clauses.
 
 Many real world problems modelled in \cmls\ directly correspond to \gls{sat}.
-However, even problems that contain \glspl{variable} with types other than
-Boolean can often be encoded as a \gls{sat} problem. Depending of the problem,
-using a \gls{sat} \glspl{solver} to solve the encoded problem can still be the
-most efficient way to solve the problem.
+However, even problems that contain \variables{} with types other than Boolean
+can often be encoded as a \gls{sat} problem. Depending of the problem, using a
+\gls{sat} \solvers{} to solve the encoded problem can still be the most
+efficient way to solve the problem.
 
 \begin{example}
-  Consider the N-Queens problem presented in \cref{ex:back-nqueens}. A possible
-  \gls{sat} encoding for this problem is the following.
+  Let us once more consider the N-Queens problem presented in
+  \cref{ex:back-nqueens}. A possible \gls{sat} encoding for this problem is the
+  following.
 
   \begin{align}
     \text{given} \hspace{2em} & N = {1,\ldots,n} & \\
@@ -929,9 +926,9 @@ most efficient way to solve the problem.
     \label{line:back-sat-diag2}& \neg q_{ij} \lor \neg q_{(i+k)(j-k)} & \forall_{i,j \in N} \forall_{k=1}^{min(n-i, j)}
   \end{align}
 
-  The encoding of the problem uses a Boolean \gls{variable} for every position
-  of the chess board. Each \gls{variable} represents if a queen will be located
-  on this position or not. \Cref{line:back-sat-at-least} forces that a queen is
+  The encoding of the problem uses a Boolean \variable{} for every position of
+  the chess board. Each \variable{} represents if a queen will be located on
+  this position or not. \Cref{line:back-sat-at-least} forces that a queen is
   placed on every column of the chess board.
   \Cref{line:back-sat-row,line:back-sat-col} ensure that only one queens is
   place in each row and column respectively.
@@ -943,20 +940,19 @@ A variation on \gls{sat} is the \gls{maxsat} problem. Where in a \gls{sat}
 problem all clauses need to be satisfied, this is not the case in a \gls{maxsat}
 problem. Instead clauses are given individual weights. The higher the weight,
 the more important the clause is for the overall problem. The goal in the
-\gls{maxsat} problem is then to find a assignment for Boolean \glspl{variable}
-that maximises the cumulative weights of the satisfied clauses.
+\gls{maxsat} problem is then to find a assignment for Boolean \variables{} that
+maximises the cumulative weights of the satisfied clauses.
 
 The \gls{maxsat} problem is analogous to a \gls{cop}. Like a \gls{cop}, the aim
 of \gls{maxsat} is to find the optimal solution to the problem. The difference
-is that the weights are given to the \glspl{constraint} instead of the
-\glspl{variable} or a function over them. It is, again, often possible to encode
-a \gls{cop} as a \gls{maxsat} problem. A naive approach approach to encode an
-integer objective is, for example, to encode each value in the domain as a
-Boolean variable and assign that same value to a clause containing just that
-Boolean variable.
+is that the weights are given to the \constraints{} instead of the \variables{}
+or a function over them. It is, again, often possible to encode a \gls{cop} as a
+\gls{maxsat} problem. A naive approach approach to encode an integer objective
+is, for example, to encode each value in the domain as a Boolean variable and
+assign that same value to a clause containing just that Boolean variable.
 
-For many problems the use of \gls{maxsat} \glspl{solver} can offer a very
-successful method to find the optimal solution to a problem.
+For many problems the use of \gls{maxsat} \solvers{} can offer a very successful
+method to find the optimal solution to a problem.
 
 \section{Other Constraint Modelling Languages}%
 \label{sec:back-other-languages}
@@ -984,13 +980,13 @@ name suggest, \gls{ampl} was designed to allow modellers to express problems
 through the use of mathematical equations. It is therefore also described as an
 ``algebraic modelling language''. Specifically \gls{ampl} was designed to model
 linear programs. These days \gls{ampl} has been extended to allow more advanced
-\gls{solver} usage. Depending on the \gls{solver} targeted by \gls{ampl}, the
+\solver{} usage. Depending on the \gls{solver} targeted by \gls{ampl}, the
 language can give the modeller access to additional functionality. For
-\glspl{solver} that have a \gls{mip} solving method, the modellers can require
-\glspl{variable} to be integers. Different types of \glspl{solver} can also have
-access to different types of constraints, such as quadratic and non-linear
-constraints. \gls{ampl} has even been extended to allow the usage of certain
-\glspl{global} when using a \gls{cp} \gls{solver} \autocite{fourer-2002-amplcp}.
+\solvers{} that have a \gls{mip} solving method, the modellers can require
+\variables{} to be integers. Different types of \solvers{} can also have access
+to different types of constraints, such as quadratic and non-linear constraints.
+\gls{ampl} has even been extended to allow the usage of certain \glspl{global}
+when using a \gls{cp} \solver{} \autocite{fourer-2002-amplcp}.
 
 \begin{example}
 
@@ -1021,8 +1017,8 @@ constraints. \gls{ampl} has even been extended to allow the usage of certain
   \minizinc{}. Like \minizinc{}, \gls{ampl} has an extensive expression
   language, which includes \gls{generator} expressions and a vast collection of
   \glspl{operator}. The building block of the model are also similar:
-  \gls{parameter} declarations, \gls{variable} declarations, \glspl{constraint},
-  and a solving goal.
+  \parameter{} declarations, \variable{} declarations, \constraints{}, and a
+  solving goal.
 
   The same problem can be modelled in \minizinc\ as follows:
 
@@ -1041,12 +1037,12 @@ constraints. \gls{ampl} has even been extended to allow the usage of certain
   more different. The main reason for this difference is the level at which
   these models are written. The \gls{ampl} model is written to target a
   \gls{mip} solver. In the \gls{ampl} language this means that you can only use
-  the language functionality that is compatible with the targeted \gls{solver};
-  in this case, all expression have to be linear equations. In \minizinc\ the
+  the language functionality that is compatible with the targeted \solver{}; in
+  this case, all expression have to be linear equations. In \minizinc\ the
   modeller is not constrained in the same way. The modeller is always encouraged
-  to create high-level \gls{constraint} models. It is the job of the
-  \gls{solver}'s \minizinc\ library to transform the high-level constraints into
-  compatible \gls{solver}-level \glspl{constraint}.
+  to create high-level \constraint{} models. It is the job of the \solver{}'s
+  \minizinc\ library to transform the high-level constraints into compatible
+  \solver{}-level \constraints{}.
 \end{example}
 
 
@@ -1062,13 +1058,13 @@ similar to the \minizinc\ syntax.
 
 Where the \gls{opl} really shines is when modelling scheduling problems.
 Resources and activities are separate objects in the \gls{opl}. This allows
-users express resource scheduling \glspl{constraint} in an incremental and more
+users express resource scheduling \constraints{} in an incremental and more
 natural fashion. When solving a scheduling problem, the \gls{opl} makes use of
-specialised \gls{interval} \glspl{variable}, which represent when a task will be
+specialised \gls{interval} \variables{}, which represent when a task will be
 scheduled.
 
 \begin{example}
-  For example the \gls{variable} declarations and \glspl{constraint}
+  For example the \variable{} declarations and \constraints{}
   for a jobshop problem would look like this in an \gls{opl} model:
 
   \begin{plain}
@@ -1092,7 +1088,7 @@ scheduled.
     };
   \end{plain}
 
-  The equivalent declarations and \glspl{constraint} would look like this in
+  The equivalent declarations and \constraints{} would look like this in
   \minizinc{}:
 
   \begin{mzn}
@@ -1119,15 +1115,15 @@ scheduled.
   \end{mzn}
 
   Note that the \minizinc{} model does not have explicit Activity variables. It
-  must instead use \glspl{variable} that represent the start times of the activity
-  and a \gls{variable} to represent the time at which all activities are finished.
+  must instead use \variables{} that represent the start times of the activity
+  and a \variable{} to represent the time at which all activities are finished.
   The \gls{opl} model also has the advantage that it can first create resource
   objects and then use the \texttt{requires} keyword to force tasks on the same
   machine to be mutually exclusive. In \minizinc{} the same requirement is
   implemented through the use of \mzninline{disjunctive} constraints. Although
   this has the same effect, all mutually exclusive jobs have to be combined in a
   single statement in the model. This can make it harder in \minizinc\ to write
-  the correct \gls{constraint} and its meaning might be less clear.
+  the correct \constraint{} and its meaning might be less clear.
 
 \end{example}
 
@@ -1147,25 +1143,24 @@ the solver. Take, for example, the following \gls{opl} search definition:
 \end{plain}
 
 This search strategy will ensure that we first try and find a solution where the
-\gls{variable} \mzninline{x} takes a value smaller than \mzninline{y}, if it
-does not find a solution, then it will try finding a solution where the oposite
-is true. This search specification, like many other imaginable, cannot be
-enforce using \minizinc\ \gls{search-heuristic} \glspl{annotation}.
+\variable{} \mzninline{x} takes a value smaller than \mzninline{y}, if it does
+not find a solution, then it will try finding a solution where the oposite is
+true. This search specification, like many other imaginable, cannot be enforce
+using \minizinc\ \gls{search-heuristic} \glspl{annotation}.
 
 To support \gls{opl}'s dedicated search language, the language is tightly
-integrated with its dedicated \glspl{solver}. Its search syntax requires that
-the \gls{opl} process can directly interact with the \gls{solver}'s internal
-search mechanism and that the \gls{solver} reasons about search on the same
-level as the \gls{opl} model. It is therefore not possible to connect other
-\glspl{solver} to \gls{opl}.
+integrated with its dedicated \solvers{}. Its search syntax requires that the
+\gls{opl} process can directly interact with the \solver{}'s internal search
+mechanism and that the \solver{} reasons about search on the same level as the
+\gls{opl} model. It is therefore not possible to connect other \solvers{} to
+\gls{opl}.
 
 \subsection{Essence}%
 \label{sub:back-essence}
 
 \gls{essence} \autocite{frisch-2007-essence} is another high-level \cml\ is
-cherished for its adoption of high-level \gls{variable} types. In addition to
-all variable types that are contained in \minizinc{}, \gls{essence} also
-contains:
+cherished for its adoption of high-level \variable{} types. In addition to all
+variable types that are contained in \minizinc{}, \gls{essence} also contains:
 
 \begin{itemize}
   \item finite sets of non-iteger types,
@@ -1176,7 +1171,7 @@ contains:
 
 Since sets, multisets, and functions can be defined on any other type, these
 types can be arbitrary nested and the modeller can define, for example, a
-\gls{variable} that is a set of set of integers. Partitions can be defined for
+\variable{} that is a set of set of integers. Partitions can be defined for
 finite types. These types in \gls{essence} are restricted to Booleans,
 enumerated types, or a restricted set of integers.
 
@@ -1230,19 +1225,19 @@ enumerated types, or a restricted set of integers.
   );
   \end{mzn}
 
-  Note that, through the \gls{essence} type system, the first 2
-  \glspl{constraint} in the \minizinc{} are implied in the \gls{essence} model.
-  This is an example where the use of high-level types can help give the
-  modeller create more concise models.
+  Note that, through the \gls{essence} type system, the first 2 \constraints{}
+  in the \minizinc{} are implied in the \gls{essence} model. This is an example
+  where the use of high-level types can help give the modeller create more
+  concise models.
 
 \end{example}
 
 The high-level variables available in \gls{essence} are often not directly
-supported by the \glspl{solver} that is employed to solve \gls{essence}
-instances. To solve the problem, not only do the \glspl{constraint} have to be
-translated to \glspl{constraint} supported by the solver, but also all
-\glspl{variable} have to be translated to a combination of \glspl{constraint}
-and \glspl{variable} compatible with the targeted solver.
+supported by the \solvers{} that is employed to solve \gls{essence} instances.
+To solve the problem, not only do the \constraints{} have to be translated to
+\constraints{} supported by the solver, but also all \variables{} have to be
+translated to a combination of \constraints{} and \variables{} compatible with
+the targeted solver.
 
 \section{Term Rewriting}%
 \label{sec:back-term}
@@ -1296,11 +1291,11 @@ will ensure that the same \flatzinc{} is produced independently of the order in
 which the \minizinc\ model is processed. This is a desirable quality as it makes
 the behaviour of the translation process more predictable.
 
-Many of the techniques used by \glspl{solver} targeted by \minizinc\ are proven
-to be complete. Meaning that they are guaranteed to find a (best) solution to
-the problem or prove that there is none. For this quality to hold for the
-\minizinc\ solving process, it has to be guaranteed that the \minizinc\
-translation process terminates (so the solving process can start).
+Many of the techniques used by \solvers{} targeted by \minizinc\ are proven to
+be complete. Meaning that they are guaranteed to find a (best) solution to the
+problem or prove that there is none. For this quality to hold for the \minizinc\
+solving process, it has to be guaranteed that the \minizinc\ translation process
+terminates (so the solving process can start).
 
 In the remainder of this section we will discuss two types of \glspl{trs} that
 are closely related to \cmls\ and their compilation into solver level constraint
@@ -1313,12 +1308,11 @@ models: \gls{clp} and \gls{chr}.
 \gls{clp} \autocite{marriott-1998-clp} can be seen as a predecessor of \cmls{}
 like \minizinc. A constraint logic program describes the process in which a high
 level constraint model is eventually rewritten into a solver level constraints
-and added to a \gls{solver}. Like in \minizinc, can define \gls{constraint}
-predicates to use in the definition of the \gls{constraint} model. Different
-from \minizinc{}, constraint predicates in \gls{clp} can be rewritten in
-multiple ways. The goal of a constraint logic program is to rewrite all
-\glspl{constraint} in such a way that the solver level \glspl{constraint} are
-all satisfied.
+and added to a \solver{}. Like in \minizinc, can define \constraint{} predicates
+to use in the definition of the \constraint{} model. Different from \minizinc{},
+constraint predicates in \gls{clp} can be rewritten in multiple ways. The goal
+of a constraint logic program is to rewrite all \constraints{} in such a way
+that the solver level \glspl{constraint} are all satisfied.
 
 Variables are another notable difference between \cmls\ and \gls{clp}. In
 \gls{clp}, like in a conventional \gls{trs}, a variable is merely a name. The
@@ -1341,35 +1335,34 @@ the program itself can be said to be unsatisfiable. Even when a correct
 rewriting is found, it is possible to continue the process. This ways you can
 find all possible correct ways to rewrite the program.
 
-To implement this mechanism there is a tight integration between the solver,
+To implement this mechanism there is a tight integration between the \solver{},
 referred to as the \gls{constraint-store}, and the evaluator of the constraint
-logic program. In addition to just adding \glspl{constraint}, the program can
-also inspect the status of the constraint and retract constraints from the
-constraint store. This allows the program to detect when the constraint store
-has become inconsistent and then \gls{backtrack} the constraint store to the
-last decision (\ie\ restore the \gls{constraint-store} to its state before the
-last decision was made) and try the next rewriting rule.
+logic program. In addition to just adding \constraints{}, the program can also
+inspect the status of the constraint and retract constraints from the constraint
+store. This allows the program to detect when the constraint store has become
+inconsistent and then \gls{backtrack} the constraint store to the last decision
+(\ie\ restore the \gls{constraint-store} to its state before the last decision
+was made) and try the next rewriting rule.
 
 The strength of the \gls{constraint-store} can influence the correctness of a
-constraint logic program. Some \glspl{solver} are incomplete; it is unable to
-tell if some of its \glspl{constraint} are satisfied or not. This, for example,
-happens with \glspl{solver} that work with integer \glspl{domain}. In these
-cases the programmer must use the \mzninline{labeling} constraint to force
-constant values for the variables. Once the variables have been assigned
-constant values, the solver will be able to decide if the constraints are
-satisfied.
+constraint logic program. Some \solvers{} are incomplete; it is unable to tell
+if some of its \constraints{} are satisfied or not. This, for example, happens
+with \solvers{} that work with integer \glspl{domain}. In these cases the
+programmer must use the \mzninline{labeling} constraint to force constant values
+for the variables. Once the variables have been assigned constant values, the
+solver will be able to decide if the constraints are satisfied.
 
 \subsection{Constraint Handling Rules}%
 \label{sub:back-chr}
 \glsreset{chr}
 
-When \glspl{constraint} are seen as terms in a \gls{trs}, then it is not just
-possible to define rules to rewrite constraints to the level of a \gls{solver}.
-It is also possible to define rules to simplify, propagate, and derive new
+When \constraints{} are seen as terms in a \gls{trs}, then it is not just
+possible to define rules to rewrite constraints to the level of a \solver{}. It
+is also possible to define rules to simplify, propagate, and derive new
 constraints within the solver. \gls{chr} follow from this idea. \gls{chr} are a
 language extension (targeted at \gls{clp}) to allow user-defined constraints
-within a \gls{solver}. \Glspl{constraint} defined using \gls{chr} are rewritten
-into simpler constraints until they are solved.
+within a \solver{}. \constraints{} defined using \gls{chr} are rewritten into
+simpler constraints until they are solved.
 
 Different from \gls{clp}, \gls{chr} allows term rewriting rules that are
 multi-headed. This means that, for some rules, multiple terms must match, to
@@ -1392,12 +1385,12 @@ apply the rule.
     \item The first rules states that if \texttt{X = Y}, then \texttt{X -> Y} is
           logically true. This rule removes the term \texttt{X -> Y}. Since the
           constraint is said to be logically true, nothing gets added. \texttt{X
-          = Y} functions as a guard. This \gls{solver} builtin \gls{constraint}
-          is required for the rewriting rule to apply.
+          = Y} functions as a guard. This \solver{} builtin \constraint{} is
+          required for the rewriting rule to apply.
 
     \item The second rule implements the anti-symmetry of logical implications;
           the two implications, \texttt{X -> Y} and \texttt{Y -> X}, are
-          replaced by a \gls{solver} builtin, \texttt{X = Y}.
+          replaced by a \solver{} builtin, \texttt{X = Y}.
 
     \item Finally, the transitivity rule introduces a derived constraint. When
           it finds constraints \texttt{X -> Y} and \texttt{Y -> Z}, then it adds
@@ -1420,7 +1413,7 @@ rules are a combination of both types of rules in the form:
 \[ H_{1}, \ldots H_{l} \backslash H_{l+1}, \ldots, H_{n} \texttt{<=>} G_{1}, \ldots{}, G_{m} | B_{1}, \ldots, B_{o} \]
 
 It is possible to rewrite using a simpagation rule when there are terms matching
-\(H_{1}, \ldots, H_{n}\) and there are \gls{solver} built-ins
+\(H_{1}, \ldots, H_{n}\) and there are \solver{} built-ins
 \(G_{1}, \ldots{}, G_{m}\). When the simpagation rule is applied, the terms
 \(H_{l+1}, \ldots, H_{n}\) are replaced by the terms \(B_{1}, \ldots, B_{o}\).
 The terms \(H_{1}, \ldots H_{l}\) are kept in the system. Since simpagation
@@ -1481,10 +1474,10 @@ proven to hold, and remove variables that have become unused. These optimisation
 techniques are discussed in \cref{subsec:back-fzn-optimisation}.
 
 The backend will convert the internal solver level constraint model into a
-format that can be used by the targeted \gls{solver}. Given the formatted
-artefact, a solver process, controlled by the backend, can then be started.
-Whenever the solver process produces a solution, the backend will reconstruct
-the solution to the specification of the original \minizinc{} model.
+format that can be used by the targeted \solver{}. Given the formatted artefact,
+a solver process, controlled by the backend, can then be started. Whenever the
+solver process produces a solution, the backend will reconstruct the solution to
+the specification of the original \minizinc{} model.
 
 In this section we will discuss the flattening and optimisation process as
 employed by the 2.5.5 version of \minizinc{} \autocite{minizinc-2021-minizinc}.
@@ -1494,14 +1487,14 @@ employed by the 2.5.5 version of \minizinc{} \autocite{minizinc-2021-minizinc}.
 
 The goal of the flattening process is to arrive at a ``flat'' constraint model:
 it only contains constraints that consist of a singular call instruction, all
-arguments to calls are \gls{parameter} literals or \gls{variable} identifiers,
-and the call itself is a constraint primitive for the target \gls{solver}.
+arguments to calls are \parameter{} literals or \variable{} identifiers, and the
+call itself is a constraint primitive for the target \solver{}.
 
 To arrive at a flat model, the flattening process will transverse the
-declarations, \glspl{constraint}, and the solver goal and flatten any expression
+declarations, \constraints{}, and the solver goal and flatten any expression
 contained in these items. During the flattening of an expression, the expression
 rewritten into other \minizinc\ expressions according to the decomposition given
-in the target \gls{solver}'s \minizinc\ library. Enforced by \minizinc{}'s type
+in the target \solver{}'s \minizinc\ library. Enforced by \minizinc{}'s type
 system, at most one rule applies for any given constraint. The flattening of
 expressions is performed bottom-up, we flatten any sub-expression before its
 parent expression. For instance, in a call each argument is flattened before the
@@ -1522,33 +1515,33 @@ be replaced by an instantiation of this function body using the arguments to the
 call. Calls are, however, not the only type of expression that are decomposed
 during the flattening process. Other expression, like \gls{operator}
 expressions, variable array access, and if-then-else expressions, might also
-have to be decomposed for the targeted \gls{solver}. During the flattening
-process, these expressions are rewritten into equivalent call expressions that
-will start the decomposition process.
+have to be decomposed for the targeted \solver{}. During the flattening process,
+these expressions are rewritten into equivalent call expressions that will start
+the decomposition process.
 
 A notable effect of the flattening is that sub-expression are replaced by
-literals or identifiers. If the expression contains only \glspl{parameter}, then
-the flattening of the expression is merely a calculation to find the value of
-the literal to be put in its place. If, however, the expression contains a
-\gls{variable}, then this calculation cannot be performed during the flattening
-process. Instead, a new \gls{variable} must be created to represent the value of
+literals or identifiers. If the expression contains only \parameters{}, then the
+flattening of the expression is merely a calculation to find the value of the
+literal to be put in its place. If, however, the expression contains a
+\variable{}, then this calculation cannot be performed during the flattening
+process. Instead, a new \variable{} must be created to represent the value of
 the sub-expression and it must be constrained to take the value corresponding to
-the expression. The creation of this new \gls{variable} and defining
-\glspl{constraint} happens in one of two ways:
+the expression. The creation of this new \variable{} and defining \constraints{}
+happens in one of two ways:
 
 \begin{itemize}
 
-  \item For Boolean expressions in a reified context, the new \gls{variable} is
+  \item For Boolean expressions in a reified context, the new \variable{} is
         inserted by the flattening process itself. To constrain this
-        \gls{variable}, the flattener will then add a new reified constraint.
-        This constraint contains a call a variation of the call that would have
-        been generated for the expression in root context. The name of the
-        function is appended with \mzninline{_reif} and an extra Boolean
-        \gls{variable} argument is added to the call. The definition of this
-        constraint should implement the reification of the original expression:
-        setting the additional argument to \mzninline{true} if the constraint is
-        satisfied, and \mzninline{false} otherwise. For example, the constraint
-        in \minizinc{}
+        \variable{}, the flattener will then add a new reified constraint. This
+        constraint contains a call a variation of the call that would have been
+        generated for the expression in root context. The name of the function
+        is appended with \mzninline{_reif} and an extra Boolean \variable{}
+        argument is added to the call. The definition of this constraint should
+        implement the reification of the original expression: setting the
+        additional argument to \mzninline{true} if the constraint is satisfied,
+        and \mzninline{false} otherwise. For example, the constraint in
+        \minizinc{}
 
         \begin{mzn}
           constraint b \/ this_call(x, y);
@@ -1562,11 +1555,10 @@ the expression. The creation of this new \gls{variable} and defining
           constraint b \/ i1
         \end{mzn}
 
-  \item For other expressions, the \gls{variable} and defining
-        \glspl{constraint} are introduced in the definition of the function
-        itself. For example, the definition of the \mzninline{max} function in
-        the standard library, which calculates the maximum of two values, is
-        defined as:
+  \item For other expressions, the \variable{} and defining \constraints{} are
+        introduced in the definition of the function itself. For example, the
+        definition of the \mzninline{max} function in the standard library,
+        which calculates the maximum of two values, is defined as:
 
         \begin{mzn}
           function var int: max(var int: x, var int: y) :: promise_total =
@@ -1576,15 +1568,15 @@ the expression. The creation of this new \gls{variable} and defining
             } in m;
         \end{mzn}
 
-        Using a \gls{let} it explicitly creates a new \gls{variable}, constrains
-        this \gls{variable} to take to correct value, and returns the newly
-        created \gls{variable}.
+        Using a \gls{let} it explicitly creates a new \variable{}, constrains
+        this \variable{} to take to correct value, and returns the newly created
+        \variable{}.
 \end{itemize}
 
 These are the basic steps that are followed to flatten \minizinc\ instance. This
 is, however, not the complete process. The quality of a \flatzinc\ model is of
-the utmost importance. A \flatzinc\ containing extra \glspl{variable} and
-\glspl{constraint} that do not add any information to the solving process might
+the utmost importance. A \flatzinc\ containing extra \variables{} and
+\constraints{} that do not add any information to the solving process might
 exponentially slow down the solving process. Therefore, the \minizinc\
 flattening process is extended using many techniques to help improve the quality
 of the flattened model. In \crefrange{subsec:back-cse}{subsec:back-delayed-rew}
@@ -1610,9 +1602,9 @@ discrete optimisation \autocite{marinov-2005-sat-optimisations,
   \end{mzn}
 
   the expression \mzninline{abs(x)} is occurs twice. There is however no need to
-  create two separate \glspl{variable} (and defining \glspl{constraint}) to
-  represent the absolute value of \mzninline{x}. The same \gls{variable} can be
-  used to represent the \mzninline{abs(x)} in both sides of the disjunction.
+  create two separate \variables{} (and defining \constraints{}) to represent
+  the absolute value of \mzninline{x}. The same \variable{} can be used to
+  represent the \mzninline{abs(x)} in both sides of the disjunction.
 \end{example}
 
 Seeing that the same expression occurs multiple times is not always easy. Some
@@ -1650,7 +1642,7 @@ normal to evaluate \mzninline{x = pow(i, 2)}. However, the expression defining
 replaced by the earlier stored result: \mzninline{y = x}.
 
 \gls{cse} also has an important interaction with the occurence of reified
-constraints. \Glspl{reification} of a \gls{constraint} are often defined in the
+constraints. \Glspl{reification} of a \constraint{} 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 solving process if we can detect that a
@@ -1694,14 +1686,14 @@ constraint.
 \subsection{Adjusting Domain}%
 \label{subsec:back-adjusting-dom}
 
-As discussed in \cref{subsec:back-cp}, the \glspl{domain} of \glspl{variable}
-can sometimes be directly changed because of the addition of a \gls{constraint}.
-Similarly, depending on the \glspl{domain} of \glspl{variable} some constraints
-can be proven \mzninline{true} or \mzninline{false}.
+As discussed in \cref{subsec:back-cp}, the \glspl{domain} of \variables{} can
+sometimes be directly changed because of the addition of a \constraint{}.
+Similarly, depending on the \glspl{domain} of \variables{} some constraints can
+be proven \mzninline{true} or \mzninline{false}.
 
 This principle also applies during the flattening of a \minizinc\ model. It is
 generally a good idea to detect cases where we can directly change the
-\gls{domain} of a \gls{variable}. Sometimes this might mean that the constraint
+\gls{domain} of a \variable{}. Sometimes this might mean that the constraint
 does not need to be added at all and that constricting the domain is enough.
 Tight domains can also allow us to avoid the creation of reified constraints
 when the truth-value of a reified constraints can be determined from the
@@ -1720,25 +1712,24 @@ when the truth-value of a reified constraints can be determined from the
   \end{mzn}
 
   Given the \glspl{domain} specified in the model, the second constraint is
-  flattened using to reified \glspl{constraint} for each side of the
-  implication.
+  flattened using to reified \constraints{} for each side of the implication.
 
-  If we however consider the first \gls{constraint}, then we deduce that
+  If we however consider the first \constraint{}, then we deduce that
   \mzninline{a} must always take a value that is 4 or lower. When the compiler
-  adjust the domain of \mzninline{a} while flattening the first
-  \gls{constraint}, then the second \gls{constraint} can be simplified. The
-  expression \mzninline{a > 5} is known to be \mzninline{false}, which means
-  that the constraint can be simplified to \mzninline{true}.
+  adjust the domain of \mzninline{a} while flattening the first \constraint{},
+  then the second \gls{constraint} can be simplified. The expression
+  \mzninline{a > 5} is known to be \mzninline{false}, which means that the
+  constraint can be simplified to \mzninline{true}.
 \end{example}
 
 During flattening, the \minizinc\ compiler will actively remove values from the
 \gls{domain} when it encounters constraints that trivially reduces it. For
-example, constraints with a single comparison expression between a
-\gls{variable} and a \gls{parameter} (\eg\ \mzninline{x != 5}), constraint with
-a single comparison between two \glspl{variable} (\eg\ \mzninline{x >= y}),
-constraints that directly change the domain (\eg\ \mzninline{x in 3..5}). It,
-however, will not perform more complex \gls{propagation}, like the
-\gls{propagation} of \glspl{global}.
+example, constraints with a single comparison expression between a \variable{}
+and a \parameter{} (\eg\ \mzninline{x != 5}), constraint with a single
+comparison between two \variables{} (\eg\ \mzninline{x >= y}), constraints that
+directly change the domain (\eg\ \mzninline{x in 3..5}). It, however, will not
+perform more complex \gls{propagation}, like the \gls{propagation} of
+\glspl{global}.
 
 \subsection{Constraint Aggregation}%
 \label{subsec:back-aggregation}
@@ -1747,7 +1738,7 @@ 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:
+  2*y <= z} could result in the following \flatzinc:
 
 \begin{nzn}
   var int: x;
@@ -1762,8 +1753,8 @@ operators. For example the evaluation of the linear constraint \mzninline{x +
 
 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 \gls{solver}'s performance. These \glspl{solver} would likely perform better
-had they received the equivalent linear constraint
+the \solver{}'s performance. These \solvers{} would likely perform better had
+they received the equivalent linear constraint
 
 \begin{mzn}
 constraint int_lin_le([1,2,-1], [x,y,z], 0)
@@ -1776,7 +1767,7 @@ the solution.
 This can be resolved using the \gls{aggregation} of constraints. 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 \glspl{variable}. For example, the
+that eliminates 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.
@@ -1784,10 +1775,10 @@ global cardinality constraints.
 The \minizinc\ compiler aggregates expressions whenever possible. When the
 \minizinc\ compiler reaches an expression that could potentially be part of an
 aggregated constraint, the compiler will not flatten the expression. The
-compiler will instead perform a search of its sub-expression to collect all other
-expressions to form an aggregated constraint. The flattening process continues
-by flattening this aggregated constraint, which might still contain unflattened
-arguments.
+compiler will instead perform a search of its sub-expression to collect all
+other expressions to form an aggregated constraint. The flattening process
+continues by flattening this aggregated constraint, which might still contain
+unflattened arguments.
 
 \subsection{Delayed Rewriting}%
 \label{subsec:back-delayed-rew}
@@ -1826,43 +1817,42 @@ evaluating a predicate may also \emph{impose} new bounds on variables, so it is
 not always clear which order of evaluation is best.
 
 The same problem occurs with \glspl{reification} that are produced during
-flattening. Other constraints could fix the domain of the reified \gls{variable}
+flattening. Other constraints could fix the domain of the reified \variable{}
 and make the \gls{reification} unnecessary. Instead the constraint (or its
 negation) can be flattened in root context. This could avoid the use of a big
 decomposition or an expensive propagator.
 
 To tackle this problem, the \minizinc\ compiler employs \gls{del-rew}. When a
-linear \gls{constraint} is aggregated or a relational \gls{reification}
-\gls{constraint} is introduced it is not directly flattened. Instead these
+linear \constraint{} is aggregated or a relational \gls{reification}
+\constraint{} is introduced it is not directly flattened. Instead these
 constraints are appended to the end of the current \gls{ast}. All other
 constraints currently still unflattened, that could change the relevant
 \glspl{domain}, will be flattened first.
 
-Note that this heuristic does not guarantee that \glspl{variable} have their
-tightest possible \gls{domain}. One delayed \gls{constraint} can still influence
-the \glspl{domain} of \glspl{variable} used by other delayed \glspl{constraint}.
+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{}.
 
 \subsection{FlatZinc Optimisation}%
 \label{subsec:back-fzn-optimisation}
 
 After the compiler is done flattening the \minizinc\ instance, it enters the
 optimisation phase. This phase occurs at the same stage as the as the solver
-input language. Depending on the targeted \gls{solver}, the \minizinc\ flattener
+input language. Depending on the targeted \solver{}, the \minizinc\ flattener
 might still understand the meaning of certain constraints. In these cases,
 \gls{propagation} methods (as discussed in \cref{subsec:back-cp}) can be used to
-eliminate values from variable \glspl{domain} and simplify \glspl{constraint}.
+eliminate values from variable \glspl{domain} and simplify \constraints{}.
 
 In the current implementation the main focus of the flattener is to propagate
 Boolean constraint. The flattener try and reduce the number of Boolean variables
 and try and reduce the number of literals in clauses or logical and constraints.
 The additional propagation might fix the reification of a constraint. If this
-constraint is not yet rewritten, then the \gls{solver} will know to use a direct
+constraint is not yet rewritten, then the \solver{} will know to use a direct
 constraint instead of a reified version.
 
-Even more important than the Boolean constraints, are equality
-\glspl{constraint}. The flattening is in the unique position to \gls{unify}
-\glspl{variable} when they are found to be equal. Since they both have to take
-the same value, only a single \gls{variable} is required in the \flatzinc\ model
-to represent them both. Whenever any (recognisable) equality constraint is found
-during the optimisation phase, it is removed and the two \glspl{variable} are
-unified.
+Even more important than the Boolean constraints, are equality \constraints{}.
+The flattening is in the unique position to \gls{unify} \variables{} when they
+are found to be equal. Since they both have to take the same value, only a
+single \variable{} is required in the \flatzinc\ model to represent them both.
+Whenever any (recognisable) equality constraint is found during the optimisation
+phase, it is removed and the two \variables{} are unified.