%************************************************
\chapter{Rewriting Constraint Modelling Languages}\label{ch:rewriting}
%************************************************

\input{chapters/3_rewriting_preamble}


\section{Architecture Overview}
\label{sec:rew-arch}

\noindent{}\Gls{rewriting} a \minizinc{} instance into \gls{slv-mod} might often seem like a simple \gls{trs}.
In reality, however, \minizinc{} is quite a complex language, and producing a good \gls{slv-mod} is far from trivial. 

Thus, in practice, this rewriting process is a highly complex task that needs to carefully track interactions between \constraints{} and how they affect \variables{}.
To create an efficient \gls{slv-mod} the \gls{rewriting} process uses many simplification techniques such as:

\begin{itemize}
	\item continuously updating \variable{} \domains{},
	\item \gls{propagation} for known \constraints{},
	\item specialized \glspl{decomp} when variables get \gls{fixed},
	\item \gls{aggregation},
	\item common sub-expression elimination,
	\item and removing \variables{} and \constraints{} that are not required any longer.
\end{itemize}

We now present a new architecture for the \gls{rewriting} process that has been designed for the modern day needs of \minizinc{}.
At the core of our \gls{rewriting} process lie formalized rewriting rules.
As such, this architecture represents an abstract machine model for \minizinc{}.
These rules allow us to reason about the system and about the simplifications both to the process and the resulting \gls{slv-mod}.
The process can even be made incremental: in \cref{ch:incremental} we discuss how when making incremental changes to the \minizinc{} \instance{}, unchanged parts of the \instance{} do not need to be rewritten again.

\begin{figure}
	\centering
	\includegraphics[width=\linewidth]{assets/img/rew_compilation_structure}
	\caption{\label{fig:rew-comp} The proposed process for the compilation of \minizinc{} instances.}
\end{figure}

The process of the new architecture is shown in \cref{fig:rew-comp}.
After parsing and type checking, a \minizinc{} model is first compiled into a smaller constraint language called \microzinc{}, independent of the data.
For efficient execution, the \microzinc{} is then transformed into a \gls{byte-code}.
Together, the \gls{byte-code} and a complete \gls{parameter-assignment} form an \instance{} that can be executed by the \microzinc{} \interpreter{}.
During its execution, the \interpreter{} continuously updates a \cmodel{} according to the \microzinc{} definition.
The \cmodel{} in the \interpreter{} is internally represented as a \nanozinc{} program.
\nanozinc{} is a slight extension of the \flatzinc{} format.
The \interpreter{} finishes when it reaches a \gls{slv-mod}.

We have developed a prototype of this tool chain, and present experimental validation that the new tool chain can perform \gls{rewriting} much faster, and produce better models, than the current \minizinc{} \compiler{}.

\section{\glsentrytext{microzinc} and \glsentrytext{nanozinc}}\label{sec:rew-micronano}

This section introduces the two sub-languages of \minizinc{} at the core of the new architecture we have developed.

\microzinc{} is a simple language used to define transformations to be performed by the \interpreter{}.
It is simplified subset of \minizinc{}.
The transformation are represented in the language through the use of function definitions.
A function of type \mzninline{var bool}, describing a relation, can be defined as a \gls{native} \constraint{}.
Otherwise, a function body must be provided for \gls{rewriting}.
The function body can use a restriction of the \minizinc{} expression language.

An important difference between \minizinc{} and \microzinc{} is that a well-formed \microzinc{} does not contain partial expressions.
Any partiality in the \minizinc{} model must be explicitly expressed using total functions in \microzinc{}.
As such, \constraints{} introduced in \microzinc{} \glspl{let} can be globally enforced.
They are guaranteed to only constrain the \variables{} introduced in the same \gls{let}.

\nanozinc{} is used to represent the current state of the \instance{}.
\nanozinc{} is similar to \flatzinc{} in that it contains only declarations of \variables{} and a flat list of \constraints{}.
However, while all function calls in \flatzinc{} need to be \gls{native}, \nanozinc{} calls can refer to any function implemented in \microzinc{}.
Furthermore, \nanozinc{} allows for \constraints{} to be ``attached'' to a \variable{}, in order to be able to track their lifetime and remove them if the corresponding \variable{} becomes unused.
As a small syntactic difference with \flatzinc{}, \constraints{} and \variable{} declarations in \nanozinc{} can be freely interleaved.

The core of the syntax of \microzinc{} is defined in \cref{fig:rew-uzn-syntax}.
In \microzinc{} it is specifically used to mark functions that are \gls{native} to the target \solver{}.
We have omitted the definitions of \syntax{<mzn-type-inst>} and \syntax{<ident>}, which can be assumed to be the same as the definition of \syntax{<type-inst>} and \syntax{<ident>} in the \minizinc{} grammar, see \cref{ch:minizinc-grammar}.
While we omit the typing rules here for space reasons, we will assume that in well-typed \microzinc{} programs conditions of expressions are \parameters{}.
This means that the where conditions \syntax{<exp>} in \glspl{comprehension}, the conditions \syntax{<exp>} in \gls{conditional} expressions, and the \syntax{<literal>} index in \gls{array} accesses must have \mzninline{par} type.
In \minizinc{} the use of \variables{} in these positions is allowed, and these expressions are rewritten to function calls.
We will discuss how the same transformation takes place in when translating \minizinc{} to \microzinc{}.

\begin{figure}
	\begin{grammar}
		<model> ::= <pred-decl>*<fun-decl>*

		<fun-decl> ::= "function" <type-inst>":" <ident>"(" <typing> ["," <typing>]* ")" "=" <exp>";"
		\alt "function" "var" "bool" ":" <ident>"(" <typing> ["," <typing>]* ")"";"

		<literal> ::= <constant> | <ident>

		<exp> ::= <literal>
		\alt <ident>"(" <exp> ["," <exp>]* ")"
		\alt "let" "{" <item>* "}" "in" <literal>
		\alt "if" <exp> "then" <exp> "else" <exp> "endif"
		\alt "[" <exp> "|" <gen-exp> "where" <exp> "]"
		\alt <ident>"[" <literal> "]"

		<item> ::= <typing> [ "=" <exp> ]";"
		\alt "tuple(" <type-inst> ["," <type-inst>]* "):" <ident> = "(" <exp> ["," <exp>]* ")"";"
		\alt "(" <typing> ["," <typing>]* ")" "=" <exp>";"
		\alt "constraint" <exp>";"

		<typing> ::= <type-inst>":" <ident>

		<gen-exp> ::= <ident> "in" <exp> ["," <ident> "in" <exp> ]*
	\end{grammar}
	\caption{\label{fig:rew-uzn-syntax}Syntax of \microzinc{}.}
\end{figure}

A \nanozinc{} program, defined in \cref{fig:rew-nzn-syntax}, is simply a list of \variable{} declarations and \constraints{} in the form of calls.
The syntax ``\texttt{↳}'' will be used to ``attach'' \constraints{} to \variables{} in order to track dependent \constraints{}.
This will be explained in detail in \cref{sec:rew-nanozinc}.

\begin{figure}
	\begin{grammar}
		<nzn> ::= <nzn-item>*

		<nzn-item> ::= <nzn-def> | <nzn-con>

		<nzn-con> ::= "constraint" <ident>"(" <literal> ["," <literal>]* ")"";"

		<nzn-var> ::= "var" <nzn-dom> ":" <ident> ";" <nzn-attach>*

		<nzn-dom> ::=  <constant> ".." <constant> | <constant>
		\alt "bool" | "int" | "float" | "set of int"

		<nzn-attach> ::= "↳" <nzn-con>
	\end{grammar}
	\caption{\label{fig:rew-nzn-syntax}Syntax of \nanozinc{}.}
