dekker-phd-thesis/chapters/2_background.tex

%************************************************
\chapter{Review of Literature}\label{ch:background}
%************************************************

A goal shared between all programming languages is to provide a certain level of
abstraction: an assembly language allows you to abstract from the binary
instructions and memory positions; Low-level imperial languages, like FORTRAN,
were the first to allow you to abstract from the processor architecture of the
target machine; and nowadays writing a program requires little knowledge of the
actual workings of the hardware on which the program is executed.

Freuder states that the ``Holy Grail'' of programming languages would be where
the user merely states the problem, and the computer solves it and that
\gls{constraint-modelling} is one of the biggest steps towards this goal to this
day \autocite*{freuder-1997-holygrail}. Different from imperative (and even
other declarative) languages, in a \cml{} the modeller does not describe how to
solve the problem, but rather provides the problem requirements. You could say
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}.

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 a
\gls{objective} \(z\). In this case the goal is to find a solution that
satisfies all \glspl{constraint} 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.

\begin{listing}
  \pyfile{assets/py/2_dyn_knapsack.py}
  \caption{\label{lst:2-dyn-knapsack} A Python program that solves a 0-1 knapsack
    problem using dynamic programming}
\end{listing}

\begin{example}%
\label{ex:back-knapsack}

  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}:

  \begin{equation*}
    \text{maximise}~z~\text{subject to}~
    \begin{cases}
      S \subseteq T \\
      z = \sum_{i \in S} joy(i) \\
      \sum_{i \in S} space(i) < C \\
    \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.

  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
  mathematical definition and generate a definition that can be used by
  dedicated solvers.

\end{example}

In the remainder of this chapter we will first, in \cref{sec:back-minizinc}
introduce \minizinc\ as the leading \cml\ used within this thesis.
\cref{sec:back-mzn-interpreter} explains the process that the current \minizinc\
interpreter uses to translate a \minizinc\ model into a solver-level constraint
model. Then, \cref{sec:back-other-languages} introduces alternative \cmls\ and
compares their functionality to \minizinc{}. Finally, \cref{sec:back-term} and
\cref{sec:back-clp} survey the closely related fields of \gls{trs} and
\gls{clp}.

\section{\glsentrytext{minizinc}}%
\label{sec:back-minizinc}

\minizinc{} is a high-level, solver- and data-independent modelling language for
discrete satisfiability and optimisation problems
\autocite{nethercote-2007-minizinc}. Its expressive language and extensive
library of constraints allow users to easily model complex problems.

\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}

\begin{example}%
\label{ex:back-mzn-knapsack}

  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 \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.

  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}.
\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 the assignments

\begin{mzn}
TOYS = {football, tennisball, stuffed_elephant};
toy_joy = [63, 12, 100];
toy_space = [32, 8, 40];
space_left = 44;
\end{mzn}

the following model is the result of flattening:

\begin{mzn}
var 0..1: selection_0;
var 0..1: selection_1;
var 0..1: selection_2;
var 0..175: total_joy:: is_defined_var;
constraint int_lin_le([32,8,40],[selection_0,selection_1,selection_2],44);
constraint int_lin_eq([63,12,100,-1],[selection_0,selection_1,selection_2,total_joy],0):: defines_var(total_joy);
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
\mzninline{total_joy} that satisfies all constraints and maximises
\mzninline{total_joy}, or report that there is no such assignment.

\subsection{Model Structure}%
\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}.
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
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
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

\begin{mzn}
  array[5..10] of var bool: bs;
\end{mzn}

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

\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
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.

\gls{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
expression. It is important that the solver-level versions of the expressions
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}
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;}.

\jip{TODO:\@ add some information about search in \minizinc{}. It's probably
  pretty relevant.}

