diff --git a/chapters/3_rewriting.tex b/chapters/3_rewriting.tex index 3b32cf2..6d8f72b 100644 --- a/chapters/3_rewriting.tex +++ b/chapters/3_rewriting.tex @@ -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{} and \syntax{}, which can be assumed to be the same as the definition of \syntax{} and \syntax{} 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{} in \glspl{comprehension}, the conditions \syntax{} in if-then-else expressions, and the \syntax{} 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} ::= ** ::= "function" ":" "(" ["," ]* ")" "=" ";" - \alt "function" "var" "bool" ":" "(" ["," ]* ")" ";" + \alt "function" "var" "bool" ":" "(" ["," ]* ")"";" ::= | @@ -91,7 +93,7 @@ This means that the where conditions \syntax{} in \glspl{comprehension}, th \alt "[" "]" ::= [ "=" ]";" - \alt "tuple(" ["," ]* "):" = "(" ["," ]* ")"; + \alt "tuple(" ["," ]* "):" = "(" ["," ]* ")"";" \alt "(" ["," ]* ")" "=" ";" \alt "constraint" ";" @@ -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,20 +189,22 @@ 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) = - let { - set of int: idx = index_set(x) - var bool: total = x in idx; - var idx: xs; - int: m = min(idx); - % Give xs the value of x when result is total - constraint total -> xs = x; - % Otherwise, give xs the value m instead - constraint not total -> xs = m; - % element constraint that is guaranteed to be total - var res = element(a, xs); - tuple(var int, var bool): ret = (res, total); - } in ret; + 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; + var idx: xs; + int: m = min(idx); + % Give xs the value of x when result is total + constraint total -> xs = x; + % Otherwise, give xs the value m instead + constraint not total -> xs = m; + % element constraint that is guaranteed to be total + tuple(var bool, var int): res = (total, element(a, xs)); + } in ret; \end{mzn} Similar to the replacement of optional values, all occurrences of the \mzninline{element} function are replaced by \mzninline{element_safe}. @@ -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}