Notes from Andreas

assets/listing/intro_open_shop.mod

@@ -8,9 +8,9 @@ var end_time integer >= 0;@\Vlabel{line:intro:var:end}@
 minimize goal: end_time;@\Vlabel{line:intro:goal}@
 subject to job_excl {m in 1..Machines, j1 in 1..Jobs, j2 in j1+1..Jobs}:@\Vlabel{line:intro:con:start}@
 	start[m,j1] + Duration[m,j1] <= start[m,j2]
-	or start[m,j2] + Duration[m,j2] <= start[m,j1];
+	or start[m,j2] + Duration[m,j2] <= start[m,j1];@\Vlabel{line:intro:or:first}@
 subject to machine_excl {j in 1..Jobs, m1 in 1..Machines, m2 in m1+1..Machines}:
 	start[m1,j] + Duration[m1,j] <= start[m2,j]
-	or start[m2,j] + Duration[m2,j] <= start[m1,j];
+	or start[m2,j] + Duration[m2,j] <= start[m1,j];@\Vlabel{line:intro:or:second}@
 subject to push_end_time {m in 1..Machines, j in 1..Jobs}:
 	start[m,j] + Duration[m,j] <= end_time;@\Vlabel{line:intro:con:end}@

chapters/1_introduction.tex

@@ -104,7 +104,7 @@ The \glsxtrshort{ampl} model provides a clear definition of the problem class, b
 Moreover, the process to encode an \instance{} into a \gls{slv-mod} all happens ``behind the scenes''.
 The \solver{} cannot specify how, for example, an operator is best rewritten.
 As such, \glsxtrshort{ampl} cannot rewrite all models for all its \solvers{}.
-For example, since the model in \cref{lst:intro-open-shop} uses the \mzninline{or} operator, it can only be encoded for \solvers{} that support \glsxtrshort{ampl}'s \gls{cp} interface.
+For example, since the model in \cref{lst:intro-open-shop} uses the \mzninline{or} operator (see lines \ref{line:intro:or:first} and \ref{line:intro:or:second}), it can only be encoded for \solvers{} that support \glsxtrshort{ampl}'s \gls{cp} interface.
 
 Although they do support the \gls{rewriting} of models between different problem classes, other traditional \cmls{}, such as \gls{essence} and \glsxtrshort{opl}, exhibit the same problems.
 They do not provide any way to capture common concepts.
@@ -132,7 +132,7 @@ For example, the concepts of one task preceding another and non-overlapping of t
 
 The definition of \texttt{non\_overlap} requires that either task A precedes task B, or vice versa.
 However, unlike the \glsxtrshort{ampl} model, Prolog would not provide this choice to the \solver{}.
-Instead, it enforces one, tests if this works, and it otherwise enforces the other.
+Instead, it enforces one, tests if this works, and otherwise it enforces the other.
 
 This is a powerful mechanism where choices are made in the \gls{rewriting} process, and not in the \solver{}.
 The problem with the mechanism is that it requires a highly incremental interface with the \solver{} that can incrementally post and retract \constraints{}.
@@ -186,7 +186,7 @@ Now, the language is also used to target low-level \solvers{}, such as \gls{sat}
 For them, the encoding of the same \minizinc{} \instance{} results in a much larger \gls{slv-mod}.
 Additionally, \minizinc{} is used in progressively more \gls{meta-optimization} toolchains.
 To a great extent, this is testament to the effectiveness of the language.
-However, as they have become more common, these extended uses have revealed weaknesses of the existing \minizinc{} tool chain.
+However, as they have become more common, these extended uses have revealed weaknesses of the existing \minizinc{} toolchain.
 In particular:
 
 \begin{itemize}
@@ -209,7 +209,7 @@ In particular:
 
 	\item Monolithic \gls{rewriting} is wasteful.
 		When \minizinc{} is used as part of a \gls{meta-optimization} toolchain, there is typically a large base model, common to all sub-problems, and a small set of \constraints{}, which are added or removed in each iteration.