Common structures in \minizinc\ can be captured using function declarations. A
user can declare a function \mzninline{function @\(T\)@: @\(I\)@(@\(P\)@) = E;}.
In the function declaration \(T\) is the type of the result of the function,
\(I\) is the identifier for the function, \(P\) is a list types and identifiers
for the parameters of the functions, and finally \(E\) is the expression that
can use the parameters \(P\) and when flattened will give the result of the
function. The \minizinc\ language offers the keywords \mzninline{predicate} and
\mzninline{test} as a shorthand for \mzninline{function var bool} and
\mzninline{function bool} respectively. For example a function that squares an
integer can be defined as follows.

\begin{mzn}
  function int: square(int: a) = a * a;
\end{mzn}

Function declarations are also the main way in which \gls{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.
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.

\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 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}.
\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 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.

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 an 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 a shorthand 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 \gls{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''
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 a \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 \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
\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
\glspl{variable}.

\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 an \gls{array} that contains the doubled even
values of an \gls{array} \mzninline{x}.

\begin{mzn}
  [ xi * 2 | xi in x where x mod 2 == 0]
\end{mzn}

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
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
``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 \glspl{variable} that
are introduced might need to be renamed in the resulting solver level model.
Different from top-level definitions, the \glspl{variable} 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
definitions and in the resulting expression.

\subsection{Reification}%
\label{subsec:back-reification}

With the rich expression language in \minizinc{}, \glspl{constraint} 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
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.

\begin{example}
  Consider the \minizinc\ model:

  \begin{mzn}
    array[1..10] of var 1..15: x;
    constraint all_different(x);
    solve maximize sum(i in 1..10) (x[i] mod 2 == 0);
  \end{mzn}

  This model maximises the number of even numbers taken by the elements of the
  array \mzninline{x}. In this model the expression \mzninline{x[i] mod 2 == 0}
  has to reified. Since the elements have a domain from 1 to 15 and are
  constrained to take different values, not all elements of \mzninline{x} can
  take even values. Instead the solver is tasked to maximise the number of
  reified variables it can set to \mzninline{true}.
\end{example}

We say that the same expression can be used in \emph{root context} as well as in
a \emph{reified context}. In \minizinc{}, almost all expressions can be used in
both contexts.

\subsection{Handling Undefined Expressions}%
\label{subsec:back-mzn-partial}

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 the given index set: \\
  \mzninline{array1d(1..3, [1,2,3])[0] = @??@}

  \item Finding the minimum or maximum or an empty set: \\ \mzninline{min({})
  =@??@}

  \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 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
in \cmls\ \autocite*{frisch-2009-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[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}.

\end{description}

In practice, it is often natural to guard against undefined behaviour using
Boolean logic. Relational semantics therefore often feel the most natural for
the users of constraint modelling languages. This is why the \minizinc\ uses
relational semantics during its evaluation.

For example, one might deal with a zero divisor using a disjunction:

\begin{mzn}
  constraint d == 0 \/ a div d < 3;
\end{mzn}

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}

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.

\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. To understand the challenges in the translations a
\minizinc\ model into a solver level \gls{constraint} model, this section will
discuss the different technologies used used by \minizinc\ solver targets: their
input types and the basic method of solving the given problem.

\subsection{Boolean Satisfiability}%
\label{subsec:back-sat}

\subsection{Mathematical Programming}%
\label{subsec:back-mip}

\subsection{Constraint Programming}%
\label{subsec:back-cp}

\subsection{Hybrid Technologies}%
\label{subsec:back-hybrid}


\section{Compiling \glsentrytext{minizinc}}%
\label{sec:back-mzn-interpreter}

\jip{This section is the only one here that is not really literature review.
  Maybe this should just be a separate chapter. It is ``new'' in the sense that
  is the first real description of some parts of the compiler, but it is
  relatively short.}

Traditionally the compilation process is split into three sequential parts: the
\emph{frontend}, the \emph{middle-end}, and the \emph{backend}. It is the job of
the frontend to parse the user input, report on any errors or inconsistencies in
the input, and transform it into an internal representation. The middle-end
performs the main translation in a target-independent fashion. It converts the
internal representation at the level of the compiler frontend to another
internal representation as close to the level required by the compilation
targets. The final transformation to the format required by the compilation
target are performed by the backend. When a compiler is separated into these few
steps, then adding support for new language or compilation target only require
the addition of a frontend or backend respectively.

The \minizinc\ compilation process categorised in the same three categories, as
shown in \cref{fig:back-mzn-comp}. In the frontend, a \minizinc\ model is first
parsed together with its data into an \gls{ast}. The process will then analyse
the \gls{ast} to discover the types of all expressions used in the instance. If
an inconsistency is discovered, then an error is reported to the user. Finally,
the frontend will also preprocess the \gls{ast}. This process is used to rewrite
expressions into a common form for the middle-end, \eg\ remove the ``syntactic''
sugar. For instance, replacing the usage of enumerated types by normal integers.

\begin{figure}
  \centering
  \includegraphics[width=\linewidth]{assets/img/back_compilation_structure}
  \caption{\label{fig:back-mzn-comp} The compilation structure of the \minizinc\
    compiler.}
\end{figure}

The middle-end contains the most important two processes: the flattening and the
optimisation. During the flattening process the high-level (\minizinc{})
constraint model is rewritten into a solver level (\flatzinc{}) constraint
model. It could be noted that the flattening step depends on the compilation
target to define its solver level constraints. Even though the information
required for this step is target dependent, we consider it part of the
middle-end as the mechanism is the same for all compilation targets. A full
description of this process will follow in \cref{subsec:back-flattening}. Once a
solver level constraint model is constructed, the \minizinc\ compiler will try
to optimise this model: shrink domains of variables, remove constraints that are
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.

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}.

