\noindent{}Rewriting a high-level constraint model down into an equivalent solver-level
constraint model might often seem like a simple term rewriting system. In
reality, however, simple rewriting of the model will often result in sub-optimal
solver-level model and this might result in exponentially more work for the
solver. To combat this problem many techniques have been developed 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. And 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 and effectively \textbf{detect and eliminate dead code} introduced by
        functional definitions
\end{itemize}

The new architecture is shown in \Cref{fig:rew-comp}. A constraint model is
first compiled into a smaller constraint language called \microzinc{},
independent of the data. After the \microzinc{} is transformed into a byte code,
it is interpreted with the data to produce \nanozinc\ code, an extension of the
existing \flatzinc\ format. The interpreter can even be made incremental: in
\cref{ch:incremental} we discuss how in meta optimisation, no recompilation is
required.

We have developed a prototype of this tool chain, and present experimental
validation of these advantages. The prototype is still very experimental, but
preliminary results suggest the new tool chain can perform flattening much
faster, and produce better models, than the current \minizinc\ compiler.

This chapter is organised as follows. \Cref{sec:4-micronano} introduces the
\microzinc\ and \nanozinc\ languages, the new intermediate representation we
propose that enables more efficient flattening. \Cref{sec:4-simplification}
describes how we can perform various processing and simplification steps on this
representation, and in \cref{sec:4-experiments} we report on the experimental
results of the prototype implementation. Finally, \Cref{sec:4-conclusion}
presents our conclusions.

\begin{figure}
  \centering
  \includegraphics[width=\linewidth]{assets/img/rew_compilation_structure}
  \caption{\label{fig:rew-comp} The proposed process for the compilation of
    \minizinc\ instances.}
\end{figure}

