From 7665f6beda491abbbfb3b2b0e48226603688503b Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Thu, 11 Mar 2021 12:09:47 +1100 Subject: [PATCH] Convert math context for rewriting chapter --- chapters/4_rewriting.tex | 280 +++++++++++++++++++-------------------- 1 file changed, 140 insertions(+), 140 deletions(-) diff --git a/chapters/4_rewriting.tex b/chapters/4_rewriting.tex index 7ace930..8c38e4d 100644 --- a/chapters/4_rewriting.tex +++ b/chapters/4_rewriting.tex @@ -162,7 +162,7 @@ expressions have \mzninline{par} type. A \nanozinc\ program, defined in \cref{fig:4-nzn-syntax}, is simply a list of calls, where the result of each call is bound to either an identifier or the -constant true. The \syntax{$\sep$ *} will be used to track dependent +constant true. The \syntax{\(\sep\) *} will be used to track dependent constraints (this will be explained in detail in \cref{sec:4-nanozinc}, for now you can assume it is empty). @@ -170,7 +170,7 @@ you can assume it is empty). \begin{grammar} ::= * - ::= $\mapsto$ $\sep$ * + ::= \(\mapsto\) \(\sep\) * ::= | @@ -207,10 +207,10 @@ The translation from \minizinc\ to \microzinc\ involves the following steps: \end{enumerate} % \begin{algorithm}[H] -% \KwData{A \minizinc\ model $M = \langle{}V, C, F\rangle{}$, where $V$ is a set of declaration -% items, $C$ is a set of constraint items, and $F$ are the definitions for all -% functions used in $M$.} -% \KwResult{A list of \microzinc\ defintions $\mu$ and a \nanozinc\ program $n$.} +% \KwData{A \minizinc\ model \(M = \langle{}V, C, F\rangle{}\), where \(V\) is a set of declaration +% items, \(C\) is a set of constraint items, and \(F\) are the definitions for all +% functions used in \(M\).} +% \KwResult{A list of \microzinc\ defintions \(\mu\) and a \nanozinc\ program \(n\).} % \While{not at end of this document}{ % read current\; @@ -226,10 +226,10 @@ The translation from \minizinc\ to \microzinc\ involves the following steps: % \begin{algorithm}[H] -% \KwData{A \minizinc\ expression $e$ and $rn$ a function to rename identifiers} -% \KwResult{A \microzinc\ expression $e'$.} +% \KwData{A \minizinc\ expression \(e\) and \(rn\) a function to rename identifiers} +% \KwResult{A \microzinc\ expression \(e'\).} -% \Switch{$e$} { +% \Switch{\(e\)} { % \Case{\textup{\texttt{if \(c\) then \(e_{1}\) else \(e_{2}\) endif}}}{ % \eIf{\(type(c) \in \textup{\texttt{var}}\)}{ % \(e' \longleftarrow \texttt{MicroExpr}(\texttt{slv\_if\_then\_else(\(c\), \(e_{1}\), \(e_{2}\))}, rn)\) @@ -243,7 +243,7 @@ The translation from \minizinc\ to \microzinc\ involves the following steps: % \Case{\textup{(call)} \(n(e_{1}, ..., e_{n})\)}{ % } -% \lCase{\textup{(ident)} $id$} {\(e' \longleftarrow rn(id)\)} +% \lCase{\textup{(ident)} \(id\)} {\(e' \longleftarrow rn(id)\)} % \lOther{\(e' \longleftarrow e\)} % } % \Return{\(e'\)} @@ -252,7 +252,7 @@ The translation from \minizinc\ to \microzinc\ involves the following steps: \begin{example} Consider the following \minizinc\ model, a simple unsatisfiable ``pigeonhole - problem'', trying to assign $n$ pigeons to $n-1$ holes: + problem'', trying to assign \(n\) pigeons to \(n-1\) holes: \begin{mzn} predicate all_different(array[int] of var int: x) = @@ -268,7 +268,7 @@ The translation from \minizinc\ to \microzinc\ involves the following steps: The translation to \microzinc\ turns all expressions into function calls, replaces the special generator syntax in the \mzninline{forall} with an array comprehension, and creates the \mzninline{main} function. Note how the domain - $1..n-1$ of the \mzninline{pigeon} array is replaced by a \mzninline{set_in} + \(1..n-1\) of the \mzninline{pigeon} array is replaced by a \mzninline{set_in} constraint for each element of the array. \begin{mzn} @@ -291,8 +291,8 @@ The translation from \minizinc\ to \microzinc\ involves the following steps: \end{mzn} For a concrete instance of the model, we can then create a simple \nanozinc\ - program that calls \mzninline{main}, for example for $n=10$: - \mzninline{true @$\mapsto$@ main(10) @$\sep$@ []}. + program that calls \mzninline{main}, for example for \(n=10\): + \nzninline{true @\(\mapsto\)@ main(10) @\(\sep\)@ []}. \end{example} \subsection{Partial Evaluation of \glsentrytext{nanozinc}}\label{sub:4-partial} @@ -365,18 +365,18 @@ result. \begin{example}\label{ex:4-absnzn} Consider the \minizinc\ fragment\\\mzninline{constraint abs(x) > y;}\\ where - \mzninline{x} and \mzninline{y} have domain $[-10, 10]$. After rewriting all + \mzninline{x} and \mzninline{y} have domain \([-10, 10]\). After rewriting all definitions, the resulting \nanozinc\ program could look like this: - \begin{mzn} - x @$\mapsto$@ mkvar(-10..10) @$\sep$@ [] - y @$\mapsto$@ mkvar(-10..10) @$\sep$@ [] - z @$\mapsto$@ mkvar(-infinity,infinity) @$\sep$@ [] - b0 @$\mapsto$@ int_abs(x, z) @$\sep$@ [] - t @$\mapsto$@ z @$\sep$@ [b0] - b1 @$\mapsto$@ int_gt(t,y) @$\sep$@ [] - true @$\mapsto$@ true @$\sep$@ [b1] - \end{mzn} + \begin{nzn} + x @\(\mapsto\)@ mkvar(-10..10) @\(\sep\)@ [] + y @\(\mapsto\)@ mkvar(-10..10) @\(\sep\)@ [] + z @\(\mapsto\)@ mkvar(-infinity,infinity) @\(\sep\)@ [] + b0 @\(\mapsto\)@ int_abs(x, z) @\(\sep\)@ [] + t @\(\mapsto\)@ z @\(\sep\)@ [b0] + b1 @\(\mapsto\)@ int_gt(t,y) @\(\sep\)@ [] + true @\(\mapsto\)@ true @\(\sep\)@ [b1] + \end{nzn} 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 @@ -407,44 +407,44 @@ suitable alpha renaming. \begin{figure*} \centering \begin{prooftree} - \AxiomC{$\ptinline{F($p_1, \ldots, p_k$) = E;} \in \Prog$ where the $p_i$ + \AxiomC{\(\ptinline{F(\(p_1, \ldots, p_k\)) = E;} \in \Prog\) where the \(p_i\) are fresh} \noLine\ - \UnaryInfC{\Sem{$a_i$}{\Prog, \Env_{i-1}} $\Rightarrow~ \tuple{v_i, + \UnaryInfC{\Sem{\(a_i\)}{\Prog, \Env_{i-1}} \(\Rightarrow~ \tuple{v_i, \Env_i'}, \ \Env_0=\Env, \Env_i=\Env_i'\cup\{p_i\mapsto v_i\sep[]\} \quad \forall 1 \leq - i \leq k$} + i \leq k\)} \noLine\ \UnaryInfC{\Sem{E}{\Prog, \Env_k} - $\Rightarrow ~ \tuple{v, \Env'}$} + \(\Rightarrow ~ \tuple{v, \Env'}\)} \RightLabel{(Call)} - \UnaryInfC{\Sem{F($a_1, \ldots, a_k$)}{\Prog, \Env} $\Rightarrow$ - $\tuple{v, \Env'}$} + \UnaryInfC{\Sem{F(\(a_1, \ldots, a_k\))}{\Prog, \Env} \(\Rightarrow\) + \(\tuple{v, \Env'}\)} \end{prooftree} \begin{prooftree} - \AxiomC{$\ptinline{F} \in$ Builtins} + \AxiomC{\(\ptinline{F} \in\) Builtins} % \noLine - \AxiomC{\Sem{$a_i$}{\Prog, \Env} $\Rightarrow~ \tuple{v_i, \Env}, + \AxiomC{\Sem{\(a_i\)}{\Prog, \Env} \(\Rightarrow~ \tuple{v_i, \Env}, \forall 1 \leq - i \leq k$} -% $\ldots$, \Sem{$a_k$}{\Prog, \Env} $\Rightarrow~\tuple{\Ctx_k,v_k}$} + i \leq k\)} +% \(\ldots\), \Sem{\(a_k\)}{\Prog, \Env} \(\Rightarrow~\tuple{\Ctx_k,v_k}\)} \RightLabel{(CallBuiltin)} - \BinaryInfC{\Sem{F($a_1, \ldots, a_k$)}{\Prog, \Env} $\Rightarrow$ - $\tuple{ \mathit{eval}(\ptinline{F}(v_1,\ldots, v_k)), \Env}$} + \BinaryInfC{\Sem{F(\(a_1, \ldots, a_k\))}{\Prog, \Env} \(\Rightarrow\) + \(\tuple{ \mathit{eval}(\ptinline{F}(v_1,\ldots, v_k)), \Env}\)} \end{prooftree} \begin{prooftree} - \AxiomC{$\ptinline{F($p_1, \ldots, p_k$);} \in \Prog$} + \AxiomC{\(\ptinline{F(\(p_1, \ldots, p_k\));} \in \Prog\)} % \noLine - \AxiomC{\Sem{$a_i$}{\Prog, \Env_{i-1}} $\Rightarrow~ \tuple{v_i, \Env_i}, + \AxiomC{\Sem{\(a_i\)}{\Prog, \Env_{i-1}} \(\Rightarrow~ \tuple{v_i, \Env_i}, ~\forall 1 \leq - i \leq k$} -% $\ldots$, \Sem{$a_k$}{\Prog, \Env} $\Rightarrow~\tuple{\Ctx_k,v_k}$} + i \leq k\)} +% \(\ldots\), \Sem{\(a_k\)}{\Prog, \Env} \(\Rightarrow~\tuple{\Ctx_k,v_k}\)} \RightLabel{(CallPrimitive)} - \BinaryInfC{\Sem{F($a_1, \ldots, a_k$)}{\Prog, \Env_0} $\Rightarrow$ - $\tuple{ x, \{ x \mapsto \ptinline{F}(v_1,\ldots, v_k) \sep [] \} \cup \Env_k}$} + \BinaryInfC{\Sem{F(\(a_1, \ldots, a_k\))}{\Prog, \Env_0} \(\Rightarrow\) + \(\tuple{ x, \{ x \mapsto \ptinline{F}(v_1,\ldots, v_k) \sep [] \} \cup \Env_k}\)} \end{prooftree} \caption{\label{fig:4-rewrite-to-nzn-calls} Rewriting rules for partial evaluation of \microzinc\ calls to \nanozinc.} @@ -453,10 +453,10 @@ 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 first -evaluates all actual parameter expressions $a_i$, creating new contexts where -the evaluation results are bound to the formal parameters $p_i$. It then -evaluates the function body $\ptinline{E}$ on this context, and returns the +\microzinc\ program \(\Prog\) and \nanozinc\ program \(\Env\). The rule first +evaluates all actual parameter expressions \(a_i\), creating new contexts where +the evaluation results are bound to the formal parameters \(p_i\). It then +evaluates the function body \(\ptinline{E}\) on this context, and returns the result. The (CallBuiltin) rule applies to ``built-in'' functions that can be evaluated @@ -467,61 +467,61 @@ parameter values. The (CallPrimitive) rule applies to non-built-in functions that are defined without a function body. These are considered primitives, and as such simply need to be transferred into the \nanozinc\ program. The rule evaluates all -actual parameters, and creates a new variable $x$ to store the result, which is +actual parameters, and creates a new variable \(x\) to store the result, which is simply the function applied to the evaluated parameters. \begin{figure*} \centering \begin{prooftree} - \AxiomC{\Sem{$\mathbf{I}$}{\Prog, \Env} $\Rightarrow (\Ctx, \Env')$} - \AxiomC{\Sem{$E$}{\Prog, \Env'} $\Rightarrow \tuple{v, \Env''}$} - \AxiomC{$x$ fresh} + \AxiomC{\Sem{\(\mathbf{I}\)}{\Prog, \Env} \(\Rightarrow (\Ctx, \Env')\)} + \AxiomC{\Sem{\(E\)}{\Prog, \Env'} \(\Rightarrow \tuple{v, \Env''}\)} + \AxiomC{\(x\) fresh} \RightLabel{(LetC)} - \TrinaryInfC{\Sem{let \{ $\mathbf{I}$ \} in $E$}{\Prog, \Env} $\Rightarrow - \tuple{x, \{ x \mapsto v \sep \Ctx \} \cup \Env''}$} + \TrinaryInfC{\Sem{let \{ \(\mathbf{I}\) \} in \(E\)}{\Prog, \Env} \(\Rightarrow + \tuple{x, \{ x \mapsto v \sep \Ctx \} \cup \Env''}\)} \end{prooftree} % \begin{prooftree} -% \AxiomC{\Sem{$E_1$}{\Prog, \Env} $\Rightarrow \Ctx_1, r_1$} -% \AxiomC{\Sem{$E_2$}{\Prog, \Env} $\Rightarrow \Ctx_2, r_2$} +% \AxiomC{\Sem{\(E_1\)}{\Prog, \Env} \(\Rightarrow \Ctx_1, r_1\)} +% \AxiomC{\Sem{\(E_2\)}{\Prog, \Env} \(\Rightarrow \Ctx_2, r_2\)} % \RightLabel{(Rel)} -% \BinaryInfC{\Sem{$E_1 \bowtie E_2$}{\Prog, \Env} $\Rightarrow \Ctx_1 \wedge \Ctx_2 \wedge (r_1 \bowtie r_2)$} +% \BinaryInfC{\Sem{\(E_1 \bowtie E_2\)}{\Prog, \Env} \(\Rightarrow \Ctx_1 \wedge \Ctx_2 \wedge (r_1 \bowtie r_2)\)} % \end{prooftree} \begin{prooftree} \AxiomC{} \RightLabel{(Item0)} - \UnaryInfC{\Sem{$\epsilon$}{\Prog, \Env} $\Rightarrow - (\ptinline{true}, \Env$)} + \UnaryInfC{\Sem{\(\epsilon\)}{\Prog, \Env} \(\Rightarrow + (\ptinline{true}, \Env\))} \end{prooftree} \begin{prooftree} - \AxiomC{\Sem{$\mathbf{I}$}{\Prog, \Env\ \cup\ \{x \mapsto\ \texttt{mkvar()} \sep\ []\}} $\Rightarrow (\Ctx, \Env')$} + \AxiomC{\Sem{\(\mathbf{I}\)}{\Prog, \Env\ \cup\ \{x \mapsto\ \texttt{mkvar()} \sep\ []\}} \(\Rightarrow (\Ctx, \Env')\)} \RightLabel{(ItemT)} - \UnaryInfC{\Sem{$t:x, \mathbf{I}$}{\Prog, \Env} $\Rightarrow - (\Ctx, \Env')$} + \UnaryInfC{\Sem{\(t:x, \mathbf{I}\)}{\Prog, \Env} \(\Rightarrow + (\Ctx, \Env')\)} \end{prooftree} \begin{prooftree} - \AxiomC{\Sem{$E$}{\Prog, \Env} $\Rightarrow \tuple{v, \Env'}$} - \AxiomC{\Sem{$\mathbf{I}$}{\Prog, \Env' \cup\ \{x \mapsto\ v \sep\ [] \}} $\Rightarrow (\Ctx, \Env'')$} + \AxiomC{\Sem{\(E\)}{\Prog, \Env} \(\Rightarrow \tuple{v, \Env'}\)} + \AxiomC{\Sem{\(\mathbf{I}\)}{\Prog, \Env' \cup\ \{x \mapsto\ v \sep\ [] \}} \(\Rightarrow (\Ctx, \Env'')\)} \RightLabel{(ItemTE)} - \BinaryInfC{\Sem{$t:x = E, \mathbf{I}$}{\Prog, \Env} $\Rightarrow - (\Ctx, \Env'')$} + \BinaryInfC{\Sem{\(t:x = E, \mathbf{I}\)}{\Prog, \Env} \(\Rightarrow + (\Ctx, \Env'')\)} \end{prooftree} \begin{prooftree} - \AxiomC{\Sem{$C$}{\Prog, \Env} $\Rightarrow \tuple{v, \Env'}$} - \AxiomC{\Sem{$\mathbf{I}$}{\Prog, \Env'} $\Rightarrow (\Ctx, \Env'')$} + \AxiomC{\Sem{\(C\)}{\Prog, \Env} \(\Rightarrow \tuple{v, \Env'}\)} + \AxiomC{\Sem{\(\mathbf{I}\)}{\Prog, \Env'} \(\Rightarrow (\Ctx, \Env'')\)} \RightLabel{(ItemC)} - \BinaryInfC{\Sem{$\mbox{constraint~} C, \mathbf{I}$}{\Prog, \Env} $\Rightarrow - (\{v\}\cup\Ctx, \Env'')$} + \BinaryInfC{\Sem{\(\mbox{constraint~} C, \mathbf{I}\)}{\Prog, \Env} \(\Rightarrow + (\{v\}\cup\Ctx, \Env'')\)} \end{prooftree} \caption{\label{fig:4-rewrite-to-nzn-let} Rewriting rules for partial evaluation of \microzinc\ let expressions to \nanozinc.} \end{figure*} The rules in \cref{fig:4-rewrite-to-nzn-let} considers let expressions. The -(LetC) rule generates the constraints $\phi$ and \nanozinc\ program $\Env'$ -defined by the let items \textbf{I}, then evaluates the body expression $E$ in -this new context. It finally binds the result $v$ to a fresh variable $x$, -collecting the constraints $\phi$ that arose from the let items: $x\mapsto -v\sep\phi$. The (ItemT) rule handles introduction of new variables by adding +(LetC) rule generates the constraints \(\phi\) and \nanozinc\ program \(\Env'\) +defined by the let items \textbf{I}, then evaluates the body expression \(E\) in +this new context. It finally binds the result \(v\) to a fresh variable \(x\), +collecting the constraints \(\phi\) that arose from the let items: \(x\mapsto +v\sep\phi\). 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 adding a definition to the context to evaluate the result of the items. The (Item0) rule @@ -531,56 +531,56 @@ is the base case for a list of let items. \centering \begin{prooftree} \RightLabel{(IdC)} - \AxiomC{$x \in \langle ident \rangle$} - \AxiomC{$v \in \langle literal \rangle$} - \BinaryInfC{\Sem{$x$}{\Prog, \{x \mapsto\ v \sep\ []\} \cup\ \Env} $\Rightarrow \tuple{v, \{x \mapsto v \sep [] \} \cup \Env}$} + \AxiomC{\(x \in \langle ident \rangle\)} + \AxiomC{\(v \in \langle literal \rangle\)} + \BinaryInfC{\Sem{\(x\)}{\Prog, \{x \mapsto\ v \sep\ []\} \cup\ \Env} \(\Rightarrow \tuple{v, \{x \mapsto v \sep [] \} \cup \Env}\)} \end{prooftree} \begin{prooftree} \RightLabel{(IdX)} - \AxiomC{$x \in \langle ident \rangle$} - \AxiomC{$v$} - \AxiomC{$\phi$ otherwise} - \TrinaryInfC{\Sem{$x$}{\Prog, \{x \mapsto\ v \sep\ \phi\ \} \cup\ \Env} $\Rightarrow \tuple{x, \{x \mapsto v \sep \phi \} \cup \Env}$} + \AxiomC{\(x \in \langle ident \rangle\)} + \AxiomC{\(v\)} + \AxiomC{\(\phi\) otherwise} + \TrinaryInfC{\Sem{\(x\)}{\Prog, \{x \mapsto\ v \sep\ \phi\ \} \cup\ \Env} \(\Rightarrow \tuple{x, \{x \mapsto v \sep \phi \} \cup \Env}\)} \end{prooftree} \begin{prooftree} \RightLabel{(Const)} - \AxiomC{$c$ constant} - \UnaryInfC{\Sem{c}{\Prog, \Env} $\Rightarrow \tuple{c, \Env}$} + \AxiomC{\(c\) constant} + \UnaryInfC{\Sem{c}{\Prog, \Env} \(\Rightarrow \tuple{c, \Env}\)} \end{prooftree} \begin{prooftree} - \RightLabel{(If$_T$)} - \AxiomC{\Sem{$C$}{\Prog, \Env} $\Rightarrow$ $\tuple{\ptinline{true}, \_}$} - \UnaryInfC{\Sem{if $C$ then $E_t$ else $E_e$ endif}{\Prog, \Env} $\Rightarrow$ \Sem{$E_t$}{\Prog, \Env}} + \RightLabel{(If\(_T\))} + \AxiomC{\Sem{\(C\)}{\Prog, \Env} \(\Rightarrow\) \(\tuple{\ptinline{true}, \_}\)} + \UnaryInfC{\Sem{if \(C\) then \(E_t\) else \(E_e\) endif}{\Prog, \Env} \(\Rightarrow\) \Sem{\(E_t\)}{\Prog, \Env}} \end{prooftree} \begin{prooftree} - \RightLabel{(If$_F$)} - \AxiomC{\Sem{$C$}{\Prog, \Env} $\Rightarrow$ $\tuple{\ptinline{false}, \_}$} - \UnaryInfC{\Sem{if $C$ then $E_t$ else $E_e$ endif}{\Prog, \Env} $\Rightarrow$ \Sem{$E_e$}{\Prog, \Env}} + \RightLabel{(If\(_F\))} + \AxiomC{\Sem{\(C\)}{\Prog, \Env} \(\Rightarrow\) \(\tuple{\ptinline{false}, \_}\)} + \UnaryInfC{\Sem{if \(C\) then \(E_t\) else \(E_e\) endif}{\Prog, \Env} \(\Rightarrow\) \Sem{\(E_e\)}{\Prog, \Env}} \end{prooftree} \begin{prooftree} - \AxiomC{\Sem{G}{\Prog,\Env} $\Rightarrow \tuple{ \ptinline{true}, \_}$} - \AxiomC{\Sem{$E$}{\Prog, \Env} $\Rightarrow \tuple {v, \Env'}$} + \AxiomC{\Sem{G}{\Prog,\Env} \(\Rightarrow \tuple{ \ptinline{true}, \_}\)} + \AxiomC{\Sem{\(E\)}{\Prog, \Env} \(\Rightarrow \tuple {v, \Env'}\)} \RightLabel{(WhereT)} - \BinaryInfC{\Sem{$[E ~|~ \mbox{where~} G]$}{\Prog, \Env} $\Rightarrow - \tuple{[v], \Env'}$} + \BinaryInfC{\Sem{\([E ~|~ \mbox{where~} G]\)}{\Prog, \Env} \(\Rightarrow + \tuple{[v], \Env'}\)} \end{prooftree} \begin{prooftree} - \AxiomC{\Sem{G}{\Prog,\Env} $\Rightarrow \tuple{ \ptinline{false}, \_}$} + \AxiomC{\Sem{G}{\Prog,\Env} \(\Rightarrow \tuple{ \ptinline{false}, \_}\)} \RightLabel{(WhereF)} - \UnaryInfC{\Sem{$[E ~|~ \mbox{where~} G]$}{\Prog, \Env} $\Rightarrow - \tuple{[], \Env}$} + \UnaryInfC{\Sem{\([E ~|~ \mbox{where~} G]\)}{\Prog, \Env} \(\Rightarrow + \tuple{[], \Env}\)} \end{prooftree} \begin{prooftree} - \AxiomC{\Sem{$\mathit{PE}$}{\Prog,\Env} $\Rightarrow \tuple{S, \_}$} + \AxiomC{\Sem{\(\mathit{PE}\)}{\Prog,\Env} \(\Rightarrow \tuple{S, \_}\)} \noLine\ - \UnaryInfC{\Sem{$[E ~|~ \mathit{GE} \mbox{~where~} G]$}{\Prog, \Env\ \cup\ \{ x\mapsto\ + \UnaryInfC{\Sem{\([E ~|~ \mathit{GE} \mbox{~where~} G]\)}{\Prog, \Env\ \cup\ \{ x\mapsto\ v \sep\ []\}}} \noLine\ - \UnaryInfC{\hspace{8em} $\Rightarrow \tuple{A_v, \Env \cup \{x \mapsto v \sep []\} \cup \Env_v}, \forall - v \in S $} + \UnaryInfC{\hspace{8em} \(\Rightarrow \tuple{A_v, \Env \cup \{x \mapsto v \sep []\} \cup \Env_v}, \forall + v \in S \)} \RightLabel{(ListG)} - \UnaryInfC{\Sem{$[E~|~ x \mbox{~in~} \mathit{PE}, \mathit{GE} \mbox{~where~} G]$}{\Prog, \Env} $\Rightarrow - \tuple{\mbox{concat} [ A_v ~|~ v \in S ], \Env \cup \bigcup_{v \in S} \Env_v}$} + \UnaryInfC{\Sem{\([E~|~ x \mbox{~in~} \mathit{PE}, \mathit{GE} \mbox{~where~} G]\)}{\Prog, \Env} \(\Rightarrow + \tuple{\mbox{concat} [ A_v ~|~ v \in S ], \Env \cup \bigcup_{v \in S} \Env_v}\)} \end{prooftree} \caption{\label{fig:4-rewrite-to-nzn-other} Rewriting rules for partial evaluation of other \microzinc\ expressions to \nanozinc.} @@ -592,14 +592,14 @@ 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 (Const) rule simply -returns the constant. The (If$_T$) and (If$_F$) rules evaluate the if condition +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. The (WhereF) rule evaluates the guard and when false returns an empty list. The (ListG) rule evaluates the iteration set -$PE$ to get its value $S$, which must be fixed. It then evaluates the expression -$E$ with all the different possible values $v \in S$ of the generator $x$, -collecting the additional \nanozinc\ definitions $\Env_v$. It returns the +\(PE\) to get its value \(S\), which must be fixed. It then evaluates the expression +\(E\) with all the different possible values \(v \in S\) of the generator \(x\), +collecting the additional \nanozinc\ definitions \(\Env_v\). It returns the concatenation of the resulting lists with all the additional \nanozinc\ items. \subsection{Prototype Implementation} @@ -652,7 +652,7 @@ constraint, we can pick any value for it. The model without the variable is therefore equisatisfiable with the original model. Consider now the case where a variable in \nanozinc\ is only used in its own -auxiliary definitions (the \mzninline{@$\sep\phi$@} part). +auxiliary definitions (the \mzninline{@\(\sep\phi\)@} part). \begin{example}\label{ex:4-absreif} The following is a slight variation on the \minizinc\ fragment in @@ -672,16 +672,16 @@ auxiliary definitions (the \mzninline{@$\sep\phi$@} part). constraint for the disjunction, which uses the variable \mzninline{b1} that was introduced for \mzninline{abs(x) > y}: - \begin{mzn} - c @$\mapsto$@ true @$\sep$@ [] - x @$\mapsto$@ mkvar(-10..10) @$\sep$@ [] - y @$\mapsto$@ mkvar(-10..10) @$\sep$@ [] - b0 @$\mapsto$@ int_abs(x, z) @$\sep$@ [] - b1 @$\mapsto$@ int_gt(t,y) @$\sep$@ [] - z @$\mapsto$@ mkvar(-infinity,infinity) @$\sep$@ [] - t @$\mapsto$@ z @$\sep$@ [b0] - b2 @$\mapsto$@ bool_or(b1,c) @$\sep$@ [] - true @$\mapsto$@ true @$\sep$@ [b2,c] + \begin{nzn} + c @\(\mapsto\)@ true @\(\sep\)@ [] + x @\(\mapsto\)@ mkvar(-10..10) @\(\sep\)@ [] + y @\(\mapsto\)@ mkvar(-10..10) @\(\sep\)@ [] + b0 @\(\mapsto\)@ int_abs(x, z) @\(\sep\)@ [] + b1 @\(\mapsto\)@ int_gt(t,y) @\(\sep\)@ [] + z @\(\mapsto\)@ mkvar(-infinity,infinity) @\(\sep\)@ [] + t @\(\mapsto\)@ z @\(\sep\)@ [b0] + b2 @\(\mapsto\)@ bool_or(b1,c) @\(\sep\)@ [] + true @\(\mapsto\)@ true @\(\sep\)@ [b2,c] \end{mzn} Since \mzninline{c} is bound to \mzninline{true}, the disjunction @@ -699,12 +699,12 @@ auxiliary definitions (the \mzninline{@$\sep\phi$@} part). and can be removed, and then \mzninline{z}. The resulting \nanozinc\ program is much more compact: - \begin{mzn} - c @$\mapsto$@ true @$\sep$@ [] - x @$\mapsto$@ mkvar(-10..10) @$\sep$@ [] - y @$\mapsto$@ mkvar(-10..10) @$\sep$@ [] - true @$\mapsto$@ true @$\sep$@ [] - \end{mzn} + \begin{nzn} + c @\(\mapsto\)@ true @\(\sep\)@ [] + x @\(\mapsto\)@ mkvar(-10..10) @\(\sep\)@ [] + y @\(\mapsto\)@ mkvar(-10..10) @\(\sep\)@ [] + true @\(\mapsto\)@ true @\(\sep\)@ [] + \end{nzn} We assume here that \mzninline{c}, \mzninline{x} and \mzninline{y} are used in other parts of the model not shown here and therefore not removed. @@ -829,16 +829,16 @@ The more complicated case for \mzninline{x=y} is when both \mzninline{x} and as \mzninline{constraint f(a)=g(b)}. Let us assume that part of the corresponding \nanozinc\ code looks like this: -\begin{mzn} - x @$\mapsto$@ mkvar() @$\sep$@ []; - y @$\mapsto$@ mkvar() @$\sep$@ []; - b0 @$\mapsto$@ f_rel(a,x) @$\sep$@ []; - b1 @$\mapsto$@ g_rel(b,y) @$\sep$@ []; - t0 @$\mapsto$@ x @$\sep$@ [b0]; - t1 @$\mapsto$@ y @$\sep$@ [b1]; - b2 @$\mapsto$@ int_eq(t0,t1) @$\sep$@ []; - true @$\mapsto$@ true @$\sep$@ [b2]; -\end{mzn} +\begin{nzn} + x @\(\mapsto\)@ mkvar() @\(\sep\)@ []; + y @\(\mapsto\)@ mkvar() @\(\sep\)@ []; + b0 @\(\mapsto\)@ f_rel(a,x) @\(\sep\)@ []; + b1 @\(\mapsto\)@ g_rel(b,y) @\(\sep\)@ []; + t0 @\(\mapsto\)@ x @\(\sep\)@ [b0]; + t1 @\(\mapsto\)@ y @\(\sep\)@ [b1]; + b2 @\(\mapsto\)@ int_eq(t0,t1) @\(\sep\)@ []; + true @\(\mapsto\)@ true @\(\sep\)@ [b2]; +\end{nzn} In this case, simply removing either \mzninline{t0} or \mzninline{t1} would not be correct, since that would trigger the removal of the corresponding definition @@ -852,13 +852,13 @@ definition is removed. The interpreter moves all auxiliary constraints from \mzninline{true} item, and then removes the \mzninline{int_eq} constraint and \mzninline{t1}. The resulting \nanozinc\ looks like this: -\begin{mzn} - x @$\mapsto$@ mkvar() @$\sep$@ []; - b0 @$\mapsto$@ f_rel(a,x) @$\sep$@ []; - b1 @$\mapsto$@ g_rel(b,t0) @$\sep$@ []; - t0 @$\mapsto$@ x @$\sep$@ [b0]; - true @$\mapsto$@ true @$\sep$@ [b1]; -\end{mzn} +\begin{nzn} + x @\(\mapsto\)@ mkvar() @\(\sep\)@ []; + b0 @\(\mapsto\)@ f_rel(a,x) @\(\sep\)@ []; + b1 @\(\mapsto\)@ g_rel(b,t0) @\(\sep\)@ []; + t0 @\(\mapsto\)@ x @\(\sep\)@ [b0]; + true @\(\mapsto\)@ true @\(\sep\)@ [b1]; +\end{nzn} The process of equality propagation is similar to unification in logic programming \autocite{warren-1983-wam}. However, since equations in \minizinc\ @@ -1081,7 +1081,7 @@ Times are averages of 10 runs.\footnote{All models obtained from \Cref{sfig:4-compareruntime} compares the flattening time for each of the 100 instances. Points below the line indicate that the new system is faster. On -average, the new system achieves a speed-up of $2.3$, with very few instances +average, the new system achieves a speed-up of \(2.3\), with very few instances not achieving any speedup. In terms of memory performance (\cref{sfig:4-comparemem}), version 2.4.3 can sometimes still outperform the new prototype. We have identified that the main memory bottlenecks are our currently