From 147e6910630b659a01c73802419f7f14be859968 Mon Sep 17 00:00:00 2001
From: "Jip J. Dekker" <jip@dekker.one>
Date: Tue, 20 Jul 2021 21:22:20 +1000
Subject: [PATCH] Use of floating listings in rewriting chapter

---
 assets/listing/rew_abs.mzn        |   5 ++
 assets/listing/rew_elem_safe.mzn  |  16 ++++
 assets/listing/rew_knapsack.mzn   |  16 ++++
 assets/listing/rew_opt_plus.mzn   |  11 +++
 assets/listing/rew_pigeon_mzn.mzn |   8 ++
 assets/listing/rew_pigeon_uzn.mzn |  16 ++++
 chapters/3_rewriting.tex          | 139 +++++++++---------------------
 7 files changed, 113 insertions(+), 98 deletions(-)
 create mode 100644 assets/listing/rew_abs.mzn
 create mode 100644 assets/listing/rew_elem_safe.mzn
 create mode 100644 assets/listing/rew_knapsack.mzn
 create mode 100644 assets/listing/rew_opt_plus.mzn
 create mode 100644 assets/listing/rew_pigeon_mzn.mzn
 create mode 100644 assets/listing/rew_pigeon_uzn.mzn

diff --git a/assets/listing/rew_abs.mzn b/assets/listing/rew_abs.mzn
new file mode 100644
index 0000000..a011bff
--- /dev/null
+++ b/assets/listing/rew_abs.mzn
@@ -0,0 +1,5 @@
+function var int: abs(var int: x) =
+	let {
+		var int: z;
+		constraint int_abs(x, z);
+	} in z;
diff --git a/assets/listing/rew_elem_safe.mzn b/assets/listing/rew_elem_safe.mzn
new file mode 100644
index 0000000..2966536
--- /dev/null
+++ b/assets/listing/rew_elem_safe.mzn
@@ -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;
diff --git a/assets/listing/rew_knapsack.mzn b/assets/listing/rew_knapsack.mzn
new file mode 100644
index 0000000..f7da336
--- /dev/null
+++ b/assets/listing/rew_knapsack.mzn
@@ -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);
diff --git a/assets/listing/rew_opt_plus.mzn b/assets/listing/rew_opt_plus.mzn
new file mode 100644
index 0000000..1ec4854
--- /dev/null
+++ b/assets/listing/rew_opt_plus.mzn
@@ -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;
diff --git a/assets/listing/rew_pigeon_mzn.mzn b/assets/listing/rew_pigeon_mzn.mzn
new file mode 100644
index 0000000..cd13e1b
--- /dev/null
+++ b/assets/listing/rew_pigeon_mzn.mzn
@@ -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);
diff --git a/assets/listing/rew_pigeon_uzn.mzn b/assets/listing/rew_pigeon_uzn.mzn
new file mode 100644
index 0000000..5c08f34
--- /dev/null
+++ b/assets/listing/rew_pigeon_uzn.mzn
@@ -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;
diff --git a/chapters/3_rewriting.tex b/chapters/3_rewriting.tex
index 1d2fa30..1f81979 100644
--- a/chapters/3_rewriting.tex
+++ b/chapters/3_rewriting.tex
@@ -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}
-
-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.
+\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}.