diff --git a/assets/glossary.tex b/assets/glossary.tex index 0a3364d..8ebbebd 100644 --- a/assets/glossary.tex +++ b/assets/glossary.tex @@ -221,7 +221,7 @@ } \newglossaryentry{operator}{ - name={operators}, + name={operator}, description={}, } diff --git a/chapters/2_background.tex b/chapters/2_background.tex index ef502ff..8502170 100644 --- a/chapters/2_background.tex +++ b/chapters/2_background.tex @@ -76,14 +76,16 @@ the model. \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}. +In the remainder of this chapter we will first, in \cref{sec:back-minizinc} we +introduce \minizinc\ as the leading \cml\ used within this thesis. In +\cref{sec:back-solving} we discuss how \gls{cp} can be used to solve a +constraint model. We also briefly discuss other solving techniques and the +problem format these techniques expect. \Cref{sec:back-other-languages} +introduces alternative \cmls\ and compares their functionality to \minizinc{}. +Then,\cref{sec:back-term} survey the some closely related technologies in the +field of \glspl{trs}. Finally, \cref{sec:back-mzn-interpreter} explores the +process that the current \minizinc\ interpreter uses to translate a \minizinc\ +instance into a solver-level constraint model. \section{\glsentrytext{minizinc}}% \label{sec:back-minizinc} @@ -109,9 +111,9 @@ library of constraints allow users to easily model complex problems. 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 + \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\). The model then declares its \glspl{variable}. \Lref{line:back:knap:sel} @@ -330,6 +332,7 @@ 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} @@ -489,17 +492,29 @@ 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 Division (or modulus) when the divisor is zero: - \item Array access when the index is outside the given index set: \\ - \mzninline{array1d(1..3, [1,2,3])[0] = @??@} + \begin{mzn} + x div 0 = @??@ + \end{mzn} - \item Finding the minimum or maximum or an empty set: \\ \mzninline{min({}) - =@??@} + \item Array access when the index is outside the given index set: - \item Computing the square root of a negative value: \\ \mzninline{sqrt(-1) = - @??@} + \begin{mzn} + array1d(1..3, [1,2,3])[0] = @??@ + \end{mzn} + + \item Finding the minimum or maximum or an empty set: + + \begin{mzn} + min({}) = @??@ + \end{mzn} + + \item Computing the square root of a negative value: + + \begin{mzn} + sqrt(-1) = @??@ + \end{mzn} \end{itemize} @@ -589,331 +604,6 @@ input types and the basic method of solving the given problem. \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} @@ -1251,3 +941,327 @@ constraint store to its state before the last decision was made). \subsection{ACD Term Rewriting}% \label{subsec:back-acd} + +\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