\end{figure}

\subsection{\glsentrytext{minizinc} to \glsentrytext{microzinc}}

The translation from \minizinc{} to \microzinc{} involves the following steps.

\begin{enumerate}

	\item Transform all expressions that are valid in \minizinc{} but not in \microzinc{}.
		This includes simple cases such as replacing operator expressions, like \mzninline{x+y}, by function calls, \mzninline{int_plus(x,y)}, and replacing generators in calls, like \mzninline{sum(x in A)(x)}, by \glspl{comprehension}, \mzninline{sum([x|x in A])}.
		As mentioned above, \gls{conditional} expressions where the decision is made by a \variable{} are also not directly supported in \microzinc{}.
		These expressions are therefore also replaced by function calls that are possibly decomposed.
		An expression \mzninline{if x then A else B endif}, where \mzninline{x} is a \variable{}, is replaced the following call.
		
		\begin{mzn}
			if_then_else([x, true], [A, B])
		\end{mzn}

		And, an expression \mzninline{A[x]}, where \mzninline{x} is a \variable{}, is replaced by the following call.

		\begin{mzn}
			element(A, x)
		\end{mzn}

		\mzninline{element} is a well-known \gls{global}.
		For many \gls{cp} \solvers{} it is a \gls{native} \constraint{} and for other \solvers{} there have long been accepted \glspl{decomp}.
		A recent study by \textcite{stuckey-2019-conditionals} describes how \mzninline{if_then_else} can be decomposed for different types of \solvers{}.

	\item Replace optional \variables{} into non-optional forms.
		As shown by \textcite{mears-2014-option}, optional type \variables{} can be represented using a \variable{} of the same non-optional type and a Boolean \variable{}.
		The Boolean \variable{}, then, represents if the variable exists or is absent, while the non-optional \variable{} of the same type represents the value of the optional \variable{} if it exists.
		In \microzinc{} this can be represented as a tuple of the two \variables{}.
		The function definitions for optional types then take both \variables{} into account.
		For example, the definition of \mzninline{int_plus(x, y)} for optional types can be translated into the function shown in \cref{lst:rew-opt-plus}.

		\begin{listing}
			\mznfile{assets/listing/rew_opt_plus.mzn}
			\caption{\label{lst:rew-opt-plus} A definition of \mzninline{int_plus} for optional integers in \microzinc{} syntax.}
		\end{listing}

	\item Lift the partiality in expressions into the surrounding context to implement \minizinc{}'s relational semantics.
		In contrast to \minizinc{}, a \microzinc{} expression must be total.
		\textcite{stuckey-2013-functions} have extensively examined these problems and describe how to transform any partial function into a total function while maintaining the relational semantics of the original \cmodel{}.
		A general approach for describing the partiality in \microzinc{} functions is to make the function return an additional Boolean \variable{}.
		This \variable{} indicates whether the result of the function call is defined w.r.t. the function arguments.
		The resulting value of the function is then adjusted to return a predefined value when it would normally be undefined.
		For example, the \mzninline{element} function in \minizinc{} is declared as follows.

		\begin{mzn}
			function var int: element(array of int: a, var int: x);
		\end{mzn}

		\noindent{}It is only defined when \mzninline{x in index_set(a)}.
		The function shown in \cref{lst:rew-elem-safe} is a total version of this function that can be used in \microzinc{}\footnote{For brevity's sake, we will still use \minizinc{} \glspl{operator} to write the \microzinc{} definition.}.

		\begin{listing}
			\mznfile{assets/listing/rew_elem_safe.mzn}
			\caption{\label{lst:rew-elem-safe} A total of the \mzninline{element} function in \microzinc{}.}
		\end{listing}

		Similar to the replacement of optional values, all occurrences of the \mzninline{element} function are replaced by \mzninline{element_safe}.
		The usage of its result should be guarded by the returned totality variable in the surrounding Boolean context.
		This means that, for example, the expression \mzninline{element(e, v) = 5 \/ b} would be replaced by the following expression.

		\begin{mzn}
			let {
				(var int: res, var bool: total) = element(e, v);
			} in (total /\ res = 5) \/ b;
		\end{mzn}

	\item Resolve sub-type based overloading statically.
		To prevent the runtime overhead of the dynamic lookup of overloaded function definitions for every call, the function dispatch in \microzinc{} is determined statically.

		It is important, however, that the correct version of a function is chosen when it allows for either \variable{} and \parameter{} arguments.
		And, as we will later discuss in more detail, is possible for a \variable{} to be \gls{fixed} to a single value during the \gls{rewriting} process.
		At that point it can be treated as a \parameter{}.
		To ensure the correct version of the function is used, functions are changed to, at runtime, check if a \variable{} is fixed and, if so, dispatch to the \parameter{} version of the function.
		If we, for example, have a \minizinc{} function \mzninline{f} that is overloaded on \mzninline{var int} and \mzninline{int}, then the \microzinc{} transformation can be described by the following two functions.

		\begin{mzn}
			function f_int(int: x) = /* original body */;
			function f_varint(var int: x) =
			if is_fixed(x) then
				f_int(fix(x))
			else
				/* original body */;
			endif;
		\end{mzn}

	\item Transform all function definitions so that they do not refer to \variables{} and \parameters{} defined outside the scope of the function.
		Instead, they are added as extra arguments to the function definition and each call.

	\item Move all top-level \variable{} declarations and \constraints{} into a let expression in the body of a new function called \mzninline{main}.
		The arguments to this function are the top-level \parameters{} of the \minizinc{} model, and it returns a fresh Boolean \variable{}.

\end{enumerate}

\begin{example}

	Consider the \minizinc{} model in \cref{lst:rew-pigeon-mzn}.
	It describes a simple \gls{unsat} ``pigeonhole problem'': trying to assign \(n\) pigeons to \(n-1\) holes.

		\begin{listing}
			\mznfile{assets/listing/rew_pigeon_mzn.mzn}
			\caption{\label{lst:rew-pigeon-mzn} A \minizinc{} model of the pigeonhole problem.}
		\end{listing}

	The translation to \microzinc{} turns all expressions into function calls, replaces the special generator syntax in the \mzninline{forall} with an \gls{array} \gls{comprehension}, and creates the \mzninline{main} function.
	The result of this translation is shown in \cref{lst:rew-pigeon-uzn}.

	\begin{listing}
		\mznfile{assets/listing/rew_pigeon_uzn.mzn}
		\caption{\label{lst:rew-pigeon-uzn} The \microzinc{} translation of the pigeonhole problem in \cref{lst:rew-pigeon-mzn}.}
	\end{listing}

	For an \instance{} of the \cmodel{}, we can then create a simple \nanozinc{} program that calls \mzninline{main}.
	For example for \(n=10\), we would create the following \nanozinc{} program.

	\begin{nzn}
		constraint main(10);
	\end{nzn}

\end{example}

\subsection{Partial Evaluation of \glsentrytext{nanozinc}}\label{sub:rew-partial}

Each call in a \nanozinc{} program is either a call to a \gls{native} \constraint{}, or it has a corresponding \microzinc{} function definition.
The goal of partial evaluation is to rewrite the \nanozinc{} program into a \gls{slv-mod}, i.e., a program where all calls are calls to \gls{native} \constraints{}. 

To achieve this, we define the semantics of \microzinc{} as a \gls{rewriting} system that produces \nanozinc{} calls.
Each non-\gls{native} call in a \nanozinc{} program can then be replaced with the result of evaluating the corresponding \microzinc{} function.

A key element of this \gls{rewriting} process, then, is the transformation of functional expressions into relational form.
For this to happen, the \gls{rewriting} process introduces fresh \variables{} to represent intermediate expressions.

\begin{example}\label{ex:rew-abs}
	Consider the (reasonably typical) \minizinc{} encoding for the absolute value function presented in \cref{lst:rew-abs}.
	When an occurrence of \mzninline{abs} is encountered, the call will be replaced by a \variable{} \mzninline{z}.
	But before that can occur, the \variable{} must be introduced, and the \constraint{} \mzninline{int_abs(x, z)} is added to the model, enforcing its value.

	\begin{listing}
		\mznfile{assets/listing/rew_abs.mzn}
		\caption{\label{lst:rew-abs} A \minizinc{} definition for the absolute value function.}
	\end{listing}
\end{example}

The function \mzninline{abs(x)} above is a total function: for every value of \mzninline{x}, there is always exactly one valid value of \mzninline{z}.
In this case, the \constraint{} introduced in the \gls{let} may be enforced globally, and multiple occurrences of \mzninline{abs(x)} may be replaced with the same \mzninline{z}.
However, the introduced \mzninline{int_abs} \constraint{} is only needed so long as any other \constraint{} refers to \mzninline{z}.
If \mzninline{z} is unused in the rest of the model, both \mzninline{z} and the \mzninline{int_abs} \constraint{} can be removed.

As we shall see in \cref{sec:rew-simplification}, certain optimizations and simplifications during the evaluation can lead to many expressions becoming unused.
It is therefore important to track which \constraints{} were merely introduced to define results of function calls.
In order to track these dependencies, \nanozinc{} attaches \constraints{} that define a variable to the item that introduces the \variable{}.

\subsection{\glsentrytext{nanozinc}}\label{sec:rew-nanozinc}

A \nanozinc{} program (\cref{fig:rew-nzn-syntax}) consists of a topologically-ordered list of declarations of \variables{} and \constraints{}.
\Variables{} are declared with an identifier, a domain, and are associated with a list of attached \constraints{}.
\Constraints{} can also occur at the top-level of the \nanozinc{} program.
These are said to be the \rootc{}-context \constraints{} of the \cmodel{}, i.e., those that have to hold globally and are not just used to define an \gls{avar}.
Only root-context \constraints{} can effectively constrain the overall problem.
\Constraints{} attached to \variables{} originate from function calls, and since all functions are guaranteed to be total, attached \constraints{} can only define the function result.

\begin{example}\label{ex:rew-absnzn}

	Consider the following \minizinc{} fragment.

	\begin{mzn}
		constraint abs(x) > y;
	\end{mzn}

	\noindent{}If we assume that \mzninline{x} and \mzninline{y} have a \domain{} of \mzninline{-10..10}, then after \gls{rewriting} it would result in the following resulting \nanozinc{} program.

	\begin{nzn}
		var -10..10: x;
		var -10..10: y;
		var int: z;
		↳ constraint int_abs(x, z);
		constraint int_gt(z, y);
	\end{nzn}

	Evaluating the call \mzninline{abs(x)} introduces a new \variable{} \mzninline{z} (with unrestricted domain) and the \mzninline{int_abs} \constraint{} that is used to define \mzninline{z}.
	The top-level \constraint{} \mzninline{abs(x) > y} is rewritten into \mzninline{int_gt(z, y)} and added as a top-level \constraint{}.
\end{example}

\subsection{Rewriting Rules}

The core of the proposed \minizinc{} architecture is an abstract machine that rewrites \nanozinc{} items using the corresponding \microzinc{} function definitions.
We can now formally define the rewriting rules for this abstract machine.

The full set of rules appears in \cref{fig:rew-rewrite-to-nzn-calls,fig:rew-rewrite-to-nzn-let,fig:rew-rewrite-to-nzn-other}.
To simplify presentation, we assume that all rules that introduce new identifiers into the \nanozinc{} program do so in a way that ensures those identifiers are fresh (i.e., not used in the rest of the \nanozinc{} program), by suitable alpha renaming.
We also present our rules using a \emph{call by name} evaluation strategy, i.e., the arguments to function calls are substituted into function body.
As such, they are only evaluated when required for the result of the function.
Although pure \microzinc{} behaves the same under any call evaluation strategy, in implementation a \emph{call by value} strategy might provide more predictable behaviour with debugging functions in the \minizinc{} language, such as \mzninline{trace} and \mzninline{assert}.

\begin{figure*}[p]
	\centering
	\begin{prooftree}
		\hypo{\texttt{function} ~t\texttt{:}~\ptinline{F(\(p_1, \ldots{}, p_k\)) = E;} \in{} \Prog{} \text{~where the~} p_i \text{~are fresh}}
		\infer[no rule]1{\Sem{\(\ptinline{E}_{[p_i \mapsto a_i, \forall{} 1 \leq{} i \leq{} k]}\)}{\Prog, \Env} \Rightarrow{} \tuple{v, \Env'}}
		\infer1[(Call)]{\Sem{F(\(a_1, \ldots, a_k\))}{\Prog, \Env} \Rightarrow{} \tuple{v, \Env'}}
	\end{prooftree} \\
	\bigskip
	\begin{prooftree}
		\hypo{\ptinline{F} \in \text{Builtins}}
		\infer1[(CallBuiltin)]{\Sem{F(\(a_1, \ldots, a_k\))}{\Prog, \Env} \Rightarrow{} \tuple{\ensuremath{\mathit{eval}(\ptinline{F}(a_1,\ldots, a_k))}, \Env}}
	\end{prooftree} \\
	\bigskip
	\begin{prooftree}
		\hypo{\texttt{function var bool:}~\ptinline{F(\(p_1, \ldots, p_k\));} \in \Prog}
		\infer1[(CallNative)]{\Sem{F(\(a_1, \ldots, a_k\))}{\Prog, \Env} \Rightarrow{}
			\tuple{\ensuremath{\texttt{constraint}~\ptinline{F}(a_1, \ldots, a_k), \Env}}}
	\end{prooftree}
	\caption{\label{fig:rew-rewrite-to-nzn-calls} Rewriting rules for partial evaluation of \microzinc{} calls to \nanozinc{}.}
\end{figure*}

The rules in \cref{fig:rew-rewrite-to-nzn-calls} handle function calls.
The first rule, (Call), evaluates a function call expression in the context of a \microzinc{} program \(\Prog{}\) and \nanozinc{} program \(\Env{}\).
The rule evaluates the function body \(\ptinline{E}\) where the formal parameters \(p_{i}\) are substituted by the call arguments \(a_{i}\).\footnote{We use \(E_{[a \mapsto b]}\) as a notation for the expression \(E\) where \(a\) is substituted by \(b\).} The result of this evaluation is the result of the function call.

The (CallBuiltin) rule applies to ``built-in'' functions that can be evaluated directly, such as arithmetic and Boolean operations on fixed values.
The rule simply returns the result of evaluating the built-in function on the evaluated parameter values.

The (CallNative) rule applies to calls to \mzninline{var bool} functions, that describe relations, that have been marked as \constraints{} \gls{native} to the \solver{}.
Since these are directly supported by the \solver{}, they simply need to be transferred into the \nanozinc{} program.

\begin{figure*}[p]
	\centering
	\begin{prooftree}
		\hypo{\Sem{\(\mathbf{I} \mid{} \mathbf{X}\)}{\Prog, \Env, \emptyset} \Rightarrow \tuple{x, \Env'}}
		\infer1[(Let)]{\Sem{let \{ \(\mathbf{I}\) \} in \(\mathbf{X}\)}{\Prog, \Env} \Rightarrow{} \tuple{x, \Env'}}
	\end{prooftree} \\
	\bigskip
	\begin{prooftree}
		\hypo{\Sem{\(\mathbf{X}\)}{\Prog, \{ t : x \} \cup{} \Env} \Rightarrow \tuple{x, \{ t: x \} \cup{} \Env'}}
		\infer1[(Item0)]{\Sem{\(\epsilon{} \mid{} \mathbf{X}\)}{\Prog, \{ t: x \}\cup{}\Env, \Ctx} \Rightarrow{} \tuple{x, \{ t: x \texttt{~↳~} \Ctx{} \} \cup{} \Env'}}
	\end{prooftree} \\
	\bigskip
	\begin{prooftree}
		\hypo{\Sem{\(C\)}{\Prog, \Env} \Rightarrow \tuple{c, \Env'}}
		\hypo{\Sem{\(\mathbf{I} \mid{} \mathbf{X}\)}{\Prog, \Env', \{c\}\cup\Ctx} \Rightarrow \tuple{x, \Env''}}
		\infer2[(ItemC)]{\Sem{\(\mbox{constraint}~C\texttt{;} \mathbf{I} \mid{} \mathbf{X}\)}{\Prog, \Env, \Ctx} \Rightarrow{} \tuple{x, \Env''}}
	\end{prooftree} \\
	\bigskip
	\begin{prooftree}
		\hypo{\Sem{\(\mathbf{I} \mid{} \mathbf{X}\)}{\Prog, \Env{} \cup{} \{t : x\}, \Ctx} \Rightarrow \tuple{x, \Env'}}
		\infer1[(ItemT)]{\Sem{\(t\texttt{:}~x\texttt{;} \mathbf{I} \mid{} \mathbf{X}\)}{\Prog, \Env, \Ctx} \Rightarrow{} \tuple{x, \Env'}}
	\end{prooftree} \\
	\bigskip
	\begin{prooftree}
		\hypo{\Sem{\(E\)}{\Prog, \Env} \Rightarrow \tuple{v, \Env'}}
		\hypo{\Sem{\(\mathbf{I}_{[x \mapsto v]} \mid{} \mathbf{X}_{[x \mapsto v]}\)}{\Prog, \Env', \Ctx} \Rightarrow{} \tuple{x, \Env''}}
		\infer2[(ItemTE)]{\Sem{\(t\texttt{:}~x = E\texttt{;} \mathbf{I} \mid{} \mathbf{X}\)}{\Prog, \Env, \Ctx} \Rightarrow{} \tuple{x, \Env''}}
	\end{prooftree} \\
	\bigskip
	\begin{prooftree}
		\hypo{\Sem{\(E_{i}\)}{\Prog,\Env^{i-1}} \Rightarrow \tuple{v_{i}, \Env^{i}}, \forall{} 1 \leq{} i \leq{} k}
		\infer[no rule]1{\Sem{\(\mathbf{I}_{[x_{\langle{}i\rangle} \mapsto v_{i}, \forall{} 1 \leq{} i \leq{} k]} \mid{} \mathbf{X}_{[x_{\langle{}i\rangle} \mapsto v_{i}, \forall{} 1 \leq{} i \leq{} k]}\)}{\Prog, \Env^{k}, \Ctx} \Rightarrow{} \tuple{x, \Env'}}
		\infer1[(ItemTupC)]{\Sem{\( \texttt{tuple(}t_{1}, \ldots, t_{k}\texttt{):}~x = \left(E_{1}, \ldots, E_{k}\right)\)}{\Prog, \Env^{0}, \Ctx} \Rightarrow{} \tuple{x, \Env'}}
	\end{prooftree} \\
	\bigskip
	\begin{prooftree}
		\hypo{\Sem{\(E\)}{\Prog, \Env} \Rightarrow \tuple{\left(v_{\langle{}1\rangle}, \ldots, v_{\langle{}k\rangle}\right), \Env'}}
		\infer[no rule]1{\Sem{\(\mathbf{I}_{[x_{i} \mapsto v_{\langle{}i\rangle}, \forall{} 1 \leq{} i \leq{} k]} \mid{} \mathbf{X}_{[x_{i} \mapsto v_{\langle{}i\rangle}, \forall{} 1 \leq{} i \leq{} k]}\)}{\Prog, \Env', \Ctx} \Rightarrow{} \tuple{x, \Env''}}
		\infer1[(ItemTupD)]{\Sem{\(\left(t_{1}\texttt{:}~x_{1}, \ldots, t_{k}\texttt{:}~x_{k}\right) = E\texttt{;} \mathbf{I} \mid{} \mathbf{X}\)}{\Prog, \Env, \Ctx} \Rightarrow{} \tuple{x, \Env''}}
	\end{prooftree}
	\caption{\label{fig:rew-rewrite-to-nzn-let} Rewriting rules for partial evaluation of \microzinc{} \glspl{let} to \nanozinc{}.}
\end{figure*}

The rules in \cref{fig:rew-rewrite-to-nzn-let} consider \glspl{let}.
Starting from the main rule, (Let), the let items \textbf{I} are evaluated one at a time.
\Glspl{constraint} that follow from the evaluation of the let expression, by the (ItemC) rule, are collected in the third component, \(\phi{}\), of the evaluation arguments.
When all inner items have been evaluated, the captured \constraints{} are attached to the literal returned by the body of the let expression \textbf{X} in (Item0).
The (ItemT) rule handles introduction of new \variables{} by adding them to the context.
The (ItemTE) rule handles introduction of new \variables{} with a defining equation by evaluating them in the current context and substituting the name of the new \variable{} by the result of evaluation in the entire scope of the variable.
The rules (ItemTupC) and (ItemTupD) are for the construction and deconstruction of tuple objects.
We use the notation \(x_{\langle{}i\rangle}\) to mark the \(i^{\text{th}}\) member of the tuple \(x\) in our substitution notation.

\begin{figure*}
	\centering
	\begin{prooftree}
		\hypo{x \in \langle \text{ident} \rangle}
		\hypo{\{t: x \texttt{~↳~} \phi{} \} \in \Env}
		\infer2[(Ident)]{\Sem{\(x\)}{\Prog, \Env} \Rightarrow{} \tuple{x, \Env}}
	\end{prooftree} \\
	\bigskip
	\begin{prooftree}
		\hypo{c \text{~constant}}
		\infer1[(Const)]{\Sem{\(c\)}{\Prog, \Env} \Rightarrow{} \tuple{c, \Env}}
	\end{prooftree} \\
	\bigskip
	\begin{prooftree}
		\hypo{\Sem{\(x\)}{\Prog, \Env} \Rightarrow \tuple{[x_{n}, \ldots, x_{m}], \Env'}}
		\hypo{\Sem{\(i\)}{\Prog, \Env'} \Rightarrow \tuple{v, \Env''}}
		\hypo{v \in [n \ldots{} m]}
		\infer3[(Access)]{\Sem{\(x\texttt{[}i\texttt{]}\)}{\Prog, \Env} \Rightarrow{} \tuple{x_{v}, \Env''}}
	\end{prooftree} \\
	\bigskip
	\begin{prooftree}
		\hypo{\Sem{\(C\)}{\Prog, \Env} \Rightarrow \tuple{\ptinline{true}, \_}}
		\infer1[(If\(_T\))]{\Sem{if \(C\) then \(E_t\) else \(E_e\) endif}{\Prog, \Env} \Rightarrow{} \Sem{\(E_t\)}{\Prog, \Env}}
	\end{prooftree} \\
	\bigskip
	\begin{prooftree}
		\hypo{\Sem{\(C\)}{\Prog, \Env} \Rightarrow \tuple{\ptinline{false}, \_}}
		\infer1[(If\(_F\))]{\Sem{if \(C\) then \(E_t\) else \(E_e\) endif}{\Prog, \Env} \Rightarrow{} \Sem{\(E_e\)}{\Prog, \Env}}
	\end{prooftree} \\
	\bigskip
	\begin{prooftree}
		\hypo{\Sem{G}{\Prog,\Env} \Rightarrow \tuple{ \ptinline{true}, \_}}
		\hypo{\Sem{\(E\)}{\Prog, \Env} \Rightarrow \tuple {v, \Env'}}
		\infer2[(WhereT)]{\Sem{\([E ~|~ \mbox{where~} G]\)}{\Prog, \Env} \Rightarrow{} \tuple{[v], \Env'}}
	\end{prooftree} \\
	\bigskip
	\begin{prooftree}
		\hypo{\Sem{G}{\Prog,\Env} \Rightarrow \tuple{\ptinline{false}, \_}}
		\infer1[(WhereF)]{\Sem{\([E ~|~ \mbox{where~} G]\)}{\Prog, \Env} \Rightarrow{} \tuple{[], \Env}}
	\end{prooftree} \\
	\bigskip
	\begin{prooftree}
		\hypo{\Sem{\(\mathit{PE}\)}{\Prog,\Env} \Rightarrow \tuple{S, \_}}
		\infer[no rule]1{\Sem{\([E ~|~ \mathit{GE} \mbox{~where~} G]\)}{\Prog, \Env_{[x \mapsto{} v]}} \Rightarrow{} \tuple{A_v, \Env_{[x \mapsto{} v]} \cup{} \Env{}_{v}}, \forall{} v \in{} S }
		\infer1[(ListG)]{\Sem{\([E~|~ x \mbox{~in~} \mathit{PE}, \mathit{GE} \mbox{~where~} G]\)}{\Prog, \Env} \Rightarrow{}
		\tuple{\mbox{concat} [ A_v~|~v \in{} S ], \Env{} \cup{} \bigcup{}_{v \in{} S} \Env{}_{v}}}
	\end{prooftree}
	\caption{\label{fig:rew-rewrite-to-nzn-other} Rewriting rules for partial evaluation of other \microzinc{} expressions to \nanozinc{}.}
\end{figure*}

Finally, the rules in \cref{fig:rew-rewrite-to-nzn-other} handle the evaluation of \variables{}, constants, \glspl{conditional}, and \glspl{comprehension}.
The (Ident) rule looks up a \variable{} in the environment and returns the \variable{} itself to be used in any \constraints{}.
The (Const) rule simply returns the constant.
The (Acess) rule evaluates the \gls{array} expression \(x\) and the index \(i\).
It then returns the element from the evaluated \gls{array} chosen by the evaluated index.
Note that, in well-defined \microzinc{}, the index \(i\) must evaluate to a value within the index range of the evaluated \gls{array} \(x\).
The (If\(_T\)) and (If\(_F\)) rules evaluate the if condition and then return the result of the then or else branch appropriately.
The (WhereT) rule evaluates the guard of a where \gls{comprehension} and if \true{} returns the resulting expression in a list.
The (WhereF) rule evaluates the guard and when \false{} returns an empty list.
The (ListG) rule evaluates the iteration set \(PE\) to get its value \(S\), which must be fixed.
It then evaluates the expression \(E\) with all the different possible values \(v \in S\) of the generator \(x\), collecting the additional \nanozinc{} definitions \(\Env_v\).
It returns the concatenation of the resulting lists with all the additional \nanozinc{} items.

\subsection{Prototype Implementation}

Our prototype implementation of the \microzinc{}/\nanozinc{} framework consists of the following components.

The \gls{compiler} translates \minizinc{} into a \gls{byte-code} encoding of \microzinc{}.
The compiler currently supports a significant subset of the full \minizinc{} language.
The missing features, such floating point values and complex output statements, require additional engineering effort, but do not require new technology.

The \gls{interpreter} evaluates \microzinc{} \gls{byte-code} and \nanozinc{} programs based on the \gls{rewriting} system introduced in this section.
It can read \parameters{} from a file or via an \gls{api}.
The \gls{interpreter} constructs the call to the \mzninline{main} function, and then performs the \gls{rewriting} into \gls{slv-mod} \nanozinc{}.
Memory management is implemented using reference counting, which lends itself well to the simplifications discussed in the next section.
The interpreter is written in around 3.5kLOC of C++ to enable easy embedding into applications and other programming languages.

The framework has the ability to support multiple \solvers{}.
It can pretty-print the \nanozinc{} code to standard \flatzinc{}, so that any solver currently compatible with \minizinc{} can be used.
Additionally, a direct C++ \gls{api} can be used to connect solvers directly, in order to enable incremental solving.
We revisit this topic in \cref{ch:incremental}.
The source code for the complete system will be made available under an open source licence.
\todo{Actually make source available}

\section{NanoZinc Simplification}\label{sec:rew-simplification}

The previous section introduced the basic evaluation model of \nanozinc: each call that has a corresponding \microzinc{} definition can be rewritten into a set of calls by evaluating the \microzinc{} code.
This section looks at further steps that the system can perform in order to produce better, more compact \glspl{slv-mod}.

\subsection{Removing unused decision variables and constraints}

The most basic form of simplification is to identify \variables{} that are not used by any call, and remove them.
This is correct because the semantics of \nanozinc{} requires us to find values for all \variables{} such that all \constraints{} are \gls{satisfied} --- but if a \variable{} does not occur in any \constraint{}, we can pick any value for it.
The model without the unused \variable{} is therefore \gls{eqsat} with the original model.

Consider now the case where a \variable{} in \nanozinc{} is only used in its attached \constraints{}.
The \constraints{} directly succeeding the declaration prepended by \texttt{↳}.

\begin{example}\label{ex:rew-absreif}

	The following is a slight variation on the \minizinc{} fragment in \cref{ex:rew-absnzn}.

	\begin{mzn}
		constraint abs(x) > y \/ c;
		constraint c;
	\end{mzn}

	The \constraint{} \mzninline{abs(x) > y} is now used in a disjunction.
	This means that instead of enforcing the \constraint{} globally, we need to create a \gls{reif}.
	Following the rewriting rules, the generated \nanozinc{} code will look very similar to the code generated in \cref{ex:rew-absnzn}, but with an additional \mzninline{bool_or} \constraint{} for the disjunction.
	It uses a \variable{} \mzninline{b} that will be introduced for \mzninline{abs(x) > y}.
	The \gls{rewriting} of this fragment will result in the following \nanozinc{} program.

	\begin{nzn}
		var true: c;
		var -10..10: x;
		var -10..10: y;
		var int: z;
		↳ constraint int_abs(x, z);
		var bool: b;
		↳ constraint int_gt_reif(z, y, b);
		constraint bool_or(b, c);
	\end{nzn}

	Evaluating \mzninline{constraint c} has resulted in the domain of \mzninline{c} to be \gls{fixed} to \true{}.
	The disjunction now trivially holds, independent of the value of \mzninline{b}.
	The \gls{reif} of \mzninline{abs(x) > y} is therefore not required.
	However, the \gls{rewriting} has to choose a particular order in which arguments are evaluated, so it is always possible that it already evaluated the left-hand side before ``noticing'' that the disjunction is \gls{satisfied}.

	If the system now simplifies the \constraint{} \mzninline{bool_or(b, c)} to true, then the identifier \mzninline{b} will become unused outside its attached \constraints{}.
	It was only referenced from the \mzninline{bool_or} call.
	Removing \mzninline{b} leads to its defining \constraint{}, \mzninline{int_gt_reif}, being removed.
	This in turn means that \mzninline{z} is not referenced anywhere outside its attached \constraints{}.
	It can also be removed together with its definition.
	The resulting \nanozinc{} program is much more compact.

	\begin{nzn}
		var true: c;
		var -10..10: x;
		var -10..10: y;
	\end{nzn}

	We assume here that \mzninline{c}, \mzninline{x} and \mzninline{y} are used in other parts of the model not shown here and therefore not removed.
	Note how it is crucial to exclude the attached \constraints{} when counting the usage of \variables{}.
	\mzninline{int_abs(x, z)}, the \constraint{}  which merely defines \mzninline{z}, would otherwise force us to keep \mzninline{z} in the \nanozinc{} program, if it were included in the count.
\end{example}

It is important to notice the difference between \constraints{} that appear at the top level and \constraints{} that appear as part of the attached \constraints{} of a \variable{}.
Top-level \constraints{} help define the problem, they are globally enforced and cannot be removed from the problem unless it can be proved that its relations are already enforced.
\Constraints{} attached to a \variable{}, on the other hand, are used to define a \variable{}.
\Constraints{} are generally attached when they stem from a functional relation, like \mzninline{abs(x)} in the example, or from a \gls{reif}, like \mzninline{abs(x) > y} when used in the disjunction with \mzninline{c}.
In this thesis we will follow the same naming standard as \minizinc{}, where a \gls{reif} of a \constraint{} has the same name as the original \constraint{} with \texttt{\_reif} appended.

\begin{example}
	The importance of the use of attached \constraints{} when removing unused \variables{} and \constraints{} is demonstrated in the following \minizinc{} fragment.

	\begin{mzn}
		int: n;
		var int: x;
		function var int: f(var int: x, int: i) = let {
			var int: y;
			constraint y = x * i;
		} in y;
		constraint [f(x,i) | i in 1..n][n] == 10;
	\end{mzn}

	The \gls{rewriting} of this \minizinc{} model will initially create the \mzninline{n} elements for the \gls{array} \gls{comprehension}.
	Each element is evaluated as a new \variable{} \mzninline{y} and a \constraint{} to ensure that \mzninline{y} is the multiplication of \mzninline{x} and \mzninline{i}.
	Although \mzninline{n} variables are created, only the last \variable{} is constrained to take the value ten.
	All other \variables{} can thus be removed, and the model will stay \gls{eqsat}.

	In the \nanozinc{} version of this model, each of the multiplications \constraints{} will be added to the list of attached \constraints{} of its corresponding \mzninline{y} \variable{}.
	When, after evaluating the \gls{array} access, all of those \variables{} except the last are detected to be unused, their removal triggers the removal of the subtraction \constraints{}.

	For this example the current \minizinc{} compiler, version 2.5.5, will produce a \gls{slv-mod} that contains:

	\begin{itemize}
		\item the variable \mzninline{x},
		\item \mzninline{n-1} variables \mzninline{y},
		\item \mzninline{n-1} multiplication \constraints{}.
	\end{itemize}
	
	\noindent{}This is despite the fact that the \domain{} of the \variable{} \mzninline{x} has already been \gls{fixed} to 10\@.
	The \nanozinc{} system can correctly detect that the \mzninline{y} \variables{} and multiplication \constraints{} are not required.
\end{example}

\paragraph{Implementation} The removal of unused identifiers is taken care of by garbage collection in the interpreter.
Since our prototype interpreter uses reference counting, it already accurately tracks the liveness of each identifier.

\subsection{Constraint Propagation}

\Gls{propagation} is the main inference technique used in \gls{cp} \solvers{}, as discussed in \cref{subsec:back-cp}.
At its core, \gls{propagation} simplifies the internal representation of the \gls{slv-mod}: it removes inconsistent values from \variable{} \domains{}, and it may be able to detect that certain \constraints{} are subsumed, which means that they can be removed safely.
Since a \nanozinc{} program is in fact quite similar to the internal representation of \gls{cp} \solver{}, we can use \gls{propagation} to simplify \nanozinc{}.

When using \gls{propagation} for \nanozinc{} simplification, we have to carefully consider its effects.
For instance, given the \constraint{} \mzninline{x > y}, with initial \domains{} \mzninline{x in 1..10, y in 1..10}, \gls{propagation} would result in the \domains{} being tightened to \mzninline{x in 2..10, y in 1..9}.
Note, however, that this may now prevent us from removing \mzninline{x} or \mzninline{y}: even if they later become unused, the tightened \domains{} may impose a \constraint{} on their \variables{}.
When the \domain{} of a \variable{} is tighter than the \gls{bounds} given by its defining expression, the \domain{} are said to be \gls{binding}.
For instance, if \mzninline{x} is defined as \mzninline{abs(z)}, then any restriction on the \domain{} of \mzninline{x} constrains the possible values of \mzninline{z} through the \mzninline{abs} function.
We therefore need to track whether the \domain{} of a \variable{} is the result of external \constraints{}, or is the consequence of its own definition.

A further effect of \gls{propagation} is the replacement of \constraints{} by simpler versions.
A \constraint{} \mzninline{x=y+z}, where the \domain{} of \mzninline{z} has been tightened to the singleton \mzninline{0..0}, can be rewritten to \mzninline{x=y}.
Propagating the effect of one \constraint{} can thus trigger the propagation of other \constraints{}, and \constraint{} solvers typically run all \glspl{propagator} until they reach a \gls{fixpoint}.

The \nanozinc{} \gls{interpreter} applies \glspl{propagator} for the most important \constraints{}, such as linear and Boolean \constraints{}, which can lead to significant reductions in the size of the generated \gls{slv-mod}.
It has been shown previously that applying full \gls{propagation} during compilation can be beneficial \autocite{leo-2015-multipass}.
This works particularly well when the target solver requires complicated reformulations, such as linearization for \gls{mip} \solvers{} \autocite{belov-2016-linearization}.

Returning to the example above, \gls{propagation} (and other model simplifications) can result in equality \constraints{} \mzninline{x=y} being introduced.
For certain types of target \solvers{}, in particular those based on \gls{cp}, equality \constraints{} can lead to exponentially larger search trees if not detected and simplified.
Equalities therefore present a valuable opportunity for model simplification, but also pose some challenges.

Consider the simple case of \mzninline{x=y} where one of the \variables{}, say \mzninline{x}, was a top-level variable introduced by the modeller, and not defined as the result of a function call.
In that case, we can propagate the equality \constraint{} by replacing all occurrences of \mzninline{x} with \mzninline{y}, and remove the definition of \mzninline{x}.

The more complicated case for \mzninline{x=y} is when both \mzninline{x} and \mzninline{y} are the result of function calls.
For example, a \constraint{} such as \mzninline{constraint f(a)=g(b)}.
Assuming functions \mzninline{f} and \mzninline{g} are directly rewritten into relational forms \mzninline{f_rel} and \mzninline{g_rel}, the corresponding \nanozinc{} code looks as follows.

\begin{nzn}
	var int: x;
	↳ constraint f_rel(a, x);
	var int: y;
	↳ constraint g_rel(b, y);
	constraint int_eq(x, y);
\end{nzn}

In this case, simply removing either \mzninline{x} or \mzninline{y} would not be correct.
This would trigger the removal of the corresponding definition \mzninline{f_rel(a, x)} or \mzninline{g_rel(b, y)}, leaving nothing to be substituted.
Rather, the \interpreter{} needs to pick one of the two definitions and promote it to top-level status.
Let us assume that the \interpreter{} decides to replace \mzninline{y} by \mzninline{x}.
\mzninline{y} is then globally replaced by \mzninline{x}, and its declaration is removed.
The \interpreter{} moves all attached \constraints{} from \mzninline{y} into the list of top-level \constraints{}, and then removes the \mzninline{int_eq} \constraint{}.
The following \nanozinc{} program would be its result.

\begin{nzn}
	var int: x;
	↳ constraint f_rel(a, x);
	constraint g_rel(b, x);
\end{nzn}

The process of equality propagation is similar to unification in logic programming \autocite{warren-1983-wam}.
However, since equations in \minizinc{} always concern scalar variables rather than terms, we can restrict ourselves to this simple substitution scheme and leave the further checking of the resulting equalities to the target \solver{}.

\paragraph{Implementation}

\Gls{rewriting} a function call that has a \microzinc{} definition and \gls{rewriting} a \constraint{} due to \gls{propagation} are very similar.
The \interpreter{} therefore simply interleaves both forms of \gls{rewriting}.
Efficient \gls{propagation} engines ``wake up'' a \gls{propagator} only when one of its \variables{} has received an update (i.e., when its \domain{} has been shrunk).
To enable this, the \interpreter{} needs to keep a data structure linking \variables{} to the \constraints{} where they appear (in addition to the reverse links from calls to the \variables{} in their arguments).
These links do not take part in the reference counting.

Together with its current \domain{}, each \variable{} in the interpreter also contains a Boolean flag.
This flag signifies whether the \domain{} of the \variable{} is \gls{binding}.
It is set when the \domain{} of a \variable{} is tightened by a \constraint{} that is not attached to the \variable{}.
When the flag is set, the \variable{} cannot be removed, even when the reference count is zero.
This \constraint{} may then become subsumed after \gls{propagation} and can then be removed.
Its meaning is now completely captured by the \domains{} of the \variables{}.
However, if any defining \constraint{} can later determine the same, or a strictly tighter, \domain{}, then it is not \gls{binding} any longer.
It is again fully implied by its defining \constraints{}.
The flag can then be unset and the \variable{} can potentially be removed.

\subsection{Delayed Rewriting}

\Gls{propagation} can tighten \domains{} of \variables{} or even fix them to a single value.
When this happens for the arguments of a call, a more specific \gls{decomp} may become available.
As discussed in \cref{subsec:back-delayed-rew}, it is therefore important to evaluate calls when all possible information is available to create efficient \glspl{slv-mod}.

In our \microzinc{}/\nanozinc{} system, we allow functions to be annotated as potential candidates for \gls{del-rew}.
Any annotated \constraint{} is handled by the (CallNative) rule rather than the (Call) rule, which means that it is simply added as a call into the \nanozinc{} code, without evaluating its body.
When \gls{propagation} reaches a \gls{fixpoint}, all annotations are removed from the current \nanozinc{} program, and evaluation resumes with the function bodies.

This crucial optimization enables rewriting in multiple phases.
For example, a \cmodel{} targeted at a \gls{mip} \solver{} is rewritten into Boolean and reified \constraints{}, whose definitions are annotated to be delayed.
The \nanozinc{} program can then be fully simplified by \gls{propagation}, before the Boolean and reified \constraints{} are rewritten into \gls{native} linear \constraints{} suitable for \gls{mip}.

\subsection{Common Sub-expression Elimination}%
\label{sec:rew-cse}

As shown in \cref{subsec:back-cse}, \gls{cse} is a crucial technique to avoid duplications in a \gls{model}.
In our architecture \gls{cse} is performed on two levels.

The \microzinc{} \interpreter{} performs \gls{cse} through memoization.
It maintains a table that maps a function identifier and the call arguments to its result for each call instruction that is executed.
Before it executes a call instruction, it searches the table for an entry with identical function identifier and call arguments.
Since functions in \microzinc{} are guaranteed to be pure and total, whenever the table search succeeds, the result can be used instead of executing the call instruction.

Earlier in the process, however, the \minizinc{} to \microzinc{} \compiler{} can perform \gls{cse} as it is performed in many other programming languages.

\begin{example}
	For instance, let us reconsider the following \minizinc{} fragment from \cref{ex:back-cse}.

	\begin{mzn}
		(abs(x)*2 >= 20) \/ (abs(x)+5 >= 15)
	\end{mzn}

	In this case a static \gls{compiler} analysis could detect that the same syntactical expression, \mzninline{abs(x)}, occurs twice.
	Since these expressions are guaranteed to have equivalent results, this analysis could then hoist the shared expression into a \gls{let}.

	\begin{mzn}
		constraint let { var int: y = abs(x) } in
			(y*2 >= 20) \/ (y+5 >= 15)
	\end{mzn}

\end{example}

As such, the \compiler{} can enforce sharing of common sub-expressions before evaluation begins.
It is worth noting that, although the \gls{cse} approach based on memoization would also cover the static example above, this method can potentially avoid many dynamic table look-ups.
Since the static analysis is cheap, it is valuable to combine both approaches.
The static approach can be further improved by inlining function calls, since that may expose more calls as being syntactically equal.

\paragraph{Implementation} In the implementation of our \microzinc{} \interpreter{}, \gls{cse} directly interacts with the reference counting mechanism.
It is clear that when an expression is reused by returning it from the \gls{cse} table, this creates a new reference to that expression.
However, the entries in the \gls{cse} table should not keep the corresponding variables alive.
Otherwise, none of the \variables{} would ever become unused.
Therefore, we treat \gls{cse} entries as weak references.
They reference a \variable{}, but do not affect its liveness (i.e., increase its reference count).
If an entry is found in the \gls{cse} table with a reference count of zero, it is removed from the table and its contents are not used.

The usage of a \gls{cse} table can be costly.
The memory requirement and time spent finding entries can be significant in the overall process.
This is aggravated by the fact that \minizinc{} has many places where a function's body only contains a single call to a function that is not used anywhere else.
Although this structure offers flexibility when defining \minizinc{} libraries, it results in many \gls{cse} entries that differ only by their function identifier.

\begin{example}
	For example, the definition of the \mzninline{knapsack} \gls{global} in the \minizinc{} standard library is shown in \cref{lst:rew-knapsack}.
	After checking the \parameter{} arguments, the function merely returns the result of \mzninline{fzn_knapsack}.
	This function is implemented in the \solver{} library to provide the implementation of the \mzninline{knapsack} \gls{global}.
	The extra function layer ensures that these checks can be performed independently of the \solver{} library and that the \solver{} can make certain assumptions about the function arguments.
	But because the modeller will only use \mzninline{knapsack}, it does not make sense to also create \gls{cse} entries for \mzninline{fzn_knapsack}, as it will never be used.
\end{example}
\begin{listing}
	\mznfile{assets/listing/rew_knapsack.mzn}
	\caption{\label{lst:rew-knapsack} The definition of \mzninline{knapsack} in the \minizinc{} standard library.}
\end{listing}

Therefore, we have added a flag to our call instruction.
This flag controls whether the call is subject to \gls{cse}.
This allows us to disable the \gls{cse} when it is guaranteed to be unnecessary.

\subsection{Constraint Aggregation}%
\label{subsec:rew-aggregation}

In our new system it is still possible to support \gls{aggregation}.
We aggregate \constraints{} by combining \constraints{} connected through attached \constraints{}, eliminating the need for \gls{avar} to which they are attached.
To aggregate a certain kind of \constraint{}, it is marked as a \gls{native} \constraint{}.
These functional definitions are kept in the \nanozinc{} program until a top-level \constraint{} is posted that uses the \variables{} to which they are attached.
Once this happens, the interpreter will employ dedicated \gls{aggregation} logic to visit the attached \constraints{} and combine them.
The top-level \gls{constraint} is then replaced by the combined \gls{constraint}.
When the \gls{avar} become unused, they will be removed using the normal mechanisms.

\begin{example} For example, let us reconsider the linear \constraint{} from \cref{ex:back-agg}: \mzninline{x + 2*y <= z}.
	The constraint will result in the following \nanozinc{}.

	\begin{nzn}
		var int: x;
		var int: y;
		var int: z;
		var int: i1;
		↳ constraint '*'(y, 2, i1);
		var int: i2;
		↳ constraint '+'(x, i1, i2);
		constraint '<='(i2, z);
	\end{nzn}

	\mzninline{*} and \mzninline{+} were marked as \gls{native} \constraints{} as they can be aggregated into a linear \constraint{}.
	Their functional definitions are put in place in the \nanozinc{}, and then a top-level \mzninline{<=} \constraint{} is created.
	The \interpreter{} will then recursively visit the arguments of the \constraints{}.
	The \constraints{} are then combined into the following linear \constraint{}.

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

\section{Experiments}\label{sec:rew-experiments}

We have created a prototype implementation of the architecture presented in the preceding sections.
It consists of a \compiler{} from \minizinc{} to \microzinc{}, and a \microzinc{} \interpreter{} producing \nanozinc{}.
The system supports a significant subset of the full \minizinc{} language; notable features that are missing are support for set and float variables, option types, and compilation of model output expressions and annotations.
We will release our implementation under an open-source licence and can make it available to the reviewers upon request.
\todo{I suppose it is time to release the prototype.}

The implementation is not optimized for performance yet, but was created as a faithful implementation of the developed concepts, in order to evaluate their suitability and provide a solid baseline for future improvements.
In the following we present experimental results on basic \gls{rewriting} performance as well as a comparison with \glspl{interpreter} of other programming languages to demonstrate the efficiency gains that are possible thanks to the new architecture.
A description of the used computational environment, \minizinc{} instances, and versioned software has been included in \cref{ch:benchmarks}.

For our first experiment, we selected 17 models from the annual \minizinc{} challenge and compiled 5 instances of each model to \flatzinc{}, using the current \minizinc{} release version 2.5.5 and the new prototype system.
In both cases we use the standard \minizinc{} library of \glspl{global} (i.e., we decompose those \constraints{} rather than using \solver{} \gls{native} \constraints{}, in order to stress-test the \gls{rewriting}).
We measured pure \gls{rewriting} time, i.e., without time required to parse and type check in version 2.5.5, and without time required for compilation to \microzinc{} in the new system (compilation is usually very fast).
Times are averages of 10 runs.

\Cref{sfig:rew-compareruntime} compares the \gls{rewriting} time for each of \instances{}.
Points below the line indicate that the new system is faster.
On average, the new system achieves a speed-up of 5.5, with every \instance{} achieving at least 2.5 speed-up and multiple \instances{} with a speed-up of over 100.
In terms of memory performance (\cref{sfig:rew-comparemem}), version 2.5.5 can sometimes still outperform the new prototype.
We have identified that the main memory bottlenecks are our currently unoptimized implementations of \gls{cse} lookup tables and argument vectors.
These are very encouraging results, given that we are comparing a largely unoptimized prototype to a mature piece of software.

\begin{figure}
	\centering
	\begin{subfigure}[b]{.48\columnwidth}
		\centering
		\includegraphics[width=\columnwidth]{assets/img/rew_compare_runtime}
		\caption{\label{sfig:rew-compareruntime}Average run time (ms)}
	\end{subfigure}%
	\hspace{0.04\columnwidth}%
	\begin{subfigure}[b]{.48\columnwidth}
		\centering
		\includegraphics[width=\columnwidth]{assets/img/rew_compare_memory}
		\caption{\label{sfig:rew-comparemem}Maximum resident set size (kbytes)}
	\end{subfigure}
	\caption{\label{fig:4-runtime}Performance on \gls{rewriting} \minizinc{} Challenge \instances{}. \minizinc{} 2.5.5 (x-axis) vs our prototype (y-axis), log-log plot. Dots below the line indicate the new system is better.}
\end{figure}

Our second experiment considers three well-known computational recursive functions: Ackermann, Fibonacci, and Takeuchi.
These functions are often used as a benchmark for implementations of functional programming languages.
Since the \minizinc{} language includes a strong functional programming component, we use these same functions as a benchmark for our prototype \interpreter{}.
In addition to \minizinc{} 2.5.5, we also compare our \interpreter{} to Python 3.8.5 \autocite{rossum-2009-python3} and OCaml 4.10.0 \autocite{leroy-2020-ocaml}.
The chosen function arguments try to exercise the \glspl{interpreter}, but without running into their limitations. 
Times are averages of 1000 runs.

The results of the experiment are shown in \cref{fig:rew-interpreter-comp}.
For all experiments there is a clear ordering in the results: 
\begin{itemize}
	\item OCaml is the clear winner,
	\item our prototype finishes in second place,
	\item Python is a close third,
	\item and finally \minizinc{} 2.5.5.
\end{itemize}
Our prototype performs well in this test.
It clearly outperforms \minizinc{} 2.5.5 with about 10 times speed-up, and it slightly outperforms Python, an optimized \interpreter{} for a general programming language.
It is clear though that OCaml, a language that is dedicated to these types of programs, still outperforms our prototype.
We are convinced, however, that we can get closer to its performance given the right improvements in our prototype.

\begin{figure}
	\centering
	\includegraphics[width=\columnwidth]{assets/img/rew_interpreter_plot}
	\caption{\label{fig:rew-interpreter-comp} Run-time comparison of interpreters
		on recursive functions: Takeuchi, Fibonacci, and Ackermann.}
\end{figure}

% \section{Summary}%
% \label{sec:rew-summary}

% In this chapter, we introduced a systematic view of the execution of \minizinc{}, revisiting the rewriting from high-level \minizinc{} to solver-level \flatzinc{}.
% We first introduced the intermediate languages \microzinc{} and \nanozinc{} and explained how \minizinc{} can be transformed into a set of \microzinc{} definitions and a \nanozinc{} program.
% We then, crucially, discussed how to partially evaluate a \nanozinc{} program using \microzinc{} definitions and present formal definitions of the rewriting rules applied during partial evaluation.

% Continuously applying these rules would result in a correct solver-level model, but it is unlikely to be the best model for the solver.
% We, therefore, discuss multiple techniques to improve the \gls{slv-mod} during the partial evaluation of \nanozinc{}.
% First, we introduce a novel technique to eliminate all unused variables and \constraints{}: we track all \constraints{} that are introduced only to define a variable.
% This means we can keep an accurate count of when a variable becomes unused by counting only the references to a variable in \constraints{} that do not help define it.
% Then, we discuss the use of \gls{propagation} during the partial evaluation of the \nanozinc{} program.
% This technique can help shrink the domains of the decision variable or even combine variables known to be equal.
% When a redefinition of a \constraint{} requires the introspection into the current domain of a variable, it is often important to have the tightest possible domain.
% Hence, we discuss how in choosing the next \nanozinc{} \constraint{} to rewrite, the interpreter can sometimes delay the rewriting of certain \constraints{} to ensure the most amount of information is available.
% \Gls{cse}, our next optimisation technique, ensures that we do not create or evaluate the same \constraint{} or function twice and reuse variables where possible.
% Finally, the last optimisation technique we discuss is the use of \gls{aggregation}.
% The use of \gls{aggregation} ensures that individual functional \constraints{} can be collected and combined into an aggregated form.
% This allows us to avoid the existence of intermediate variables in some cases.
% This optimisation is very important for \gls{mip} solvers.

% Finally, we test the described system using an experimental implementation.
% We compare this experimental implementation against the current \minizinc{} interpreter, version 2.5.3, and look at both runtime and its memory usage.
% Although the experimental implementation there are instances where the experimental implementation uses more memory than the current \minizinc{} interpreter, it clearly outperforms the current \minizinc{} interpreter in terms of time.
