Dekker1/dekker-phd-thesis
Archived
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Comments from Peter

Browse Source
This commit is contained in:
Jip J. Dekker 2021-07-17 14:11:05 +10:00
parent 1771f3e6f9
commit b64b9178d8
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
1 changed files with 51 additions and 39 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

68
chapters/3_rewriting.tex
View File

@ -19,7 +19,7 @@ To create an efficient \gls{slv-mod} the \gls{rewriting} process uses many simpl
\item \gls{propagation} for known \constraints{},
\item specialised \glspl{decomp} when variables get \gls{fixed},
\item \gls{aggregation},
\item \glsxtrlong{cse},
\item common sub-expression elimination,
\item and removing \variables{} and \constraints{} that are no longer required.
\end{itemize}
@ -38,7 +38,7 @@ The process can even be made incremental: in \cref{ch:incremental} we discuss ho
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.
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{}.
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.
@ -50,7 +50,7 @@ We have developed a prototype of this tool chain, and present experimental valid
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 the transformations to be performed by the \interpreter{}.
\microzinc{} is a simple language used to define transformations to be performed by the \interpreter{}.
It is simplified subset of \minizinc{}.
The transformation are represented in the language through the use of function definitions.
A function of type \mzninline{var bool}, describing a relationship, can be defined as a \gls{native} \constraint{}.
@ -73,13 +73,15 @@ In \microzinc{} it is specifically used to mark functions that are \gls{native}
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 conditional expressions are \parameters{}.
This means that the where conditions \syntax{<exp>} in \glspl{comprehension}, the conditions \syntax{<exp>} in if-then-else expressions, and the \syntax{<literal>} index in array accesses must have \mzninline{par} type.
In \minizinc{} the use of \variables{} in these positions is allowed and these expressions are rewritten to function calls.
We will discuss how the same transformation takes place in when translating \minizinc{} to \microzinc{}.
\begin{figure}
\begin{grammar}
<model> ::= <pred-decl>*<fun-decl>*
<fun-decl> ::= "function" <type-inst>":" <ident>"(" <typing> ["," <typing>]* ")" "=" <exp>";"
\alt "function" "var" "bool" ":" <ident>"(" <typing> ["," <typing>]* ")" ";"
\alt "function" "var" "bool" ":" <ident>"(" <typing> ["," <typing>]* ")"";"
<literal> ::= <constant> | <ident>
@ -91,7 +93,7 @@ This means that the where conditions \syntax{<exp>} in \glspl{comprehension}, th
\alt <ident>"[" <literal> "]"
<item> ::= <typing> [ "=" <exp> ]";"
\alt "tuple(" <type-inst> ["," <type-inst>]* "):" <ident> = "(" <exp> ["," <exp>]* ")";
\alt "tuple(" <type-inst> ["," <type-inst>]* "):" <ident> = "(" <exp> ["," <exp>]* ")"";"
\alt "(" <typing> ["," <typing>]* ")" "=" <exp>";"
\alt "constraint" <exp>";"
@ -126,7 +128,7 @@ This will be explained in detail in \cref{sec:rew-nanozinc}.
\subsection{\glsentrytext{minizinc} to \glsentrytext{microzinc}}
The translation from \minizinc{} to \microzinc{} involves the following steps:
The translation from \minizinc{} to \microzinc{} involves the following steps.
\begin{enumerate}
@ -158,13 +160,16 @@ The translation from \minizinc{} to \microzinc{} involves the following steps:
For example, the definition of \mzninline{int_plus(x, y)} for optional types can be translated into the following function.
\begin{mzn}
function var int: int_plus(tuple(var bool, var int): x, tuple(var bool, var int): y) =
function tuple(var bool, var int): int_plus(
tuple(var bool, var int): x,
tuple(var bool, var int): y
) =
let {
(x1, x2) = x;
(y1, y2) = y;
var int: x3 = if_then_else([x1, true], [x2, 0]);
var int: y3 = if_then_else([y1, true], [y2, 0]);
var int: res = int_plus(x3, y3);
tuple(var bool, var int): res = (bool_and(x1, y1), int_plus(x3, y3));
} in res;
\end{mzn}
@ -184,7 +189,10 @@ The translation from \minizinc{} to \microzinc{} involves the following steps:
The following function 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{mzn}
function tuple(var int, var bool): element_safe(array of int: a, var int: x) =
function tuple(var bool, var int): element_safe(
array of int: a,
var int: x
) =
let {
set of int: idx = index_set(x)
var bool: total = x in idx;
@ -195,8 +203,7 @@ The translation from \minizinc{} to \microzinc{} involves the following steps:
% Otherwise, give xs the value m instead
constraint not total -> xs = m;
% element constraint that is guaranteed to be total
var res = element(a, xs);
tuple(var int, var bool): ret = (res, total);
tuple(var bool, var int): res = (total, element(a, xs));
} in ret;
\end{mzn}
@ -239,7 +246,7 @@ The translation from \minizinc{} to \microzinc{} involves the following steps:
\begin{example}
Consider the following \minizinc{} model, a simple \gls{unsat} ``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) =
@ -272,7 +279,8 @@ The translation from \minizinc{} to \microzinc{} involves the following steps:
} in root_ctx;
\end{mzn}
For an \instance of the \cmodel{}, we can then create a simple \nanozinc{} program that calls \mzninline{main}, for example for \(n=10\):
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);
@ -292,7 +300,7 @@ A key element of this \gls{rewriting} process, then, is the transformation of fu
For this to happen, the \gls{rewriting} process introduces fresh \variables{} to represent intermediate expressions.
\begin{example}\label{ex:rew-abs}
Consider the following (reasonably typical) \minizinc{} encoding for the absolute value function:
Consider the following (reasonably typical) \minizinc{} encoding for the absolute value function.
\begin{mzn}
function var int: abs(var int: x) =
@ -332,7 +340,7 @@ Only root-context \constraints{} can effectively constrain the overall problem.
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}, the resulting \nanozinc{} program could look like this:
\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;
@ -354,7 +362,7 @@ We can now formally define the rewriting rules for this abstract machine.
The full set of rules appears in \cref{fig:rew-rewrite-to-nzn-calls,fig:rew-rewrite-to-nzn-let,fig:rew-rewrite-to-nzn-other}.
To simplify presentation, we assume that all rules that introduce new identifiers into the \nanozinc{} program do so in a way that ensures those identifiers are fresh (\ie{} not used in the rest of the \nanozinc{} program), by suitable alpha renaming.
\begin{figure*}
\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}}
@ -383,10 +391,10 @@ 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 (CallNative) rule applies to calls to functions for \constraints{} \gls{native} to the \solver{}.
The (CallNative) rule applies to calls to \mzninline{var bool} functions, that describe relationships, 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*}
\begin{figure*}[p]
\centering
\begin{prooftree}
\hypo{\Sem{\(\mathbf{I} \mid{} \mathbf{X}\)}{\Prog, \Env, \emptyset} \Rightarrow \tuple{x, \Env'}}
@ -449,15 +457,15 @@ We use the notation \(x_{\langle{}i\rangle}\) to mark the \(i^{\text{th}}\) memb
\end{prooftree} \\
\bigskip
\begin{prooftree}
\hypo{\Sem{\(x\)}{\Prog, \Env} \Rightarrow \tuple{[x_{1}, \ldots, x_{n}], \Env'}}
\hypo{\Sem{\(i\)}{\Prog, \Env'} \Rightarrow \tuple{v, \Env''}}
\hypo{v \in [1 \ldots{} n]}
\infer3[(Access)]{\Sem{\(x\texttt{[}i\texttt{]}\)}{\Prog, \Env} \Rightarrow{} \tuple{x_{v}, \Env''}}
\hypo{c \text{~constant}}
\infer1[(Const)]{\Sem{\(c\)}{\Prog, \Env} \Rightarrow{} \tuple{c, \Env}}
\end{prooftree} \\
\bigskip
\begin{prooftree}
\hypo{c \text{~constant}}
\infer1[(Const)]{\Sem{\(c\)}{\Prog, \Env} \Rightarrow{} \tuple{c, \Env}}
\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}
@ -492,8 +500,11 @@ We use the notation \(x_{\langle{}i\rangle}\) to mark the \(i^{\text{th}}\) memb
\end{figure*}
Finally, the rules in \cref{fig:rew-rewrite-to-nzn-other} handle the evaluation of \variables{}, constants, conditionals and comprehensions.
The (Ident) rule looks up a \variable{} in the environment and return its fixed value (for constants) or the \variable{} itself.
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 array expression \(x\) and the index \(i\).
It then returns the element from the evaluated 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 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 comprehension and if true returns the resulting expression in a list.
The (WhereF) rule evaluates the guard and when false returns an empty list.
@ -571,7 +582,7 @@ The constraints directly succeeding the declaration prepended by \texttt{↳}.
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:
The resulting \nanozinc{} program is much more compact.
\begin{nzn}
var true: c;
@ -692,11 +703,12 @@ 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 flag is set when the \domain{} of a \variable{} is tightened by a \constraint{} that is not attached to the \variable{}.
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{}.
If, however, any defining \constraint{} further tightens the \domain{}, then it is is no longer \gls{binding}, because it is again fully implied by its defining \constraints{}.
However, if any defining \constraint{} can later determine the same, or a strictly tighter, \domain{}, then it is is no longer \gls{binding}.
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}