Convert math context for rewriting chapter
This commit is contained in:
parent
bc5d82ae2a
commit
7665f6beda
@ -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$ <ident>*} will be used to track dependent
|
||||
constant true. The \syntax{\(\sep\) <ident>*} 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}
|
||||
<nzn> ::= <nzn-def>*
|
||||
|
||||
<nzn-def> ::= <nzn-result> $\mapsto$ <nzn-bind> $\sep$ <ident>*
|
||||
<nzn-def> ::= <nzn-result> \(\mapsto\) <nzn-bind> \(\sep\) <ident>*
|
||||
|
||||
<nzn-bind> ::= <ident> | <nzn-call>
|
||||
|
||||
@ -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
|
||||
|
||||
Reference in New Issue
Block a user