|
|
|
|
@ -4,20 +4,59 @@
|
|
|
|
|
|
|
|
|
|
\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.
|
|
|
|
|
Models written in \minizinc\ can be translated into \microzinc{}.
|
|
|
|
|
\Glspl{model} written in \minizinc\ can be translated into \microzinc{}.
|
|
|
|
|
|
|
|
|
|
\nanozinc{} is similar to \flatzinc\ in that it contains only simple variable declarations and flat constraints.
|
|
|
|
|
However, while all function calls in \flatzinc\ need to be solver-level primitives, \nanozinc\ calls can refer to functions implemented in \microzinc{}.
|
|
|
|
|
Furthermore, \nanozinc\ allows for constraints to be bound to a specific variable and constraints and variables declarations can be interleaved.
|
|
|
|
|
\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}.
|
|
|
|
|
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.
|
|
|
|
|
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}
|
|
|
|
|
@ -48,9 +87,7 @@ While we omit the typing rules here for space reasons, we will assume that in we
|
|
|
|
|
\caption{\label{fig:rew-uzn-syntax}Syntax of \microzinc{}.}
|
|
|
|
|
\end{figure}
|
|
|
|
|
|
|
|
|
|
\newcommand{\sep}{\rhd}
|
|
|
|
|
|
|
|
|
|
A \nanozinc\ program, defined in \cref{fig:rew-nzn-syntax}, is simply a list of variable declaration and constraints in the form of calls.
|
|
|
|
|
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}
|
|
|
|
|
@ -79,7 +116,8 @@ The translation from \minizinc\ to \microzinc{} involves the following steps:
|
|
|
|
|
|
|
|
|
|
\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, more complex rules for rewriting conditionals with \variables{}, are also replaced by function calls.
|
|
|
|
|
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}
|
|
|
|
|
@ -88,26 +126,32 @@ The translation from \minizinc\ to \microzinc{} involves the following steps:
|
|
|
|
|
|
|
|
|
|
\noindent{}And, an expression \mzninline{A[x]}, where \mzninline{x} is a \variable{}, is replaced by a call:
|
|
|
|
|
|
|
|
|
|
\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.
|
|
|
|
|
\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.
|
|
|
|
|
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 both a Boolean variable that indicates the totality with regards to the input variables and the resulting value of the function that is adjusted to return a predefined value when it would normally be undefined.
|
|
|
|
|
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}
|
|
|
|
|
|
|
|
|
|
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\ operators to write the \microzinc\ definition.}:
|
|
|
|
|
\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) =
|
|
|
|
|
@ -118,7 +162,7 @@ The translation from \minizinc\ to \microzinc{} involves the following steps:
|
|
|
|
|
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.
|
|
|
|
|
% 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);
|
|
|
|
|
@ -126,7 +170,8 @@ The translation from \minizinc\ to \microzinc{} involves the following steps:
|
|
|
|
|
} in ret;
|
|
|
|
|
\end{mzn}
|
|
|
|
|
|
|
|
|
|
Similar to the replacement of optional values, all usage of the \mzninline{element} function are replaced by \mzninline{element_safe} and the usage of its result should be guarded by the returned totality variable in the surrounding Boolean context.
|
|
|
|
|
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}
|
|
|
|
|
@ -138,10 +183,11 @@ The translation from \minizinc\ to \microzinc{} involves the following steps:
|
|
|
|
|
\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 both variable and parameter parameters.
|
|
|
|
|
And, as we will later discuss in more detail, is possible for variables to be fixed to a single value, at which point they can be treated as parameters.
|
|
|
|
|
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:
|
|
|
|
|
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 */;
|
|
|
|
|
@ -153,15 +199,15 @@ The translation from \minizinc\ to \microzinc{} involves the following steps:
|
|
|
|
|
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 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.
|
|
|
|
|
\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 unsatisfiable ``pigeonhole problem'', trying to assign \(n\) pigeons to \(n-1\) holes:
|
|
|
|
|
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) =
|
|
|
|
|
@ -174,8 +220,7 @@ The translation from \minizinc\ to \microzinc{} involves the following steps:
|
|
|
|
|
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.
|
|
|
|
|
Note how the domain \(1..n-1\) of the \mzninline{pigeon} array is replaced by a \mzninline{set_in} constraint for each element of the array.
|
|
|
|
|
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) =
|
|
|
|
|
@ -188,16 +233,12 @@ The translation from \minizinc\ to \microzinc{} involves the following steps:
|
|
|
|
|
|
|
|
|
|
function var bool: main(int: n) = let {
|
|
|
|
|
var bool: root_ctx;
|
|
|
|
|
array[range(1, n)] of var int: pigeon;
|
|
|
|
|
constraint forall([
|
|
|
|
|
set_in(element(pigeon, i), range(1, int_minus(n,1)))
|
|
|
|
|
| i in range(1, n)
|
|
|
|
|
])
|
|
|
|
|
array[1..n] of var 1..n-1: pigeon;
|
|
|
|
|
constraint all_different(pigeon);
|
|
|
|
|
} in root_ctx;
|
|
|
|
|
\end{mzn}
|
|
|
|
|
|
|
|
|
|
For a concrete instance of the model, we can then create a simple \nanozinc\ program that calls \mzninline{main}, for example for \(n=10\):
|
|
|
|
|
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);
|
|
|
|
|
@ -207,14 +248,14 @@ The translation from \minizinc\ to \microzinc{} involves the following steps:
|
|
|
|
|
|
|
|
|
|
\subsection{Partial Evaluation of \glsentrytext{nanozinc}}\label{sub:rew-partial}
|
|
|
|
|
|
|
|
|
|
Each call in a \nanozinc\ program is either a call to a solver-level predicate, or it has a corresponding \microzinc\ function definition.
|
|
|
|
|
The goal of partial evaluation is to transform the \nanozinc\ program into (essentially) \flatzinc{}, \ie\ a program where all calls are calls to solver-level predicates.
|
|
|
|
|
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 rewriting system that produces \nanozinc\ calls.
|
|
|
|
|
Each non-primitive call in a \nanozinc\ program can then be replaced with the result of evaluating the corresponding \microzinc\ function.
|
|
|
|
|
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 rewriting process, then, is the transformation of functional expressions into relational form.
|
|
|
|
|
For this to happen, the rewriting process introduces fresh variables to represent intermediate expressions, and keeps track of constraints added during the rewriting.
|
|
|
|
|
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:
|
|
|
|
|
@ -227,8 +268,8 @@ For this to happen, the rewriting process introduces fresh variables to represen
|
|
|
|
|
} 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.
|
|
|
|
|
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}.
|
|
|
|
|
@ -238,27 +279,27 @@ If \mzninline{z} is unused in the rest of the model, both \mzninline{z} and the
|
|
|
|
|
|
|
|
|
|
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.
|
|
|
|
|
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 variables declaration 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 auxiliary variable.
|
|
|
|
|
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.
|
|
|
|
|
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
|
|
|
|
|
Consider the \minizinc{} fragment
|
|
|
|
|
|
|
|
|
|
\begin{mzn}
|
|
|
|
|
constraint abs(x) > y;
|
|
|
|
|
\end{mzn}
|
|
|
|
|
|
|
|
|
|
where \mzninline{x} and \mzninline{y} have domain \mzninline{-10..10}.
|
|
|
|
|
After rewriting all definitions, the resulting \nanozinc\ program could look like this:
|
|
|
|
|
\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;
|
|
|
|
|
@ -268,17 +309,17 @@ Constraints attached to variables originate from function calls, and since all f
|
|
|
|
|
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.
|
|
|
|
|
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 performs the rewriting of \nanozinc\ items using the corresponding \microzinc\ function definitions.
|
|
|
|
|
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.
|
|
|
|
|
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
|
|
|
|
|
@ -309,8 +350,8 @@ The rule evaluates the function body \(\ptinline{E}\) where the formal parameter
|
|
|
|
|
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 solver predicates.
|
|
|
|
|
These are considered primitives, and as such simply need to be transferred into the \nanozinc\ program.
|
|
|
|
|
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
|
|
|
|
|
@ -359,9 +400,9 @@ These are considered primitives, and as such simply need to be transferred into
|
|
|
|
|
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.
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
@ -416,66 +457,66 @@ We use the notation \(x_{\langle{}i\rangle}\) to mark the \(i^{\text{th}}\) memb
|
|
|
|
|
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.
|
|
|
|
|
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 (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.
|
|
|
|
|
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.
|
|
|
|
|
Our prototype implementation of the \microzinc{}/\nanozinc{} framework consists of the following components.
|
|
|
|
|
|
|
|
|
|
The \textbf{compiler} translates \minizinc\ into a \textbf{byte code} encoding of \microzinc{}.
|
|
|
|
|
The compiler currently supports a significant subset of the full \minizinc\ language, with the missing features (such as multi-dimensional arrays and complex output statements) requiring additional engineering effort but no new technology.
|
|
|
|
|
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 \textbf{interpreter} evaluates \microzinc\ byte code and \nanozinc\ programs based on the rewrite system introduced in this section.
|
|
|
|
|
It can read parameter data from a file or via an API\@.
|
|
|
|
|
The interpreter constructs the call to the \mzninline{main} function, and then performs the rewriting into flat \nanozinc{}.
|
|
|
|
|
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 includes \textbf{interfaces} 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++ API can be used to connect solvers directly, in order to enable incremental solving.
|
|
|
|
|
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.
|
|
|
|
|
\jip{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 \nanozinc\ code.
|
|
|
|
|
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 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 equisatisfiable with the original model.
|
|
|
|
|
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{↳}).
|
|
|
|
|
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}:
|
|
|
|
|
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, the model needs to reason about whether the constraint holds or not.
|
|
|
|
|
This is called \gls{reification} (we will come back to this in \cref{sec:rew-cse}).
|
|
|
|
|
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, which uses a variable \mzninline{b} that will be introduced for \mzninline{abs(x) > y}:
|
|
|
|
|
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{reification}.
|
|
|
|
|
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;
|
|
|
|
|
@ -488,13 +529,16 @@ Consider now the case where a variable in \nanozinc\ is only used in its own aux
|
|
|
|
|
constraint bool_or(b, c);
|
|
|
|
|
\end{nzn}
|
|
|
|
|
|
|
|
|
|
Evaluating \mzninline{constraint c} will result in the domain of \mzninline{c} to be bound to \mzninline{true}, the disjunction then trivially holds, independent of the value of \mzninline{b}.
|
|
|
|
|
The constraint \mzninline{abs(x) > y} is therefore not required.
|
|
|
|
|
However, the 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.
|
|
|
|
|
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{reification} 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}, the identifier \mzninline{b} will become unused outside its auxiliary definitions, since it was only referenced from the \mzninline{bool_or} call.
|
|
|
|
|
Removing \mzninline{b} leads will also its defining constraint, \mzninline{int_gt_reif}, being removed.
|
|
|
|
|
This in turn means that \mzninline{z} is not referenced anywhere outside its auxiliary definitions and can be removed together with its definition.
|
|
|
|
|
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}
|
|
|
|
|
@ -504,43 +548,45 @@ Consider now the case where a variable in \nanozinc\ is only used in its own aux
|
|
|
|
|
\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}
|
|
|
|
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
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.
|
|
|
|
|
Constraint 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 the reflection if a constraint holds or not, like \mzninline{abs(x) > y} when used in the disjunction with \mzninline{c}.
|
|
|
|
|
These types of reflection constraints are typically called \glspl{reification}.
|
|
|
|
|
In this thesis we will follow the same naming standard as \minizinc\ where a \gls{reification} of a constraint has the same name as the original constraint with \texttt{\_reif} appended.
|
|
|
|
|
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{reification}, 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{reification} 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:
|
|
|
|
|
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;
|
|
|
|
|
constraint y = x * i;
|
|
|
|
|
} in y;
|
|
|
|
|
constraint [f(x,i) | i in 1..n][1] == 10;
|
|
|
|
|
constraint [f(x,i) | i in 1..n][n] == 10;
|
|
|
|
|
\end{mzn}
|
|
|
|
|
|
|
|
|
|
The rewriting of this instance 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 division 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 equisatisfiable.
|
|
|
|
|
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 division 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.
|
|
|
|
|
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 \flatzinc\ program that contains the variable \mzninline{x}, \mzninline{n-1} variables \mzninline{y}, and \mzninline{n} constraints for the division.
|
|
|
|
|
The first \mzninline{y} variable is directly replaced with the constant 10\@.
|
|
|
|
|
Using the \nanozinc\ system, this only produces 1 \variable{}, \mzninline{x}, and 1 \constraint{}:
|
|
|
|
|
\begin{mzn}
|
|
|
|
|
constraint int_minus(x,1,10);
|
|
|
|
|
\end{mzn}
|
|
|
|
|
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.
|
|
|
|
|
@ -550,30 +596,31 @@ Since our prototype interpreter uses reference counting, it already accurately t
|
|
|
|
|
|
|
|
|
|
\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.
|
|
|
|
|
This, in turn, offers another way that \variables{} can become unused.
|
|
|
|
|
|
|
|
|
|
When using \gls{propagation} for \nanozinc{} simplification, we do 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}, would result in the domains being tightened to \mzninline{x in 2..10, y in 1..9}.
|
|
|
|
|
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 a variable domain has been enforced through external constraints, or is the consequence of its own 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 propagation rules or algorithms until they reach a fix-point.
|
|
|
|
|
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\ interpreter applies propagation rules for the most important constraints, such as linear and Boolean constraints, which can lead to significant reductions in generated code size.
|
|
|
|
|
It has been shown previously that applying full \gls{propagation} during compilation can be beneficial \autocite{leo-2015-multipass}, in particular when the target solver requires complicated reformulations (such as linearisation for MIP solvers \autocite{belov-2016-linearisation}).
|
|
|
|
|
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 constraint programming, equality constraints can lead to exponentially larger search trees if not detected and simplified.
|
|
|
|
|
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}.
|
|
|
|
|
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 model fragment such as \mzninline{constraint f(a)=g(b)}.
|
|
|
|
|
Let us assume that part of the corresponding \nanozinc\ code looks like this:
|
|
|
|
|
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;
|
|
|
|
|
@ -583,12 +630,13 @@ Let us assume that part of the corresponding \nanozinc\ code looks like this:
|
|
|
|
|
constraint int_eq(x, y);
|
|
|
|
|
\end{nzn}
|
|
|
|
|
|
|
|
|
|
In this case, simply removing either \mzninline{x} or \mzninline{y} would not be correct, since that 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}.
|
|
|
|
|
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:
|
|
|
|
|
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;
|
|
|
|
|
@ -596,18 +644,18 @@ The resulting \nanozinc\ looks like this:
|
|
|
|
|
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 constraint solver.
|
|
|
|
|
The process of equality propagation is similar to \gls{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}
|
|
|
|
|
|
|
|
|
|
Rewriting a function call that has a \microzinc\ definition and rewriting a constraint due to \gls{propagation} are very similar.
|
|
|
|
|
The interpreter therefore simply interleaves both forms of rewriting.
|
|
|
|
|
Efficient \gls{propagation} engines ``wake up'' a constraint 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).
|
|
|
|
|
\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 \gls{domain}, each \variable{} in the interpreter also contains a Boolean flag.
|
|
|
|
|
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}.
|
|
|
|
|
@ -617,15 +665,18 @@ The flag can then be unset and the variable can potentially be removed.
|
|
|
|
|
|
|
|
|
|
\subsection{Delayed Rewriting}
|
|
|
|
|
|
|
|
|
|
If more information becomes available (though for example), a better decomposition of a call might become available.
|
|
|
|
|
\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{}.
|
|
|
|
|
As a solution to this problem, 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 (CallPrimitive) rule rather than the (Call) rule, which means that it is simply added as a call into the \nanozinc{} code, without evaluating its body.
|
|
|
|
|
|
|
|
|
|
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 model targeted at a \gls{mip} solver is rewritten into Boolean and reified constraints, whose definitions are annotated to be delayed.
|
|
|
|
|
The \nanozinc\ model can then be fully simplified by \gls{propagation}, before the Boolean and reified constraints are rewritten into lower-level linear primitives suitable for \gls{mip}.
|
|
|
|
|
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}
|
|
|
|
|
@ -636,9 +687,9 @@ 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.
|
|
|
|
|
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 form of \gls{cse} such as it is performed in many other programming languages.
|
|
|
|
|
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}
|
|
|
|
|
@ -657,14 +708,14 @@ Earlier in the process, however, the \minizinc{} to \microzinc{} \compiler{} can
|
|
|
|
|
|
|
|
|
|
\end{example}
|
|
|
|
|
|
|
|
|
|
As such, the compiler can enforce sharing of common sub-expressions before evaluation begins.
|
|
|
|
|
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.
|
|
|
|
|
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.
|
|
|
|
|
@ -672,8 +723,7 @@ If an entry is found in the \gls{cse} table with a reference count of zero, it i
|
|
|
|
|
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.
|
|
|
|
|
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.
|
|
|
|
|
@ -717,27 +767,28 @@ When the \glspl{ivar} become unused, they will be removed using the normal mecha
|
|
|
|
|
\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.
|
|
|
|
|
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.
|
|
|
|
|
\jip{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 flattening performance as well as incremental flattening and solving that demonstrate the efficiency gains that are possible thanks to the new architecture.
|
|
|
|
|
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}.
|
|
|
|
|
|
|
|
|
|
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.
|
|
|
|
|
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 \(2.3\), with very few instances not achieving any speedup.
|
|
|
|
|
In terms of memory performance (\cref{sfig:rew-comparemem}), version 2.4.3 can sometimes still outperform the new prototype.
|
|
|
|
|
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}[t]
|
|
|
|
|
\begin{figure}
|
|
|
|
|
\centering
|
|
|
|
|
\begin{subfigure}[b]{.48\columnwidth}
|
|
|
|
|
\centering
|
|
|
|
|
@ -755,16 +806,33 @@ These are very encouraging results, given that we are comparing a largely unopti
|
|
|
|
|
plot. Dots below the line indicate the new system is better.}
|
|
|
|
|
\end{figure}
|
|
|
|
|
|
|
|
|
|
\begin{figure}[ht]
|
|
|
|
|
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}
|
|
|
|
|
|
|
|
|
|
|