\subsection{Flattening}%
\label{subsec:back-flattening}

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}.

To arrive at a flat model, the flattening process will transverse the
declarations, \glspl{constraint}, and the solver goal and flatten any expression
contained in these items. The flattening of an expression is a recursive
process. \Gls{parameter} literals and \gls{variable} identifiers are already
flat. For any other kind of expression, its arguments are first flattened. If
the expression itself is a constraint primitive, then it is ready

\jip{This should say something about introducing relational reified constraints.}

\paragraph{Common Sub-expression Elimination}

Because the evaluation of a \minizinc\ expression cannot have any side-effects, 
In some cases, it is even possible to not generate definitions in the first
place through the use of \gls{cse}. This simplification is a well understood
technique that originates from compiler optimisation \autocite{cocke-1970-cse}
and has proven to be very effective in discrete optimisation
\autocite{marinov-2005-sat-optimisations, araya-2008-cse-numcsp}, including
during the evaluation of \cmls\ \autocite{rendl-2009-enhanced-tailoring}.

For instance, in the constraint\\
\begin{mzn}
  constraint (abs(x)*2 >= 20) \/ (abs(x)+5 >= 15);
\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.

Seeing that the same expression occurs multiple times is not always easy. Some
expressions only become syntactically equal during evaluation, as in the
following example.

\begin{example}
  Consider the fragment:

  \begin{mzn}
    function var float: pythagoras(var float: a, var float: b) =
      let {
        var float: x = pow(a, 2);
        var float: y = pow(b, 2);
      } in sqrt(x + y);
    constraint pythagoras(i, i) >= 5;
  \end{mzn}

  Although the expressions \mzninline{pow(a, 2)} and \mzninline{pow(b, 2)} are
  not syntactically equal, the function call \mzninline{pythagoras(i,i)} using
  the same variable for \mzninline{a} and \mzninline{b} makes them equivalent.
\end{example}

A straightforward approach to ensure that the same instantiation of a function
To ensure that syntactically equal expressions are only evaluated once the
\minizinc\ compiler through the use of memorisation. After the flattening of an
expression, the instantiated expression and its result are stored in a lookup
table, the \gls{cse} table. Then before any consequent expression is flattened
the \gls{cse} table is consulted. If an equivalent expression is found, then the
accompanying result is used; otherwise, the evaluation proceeds as normal.

