892 lines
59 KiB
TeX
892 lines
59 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 a \gls{slv-mod} may often seem like a simple \gls{trs}.
|
|
In reality, however, \minizinc{} is quite a complex language, and producing a good \gls{slv-mod} is far from trivial.
|
|
|
|
Thus, in practice, this rewriting process is a highly complex task that needs to carefully track interactions between \constraints{} and how they affect \variables{}.
|
|
To create an efficient \gls{slv-mod} the \gls{rewriting} process uses many simplification techniques such as:
|
|
|
|
\begin{itemize}
|
|
\item continuously updating \variable{} \domains{},
|
|
\item \gls{propagation} for known \constraints{},
|
|
\item specialized \glspl{decomp} when variables get \gls{fixed},
|
|
\item \gls{aggregation},
|
|
\item common sub-expression elimination,
|
|
\item and removing \variables{} and \constraints{} that are not required any longer.
|
|
\end{itemize}
|
|
|
|
We now present a new architecture for the \gls{rewriting} process that has been designed for the modern day needs of \minizinc{}.
|
|
At the core of our \gls{rewriting} process lie formalized rewriting rules.
|
|
As such, this architecture represents an abstract machine model for \minizinc{}.
|
|
These rules allow us to reason about the system and about the simplifications both to the process and the resulting \gls{slv-mod}.
|
|
The process can even be made incremental: in \cref{ch:incremental} we discuss how when making incremental changes to the \minizinc{} \instance{}, unchanged parts of the \instance{} do not need to be rewritten again.
|
|
|
|
\begin{figure}
|
|
\centering
|
|
\includegraphics[width=\linewidth]{assets/img/rew_compilation_structure}
|
|
\caption{\label{fig:rew-comp} The proposed process for the compilation of \minizinc{} instances.}
|
|
\end{figure}
|
|
|
|
The process of the new architecture is shown in \cref{fig:rew-comp}.
|
|
After parsing and type checking, a \minizinc{} model is first compiled into a smaller constraint language called \microzinc{}, independent of the data.
|
|
For efficient execution, the \microzinc{} is then transformed into a \gls{byte-code}.
|
|
Together, the \gls{byte-code} and a complete \gls{parameter-assignment} form an \instance{} that can be executed by the \microzinc{} \interpreter{}.
|
|
During its execution, the \interpreter{} continuously updates a \cmodel{} according to the \microzinc{} definition.
|
|
The \cmodel{} in the \interpreter{} is internally represented as a \nanozinc{} program.
|
|
\nanozinc{} is a slight extension of the \flatzinc{} format.
|
|
The \interpreter{} finishes when it reaches a \gls{slv-mod}.
|
|
|
|
We have developed a prototype of this 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{}.
|
|
|
|
\section{\glsentrytext{microzinc} and \glsentrytext{nanozinc}}\label{sec:rew-micronano}
|
|
|
|
This section introduces the two sub-languages of \minizinc{} at the core of the new architecture we have developed.
|
|
|
|
\microzinc{} is a simple language used to define transformations to be performed by the \interpreter{}.
|
|
It is a simplified subset of \minizinc{}.
|
|
The transformation are represented in the language through the use of function definitions.
|
|
A function of type \mzninline{var bool}, describing a relation, can be defined as a \gls{native} \constraint{}.
|
|
Otherwise, a function body must be provided for \gls{rewriting}.
|
|
The function body can use a restriction of the \minizinc{} expression language.
|
|
|
|
An important difference between \minizinc{} and \microzinc{} is that a well-formed \microzinc{} does not contain partial expressions.
|
|
Any partiality in the \minizinc{} model must be explicitly expressed using total functions in \microzinc{}.
|
|
As such, \constraints{} introduced in \microzinc{} \glspl{let} can be globally enforced.
|
|
They are guaranteed to only constrain the \variables{} introduced in the same \gls{let}.
|
|
|
|
\nanozinc{} is used to represent the current state of the \instance{}.
|
|
\nanozinc{} is similar to \flatzinc{} in that it contains only declarations of \variables{} and a flat list of \constraints{}.
|
|
However, while all function calls in \flatzinc{} need to be \gls{native}, \nanozinc{} calls can refer to any function implemented in \microzinc{}.
|
|
Furthermore, \nanozinc{} allows for \constraints{} to be ``attached'' to a \variable{}, in order to be able to track their lifetime and remove them if the corresponding \variable{} becomes unused.
|
|
As a small syntactic difference with \flatzinc{}, \constraints{} and \variable{} declarations in \nanozinc{} can be freely interleaved.
|
|
|
|
The core of the syntax of \microzinc{} is defined in \cref{fig:rew-uzn-syntax}.
|
|
Function declarations without an expression body are used to mark functions that are \gls{native} to the target \solver{}.
|
|
We have omitted the definitions of \syntax{<mzn-type-inst>} and \syntax{<ident>}, which can be assumed to be the same as the definition of \syntax{<type-inst>} and \syntax{<ident>} in the \minizinc{} grammar, see \cref{ch:minizinc-grammar}.
|
|
While we omit the typing rules here for space reasons, we will assume that in well-typed \microzinc{} programs conditions of expressions are \parameters{}.
|
|
This means that the where conditions \syntax{<exp>} in \glspl{comprehension}, the conditions \syntax{<exp>} in \gls{conditional} expressions, and the \syntax{<literal>} index in \gls{array} accesses must have \mzninline{par} type.
|
|
In \minizinc{} the use of \variables{} in these positions is allowed, and these expressions are rewritten to function calls.
|
|
We will discuss how the same transformation takes place when translating \minizinc{} to \microzinc{}.
|
|
|
|
\begin{figure}
|
|
\begin{grammar}
|
|
<model> ::= <pred-decl>*<fun-decl>*
|
|
|
|
<fun-decl> ::= "function" <type-inst>":" <ident>"(" <typing> ["," <typing>]* ")" "=" <exp>";"
|
|
\alt "function" "var" "bool" ":" <ident>"(" <typing> ["," <typing>]* ")"";"
|
|
|
|
<literal> ::= <constant> | <ident>
|
|
|
|
<exp> ::= <literal>
|
|
\alt <ident>"(" <exp> ["," <exp>]* ")"
|
|
\alt "let" "{" <item>* "}" "in" <literal>
|
|
\alt "if" <exp> "then" <exp> "else" <exp> "endif"
|
|
\alt "[" <exp> "|" <gen-exp> "where" <exp> "]"
|
|
\alt <ident>"[" <literal> "]"
|
|
|
|
<item> ::= <typing> [ "=" <exp> ]";"
|
|
\alt "tuple(" <type-inst> ["," <type-inst>]* "):" <ident> = "(" <exp> ["," <exp>]* ")"";"
|
|
\alt "(" <typing> ["," <typing>]* ")" "=" <exp>";"
|
|
\alt "constraint" <exp>";"
|
|
|
|
<typing> ::= <type-inst>":" <ident>
|
|
|
|
<gen-exp> ::= <ident> "in" <exp> ["," <ident> "in" <exp> ]*
|
|
\end{grammar}
|
|
\caption{\label{fig:rew-uzn-syntax}Syntax of \microzinc{}.}
|
|
\end{figure}
|
|
|
|
A \nanozinc{} program, defined in \cref{fig:rew-nzn-syntax}, is simply a list of \variable{} declarations and \constraints{} in the form of calls.
|
|
The syntax ``\texttt{↳}'' will be used to ``attach'' \constraints{} to \variables{} in order to track dependent \constraints{}.
|
|
This will be explained in detail in \cref{sec:rew-nanozinc}.
|
|
|
|
\begin{figure}
|
|
\begin{grammar}
|
|
<nzn> ::= <nzn-item>*
|
|
|
|
<nzn-item> ::= <nzn-def> | <nzn-con>
|
|
|
|
<nzn-con> ::= "constraint" <ident>"(" <literal> ["," <literal>]* ")"";"
|
|
|
|
<nzn-var> ::= "var" <nzn-dom> ":" <ident> ";" <nzn-attach>*
|
|
|
|
<nzn-dom> ::= <constant> ".." <constant> | <constant>
|
|
\alt "bool" | "int" | "float" | "set of int"
|
|
|
|
<nzn-attach> ::= "↳" <nzn-con>
|
|
\end{grammar}
|
|
\caption{\label{fig:rew-nzn-syntax}Syntax of \nanozinc{}.}
|
|
\end{figure}
|
|
|
|
\subsection{\glsentrytext{minizinc} to \glsentrytext{microzinc}}
|
|
|
|
The translation from \minizinc{} to \microzinc{} involves the following steps.
|
|
|
|
\begin{enumerate}
|
|
|
|
\item Transform all expressions that are valid in \minizinc{} but not in \microzinc{}.
|
|
This includes simple cases such as replacing \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])}.
|
|
As mentioned above, \gls{conditional} expressions where the decision is made by a \variable{} are also not directly supported in \microzinc{}.
|
|
These expressions are therefore also replaced by function calls that are possibly decomposed.
|
|
An expression \mzninline{if x then A else B endif}, where \mzninline{x} is a \variable{}, is replaced the call \mzninline{if_then_else([x, true], [A, B])}.
|
|
A recent study by \textcite{stuckey-2019-conditionals} describes how \mzninline{if_then_else} can be decomposed for different types of \solvers{}.
|
|
An expression \mzninline{A[x]}, where \mzninline{x} is a \variable{}, is replaced by the call \mzninline{element(A, x)}.
|
|
\mzninline{element} is a well-known \gls{global}.
|
|
For many \gls{cp} \solvers{} it is a \gls{native} \constraint{} and for other \solvers{} there have long been accepted \glspl{decomp}.
|
|
|
|
\item Replace optional \variables{} into non-optional forms.
|
|
As shown by \textcite{mears-2014-option}, optional type \variables{} can be represented using a \variable{} of the same non-optional type and a Boolean \variable{}.
|
|
The Boolean \variable{}, then, represents if the variable exists or is absent, while the non-optional \variable{} of the same type represents the value of the optional \variable{} if it exists.
|
|
In \microzinc{} this can be represented as a tuple of the two \variables{}.
|
|
The function definitions for optional types then take both \variables{} into account.
|
|
For example, the definition of \mzninline{int_plus(x, y)} for optional types can be translated into the function shown in \cref{lst:rew-opt-plus}.
|
|
|
|
\begin{listing}
|
|
\mznfile{assets/listing/rew_opt_plus.mzn}
|
|
\caption{\label{lst:rew-opt-plus} A definition of \mzninline{int_plus} for optional integers in \microzinc{} syntax.}
|
|
\end{listing}
|
|
|
|
\item Lift the partiality in expressions into the surrounding context to implement \minizinc{}'s relational semantics.
|
|
In contrast to \minizinc{}, a \microzinc{} expression must be total.
|
|
\textcite{stuckey-2013-functions} have extensively examined these problems and describe how to transform any partial function into a total function while maintaining the relational semantics of the original \cmodel{}.
|
|
A general approach for describing the partiality in \microzinc{} functions is to make the function return an additional Boolean \variable{}.
|
|
This \variable{} indicates whether the result of the function call is defined w.r.t. the function arguments.
|
|
The resulting value of the function is then adjusted to return a predefined value when it would normally be undefined.
|
|
For example, the \mzninline{element} function in \minizinc{} is declared as follows.
|
|
|
|
\begin{mzn}
|
|
function var int: element(array of int: a, var int: x);
|
|
\end{mzn}
|
|
|
|
\noindent{}It is only defined when \mzninline{x in index_set(a)}.
|
|
The function shown in \cref{lst:rew-elem-safe} is a total version of this function that can be used in \microzinc{}\footnote{For brevity's sake, we will still use \minizinc{} \glspl{operator} to write the \microzinc{} definition.}.
|
|
|
|
\begin{listing}
|
|
\mznfile{assets/listing/rew_elem_safe.mzn}
|
|
\caption{\label{lst:rew-elem-safe} A total of the \mzninline{element} function in \microzinc{}.}
|
|
\end{listing}
|
|
|
|
Similar to the replacement of optional values, all occurrences of the \mzninline{element} function are replaced by \mzninline{element_safe}.
|
|
The usage of its result should be guarded by the returned totality variable in the surrounding Boolean context.
|
|
This means that, for example, the expression \mzninline{element(e, v) = 5 \/ b} would be replaced by the following expression.
|
|
|
|
\begin{mzn}
|
|
let {
|
|
(var int: res, var bool: total) = element_safe(e, v);
|
|
} in (total /\ res = 5) \/ b;
|
|
\end{mzn}
|
|
|
|
\item Resolve subtype 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.
|
|
As we will later discuss in more detail, is possible for a \variable{} to be \gls{fixed} to a single value during the \gls{rewriting} process.
|
|
At that point it can be treated as a \parameter{}.
|
|
To ensure the correct version of the function is used, functions are changed to, at runtime, check if a \variable{} is \gls{fixed} and, if so, dispatch to the \parameter{} version of the function.
|
|
If we, for example, have a \minizinc{} function \mzninline{f} that is overloaded on \mzninline{var int} and \mzninline{int}, then the \microzinc{} transformation can be described by the following two functions.
|
|
|
|
\begin{mzn}
|
|
function f_int(int: x) = /* original body */;
|
|
function f_varint(var int: x) =
|
|
if is_fixed(x) then
|
|
f_int(fix(x))
|
|
else
|
|
/* original body */;
|
|
endif;
|
|
\end{mzn}
|
|
|
|
\item Transform all function definitions so that they do not refer to \variables{} and \parameters{} defined outside the scope of the function.
|
|
Instead, they are added as extra arguments to the function definition and each call.
|
|
|
|
\item Move all top-level \variable{} declarations and \constraints{} into a let expression in the body of a new function called \mzninline{main}.
|
|
The arguments to this function are the top-level \parameters{} of the \minizinc{} model, and it returns a fresh Boolean \variable{}.
|
|
|
|
\end{enumerate}
|
|
|
|
\begin{example}
|
|
|
|
Consider the \minizinc{} model in \cref{lst:rew-pigeon-mzn}.
|
|
It describes a simple \gls{unsat} ``pigeonhole problem'': trying to assign \(n\) pigeons to \(n-1\) holes.
|
|
|
|
The translation to \microzinc{} turns all expressions into function calls, replaces the special generator syntax in the \mzninline{forall} with an \gls{array} \gls{comprehension}, and creates the \mzninline{main} function.
|
|
The result of this translation is shown in \cref{lst:rew-pigeon-uzn}.
|
|
|
|
\pagebreak{}
|
|
For an \instance{} of the \cmodel{}, we can then create a simple \nanozinc{} program that calls \mzninline{main}.
|
|
For example for \(n=10\), we would create the following \nanozinc{} program.
|
|
|
|
\begin{nzn}
|
|
constraint main(10);
|
|
\end{nzn}
|
|
\codeendsexample{}
|
|
\end{example}
|
|
|
|
\begin{listing}
|
|
\mznfile{assets/listing/rew_pigeon_mzn.mzn}
|
|
\caption{\label{lst:rew-pigeon-mzn} A \minizinc{} model of the pigeonhole problem.}
|
|
\end{listing}
|
|
|
|
|
|
\begin{listing}
|
|
\mznfile{assets/listing/rew_pigeon_uzn.mzn}
|
|
\caption{\label{lst:rew-pigeon-uzn} The \microzinc{} translation of the pigeonhole problem in \cref{lst:rew-pigeon-mzn}.}
|
|
\end{listing}
|
|
|
|
\subsection{Partial Evaluation of \glsentrytext{nanozinc}}\label{sub:rew-partial}
|
|
|
|
Each call in a \nanozinc{} program is either a call to a \gls{native} \constraint{}, or it has a corresponding \microzinc{} function definition.
|
|
The goal of partial evaluation is to rewrite the \nanozinc{} program into a \gls{slv-mod}, i.e., a program where all calls are calls to \gls{native} \constraints{}.
|
|
|
|
To achieve this, we define the semantics of \microzinc{} as a \gls{rewriting} system that produces \nanozinc{} calls.
|
|
Each non-\gls{native} call in a \nanozinc{} program can then be replaced with the result of evaluating the corresponding \microzinc{} function.
|
|
|
|
A key element of this \gls{rewriting} process, then, is the transformation of functional expressions into relational form.
|
|
For this to happen, the \gls{rewriting} process introduces fresh \variables{} to represent intermediate expressions.
|
|
|
|
\begin{example}\label{ex:rew-abs}
|
|
Consider the (reasonably typical) \minizinc{} encoding for the absolute value function presented in \cref{lst:rew-abs}.
|
|
When an occurrence of \mzninline{abs} is encountered, the call will be replaced by a \variable{} \mzninline{z}.
|
|
But before that can occur, the \variable{} must be introduced, and the \constraint{} \mzninline{int_abs(x, z)} is added to the model, enforcing its value.
|
|
\end{example}
|
|
\begin{listing}
|
|
\mznfile{assets/listing/rew_abs.mzn}
|
|
\caption{\label{lst:rew-abs} A \minizinc{} definition for the absolute value function.}
|
|
\end{listing}
|
|
|
|
The function \mzninline{abs(x)} above is a total function: for every value of \mzninline{x}, there is always exactly one valid value of \mzninline{z}.
|
|
In this case, the \constraint{} introduced in the \gls{let} may be enforced globally, and multiple occurrences of \mzninline{abs(x)} may be replaced with the same \mzninline{z}.
|
|
However, the introduced \mzninline{int_abs} \constraint{} is only needed so long as any other \constraint{} refers to \mzninline{z}.
|
|
If \mzninline{z} is unused in the rest of the model, both \mzninline{z} and the \mzninline{int_abs} \constraint{} can be removed.
|
|
|
|
As we shall see in \cref{sec:rew-simplification}, certain optimizations and simplifications during the evaluation can lead to many expressions becoming unused.
|
|
It is therefore important to track which \constraints{} were merely introduced to define results of function calls.
|
|
In order to track these dependencies, \nanozinc{} attaches \constraints{} that define a variable to the item that introduces the \variable{}.
|
|
|
|
\subsection{\glsentrytext{nanozinc}}\label{sec:rew-nanozinc}
|
|
|
|
A \nanozinc{} program (\cref{fig:rew-nzn-syntax}) consists of a topologically-ordered list of declarations of \variables{} and \constraints{}.
|
|
\Variables{} are declared with an identifier, a domain, and are associated with a list of attached \constraints{}.
|
|
\Constraints{} can also occur at the top-level of the \nanozinc{} program.
|
|
These are said to be the \rootc{}-context \constraints{} of the \cmodel{}, i.e., those that have to hold globally and are not just used to define an \gls{avar}.
|
|
Only root-context \constraints{} can effectively constrain the overall problem.
|
|
In \microzinc{} these \constraints{} must originate from \constraint{} items in the generated \mzninline{main} function.
|
|
\Constraints{} attached to \variables{} originate from function calls, and since all functions are guaranteed to be total, attached \constraints{} can only define the function result.
|
|
|
|
\begin{example}\label{ex:rew-absnzn}
|
|
|
|
Consider the following \minizinc{} fragment.
|
|
|
|
\begin{mzn}
|
|
constraint abs(x) > y;
|
|
\end{mzn}
|
|
|
|
\noindent{}If we assume that \mzninline{x} and \mzninline{y} have a \domain{} of \mzninline{-10..10}, then after \gls{rewriting} it would result in the following resulting \nanozinc{} program.
|
|
|
|
\begin{nzn}
|
|
var -10..10: x;
|
|
var -10..10: y;
|
|
var int: z;
|
|
↳ constraint int_abs(x, z);
|
|
constraint int_gt(z, y);
|
|
\end{nzn}
|
|
|
|
Evaluating the call \mzninline{abs(x)} introduces a new \variable{} \mzninline{z} (with unrestricted domain) and the \mzninline{int_abs} \constraint{} that is used to define \mzninline{z}.
|
|
The top-level \constraint{} \mzninline{abs(x) > y} is rewritten into \mzninline{int_gt(z, y)} and added as a top-level \constraint{}.
|
|
\end{example}
|
|
|
|
\subsection{Rewriting Rules}
|
|
|
|
The core of the proposed \minizinc{} architecture is an abstract machine that rewrites \nanozinc{} items using the corresponding \microzinc{} function definitions.
|
|
We can now formally define the rewriting rules for this abstract machine.
|
|
|
|
The full set of rules appears in \cref{fig:rew-rewrite-to-nzn-calls,fig:rew-rewrite-to-nzn-let,fig:rew-rewrite-to-nzn-other}.
|
|
To simplify presentation, we assume that all rules that introduce new identifiers into the \nanozinc{} program do so in a way that ensures those identifiers are fresh (i.e., not used in the rest of the \nanozinc{} program), by suitable alpha renaming.
|
|
We also present our rules using a \emph{call by name} evaluation strategy, i.e., the arguments to function calls are substituted into function body.
|
|
As such, they are only evaluated when required for the result of the function.
|
|
Although pure \microzinc{} behaves the same under any call evaluation strategy, in implementation a \emph{call by value} strategy can provide more predictable behaviour with debugging functions in the \minizinc{} language.
|
|
It 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.
|
|
|
|
\begin{figure*}[p]
|
|
\centering
|
|
\begin{prooftree}
|
|
\hypo{\texttt{function} ~t\texttt{:}~\ptinline{F(\(p_1, \ldots{}, p_k\)) = E;} \in{} \Prog{} \text{~where the~} p_i \text{~are fresh}}
|
|
\infer[no rule]1{\Sem{\(\ptinline{E}_{[p_i \mapsto a_i, \forall{} 1 \leq{} i \leq{} k]}\)}{\Prog, \Env} \Rightarrow{} \tuple{v, \Env'}}
|
|
\infer1[(Call)]{\Sem{F(\(a_1, \ldots, a_k\))}{\Prog, \Env} \Rightarrow{} \tuple{v, \Env'}}
|
|
\end{prooftree} \\
|
|
\bigskip
|
|
\begin{prooftree}
|
|
\hypo{\ptinline{F} \in \text{Builtins}}
|
|
\infer1[(CallBuiltin)]{\Sem{F(\(a_1, \ldots, a_k\))}{\Prog, \Env} \Rightarrow{} \tuple{\ensuremath{\mathit{eval}(\ptinline{F}(a_1,\ldots, a_k))}, \Env}}
|
|
\end{prooftree} \\
|
|
\bigskip
|
|
\begin{prooftree}
|
|
\hypo{\texttt{function var bool:}~\ptinline{F(\(p_1, \ldots, p_k\));} \in \Prog}
|
|
\infer1[(CallNative)]{\Sem{F(\(a_1, \ldots, a_k\))}{\Prog, \Env} \Rightarrow{}
|
|
\tuple{\ensuremath{\texttt{constraint}~\ptinline{F}(a_1, \ldots, a_k), \Env}}}
|
|
\end{prooftree}
|
|
\caption{\label{fig:rew-rewrite-to-nzn-calls} Rewriting rules for partial evaluation of \microzinc{} calls to \nanozinc{}.}
|
|
\end{figure*}
|
|
|
|
The rules in \cref{fig:rew-rewrite-to-nzn-calls} handle function calls.
|
|
The first rule, (Call), evaluates a function call expression in the context of a \microzinc{} program \(\Prog{}\) and \nanozinc{} program \(\Env{}\).
|
|
The rule evaluates the function body \(\ptinline{E}\) where the formal parameters \(p_{i}\) are substituted by the call arguments \(a_{i}\).\footnote{We use \(E_{[a \mapsto b]}\) as a notation for the expression \(E\) where \(a\) is substituted by \(b\).} The result of this evaluation is the result of the function call.
|
|
|
|
The (CallBuiltin) rule applies to ``built-in'' functions that can be evaluated directly, such as arithmetic and Boolean operations on \gls{fixed} values.
|
|
The rule simply returns the result of evaluating the built-in function on the evaluated parameter values.
|
|
|
|
The (CallNative) rule applies to calls to \mzninline{var bool} functions, that describe relations, that have been marked as \constraints{} \gls{native} to the \solver{}.
|
|
Since these are directly supported by the \solver{}, they simply need to be transferred into the \nanozinc{} program.
|
|
|
|
\begin{figure*}[p]
|
|
\centering
|
|
\begin{prooftree}
|
|
\hypo{\Sem{\(\mathbf{I} \mid{} \mathbf{X}\)}{\Prog, \Env, \emptyset} \Rightarrow \tuple{x, \Env'}}
|
|
\infer1[(Let)]{\Sem{let \{ \(\mathbf{I}\) \} in \(\mathbf{X}\)}{\Prog, \Env} \Rightarrow{} \tuple{x, \Env'}}
|
|
\end{prooftree} \\
|
|
\bigskip
|
|
\begin{prooftree}
|
|
\hypo{\Sem{\(\mathbf{X}\)}{\Prog, \{ t : x \} \cup{} \Env} \Rightarrow \tuple{x, \{ t: x \} \cup{} \Env'}}
|
|
\infer1[(Item0)]{\Sem{\(\epsilon{} \mid{} \mathbf{X}\)}{\Prog, \{ t: x \}\cup{}\Env, \Ctx} \Rightarrow{} \tuple{x, \{ t: x \texttt{~↳~} \Ctx{} \} \cup{} \Env'}}
|
|
\end{prooftree} \\
|
|
\bigskip
|
|
\begin{prooftree}
|
|
\hypo{\Sem{\(C\)}{\Prog, \Env} \Rightarrow \tuple{c, \Env'}}
|
|
\hypo{\Sem{\(\mathbf{I} \mid{} \mathbf{X}\)}{\Prog, \Env', \{c\}\cup\Ctx} \Rightarrow \tuple{x, \Env''}}
|
|
\infer2[(ItemC)]{\Sem{\(\mbox{constraint}~C\texttt{;} \mathbf{I} \mid{} \mathbf{X}\)}{\Prog, \Env, \Ctx} \Rightarrow{} \tuple{x, \Env''}}
|
|
\end{prooftree} \\
|
|
\bigskip
|
|
\begin{prooftree}
|
|
\hypo{\Sem{\(\mathbf{I} \mid{} \mathbf{X}\)}{\Prog, \Env{} \cup{} \{t : x\}, \Ctx} \Rightarrow \tuple{x, \Env'}}
|
|
\infer1[(ItemT)]{\Sem{\(t\texttt{:}~x\texttt{;} \mathbf{I} \mid{} \mathbf{X}\)}{\Prog, \Env, \Ctx} \Rightarrow{} \tuple{x, \Env'}}
|
|
\end{prooftree} \\
|
|
\bigskip
|
|
\begin{prooftree}
|
|
\hypo{\Sem{\(E\)}{\Prog, \Env} \Rightarrow \tuple{v, \Env'}}
|
|
\hypo{\Sem{\(\mathbf{I}_{[x \mapsto v]} \mid{} \mathbf{X}_{[x \mapsto v]}\)}{\Prog, \Env', \Ctx} \Rightarrow{} \tuple{x, \Env''}}
|
|
\infer2[(ItemTE)]{\Sem{\(t\texttt{:}~x = E\texttt{;} \mathbf{I} \mid{} \mathbf{X}\)}{\Prog, \Env, \Ctx} \Rightarrow{} \tuple{x, \Env''}}
|
|
\end{prooftree} \\
|
|
\bigskip
|
|
\begin{prooftree}
|
|
\hypo{\Sem{\(E_{i}\)}{\Prog,\Env^{i-1}} \Rightarrow \tuple{v_{i}, \Env^{i}}, \forall{} 1 \leq{} i \leq{} k}
|
|
\infer[no rule]1{\Sem{\(\mathbf{I}_{[x_{\langle{}i\rangle} \mapsto v_{i}, \forall{} 1 \leq{} i \leq{} k]} \mid{} \mathbf{X}_{[x_{\langle{}i\rangle} \mapsto v_{i}, \forall{} 1 \leq{} i \leq{} k]}\)}{\Prog, \Env^{k}, \Ctx} \Rightarrow{} \tuple{x, \Env'}}
|
|
\infer1[(ItemTupC)]{\Sem{\( \texttt{tuple(}t_{1}, \ldots, t_{k}\texttt{):}~x = \left(E_{1}, \ldots, E_{k}\right)\)}{\Prog, \Env^{0}, \Ctx} \Rightarrow{} \tuple{x, \Env'}}
|
|
\end{prooftree} \\
|
|
\bigskip
|
|
\begin{prooftree}
|
|
\hypo{\Sem{\(E\)}{\Prog, \Env} \Rightarrow \tuple{\left(v_{\langle{}1\rangle}, \ldots, v_{\langle{}k\rangle}\right), \Env'}}
|
|
\infer[no rule]1{\Sem{\(\mathbf{I}_{[x_{i} \mapsto v_{\langle{}i\rangle}, \forall{} 1 \leq{} i \leq{} k]} \mid{} \mathbf{X}_{[x_{i} \mapsto v_{\langle{}i\rangle}, \forall{} 1 \leq{} i \leq{} k]}\)}{\Prog, \Env', \Ctx} \Rightarrow{} \tuple{x, \Env''}}
|
|
\infer1[(ItemTupD)]{\Sem{\(\left(t_{1}\texttt{:}~x_{1}, \ldots, t_{k}\texttt{:}~x_{k}\right) = E\texttt{;} \mathbf{I} \mid{} \mathbf{X}\)}{\Prog, \Env, \Ctx} \Rightarrow{} \tuple{x, \Env''}}
|
|
\end{prooftree}
|
|
\caption{\label{fig:rew-rewrite-to-nzn-let} Rewriting rules for partial evaluation of \microzinc{} \glspl{let} to \nanozinc{}.}
|
|
\end{figure*}
|
|
|
|
The rules in \cref{fig:rew-rewrite-to-nzn-let} consider \glspl{let}.
|
|
Starting from the main rule, (Let), the let items \textbf{I} are evaluated one at a time.
|
|
\Glspl{constraint} that follow from the evaluation of the let expression, by the (ItemC) rule, are collected in the third component, \(\phi{}\), of the evaluation arguments.
|
|
When all inner items have been evaluated, the captured \constraints{} are attached to the literal returned by the body of the let expression \textbf{X} in (Item0).
|
|
The (ItemT) rule handles introduction of new \variables{} by adding them to the context.
|
|
The (ItemTE) rule handles introduction of new \variables{} with a defining equation by evaluating them in the current context and substituting the name of the new \variable{} by the result of evaluation in the entire scope of the variable.
|
|
The rules (ItemTupC) and (ItemTupD) are for the construction and deconstruction of tuple objects.
|
|
We use the notation \(x_{\langle{}i\rangle}\) to mark the \(i^{\text{th}}\) member of the tuple \(x\) in our substitution notation.
|
|
|
|
\begin{figure*}
|
|
\centering
|
|
\begin{prooftree}
|
|
\hypo{x \in \langle \text{ident} \rangle}
|
|
\hypo{\{t: x \texttt{~↳~} \phi{} \} \in \Env}
|
|
\infer2[(Ident)]{\Sem{\(x\)}{\Prog, \Env} \Rightarrow{} \tuple{x, \Env}}
|
|
\end{prooftree} \\
|
|
\bigskip
|
|
\begin{prooftree}
|
|
\hypo{c \text{~constant}}
|
|
\infer1[(Const)]{\Sem{\(c\)}{\Prog, \Env} \Rightarrow{} \tuple{c, \Env}}
|
|
\end{prooftree} \\
|
|
\bigskip
|
|
\begin{prooftree}
|
|
\hypo{\Sem{\(x\)}{\Prog, \Env} \Rightarrow \tuple{[x_{n}, \ldots, x_{m}], \Env'}}
|
|
\hypo{\Sem{\(i\)}{\Prog, \Env'} \Rightarrow \tuple{v, \Env''}}
|
|
\hypo{v \in [n \ldots{} m]}
|
|
\infer3[(Access)]{\Sem{\(x\texttt{[}i\texttt{]}\)}{\Prog, \Env} \Rightarrow{} \tuple{x_{v}, \Env''}}
|
|
\end{prooftree} \\
|
|
\bigskip
|
|
\begin{prooftree}
|
|
\hypo{\Sem{\(C\)}{\Prog, \Env} \Rightarrow \tuple{\ptinline{true}, \_}}
|
|
\infer1[(If\(_T\))]{\Sem{if \(C\) then \(E_t\) else \(E_e\) endif}{\Prog, \Env} \Rightarrow{} \Sem{\(E_t\)}{\Prog, \Env}}
|
|
\end{prooftree} \\
|
|
\bigskip
|
|
\begin{prooftree}
|
|
\hypo{\Sem{\(C\)}{\Prog, \Env} \Rightarrow \tuple{\ptinline{false}, \_}}
|
|
\infer1[(If\(_F\))]{\Sem{if \(C\) then \(E_t\) else \(E_e\) endif}{\Prog, \Env} \Rightarrow{} \Sem{\(E_e\)}{\Prog, \Env}}
|
|
\end{prooftree} \\
|
|
\bigskip
|
|
\begin{prooftree}
|
|
\hypo{\Sem{G}{\Prog,\Env} \Rightarrow \tuple{ \ptinline{true}, \_}}
|
|
\hypo{\Sem{\(E\)}{\Prog, \Env} \Rightarrow \tuple {v, \Env'}}
|
|
\infer2[(WhereT)]{\Sem{\([E ~|~ \mbox{where~} G]\)}{\Prog, \Env} \Rightarrow{} \tuple{[v], \Env'}}
|
|
\end{prooftree} \\
|
|
\bigskip
|
|
\begin{prooftree}
|
|
\hypo{\Sem{G}{\Prog,\Env} \Rightarrow \tuple{\ptinline{false}, \_}}
|
|
\infer1[(WhereF)]{\Sem{\([E ~|~ \mbox{where~} G]\)}{\Prog, \Env} \Rightarrow{} \tuple{[], \Env}}
|
|
\end{prooftree} \\
|
|
\bigskip
|
|
\begin{prooftree}
|
|
\hypo{\Sem{\(\mathit{PE}\)}{\Prog,\Env} \Rightarrow \tuple{S, \_}}
|
|
\infer[no rule]1{\Sem{\([E ~|~ \mathit{GE} \mbox{~where~} G]\)}{\Prog, \Env_{[x \mapsto{} v]}} \Rightarrow{} \tuple{A_v, \Env_{[x \mapsto{} v]} \cup{} \Env{}_{v}}, \forall{} v \in{} S }
|
|
\infer1[(ListG)]{\Sem{\([E~|~ x \mbox{~in~} \mathit{PE}, \mathit{GE} \mbox{~where~} G]\)}{\Prog, \Env} \Rightarrow{}
|
|
\tuple{\mbox{concat} [ A_v~|~v \in{} S ], \Env{} \cup{} \bigcup{}_{v \in{} S} \Env{}_{v}}}
|
|
\end{prooftree}
|
|
\caption{\label{fig:rew-rewrite-to-nzn-other} Rewriting rules for partial evaluation of other \microzinc{} expressions to \nanozinc{}.}
|
|
\end{figure*}
|
|
|
|
Finally, the rules in \cref{fig:rew-rewrite-to-nzn-other} handle the evaluation of \variables{}, constants, \glspl{conditional}, and \glspl{comprehension}.
|
|
The (Ident) rule looks up a \variable{} in the environment and returns the \variable{} itself to be used in any \constraints{}.
|
|
The (Const) rule simply returns the constant.
|
|
The (Acess) rule evaluates the \gls{array} expression \(x\) and the index \(i\).
|
|
It then returns the element from the evaluated \gls{array} chosen by the evaluated index.
|
|
Note that, in well-defined \microzinc{}, the index \(i\) must evaluate to a value within the index range of the evaluated \gls{array} \(x\).
|
|
The (If\(_T\)) and (If\(_F\)) rules evaluate the if condition and then return the result of the then or else branch appropriately.
|
|
The (WhereT) rule evaluates the guard of a where \gls{comprehension} and if \true{} returns the resulting expression in a list.
|
|
The (WhereF) rule evaluates the guard and when \false{} returns an empty list.
|
|
The (ListG) rule evaluates the iteration set \(PE\) to get its value \(S\), which must be \gls{fixed}.
|
|
It then evaluates the expression \(E\) with all the different possible values \(v \in S\) of the generator \(x\), collecting the additional \nanozinc{} definitions \(\Env_v\).
|
|
It returns the concatenation of the resulting lists with all the additional \nanozinc{} items.
|
|
|
|
\subsection{Prototype Implementation}
|
|
|
|
Our prototype implementation of the \microzinc{}/\nanozinc{} framework consists of the following components.
|
|
|
|
The \gls{compiler} translates \minizinc{} into a \gls{byte-code} encoding of \microzinc{}.
|
|
The compiler currently supports a significant subset of the full \minizinc{} language.
|
|
The missing features, such as floating point values and complex output statements, require additional engineering effort, but do not require new technology.
|
|
|
|
The \gls{interpreter} evaluates \microzinc{} \gls{byte-code} and \nanozinc{} programs based on the \gls{rewriting} system introduced in this section.
|
|
It can read \parameters{} from a file or via an \glsxtrshort{api}.
|
|
The \gls{interpreter} constructs the call to the \mzninline{main} function, and then performs the \gls{rewriting} into \gls{slv-mod} \nanozinc{}.
|
|
Memory management is implemented using reference counting, which lends itself well to the simplifications discussed in the next section.
|
|
The interpreter is written in around 3.5kLOC of C++ to enable easy embedding into applications and other programming languages.
|
|
|
|
The framework has the ability to support multiple \solvers{}.
|
|
It can pretty-print the \nanozinc{} code to standard \flatzinc{}, so that any solver currently compatible with \minizinc{} can be used.
|
|
Additionally, a direct C++ \glsxtrshort{api} can be used to connect solvers directly, in order to enable incremental solving.
|
|
We revisit this topic in \cref{ch:incremental}.
|
|
The source code for the complete system has been made available under an open-source licence, and it has been included in the experiment resources in \cref{ch:benchmarks}.
|
|
|
|
\section{NanoZinc Simplification}\label{sec:rew-simplification}
|
|
|
|
The previous section introduced the basic evaluation model of \nanozinc: each call that has a corresponding \microzinc{} definition can be rewritten into a set of calls by evaluating the \microzinc{} code.
|
|
This section looks at further steps that the system can perform in order to produce better, more compact \glspl{slv-mod}.
|
|
|
|
\subsection{Removing unused decision variables and constraints}
|
|
|
|
The most basic form of simplification is to identify \variables{} that are not used by any call, and remove them.
|
|
This is correct because the semantics of \nanozinc{} requires us to find values for all \variables{} such that all \constraints{} are \gls{satisfied} --- but if a \variable{} does not occur in any \constraint{}, we can pick any value for it.
|
|
The model without the unused \variable{} is therefore \gls{eqsat} with the original model.
|
|
|
|
Consider now the case where a \variable{} in \nanozinc{} is only used in its attached \constraints{}.
|
|
The \constraints{} directly succeeding the declaration prepended by \texttt{↳}.
|
|
|
|
\begin{example}\label{ex:rew-absreif}
|
|
|
|
The following is a slight variation on the \minizinc{} fragment in \cref{ex:rew-absnzn}.
|
|
|
|
\begin{mzn}
|
|
constraint abs(x) > y \/ c;
|
|
constraint c;
|
|
\end{mzn}
|
|
|
|
The \constraint{} \mzninline{abs(x) > y} is now used in a disjunction.
|
|
This means that instead of enforcing the \constraint{} globally, we need to create a \gls{reif}.
|
|
Following the rewriting rules, the generated \nanozinc{} code will look very similar to the code generated in \cref{ex:rew-absnzn}, but with an additional \mzninline{bool_or} \constraint{} for the disjunction.
|
|
It uses a \variable{} \mzninline{b} that will be introduced for \mzninline{abs(x) > y}.
|
|
The \gls{rewriting} of this fragment will result in the following \nanozinc{} program.
|
|
|
|
\begin{nzn}
|
|
var true: c;
|
|
var -10..10: x;
|
|
var -10..10: y;
|
|
var int: z;
|
|
↳ constraint int_abs(x, z);
|
|
var bool: b;
|
|
↳ constraint int_gt_reif(z, y, b);
|
|
constraint bool_or(b, c);
|
|
\end{nzn}
|
|
|
|
Evaluating \mzninline{constraint c} has resulted in the domain of \mzninline{c} to be \gls{fixed} to \true{}.
|
|
The disjunction now trivially holds, independent of the value of \mzninline{b}.
|
|
The \gls{reif} of \mzninline{abs(x) > y} is therefore not required.
|
|
However, the \gls{rewriting} has to choose a particular order in which arguments are evaluated, so it is always possible that it already evaluated the left-hand side before ``noticing'' that the disjunction is \gls{satisfied}.
|
|
|
|
If the system now simplifies the \constraint{} \mzninline{bool_or(b, c)} to true, then the identifier \mzninline{b} will become unused outside its attached \constraints{}.
|
|
It was only referenced from the \mzninline{bool_or} call.
|
|
Removing \mzninline{b} leads to its defining \constraint{}, \mzninline{int_gt_reif}, being removed.
|
|
This in turn means that \mzninline{z} is not referenced anywhere outside its attached \constraints{}.
|
|
It can also be removed together with its definition.
|
|
The resulting \nanozinc{} program is much more compact.
|
|
|
|
\begin{nzn}
|
|
var true: c;
|
|
var -10..10: x;
|
|
var -10..10: y;
|
|
\end{nzn}
|
|
|
|
We assume here that \mzninline{c}, \mzninline{x} and \mzninline{y} are used in other parts of the model not shown here and therefore not removed.
|
|
Note how it is crucial to exclude the attached \constraints{} when counting the usage of \variables{}.
|
|
\mzninline{int_abs(x, z)}, the \constraint{} which merely defines \mzninline{z}, would otherwise require us to keep \mzninline{z} in the \nanozinc{} program, if it were included in the count.
|
|
\end{example}
|
|
|
|
It is important to notice the difference between \constraints{} that appear at the top level and \constraints{} that appear as part of the attached \constraints{} of a \variable{}.
|
|
Top-level \constraints{} help define the problem, they are globally enforced and cannot be removed from the problem unless it can be proved that its relations are already enforced.
|
|
\Constraints{} attached to a \variable{}, on the other hand, are used to define a \variable{}.
|
|
\Constraints{} are generally attached when they stem from a functional relation, like \mzninline{abs(x)} in the example, or from a \gls{reif}, like \mzninline{abs(x) > y} when used in the disjunction with \mzninline{c}.
|
|
In this thesis we will follow the same naming standard as \minizinc{}, where a \gls{reif} of a \constraint{} has the same name as the original \constraint{} with \texttt{\_reif} appended.
|
|
|
|
\begin{example}
|
|
The importance of the use of attached \constraints{} when removing unused \variables{} and \constraints{} is demonstrated in the following \minizinc{} fragment.
|
|
|
|
\begin{mzn}
|
|
int: n;
|
|
var int: x;
|
|
function var int: f(var int: x, int: i) = let {
|
|
var int: y;
|
|
constraint y = x * i;
|
|
} in y;
|
|
constraint [f(x,i) | i in 1..n][n] == 10;
|
|
\end{mzn}
|
|
|
|
The \gls{rewriting} of this \minizinc{} model will initially create the \mzninline{n} elements for the \gls{array} \gls{comprehension}.
|
|
Each element is evaluated as a new \variable{} \mzninline{y} and a \constraint{} to ensure that \mzninline{y} is the multiplication of \mzninline{x} and \mzninline{i}.
|
|
Although \mzninline{n} variables are created, only the last \variable{} is constrained to take the value ten.
|
|
All other \variables{} can thus be removed, and the model will stay \gls{eqsat}.
|
|
|
|
In the \nanozinc{} version of this model, each of the multiplications \constraints{} will be added to the list of attached \constraints{} of its corresponding \mzninline{y} \variable{}.
|
|
When, after evaluating the \gls{array} access, all of those \variables{} except the last are detected to be unused, their removal triggers the removal of the multiplication \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{}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\@.
|
|
The \nanozinc{} system can correctly detect that the \mzninline{y} \variables{} and multiplication \constraints{} are not required.
|
|
\end{example}
|
|
|
|
\paragraph{Implementation} The removal of unused identifiers is taken care of by garbage collection in the interpreter.
|
|
Since our prototype interpreter uses reference counting, it already accurately tracks the liveness of each identifier.
|
|
|
|
\subsection{Constraint Propagation}
|
|
|
|
\Gls{propagation} is the main inference technique used in \gls{cp} \solvers{}, as discussed in \cref{subsec:back-cp}.
|
|
At its core, \gls{propagation} simplifies the internal representation of the \gls{slv-mod}: it removes inconsistent values from \variable{} \domains{}, and it may be able to detect that certain \constraints{} are subsumed, which means that they can be removed safely.
|
|
Since a \nanozinc{} program is in fact quite similar to the internal representation of \gls{cp} \solver{}, we can use \gls{propagation} to simplify \nanozinc{}.
|
|
|
|
When using \gls{propagation} for \nanozinc{} simplification, we have to carefully consider its effects.
|
|
For instance, given the \constraint{} \mzninline{x > y}, with initial \domains{} \mzninline{x in 1..10, y in 1..10}, \gls{propagation} would result in the \domains{} being tightened to \mzninline{x in 2..10, y in 1..9}.
|
|
Note, however, that this may now prevent us from removing \mzninline{x} or \mzninline{y}: even if they later become unused, the tightened \domains{} may impose a \constraint{} on their \variables{}.
|
|
When the \domain{} of a \variable{} is tighter than the \gls{bounds} given by its defining expression, the \domain{} are said to be \gls{binding}.
|
|
For instance, if \mzninline{x} is defined as \mzninline{abs(z)}, then any restriction on the \domain{} of \mzninline{x} constrains the possible values of \mzninline{z} through the \mzninline{abs} function.
|
|
We therefore need to track whether the \domain{} of a \variable{} is the result of external \constraints{}, or is the consequence of its own definition.
|
|
|
|
A further effect of \gls{propagation} is the replacement of \constraints{} by simpler versions.
|
|
A \constraint{} \mzninline{x=y+z}, where the \domain{} of \mzninline{z} has been tightened to the singleton \mzninline{0..0}, can be rewritten to \mzninline{x=y}.
|
|
Propagating the effect of one \constraint{} can thus trigger the propagation of other \constraints{}, and \constraint{} solvers typically run all \glspl{propagator} until they reach a \gls{fixpoint}.
|
|
|
|
The \nanozinc{} \gls{interpreter} applies \glspl{propagator} for the most important \constraints{}, such as linear and Boolean \constraints{}, which can lead to significant reductions in the size of the generated \gls{slv-mod}.
|
|
It has been shown previously that applying full \gls{propagation} during compilation can be beneficial \autocite{leo-2015-multipass}.
|
|
This works particularly well when the target solver requires complicated reformulations, such as linearization for \gls{mip} \solvers{} \autocite{belov-2016-linearization}.
|
|
|
|
Returning to the example above, \gls{propagation} (and other model simplifications) can result in equality \constraints{} \mzninline{x=y} being introduced.
|
|
For certain types of target \solvers{}, in particular those based on \gls{cp}, equality \constraints{} can lead to exponentially larger search trees if not detected and simplified.
|
|
Equalities therefore present a valuable opportunity for model simplification, but also pose some challenges.
|
|
|
|
Consider the simple case of \mzninline{x=y} where one of the \variables{}, say \mzninline{x}, was a top-level variable introduced by the modeller, and not defined as the result of a function call.
|
|
In that case, we can propagate the equality \constraint{} by replacing all occurrences of \mzninline{x} with \mzninline{y}, and remove the definition of \mzninline{x}.
|
|
|
|
The more complicated case for \mzninline{x=y} is when both \mzninline{x} and \mzninline{y} are the result of function calls.
|
|
For example, a \constraint{} such as \mzninline{constraint f(a)=g(b)}.
|
|
Assuming functions \mzninline{f} and \mzninline{g} are directly rewritten into relational forms \mzninline{f_rel} and \mzninline{g_rel}, the corresponding \nanozinc{} code looks as follows.
|
|
|
|
\begin{nzn}
|
|
var int: x;
|
|
↳ constraint f_rel(a, x);
|
|
var int: y;
|
|
↳ constraint g_rel(b, y);
|
|
constraint int_eq(x, y);
|
|
\end{nzn}
|
|
|
|
In this case, simply removing either \mzninline{x} or \mzninline{y} would not be correct.
|
|
This would trigger the removal of the corresponding definition \mzninline{f_rel(a, x)} or \mzninline{g_rel(b, y)}, leaving nothing to be substituted.
|
|
Rather, the \interpreter{} needs to pick one of the two definitions and promote it to top-level status.
|
|
Let us assume that the \interpreter{} decides to replace \mzninline{y} by \mzninline{x}.
|
|
\mzninline{y} is then globally replaced by \mzninline{x}, and its declaration is removed.
|
|
The \interpreter{} moves all attached \constraints{} from \mzninline{y} into the list of top-level \constraints{}, and then removes the \mzninline{int_eq} \constraint{}.
|
|
The following \nanozinc{} program would be its result.
|
|
|
|
\begin{nzn}
|
|
var int: x;
|
|
↳ constraint f_rel(a, x);
|
|
constraint g_rel(b, x);
|
|
\end{nzn}
|
|
|
|
The process of equality propagation is similar to unification in logic programming \autocite{warren-1983-wam}.
|
|
However, since equations in \minizinc{} always concern scalar variables rather than terms, we can restrict ourselves to this simple substitution scheme and leave the further checking of the resulting equalities to the target \solver{}.
|
|
|
|
\paragraph{Implementation}
|
|
|
|
\Gls{rewriting} a function call that has a \microzinc{} definition and \gls{rewriting} a \constraint{} due to \gls{propagation} are very similar.
|
|
The \interpreter{} therefore simply interleaves both forms of \gls{rewriting}.
|
|
Efficient \gls{propagation} engines ``wake up'' a \gls{propagator} only when one of its \variables{} has received an update (i.e., when its \domain{} has been shrunk).
|
|
To enable this, the \interpreter{} needs to keep a data structure linking \variables{} to the \constraints{} where they appear (in addition to the reverse links from calls to the \variables{} in their arguments).
|
|
These links do not take part in the reference counting.
|
|
|
|
Together with its current \domain{}, each \variable{} in the interpreter also contains a Boolean flag.
|
|
This flag signifies whether the \domain{} of the \variable{} is \gls{binding}.
|
|
It is set when the \domain{} of a \variable{} is tightened by a \constraint{} that is not attached to the \variable{}.
|
|
When the flag is set, the \variable{} cannot be removed, even when the reference count is zero.
|
|
This \constraint{} may then become subsumed after \gls{propagation} and can then be removed.
|
|
Its meaning is now completely captured by the \domains{} of the \variables{}.
|
|
However, if any defining \constraint{} can later determine the same, or a strictly tighter, \domain{}, then it is not \gls{binding} any longer.
|
|
It is again fully implied by its defining \constraints{}.
|
|
The flag can then be unset and the \variable{} can potentially be removed.
|
|
|
|
\subsection{Delayed Rewriting}
|
|
|
|
\Gls{propagation} can tighten \domains{} of \variables{} or even fix them to a single value.
|
|
When this happens for the arguments of a call, a more specific \gls{decomp} may become available.
|
|
As discussed in \cref{subsec:back-delayed-rew}, it is therefore important to evaluate calls when all possible information is available to create efficient \glspl{slv-mod}.
|
|
|
|
In our \microzinc{}/\nanozinc{} system, we allow functions to be annotated as potential candidates for \gls{del-rew}.
|
|
Any annotated \constraint{} is handled by the (CallNative) rule rather than the (Call) rule, which means that it is simply added as a call into the \nanozinc{} code, without evaluating its body.
|
|
When \gls{propagation} reaches a \gls{fixpoint}, all \glspl{annotation} are removed from the current \nanozinc{} program, and evaluation resumes with the function bodies.
|
|
|
|
This crucial optimization enables rewriting in multiple phases.
|
|
For example, a \cmodel{} targeted at a \gls{mip} \solver{} is rewritten into Boolean and reified \constraints{}, whose definitions are annotated to be delayed.
|
|
The \nanozinc{} program can then be fully simplified by \gls{propagation}, before the Boolean and reified \constraints{} are rewritten into \gls{native} linear \constraints{} suitable for \gls{mip}.
|
|
|
|
\begin{example}
|
|
Let us revisit the example from \cref{subsec:back-delayed-rew}.
|
|
The following \minizinc{} fragment calls a predicate that uses the ``Big M method''.
|
|
|
|
\begin{mzn}
|
|
function var int: lq_zero_if_b(var int: x, var bool: b) ::delayed =
|
|
x <= ub(x)*(1-b); % b -> x<=0
|
|
|
|
var 0..1000: x;
|
|
var bool: b;
|
|
constraint lq_zero_if_b(x, b);
|
|
constraint x <= 10;
|
|
\end{mzn}
|
|
|
|
If this fragment is processed without the \gls{del-rew}, then it will result in the following \nanozinc{}.
|
|
|
|
\begin{nzn}
|
|
var 0..100: x;
|
|
var bool: b;
|
|
constraint int_lin_le([1, 1000], [x,b], 1000);
|
|
\end{nzn}
|
|
|
|
Note, however, that if \mzninline{ub(x)} was known to be 100, then a stronger constraint could have been used.
|
|
When using \gls{del-rew}, the interpreter will instead first produce the following \nanozinc{}.
|
|
|
|
\begin{nzn}
|
|
var 0..100: x;
|
|
var bool: b;
|
|
constraint lq_zero_if_b(x, b);
|
|
\end{nzn}
|
|
|
|
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)}.
|
|
\end{example}
|
|
|
|
\subsection{Common Sub-expression Elimination}%
|
|
\label{sec:rew-cse}
|
|
|
|
As shown in \cref{subsec:back-cse}, \gls{cse} is a crucial technique to avoid duplications in a \gls{model}.
|
|
In our architecture \gls{cse} is performed on two levels.
|
|
|
|
The \microzinc{} \interpreter{} performs \gls{cse} through memoization.
|
|
It maintains a table that maps a function identifier and the call arguments to its result for each call instruction that is executed.
|
|
Before it executes a call instruction, it searches the table for an entry with identical function identifier and call arguments.
|
|
Since functions in \microzinc{} are guaranteed to be pure and total, whenever the table search succeeds, the result can be used instead of executing the call instruction.
|
|
|
|
Earlier in the process, however, the \minizinc{} to \microzinc{} \compiler{} can perform \gls{cse} as it is performed in many other programming languages.
|
|
|
|
\begin{example}
|
|
For instance, let us reconsider the following \minizinc{} fragment from \cref{ex:back-cse}.
|
|
|
|
\begin{mzn}
|
|
(abs(x)*2 >= 20) \/ (abs(x)+5 >= 15)
|
|
\end{mzn}
|
|
|
|
In this case a static \gls{compiler} analysis could detect that the same syntactical expression, \mzninline{abs(x)}, occurs twice.
|
|
Since these expressions are guaranteed to have equivalent results, this analysis could then hoist the shared expression into a \gls{let}.
|
|
|
|
\begin{mzn}
|
|
constraint let { var int: y = abs(x) } in
|
|
(y*2 >= 20) \/ (y+5 >= 15)
|
|
\end{mzn}
|
|
\codeendsexample{}
|
|
\end{example}
|
|
|
|
As such, the \compiler{} can enforce sharing of common sub-expressions before evaluation begins.
|
|
It is worth noting that, although the \gls{cse} approach based on memoization would also cover the static example above, this method can potentially avoid many dynamic table look-ups.
|
|
Since the static analysis is cheap, it is valuable to combine both approaches.
|
|
The static approach can be further improved by inlining function calls, since that may expose more calls as being syntactically equal.
|
|
|
|
\paragraph{Implementation} In the implementation of our \microzinc{} \interpreter{}, \gls{cse} directly interacts with the reference counting mechanism.
|
|
It is clear that when an expression is reused by returning it from the \gls{cse} table, this creates a new reference to that expression.
|
|
However, the entries in the \gls{cse} table should not keep the corresponding variables alive.
|
|
Otherwise, none of the \variables{} would ever become unused.
|
|
Therefore, we treat \gls{cse} entries as weak references.
|
|
They reference a \variable{}, but do not affect its liveness (i.e., increase its reference count).
|
|
If an entry is found in the \gls{cse} table with a reference count of zero, it is removed from the table and its contents are not used.
|
|
|
|
The usage of a \gls{cse} table can be costly.
|
|
The memory requirement and time spent finding entries can be significant in the overall process.
|
|
This is aggravated by the fact that \minizinc{} has many places where a function's body only contains a single call to a function that is not used anywhere else.
|
|
Although this structure offers flexibility when defining \minizinc{} libraries, it results in many \gls{cse} entries that differ only by their function identifier.
|
|
|
|
\begin{example}
|
|
For example, the definition of the \mzninline{knapsack} \gls{global} in the \minizinc{} standard library is shown in \cref{lst:rew-knapsack}.
|
|
After checking the \parameter{} arguments, the function merely returns the result of \mzninline{fzn_knapsack}.
|
|
This function is implemented in the \solver{} library to provide the implementation of the \mzninline{knapsack} \gls{global}.
|
|
The extra function layer ensures that these checks can be performed independently of the \solver{} library and that the \solver{} can make certain assumptions about the function arguments.
|
|
But because the modeller will only use \mzninline{knapsack}, it does not make sense to also create \gls{cse} entries for \mzninline{fzn_knapsack}, as it will never be used.
|
|
\end{example}
|
|
\begin{listing}
|
|
\mznfile{assets/listing/rew_knapsack.mzn}
|
|
\caption{\label{lst:rew-knapsack} The definition of \mzninline{knapsack} in the \minizinc{} standard library.}
|
|
\end{listing}
|
|
|
|
Therefore, we have added a flag to our call instruction.
|
|
This flag controls whether the call is subject to \gls{cse}.
|
|
This allows us to disable the \gls{cse} when it is guaranteed to be unnecessary.
|
|
|
|
\subsection{Constraint Aggregation}%
|
|
\label{subsec:rew-aggregation}
|
|
|
|
In our new system it is still possible to support \gls{aggregation}.
|
|
We aggregate \constraints{} by combining \constraints{} connected through attached \constraints{}, eliminating the need for \gls{avar} to which they are attached.
|
|
To aggregate a certain kind of \constraint{}, it is marked as a \gls{native} \constraint{}.
|
|
These functional definitions are kept in the \nanozinc{} program until a top-level \constraint{} is posted that uses the \variables{} to which they are attached.
|
|
Once this happens, the interpreter will employ dedicated \gls{aggregation} logic to visit the attached \constraints{} and combine them.
|
|
The top-level \gls{constraint} is then replaced by the combined \gls{constraint}.
|
|
When the \gls{avar} become unused, they will be removed using the normal mechanisms.
|
|
|
|
\begin{example} For example, let us reconsider the linear \constraint{} from \cref{ex:back-agg}: \mzninline{x + 2*y <= z}.
|
|
The constraint will result in the following \nanozinc{}.
|
|
|
|
\begin{nzn}
|
|
var int: x;
|
|
var int: y;
|
|
var int: z;
|
|
var int: i1;
|
|
↳ constraint '*'(y, 2, i1);
|
|
var int: i2;
|
|
↳ constraint '+'(x, i1, i2);
|
|
constraint '<='(i2, z);
|
|
\end{nzn}
|
|
|
|
\mzninline{*} and \mzninline{+} were marked as \gls{native} \constraints{} as they can be aggregated into a linear \constraint{}.
|
|
Their functional definitions are put in place in the \nanozinc{}, and then a top-level \mzninline{<=} \constraint{} is created.
|
|
The \interpreter{} will then recursively visit the arguments of the \constraints{}.
|
|
The \constraints{} are then combined into the following linear \constraint{}.
|
|
|
|
\begin{mzn}
|
|
constraint int_lin_le([1,2,-1], [x,y,z], 0)
|
|
\end{mzn}
|
|
\codeendsexample{}
|
|
\end{example}
|
|
|
|
\section{Experiments}\label{sec:rew-experiments}
|
|
|
|
We have created a prototype implementation of the architecture presented in the preceding sections.
|
|
It consists of a \compiler{} from \minizinc{} to \microzinc{}, and a \microzinc{} \interpreter{} producing \nanozinc{}.
|
|
The system supports a significant subset of the full \minizinc{} language; notable features that are missing are support for set and float variables, option types, and compilation of model output expressions and \glspl{annotation}.
|
|
|
|
The implementation is not optimized for performance yet, but was created as a faithful implementation of the developed concepts, in order to evaluate their suitability and provide a solid baseline for future improvements.
|
|
In the following we present experimental results on basic \gls{rewriting} performance as well as a comparison with \glspl{interpreter} of other programming languages to demonstrate the efficiency gains that are possible thanks to the new architecture.
|
|
A description of the used computational environment, \minizinc{} instances, and versioned software has been included in \cref{ch:benchmarks}.
|
|
|
|
For our first experiment, we selected 17 models from the annual \minizinc{} challenge and compiled 5 instances of each model to \flatzinc{}, using the current \minizinc{} release version 2.5.5 and the new prototype system.
|
|
In both cases we use the standard \minizinc{} library of \glspl{global} (i.e., we decompose those \constraints{} rather than using \solver{} \gls{native} \constraints{}, in order to stress-test the \gls{rewriting}).
|
|
We measured pure \gls{rewriting} time, i.e., without time required to parse and type check in version 2.5.5, and without time required for compilation to \microzinc{} in the new system (compilation is usually very fast).
|
|
Times are averages of 10 runs.
|
|
|
|
\Cref{sfig:rew-compareruntime} compares the \gls{rewriting} time for each of \instances{}.
|
|
Points below the line indicate that the new system is faster.
|
|
On average, the new system achieves a speed-up of 5.5, with every \instance{} achieving at least 2.5 speed-up and multiple \instances{} with a speed-up of over 100.
|
|
In terms of memory performance (\cref{sfig:rew-comparemem}), version 2.5.5 can sometimes still outperform the new prototype.
|
|
We have identified that the main memory bottlenecks are our currently unoptimized implementations of \gls{cse} lookup tables and argument vectors.
|
|
These are very encouraging results, given that we are comparing a largely unoptimized prototype to a mature piece of software.
|
|
|
|
\begin{figure}
|
|
\centering
|
|
\begin{subfigure}[b]{.48\columnwidth}
|
|
\centering
|
|
\includegraphics[width=\columnwidth]{assets/img/rew_compare_runtime}
|
|
\caption{\label{sfig:rew-compareruntime}Average run time (ms)}
|
|
\end{subfigure}%
|
|
\hspace{0.04\columnwidth}%
|
|
\begin{subfigure}[b]{.48\columnwidth}
|
|
\centering
|
|
\includegraphics[width=\columnwidth]{assets/img/rew_compare_memory}
|
|
\caption{\label{sfig:rew-comparemem}Maximum resident set size (kbytes)}
|
|
\end{subfigure}
|
|
\caption{\label{fig:4-runtime}Performance on \gls{rewriting} \minizinc{} Challenge \instances{}. \minizinc{} 2.5.5 (x-axis) vs our prototype (y-axis), log-log plot. Dots below the line indicate the new system is better.}
|
|
\end{figure}
|
|
|
|
Our second experiment considers three well-known computational recursive functions: Ackermann, Fibonacci, and Takeuchi.
|
|
These functions are often used as a benchmark for implementations of functional programming languages.
|
|
Since the \minizinc{} language includes a strong functional programming component, we use these same functions as a benchmark for our prototype \interpreter{}.
|
|
In addition to \minizinc{} 2.5.5, we also compare our \interpreter{} to Python 3.8.5 \autocite{rossum-2009-python3} and OCaml 4.10.0 \autocite{leroy-2020-ocaml}.
|
|
The chosen function arguments try to exercise the \glspl{interpreter}, but without running into their limitations.
|
|
Times are averages of 1000 runs.
|
|
|
|
The results of the experiment are shown in \cref{fig:rew-interpreter-comp}.
|
|
For all experiments there is a clear ordering in the results:
|
|
\begin{itemize}
|
|
\item OCaml is the clear winner, always at least five times faster than its closest competitor;
|
|
\item our prototype finishes in second place;
|
|
\item Python is a close third, with only a significant difference compared to our prototype on the Ackermann benchmark; and
|
|
\item \minizinc{} 2.5.5 always finishes last out of the four interpreters with significant overhead over all other competitors.
|
|
\end{itemize}
|
|
Our prototype performs well in this test.
|
|
It 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.
|
|
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}
|
|
|
|
\pagebreak{}
|
|
\section{Summary}%
|
|
\label{sec:rew-summary}
|
|
|
|
This chapter presented a new architecture for \gls{rewriting} \minizinc{} \instances{} to \glspl{slv-mod}.
|
|
We introduced the intermediate languages \microzinc{} and \nanozinc{}, which are central to the \gls{rewriting} architecture.
|
|
\minizinc{} is transformed into a set of \microzinc{} definitions and a \nanozinc{} program.
|
|
Then, a \nanozinc{} program is partially evaluated using \microzinc{} definitions.
|
|
We presented formal \gls{rewriting} rules applied during this partial evaluation.
|
|
|
|
Continuously applying these rules would result in a correct, but inefficient \gls{slv-mod}.
|
|
Therefore, 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{}.
|
|
Crucially, the system can correctly remove all unused and irrelevant \variables{} and \constraints{} by \nanozinc{}'s mechanism to attach \constraints{} to the \variable{} they define.
|
|
The prototype of this architecture is shown to be significantly faster than the current implementation of \minizinc{}.
|
|
|
|
The next chapter further extends the architecture to better reason about \gls{reif}, to fully avoid it or use \gls{half-reif} where possible.
|