\noindent{}Whether a \constraint{} has to be \gls{reified} is a crucial decision made during \gls{rewriting}.
\minizinc{} allows us to write complex \constraints{} that in the process of \gls{rewriting} result in multiple \constraints{} that reason about each other.
However, determining whether a \constraint{} holds, \(\texttt{b} \leftrightarrow{} c\), requires significantly more effort from the \solver{} than merely enforcing the constraint \(c\).
A \gls{reified} \constraint{} results in a larger \gls{decomp} or a more complex \gls{native} \constraint{}.
It it thus important that \gls{rewriting} avoids the use of \gls{reif}, whenever it is not required.
 
In this chapter we present an extended \gls{reif} analysis to help minimise the required \solver{} effort.
Not only does it consider if a \constraint{} must be \gls{reified} or not, but it also considers whether it could instead be \gls{half-reified}.

The notion of \gls{half-reif} \(\texttt{b} \rightarrow{} c\) for a \constraint{} \(c\) was introduced by \textcite{feydy-2011-half-reif}.
It is shown \gls{half-reif} can relief some of the problems and expenses of the use of \gls{reif}.
It is not always possible, however, to use a \gls{half-reif} instead of a \gls{reif}.
The authors identify the conditions required for its usage and provide an algorithm that rewrites a subset of the \minizinc{} language using the technique.
Crucially, because of the omission of \gls{let} and multiple occurrences of identifiers, this algorithm does not directly generalise to the full \minizinc{} language.
This chapter re-evaluates the usage of \gls{half-reif} and extends the \gls{rewriting} process to fully support \gls{half-reif} in \minizinc{}.

This chapter is organised as follows.
In \cref{sec:half-intro,sec:half-propagation} we introduce the core concepts of \gls{half-reif} and \glspl{propagator} for \gls{half-reified} \constraints{}, as discussed by \textcite{feydy-2011-half-reif}.
An additional benefit of \gls{half-reif} is that its \gls{decomp} can be significantly smaller than the \gls{decomp} of a \gls{reif}.
\Cref{sec:half-decomposition} shows the benefits of \gls{half-reif} when writing \glspl{decomp} for \gls{mip} and \gls{sat} \solvers{}.
In \cref{sec:half-context} we introduce our new context analysis algorithm: a way to determine where \gls{half-reif} can be used in \microzinc{}, and by extension \minizinc{}.
Then, in \cref{sec:half-rewriting}, we elaborate on how the usage of \gls{half-reif} changes the \gls{rewriting} process.
Finally, the effects of \glspl{propagator} for \gls{half-reified} \constraints{} and the automatic introduction of \gls{half-reif} is analysed in \cref{sec:half-experiments}.