In our example, the evaluation of \mzninline{pythagoras(i, i)} would proceed as
normal to evaluate \mzninline{x = pow(i, 2)}. However, the expression defining
\mzninline{y}, \mzninline{pow(i, 2)}, will be found in the \gls{cse} table and
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
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
reified constraint is in fact not required.

If a constraint is present in the root context, it means that it must hold
globally. If the same constraint is used in a reified context, it can therefore
be replaced with the constant \mzninline{true}, avoiding the need for
reification (or in fact any evaluation).

We can harness \gls{cse} to store the evaluation context when a constraint is
added, and detect when the same constraint is used in both contexts. Whenever a
lookup in the \gls{cse} table is successful, action can be taken depending on
both the current and stored evaluation context. If the stored expression was in
root context, then the constant \mzninline{true} can be used, independent of the
current context. Otherwise, if the stored expression was in reified context and
the current context is reified, then the stored result variable can be used.
Finally, if the stored expression was in reified context and the current context
is root context, then the previous result can be replaced by the constant
\mzninline{true} and the evaluation will proceed as normal with the root context
constraint.

\begin{example}
  Consider the fragment:

  \begin{mzn}
    function var bool: p(var int: x, var int: y) = q(x) /\ r(y);
    constraint b0 <-> q(x);
    constraint b1 <-> t(x,y);
    constraint b1 <-> p(x,y);
  \end{mzn}

  If we process the top-level constraints in order we create a reified call to
  \mzninline{q(x)} for the original call. Suppose processing the second
  constraint we discover \mzninline{t(x,y)} is \mzninline{true}, fixing
  \mzninline{b1}. When we then process \mzninline{q(x)} in instantiation of the
  call \mzninline{p(x,y)}, we find it is the root context. So \gls{cse} needs to
  set \mzninline{b0} to \mzninline{true}.
\end{example}

\paragraph{Adjusting domains}

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}.

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
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
\glspl{domain} of variables.

\begin{example}%
\label{ex:back-adj-dom}
  Consider the following \minizinc\ model:

  \begin{mzn}
    var 1..10: a;
    var 1..5: b;

    constraint a < b;
    constraint (a > 5) -> (a + b > 12);
  \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.

  If we however consider the first \gls{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}.
\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}.

\paragraph{Constraint Aggregation}

Complex \minizinc\ expression can sometimes result in the creation of many new
variables that represent intermediate results. This is in particular true for
linear and boolean equations that are generally written using \minizinc\
operators. For example the evaluation of the linear constraint \mzninline{x +
2*y <= z} could result in the following \flatzinc:

\begin{nzn}
  var int: x;
  var int: y;
  var int: z;
  var int: i1;
  var int: i2;
  constraint int_times(y, 2, i1);
  constraint int_plus(x, i1, i2);
  constraint int_le(i2, z);
\end{nzn}

This \flatzinc\ model is correct, but, at least for pure \gls{cp} solvers, the
existence of the intermediate variables is likely to have a negative impact on
the \gls{solver}'s performance. These \glspl{solver} would likely perform better
had they received the equivalent linear constraint

\begin{mzn}
constraint int_lin_le([1,2,-1], [x,y,z], 0)
\end{mzn}

directly. Since many solvers support linear constraints, it is often an
additional burden to have intermediate values that have to be given a value in
the solution.

This can be resolved using the \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
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.

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.

\paragraph{Delayed Rewriting}

Adjusting the \glspl{domain} of variables during flattening means that the
system becomes non-confluent, and some orders of execution may produce
``better'', \ie\ more compact or more efficient, \flatzinc{}.

