diff --git a/assets/packages.tex b/assets/packages.tex index 739bda9..3e29a36 100644 --- a/assets/packages.tex +++ b/assets/packages.tex @@ -96,7 +96,7 @@ \usepackage{ebproof} % Comments -\newcommand{\jip}[1]{\textcolor{red}{\Big[\textbf{Jip}: #1\Big]}} +\newcommand{\todo}[1]{\textcolor{red}{\Big[\textbf{TODO}: #1\Big]}} % Example environment \usepackage{amsthm} diff --git a/chapters/2_background.tex b/chapters/2_background.tex index fecbc75..cd41f8f 100644 --- a/chapters/2_background.tex +++ b/chapters/2_background.tex @@ -1235,7 +1235,7 @@ For instance, replacing the usage of enumerated types by normal integers. \includegraphics[width=\linewidth]{assets/img/back_compilation_structure} \caption{\label{fig:back-mzn-comp} The compilation structure of the \minizinc\ compiler.} - \jip{adjust to rewriting instead of flatten} + \todo{adjust to rewriting instead of flatten} \end{figure} The middle-end contains the most important two processes: the flattening and the optimisation. diff --git a/chapters/3_rewriting.tex b/chapters/3_rewriting.tex index 5ccad84..5da84ae 100644 --- a/chapters/3_rewriting.tex +++ b/chapters/3_rewriting.tex @@ -489,7 +489,7 @@ We revisit this topic in \cref{ch:incremental}. \textbf{Python bindings} to the framework are provided to enable easy scripting. The source code for the complete system will be made available under an open source license. -\jip{actually make source available} +\todo{actually make source available} \section{NanoZinc Simplification}\label{sec:rew-simplification} @@ -770,7 +770,7 @@ We have created a prototype implementation of the architecture presented in the It consists of a \compiler{} from \minizinc{} to \microzinc{}, and an incremental \microzinc{} \interpreter{} producing \nanozinc{}. The system supports a significant subset of the full \minizinc{} language; notable features that are missing are support for set and float variables, option types, and compilation of model output expressions and annotations. We will release our implementation under an open-source license and can make it available to the reviewers upon request. -\jip{I suppose it is time to release the prototype.} +\todo{I suppose it is time to release the prototype.} The implementation is not optimised for performance yet, but was created as a faithful implementation of the developed concepts, in order to evaluate their suitability and provide a solid baseline for future improvements. In the following we present experimental results on basic \gls{rewriting} performance as well as an comparison with \glspl{interpreter} of other programming languages to demonstrate the efficiency gains that are possible thanks to the new architecture. diff --git a/chapters/3_rewriting_preamble.tex b/chapters/3_rewriting_preamble.tex index 6c2c743..b20b5dd 100644 --- a/chapters/3_rewriting_preamble.tex +++ b/chapters/3_rewriting_preamble.tex @@ -1,4 +1,4 @@ -\noindent{}\jip{This probably needs a ``why?''} +\noindent{}\todo{This probably needs a ``why?''} In this chapter, we revisit the \gls{rewriting} of \minizinc{} into \glspl{slv-mod}. We describe a new \textbf{systematic view of the execution of \minizinc{}} and build on this to propose a new tool chain. diff --git a/chapters/4_half_reif.tex b/chapters/4_half_reif.tex index 6cd6214..ffb8099 100644 --- a/chapters/4_half_reif.tex +++ b/chapters/4_half_reif.tex @@ -9,7 +9,7 @@ \paragraph{Reification - Text from rewriting} -\jip{Adjust with information in the background section. Is there anything specific to the \microzinc{}/\nanozinc{} system?} +\todo{Adjust with information in the background section. Is there anything specific to the \microzinc{}/\nanozinc{} system?} Many constraint modelling languages, including \minizinc{}, not only enable \constraints{} to be globally enforced, but typically also support \constraints{} to be \emph{reified} into a Boolean variable. Reification means that a variable \mzninline{b} is constrained to be true if and only if a corresponding constraint \mzninline{c(...) @@ -47,7 +47,7 @@ Finally, if the stored expression was in reified context and the current context \minizinc{} distinguishes not only between root and reified contexts, but in addition recognises constraints in \emph{positive} contexts, also known as \emph{half-reified} \autocite{feydy-2011-half-reif}. A full explanation and discussion of half-reification can be found in \cref{ch:half-reif}. -\jip{TODO:\ Reification should also be discussed in the background. How can we +\todo{Reification should also be discussed in the background. How can we make this more specific to how it works in \nanozinc{}.} \section{An Introduction to Half Reification} @@ -624,7 +624,7 @@ During the flattening process the contexts assigned to the different expressions \begin{example} \label{ex:half-flatten} - \jip{TODO:\ Replace the previous example. It was too long and complex.} + \todo{Replace the previous example. It was too long and complex.} \end{example} A consequence of the use of \gls{half-reif}, shown in the example, is that it might form so called \emph{implication chains}. @@ -819,7 +819,7 @@ The control \variable is thus used to communicate any change in context. This new predicate can then compiled using the normal methods. \end{example} -\jip{Should we talk about \mixc{} that could have been \posc{}? I'm not sure we correctly do that one at the moment.} +\todo{Should we talk about \mixc{} that could have been \posc{}? I'm not sure we correctly do that one at the moment.} \section{Experiments} \label{sec:half-experiments} @@ -923,7 +923,7 @@ These experiments are conducted using the \gls{gecode} \solver{}, which has prop The \minizinc{} instances are flattened using the \minizinc{} 2.5.5 flattener, which can enable and disable the usage of \gls{half-reif}. The solving of the linearised models is tested using the \gls{cbc} and \gls{cplex} \gls{mip} \solvers{}. -\jip{TODO:\ Extend this section with the \gls{sat} results once they are run.} +\todo{TODO:\ Extend this section with the \gls{sat} results once they are run.} \begin{table} \begin{subtable}[b]{\linewidth} @@ -969,7 +969,7 @@ Similar to \gls{gecode}, the number of implications that is removed is dependent Lastly, the flattening time slightly increases for the linearisation process. Since there are many more constraints, the introduced optimisation mechanisms have an slightly higher overhead. -\jip{TODO:\ The \gls{sat} statistics currently only include 2019. 2020 is still WIP.} +\todo{The \gls{sat} statistics currently only include 2019. 2020 is still WIP.} Finally, statistics for the flattening the instances is shown in \cref{subtab:half-flat-bool}. Like linearisation, the usage of \gls{half-reif} significantly reduces number of constraints and \glspl{reification}. @@ -1013,9 +1013,9 @@ However, we can imagine that the removed constraints might in some cases help th An important technique used by \gls{mip} solvers is to detect certain pattern, such as cliques, during the pre-processing of the \gls{mip} instance. Some patterns might only be detected when using a full \gls{reification}. Furthermore, the performance of \gls{mip} solvers is often dependent on the order and form in which the constraints are given. -\jip{TODO:\ Is there a citation for this?} With the usage of the \gls{aggregation} and \gls{del-rew}, these can be exceedingly different when using \gls{half-reif}. +\todo{Is there a citation for this?} With the usage of the \gls{aggregation} and \gls{del-rew}, these can be exceedingly different when using \gls{half-reif}. -\jip{TODO: \gls{sat} number are still preliminary, but look optimistic. +\todo{\gls{sat} number are still preliminary, but look optimistic. Only one case where the solver time is severely impacted.} % \section{Summary} diff --git a/chapters/5_incremental.tex b/chapters/5_incremental.tex index 5fc7672..6736a94 100644 --- a/chapters/5_incremental.tex +++ b/chapters/5_incremental.tex @@ -473,7 +473,7 @@ In particular, this means that if no choice point was created before the initial \begin{example}\label{ex:6-trail} Let us look again at the resulting \nanozinc\ code from \cref{ex:rew-absreif}: - \jip{Fix example to new syntax} + \todo{Fix example to new syntax} % \begin{nzn} % c @$\mapsto$@ true @$\sep$@ [] % x @$\mapsto$@ mkvar(-10..10) @$\sep$@ [] @@ -484,7 +484,7 @@ In particular, this means that if no choice point was created before the initial Assume that we added a choice point before posting the constraint \mzninline{c}. Then the trail stores the \emph{inverse} of all modifications that were made to the \nanozinc\ as a result of \mzninline{c} (where \(\mapsfrom\) denotes restoring an identifier, and \(\lhd\) \texttt{+}/\texttt{-} respectively denote attaching and detaching constraints): - \jip{Fix example to new syntax} + \todo{Fix example to new syntax} % \begin{nzn} % % Posted c % true @$\lhd$@ -[c] diff --git a/chapters/A2_benchmark.tex b/chapters/A2_benchmark.tex index 83e1730..af29c16 100644 --- a/chapters/A2_benchmark.tex +++ b/chapters/A2_benchmark.tex @@ -145,7 +145,7 @@ In this thesis we use four different versions of the \gls{gecode} solver: In this thesis we use \gls{cplex} version 20.1 under an academic license in our experiments. \paragraph{OpenWBO} is a open source \gls{maxsat} \solver{} \autocite{martins-2014-openwbo}. -In this thesis we use version \jip{xxx} in our experiments. +In this thesis we use version \todo{xxx} in our experiments. The source code for this version can be found here: \begin{center}