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

Fix rewriting chapter based on Peter's notes

Browse Source
This commit is contained in:
Jip J. Dekker 2021-06-26 14:27:57 +10:00
parent 83cc139503
commit a478c80436
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
1 changed files with 18 additions and 17 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

35
chapters/3_rewriting.tex
View File

@ -317,6 +317,12 @@ These are considered primitives, and as such simply need to be transferred into
\infer1[(Item0)]{\Sem{\(\epsilon{} \mid{} \mathbf{X}\)}{\Prog, \{ t: x \}\cup{}\Env, \Ctx} \Rightarrow{} \tuple{x, \{ t: x \texttt{~↳~} \Ctx{} \} \cup{} \Env'}}
\end{prooftree} \\
\bigskip
\begin{prooftree}
\hypo{\Sem{\(C\)}{\Prog, \Env} \Rightarrow \tuple{c, \Env'}}
\hypo{\Sem{\(\mathbf{I} \mid{} \mathbf{X}\)}{\Prog, \Env', \{c\}\cup\Ctx} \Rightarrow \tuple{x, \Env''}}
\infer2[(ItemC)]{\Sem{\(\mbox{constraint}~C\texttt{;} \mathbf{I} \mid{} \mathbf{X}\)}{\Prog, \Env, \Ctx} \Rightarrow\ \tuple{x, \Env''}}
\end{prooftree} \\
\bigskip
\begin{prooftree}
\hypo{\Sem{\(\mathbf{I} \mid{} \mathbf{X}\)}{\Prog, \Env\ \cup\ \{t : x\}, \Ctx} \Rightarrow \tuple{x, \Env'}}
\infer1[(ItemT)]{\Sem{\(t\texttt{:}~x\texttt{;} \mathbf{I} \mid{} \mathbf{X}\)}{\Prog, \Env, \Ctx} \Rightarrow{} \tuple{x, \Env'}}
@ -338,12 +344,6 @@ These are considered primitives, and as such simply need to be transferred into
\hypo{\Sem{\(E\)}{\Prog, \Env} \Rightarrow \tuple{\left(v_{\langle{}1\rangle}, \ldots, v_{\langle{}k\rangle}\right), \Env'}}
\infer[no rule]1{\Sem{\(\mathbf{I}_{[x_{i} \mapsto v_{\langle{}i\rangle}, \forall{} 1 \leq{} i \leq{} k]} \mid{} \mathbf{X}_{[x_{i} \mapsto v_{\langle{}i\rangle}, \forall{} 1 \leq{} i \leq{} k]}\)}{\Prog, \Env', \Ctx} \Rightarrow\ \tuple{x, \Env''}}
\infer1[(ItemTupD)]{\Sem{\(\left(t_{1}\texttt{:}~x_{1}, \ldots, t_{k}\texttt{:}~x_{k}\right) = E\texttt{;} \mathbf{I} \mid{} \mathbf{X}\)}{\Prog, \Env, \Ctx} \Rightarrow\ \tuple{x, \Env''}}
\end{prooftree} \\
\bigskip
\begin{prooftree}
\hypo{\Sem{\(C\)}{\Prog, \Env} \Rightarrow \tuple{c, \Env'}}
\hypo{\Sem{\(\mathbf{I} \mid{} \mathbf{X}\)}{\Prog, \Env', \{c\}\cup\Ctx} \Rightarrow \tuple{x, \Env''}}
\infer2[(ItemC)]{\Sem{\(\mbox{constraint}~C\texttt{;} \mathbf{I} \mid{} \mathbf{X}\)}{\Prog, \Env, \Ctx} \Rightarrow\ \tuple{x, \Env''}}
\end{prooftree}
\caption{\label{fig:4-rewrite-to-nzn-let} Rewriting rules for partial evaluation
of \microzinc\ let expressions to \nanozinc{}.}
@ -351,7 +351,8 @@ These are considered primitives, and as such simply need to be transferred into
The rules in \cref{fig:4-rewrite-to-nzn-let} considers let expressions.
Starting from the main rule, (Let), the let items \textbf{I} are evaluated one at a time.
When all items are evaluated the constraints generated by the (ItemC) rule will be bound to the literal returned by the body of the let expression \textbf{X} in (Item0).
\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.
The rules (ItemTupC) and (ItemTupD) are for the construction and deconstruction of tuple objects.
@ -362,7 +363,7 @@ We use the notation \(x_{\langle{}i\rangle}\) to mark the \(i^{\text{th}}\) memb
\begin{prooftree}
\hypo{x \in \langle \text{ident} \rangle}
\hypo{\{t: x \texttt{~↳~} \phi\ \} \in \Env}
\infer2[(IdX)]{\Sem{\(x\)}{\Prog, \Env} \Rightarrow{} \tuple{x, \Env}}
\infer2[(Ident)]{\Sem{\(x\)}{\Prog, \Env} \Rightarrow{} \tuple{x, \Env}}
\end{prooftree} \\
\bigskip
\begin{prooftree}
@ -411,7 +412,7 @@ We use the notation \(x_{\langle{}i\rangle}\) to mark the \(i^{\text{th}}\) memb
Finally, the rules in \cref{fig:4-rewrite-to-nzn-other} handle the evaluation of variables, constants, conditionals and comprehensions.
For completeness, we give the details here.
The (IdX) and (IdC) rules look 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.
@ -515,7 +516,7 @@ In this thesis we will follow the same naming standard as \minizinc\ where a \gl
var int: x;
function var int: f(var int: x, int: i) = let {
var int: y;
constraint y = x div i;
constraint y = x - i;
} in y;
constraint [f(x,i) | i in 1..n][1] == 10;
\end{mzn}
@ -543,7 +544,6 @@ This, in turn, may result in \mzninline{x} or \mzninline{y} becoming unused and
This is a simple form of \gls{propagation}, the main inference method used in constraint solvers \autocite{schulte-2008-propagation}.
\gls{propagation}, in general, can not only detect when constraints are trivially true (or false), but also tighten variable domains.
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}.
These tightened domains would be reflected in the corresponding \mzninline{mkvar(...)} calls.
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.
@ -584,8 +584,7 @@ The resulting \nanozinc\ looks like this:
\begin{nzn}
var int: x;
↳ constraint f_rel(a, x);
constraint g_rel(x, y);
constraint int_eq(x, y);
constraint g_rel(b, x);
\end{nzn}
The process of equality propagation is similar to unification in logic programming \autocite{warren-1983-wam}.
@ -613,7 +612,7 @@ Adding \gls{propagation} and simplification into the rewriting system means that
This predicate expresses the constraint \mzninline{b -> x<=0}, using a well-known method called ``big-M transformation''.
The expression \mzninline{ub(x)} returns a valid upper bound for \mzninline{x}, \ie\ a fixed value known to be greater than or equal to \mzninline{x}.
This could be the initial upper bound \mzninline{x} was declared with, or the current value in the corresponding \nanozinc\ \mzninline{mkvar} call.
This could be the initial upper bound \mzninline{x} was declared with, or the current upper bound of the domain changed by \constraint{} \gls{propagation}.
If \mzninline{b} takes the value 0, the expression \mzninline{ub(x)*(1-b)} is equal to \mzninline{ub(x)}, and the constraint \mzninline{x <= ub(x)} holds trivially.
If \mzninline{b} takes the value 1, \mzninline{ub(x)*(1-b)} is equal to 0, enforcing the constraint \mzninline{x <= 0}.
\end{example}
@ -683,6 +682,8 @@ The static approach can be further improved by \emph{inlining} function calls, s
\jip{TODO:\ \gls{cse} will be discussed in the background. How can we make this
more specific to how it works in \nanozinc{}.}
\jip{Comment Peter: details or implementation -- interaction with reference counting??}
\paragraph{Reification}
\jip{Adjust with information in the background section. Is there anything specific to the \microzinc{}/\nanozinc{} system?}
@ -744,8 +745,8 @@ For example the evaluation of the linear constraint \mzninline{x + 2*y <= z} wil
constraint int_le(i2, z);
\end{nzn}
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.
These \nanozinc\ definitions are correct, but, at least for \gls{mip} solvers \jip{this was wrong}, 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, which corresponds to \mzninline{1*x + 2*y - z <= 0}.
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.
This can be resolved using the \gls{aggregation} of constraints.
@ -753,7 +754,7 @@ When we aggregate constraints we combine constraints connected through functiona
For example, the arithmetic definitions can be combined into linear constraints, Boolean logic can be combined into clauses, and counting constraints can be combined into global cardinality constraints.
In \nanozinc{}, we are able to aggregate constraints during partial evaluation.
To aggregate a certain kind of constraint, the solver must the constraint as a solver-level primitive.
To aggregate a certain kind of constraint, the \solver{} must support the constraint as a solver-level primitive.
These constraints will now be kept as temporary functional definitions in the \nanozinc\ program.
Once a top-level (relational) \gls{constraint} is posted that uses the temporary functional definitions as one of its arguments, the interpreter will employ dedicated \gls{aggregation} logic to visit the functional definitions and combine their constraints.
The top-level \gls{constraint} is then replaced by the combined \gls{constraint}.