\begin{example}
  The following example is similar to code found in the \minizinc\ libraries of
  \gls{mip} solvers.

  \begin{mzn}
    function var int: lq_zero_if_b(var int: x, var bool: b) =
      x <= ub(x)*(1-b);
  \end{mzn}

  This predicate expresses the constraint \mzninline{b -> x<=0}, using a
  well-known method called ``big-M transformation''. The expression
  \mzninline{ub(x)} returns a valid upper bound for \mzninline{x}, \ie\ a fixed
  value known to be greater than or equal to \mzninline{x}. This could be the
  initial upper bound \mzninline{x} was declared with, or the current value in
  the corresponding \nanozinc\ \mzninline{mkvar} call. If \mzninline{b} takes
  the value 0, the expression \mzninline{ub(x)*(1-b)} is equal to
  \mzninline{ub(x)}, and the constraint \mzninline{x <= ub(x)} holds trivially.
  If \mzninline{b} takes the value 1, \mzninline{ub(x)*(1-b)} is equal to 0,
  enforcing the constraint \mzninline{x <= 0}.
\end{example}

For \gls{mip} solvers, it is quite important to enforce tight bounds in order to
improve efficiency and sometimes even numerical stability. It would therefore be
useful to rewrite the \mzninline{lq_zero_if_b} predicate only after the
\glspl{domain} of the involved variables has been reduced as much as possible,
in order to take advantage of the tightest possible bounds. On the other hand,
evaluating a predicate may also \emph{impose} new bounds on variables, so it is
not always clear which order of evaluation is best.

The same problem occurs with \glspl{reification} that are produced during
flattening. Other constraints could fix the domain of the reified \gls{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
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}.

\subsection{Optimisation}%
\label{subsec:back-fzn-optimisation}

The optimisation process of the \minizinc\ compiler

\section{Other Constraint Modelling Languages}%
\label{sec:back-other-languages}

Although \minizinc\ is the \cml\ that is the primary focus of this thesis, there
are many other \cmls{}. Each \cml{} has its own focus and purpose and comes with
its own strength and weaknesses. Most of the techniques that are discusses in
this thesis can be adapted to these languages.

We will now discuss some of the other prominent \cmls{} and will compare them to
\minizinc\ to indicate to the reader where techniques might have to be adjusted
to fit other languages.

\subsection{AMPL}%
\label{sub:back-ampl}

One of the most used \cmls\ is \gls{ampl} \autocite{fourer-2003-ampl}. As the
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 an \gls{ampl} model generally
describes a \gls{linear-program}. In a \gls{linear-program} the \glspl{variable}
can take any value from a continuous range and the \gls{objective} and
\glspl{constraint} can only use linear function over \glspl{variable} (\ie\
\(\sum c_{i} x_{i}\), where all \(c_{i}\) are \glspl{parameter} and all
\(x_{i}\) are \glspl{variable}).

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}.

\begin{example}

  The following

  \begin{plain}
    set Cities ordered;
    set Paths := {i in Cities, j in Cities: ord(i) < ord(j)};
    param cost {Paths} >= 0;
    var Take {Paths} binary;

    param n := card {Cities};
    set SubSets := 0 .. (2**n - 1);
    set PowerSet {k in SubSets} := {i in Cities: (k div 2**(ord(i)-1)) mod 2 = 1};

    minimize TotalCost: sum {(i,j) in Paths} cost[i,j] * Take[i,j];

    subj to Tour {i in S}:
      sum {(i,j) in Paths} Take[i,j] + sum {(j,i) in Paths} Take[j,i] = 2;

    subj to SubtourElimation {k in SubSet diff {0,2**n-1}}:
      sum {i in PowerSet[k], j in Cities diff PowerSet[k]: (i,j) in Paths} X[i,j] +
      sum {i in PowerSet[k], j in Cities diff PowerSet[k]: (j,i) in Paths} X[j,i] >= 2;
  \end{plain}

  \begin{mzn}
    enum CITIES;
    array[CITIES, CITIES] of int: cost;

    array[CITIES] of var CITIES: next;

    constraint circuit(next);

    solve minimize sum(i in CITIES) (cost[i, next[CITIES]]);
  \end{mzn}

