Work on the rewriting introduction

chapters/4_rewriting.tex

@@ -2,10 +2,36 @@
 \chapter{Rewriting Constraint Modelling Languages}\label{ch:rewriting}
 %************************************************
 
-In this chapter  We describe a new \textbf{systematic view
+Rewriting a high-level constraint model and equivalent solver-level constraint
-  of the execution of \cmls}, and build on this to propose a new tool chain. We
+model might often seems like a simple application of a term rewriting system. In
-show how this tool chain allows us to
+reality, however, eagerly rewriting the the constraints in the model will often
+result in sub-optimal solver-level model and this might result in exponentially
+more work for the solver. Therefore, there are many techniques that can be used
+to create more efficient solver-level models such as: continuously updating
+variable domains according to the constraints, correctly resolving constraint
+sub-typing when variables get fixed, removing any variables and constraints that
+have become unused, detecting duplicate constraints, and reusing duplicate
+functional definitions.
 
+The application of all these optimisations can, however, be time intensive
+during the rewriting process. Although this was not a problem when high-level
+\cmls\ were targeting \gls{cp} solvers, where the solver-level constraint model
+stays relatively small, this poses a big problem for \gls{mip} and \gls{sat}
+solvers, whose solver-level constraint models are significantly larger.
+
+In this chapter, we revisit the rewriting of high-level \cmls\ into solver-level
+constraint models. We describe a new \textbf{systematic view of the execution of
+  \minizinc{}} and build on this to propose a new tool chain. We show how this
+tool chain allows us to:
+
+\begin{itemize}
+  \item efficiently rewrite high-level constraint models with \textbf{minimal
+        overhead}.
+  \item easily integrate a range of \textbf{optimisation and simplification}
+        techniques,
+  \item effectively \textbf{detect and eliminate dead code} introduced by
+        functional definitions
+\end{itemize}
 
 The new architecture is shown in \Cref{sfig:4-newarch}. A constraint model is
 first compiled to byte code (called \microzinc), independent of the data. The
@@ -141,7 +167,8 @@ The translation from \minizinc\ to \microzinc\ involves the following steps:
         function declaration and each call site
   \item Move all top-level variable declarations and constraints into a let
         expression in the body of a new function called \mzninline{main}, whose
-        arguments are the parameters of the model.
+        arguments are the parameters of the model and which returns a fresh
+        Boolean variable.
 \end{enumerate}
 
 \begin{example}