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

Initial syntax swtich for MicroZinc and NanoZinc

Browse Source
This commit is contained in:
Jip J. Dekker 2021-03-18 13:25:48 +11:00
parent 79f115597d
commit 4c54084bf6
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
3 changed files with 112 additions and 146 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
assets/packages.tex
View File

@ -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}}

230
chapters/4_rewriting.tex
View File

@ -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{<type-inst>} and \syntax{<ident>}, 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{<exp>} in if-then-else and where
expressions have \mzninline{par} type.
have omitted the definitions of \syntax{<mzn-type-inst>} and \syntax{<ident>},
which you can assume to be the same as the definition of \syntax{<type-inst>}
and \syntax{<ident>} 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{<exp>} in if-then-else
and where expressions have \mzninline{par} type.
\begin{figure}
\begin{grammar}
<model> ::= <fun-decl>*
<model> ::= <fun-decl>*
<fun-decl> ::= function <type-inst>: <ident>([<type-inst>: <ident>]*) [ = <exp> ];
<fun-decl> ::= "function" <type-inst>":" <ident>"(" <param> ["," <param>]* ")" [ "=" <exp> ]";"
<literal> ::= <constant> | <ident>
<literal> ::= <constant> | <ident>
<exp> ::= <literal>
\alt <ident>( <literal>* )
\alt let { <item>* } in <exp>
\alt if <exp> then <exp> else <exp> endif
\alt [ <exp> | <gen-exp> where <exp> ]
<exp> ::= <literal>
\alt <ident>"(" <literal> ["," <literal>]* ")"
\alt "let" "{" <item>* "}" "in" <exp>
\alt "if" <exp> "then" <exp> "else" <exp> "endif"
\alt "[" <exp> "|" <gen-exp> "where" <exp> "]"
\alt "(" <exp> ["," <exp>]* ")"
<item> ::= <type-inst>: <ident> [ = <exp> ];
\alt constraint <exp>;
<item> ::= <param> [ "=" <exp> ]";"
\alt "(" <param> ["," <param>]* ")" "=" <exp> ";"
\alt "constraint" <exp>";"
<gen-exp> ::= <ident> in <exp> [ , <ident> in <exp> ]*
<param> ::= <type-inst>":" <ident>
<type-inst> ::= <mzn-type-inst> | "tuple(" <mzn-type-inst> ["," <mzn-type-inst>]* ")"
<gen-exp> ::= <ident> "in" <exp> ["," <ident> "in" <exp> ]*
\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\) <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).
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}
<nzn> ::= <nzn-def>*
<nzn> ::= <nzn-item>*
<nzn-def> ::= <nzn-result> \(\mapsto\) <nzn-bind> \(\sep\) <ident>*
<nzn-item> ::= <nzn-def> | <nzn-con>
<nzn-bind> ::= <ident> | <nzn-call>
<nzn-con> ::= "constraint" <ident>"(" <literal> ["," <literal>]* ")"";"
<nzn-result> ::= <ident> | true
<nzn-var> ::= "var" <nzn-dom> ":" <ident> ";" <nzn-bind>*
<nzn-call> ::= <ident>( <literal>* )
<nzn-dom> ::= <constant> ".." <constant> | <constant>
\alt "bool" | "int" | "float" | "set of int"
<nzn-bind> ::= "└──" <nzn-con>
\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

24
chapters/A1_minizinc_grammar.tex
View File

@ -36,7 +36,7 @@ the rules for identifiers and annotations.
\alt <function-item>
\alt <annotation-item>
<ti-expr-and-id> ::= <ti-expr> ":" <ident>
<ti-expr-and-id> ::= <type-inst> ":" <ident>
% Include items
<include-item> ::= "include" <string-literal>
@ -75,7 +75,7 @@ the rules for identifiers and annotations.
<test-item> ::= "test" <operation-item-tail>
<function-item> ::= "function" <ti-expr> ":" <operation-item-tail>
<function-item> ::= "function" <type-inst> ":" <operation-item-tail>
<operation-item-tail> ::= <ident> <params> <annotations> [ "=" <expr> ]
@ -88,7 +88,7 @@ the rules for identifiers and annotations.
\begin{grammar}
% Type-inst expressions
<ti-expr> ::= <base-ti-expr>
<type-inst> ::= <base-ti-expr>
\alt <array-ti-expr>
<base-ti-expr> ::= <var-par> <opt-ti> <set-ti> <base-ti-expr-tail>
@ -115,7 +115,7 @@ the rules for identifiers and annotations.
<ti-variable-expr-tail> ::= \(regexp\left(\texttt{\$[A-Za-z][A-Za-z0-9\_]*}\right)\)
% Array type-inst expressions
<array-ti-expr> ::= "array" [ <ti-expr> "," ... ] "of" <base-ti-expr>
<array-ti-expr> ::= "array" [ <type-inst> "," ... ] "of" <base-ti-expr>
\alt "list" "of" <base-ti-expr>
\end{grammar}
@ -191,16 +191,16 @@ the rules for identifiers and annotations.
<bool-literal> ::= "false" \alt "true"
% Integer literals
<int-literal> ::= \(regexp\left(\texttt{[0-9]+}\right)\)
\alt \(regexp\left(\texttt{0x[0-9A-Fa-f]+}\right)\)
\alt \(regexp\left(\texttt{0o[0-7]+}\right)\)
<int-literal> ::= \(regexp\left(\texttt{\textbackslash{}d+}\right)\)
\alt \(regexp\left(\texttt{0x\textbackslash{}x+}\right)\)
\alt \(regexp\left(\texttt{0o\textbackslash{}O+}\right)\)
% Float literals
<float-literal> ::= \(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)\)
<float-literal> ::= \(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
<string-contents> ::= \(regexp\left(\verb=([^"\n\] | \[^\n(])*=\right)\)