diff --git a/assets/packages.tex b/assets/packages.tex index 8d80607..30e1f13 100644 --- a/assets/packages.tex +++ b/assets/packages.tex @@ -173,7 +173,7 @@ outputdir=build, ]{minizinc}}{\end{minted}} % TODO: Fix the nanozinc sytax highlighting/formatting -\newcommand{\nzninline}[1]{\mintinline[fontsize=\small,escapeinside=@@]{markdown}{#1}} +\newcommand{\nzninline}[1]{\mintinline[fontsize=\small,escapeinside=@@]{minizinc}{#1}} \newenvironment{nzn}{\VerbatimEnvironment{}\begin{minted}[ autogobble=true, breaklines, @@ -181,4 +181,4 @@ outputdir=build, numbers=none, escapeinside=@@, fontsize=\scriptsize, -]{markdown}}{\end{minted}} +]{minizinc}}{\end{minted}} diff --git a/chapters/4_rewriting.tex b/chapters/4_rewriting.tex index 47626c9..78c7144 100644 --- a/chapters/4_rewriting.tex +++ b/chapters/4_rewriting.tex @@ -121,66 +121,73 @@ presents our conclusions. This section introduces the two sub-languages of \minizinc\ at the core of the new abstract machine model we have developed. -MicroZinc (\microzinc) is a simplified subset of \minizinc\ that only contains -function declarations and a restricted expression language. Models written in -different \cmls\ can be translated into \microzinc. NanoZinc (\nanozinc) is -similar to \flatzinc\ in that it contains only simple variable declarations and -flat constraints. However, while all function calls in \flatzinc\ need to be -solver-level primitives, \nanozinc\ calls can refer to functions implemented in -\microzinc. +\microzinc\ is generally a simplified subset of \minizinc\ that only contains +function declarations and a restricted expression language, but extends +\minizinc{}'s type system with tuples. Models written in \minizinc\ can be +translated into \microzinc. \nanozinc\ is similar to \flatzinc\ in that it +contains only simple variable declarations and flat constraints. However, while +all function calls in \flatzinc\ need to be solver-level primitives, \nanozinc\ +calls can refer to functions implemented in \microzinc. The core of the syntax of \microzinc\ is defined in \cref{fig:4-uzn-syntax}. We -have omitted the definitions of \syntax{} and \syntax{}, which -you can assume to be the same as in the definition of \minizinc. While we omit -the typing rules here for space reasons, we will assume that in well-typed -\microzinc\ programs, the conditions \syntax{} in if-then-else and where -expressions have \mzninline{par} type. +have omitted the definitions of \syntax{} and \syntax{}, +which you can assume to be the same as the definition of \syntax{} +and \syntax{} in the \minizinc\ grammar, see \cref{ch:minizinc-grammar}. +While we omit the typing rules here for space reasons, we will assume that in +well-typed \microzinc\ programs, the conditions \syntax{} in if-then-else +and where expressions have \mzninline{par} type. \begin{figure} \begin{grammar} - ::= * + ::= * - ::= function : ([: ]*) [ = ]; + ::= "function" ":" "(" ["," ]* ")" [ "=" ]";" - ::= | + ::= | - ::= - \alt ( * ) - \alt let { * } in - \alt if then else endif - \alt [ | where ] + ::= + \alt "(" ["," ]* ")" + \alt "let" "{" * "}" "in" + \alt "if" "then" "else" "endif" + \alt "[" "|" "where" "]" + \alt "(" ["," ]* ")" - ::= : [ = ]; - \alt constraint ; + ::= [ "=" ]";" + \alt "(" ["," ]* ")" "=" ";" + \alt "constraint" ";" - ::= in [ , in ]* + ::= ":" + + ::= | "tuple(" ["," ]* ")" + + ::= "in" ["," "in" ]* \end{grammar} -\caption{\label{fig:4-uzn-syntax} Syntax of \microzinc.} + \caption{\label{fig:4-uzn-syntax}Syntax of \microzinc.} \end{figure} \newcommand{\sep}{\rhd} 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 -constraints (this will be explained in detail in \cref{sec:4-nanozinc}, for now -you can assume it is empty). +variable declaration and constraints in the form of calls. The syntax +``\texttt{└──}'' will be used to track dependent constraints (this will be +explained in detail in \cref{sec:4-nanozinc}, for now you can ignore them). \begin{figure} \begin{grammar} - ::= * + ::= * - ::= \(\mapsto\) \(\sep\) * + ::= | - ::= | + ::= "constraint" "(" ["," ]* ")"";" - ::= | true + ::= "var" ":" ";" * - ::= ( * ) + ::= ".." | + \alt "bool" | "int" | "float" | "set of int" + + ::= "└──" \end{grammar} -\caption{\label{fig:4-nzn-syntax} - Syntax of \nanozinc. -} + \caption{\label{fig:4-nzn-syntax}Syntax of \nanozinc.} \end{figure} \subsection{\glsentrytext{minizinc} to @@ -206,50 +213,6 @@ The translation from \minizinc\ to \microzinc\ involves the following steps: arguments are the parameters of the model. \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\).} - -% \While{not at end of this document}{ -% read current\; -% \eIf{understand}{ -% go to next section\; -% current section becomes this one\; -% }{ -% go back to the beginning of current section\; -% } -% } -% \caption{MicrowaveModel} -% \end{algorithm} - - -% \begin{algorithm}[H] -% \KwData{A \minizinc\ expression \(e\) and \(rn\) a function to rename identifiers} -% \KwResult{A \microzinc\ expression \(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)\) -% }{ -% \(c' \longleftarrow \texttt{MicroExpr(\(c, rn\))}\)\; -% \(e_{1}' \longleftarrow \texttt{MicroExpr(\(e_{1}, rn\))}\)\; -% \(e_{2}' \longleftarrow \texttt{MicroExpr(\(e_{2}\), rn)}\)\; -% \(e' \longleftarrow \texttt{if \(c'\) then \(e_{1}'\) else \(e_{2}'\) endif}\) -% } -% } -% \Case{\textup{(call)} \(n(e_{1}, ..., e_{n})\)}{ - -% } -% \lCase{\textup{(ident)} \(id\)} {\(e' \longleftarrow rn(id)\)} -% \lOther{\(e' \longleftarrow e\)} -% } -% \Return{\(e'\)} -% \caption{MicroExpr} -% \end{algorithm} - \begin{example} Consider the following \minizinc\ model, a simple unsatisfiable ``pigeonhole problem'', trying to assign \(n\) pigeons to \(n-1\) holes: @@ -292,7 +255,11 @@ The translation from \minizinc\ to \microzinc\ involves the following steps: For a concrete instance of the model, we can then create a simple \nanozinc\ program that calls \mzninline{main}, for example for \(n=10\): - \nzninline{true @\(\mapsto\)@ main(10) @\(\sep\)@ []}. + + \begin{nzn} + constraint main(10); + \end{nzn} + \end{example} \subsection{Partial Evaluation of \glsentrytext{nanozinc}}\label{sub:4-partial} @@ -364,20 +331,25 @@ 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 - definitions, the resulting \nanozinc\ program could look like this: + Consider the \minizinc\ fragment + + \begin{mzn} + constraint abs(x) > y; + \end{mzn} + + where \mzninline{x} and \mzninline{y} have domain \mzninline{-10..10}. After + rewriting all definitions, the resulting \nanozinc\ program could look like + this: \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] + var -10..10: x; + var -10..10: y; + var int: z; + └── constraint int_abs(x, z); + constraint int_gt(z, y); \end{nzn} + \jip{Adjust text to match the new \nanozinc\ formatting.} 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 its arguments. Evaluating the call \mzninline{abs(x)} introduces a new @@ -652,7 +624,8 @@ 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 constraints directly succeeding the declaration +prepended by \texttt{└── }). \begin{example}\label{ex:4-absreif} The following is a slight variation on the \minizinc\ fragment in @@ -673,15 +646,14 @@ auxiliary definitions (the \mzninline{@\(\sep\phi\)@} part). was introduced for \mzninline{abs(x) > y}: \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] + var true: c; + var -10..10: x; + var -10..10: y; + var int: z; + └── constraint int_abs(x, z); + var bool: b1; + └── constraint int_gt(z, y); + constraint bool_or(b1, c); \end{nzn} Since \mzninline{c} is bound to \mzninline{true}, the disjunction @@ -700,17 +672,16 @@ auxiliary definitions (the \mzninline{@\(\sep\phi\)@} part). is much more compact: \begin{nzn} - c @\(\mapsto\)@ true @\(\sep\)@ [] - x @\(\mapsto\)@ mkvar(-10..10) @\(\sep\)@ [] - y @\(\mapsto\)@ mkvar(-10..10) @\(\sep\)@ [] - true @\(\mapsto\)@ true @\(\sep\)@ [] + var true: c; + var -10..10: x; + var -10..10: y; \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. - + 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. \end{example} +\jip{adjust text to match the new \nanozinc\ syntax} Note how \mzninline{t} acts as a unique name for the result of the let expression (and thus the function call) --- we could not simply have used \mzninline{z}, because then \mzninline{b0} would have kept \mzninline{z} alive. @@ -830,34 +801,29 @@ as \mzninline{constraint f(a)=g(b)}. Let us assume that part of the corresponding \nanozinc\ code looks like this: \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]; + var int: x; + └── constraint f_rel(a, x); + var int: y; + └── constraint g_rel(b, y); + constraint int_eq(x, y); \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 -\mzninline{b0} or \mzninline{b1}, leaving nothing to be substituted. Rather, the -interpreter needs to pick one of the two definitions and \emph{promote} it to -top-level status. Let us assume that the interpreter decides to replace -\mzninline{t1} by \mzninline{t0}. It follows the definition of \mzninline{t1} to -find \mzninline{y}, which is then globally replaced by \mzninline{t0}, and its -definition is removed. The interpreter moves all auxiliary constraints from -\mzninline{t1} into the list of auxiliary constraints of the top-level -\mzninline{true} item, and then removes the \mzninline{int_eq} constraint and -\mzninline{t1}. The resulting \nanozinc\ looks like this: +In this case, simply removing either \mzninline{x} or \mzninline{y} would not be +correct, since that would trigger the removal of the corresponding definition +\mzninline{f_rel(a, x)} or \mzninline{g_rel(b, y)}, leaving nothing to be +substituted. Rather, the interpreter needs to pick one of the two definitions +and \emph{promote} it to top-level status. Let us assume that the interpreter +decides to replace \mzninline{y} by \mzninline{x}. \mzninline{y} is then +globally replaced by \mzninline{x}, and its declaration is removed. The +interpreter moves all auxiliary constraints from \mzninline{y} into the list of +top-level constraints, and then removes the \mzninline{int_eq} constraint. The +resulting \nanozinc\ looks like this: \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]; + var int: x; + └── constraint f_rel(a, x); + constraint g_rel(x, y); + constraint int_eq(x, y); \end{nzn} The process of equality propagation is similar to unification in logic diff --git a/chapters/A1_minizinc_grammar.tex b/chapters/A1_minizinc_grammar.tex index fc7efe6..19903d3 100644 --- a/chapters/A1_minizinc_grammar.tex +++ b/chapters/A1_minizinc_grammar.tex @@ -36,7 +36,7 @@ the rules for identifiers and annotations. \alt \alt - ::= ":" + ::= ":" % Include items ::= "include" @@ -75,7 +75,7 @@ the rules for identifiers and annotations. ::= "test" - ::= "function" ":" + ::= "function" ":" ::= [ "=" ] @@ -88,7 +88,7 @@ the rules for identifiers and annotations. \begin{grammar} % Type-inst expressions - ::= + ::= \alt ::= @@ -115,7 +115,7 @@ the rules for identifiers and annotations. ::= \(regexp\left(\texttt{\$[A-Za-z][A-Za-z0-9\_]*}\right)\) % Array type-inst expressions - ::= "array" [ "," ... ] "of" + ::= "array" [ "," ... ] "of" \alt "list" "of" \end{grammar} @@ -191,16 +191,16 @@ the rules for identifiers and annotations. ::= "false" \alt "true" % Integer literals - ::= \(regexp\left(\texttt{[0-9]+}\right)\) - \alt \(regexp\left(\texttt{0x[0-9A-Fa-f]+}\right)\) - \alt \(regexp\left(\texttt{0o[0-7]+}\right)\) + ::= \(regexp\left(\texttt{\textbackslash{}d+}\right)\) + \alt \(regexp\left(\texttt{0x\textbackslash{}x+}\right)\) + \alt \(regexp\left(\texttt{0o\textbackslash{}O+}\right)\) % Float literals - ::= \(regexp\left(\verb=[0-9]+\.[0-9]+=\right)\) - \alt \(regexp\left(\verb=[0-9]+\.[0-9]+[Ee][-+]?[0-9]+=\right)\) - \alt \(regexp\left(\verb=[0-9]+[Ee][-+]?[0-9]+=\right)\) - \alt \(regexp\left(\verb=0[xX]([0-9a-fA-F]*"."[0-9a-fA-F]+|[0-9a-fA-F]+".")([pP][+-]?[0-9]+)=\right)\) - \alt \(regexp\left(\verb=(0[xX][0-9a-fA-F]+[pP][+-]?[0-9]+)=\right)\) + ::= \(regexp\left(\verb=\d+\.\d+=\right)\) + \alt \(regexp\left(\verb=\d+\.\d+[Ee][-+]?\d+=\right)\) + \alt \(regexp\left(\verb=\d+[Ee][-+]?\d+=\right)\) + \alt \(regexp\left(\verb=0[xX](\x*\.\x+|\x+\.)([pP][+-]?\d+)=\right)\) + \alt \(regexp\left(\verb=(0[xX]\x+[pP][+-]?\d+)=\right)\) % String literals ::= \(regexp\left(\verb=([^"\n\] | \[^\n(])*=\right)\)