diff --git a/assets/shorthands.tex b/assets/shorthands.tex index 810591e..c5809f6 100644 --- a/assets/shorthands.tex +++ b/assets/shorthands.tex @@ -1,5 +1,5 @@ \newcommand{\eg}{e.g.,\xspace{}} -\newcommand{\ie}{e.g.,\xspace{}} +\newcommand{\ie}{i.e.,\xspace{}} \newcommand{\flatzinc}{\gls{flatzinc}\xspace{}} \newcommand{\microzinc}{\gls{microzinc}\xspace{}} \newcommand{\minisearch}{\gls{minisearch}\xspace{}} diff --git a/chapters/4_rewriting.tex b/chapters/4_rewriting.tex index d6f0627..eaac2a4 100644 --- a/chapters/4_rewriting.tex +++ b/chapters/4_rewriting.tex @@ -196,11 +196,10 @@ The translation from \minizinc\ to \microzinc\ involves the following steps: \subsection{Partial Evaluation of \glsentrytext{nanozinc}}\label{sub:4-partial} -Each call in a \nanozinc\ program is either a primitive, or it has a -corresponding \microzinc\ definition. The goal of partial evaluation is to -transform the \nanozinc\ program into (essentially) \flatzinc, i.e., a program -where all calls are either solver-level constraint primitives, or defining -variables. +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. 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 @@ -254,7 +253,7 @@ list of definitions. Each definition binds a variable to the result of a call or another variable, and it is associated with a list of identifiers of auxiliary constraints. The \nanozinc\ model contains a special definition \mzninline{true}, containing all ``root-context'' constraints of the model, -i.e., those that have to hold globally and are not just used to define an +\ie\ those that have to hold globally and are not just used to define an auxiliary variable. Only root-context constraints (attached to \mzninline{true}) can effectively constrain the overall problem. Constraints attached to definitions originate from function calls, and since all functions are @@ -281,17 +280,10 @@ result. constraint int_gt(z, y); \end{nzn} - \jip{Adjust text to match the new \nanozinc\ formatting.} - The variables \mzninline{x} and \mzninline{y} result in identifiers bound to - the special built-in \mzninline{mkvar}, which records the variable's domain in - its arguments. 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}, bound to a fresh identifier - \mzninline{b0}. A fresh identifier \mzninline{t} is introduced to capture both - the result \mzninline{z} as well as the list of defining constraints, - \mzninline{[b0]}. The top-level constraint \mzninline{abs(x) > y} is rewritten - into \mzninline{int_gt(t,y)} and bound to fresh identifier \mzninline{b1}, - which is added to the root-context definition \mzninline{true}. + 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} @@ -311,7 +303,7 @@ suitable alpha renaming. \begin{figure*} \centering \begin{prooftree} - \hypo{\ptinline{F(\(p_1, \ldots{}, p_k\)) = E;} \in{} \Prog{} \text{~where the~} p_i \text{~are fresh}} + \hypo{\texttt{function} ~t\texttt{:}~\ptinline{F(\(p_1, \ldots{}, p_k\)) = E;} \in{} \Prog{} \text{~where the~} p_i \text{~are fresh}} \infer[no rule]1{\Sem{E}{\Prog, \Env_{[p_i \mapsto a_i, \forall{} 1 \leq{} i \leq{} k]}} \Rightarrow \tuple{v, \Env'}} \infer1[(Call)]{\Sem{F(\(a_1, \ldots, a_k\))}{\Prog, \Env} \Rightarrow{} \tuple{v, \Env'_{[a_i \mapsto p_i, \forall{} 1 \leq{} i \leq{} k]}}} \end{prooftree} \\ @@ -322,7 +314,7 @@ suitable alpha renaming. \end{prooftree} \\ \bigskip \begin{prooftree} - \hypo{\ptinline{F(\(p_1, \ldots, p_k\));} \in \Prog} + \hypo{\texttt{predicate}~\ptinline{F(\(p_1, \ldots, p_k\));} \in \Prog} \infer1[(CallPredicate)]{\Sem{F(\(a_1, \ldots, a_k\))}{\Prog, \Env_0} \Rightarrow \tuple{\texttt{constraint~} \text{F}(v_1, \ldots, v_k), \Env_k}} \end{prooftree} @@ -541,8 +533,8 @@ prepended by \texttt{└── }). (we will come back to this in \cref{sec:4-cse}). Following the rewriting rules, the generated \nanozinc\ code will look very similar to the code generated in \cref{ex:4-absnzn}, but with an additional \mzninline{bool_or} - constraint for the disjunction, which uses the variable \mzninline{b1} that - was introduced for \mzninline{abs(x) > y}: + constraint for the disjunction, which uses a variable \mzninline{b} that will + be introduced for \mzninline{abs(x) > y}: \begin{nzn} var true: c; @@ -550,24 +542,26 @@ prepended by \texttt{└── }). var -10..10: y; var int: z; └── constraint int_abs(x, z); - var bool: b1; - └── constraint int_gt(z, y); - constraint bool_or(b1, c); + var bool: b; + └── constraint int_gt_reif(z, y, b); + constraint bool_or(b, c); \end{nzn} - Since \mzninline{c} is bound to \mzninline{true}, the disjunction - \mzninline{b2} trivially holds, independent of the value of \mzninline{b1}. - 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} 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. - If the system now simplifies the constraint \mzninline{b2} to \mzninline{true}, - the identifier \mzninline{b1} will become unused, since it was only - referenced from the \mzninline{bool_or} call. Removing \mzninline{b1} leads - to \mzninline{t} not being used by any constraint, so its definition can be - removed. This in turn means that \mzninline{b0} is not referenced anywhere - and can be removed, and then \mzninline{z}. The resulting \nanozinc\ program + If the system now simplifies the constraint \mzninline{bool_or(b, c)} to + \mzninline{true}, the identifier \mzninline{b} will become unused outside of + 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. The resulting \nanozinc\ program is much more compact: \begin{nzn} @@ -580,35 +574,35 @@ prepended by \texttt{└── }). other parts of the model not shown here and therefore not removed. \end{example} -\jip{adjust text to match the new \nanozinc\ syntax} -Note how \mzninline{t} acts as a unique name for the result of the let -expression (and thus the function call) --- we could not simply have used -\mzninline{z}, because then \mzninline{b0} would have kept \mzninline{z} alive. +Note how 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 worth noting the difference between the constraints \mzninline{b0} and -\mzninline{b1} in this example: \mzninline{b0} is referenced from the auxiliary -constraint list of another variable. This means that it is a constraint that -defines the value of a variable, and it can be enforced globally (it must hold, -under all circumstances). On the other hand, \mzninline{b1} is referenced as an -argument to the \mzninline{bool_or} call. This means that the constraint does -not have to hold globally --- rather, we require the variable \mzninline{b1} to -reflect whether the constraint holds or not, so that the \mzninline{bool_or} -can implement the disjunction. These types of constraints are typically called -\emph{reified} in constraint modelling. So \nanozinc\ uses the same syntax for -reified and globally true constraints, allocating an identifier (such as -\mzninline{b0} or \mzninline{b1}) for any constraint. Whether the constraint is -reified or not depends on where that identifier appears. +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. \begin{example} The importance of the use of auxiliary definitions when removing dead variables and constraints is demonstrated in the following example: \begin{mzn} - int n; + int: n; var int: x; function var int: f(var int: x, int: i) = let { var int: y; - constraint y = int_minus(x, i); + constraint y = x div i; } in y; constraint [f(x,i) | i in 1..n][1] == 10; \end{mzn} @@ -616,22 +610,22 @@ reified or not depends on where that identifier appears. 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 - subtraction 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. + 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. - In the \nanozinc\ version of this model, each of the subtraction constraints - will be added to the list of auxiliary constraints of its corresponding + 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. - For this example the current \minizinc\ compiler, version 2.3.2, will produce + 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 subtraction. + 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, only 1 variable, \mzninline{x}, and 1 constraint, - \mzninline{10 = int_minus(x,1);} is produced. + \mzninline{constraint int_minus(x,1,10);} is produced. \end{example} \paragraph{Implementation} The removal of unused identifiers is taken care of @@ -737,7 +731,7 @@ Rewriting a function call that has a \microzinc\ definition and rewriting a constraint due to propagation are very similar. The interpreter therefore simply interleaves both forms of rewriting. Efficient constraint propagation engines ``wake up'' a constraint only when one of its variables has received an update -(i.e., when its domain has been shrunk). To enable this, the interpreter needs +(\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. @@ -746,14 +740,14 @@ arguments). These links do not take part in the reference counting. Adding constraint propagation and simplification into the rewriting system means that the system becomes non-confluent, and some orders of execution may produce -``better'', i.e., more compact or more efficient, \nanozinc. +``better'', \ie\ more compact or more efficient, \nanozinc. \begin{example} The following example is similar to code found in the \minizinc\ libraries of MIP solvers. \begin{mzn} - predicate lq_zero_if_b(var int: x, var bool: b) = + function var int: lq_zero_if_b(var int: x, var bool: b) = x <= ub(x)*(1-b); \end{mzn} @@ -890,7 +884,7 @@ and the evaluation will proceed as normal with the root context constraint. Consider the fragment: \begin{mzn} - predicate p(var int: x, var int: y) = q(x) /\ r(y); + function var bool: p(var int: x, var int: y) = q(x) /\ r(y); constraint b0 <-> q(x); constraint b1 <-> t(x,y); constraint b1 <-> p(x,y); @@ -900,14 +894,14 @@ and the evaluation will proceed as normal with the root context constraint. \mzninline{q(x)} for the original call. Suppose processing the second constraint we discover \mzninline{t(x,y)} is \mzninline{true}, setting \mzninline{b1}. When we process \mzninline{q(x)} in the call - \mzninline{t(x,y)} we find it is the root context. So CSE needs to set + \mzninline{t(x,y)} we find it is the root context. So CSE needs to set \mzninline{b0} to \mzninline{true}. \end{example} \minizinc\ distinguishes not only between root and reified contexts, but in addition recognises constraints in \emph{positive} contexts, also known as -\emph{half-reified} \autocite{feydy-2011-half-reif}. We omit the details here -for brevity, but the CSE approach generalises to this extension. +\emph{half-reified} \autocite{feydy-2011-half-reif}. A full explanation and +discussion of half-reification can be found in \cref{ch:half_reif}. \section{Experiments}\label{sec:4-experiments} @@ -932,9 +926,9 @@ gains that are possible thanks to the new architecture. As a first experiment, we selected 20 models from the annual \minizinc\ challenge and compiled 5 instances of each model to \flatzinc, using the current \minizinc\ release version 2.4.3 and the new prototype system. In both cases we -use the standard \minizinc\ library of global constraints (i.e., we decompose +use the standard \minizinc\ library of global constraints (\ie\ we decompose those constraints rather than using solver built-ins, in order to stress-test -the flattening). We measured pure flattening time, i.e., without time required +the flattening). We measured pure flattening time, \ie\ without time required to parse and typecheck in version 2.4.3, and without time required for compilation to \microzinc\ in the new system (compilation is usually very fast). Times are averages of 10 runs.\footnote{All models obtained from