dekker.one
Jip Dekker's PhD Thesis
1%************************************************
2\chapter{Rewriting Constraint Modelling Languages}\label{ch:rewriting}
3%************************************************
4
5\input{chapters/3_rewriting_preamble}
6
7
8\section{Architecture Overview}
9\label{sec:rew-arch}
10
11\noindent{}\Gls{rewriting} a \minizinc{} instance into a \gls{slv-mod} may often seem like a simple \gls{trs}.
12In reality, however, \minizinc{} is quite a complex language, and producing a good \gls{slv-mod} is far from trivial.
13
14Thus, in practice, this rewriting process is a highly complex task that needs to carefully track interactions between \constraints{} and how they affect \variables{}.
15To create an efficient \gls{slv-mod} the \gls{rewriting} process uses many simplification techniques such as:
16
17\begin{itemize}
18 \item continuously updating \variable{} \domains{},
19 \item \gls{propagation} for known \constraints{},
20 \item specialized \glspl{decomp} when variables get \gls{fixed},
21 \item \gls{aggregation},
22 \item common sub-expression elimination,
23 \item and removing \variables{} and \constraints{} that are not required any longer.
24\end{itemize}
25
26We now present a new architecture for the \gls{rewriting} process that has been designed for the modern day needs of \minizinc{}.
27At the core of our \gls{rewriting} process lie formalized rewriting rules.
28As such, this architecture represents an abstract machine model for \minizinc{}.
29These rules allow us to reason about the system and about the simplifications both to the process and the resulting \gls{slv-mod}.
30The 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.
31
32\begin{figure}
33 \centering
34 \includegraphics[width=\linewidth]{assets/img/rew_compilation_structure}
35 \caption{\label{fig:rew-comp} The proposed process for the compilation of \minizinc{} instances.}
36\end{figure}
37
38The process of the new architecture is shown in \cref{fig:rew-comp}.
39After parsing and type checking, a \minizinc{} model is first compiled into a smaller constraint language called \microzinc{}, independent of the data.
40For efficient execution, the \microzinc{} is then transformed into a \gls{byte-code}.
41Together, the \gls{byte-code} and a complete \gls{parameter-assignment} form an \instance{} that can be executed by the \microzinc{} \interpreter{}.
42During its execution, the \interpreter{} continuously updates a \cmodel{} according to the \microzinc{} definition.
43The \cmodel{} in the \interpreter{} is internally represented as a \nanozinc{} program.
44\nanozinc{} is a slight extension of the \flatzinc{} format.
45The \interpreter{} finishes when it reaches a \gls{slv-mod}.
46
47We have developed a prototype of this toolchain, and present experimental validation that the new tool chain can perform \gls{rewriting} much faster, and produce better models, than the current \minizinc{} \compiler{}.
48
49\section{\glsentrytext{microzinc} and \glsentrytext{nanozinc}}\label{sec:rew-micronano}
50
51This section introduces the two sub-languages of \minizinc{} at the core of the new architecture we have developed.
52
53\microzinc{} is a simple language used to define transformations to be performed by the \interpreter{}.
54It is a simplified subset of \minizinc{}.
55The transformation are represented in the language through the use of function definitions.
56A function of type \mzninline{var bool}, describing a relation, can be defined as a \gls{native} \constraint{}.
57Otherwise, a function body must be provided for \gls{rewriting}.
58The function body can use a restriction of the \minizinc{} expression language.
59
60An important difference between \minizinc{} and \microzinc{} is that a well-formed \microzinc{} does not contain partial expressions.
61Any partiality in the \minizinc{} model must be explicitly expressed using total functions in \microzinc{}.
62As such, \constraints{} introduced in \microzinc{} \glspl{let} can be globally enforced.
63They are guaranteed to only constrain the \variables{} introduced in the same \gls{let}.
64
65\nanozinc{} is used to represent the current state of the \instance{}.
66\nanozinc{} is similar to \flatzinc{} in that it contains only declarations of \variables{} and a flat list of \constraints{}.
67However, while all function calls in \flatzinc{} need to be \gls{native}, \nanozinc{} calls can refer to any function implemented in \microzinc{}.
68Furthermore, \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.
69As a small syntactic difference with \flatzinc{}, \constraints{} and \variable{} declarations in \nanozinc{} can be freely interleaved.
70
71The core of the syntax of \microzinc{} is defined in \cref{fig:rew-uzn-syntax}.
72Function declarations without an expression body are used to mark functions that are \gls{native} to the target \solver{}.
73We 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}.
74While we omit the typing rules here for space reasons, we will assume that in well-typed \microzinc{} programs conditions of expressions are \parameters{}.
75This 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.
76In \minizinc{} the use of \variables{} in these positions is allowed, and these expressions are rewritten to function calls.
77We will discuss how the same transformation takes place when translating \minizinc{} to \microzinc{}.
78
79\begin{figure}
80 \begin{grammar}
81 <model> ::= <pred-decl>*<fun-decl>*
82
83 <fun-decl> ::= "function" <type-inst>":" <ident>"(" <typing> ["," <typing>]* ")" "=" <exp>";"
84 \alt "function" "var" "bool" ":" <ident>"(" <typing> ["," <typing>]* ")"";"
85
86 <literal> ::= <constant> | <ident>
87
88 <exp> ::= <literal>
89 \alt <ident>"(" <exp> ["," <exp>]* ")"
90 \alt "let" "{" <item>* "}" "in" <literal>
91 \alt "if" <exp> "then" <exp> "else" <exp> "endif"
92 \alt "[" <exp> "|" <gen-exp> "where" <exp> "]"
93 \alt <ident>"[" <literal> "]"
94
95 <item> ::= <typing> [ "=" <exp> ]";"
96 \alt "tuple(" <type-inst> ["," <type-inst>]* "):" <ident> = "(" <exp> ["," <exp>]* ")"";"
97 \alt "(" <typing> ["," <typing>]* ")" "=" <exp>";"
98 \alt "constraint" <exp>";"
99
100 <typing> ::= <type-inst>":" <ident>
101
102 <gen-exp> ::= <ident> "in" <exp> ["," <ident> "in" <exp> ]*
103 \end{grammar}
104 \caption{\label{fig:rew-uzn-syntax}Syntax of \microzinc{}.}
105\end{figure}
106
107A \nanozinc{} program, defined in \cref{fig:rew-nzn-syntax}, is simply a list of \variable{} declarations and \constraints{} in the form of calls.
108The syntax ``\texttt{↳}'' will be used to ``attach'' \constraints{} to \variables{} in order to track dependent \constraints{}.
109This will be explained in detail in \cref{sec:rew-nanozinc}.
110
111\begin{figure}
112 \begin{grammar}
113 <nzn> ::= <nzn-item>*
114
115 <nzn-item> ::= <nzn-def> | <nzn-con>
116
117 <nzn-con> ::= "constraint" <ident>"(" <literal> ["," <literal>]* ")"";"
118
119 <nzn-var> ::= "var" <nzn-dom> ":" <ident> ";" <nzn-attach>*
120
121 <nzn-dom> ::= <constant> ".." <constant> | <constant>
122 \alt "bool" | "int" | "float" | "set of int"
123
124 <nzn-attach> ::= "↳" <nzn-con>
125 \end{grammar}
126 \caption{\label{fig:rew-nzn-syntax}Syntax of \nanozinc{}.}
127\end{figure}
128
129\subsection{\glsentrytext{minizinc} to \glsentrytext{microzinc}}
130
131The translation from \minizinc{} to \microzinc{} involves the following steps.
132
133\begin{enumerate}
134
135 \item Transform all expressions that are valid in \minizinc{} but not in \microzinc{}.
136 This includes simple cases such as replacing \gls{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])}.
137 As mentioned above, \gls{conditional} expressions where the decision is made by a \variable{} are also not directly supported in \microzinc{}.
138 These expressions are therefore also replaced by function calls that are possibly decomposed.
139 An expression \mzninline{if x then A else B endif}, where \mzninline{x} is a \variable{}, is replaced the call \mzninline{if_then_else([x, true], [A, B])}.
140 A recent study by \textcite{stuckey-2019-conditionals} describes how \mzninline{if_then_else} can be decomposed for different types of \solvers{}.
141 An expression \mzninline{A[x]}, where \mzninline{x} is a \variable{}, is replaced by the call \mzninline{element(A, x)}.
142 \mzninline{element} is a well-known \gls{global}.
143 For many \gls{cp} \solvers{} it is a \gls{native} \constraint{} and for other \solvers{} there have long been accepted \glspl{decomp}.
144
145 \item Replace optional \variables{} into non-optional forms.
146 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{}.
147 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.
148 In \microzinc{} this can be represented as a tuple of the two \variables{}.
149 The function definitions for optional types then take both \variables{} into account.
150 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}.
151
152 \begin{listing}
153 \mznfile{assets/listing/rew_opt_plus.mzn}
154 \caption{\label{lst:rew-opt-plus} A definition of \mzninline{int_plus} for optional integers in \microzinc{} syntax.}
155 \end{listing}
156
157 \item Lift the partiality in expressions into the surrounding context to implement \minizinc{}'s relational semantics.
158 In contrast to \minizinc{}, a \microzinc{} expression must be total.
159 \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{}.
160 A general approach for describing the partiality in \microzinc{} functions is to make the function return an additional Boolean \variable{}.
161 This \variable{} indicates whether the result of the function call is defined w.r.t. the function arguments.
162 The resulting value of the function is then adjusted to return a predefined value when it would normally be undefined.
163 For example, the \mzninline{element} function in \minizinc{} is declared as follows.
164
165 \begin{mzn}
166 function var int: element(array of int: a, var int: x);
167 \end{mzn}
168
169 \noindent{}It is only defined when \mzninline{x in index_set(a)}.
170 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.}.
171
172 \begin{listing}
173 \mznfile{assets/listing/rew_elem_safe.mzn}
174 \caption{\label{lst:rew-elem-safe} A total of the \mzninline{element} function in \microzinc{}.}
175 \end{listing}
176
177 Similar to the replacement of optional values, all occurrences of the \mzninline{element} function are replaced by \mzninline{element_safe}.
178 The usage of its result should be guarded by the returned totality variable in the surrounding Boolean context.
179 This means that, for example, the expression \mzninline{element(e, v) = 5 \/ b} would be replaced by the following expression.
180
181 \begin{mzn}
182 let {
183 (var int: res, var bool: total) = element_safe(e, v);
184 } in (total /\ res = 5) \/ b;
185 \end{mzn}
186
187 \item Resolve subtype based overloading statically.
188 To prevent the runtime overhead of the dynamic lookup of overloaded function definitions for every call, the function dispatch in \microzinc{} is determined statically.
189
190 It is important, however, that the correct version of a function is chosen when it allows for either \variable{} and \parameter{} arguments.
191 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.
192 At that point it can be treated as a \parameter{}.
193 To ensure the correct version of the function is used, functions are changed to, at runtime, check if a \variable{} is \gls{fixed} and, if so, dispatch to the \parameter{} version of the function.
194 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.
195
196 \begin{mzn}
197 function f_int(int: x) = /* original body */;
198 function f_varint(var int: x) =
199 if is_fixed(x) then
200 f_int(fix(x))
201 else
202 /* original body */;
203 endif;
204 \end{mzn}
205
206 \item Transform all function definitions so that they do not refer to \variables{} and \parameters{} defined outside the scope of the function.
207 Instead, they are added as extra arguments to the function definition and each call.
208
209 \item Move all top-level \variable{} declarations and \constraints{} into a let expression in the body of a new function called \mzninline{main}.
210 The arguments to this function are the top-level \parameters{} of the \minizinc{} model, and it returns a fresh Boolean \variable{}.
211
212\end{enumerate}
213
214\begin{example}
215
216 Consider the \minizinc{} model in \cref{lst:rew-pigeon-mzn}.
217 It describes a simple \gls{unsat} ``pigeonhole problem'': trying to assign \(n\) pigeons to \(n-1\) holes.
218
219 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.
220 The result of this translation is shown in \cref{lst:rew-pigeon-uzn}.
221
222 \pagebreak{}
223 For an \instance{} of the \cmodel{}, we can then create a simple \nanozinc{} program that calls \mzninline{main}.
224 For example for \(n=10\), we would create the following \nanozinc{} program.
225
226 \begin{nzn}
227 constraint main(10);
228 \end{nzn}
229 \codeendsexample{}
230\end{example}
231
232\begin{listing}
233 \mznfile{assets/listing/rew_pigeon_mzn.mzn}
234 \caption{\label{lst:rew-pigeon-mzn} A \minizinc{} model of the pigeonhole problem.}
235\end{listing}
236
237
238\begin{listing}
239 \mznfile{assets/listing/rew_pigeon_uzn.mzn}
240 \caption{\label{lst:rew-pigeon-uzn} The \microzinc{} translation of the pigeonhole problem in \cref{lst:rew-pigeon-mzn}.}
241\end{listing}
242
243\subsection{Partial Evaluation of \glsentrytext{nanozinc}}\label{sub:rew-partial}
244
245Each call in a \nanozinc{} program is either a call to a \gls{native} \constraint{}, or it has a corresponding \microzinc{} function definition.
246The 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{}.
247
248To achieve this, we define the semantics of \microzinc{} as a \gls{rewriting} system that produces \nanozinc{} calls.
249Each non-\gls{native} call in a \nanozinc{} program can then be replaced with the result of evaluating the corresponding \microzinc{} function.
250
251A key element of this \gls{rewriting} process, then, is the transformation of functional expressions into relational form.
252For this to happen, the \gls{rewriting} process introduces fresh \variables{} to represent intermediate expressions.
253
254\begin{example}\label{ex:rew-abs}
255 Consider the (reasonably typical) \minizinc{} encoding for the absolute value function presented in \cref{lst:rew-abs}.
256 When an occurrence of \mzninline{abs} is encountered, the call will be replaced by a \variable{} \mzninline{z}.
257 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.
258\end{example}
259\begin{listing}
260 \mznfile{assets/listing/rew_abs.mzn}
261 \caption{\label{lst:rew-abs} A \minizinc{} definition for the absolute value function.}
262\end{listing}
263
264The 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}.
265In 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}.
266However, the introduced \mzninline{int_abs} \constraint{} is only needed so long as any other \constraint{} refers to \mzninline{z}.
267If \mzninline{z} is unused in the rest of the model, both \mzninline{z} and the \mzninline{int_abs} \constraint{} can be removed.
268
269As we shall see in \cref{sec:rew-simplification}, certain optimizations and simplifications during the evaluation can lead to many expressions becoming unused.
270It is therefore important to track which \constraints{} were merely introduced to define results of function calls.
271In order to track these dependencies, \nanozinc{} attaches \constraints{} that define a variable to the item that introduces the \variable{}.
272
273\subsection{\glsentrytext{nanozinc}}\label{sec:rew-nanozinc}
274
275A \nanozinc{} program (\cref{fig:rew-nzn-syntax}) consists of a topologically-ordered list of declarations of \variables{} and \constraints{}.
276\Variables{} are declared with an identifier, a domain, and are associated with a list of attached \constraints{}.
277\Constraints{} can also occur at the top-level of the \nanozinc{} program.
278These 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}.
279Only root-context \constraints{} can effectively constrain the overall problem.
280In \microzinc{} these \constraints{} must originate from \constraint{} items in the generated \mzninline{main} function.
281\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.
282
283\begin{example}\label{ex:rew-absnzn}
284
285 Consider the following \minizinc{} fragment.
286
287 \begin{mzn}
288 constraint abs(x) > y;
289 \end{mzn}
290
291 \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.
292
293 \begin{nzn}
294 var -10..10: x;
295 var -10..10: y;
296 var int: z;
297 ↳ constraint int_abs(x, z);
298 constraint int_gt(z, y);
299 \end{nzn}
300
301 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}.
302 The top-level \constraint{} \mzninline{abs(x) > y} is rewritten into \mzninline{int_gt(z, y)} and added as a top-level \constraint{}.
303\end{example}
304
305\subsection{Rewriting Rules}
306
307The core of the proposed \minizinc{} architecture is an abstract machine that rewrites \nanozinc{} items using the corresponding \microzinc{} function definitions.
308We can now formally define the rewriting rules for this abstract machine.
309
310The 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}.
311To 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.
312We also present our rules using a \emph{call by name} evaluation strategy, i.e., the arguments to function calls are substituted into function body.
313As such, they are only evaluated when required for the result of the function.
314Although pure \microzinc{} behaves the same under any call evaluation strategy, in implementation a \emph{call by value} strategy can provide more predictable behaviour with debugging functions in the \minizinc{} language.
315It would likely be unexpected that functions such as \mzninline{trace} and \mzninline{assert} are only evaluated if and when their values are required (call by name), instead of when the function call is encountered.
316
317\begin{figure*}[p]
318 \centering
319 \begin{prooftree}
320 \hypo{\texttt{function} ~t\texttt{:}~\ptinline{F(\(p_1, \ldots{}, p_k\)) = E;} \in{} \Prog{} \text{~where the~} p_i \text{~are fresh}}
321 \infer[no rule]1{\Sem{\(\ptinline{E}_{[p_i \mapsto a_i, \forall{} 1 \leq{} i \leq{} k]}\)}{\Prog, \Env} \Rightarrow{} \tuple{v, \Env'}}
322 \infer1[(Call)]{\Sem{F(\(a_1, \ldots, a_k\))}{\Prog, \Env} \Rightarrow{} \tuple{v, \Env'}}
323 \end{prooftree} \\
324 \bigskip
325 \begin{prooftree}
326 \hypo{\ptinline{F} \in \text{Builtins}}
327 \infer1[(CallBuiltin)]{\Sem{F(\(a_1, \ldots, a_k\))}{\Prog, \Env} \Rightarrow{} \tuple{\ensuremath{\mathit{eval}(\ptinline{F}(a_1,\ldots, a_k))}, \Env}}
328 \end{prooftree} \\
329 \bigskip
330 \begin{prooftree}
331 \hypo{\texttt{function var bool:}~\ptinline{F(\(p_1, \ldots, p_k\));} \in \Prog}
332 \infer1[(CallNative)]{\Sem{F(\(a_1, \ldots, a_k\))}{\Prog, \Env} \Rightarrow{}
333 \tuple{\ensuremath{\texttt{constraint}~\ptinline{F}(a_1, \ldots, a_k), \Env}}}
334 \end{prooftree}
335 \caption{\label{fig:rew-rewrite-to-nzn-calls} Rewriting rules for partial evaluation of \microzinc{} calls to \nanozinc{}.}
336\end{figure*}
337
338The rules in \cref{fig:rew-rewrite-to-nzn-calls} handle function calls.
339The first rule, (Call), evaluates a function call expression in the context of a \microzinc{} program \(\Prog{}\) and \nanozinc{} program \(\Env{}\).
340The 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.
341
342The (CallBuiltin) rule applies to ``built-in'' functions that can be evaluated directly, such as arithmetic and Boolean operations on \gls{fixed} values.
343The rule simply returns the result of evaluating the built-in function on the evaluated parameter values.
344
345The (CallNative) rule applies to calls to \mzninline{var bool} functions, that describe relations, that have been marked as \constraints{} \gls{native} to the \solver{}.
346Since these are directly supported by the \solver{}, they simply need to be transferred into the \nanozinc{} program.
347
348\begin{figure*}[p]
349 \centering
350 \begin{prooftree}
351 \hypo{\Sem{\(\mathbf{I} \mid{} \mathbf{X}\)}{\Prog, \Env, \emptyset} \Rightarrow \tuple{x, \Env'}}
352 \infer1[(Let)]{\Sem{let \{ \(\mathbf{I}\) \} in \(\mathbf{X}\)}{\Prog, \Env} \Rightarrow{} \tuple{x, \Env'}}
353 \end{prooftree} \\
354 \bigskip
355 \begin{prooftree}
356 \hypo{\Sem{\(\mathbf{X}\)}{\Prog, \{ t : x \} \cup{} \Env} \Rightarrow \tuple{x, \{ t: x \} \cup{} \Env'}}
357 \infer1[(Item0)]{\Sem{\(\epsilon{} \mid{} \mathbf{X}\)}{\Prog, \{ t: x \}\cup{}\Env, \Ctx} \Rightarrow{} \tuple{x, \{ t: x \texttt{~↳~} \Ctx{} \} \cup{} \Env'}}
358 \end{prooftree} \\
359 \bigskip
360 \begin{prooftree}
361 \hypo{\Sem{\(C\)}{\Prog, \Env} \Rightarrow \tuple{c, \Env'}}
362 \hypo{\Sem{\(\mathbf{I} \mid{} \mathbf{X}\)}{\Prog, \Env', \{c\}\cup\Ctx} \Rightarrow \tuple{x, \Env''}}
363 \infer2[(ItemC)]{\Sem{\(\mbox{constraint}~C\texttt{;} \mathbf{I} \mid{} \mathbf{X}\)}{\Prog, \Env, \Ctx} \Rightarrow{} \tuple{x, \Env''}}
364 \end{prooftree} \\
365 \bigskip
366 \begin{prooftree}
367 \hypo{\Sem{\(\mathbf{I} \mid{} \mathbf{X}\)}{\Prog, \Env{} \cup{} \{t : x\}, \Ctx} \Rightarrow \tuple{x, \Env'}}
368 \infer1[(ItemT)]{\Sem{\(t\texttt{:}~x\texttt{;} \mathbf{I} \mid{} \mathbf{X}\)}{\Prog, \Env, \Ctx} \Rightarrow{} \tuple{x, \Env'}}
369 \end{prooftree} \\
370 \bigskip
371 \begin{prooftree}
372 \hypo{\Sem{\(E\)}{\Prog, \Env} \Rightarrow \tuple{v, \Env'}}
373 \hypo{\Sem{\(\mathbf{I}_{[x \mapsto v]} \mid{} \mathbf{X}_{[x \mapsto v]}\)}{\Prog, \Env', \Ctx} \Rightarrow{} \tuple{x, \Env''}}
374 \infer2[(ItemTE)]{\Sem{\(t\texttt{:}~x = E\texttt{;} \mathbf{I} \mid{} \mathbf{X}\)}{\Prog, \Env, \Ctx} \Rightarrow{} \tuple{x, \Env''}}
375 \end{prooftree} \\
376 \bigskip
377 \begin{prooftree}
378 \hypo{\Sem{\(E_{i}\)}{\Prog,\Env^{i-1}} \Rightarrow \tuple{v_{i}, \Env^{i}}, \forall{} 1 \leq{} i \leq{} k}
379 \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'}}
380 \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'}}
381 \end{prooftree} \\
382 \bigskip
383 \begin{prooftree}
384 \hypo{\Sem{\(E\)}{\Prog, \Env} \Rightarrow \tuple{\left(v_{\langle{}1\rangle}, \ldots, v_{\langle{}k\rangle}\right), \Env'}}
385 \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''}}
386 \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''}}
387 \end{prooftree}
388 \caption{\label{fig:rew-rewrite-to-nzn-let} Rewriting rules for partial evaluation of \microzinc{} \glspl{let} to \nanozinc{}.}
389\end{figure*}
390
391The rules in \cref{fig:rew-rewrite-to-nzn-let} consider \glspl{let}.
392Starting from the main rule, (Let), the let items \textbf{I} are evaluated one at a time.
393\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.
394When 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).
395The (ItemT) rule handles introduction of new \variables{} by adding them to the context.
396The (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.
397The rules (ItemTupC) and (ItemTupD) are for the construction and deconstruction of tuple objects.
398We use the notation \(x_{\langle{}i\rangle}\) to mark the \(i^{\text{th}}\) member of the tuple \(x\) in our substitution notation.
399
400\begin{figure*}
401 \centering
402 \begin{prooftree}
403 \hypo{x \in \langle \text{ident} \rangle}
404 \hypo{\{t: x \texttt{~↳~} \phi{} \} \in \Env}
405 \infer2[(Ident)]{\Sem{\(x\)}{\Prog, \Env} \Rightarrow{} \tuple{x, \Env}}
406 \end{prooftree} \\
407 \bigskip
408 \begin{prooftree}
409 \hypo{c \text{~constant}}
410 \infer1[(Const)]{\Sem{\(c\)}{\Prog, \Env} \Rightarrow{} \tuple{c, \Env}}
411 \end{prooftree} \\
412 \bigskip
413 \begin{prooftree}
414 \hypo{\Sem{\(x\)}{\Prog, \Env} \Rightarrow \tuple{[x_{n}, \ldots, x_{m}], \Env'}}
415 \hypo{\Sem{\(i\)}{\Prog, \Env'} \Rightarrow \tuple{v, \Env''}}
416 \hypo{v \in [n \ldots{} m]}
417 \infer3[(Access)]{\Sem{\(x\texttt{[}i\texttt{]}\)}{\Prog, \Env} \Rightarrow{} \tuple{x_{v}, \Env''}}
418 \end{prooftree} \\
419 \bigskip
420 \begin{prooftree}
421 \hypo{\Sem{\(C\)}{\Prog, \Env} \Rightarrow \tuple{\ptinline{true}, \_}}
422 \infer1[(If\(_T\))]{\Sem{if \(C\) then \(E_t\) else \(E_e\) endif}{\Prog, \Env} \Rightarrow{} \Sem{\(E_t\)}{\Prog, \Env}}
423 \end{prooftree} \\
424 \bigskip
425 \begin{prooftree}
426 \hypo{\Sem{\(C\)}{\Prog, \Env} \Rightarrow \tuple{\ptinline{false}, \_}}
427 \infer1[(If\(_F\))]{\Sem{if \(C\) then \(E_t\) else \(E_e\) endif}{\Prog, \Env} \Rightarrow{} \Sem{\(E_e\)}{\Prog, \Env}}
428 \end{prooftree} \\
429 \bigskip
430 \begin{prooftree}
431 \hypo{\Sem{G}{\Prog,\Env} \Rightarrow \tuple{ \ptinline{true}, \_}}
432 \hypo{\Sem{\(E\)}{\Prog, \Env} \Rightarrow \tuple {v, \Env'}}
433 \infer2[(WhereT)]{\Sem{\([E ~|~ \mbox{where~} G]\)}{\Prog, \Env} \Rightarrow{} \tuple{[v], \Env'}}
434 \end{prooftree} \\
435 \bigskip
436 \begin{prooftree}
437 \hypo{\Sem{G}{\Prog,\Env} \Rightarrow \tuple{\ptinline{false}, \_}}
438 \infer1[(WhereF)]{\Sem{\([E ~|~ \mbox{where~} G]\)}{\Prog, \Env} \Rightarrow{} \tuple{[], \Env}}
439 \end{prooftree} \\
440 \bigskip
441 \begin{prooftree}
442 \hypo{\Sem{\(\mathit{PE}\)}{\Prog,\Env} \Rightarrow \tuple{S, \_}}
443 \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 }
444 \infer1[(ListG)]{\Sem{\([E~|~ x \mbox{~in~} \mathit{PE}, \mathit{GE} \mbox{~where~} G]\)}{\Prog, \Env} \Rightarrow{}
445 \tuple{\mbox{concat} [ A_v~|~v \in{} S ], \Env{} \cup{} \bigcup{}_{v \in{} S} \Env{}_{v}}}
446 \end{prooftree}
447 \caption{\label{fig:rew-rewrite-to-nzn-other} Rewriting rules for partial evaluation of other \microzinc{} expressions to \nanozinc{}.}
448\end{figure*}
449
450Finally, the rules in \cref{fig:rew-rewrite-to-nzn-other} handle the evaluation of \variables{}, constants, \glspl{conditional}, and \glspl{comprehension}.
451The (Ident) rule looks up a \variable{} in the environment and returns the \variable{} itself to be used in any \constraints{}.
452The (Const) rule simply returns the constant.
453The (Acess) rule evaluates the \gls{array} expression \(x\) and the index \(i\).
454It then returns the element from the evaluated \gls{array} chosen by the evaluated index.
455Note that, in well-defined \microzinc{}, the index \(i\) must evaluate to a value within the index range of the evaluated \gls{array} \(x\).
456The (If\(_T\)) and (If\(_F\)) rules evaluate the if condition and then return the result of the then or else branch appropriately.
457The (WhereT) rule evaluates the guard of a where \gls{comprehension} and if \true{} returns the resulting expression in a list.
458The (WhereF) rule evaluates the guard and when \false{} returns an empty list.
459The (ListG) rule evaluates the iteration set \(PE\) to get its value \(S\), which must be \gls{fixed}.
460It 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\).
461It returns the concatenation of the resulting lists with all the additional \nanozinc{} items.
462
463\subsection{Prototype Implementation}
464
465Our prototype implementation of the \microzinc{}/\nanozinc{} framework consists of the following components.
466
467The \gls{compiler} translates \minizinc{} into a \gls{byte-code} encoding of \microzinc{}.
468The compiler currently supports a significant subset of the full \minizinc{} language.
469The missing features, such as floating point values and complex output statements, require additional engineering effort, but do not require new technology.
470
471The \gls{interpreter} evaluates \microzinc{} \gls{byte-code} and \nanozinc{} programs based on the \gls{rewriting} system introduced in this section.
472It can read \parameters{} from a file or via an \glsxtrshort{api}.
473The \gls{interpreter} constructs the call to the \mzninline{main} function, and then performs the \gls{rewriting} into \gls{slv-mod} \nanozinc{}.
474Memory management is implemented using reference counting, which lends itself well to the simplifications discussed in the next section.
475The interpreter is written in around 3.5kLOC of C++ to enable easy embedding into applications and other programming languages.
476
477The framework has the ability to support multiple \solvers{}.
478It can pretty-print the \nanozinc{} code to standard \flatzinc{}, so that any solver currently compatible with \minizinc{} can be used.
479Additionally, a direct C++ \glsxtrshort{api} can be used to connect solvers directly, in order to enable incremental solving.
480We revisit this topic in \cref{ch:incremental}.
481The source code for the complete system has been made available under an open-source licence, and it has been included in the experiment resources in \cref{ch:benchmarks}.
482
483\section{NanoZinc Simplification}\label{sec:rew-simplification}
484
485The 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.
486This section looks at further steps that the system can perform in order to produce better, more compact \glspl{slv-mod}.
487
488\subsection{Removing unused decision variables and constraints}
489
490The most basic form of simplification is to identify \variables{} that are not used by any call, and remove them.
491This 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.
492The model without the unused \variable{} is therefore \gls{eqsat} with the original model.
493
494Consider now the case where a \variable{} in \nanozinc{} is only used in its attached \constraints{}.
495The \constraints{} directly succeeding the declaration prepended by \texttt{↳}.
496
497\begin{example}\label{ex:rew-absreif}
498
499 The following is a slight variation on the \minizinc{} fragment in \cref{ex:rew-absnzn}.
500
501 \begin{mzn}
502 constraint abs(x) > y \/ c;
503 constraint c;
504 \end{mzn}
505
506 The \constraint{} \mzninline{abs(x) > y} is now used in a disjunction.
507 This means that instead of enforcing the \constraint{} globally, we need to create a \gls{reif}.
508 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.
509 It uses a \variable{} \mzninline{b} that will be introduced for \mzninline{abs(x) > y}.
510 The \gls{rewriting} of this fragment will result in the following \nanozinc{} program.
511
512 \begin{nzn}
513 var true: c;
514 var -10..10: x;
515 var -10..10: y;
516 var int: z;
517 ↳ constraint int_abs(x, z);
518 var bool: b;
519 ↳ constraint int_gt_reif(z, y, b);
520 constraint bool_or(b, c);
521 \end{nzn}
522
523 Evaluating \mzninline{constraint c} has resulted in the domain of \mzninline{c} to be \gls{fixed} to \true{}.
524 The disjunction now trivially holds, independent of the value of \mzninline{b}.
525 The \gls{reif} of \mzninline{abs(x) > y} is therefore not required.
526 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}.
527
528 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{}.
529 It was only referenced from the \mzninline{bool_or} call.
530 Removing \mzninline{b} leads to its defining \constraint{}, \mzninline{int_gt_reif}, being removed.
531 This in turn means that \mzninline{z} is not referenced anywhere outside its attached \constraints{}.
532 It can also be removed together with its definition.
533 The resulting \nanozinc{} program is much more compact.
534
535 \begin{nzn}
536 var true: c;
537 var -10..10: x;
538 var -10..10: y;
539 \end{nzn}
540
541 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.
542 Note how it is crucial to exclude the attached \constraints{} when counting the usage of \variables{}.
543 \mzninline{int_abs(x, z)}, the \constraint{} which merely defines \mzninline{z}, would otherwise require us to keep \mzninline{z} in the \nanozinc{} program, if it were included in the count.
544\end{example}
545
546It 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{}.
547Top-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.
548\Constraints{} attached to a \variable{}, on the other hand, are used to define a \variable{}.
549\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}.
550In 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.
551
552\begin{example}
553 The importance of the use of attached \constraints{} when removing unused \variables{} and \constraints{} is demonstrated in the following \minizinc{} fragment.
554
555 \begin{mzn}
556 int: n;
557 var int: x;
558 function var int: f(var int: x, int: i) = let {
559 var int: y;
560 constraint y = x * i;
561 } in y;
562 constraint [f(x,i) | i in 1..n][n] == 10;
563 \end{mzn}
564
565 The \gls{rewriting} of this \minizinc{} model will initially create the \mzninline{n} elements for the \gls{array} \gls{comprehension}.
566 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}.
567 Although \mzninline{n} variables are created, only the last \variable{} is constrained to take the value ten.
568 All other \variables{} can thus be removed, and the model will stay \gls{eqsat}.
569
570 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{}.
571 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 multiplication \constraints{}.
572
573 For this example the current \minizinc{} compiler, version 2.5.5, will produce a \gls{slv-mod} that contains:
574
575 \begin{itemize}
576 \item the variable \mzninline{x},
577 \item \mzninline{n-1} variables \mzninline{y},
578 \item \mzninline{n-1} multiplication \constraints{}.
579 \end{itemize}
580
581 \noindent{}It creates the definitions for \mzninline{y} despite the fact that the \domain{} of the \variable{} \mzninline{x} has already been \gls{fixed} to 1\@.
582 The \nanozinc{} system can correctly detect that the \mzninline{y} \variables{} and multiplication \constraints{} are not required.
583\end{example}
584
585\paragraph{Implementation} The removal of unused identifiers is taken care of by garbage collection in the interpreter.
586Since our prototype interpreter uses reference counting, it already accurately tracks the liveness of each identifier.
587
588\subsection{Constraint Propagation}
589
590\Gls{propagation} is the main inference technique used in \gls{cp} \solvers{}, as discussed in \cref{subsec:back-cp}.
591At 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.
592Since a \nanozinc{} program is in fact quite similar to the internal representation of \gls{cp} \solver{}, we can use \gls{propagation} to simplify \nanozinc{}.
593
594When using \gls{propagation} for \nanozinc{} simplification, we have to carefully consider its effects.
595For 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}.
596Note, 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{}.
597When the \domain{} of a \variable{} is tighter than the \gls{bounds} given by its defining expression, the \domain{} are said to be \gls{binding}.
598For 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.
599We therefore need to track whether the \domain{} of a \variable{} is the result of external \constraints{}, or is the consequence of its own definition.
600
601A further effect of \gls{propagation} is the replacement of \constraints{} by simpler versions.
602A \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}.
603Propagating 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}.
604
605The \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}.
606It has been shown previously that applying full \gls{propagation} during compilation can be beneficial \autocite{leo-2015-multipass}.
607This works particularly well when the target solver requires complicated reformulations, such as linearization for \gls{mip} \solvers{} \autocite{belov-2016-linearization}.
608
609Returning to the example above, \gls{propagation} (and other model simplifications) can result in equality \constraints{} \mzninline{x=y} being introduced.
610For 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.
611Equalities therefore present a valuable opportunity for model simplification, but also pose some challenges.
612
613Consider 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.
614In 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}.
615
616The more complicated case for \mzninline{x=y} is when both \mzninline{x} and \mzninline{y} are the result of function calls.
617For example, a \constraint{} such as \mzninline{constraint f(a)=g(b)}.
618Assuming 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.
619
620\begin{nzn}
621 var int: x;
622 ↳ constraint f_rel(a, x);
623 var int: y;
624 ↳ constraint g_rel(b, y);
625 constraint int_eq(x, y);
626\end{nzn}
627
628In this case, simply removing either \mzninline{x} or \mzninline{y} would not be correct.
629This would trigger the removal of the corresponding definition \mzninline{f_rel(a, x)} or \mzninline{g_rel(b, y)}, leaving nothing to be substituted.
630Rather, the \interpreter{} needs to pick one of the two definitions and promote it to top-level status.
631Let us assume that the \interpreter{} decides to replace \mzninline{y} by \mzninline{x}.
632\mzninline{y} is then globally replaced by \mzninline{x}, and its declaration is removed.
633The \interpreter{} moves all attached \constraints{} from \mzninline{y} into the list of top-level \constraints{}, and then removes the \mzninline{int_eq} \constraint{}.
634The following \nanozinc{} program would be its result.
635
636\begin{nzn}
637 var int: x;
638 ↳ constraint f_rel(a, x);
639 constraint g_rel(b, x);
640\end{nzn}
641
642The process of equality propagation is similar to unification in logic programming \autocite{warren-1983-wam}.
643However, 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{}.
644
645\paragraph{Implementation}
646
647\Gls{rewriting} a function call that has a \microzinc{} definition and \gls{rewriting} a \constraint{} due to \gls{propagation} are very similar.
648The \interpreter{} therefore simply interleaves both forms of \gls{rewriting}.
649Efficient \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).
650To 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).
651These links do not take part in the reference counting.
652
653Together with its current \domain{}, each \variable{} in the interpreter also contains a Boolean flag.
654This flag signifies whether the \domain{} of the \variable{} is \gls{binding}.
655It is set when the \domain{} of a \variable{} is tightened by a \constraint{} that is not attached to the \variable{}.
656When the flag is set, the \variable{} cannot be removed, even when the reference count is zero.
657This \constraint{} may then become subsumed after \gls{propagation} and can then be removed.
658Its meaning is now completely captured by the \domains{} of the \variables{}.
659However, if any defining \constraint{} can later determine the same, or a strictly tighter, \domain{}, then it is not \gls{binding} any longer.
660It is again fully implied by its defining \constraints{}.
661The flag can then be unset and the \variable{} can potentially be removed.
662
663\subsection{Delayed Rewriting}
664
665\Gls{propagation} can tighten \domains{} of \variables{} or even fix them to a single value.
666When this happens for the arguments of a call, a more specific \gls{decomp} may become available.
667As 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}.
668
669In our \microzinc{}/\nanozinc{} system, we allow functions to be annotated as potential candidates for \gls{del-rew}.
670Any 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.
671When \gls{propagation} reaches a \gls{fixpoint}, all \glspl{annotation} are removed from the current \nanozinc{} program, and evaluation resumes with the function bodies.
672
673This crucial optimization enables rewriting in multiple phases.
674For example, a \cmodel{} targeted at a \gls{mip} \solver{} is rewritten into Boolean and reified \constraints{}, whose definitions are annotated to be delayed.
675The \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}.
676
677\begin{example}
678 Let us revisit the example from \cref{subsec:back-delayed-rew}.
679 The following \minizinc{} fragment calls a predicate that uses the ``Big M method''.
680
681 \begin{mzn}
682 function var int: lq_zero_if_b(var int: x, var bool: b) ::delayed =
683 x <= ub(x)*(1-b); % b -> x<=0
684
685 var 0..1000: x;
686 var bool: b;
687 constraint lq_zero_if_b(x, b);
688 constraint x <= 10;
689 \end{mzn}
690
691 If this fragment is processed without the \gls{del-rew}, then it will result in the following \nanozinc{}.
692
693 \begin{nzn}
694 var 0..100: x;
695 var bool: b;
696 constraint int_lin_le([1, 1000], [x,b], 1000);
697 \end{nzn}
698
699 Note, however, that if \mzninline{ub(x)} was known to be 100, then a stronger constraint could have been used.
700 When using \gls{del-rew}, the interpreter will instead first produce the following \nanozinc{}.
701
702 \begin{nzn}
703 var 0..100: x;
704 var bool: b;
705 constraint lq_zero_if_b(x, b);
706 \end{nzn}
707
708 Because the evaluation of \mzninline{lq_zero_if_b} is delayed until after the domain changes of \mzninline{x} it can instead produce \mzninline{int_lin_le([1, 100], [x,b], 100)}.
709\end{example}
710
711\subsection{Common Sub-expression Elimination}%
712\label{sec:rew-cse}
713
714As shown in \cref{subsec:back-cse}, \gls{cse} is a crucial technique to avoid duplications in a \gls{model}.
715In our architecture \gls{cse} is performed on two levels.
716
717The \microzinc{} \interpreter{} performs \gls{cse} through memoization.
718It maintains a table that maps a function identifier and the call arguments to its result for each call instruction that is executed.
719Before it executes a call instruction, it searches the table for an entry with identical function identifier and call arguments.
720Since 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.
721
722Earlier in the process, however, the \minizinc{} to \microzinc{} \compiler{} can perform \gls{cse} as it is performed in many other programming languages.
723
724\begin{example}
725 For instance, let us reconsider the following \minizinc{} fragment from \cref{ex:back-cse}.
726
727 \begin{mzn}
728 (abs(x)*2 >= 20) \/ (abs(x)+5 >= 15)
729 \end{mzn}
730
731 In this case a static \gls{compiler} analysis could detect that the same syntactical expression, \mzninline{abs(x)}, occurs twice.
732 Since these expressions are guaranteed to have equivalent results, this analysis could then hoist the shared expression into a \gls{let}.
733
734 \begin{mzn}
735 constraint let { var int: y = abs(x) } in
736 (y*2 >= 20) \/ (y+5 >= 15)
737 \end{mzn}
738 \codeendsexample{}
739\end{example}
740
741As such, the \compiler{} can enforce sharing of common sub-expressions before evaluation begins.
742It 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.
743Since the static analysis is cheap, it is valuable to combine both approaches.
744The static approach can be further improved by inlining function calls, since that may expose more calls as being syntactically equal.
745
746\paragraph{Implementation} In the implementation of our \microzinc{} \interpreter{}, \gls{cse} directly interacts with the reference counting mechanism.
747It is clear that when an expression is reused by returning it from the \gls{cse} table, this creates a new reference to that expression.
748However, the entries in the \gls{cse} table should not keep the corresponding variables alive.
749Otherwise, none of the \variables{} would ever become unused.
750Therefore, we treat \gls{cse} entries as weak references.
751They reference a \variable{}, but do not affect its liveness (i.e., increase its reference count).
752If 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.
753
754The usage of a \gls{cse} table can be costly.
755The memory requirement and time spent finding entries can be significant in the overall process.
756This 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.
757Although this structure offers flexibility when defining \minizinc{} libraries, it results in many \gls{cse} entries that differ only by their function identifier.
758
759\begin{example}
760 For example, the definition of the \mzninline{knapsack} \gls{global} in the \minizinc{} standard library is shown in \cref{lst:rew-knapsack}.
761 After checking the \parameter{} arguments, the function merely returns the result of \mzninline{fzn_knapsack}.
762 This function is implemented in the \solver{} library to provide the implementation of the \mzninline{knapsack} \gls{global}.
763 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.
764 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.
765\end{example}
766\begin{listing}
767 \mznfile{assets/listing/rew_knapsack.mzn}
768 \caption{\label{lst:rew-knapsack} The definition of \mzninline{knapsack} in the \minizinc{} standard library.}
769\end{listing}
770
771Therefore, we have added a flag to our call instruction.
772This flag controls whether the call is subject to \gls{cse}.
773This allows us to disable the \gls{cse} when it is guaranteed to be unnecessary.
774
775\subsection{Constraint Aggregation}%
776\label{subsec:rew-aggregation}
777
778In our new system it is still possible to support \gls{aggregation}.
779We aggregate \constraints{} by combining \constraints{} connected through attached \constraints{}, eliminating the need for \gls{avar} to which they are attached.
780To aggregate a certain kind of \constraint{}, it is marked as a \gls{native} \constraint{}.
781These functional definitions are kept in the \nanozinc{} program until a top-level \constraint{} is posted that uses the \variables{} to which they are attached.
782Once this happens, the interpreter will employ dedicated \gls{aggregation} logic to visit the attached \constraints{} and combine them.
783The top-level \gls{constraint} is then replaced by the combined \gls{constraint}.
784When the \gls{avar} become unused, they will be removed using the normal mechanisms.
785
786\begin{example} For example, let us reconsider the linear \constraint{} from \cref{ex:back-agg}: \mzninline{x + 2*y <= z}.
787 The constraint will result in the following \nanozinc{}.
788
789 \begin{nzn}
790 var int: x;
791 var int: y;
792 var int: z;
793 var int: i1;
794 ↳ constraint '*'(y, 2, i1);
795 var int: i2;
796 ↳ constraint '+'(x, i1, i2);
797 constraint '<='(i2, z);
798 \end{nzn}
799
800 \mzninline{*} and \mzninline{+} were marked as \gls{native} \constraints{} as they can be aggregated into a linear \constraint{}.
801 Their functional definitions are put in place in the \nanozinc{}, and then a top-level \mzninline{<=} \constraint{} is created.
802 The \interpreter{} will then recursively visit the arguments of the \constraints{}.
803 The \constraints{} are then combined into the following linear \constraint{}.
804
805 \begin{mzn}
806 constraint int_lin_le([1,2,-1], [x,y,z], 0)
807 \end{mzn}
808 \codeendsexample{}
809\end{example}
810
811\section{Experiments}\label{sec:rew-experiments}
812
813We have created a prototype implementation of the architecture presented in the preceding sections.
814It consists of a \compiler{} from \minizinc{} to \microzinc{}, and a \microzinc{} \interpreter{} producing \nanozinc{}.
815The 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 \glspl{annotation}.
816
817The 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.
818In 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.
819A description of the used computational environment, \minizinc{} instances, and versioned software has been included in \cref{ch:benchmarks}.
820
821For 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.
822In 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}).
823We 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).
824Times are averages of 10 runs.
825
826\Cref{sfig:rew-compareruntime} compares the \gls{rewriting} time for each of \instances{}.
827Points below the line indicate that the new system is faster.
828On 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.
829In terms of memory performance (\cref{sfig:rew-comparemem}), version 2.5.5 can sometimes still outperform the new prototype.
830We have identified that the main memory bottlenecks are our currently unoptimized implementations of \gls{cse} lookup tables and argument vectors.
831These are very encouraging results, given that we are comparing a largely unoptimized prototype to a mature piece of software.
832
833\begin{figure}
834 \centering
835 \begin{subfigure}[b]{.48\columnwidth}
836 \centering
837 \includegraphics[width=\columnwidth]{assets/img/rew_compare_runtime}
838 \caption{\label{sfig:rew-compareruntime}Average run time (ms)}
839 \end{subfigure}%
840 \hspace{0.04\columnwidth}%
841 \begin{subfigure}[b]{.48\columnwidth}
842 \centering
843 \includegraphics[width=\columnwidth]{assets/img/rew_compare_memory}
844 \caption{\label{sfig:rew-comparemem}Maximum resident set size (kbytes)}
845 \end{subfigure}
846 \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.}
847\end{figure}
848
849Our second experiment considers three well-known computational recursive functions: Ackermann, Fibonacci, and Takeuchi.
850These functions are often used as a benchmark for implementations of functional programming languages.
851Since the \minizinc{} language includes a strong functional programming component, we use these same functions as a benchmark for our prototype \interpreter{}.
852In 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}.
853The chosen function arguments try to exercise the \glspl{interpreter}, but without running into their limitations.
854Times are averages of 1000 runs.
855
856The results of the experiment are shown in \cref{fig:rew-interpreter-comp}.
857For all experiments there is a clear ordering in the results:
858\begin{itemize}
859 \item OCaml is the clear winner, always at least five times faster than its closest competitor;
860 \item our prototype finishes in second place;
861 \item Python is a close third, with only a significant difference compared to our prototype on the Ackermann benchmark; and
862 \item \minizinc{} 2.5.5 always finishes last out of the four interpreters with significant overhead over all other competitors.
863\end{itemize}
864Our prototype performs well in this test.
865It clearly outperforms \minizinc{} 2.5.5 with about ten times speed-up, and it slightly outperforms Python, an optimized \interpreter{} for a general programming language.
866It is clear though that OCaml, a language that is dedicated to these types of programs, still outperforms our prototype.
867We are convinced, however, that we can get closer to its performance given the right improvements in our prototype.
868
869\begin{figure}
870 \centering
871 \includegraphics[width=\columnwidth]{assets/img/rew_interpreter_plot}
872 \caption{\label{fig:rew-interpreter-comp} Run-time comparison of interpreters
873 on recursive functions: Takeuchi, Fibonacci, and Ackermann.}
874\end{figure}
875
876\pagebreak{}
877\section{Summary}%
878\label{sec:rew-summary}
879
880This chapter presented a new architecture for \gls{rewriting} \minizinc{} \instances{} to \glspl{slv-mod}.
881We introduced the intermediate languages \microzinc{} and \nanozinc{}, which are central to the \gls{rewriting} architecture.
882\minizinc{} is transformed into a set of \microzinc{} definitions and a \nanozinc{} program.
883Then, a \nanozinc{} program is partially evaluated using \microzinc{} definitions.
884We presented formal \gls{rewriting} rules applied during this partial evaluation.
885
886Continuously applying these rules would result in a correct, but inefficient \gls{slv-mod}.
887Therefore, we extended the partial evaluation using well-known techniques to improve the \gls{slv-mod}: \gls{propagation} is used throughout the rewriting process, calls can be delayed until more information is known, \gls{cse} is used both when evaluating calls and during the \minizinc{} to \microzinc{} transformation, and \constraints{} can be aggregated when beneficial for the \solver{}.
888Crucially, the system can correctly remove all unused and irrelevant \variables{} and \constraints{} by \nanozinc{}'s mechanism to attach \constraints{} to the \variable{} they define.
889The prototype of this architecture is shown to be significantly faster than the current implementation of \minizinc{}.
890
891The next chapter further extends the architecture to better reason about \gls{reif}, to fully avoid it or use \gls{half-reif} where possible.