\end{example}

\subsection{OPL}%
\label{sub:back-opl}

\glsaccesslong{opl} \autocite{van-hentenryck-1999-opl} is a \cml\ that has a
focus aims to combine the strengths of mathematical programming languages like
\gls{ampl} with the strengths of \gls{cp}. The syntax of \gls{opl} is very
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
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
scheduled. For example the \gls{variable} declarations and \glspl{constraint}
for a jobshop problem would look like this in an \gls{opl} model:

\begin{plain}
  ScheduleHorizon = sum(j in Jobs, t in Tasks) duration[j, t];
  Activity task[j in Jobs, t in Tasks] (duration[j,t]);
  Activity makespan;
  UnaryResource tool[Machines];

  minimize makespan.end
  subject to {
    forall (j in Jobs)
      task[j,nbTasks] precedes makespan;

    forall (j in Jobs)
      forall (t in 1..nbTasks-1)
        task[j, t] precedes task[j, t+1];

    forall (j in Jobs)
      forall (t in Tasks)
        task[j, t] requires tool[resource[j, t]];
  };
\end{plain}

The equivalent declarations and \glspl{constraint} would look like this in
\minizinc{}:

\begin{mzn}
  int: horizon = sum(j in Jobs, t in Tasks)(duration[j,t]);
  var 0..horizon: makespan;
  array[JOB,TASK] of var 0..maxt: start;

  constraint forall(j in Jobs, t in 1..nbTasks-1) (
    start[j,t] + duration[j,t] <= start[j,t+1]
  );

  constraint forall(j in Jobs) (
    start[j, nbTasks] + duration[j, nbTasks] <= makespan
  );

  constraint forall(m in Machines) (
    disjunctive(
      [start[j,t] | j in Jobs, t in Tasks where resource[j,t] == m],
      [duration[j,t] | j in Jobs, t in Tasks where resource[j,t] == m],
    )
  );

  solve minimize makespan;
\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.
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 \gls{opl} also contains a specialised search syntax that can be used to
instruct its solvers \autocite{van-hentenryck-2000-opl-search}. This syntax
allows the modellers full programmatic control over how the solver will explore
the search space depending on the current state of the variables. This offers to
modeller more control over the search in comparison to the
\gls{search-heuristic} \glspl{annotation} in \minizinc{}, which only allow
modellers to select predefined \glspl{search-heuristic} already implemented in
the solver. Take, for example, the following \gls{opl} search definition:

\begin{plain}
  search {
    try x < y | y >= x endtry;
  }
\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}.

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}.

The \gls{opl} does not allow modellers to create their own (user-defined)
functions. A modeller is restricted to the \gls{global} constraint library
provided by the \gls{opl}'s standard library.

\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:

\begin{itemize}
  \item finite sets of non-iteger types,
  \item finite multisets of any type,
  \item finite (partial) functions,
  \item and (regular) partitions of finite types.
\end{itemize}

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
finite types. These types in \gls{essence} are restricted to Booleans,
enumerated types, or a restricted set of integers.

For example, the Social Golfers Problem, can be modelled in \gls{essence} as
follows:

\begin{plain}
language Essence 1.3

given w, g, s : int(1..)

letting Golfers be new type of size g * s

find sched : set (size w) of
             partition (regular, numParts g, partSize s) from Golfers

such that

forAll g1, g2 : Golfers, g1 < g2 .
    (sum week in sched . toInt(together({g1, g2}, week))) <= 1
\end{plain}

In \minizinc{} the same problem could be modelled as:

\begin{mzn}
include "globals.mzn";

int: g;
int: w;
int: s;

enum: golfers = anon_enum(g * s);

set of int: groups = 1..g;
set of int: rounds = 1..w;
array [rounds, groups] of var set of golfers: group;

