\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:rew-experiments} we report on the experimental results of the prototype implementation.

\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}

