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

Tiny change

Browse Source
This commit is contained in:
Jip J. Dekker 2021-07-28 17:39:27 +10:00
parent ce1740308d
commit 72662f0508
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
3 changed files with 9 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
chapters/3_rewriting.tex
View File

@ -476,14 +476,14 @@ The compiler currently supports a significant subset of the full \minizinc{} lan
The missing features, such floating point values and complex output statements, require additional engineering effort, but do not require new technology. The missing features, such floating point values and complex output statements, require additional engineering effort, but do not require new technology.
The \gls{interpreter} evaluates \microzinc{} \gls{byte-code} and \nanozinc{} programs based on the \gls{rewriting} system introduced in this section. The \gls{interpreter} evaluates \microzinc{} \gls{byte-code} and \nanozinc{} programs based on the \gls{rewriting} system introduced in this section.
It can read \parameters{} from a file or via an \gls{api}. It can read \parameters{} from a file or via an \glsxtrshort{api}.
The \gls{interpreter} constructs the call to the \mzninline{main} function, and then performs the \gls{rewriting} into \gls{slv-mod} \nanozinc{}. The \gls{interpreter} constructs the call to the \mzninline{main} function, and then performs the \gls{rewriting} into \gls{slv-mod} \nanozinc{}.
Memory management is implemented using reference counting, which lends itself well to the simplifications discussed in the next section. Memory management is implemented using reference counting, which lends itself well to the simplifications discussed in the next section.
The interpreter is written in around 3.5kLOC of C++ to enable easy embedding into applications and other programming languages. The interpreter is written in around 3.5kLOC of C++ to enable easy embedding into applications and other programming languages.
The framework has the ability to support multiple \solvers{}. The framework has the ability to support multiple \solvers{}.
It can pretty-print the \nanozinc{} code to standard \flatzinc{}, so that any solver currently compatible with \minizinc{} can be used. It can pretty-print the \nanozinc{} code to standard \flatzinc{}, so that any solver currently compatible with \minizinc{} can be used.
Additionally, a direct C++ \gls{api} can be used to connect solvers directly, in order to enable incremental solving. Additionally, a direct C++ \glsxtrshort{api} can be used to connect solvers directly, in order to enable incremental solving.
We revisit this topic in \cref{ch:incremental}. We revisit this topic in \cref{ch:incremental}.
The source code for the complete system will be made available under an open source licence. The source code for the complete system will be made available under an open source licence.
\todo{Actually make source available} \todo{Actually make source available}

8
chapters/4_half_reif.tex
View File

@ -499,15 +499,15 @@ The context in which the result of a call expression is used must also be consid
The (Call) rule, therefore, introduces the \ctxfunc{ident}{ctx} syntax. The (Call) rule, therefore, introduces the \ctxfunc{ident}{ctx} syntax.
This syntax is used to declare that the \compiler{} must introduce a \microzinc{} function variant that rewrites the function call to \(ident\) in the context \(ctx\). This syntax is used to declare that the \compiler{} must introduce a \microzinc{} function variant that rewrites the function call to \(ident\) in the context \(ctx\).
This means that if \(ctx\) is \rootc{}, the \compiler{} can use the function as defined. This means that if \(ctx\) is \rootc{}, the \compiler{} can use the function as defined.
Otherwise, the \compiler{} follows the following steps to try to introduce the most compatible variant of the function: Otherwise, the \compiler{} follows the following steps to try to introduce the most compatible variant of the function.
\begin{enumerate} \begin{enumerate}
\item If a direct definition for \(ctx\) definition exists, then use this definition. \item If a direct definition for \(ctx\) definition exists, then use this definition.
\begin{description} \begin{description}
\item[\posc] \glspl{half-reif} can be defined as \(ident\)\mzninline{_imp}. \item[\posc] \Glspl{half-reif} can be defined as \(ident\)\mzninline{_imp}.
\item[\negc] negations of \glspl{half-reif} can be defined as \(ident\)\mzninline{_imp_neg}. \item[\negc] Negations of \glspl{half-reif} can be defined as \(ident\)\mzninline{_imp_neg}.
\item[\mixc] \glspl{reif} can be defined as \(ident\)\mzninline{_reif}. \item[\mixc] \Glspl{reif} can be defined as \(ident\)\mzninline{_reif}.
\end{description} \end{description}
\item If \(ident\) is a \microzinc{} function with an expression body \(E\), then a copy of the function can be made that is evaluated in the desired context: \ctxeval{E}{ctx}. \item If \(ident\) is a \microzinc{} function with an expression body \(E\), then a copy of the function can be made that is evaluated in the desired context: \ctxeval{E}{ctx}.

