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

Add MiniZinc syntax specification in the appendix

Browse Source
This commit is contained in:
Jip J. Dekker 2021-03-08 11:42:49 +11:00
parent cfd7c5a960
commit 25c23ae378
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
3 changed files with 300 additions and 25 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

41
chapters/4_rewriting.tex
View File

@ -180,20 +180,19 @@ 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. \minizinc\ models
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
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.
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 \pari\
type.
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 \pari\ type.
\begin{figure}
\begin{grammar}
@ -219,11 +218,11 @@ type.
\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
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).
constraints (this will be explained in detail in \cref{sec:4-nanozinc}, for now
you can assume it is empty).
\begin{figure}
\begin{grammar}
@ -270,9 +269,9 @@ The translation from \minizinc\ to \microzinc\ involves the following steps:
\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]
);
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;
@ -304,9 +303,9 @@ The translation from \minizinc\ to \microzinc\ involves the following steps:
} in true;
\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$@ []}.
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$@ []}.
\end{example}
\subsection{Partial Evaluation of NanoZinc}

274
chapters/A1_minizinc_grammar.tex Normal file
View File

@ -0,0 +1,274 @@
%************************************************
\chapter{The Syntax of \glsentrytext{minizinc}}\label{ch:minizinc-grammar}
%************************************************
%
\minizinc\ \autocite{nethercote-2007-minizinc} is a solver-independent
constraint modelling language that is used as the example high-level constraint
modelling language throughout this thesis. This chapter offers a formal
specification of the grammar of the current version \minizinc\ language,
corresponding with \minizinc\ version 2.5.3.
For the convinience of the reader the grammar has been split into several parts.
\Cref{sec:mzn-grammar-items} shows the syntax for the top-level structure of a
model. \Cref{sec:mzn-grammar-typeinst} shows the syntax of type expressions,
used for variable declarations and return types of variables.
\Cref{sec:mzn-grammar-expressions} shows the syntax of expressions used all
other parts of the model. Finally, \Cref{sec:mzn-grammar-expressions} contains
the rules for identifiers and annotations.
\section{Items}
\label{sec:mzn-grammar-items}
\begin{grammar}
% A MiniZinc model
<model> ::= [ <item> ";" ... ]
% Items
<item> ::= <include-item>
\alt <var-decl-item>
\alt <enum-item>
\alt <assign-item>
\alt <constraint-item>
\alt <solve-item>
\alt <output-item>
\alt <predicate-item>
\alt <test-item>
\alt <function-item>
\alt <annotation-item>
<ti-expr-and-id> ::= <ti-expr> ":" <ident>
% Include items
<include-item> ::= "include" <string-literal>
% Variable declaration items
<var-decl-item> ::= <ti-expr-and-id> <annotations> [ "=" <expr> ]
% Enum items
<enum-item> ::= "enum" <ident> <annotations> [ "=" <enum-cases-list> ]
<enum-cases-list> ::= <enum-cases>
\alt <enum-cases-list> "++" <enum-cases>
<enum-cases> ::= "{" <ident> "," ... "}"
\alt <ident> "(" <ident> ")"
% Assign items
<assign-item> ::= <ident> "=" <expr>
% Constraint items
<constraint-item> ::= "constraint" <string-annotation> <expr>
% Solve item
<solve-item> ::= "solve" <annotations> "satisfy"
\alt "solve" <annotations> "minimize" <expr>
\alt "solve" <annotations> "maximize" <expr>
% Output items
<output-item> ::= "output" <expr>
% Annotation items
<annotation-item> ::= "annotation" <ident> <params>
% Predicate, test and function items
<predicate-item> ::= "predicate" <operation-item-tail>
<test-item> ::= "test" <operation-item-tail>
<function-item> ::= "function" <ti-expr> ":" <operation-item-tail>
<operation-item-tail> ::= <ident> <params> <annotations> [ "=" <expr> ]
<params> ::= [ ( <ti-expr-and-id> "," ... ) ]
\end{grammar}
\section{Type Instance Expressions}
\label{sec:mzn-grammar-typeinst}
\begin{grammar}
% Type-inst expressions
<ti-expr> ::= <base-ti-expr>
\alt <array-ti-expr>
<base-ti-expr> ::= <var-par> <opt-ti> <set-ti> <base-ti-expr-tail>
<var-par> ::= "var" \alt "par" \alt <empty>
<opt-ti> ::= "opt" \alt <empty>
<set-ti> ::= "set" "of" \alt <empty>
<base-type> ::= "bool"
\alt "int"
\alt "float"
\alt "string"
<base-ti-expr-tail> ::= <ident>
\alt <base-type>
\alt <ti-variable-expr-tail>
\alt "ann"
\alt \{ <expr> "," ... \}
\alt <num-expr> ".." <num-expr>
% % Type-inst variables
<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>
\alt "list" "of" <base-ti-expr>
\end{grammar}
\section{Expressions}
\label{sec:mzn-grammar-expressions}
\begin{grammar}
% Expressions
<expr> ::= <expr-atom> <expr-binop-tail>
<expr-atom> ::= <expr-atom-head> <expr-atom-tail> <annotations>
<expr-binop-tail> ::= [ <bin-op> <expr> ]
<expr-atom-head> ::= <builtin-un-op> <expr-atom>
\alt "(" <expr> ")"
\alt <ident-or-quoted-op>
\alt "_"
\alt <bool-literal>
\alt <int-literal>
\alt <float-literal>
\alt <string-literal>
\alt <set-literal>
\alt <set-comp>
\alt <array-literal>
\alt <array-literal-2d>
\alt <array-comp>
\alt <ann-literal>
\alt <if-then-else-expr>
\alt <let-expr>
\alt <call-expr>
\alt <gen-call-expr>
<expr-atom-tail> ::= <empty>
\alt <array-access-tail> <expr-atom-tail>
% Numeric expressions
<num-expr> ::= <num-expr-atom> <num-expr-binop-tail>
<num-expr-atom> ::= <num-expr-atom-head> <expr-atom-tail> <annotations>
<num-expr-binop-tail> ::= [ <num-bin-op> <num-expr> ]
<num-expr-atom-head> ::= <builtin-num-un-op> <num-expr-atom>
\alt "(" <num-expr> ")"
\alt <ident-or-quoted-op>
\alt <int-literal>
\alt <float-literal>
\alt <if-then-else-expr>
\alt <let-expr>
\alt <call-expr>
\alt <gen-call-expr>
% Built-in operators
<builtin-op> ::= <builtin-bin-op> \alt <builtin-un-op>
<bin-op> ::= <builtin-bin-op> \alt ‘<ident>‘
<builtin-bin-op> ::= "<->" \alt "->" \alt "<-" \alt "\\/" \alt "xor" \alt "/\\" \alt "<" \alt ">" \alt "<=" \alt ">=" \alt "==" \alt "=" \alt "!="
\alt "in" \alt "subset" \alt "superset" \alt "union" \alt "diff" \alt "symdiff"
\alt ".." \alt "intersect" \alt "++" \alt <builtin-num-bin-op>
<builtin-un-op> ::= "not" \alt <builtin-num-un-op>
% Built-in numeric operators
<num-bin-op> ::= <builtin-num-bin-op> \alt ‘<ident>‘
<builtin-num-bin-op> ::= "+" \alt "-" \alt "*" \alt "/" \alt "div" \alt "mod" \alt "^"
<builtin-num-un-op> ::= "+" \alt "-"
% Boolean literals
<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)\)
% 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)\)
% String literals
<string-contents> ::= \(regexp\left(\verb=([^"\n\] | \[^\n(])*=\right)\)
<string-literal> ::= \" <string-contents> \"
\alt \" <string-contents> "\\(" <string-interpolate-tail>
<string-interpolate-tail> ::= <expr> ")" <string-contents> \"
\alt <expr> ")"<string-contents> "\\(" <string-interpolate-tail>
% Set literals
<set-literal> ::= "{" [ <expr> "," ... ] "}"
% Set comprehensions
<set-comp> ::= "{" <expr> "\alt" <comp-tail> "}"
<comp-tail> ::= <generator> [ "where" <expr> ] "," ...
<generator> ::= <ident> "," ... "in" <expr>
% Array literals
<array-literal> ::= "[" [ <expr> "," ... ] "]"
% 2D Array literals
<array-literal-2d> ::= "[\alt" [ (<expr> "," ...) "\alt" ... ] "\alt]"
% Array comprehensions
<array-comp> ::= "[" <expr> "\alt" <comp-tail> "]"
% Array access
<array-access-tail> ::= "[" <expr> "," ... "]"
% Annotation literals
<ann-literal> ::= <ident> [ "(" <expr> "," ... ")" ]
% If-then-else expressions
<if-then-else-expr> ::= "if" <expr> "then" <expr> [ "elseif" <expr> "then" <expr> ]* "else" <expr> "endif"
% Call expressions
<call-expr> ::= <ident-or-quoted-op> [ "(" <expr> "," ... ")" ]
% Let expressions
<let-expr> ::= "let" "{" <let-item> ";" ... "}" "in" <expr>
<let-item> ::= <var-decl-item>
\alt <constraint-item>
% Generator call expressions
<gen-call-expr> ::= <ident-or-quoted-op> "(" <comp-tail> ")" "(" <expr> ")"
\end{grammar}
\section{Identifiers and Annotations}
\label{sec:mzn-grammar-misc}
\begin{grammar}
% % Miscellaneous
% Identifiers
<ident> ::= \(regexp\left(\texttt{[A-Za-z][A-Za-z0-9\_]*}\right)\)
\alt \(regexp\left(\verb|'[^'\xa\xd\x0]*'|\right)\)
% Identifiers and quoted operators
<ident-or-quoted-op> ::= <ident>
\alt ’<builtin-op>’
% Annotations
<annotations> ::= [ "::" <annotation> ]*
<annotation> ::= <expr-atom-head> <expr-atom-tail>
<string-annotation> ::= "::" <string-literal>
\end{grammar}

10
dekker_thesis.tex
View File

@ -33,9 +33,9 @@ Some ideas and figures included in this thesis have previously appeared in the
following publication:
\begin{refsection}[ownpubs]
\small
\nocite{*} % is local to to the enclosing refsection
\printbibliography[heading=none]
\small
\nocite{*} % is local to to the enclosing refsection
\printbibliography[heading=none]
\end{refsection}
\mainmatter{}
@ -46,8 +46,10 @@ following publication:
\include{chapters/5_half_reif}
\include{chapters/6_incremental}
\backmatter{}
\appendix{}
\include{chapters/A1_minizinc_grammar}
\backmatter{}
\printbibliography{}
% \tableofcontents{}
% \addcontentsline{toc}{chapter}{Contents}