-		In the current tool chain, the whole model must be fully rewritten to a \gls{slv-mod} each time.
+		In the current toolchain, the whole model must be fully rewritten to a \gls{slv-mod} each time.
 		Not only does this repeat all the work done to rewrite the base model, this means a large (sometimes dominant) portion of runtime is simply spent \gls{rewriting} the core model over and over again.
 		This also prevents the \solver{} from carrying over anything it learnt from one problem to the next.
 

chapters/3_rewriting.tex

@@ -44,7 +44,7 @@ The \cmodel{} in the \interpreter{} is internally represented as a \nanozinc{} p
 \nanozinc{} is a slight extension of the \flatzinc{} format.
 The \interpreter{} finishes when it reaches a \gls{slv-mod}.
 
-We have developed a prototype of this tool chain, and present experimental validation that the new tool chain can perform \gls{rewriting} much faster, and produce better models, than the current \minizinc{} \compiler{}.
+We have developed a prototype of this toolchain, and present experimental validation that the new tool chain can perform \gls{rewriting} much faster, and produce better models, than the current \minizinc{} \compiler{}.
 
 \section{\glsentrytext{microzinc} and \glsentrytext{nanozinc}}\label{sec:rew-micronano}
 

chapters/3_rewriting_preamble.tex

@@ -1,6 +1,6 @@
 \noindent{}In this chapter, we develop a new architecture for \gls{rewriting} \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.
+We describe a new \textbf{systematic view of the execution of \minizinc{}} and build on this to propose a new toolchain.
-We show how this tool chain allows us to:
+We show how this toolchain allows us to:
 
 \begin{itemize}
 

chapters/6_conclusions.tex

@@ -60,7 +60,7 @@ This could potentially lead to the ability to prove certain properties of the \g
 Additionally, the architecture introduces reasoning about the transition from \minizinc{} \instances{} to \gls{slv-mod} as two different levels: the transition from \minizinc{} to \microzinc{} and the evaluation of the \nanozinc{} program to create a \gls{slv-mod}.
 In our prototype we have presented techniques to help improve the quality of the \gls{slv-mod}, but many improvements to these techniques and other techniques may be possible.
 Finally, we use \nanozinc{} to track \constraints{} that are introduced to define a \variable{}.
-Although we have showed how this helps when a \variable{} becomes unused, we not yet investigated if the same information might help improve \solver{} performance.
+Although we have showed how this helps when a \variable{} becomes unused, we not yet investigated if the same information can help improve \solver{} performance.
 A possible example of where this information can be useful is found in \gls{cp} \solvers{}.
 In these \solvers{}, a functionally defined \variable{} can become unused when the \constraints{} that use \variable{} have already been \gls{satisfied}, independent of its \gls{fixed} value.
 Like we can remove the defining \constraint{} during \gls{rewriting}, in a \gls{cp} \solver{} we could stop further \gls{propagation} of this \constraint{} and possibly speed up the solving.
@@ -79,7 +79,7 @@ Depending on the context of a \constraint{}, we can decide if a \gls{reif} can b
 We noted that \gls{half-reif} interacts with some existing simplification techniques in the architecture and propose alterations to accommodate them.
 Foremost, \gls{cse} cannot always reuse the same results for identical \constraints{} any more.
 It must now also consider the context of the \constraint{}.
-For \constraints{} were \gls{cse} is triggered in multiple contexts, we propose rules to either use the result that is acceptable in both contexts, or create such a result.
+For \constraints{} where \gls{cse} is triggered in multiple contexts, we propose rules to either use the result that is acceptable in both contexts, or create such a result.
 Using this adjustment, we ensure that identical \constraints{} are not duplicated and re-use the same \gls{cvar}, even when they occurred in different contexts.
 The usage of \gls{propagation} can change the context of a \constraint{} during the \gls{rewriting} process.
 We described how we can communicate this change through the \glspl{cvar} of (half-)\glspl{reif}.