6
chapters/5_incremental.tex
View File

@ -784,7 +784,7 @@ To demonstrate the advantage that dedicated incremental methods for \minizinc{}
We consider the use of lexicographic search and round-robin \gls{lns}, each evaluated on a different \minizinc{} model. We consider the use of lexicographic search and round-robin \gls{lns}, each evaluated on a different \minizinc{} model.
We compare our methods against a naive system that repeatedly programmatically changes an \instance{}, rewrites the full \instance{}, and starts a new \solver{} process each time. We compare our methods against a naive system that repeatedly programmatically changes an \instance{}, rewrites the full \instance{}, and starts a new \solver{} process each time.
The solving in our tests is performed by the \gls{gecode} \gls{solver}. The solving in our tests is performed by the \gls{gecode} \gls{solver}.
When using our incremental interface, it is connected using the fully incremental \gls{api}. When using our incremental interface, it is connected using the fully incremental \glsxtrshort{api}.
The naive system and incremental interface use our architecture prototype to rewrite the \instances{}. The naive system and incremental interface use our architecture prototype to rewrite the \instances{}.
Like the previous experiment, the \gls{rbmo} \instances{} are rewritten using the \minizinc{} 2.5.5 \compiler{}, adjusted to rewrite \gls{rbmo} specifications. Like the previous experiment, the \gls{rbmo} \instances{} are rewritten using the \minizinc{} 2.5.5 \compiler{}, adjusted to rewrite \gls{rbmo} specifications.
We compare the time that is required to (repeatedly) rewrite an \instance{} and the time taken by the \solver{}. We compare the time that is required to (repeatedly) rewrite an \instance{} and the time taken by the \solver{}.
@ -815,7 +815,7 @@ They show that both incremental methods have a clear advantage over our naive ba
Although some additional time is spent \gls{rewriting} the \gls{rbmo} models compared to the incremental, it is minimal. Although some additional time is spent \gls{rewriting} the \gls{rbmo} models compared to the incremental, it is minimal.
The \gls{rewriting} of the \gls{rbmo} \instances{} would likely take less time when using the new prototype architecture. The \gls{rewriting} of the \gls{rbmo} \instances{} would likely take less time when using the new prototype architecture.
Between all the methods, solving time is very similar, but \gls{rbmo} seems to have a slight advantage. Between all the methods, solving time is very similar, but \gls{rbmo} seems to have a slight advantage.
We do not notice any benefit from the use of the incremental solver \gls{api}. We do not notice any benefit from the use of the incremental solver \glsxtrshort{api}.
\subsubsection{GBAC} \subsubsection{GBAC}
@ -827,7 +827,7 @@ It should be noted that the \gls{rbmo} method is not guaranteed to apply the exa
\Cref{subfig:inc-cmp-lex} shows the results of applying 1000 \glspl{neighbourhood}. \Cref{subfig:inc-cmp-lex} shows the results of applying 1000 \glspl{neighbourhood}.
In this case there is an even more pronounced difference between the incremental methods and the naive method. In this case there is an even more pronounced difference between the incremental methods and the naive method.
It is surprising to see that the application of 1000 \glspl{neighbourhood} using \gls{incremental-rewriting} still performs very similar to \gls{rewriting} the \gls{rbmo} method. It is surprising to see that the application of 1000 \glspl{neighbourhood} using \gls{incremental-rewriting} still performs very similar to \gls{rewriting} the \gls{rbmo} method.
The solving times are similar between all methods and once again, we do not see any real advantage of the use of the incremental \solver{} \gls{api}. The solving times are similar between all methods and once again, we do not see any real advantage of the use of the incremental \solver{} \glsxtrshort{api}.
The advantage in solve time using \gls{rbmo} is more pronounced here, but it is hard to draw conclusions since the \glspl{neighbourhood} of this method are not exactly the same. The advantage in solve time using \gls{rbmo} is more pronounced here, but it is hard to draw conclusions since the \glspl{neighbourhood} of this method are not exactly the same.
\section{Summary} \section{Summary}