constraint forall (r in rounds, g in groups) (
  card(group[r, g]) = s
);

constraint forall(r in rounds) (
  all_disjoint(g in groups)(group[r, g])
);

constraint forall (a, b in golfers where a < b) (
  sum (r in rounds, g in groups) (
    {a, b} subset group[r, g]
  ) <= 1
);
\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.

These high-level variables 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.

\section{Term Rewriting}%
\label{sec:back-term}

At the heart of the flattening process lies a \gls{trs}. A \gls{trs}
\autocite{baader-1998-term-rewriting} describes a computational model the full
process can be describe as the application of rules \(l \rightarrow r\), that
replace a \gls{term} \(l\) with another \gls{term} \(r\). A \gls{term} is an
expression with nested sub-expressions consisting of \emph{function} and
\emph{constant} symbols. An example of a term is \(F(0 + 1,F(1,0))\), where
\(F\) and \(+\) are function symbols and \(0\) and \(1\) are constant symbols.
In a term rewriting rule, a term can also contain a \emph{term variable} which
captures a term sub-expression. For example, the following \gls{trs} consists of
some (well-known) rules to handle logical and:

\begin{align*}
(r_{1}):\hspace{5pt}& 0 \land x \rightarrow 0 \\
(r_{2}):\hspace{5pt}& 1 \land x \rightarrow x \\
(r_{3}):\hspace{5pt}& x \land y \rightarrow y \land x
\end{align*}

From these rules it follows that

\[ 1 \land 1 \land 0 \rightarrow^{r_{1}} 1 \land 0 \rightarrow^{r_{3}} 0 \land 1 \rightarrow^{r_{2}} 0 \]

Notice that there can be a choice between different rules. A \gls{trs} can be
non-deterministic. In the example we could also have applied the \(r_{1}\) twice
and arrived at the same result. Two important properties of \gls{trs} are,
therefore, \gls{termination} and \gls{confluence}. A \gls{trs} is said to be
terminating if, no-matter what order the term rewriting rules are applied, you
always arrive at a \gls{normal-form} (\ie, a term where no more rules apply). A
\gls{trs} is confluent if, no-matter what order the term rewriting rules are
applied, you always arrive at the same \gls{normal-form} (if you arrive at a
\gls{normal-form}).

It is trivial to see that our previous example is non-terminating, since you can
repeat rule \(r_{3}\) an infinite amount of times. The system, however, is
confluent as, if it arrives at the same \gls{normal-form}: if the term contains
any \(0\), then the result will be \(0\); otherwise, the result will be \(1\).

In \minizinc\ the flattening process is forced to be confluent. Through the
function definitions in the language and the type system, \minizinc{} ensures
that there is at most one applicable rule for any expression. This means that
given the same \minizinc\ model and solver library, the flattening process will
result in the same solver level constraint model.

The flattening process is, however, not guaranteed to terminate. When using
recursive functions, it is possible to create a \minizinc\ model that never
reaches a flat state. In practice, however, function definitions generally do
not contain any recursive definitions. In the absence of recursive functions the
flattening of a model is guaranteed to terminate.

\subsection{Constraint Logic Programming}%
\label{subsec:back-clp}

\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}. Different from \minizinc{}, the programmer can
define constraints that can be rewritten in multiple ways. When such a
constraint occurs in the constraint model, referred to as the goal, the
constraint logic program will try a different way whenever the problem becomes
unsatisfiable.

To implement this mechanism there is a tight integration between the solver,
referred to as the constraint store, and constraint 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 unsatisfiable and then
\gls{backtrack} the constraint store to the last decision (\ie, restore the
constraint store to its state before the last decision was made).

\subsection{Constraint Handling Rules}%
\label{sub:back-chr}

\gls{chr} are a special kind of \glspl{trs} designed to

\subsection{ACD Term Rewriting}%
\label{subsec:back-acd}