From 346945830765562eba9ccd992237ca66c8f37156 Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Fri, 21 May 2021 14:47:36 +1000 Subject: [PATCH] Small fixes --- .chktexrc | 1 + chapters/3_rewriting.tex | 53 ++++++++++++++++++++-------------------- 2 files changed, 28 insertions(+), 26 deletions(-) diff --git a/.chktexrc b/.chktexrc index 4d951e1..e374786 100644 --- a/.chktexrc +++ b/.chktexrc @@ -2,3 +2,4 @@ VerbEnvir { pgfpicture tikzpicture mzn nzn plain grammar proof } MathCmd { \hypo } WipeArg { \mzninline:{} \nzninline:{} \Sem:{} \texttt:{} } +CmdLine { -n21 } diff --git a/chapters/3_rewriting.tex b/chapters/3_rewriting.tex index 0c2db90..0b7925f 100644 --- a/chapters/3_rewriting.tex +++ b/chapters/3_rewriting.tex @@ -155,8 +155,9 @@ The translation from \minizinc\ to \microzinc{} involves the following steps: \mzninline{int_plus(x,y)}. As mentioned above, more complex rules for rewriting conditionals with variables, such as \mzninline{if x then A else B endif} and \mzninline{A[x]} where \mzninline{x} is a variable, - are also replaced by function calls (\eg\ \mzninline{if_then_else([x, - true], [A, B])} and \mzninline{element(a, x)} respectively). + are also replaced by function calls (\eg\ + \mzninline{if_then_else([x, true], [A, B])} and + \mzninline{element(a, x)} respectively). \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 @@ -432,7 +433,7 @@ suitable alpha renaming. The rules in \cref{fig:4-rewrite-to-nzn-calls} handle function calls. The first rule (Call) evaluates a function call expression in the context of a \microzinc\ -program \(\Prog\) and \nanozinc\ program \(\Env\). The rule evaluates the +program \(\Prog{}\) and \nanozinc\ program \(\Env{}\). The rule evaluates the function body \(\ptinline{E}\) where the formal parameters \(p_{i}\) are substituted by the call arguments \(a_{i}\).\footnote{We use \(E_{[a \mapsto b]}\) as a notation for the expression \(E\) where \(a\) is @@ -656,8 +657,8 @@ prepended by \texttt{↳}). 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 + 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. @@ -895,7 +896,7 @@ for MIP\@. \subsection{Common Sub-expression Elimination}\label{sec:4-cse} -\jip{Adjust with the background section. Just needs to talk about microzinc optimisation.} +\jip{Adjust with the background section. Just needs to talk about \microzinc{} optimisation.} The simplifications introduced above remove definitions from the model when we can detect that they are no longer needed. In some cases, it is even possible to @@ -958,27 +959,27 @@ 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. -\jip{TODO: \gls{cse} will be discussed in the background. How can we make this +\jip{TODO:\ \gls{cse} will be discussed in the background. How can we make this more specific to how it works in \nanozinc{}.} \paragraph{Reification} -\jip{Adjust with information in the background section. Is there anything specific to the microzinc/nanozinc system?} +\jip{Adjust with information in the background section. Is there anything specific to the \microzinc{}/\nanozinc{} system?} Many constraint modelling languages, including \minizinc{}, not only enable -constraints to be globally enforced, but typically also support constraints to -be \emph{reified} into a Boolean variable. Reification means that a variable -\mzninline{b} is constrained to be true if and only if a corresponding -constraint \mzninline{c(...)} holds. We have already seen reification in -\cref{ex:4-absreif}: the truth of constraint \mzninline{abs(x) > y} was bound to -a Boolean variable \mzninline{b1}, which was then used in a disjunction. We say -that the same constraint can be used in \emph{root context} as well as in a -\emph{reified context}. In \minizinc{}, almost all constraints can be used in both -contexts. However, reified constraints are often defined in the library in terms -of complicated decompositions into simpler constraints, or require specialised -algorithms in the target solvers. In either case, it can be very beneficial for -the efficiency of the generated \nanozinc\ program if we can detect that a -reified constraint is in fact not required. +\constraints{} to be globally enforced, but typically also support +\constraints{} to be \emph{reified} into a Boolean variable. Reification means +that a variable \mzninline{b} is constrained to be true if and only if a +corresponding constraint \mzninline{c(...)} holds. We have already seen +reification in \cref{ex:4-absreif}: the truth of constraint \mzninline{abs(x) > + y} was bound to a Boolean variable \mzninline{b1}, which was then used in a +disjunction. We say that the same constraint can be used in \emph{root context} +as well as in a \emph{reified context}. In \minizinc{}, almost all constraints +can be used in both contexts. However, reified constraints are often defined in +the library in terms of complicated decompositions into simpler constraints, or +require specialised algorithms in the target solvers. In either case, it can be +very beneficial for the efficiency of the generated \nanozinc\ program if we can +detect that a reified constraint is in fact not required. If a constraint is present in the root context, it means that it must hold globally. If the same constraint is used in a reified context, it can therefore @@ -1018,7 +1019,7 @@ addition recognises constraints in \emph{positive} contexts, also known as \emph{half-reified} \autocite{feydy-2011-half-reif}. A full explanation and discussion of half-reification can be found in \cref{ch:half_reif}. -\jip{TODO: Reification should also be discussed in the background. How can we +\jip{TODO:\ Reification should also be discussed in the background. How can we make this more specific to how it works in \nanozinc{}.} \subsection{Constraint Aggregation}% @@ -1044,8 +1045,8 @@ operators. For example the evaluation of the linear constraint \mzninline{x + These \nanozinc\ definitions are correct, but, at least for \gls{mip} solvers, the existence of the intermediate variables is likely to have a negative impact on the \gls{solver}'s performance. These \glspl{solver} would likely perform -better had they received the linear constraint \mzninline{int_lin_le([1,2,-1], - [x,y,z], 0)} directly. Since many solvers support linear constraints, it is +better had they received the linear constraint +\mzninline{int_lin_le([1,2,-1], [x,y,z], 0)} directly. Since many solvers support linear constraints, it is often an additional burden to have intermediate values that have to be given a value in the solution. @@ -1067,7 +1068,7 @@ visit the functional definitions and combine their constraints. The top-level intermediate variables become unused, they will be removed using the normal mechanisms. -\jip{TODO: Aggregation is also part of the background. How can we make this more +\jip{TODO:\ Aggregation is also part of the background. How can we make this more specific to how it works in \nanozinc{}.} \section{Experiments}\label{sec:4-experiments} @@ -1142,7 +1143,7 @@ unoptimised prototype to a mature piece of software. \pgfplotstableread[ col sep=comma, - ]{assets/table/rew_functional.csv}\rewFuncData + ]{assets/table/rew_functional.csv}\rewFuncData{} \begin{tikzpicture} \begin{axis}[ xbar,