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

Use of floating listings in rewriting chapter

Browse Source
This commit is contained in:
Jip J. Dekker 2021-07-20 21:22:20 +10:00
parent 2f0a576f4f
commit 147e691063
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
7 changed files with 113 additions and 98 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
assets/listing/rew_abs.mzn Normal file
View File

@ -0,0 +1,5 @@
function var int: abs(var int: x) =
let {
var int: z;
constraint int_abs(x, z);
} in z;

16
assets/listing/rew_elem_safe.mzn Normal file
View File

@ -0,0 +1,16 @@
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;

16
assets/listing/rew_knapsack.mzn Normal file
View File

@ -0,0 +1,16 @@
predicate knapsack(
array[int] of int: w,
array[int] of int:p,
array[int] of var int:x,
var int: W, var int: P
) =
assert(
index_set(w) = index_set(p) /\ index_set(w) = index_set(x),
"index set of weights must be equal to index set of profits and index set of items",
) /\ assert(
lb_array(w) >= 0,
"weights must be non-negative",
) /\ assert(
lb_array(p) >= 0,
"profits must be non-negative",
) /\ fzn_knapsack(w, p, x, W, P);

11
assets/listing/rew_opt_plus.mzn Normal file
View File

@ -0,0 +1,11 @@
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]);
tuple(var bool, var int): res = (bool_and(x1, y1), int_plus(x3, y3));
} in res;

8
assets/listing/rew_pigeon_mzn.mzn Normal file
View File

@ -0,0 +1,8 @@
predicate all_different(array[int] of var int: x) =
forall (i,j in 1..length(x) where i<j) (
x[i] != x[j]
);
int: n;
array[1..n] of var 1..n-1: pigeon;
constraint all_different(pigeon);

16
assets/listing/rew_pigeon_uzn.mzn Normal file
View File

@ -0,0 +1,16 @@
function var bool: all_different(array[int] of var int: x) =
let {
set of int: S = range(1, length(x));
} in forall([
int_neq(element(x, i),element(x, j))
| i in S,
j in S
where int_lt(i,j)
]);
function var bool: main(int: n) =
let {
var bool: root_ctx;
array[1..n] of var 1..n-1: pigeon;
constraint all_different(pigeon);
} in root_ctx;

131
chapters/3_rewriting.tex
View File

