860 lines
54 KiB
TeX
860 lines
54 KiB
TeX
%************************************************
|
|
\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, only applying the \glspl{decomp} of \constraints{} to the \instance{} will often result in a sub-optimal \gls{slv-mod}.
|
|
This might result in exponentially more work for the \solver{}.
|
|
|
|
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 \glspl{slv-mod} the \gls{rewriting} process uses many simplification techniques such as:
|
|
|
|
\begin{itemize}
|
|
\item continuously updating \variable{} \domains{},
|
|
\item using specialised \glspl{decomp} when variables get fixed,
|
|
\item and removing \variables{} and \constraints{} that are no longer required.
|
|
\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 formalised rewriting rules.
|
|
These rules makes it easy to reason about 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{} model, no recompilation is required for the unchanged parts.
|
|
|
|
\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 typechecking, a \minizinc{} model is first compiled into a smaller constraint language called \microzinc{}, independent of the data.
|
|
After the \microzinc{} is transformed into a \gls{byte-code} for an \interpreter{}.
|
|
This \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 extensions 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 of these advantages.
|
|
The prototype is still very experimental, but preliminary results suggest the new tool chain can perform flattening 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 abstract machine model we have developed.
|
|
|
|
\microzinc{} is a simplified subset of \minizinc\ that only contains function declarations and a restricted expression language, but it extends \minizinc{}'s type system with tuples.
|
|
\Glspl{model} written in \minizinc\ can be translated into \microzinc{}.
|
|
|
|
\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 bound to a specific \variable{} and \constraints{} and \variable{} declarations can be interleaved.
|
|
|
|
The core of the syntax of \microzinc{} is defined in \cref{fig:rew-uzn-syntax}.
|
|
We have omitted the definitions of \syntax{<mzn-type-inst>} and \syntax{<ident>}, which you can assume 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, the conditions \syntax{<exp>} in if-then-else and where expressions have \mzninline{par} type.
|
|
|
|
\begin{figure}
|
|
\begin{grammar}
|
|
<model> ::= <pred-decl>*<fun-decl>*
|
|
|
|
<pred-decl> ::= "predicate" <ident>"(" <param> ["," <param>]* ");"
|
|
|
|
<fun-decl> ::= "function" <type-inst>":" <ident>"(" <param> ["," <param>]* ")" "=" <exp>";"
|
|
|
|
<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> ::= <param> [ "=" <exp> ]";"
|
|
\alt "tuple(" <type-inst> ["," <type-inst>]* "):" <ident> = "(" <exp> ["," <exp>]* ")";
|
|
\alt "(" <param> ["," <param>]* ")" "=" <exp>";"
|
|
\alt "constraint" <exp>";"
|
|
|
|
<param> ::= <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 track dependent constraints (this will be explained in detail in \cref{sec:rew-nanozinc}, for now you can ignore them).
|
|
|
|
\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-bind>*
|
|
|
|
<nzn-dom> ::= <constant> ".." <constant> | <constant>
|
|
\alt "bool" | "int" | "float" | "set of int"
|
|
|
|
<nzn-bind> ::= "↳" <nzn-con>
|
|
\end{grammar}
|
|
\caption{\label{fig:rew-nzn-syntax}Syntax of \nanozinc{}.}
|
|
\end{figure}
|
|
|
|
\subsection{\glsentrytext{minizinc} to \glsentrytext{microzinc}/\glsentrytext{nanozinc}}
|
|
|
|
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)}.
|
|
As mentioned above, 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 by a call:
|
|
|
|
\begin{mzn}
|
|
if_then_else([x, true], [A, B])
|
|
\end{mzn}
|
|
|
|
\noindent{}And, an expression \mzninline{A[x]}, where \mzninline{x} is a \variable{}, is replaced by a call:
|
|
|
|
\begin{mzn}
|
|
element(A, x)
|
|
\end{mzn}
|
|
|
|
\item Replace optional \variables{} into non-optional forms.
|
|
As shown by Mears et al., optional variable types can be represented using a \variable{} of the same non-optional type and a Boolean \variable{} \autocite*{mears-2014-option}.
|
|
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 functions definitions for optional types then take both \variables{} into account.
|
|
For example, the definition of \mzninline{int_plus(x, y)} for optional types will add the value variable to the result of the function if Boolean \variable exists.
|
|
|
|
\item Lift the partiality in expressions into the surrounding context to implement \minizinc{}'s relational semantics.
|
|
In contrast to \minizinc{}, the evaluation of \microzinc{} will implement strict semantics for partial expressions, whereas \minizinc\ uses relational semantics.
|
|
Stuckey and Tack have extensively examined these problems and describe how to transform any partial function into a total function.
|
|
\autocite*{stuckey-2013-functions}.
|
|
A general approach for describing the partially in \microzinc{} functions is to make the function return an additional Boolean \variable{}.
|
|
This \variable{} indicates the totality with regards to the input to the function.
|
|
The resulting value of the function is then adjusted to return a predefined value when it would normally be undefined.
|
|
For example, The function
|
|
|
|
\begin{mzn}
|
|
function var int: element(array of int: a, var int: x);
|
|
\end{mzn}
|
|
|
|
\noindent{}is only defined when \mzninline{x in index_set(a)}.
|
|
A total version to be used in \microzinc{} could look like\footnote{For brevity's sake, we will still use \minizinc{} \glspl{operator} to write the \microzinc{} definition.}:
|
|
|
|
\begin{mzn}
|
|
function tuple(var int, var bool): element_safe(array of int: a, var int: x) =
|
|
let {
|
|
set of int: idx = index_set(x)
|
|
var bool: total = x in idx;
|
|
var idx: xs;
|
|
int: m = min(idx);
|
|
% Give xs the value of x when result is total
|
|
constraint total -> xs = x;
|
|
% Otherwise, give xs the value m instead
|
|
constraint not total -> xs = m;
|
|
% element constraint that is guaranteed to be total
|
|
var res = element(a, xs);
|
|
tuple(var int, var bool): ret = (res, total);
|
|
} in ret;
|
|
\end{mzn}
|
|
|
|
Similar to the replacement of optional values, all usage 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 transformed into:
|
|
|
|
\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 which 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 might look like:
|
|
|
|
\begin{mzn}
|
|
function f_int(int: x) = /* original body */;
|
|
function f_varint(varint: x) =
|
|
if is_fixed(x) then
|
|
f_int(x)
|
|
else
|
|
/* original body */;
|
|
endif;
|
|
\end{mzn}
|
|
|
|
\item Transform all function definitions so that they do not refer to top-level \variables{}, by adding those \variables{} as extra arguments to the function declaration and each call site.
|
|
|
|
\item Move all top-level \variable{} declarations and \constraints{} into a let expression in the body of a new function called \mzninline{main}, whose arguments are the parameters of the model and which returns a fresh Boolean \variable{}.
|
|
|
|
\end{enumerate}
|
|
|
|
\begin{example}
|
|
|
|
Consider the following \minizinc{} model, a simple \gls{unsat} ``pigeonhole problem'', trying to assign \(n\) pigeons to \(n-1\) holes:
|
|
|
|
\begin{mzn}
|
|
predicate all_different(array[int] of var int: x) =
|
|
forall (i,j in 1..length(x) where i<j) (
|
|
x[i] != x[j]
|
|
);
|
|
|
|
int: n;
|
|
array[1..n] of var 1..n-1: pigeon;
|
|
constraint all_different(pigeon);
|
|
\end{mzn}
|
|
|
|
The translation to \microzinc{} turns all expressions into function calls, replaces the special generator syntax in the \mzninline{forall} with an array comprehension, and creates the \mzninline{main} function.
|
|
|
|
\begin{mzn}
|
|
function var bool: all_different(array[int] of var int: x) =
|
|
forall([
|
|
int_neq(element(x, i),element(x, j))
|
|
| i in range(1, length(x)),
|
|
j in range(1, length(x))
|
|
where int_lt(i,j)
|
|
]);
|
|
|
|
function var bool: main(int: n) = let {
|
|
var bool: root_ctx;
|
|
array[1..n] of var 1..n-1: pigeon;
|
|
constraint all_different(pigeon);
|
|
} in root_ctx;
|
|
\end{mzn}
|
|
|
|
For an \instance of the \cmodel{}, we can then create a simple \nanozinc{} program that calls \mzninline{main}, for example for \(n=10\):
|
|
|
|
\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} predicate, or it has a corresponding \microzinc\ function definition.
|
|
The goal of partial evaluation is to rewrite the \nanozinc{} program into a \gls{slv-mod}, \ie\ a program where all calls are calls to \gls{native} predicates.
|
|
|
|
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 \glspl{ivar} to represent intermediate expressions.
|
|
|
|
\begin{example}\label{ex:rew-abs}
|
|
Consider the following (reasonably typical) \minizinc\ encoding for the absolute value function:
|
|
|
|
\begin{mzn}
|
|
function var int: abs(var int: x) =
|
|
let {
|
|
var int: z;
|
|
constraint int_abs(x, z);
|
|
} in z;
|
|
\end{mzn}
|
|
|
|
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.
|
|
\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 \mzninline{let} expression 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 \emph{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 optimisations 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\ model (\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 it is associated with a list of identifiers of auxiliary \constraints{}.
|
|
\Constraints{} can also occur at the top-level of the \nanozinc{} model.
|
|
These are said to be the ``root-context'' \constraints{} of the model, \ie\ those that have to hold globally and are not just used to define an \gls{ivar}.
|
|
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 \minizinc{} fragment
|
|
|
|
\begin{mzn}
|
|
constraint abs(x) > y;
|
|
\end{mzn}
|
|
|
|
\noindent{}where \mzninline{x} and \mzninline{y} have domain \mzninline{-10..10}.
|
|
After rewriting all definitions, the resulting \nanozinc{} program could look like this:
|
|
|
|
\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 (\ie\ not used in the rest of the \nanozinc\ program), by suitable alpha renaming.
|
|
|
|
\begin{figure*}
|
|
\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{predicate}~\ptinline{F(\(p_1, \ldots, p_k\));} \in \Prog}
|
|
\infer1[(CallPredicate)]{\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 (CallPredicate) rule applies to calls to predicates \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*}
|
|
\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\ let expressions to \nanozinc{}.}
|
|
\end{figure*}
|
|
|
|
The rules in \cref{fig:rew-rewrite-to-nzn-let} considers let expressions.
|
|
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 captured in a third evaluation arguments.
|
|
When all inner items have been evaluated, the captured \constraints{} are bound 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 remainder of the namespace.
|
|
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{\Sem{\(x\)}{\Prog, \Env} \Rightarrow \tuple{[x_{1}, \ldots, x_{n}], \Env'}}
|
|
\hypo{\Sem{\(i\)}{\Prog, \Env'} \Rightarrow \tuple{v, \Env''}}
|
|
\hypo{v \in [1 \ldots{} n]}
|
|
\infer3[(Access)]{\Sem{\(x\texttt{[}i\texttt{]}\)}{\Prog, \Env} \Rightarrow{} \tuple{x_{v}, \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{\(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, conditionals and comprehensions.
|
|
For completeness, we give the details here.
|
|
|
|
The (Ident) rule looks up a \variable{} in the environment and return its bound value (for constants) or the \variable{} itself.
|
|
The (Const) rule simply returns the constant.
|
|
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 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, with the missing features (such floating point values and complex output statements) requiring additional engineering effort but no 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 optimisations 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 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}.
|
|
|
|
\textbf{Python bindings} to the framework are provided to enable easy scripting.
|
|
The source code for the complete system will be made available under an open source license.
|
|
\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 dead 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 \variable{} is therefore \gls{eqsat} with the original model.
|
|
|
|
Consider now the case where a \variable{} in \nanozinc is only used in its own auxiliary definitions (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}:
|
|
|
|
\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 bound to \mzninline{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 true.
|
|
|
|
If the system now simplifies the constraint \mzninline{bool_or(b, c)} to \mzninline{true}, then the identifier \mzninline{b} will become unused outside its auxiliary definitions.
|
|
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 auxiliary definitions
|
|
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 counting usage of \variables{} outside its auxiliary definitions allows us to remove the \mzninline{z} variable --- we could not simply have counted the usage of \mzninline{z} in all \constraints{} since the \constraint{} used to define it, \mzninline{int_abs(x, z)}, would have kept it alive.
|
|
\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 auxiliary definitions of a \variable{}.
|
|
Top-level \constraint{} help define the problem, they are globally enforced and cannot be removed from the problem unless it can be proved that its relationship is already enforced.
|
|
\Constraints{} in auxiliary definitions, on the other hand, are used to define a \variable{}.
|
|
Auxiliary definitions generally occur from a functional relationship, 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 auxiliary definitions when removing dead \variables{} and \constraints{} is demonstrated in the following example:
|
|
|
|
\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 array 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 first \variable{} is constrained to be 10. 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 auxiliary \constraints{} of its corresponding \mzninline{y} \variable{}.
|
|
When, after evaluating the array access, all of those \variables{} except the first 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 another important technique used to simplify the produced \nanozinc{}.
|
|
It allows us to tighten the \glspl{domain} of \variables{} in the \nanozinc{} and remove \constraints{} proven to hold.
|
|
This, in turn, offers another way that \variables{} can become unused.
|
|
|
|
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 definition.
|
|
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 linearisation for \gls{mip} \solvers{} \autocite{belov-2016-linearisation}.
|
|
|
|
Returning to the example above, \gls{propagation} (and other model simplifications) can result in \emph{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, \eg\ from a \constraint{} such as \mzninline{constraint f(a)=g(b)}.
|
|
The corresponding \nanozinc{} code looks like this:
|
|
|
|
\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 \emph{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 auxiliary \constraints{} from \mzninline{y} into the list of top-level \constraints{}, and then removes the \mzninline{int_eq} \constraint{}.
|
|
The resulting \nanozinc{} looks like this:
|
|
|
|
\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 (\ie\ 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 \gls{domain} of the \variable{} is an additional constraint.
|
|
When the flag is set, the \variable{} cannot be removed, even when the reference count is zero.
|
|
This happens when a \constraint{} that does not define the variable changes its \gls{domain}.
|
|
This \constraint{} might thereafter be removed, if it now proven to hold, but its effects will still be enforced.
|
|
If, however, any defining \constraint{} further tightens the \gls{domain}, then its constraint is no longer constraining.
|
|
The flag can then be unset and the variable can potentially be removed.
|
|
|
|
\subsection{Delayed Rewriting}
|
|
|
|
\gls{propagation} might change \variables{}.
|
|
It might shrink their \domains{} or even fix them to a single value.
|
|
When this happens for the arguments of a call, a more specific \gls{decomp} might become available.
|
|
It is therefore important to evaluate calls when all possible information is available to create efficient \nanozinc{}.
|
|
|
|
In our \microzinc{}/\nanozinc{} system, we allow predicates and functions to be annotated as potential candidates for \gls{del-rew}.
|
|
Any annotated \constraint{} is handled by the (CallPredicate) 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 fix-point, all annotations are removed from the current \nanozinc{} program, and evaluation resumes with the predicate bodies.
|
|
|
|
This crucial optimisation enables rewriting in multiple \emph{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}
|
|
|
|
\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 memorisation.
|
|
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 \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 result, this analysis could then be able to hoist into a let expression.
|
|
|
|
\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 memorisation would also covers 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 \emph{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 a new reference must created when an entry of the \gls{cse} is reused in \nanozinc{}, but the entries of the table themselves are also essentially references.
|
|
However, when a \variable{} is no longer referenced in the \nanozinc{}, we still expect it to be removed, even if it is still part of the \gls{cse} table.
|
|
As such, we treat \gls{cse} entries as \emph{weak} references.
|
|
They reference an object, but do not affect its liveness (\ie{} 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.
|
|
It requires a lot of memory and the time to find 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.
|
|
Therefore, we have added an additional flag to our call instruction.
|
|
This flag controls whether the call is subject \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 functional definitions, eliminating the need for \glspl{ivar}.
|
|
To aggregate a certain kind of \constraint{}, it is marked as a \gls{native} \constraint{}.
|
|
These \constraints will now be kept as temporary functional definitions in the \nanozinc{} program.
|
|
These functional definitions are kept in the \nanozinc{} program until a top-level (relational) \constraint{} is posted that uses these definitions.
|
|
Once this happens, the interpreter will employ dedicated \gls{aggregation} logic to visit the functional definitions and combine their constraints.
|
|
The top-level \gls{constraint} is then replaced by the combined \gls{constraint}.
|
|
When the \glspl{ivar} 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);
|
|
var int: i2;
|
|
↳ constraint '+'(x, i1);
|
|
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 a single 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 an incremental \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 license and can make it available to the reviewers upon request.
|
|
\todo{I suppose it is time to release the prototype.}
|
|
|
|
The implementation is not optimised 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 an 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 global constraints (\ie\ we decompose those constraints rather than using solver primitives, in order to stress-test the flattening).
|
|
We measured pure flattening time, \ie\ 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 flattening time for each of the 100 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 speedup and multiple \instances{} with a speedup 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 unoptimised implementations of \gls{cse} lookup tables and argument vectors.
|
|
These are very encouraging results, given that we are comparing a largely unoptimised 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 flattening MiniZinc Challenge
|
|
instances. \minizinc\ 2.5.5 (x-axis) vs new architecture (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 limitations of any of them.
|
|
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 protoype performs well in this test.
|
|
It clearly outperforms \minizinc{} 2.5.5 with about 10 times speedup and it slightly outperforms Python, an optimised \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 solver-level constraint model 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.
|