From 72662f0508262dadefd874ae13e330641d283b4f Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Wed, 28 Jul 2021 17:39:27 +1000 Subject: [PATCH] Tiny change --- chapters/3_rewriting.tex | 4 ++-- chapters/4_half_reif.tex | 8 ++++---- chapters/5_incremental.tex | 6 +++--- 3 files changed, 9 insertions(+), 9 deletions(-) diff --git a/chapters/3_rewriting.tex b/chapters/3_rewriting.tex index 1438971..dc208a2 100644 --- a/chapters/3_rewriting.tex +++ b/chapters/3_rewriting.tex @@ -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 \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{}. 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 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. -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}. The source code for the complete system will be made available under an open source licence. \todo{Actually make source available} diff --git a/chapters/4_half_reif.tex b/chapters/4_half_reif.tex index 2c06dc3..4a1958a 100644 --- a/chapters/4_half_reif.tex +++ b/chapters/4_half_reif.tex @@ -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. 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. -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} \item If a direct definition for \(ctx\) definition exists, then use this definition. \begin{description} - \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[\mixc] \glspl{reif} can be defined as \(ident\)\mzninline{_reif}. + \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[\mixc] \Glspl{reif} can be defined as \(ident\)\mzninline{_reif}. \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}. diff --git a/chapters/5_incremental.tex b/chapters/5_incremental.tex index b329828..4bbb570 100644 --- a/chapters/5_incremental.tex +++ b/chapters/5_incremental.tex @@ -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 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}. -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{}. 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{}. @@ -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. 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. -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} @@ -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}. 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. -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. \section{Summary}