Add rewriting summary

chapters/4_rewriting.tex

@@ -996,3 +996,44 @@ unoptimised prototype to a mature piece of software.
     instances. \minizinc\ 2.4.3 (x-axis) vs new architecture (y-axis), log-log
     plot. Dots below the line indicate the new system is better.}
 \end{figure}
+
+\section{Summary}%
+\label{sec:rew-summary}
+
+In this chapter, we introduced a systematic view of the execution of \minizinc,
+revisiting the rewriting from high-level \minizinc\ to solver-level \flatzinc.
+We first introduced introduced the intermediate languages \microzinc\ and
+\nanozinc\ and explained how \minizinc\ can be transformed into a set of
+\microzinc\ definitions and a \nanozinc\ program. We then, crucially, discussed
+how to partially evaluate a \nanozinc\ program using \microzinc\ definitions and
+present formal definitions of the rewriting rules applied during partial
+evaluation.
+
+Continuously applying these rules would result in a correct solver-level model,
+but it is unlikely to be the best model for the solver. We, therefore, discuss
+multiple techniques to improve the solver-level constraint model during the
+partial evaluation of \nanozinc. First, we introduce a novel technique to
+eliminate all unused variables and constraints: we track all constraints that
+are introduced only to define a variable. This means we can keep an accurate
+count of when a variable becomes unused by counting only the references to a
+variable in constraints that do not help define it. Then, we discuss the use of
+constraint propagation during the partial evaluation of the \nanozinc\ program.
+This technique can help shrink the domains of the decision variable or even
+combine variables known to be equal. When a redefinition of a constraint
+requires the introspection into the current domain of a variable, it is often
+important to have the tightest possible domain. Hence, we discuss how in
+choosing the the next \nanozinc\ constraint to rewrite, the interpreter can
+sometimes delay the rewriting of certain constraints to ensure the most amount
+of information is available. The final optimisation technique, \gls{cse},
+ensures that we do not create or evaluate the same constraint or function twice
+and reuse variables where possible.
+
+\jip{todo: Aggregation}
+
+Finally, we test the described system using a experimental implementation. We
+compare this experimental implementation against the current \minizinc\
+interpreter, version 2.5.3, and look at both runtime and its memory usage.
+Although the experimental implementation there are instances where the
+experimental implementation uses more memory than the current \minizinc\
+interpreter, it clearly outperforms the current \minizinc\ interpreter in terms
+of time.