@ -157,21 +157,12 @@ The translation from \minizinc{} to \microzinc{} involves the following steps.
The Boolean \variable{}, then, represents if the variable exists or is absent, while the non-optional \variable{} of the same type represents the value of the optional \variable{} if it exists.
In \microzinc{} this can be represented as a tuple of the two \variables{}.
The function definitions for optional types then take both \variables{} into account.
For example, the definition of \mzninline{int_plus(x, y)} for optional types can be translated into the following function.
For example, the definition of \mzninline{int_plus(x, y)} for optional types can be translated into the function shown in \cref{lst:rew-opt-plus}.
\begin{mzn}
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]);
tuple(var bool, var int): res = (bool_and(x1, y1), int_plus(x3, y3));
} in res;
\end{mzn}
\begin{listing}
\mznfile{assets/listing/rew_opt_plus.mzn}
\caption{\label{lst:rew-opt-plus} A definition of \mzninline{int_plus} for optional integers in \microzinc{} syntax.}
\end{listing}
\item Lift the partiality in expressions into the surrounding context to implement \minizinc{}'s relational semantics.
In contrast to \minizinc{}, a \microzinc{} expression must be total.
@ -186,26 +177,12 @@ The translation from \minizinc{} to \microzinc{} involves the following steps.
\end{mzn}
\noindent{}It is only defined when \mzninline{x in index_set(a)}.
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.}
The function shown in \cref{lst:rew-elem-safe} 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 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}
\begin{listing}
\mznfile{assets/listing/rew_elem_safe.mzn}
\caption{\label{lst:rew-elem-safe} A total of the \mzninline{element} function in \microzinc{}.}
\end{listing}
Similar to the replacement of optional values, all occurrences of the \mzninline{element} function are replaced by \mzninline{element_safe}.
The usage of its result should be guarded by the returned totality variable in the surrounding Boolean context.
@ -246,40 +223,23 @@ 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 \minizinc{} model in \cref{lst:rew-pigeon-mzn}.
It describes 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) =
forall (i,j in 1..length(x) where i<j) (
x[i] != x[j]
);
int: n;
array[1..n] of var 1..n-1: pigeon;
constraint all_different(pigeon);
\end{mzn}
\begin{listing}
\mznfile{assets/listing/rew_pigeon_mzn.mzn}
\caption{\label{lst:rew-pigeon-mzn} A \minizinc{} model of the pigeonhole problem.}
\end{listing}
The translation to \microzinc{} turns all expressions into function calls, replaces the special generator syntax in the \mzninline{forall} with an \gls{array} \gls{comprehension}, and creates the \mzninline{main} function.
The result of this translation is shown in \cref{lst:rew-pigeon-uzn}.
\begin{mzn}
function var bool: all_different(array[int] of var int: x) =
let {
set of int: S = range(1, length(x));
} in forall([
int_neq(element(x, i),element(x, j))
| i in S,
j in S
where int_lt(i,j)
]);
\begin{listing}
\mznfile{assets/listing/rew_pigeon_uzn.mzn}
\caption{\label{lst:rew-pigeon-uzn} The \microzinc{} tranlation of the pigeonhole problem in \cref{lst:rew-pigeon-mzn}.}
\end{listing}
function var bool: main(int: n) = let {
var bool: root_ctx;
array[1..n] of var 1..n-1: pigeon;
constraint all_different(pigeon);
} in root_ctx;
\end{mzn}
For an \instance of the \cmodel{}, we can then create a simple \nanozinc{} program that calls \mzninline{main}.
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}
@ -300,22 +260,18 @@ 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.
\begin{mzn}
function var int: abs(var int: x) =
let {
var int: z;
constraint int_abs(x, z);
} in z;
\end{mzn}
Consider the (reasonably typical) \minizinc{} encoding for the absolute value function presented in \cref{lst:rew-abs}.
When an occurrence of \mzninline{abs} is encountered, the call will be replaced by a \variable{} \mzninline{z}.
But before that can occur, the \variable{} must be introduced, and the \constraint{} \mzninline{int_abs(x, z)} is added to the model, enforcing its value.
\begin{listing}
\mznfile{assets/listing/rew_abs.mzn}
\caption{\label{lst:rew-abs} A \minizinc{} definition for the absolute value function.}
\end{listing}
\end{example}
The function \mzninline{abs(x)} above is a total function: for every value of \mzninline{x}, there is always exactly one valid value of \mzninline{z}.
In this case, the \constraint{} introduced in the \mzninline{let} expression may be enforced globally, and multiple occurrences of \mzninline{abs(x)} may be replaced with the same \mzninline{z}.
In this case, the \constraint{} introduced in the \gls{let} may be enforced globally, and multiple occurrences of \mzninline{abs(x)} may be replaced with the same \mzninline{z}.
However, the introduced \mzninline{int_abs} \constraint{} is only needed so long as any other \constraint{} refers to \mzninline{z}.
If \mzninline{z} is unused in the rest of the model, both \mzninline{z} and the \mzninline{int_abs} \constraint{} can be removed.
@ -742,7 +698,7 @@ Since functions in \microzinc{} are guaranteed to be pure and total, whenever th
Earlier in the process, however, the \minizinc{} to \microzinc{} \compiler{} can perform \gls{cse} as it is performed in many other programming languages.
\begin{example}
For instance, let us reconsider the \minizinc{} fragment from \cref{ex:back-cse}
For instance, let us reconsider the following \minizinc{} fragment from \cref{ex:back-cse}.
\begin{mzn}
(abs(x)*2 >= 20) \/ (abs(x)+5 >= 15)
@ -775,31 +731,18 @@ The usage of a \gls{cse} table can be costly.
The memory requirement and time spent finding entries can be significant in the overall process.
This is aggravated by the fact that \minizinc{} has many places where a function's body only contains a single call to a function that is not used anywhere else.
Although this structure offers flexibility when defining \minizinc{} libraries, it results in many \gls{cse} entries that differ only by their function identifier.
For example, the \mzninline{knapsack} \gls{global} is defined in the \minizinc{} standard library as follows.
\begin{mzn}
predicate knapsack(
array[int] of int: w,
array[int] of int:p,
array[int] of var int:x,
var int: W, var int: P
) =
assert(
index_set(w) = index_set(p) /\ index_set(w) = index_set(x),
"index set of weights must be equal to index set of profits and index set of items",
) /\ assert(
lb_array(w) >= 0,
"weights must be non-negative",
) /\ assert(
lb_array(p) >= 0,
"profits must be non-negative",
) /\ fzn_knapsack(w, p, x, W, P);
\end{mzn}
\begin{example}
For example, the definition of the \mzninline{knapsack} \gls{global} in the \minizinc{} standard library is shown in \cref{lst:rew-knapsack}.
After checking the \parameter{} arguments, the function merely returns the result of \mzninline{fzn_knapsack}.
This function is implemented in the \solver{} library to provide the implementation of the \mzninline{knapsack} \gls{global}.
The extra function layer ensures that these checks can be performed independently of the \solver{} library and that the \solver{} can make certain assumptions about the function arguments.
But because the modeller will only use \mzninline{knapsack}, it does not make sense to also create \gls{cse} entries for \mzninline{fzn_knapsack}, as it will never be used.
\end{example}
\begin{listing}
\mznfile{assets/listing/rew_knapsack.mzn}
\caption{\label{lst:rew-knapsack} The definition of \mzninline{knapsack} in the \minizinc{} standard library.}
\end{listing}
Therefore, we have added an additional flag to our call instruction.
This flag controls whether the call is subject to \gls{cse}.