%************************************************
\chapter{Half Reification}\label{ch:half-reif}
%************************************************

\input{chapters/4_half_reif_preamble}

\section{Introduction to Half Reification}

The complex expressions language used in \cmls{}, such as \minizinc{}, often require the use of \gls{reification} in the flattening process to reach a solver level constraint model.
If the Boolean expression \mzninline{pred(...)} is seen in a non-root context, then a new Boolean \variable{} \mzninline{b} is introduced to replace the expression.
The flattener then enforces a \constraint{} \mzninline{pred_reif(...,b)}, which binds the \variable{} to be the \emph{truth-value} of the expression (\ie\ \mzninline{b <-> pred(...)}).

A weakness of reification is that each reified version of a constraint requires further implementation to create, and indeed most solvers do not provide any reified versions of their \gls{global} \constraints{}.

\begin{example}\label{ex:hr-alldiff}
	Consider the complex constraint

	\begin{mzn}
		constraint i <= 4 -> all_different([i,x-i,x]);
	\end{mzn}

	The usual flattened form would be

	\begin{mzn}
		constraint int_le_reif(i, 4, b1);   % b1 holds iff i <= 4
		constraint int_minus(x, i, t1);     % t1 = x - i
		constraint all_different_reif([i,t1,x], b2);
		constraint bool_clause([b2], [b1])  % b1 implies b2
	\end{mzn}

	but no solver we are aware of implements the third primitive constraint.
	%
	\footnote{Although there are versions of soft \mzninline{all_different}, they
	do not define this form.}
\end{example}

Reified \gls{global} \constraints{} are not implemented because a reified constraint \mzninline{b <-> pred(...)} must also implement a propagator for \mzninline{not pred(...)} (in the case that \mzninline{b = false}).
While for some global \constraints{}, \eg\ \mzninline{all_different}, this may be reasonable to implement, for most, such as \texttt{cumulative}, the task seems to be very difficult.

Another weakness of the reification is that it may keep track of more information than is required.
In a typical solver, the first reified constraint \mzninline{b1 <-> i <= 4} will wake up whenever the upper bound of \texttt{i} changes in order to check whether it should set \texttt{b1} to \mzninline{true}.
But setting \mzninline{b1} to \mzninline{true} will \emph{never} cause any further propagation.
There is no reason to check this.

This is particularly important when the target solver is a mixed integer programming solver.
In order to linearise a reified linear constraint we need to create two linear \constraints{}, but if we are only interested in half of the behaviour we can manage this with one linear constraint.

\begin{example}
  Consider the constraint \mzninline{b1 <-> i <= 4}, where \texttt{i} can take
  values in the domain \mzninline{0..10} then its linearisation is

  \begin{mzn}
    constraint i <= 10 - 6 * b1;   % b1 -> i <= 4
    constraint i >= 5 - 5 * b1;    % not b1 -> i >= 5
  \end{mzn}

	But in the system of \constraints{} where this constraint occurs knowing that
	\texttt{b1} is 0 will never cause the system to fail, hence we do not need to
	keep track of it.
%
	We can simply use the second constraint in the linearisation, which always
	allows that \texttt{b1} takes the value 0.
\end{example}

The simple flattening used above treats partial functions in the following
manner.
%
Application of a partial function to a value for which it is not defined gives
value \undefined, and this \undefined\ function percolates up through every
expression to the top level conjunction, making the model unsatisfiable.
%
For the example
%
\jip{TODO:\ What goes here???}

In this chapter we study the usage of \gls{half-reif}. \gls{half-reif} follows
from the notion that in many cases it might be sufficient to use the logical
implication of an expression, \mzninline{b -> pred(...)}, instead of the
logical equivalence, \mzninline{b <-> pred(...)}. Flattening with
\gls{half-reif} is an approach that improves upon all these weaknesses of
flattening with \emph{full} reification.

\begin{itemize}
	\item Half reified \constraints{} add no burden to the solver writer; if they
		have a propagator for constraint \mzninline{pred(....)} then they can
		straightforwardly construct a half reified propagator for \mzninline{b ->
		pred(...)}.

	\item Flattening with \gls{half-reif} can produce smaller linear models when
		used with a mixed integer programming solver.

	\item Half reified \constraints{} \mzninline{b -> pred(...)} can implement fully
		reified \constraints{} without any loss of propagation strength (assuming
		reified \constraints{} are negatable). \jip{TODO:\ should this still be here?}

	\item Flattening with half reification can naturally produce the relational
		semantics when flattening partial functions in positive contexts.
		\jip{TODO:\ should this still be here?}

	\item Flattening with half reification can produce more efficient propagation
		when flattening complex \constraints{}. \jip{TODO:\ should this still be
		here?}
\end{itemize}

The remainder of the chapter is organised as follows.
\Cref{sec:half-propagation} discusses the propagation of half-reified \constraints{}.
\Cref{sec:half-decomposition} discusses the decomposition of half-reified constraint.
\Cref{sec:half-context} introduces the notion of context analysis: a way to determine if \gls{half-reif} can be used for a certain expression.
Finally, \cref{sec:half-flattening} explains how this information can be used during the flattening process.

\section{Propagation and Half Reification}%
\label{sec:half-propagation}

The tasks of a propagator for any constraint can logically be split into two tasks:

\begin{enumerate}
	\item To \(check\) if the constraint can still be satisfied (and otherwise \emph{fail} the current state)
	\item To \(prune\) values from the \glspl{domain} of \variables{} that would violate the constraint.
\end{enumerate}

When creating a propagator for the \gls{half-reif} of a constraint, it can be constructed from these two tasks.
The half-reified propagator is dependent on an additional argument \(b\), which is a Boolean \variable{}.
The Boolean \variable{} can be in three states, it can currently not have been assigned a value, it can be assigned \mzninline{true}, or it can be assigned \mzninline{false}.
Given \(b\), \(check\), and \(prune\), \cref{alg:half-prop} shows pseudo code for the propagation of the \gls{half-reif} of the constraint.

\begin{algorithm}
	
	\KwIn{A function \(check\), that returns false when the constraint \(c\) cannot be satisfied, a function \(prune\), that eliminates values from \variable{} \glspl{domain} that violate the constraint \(c\), and a Boolean control \variable{} \(b\).
	}
	\KwResult{This pseudo code propagates the \gls{half-reif} of \(c\) (\ie{} \(b \implies\ c\)).}

	\BlankLine{}
	\If{\(b\) {\normalfont is unassigned} }{
		\If{\(\neg{}check()\)}{
			\(b \longleftarrow \) \mzninline{false}\;
		}
	}
	\If{\(b = \) \mzninline{true}}{
		\(prune()\)\;
	}

	\caption{\label{alg:half-prop} Propagation pseudo code for the \gls{half-reif} of a constraint \(c\), based on the propagator for \(c\).}
\end{algorithm}

Logically, the creation of propagators for \glspl{half-reif} can always follow this simple principle.
In practice, however, this is not always possible.
In some cases, propagators do not explicitly define \(check\) as a separate step.
Instead, this process can be implicit.
The propagator merely prunes the \glspl{domain} of the \variables{}.
When a \gls{domain} is found to be empty, then the propagator fails the current state.
It is not possible possible to construct the half-reified propagator from such an implicit \(check\) operation.
Instead a new explicit \(check\) method has to be devised to implement the propagator of the \gls{half-reif}.

In \cref{sec:half-experiments} we assess the implementation of propagators for the \glspl{half-reif} of \mzninline{all_different} and \mzninline{element}.
Both propagators are designed and implemented in \gls{chuffed} according to the principle explained above.

\begin{itemize}
	\item custom implemented half-reified propagations.
	\item benefits
	\item downside
	\item experimental results
\end{itemize}

Another weakness of the reification is that it may keep track of more information than is required.
In a typical solver, the first reified constraint \mzninline{b1 <-> i <= 4} will wake up whenever the upper bound of \texttt{i} changes in order to check whether it should set \texttt{b1} to \mzninline{true}.
But setting \mzninline{b1} to \mzninline{true} will \emph{never} cause any further propagation.
There is no reason to check this.

A propagation engine gains certain advantages from \gls{half-reif}, but also may suffer certain penalties.
Half reification can cause propagators to wake up less frequently, since variables that are fixed to true by full reification will never be fixed by half reification.
This is advantageous, but a corresponding disadvantage is that variables that are fixed can allow the simplification of the propagator, and hence make its propagation faster.

When full reification is applicable (where we are not using half reified predicates) an alternative to half reification is to implement full reification \mzninline{x <-> pred(...)} by two half reified propagators \mzninline{x -> pred(...)}, \mzninline{y \half \neg pred(...)}, \mzninline{x <-> not y}.
This does not lose propagation strength.
For Booleans appearing in a positive context we can make the propagator \mzninline{y -> not pred(...)} run at the lowest priority, since it will never cause failure.
Similarly in negative contexts we can make the propagator \mzninline{b -> pred(...)} run at the lowest priority.
This means that Boolean variables are still fixed at the same time, but there is less overhead.

\section{Decomposition and Half Reification}%
\label{sec:half-decomposition}

The use of \gls{half-reif} does not only offer a benefit when a propagator for the half-reified constraint is available.
It can also be beneficial in the decomposition of constraints.
Compared to full \gls{reification}, the decomposition of a \gls{half-reif} does not need to keep track of as much information.
In particular, this can be beneficial when the target \solver{} is a \gls{mip} or \gls{sat} solver.
The decompositions for these solver technologies often explicitly encode reified constraints using two implications.
If, however, a \gls{reification} is replaced by a \gls{half-reif}, then only one of these implication is required.

\begin{example}

	Consider the \gls{reification} of the \constraint{} \mzninline{i <= 4} using the control variable \mzninline{b}, where \mzninline{i} can take values in the domain \mzninline{0..10}.
	If the target solver is a \gls{mip} solver, then this \gls{reification} would be linearised.
	It would take the following form:

  \begin{mzn}
    constraint i <= 10 - 6 * b;   % b -> i <= 4
    constraint i >= 5 - 5 * b;    % not b -> i >= 5
  \end{mzn}

	Instead, if we could determine that the \constraint{} could be half-reified, then the linearisation could be simplified to only the first constraint.
\end{example}

The same principle can be applied all throughout the linearisation process.
Ultimately, \minizinc{}'s linearisation library rewrites most \glspl{reification} in terms of implied less than or equal to constraint.
For all these \glspl{reification}, its replacement by a \gls{half-reif} can remove half of the implications required for the \gls{reification}.

For \gls{sat} solvers, a decomposition for a \gls{half-reif} can be created from its regular decomposition.
Any constraint \(c\) will decompose into \gls{cnf}:
\[ c = \forall_{i} \exists_{j} lit_{ij} \]
The \gls{half-reif}, with control variable \(b\), could then be encoded as:
\[ b \implies c = \forall_{i} \neg b \lor \exists_{j} lit_{ij} \]
The transition from the \gls{cnf} of the regular constraint to its \gls{half-reif} only adds a single literal to each clause.

It is, however, not as straightforward to construct its full \gls{reification}. 
In addition to the half-reified \gls{cnf}, a generic \gls{reification} would require the reverse implication, \(\neg b \implies \neg c\).
Based on the \gls{cnf} of \(c\), this would result in the following logical formula: 
\[ \neg b \implies \neg c = \forall_{i} b \lor \neg \exists_{j} lit_{ij} \]
This formula, however, is no longer a direct set of clauses.
Rewriting this formula into \gls{cnf} would result in:
\[ \neg b \implies \neg c = \forall_{i,j} b \lor lit_{ij} \]
This adds a new binary clause for every literal in the original \gls{cnf}.
This overhead can be avoided when using \gls{half-reif}.
\jip{TODO: it would be great to conclude here that all these clauses are unnecessary in a positive context, since \(b\) would never be set to false.}

According to the principles above, decomposition libraries for the full \minizinc{} language have been implemented for \gls{mip} and \gls{sat} solvers.
In \cref{sec:half-experiments} we asses the effects when flattening with \gls{half-reif}.

\section{Context Analysis}%
\label{sec:half-context}

\Gls{half-reif} can be used instead of full \gls{reification} when the \gls{reification} can never be forced to be false.
We see this in, for example, a disjunction \(a \lor b\).
No matter the value of \(a\), setting the value of \(b\) to be true can never make the overall expression false.
At any \(b\) is thus never forced to be false.
This requirement follows from the difference between implication and logical equivalences.
Setting the left hand side of a implication to false, does not influence the value on the right hand side.
So if we know that this is never required in the overall expression, then using an implication instead of a logical equivalence, \ie a \gls{half-reif} instead of a full \gls{reification}, does not change the meaning of the constraint.

This property can be extended to include non-Boolean expressions.
Since Boolean expressions in \minizinc{} can be used in, for example, integer expressions, we can apply similar reasoning to these types of expressions.
For example the left hand side of the constraint 

\begin{mzn}
	constraint count(x in arr)(x = 5) > 5; 
\end{mzn}

is an integer expression that contains the Boolean expression \mzninline{x = 5}.
Since the increasing left hand side of the constraint will only ever help satisfy the constraint, the expression \mzninline{x = 5} will never forced to be false.
This means that we can half-reify the expression.

To systematically analyse whether Booelean expressions can be half-reified, we introduce extra distinctions in the context of expressions.
Before, we would merely distinguish between \rootc{} context and \emph{non-root} context.
Now, we will categorise the latter into:

\begin{description}

	\item[\posc{} context] when an expression must reach \emph{at least} a certain value to satisfy its enclosing constraint.
		The expression is never forced to take a lower value.

	\item[\negc{} context] when an expression can reach \emph{at most} a certain value to satisfy its enclosing constraint.
		The expression is never forced to take a higher value.

	\item[\mixc{} context] when an expression must take an \emph{exact value}, be within a \emph{specified range} or when during flattening it cannot be determined whether the expression must be increased or decreased to satisfy the enclosing constraint.

\end{description}

As previously explained, \gls{half-reif} can be used for expressions in \posc{} context.
Although expressions in a \negc{} context cannot be directly half-reified, the negation of a expression in a \negc{} context can be half-reified.
Consider, for example, the constraint

\begin{mzn}
	constraint b \/ not (x = 5);
\end{mzn}

The expression \mzninline{x = 5} is in a \negc{} context.
Although a \gls{half-reif} cannot be used directly, in some cases the solver can negate the expression which are then placed in a \posc{} context.
Our example can be transformed into:

\begin{mzn}
	constraint b \/ x != 5;
\end{mzn}

The transformed expression, \mzninline{x != 5}, is now in a \posc{} context.
We can also speak of this process as ``pushing the negation inwards''.

Expressions in a \mixc{} context are in a position where \gls{half-reif} is impossible.
Only full \gls{reification} can be used for expressions in that are in this context.
This occurs, for example, when using an exclusive or expression in a constraint.
The value that one side must take directly depends on the value that the other side takes.
Each side can thus be forced to be true or false.
The \mixc{} context can also be used as a ``fall back'' context.
If it cannot be determined if an expression is in a \posc{} or \negc{} context, then it is always safe to say the expression is in a \mixc{} context.

When taking into account the possible undefinedness of an expression, every expression in a \minizinc{} model has two different contexts: the context in which the expression itself occurs, its \emph{value context}, and the context in which the partiality of the expression is captured, its \emph{partiality context}.
As described in \cref{subsec:back-mzn-partial}, \minizinc{} uses relational semantics of partial values.
This means that if a function does not have a result, then its nearest enclosing Boolean expression is set to false.
In practice, this means that a condition that tests if the function will return a value is added to the nearest enclosing Boolean expression.
The \emph{partiality} context is the context in which this condition is placed.

The context of an expression cannot always be determined by merely considering \minizinc\ expressions top-down.
Expressions bound to a variable can be used multiple times in expressions that influence their context.

\begin{example}
	Consider the following \minizinc\ fragment.

	\begin{mzn}
		constraint let {
			var bool: x = pred(a, b, c);
		} in y -> x /\ x -> z;
	\end{mzn}

	The predicate call \mzninline{pred(a, b, c)} is bound to the variable \mzninline{x}.
	The call is in \posc\ context, and can be half-reified, if the variable \mzninline{x} is only used in \posc{} context.
	Although this is the case in the left side of the conjunction, the other side uses \mzninline{x} in a \negc{} context.
	This means that \mzninline{pred(a, b, c)} is in a \mixc{} context, and must fully reified.
\end{example}

Note that an alternative approach for this example would be to replace the identifier with its definition.
It would then be possible half-reify the call and the negation of the call.
Although this would increase the use of \gls{half-reif}, it should be noted that the propagation of these two \glspl{half-reif} would be equivalent to propagating the full \gls{reification} of the call.
In this scenario, we prefer to create the full \gls{reification} as it decreases the number of \variables{} and \constraint{} in the model.

\subsection{Automated analysis}%
\label{subsec:half-automated}

In the architecture introduced in \cref{ch:rewriting}, contexts of the expressions can be determined automatically.
The analysis is best performed during the compilation process from \minizinc{} to \microzinc{}, instead of during the \microzinc{} interpretation, since it requires knowledge about all usages of certain \variable{} at the same time.
Without loss of generality we can define the context analysis process for \microzinc{} models.
This has the advantage that the value and partiality have already been explicitly separated and no longer requires special handling.

We describe the context analysis performed on the \microzinc{} syntax in the form of inference rules.
The full set of rules appears in \cref{fig:half-analysis-expr,fig:half-analysis-it}.
Each rules describe how an expression is found in a context \(ctx\), above the line, changes the context of subordinate expressions, below the line.
The syntax \ctxeval{e}{ctx} is used to assert that the expression \(e\) is evaluated in the context \(ctx\).
We now specify two context transformations that will be used in further algorithms to transition between different contexts: \changepos{} and \changeneg{}.
The behaviour of these transformations is shown in \cref{fig:half-ctx-trans}.

\begin{figure*}
	\begin{center}
		\begin{tabular}{ccc}
			\(
			\begin{array}{lcl}
				\changepos \rootc & = & \posc \\
				\changepos \posc  & = & \posc \\
				\changepos \negc  & = & \negc \\
				\changepos \mixc  & = & \mixc
			\end{array}
			\)
			& ~ &
			\(
			\begin{array}{lcl}
				\changeneg \rootc & = & \negc \\
				\changeneg \posc  & = & \negc \\
				\changeneg \negc  & = & \posc \\
				\changeneg \mixc  & = & \mixc
			\end{array}
			\)
		\end{tabular}
	\end{center}
	\caption{\label{fig:half-ctx-trans} Definitions of the \changepos{} and \changeneg{} context transitions.}
\end{figure*}

\begin{figure*}
  \centering
  \begin{prooftree}
		\hypo{\ctxeval{x}{ctx}}
		\infer1[(Ident)]{\text{pushCtx}(x, ctx)}
  \end{prooftree} \\
  \bigskip
  \begin{prooftree}
		\hypo{\ctxeval{ident\texttt{(} e_{1}, \ldots, e_{n} \texttt{)}}{ctx}}
		\hypo{\text{argCtx}(ident, ctx) = \tuple{ ctx'_{1}, \ldots, ctx'_{n}}}
		\infer2[(Call)]{\ctxfunc{ident}{ctx},~\ctxeval{e_{1}}{ctx'_{1}},~\ldots,~ \ctxeval{e_{n}}{ctx'_{n}}}
  \end{prooftree} \\
  \bigskip
  \begin{prooftree}
		\hypo{\ctxeval{x\texttt{[}i\texttt{]}}{ctx}}
		\infer1[(Access)]{\ctxeval{x}{\changepos{}ctx}}
  \end{prooftree} \\
  \bigskip
  \begin{prooftree}
		\hypo{\ctxeval{\texttt{if }b\texttt{ then } e_{1} \texttt{ else } e_{2} \texttt{ endif}}{ctx}}
		\infer1[(ITE)]{\ctxeval{e_{1}}{\changepos{}ctx},~\ctxeval{e_{2}}{\changepos{}ctx}}
  \end{prooftree} \\
  \bigskip
  \begin{prooftree}
		\hypo{\ctxeval{\texttt{[}e~\texttt{|}~G\texttt{]}}{ctx}}
		\infer1[(Compr)]{\ctxeval{e}{ctx}}
  \end{prooftree} \\
  \bigskip
  \begin{prooftree}
		\hypo{\ctxeval{\texttt{[}e_{1}, \ldots, e_{n}\texttt{]}}{ctx}}
		\infer1[(Arr)]{\ctxeval{e_{1}}{ctx}, \ldots, \ctxeval{e_{n}}{ctx}}
  \end{prooftree}
	\caption{\label{fig:half-analysis-expr} Context inference rules for \microzinc\ expressions.}
\end{figure*}

\Cref{fig:half-analysis-expr} shows the inference rules for all \microzinc{} expressions, apart from let expressions.
The first rule, (Ident), is unique in the sense that the context of an identifier does not directly affects any sub-expressions.
Instead every context in which the identifier are found are collected and will be processed when evaluating the corresponding declaration.
Note that the presented inference rules do not have any explicit state object.
Instead, we introduce the functions ``pushCtx'' and ``collectCtx''.
These functions track and combine the contexts in which an value is used in an implicit global state.

Most changes in the context of \microzinc{} expressions stem from the consequent (Call) rule.
A call expression can change the context in which its arguments should be evaluated.
As an input to the inference process, a ``argCtx'' function is used to give the context of the arguments of a function, given the function itself and the context of the call.
A definition for this function for the \minizinc\ operators can be found in \cref{alg:arg-ctx}.\footnote{We use \minizinc\ operator syntax instead of \microzinc{} identifiers for brevity and clarity.}

Although a standard definition for the ``argMax'' function may cover the most common cases, it does not cover user-defined functions stemming from \minizinc{}.
To address this issue, we introduce the \minizinc{} annotations \mzninline{promise_ctx_monotone} and \mzninline{promise_ctx_antitone} to represent the operations \changepos{} and \changeneg{} respectively.
When a function argument is annotated with one of these annotations, the context of the argument in a call in context \(ctx\) is transformed with the operation coressponding to the annotation (\eg\ \(\changepos{}ctx\) or \(\changeneg{}ctx\)).
If a function argument is not annotated, then the argument is evaluated in \mixc context.

\begin{example}

	Consider the following user-defined \minizinc\ implementation of a logical implication.

	\begin{mzn}
		predicate impli(
			var bool: x ::promise_ctx_antitone,
			var bool: y ::promise_ctx_monotone
		) =
			not x \/ y;
	\end{mzn}

	The annotations placed on the argument of the \mzninline{impli} function will apply the same context transformations as a direct \minizinc\ implication, as shown in \cref{alg:arg-ctx}.
	In term of context analysis, this function now is equivalent to the \minizinc implication operator.

\end{example}

\begin{algorithm}
	\KwIn{A \minizinc\ operator \(op\) and calling context \(ctx\)}

	\KwOut{A tuple containing the contexts of the arguments \(\tuple{ctx_{1}, \ldots{}, ctx_{n}}\)}

	\Switch{op}{
		\Case{\mzninline{ not }}{
			\Return{\tuple{\changeneg{}ctx}}
		}
		\Case{\mzninline{ \/ }, \mzninline{+ }}{
			\Return{\tuple{\changepos{}ctx, \changepos{}ctx}}
		}
		\Case{\mzninline{ -> }, \mzninline{< }, \mzninline{<= }}{
			\Return{\tuple{\changeneg{}ctx, \changepos{}ctx}}
		}
		\Case{\mzninline{ > }, \mzninline{>= }, \mzninline{- }}{
			\Return{\tuple{\changepos{}ctx, \changeneg{}ctx}}
		}
		\Case{\mzninline{ <-> }, \mzninline{xor }, \mzninline{* }}{
			\Return{\tuple{\mixc, \mixc}}
		}
		\Case{\mzninline{ /\ }}{
			\Return{\tuple{ctx, ctx}}
		}
		\Other{
			\Return{\tuple{\mixc, \ldots, \mixc}}
		}
	}
	\caption{\label{alg:arg-ctx} Definition of the \emph{argCtx} function for \minizinc\ operators.}
\end{algorithm}

The context in which the result of a call expression is used must also be considered.
The (Call) rule, therefore, introduces the \ctxfunc{ident}{ctx} syntax.
This syntax is used to declare that the compiler must introduce a \microzinc\ function variant that flattens the function call to \(ident\) in the context \(ctx\).
This means that if \(ctx\) is \rootc{}, the compiler can use the the function as defined.
Otherwise, the compiler follows the following steps to try to introduce the most compatible variant of the function:

\begin{enumerate}
	\item If a direct definition for \(ctx\) definition exists, then use this definition.

		\begin{description}
			\item[\posc] \glspl{half-reif} can be defined as \(ident\)\mzninline{_imp}.
			\item[\negc] negations of \glspl{half-reif} can be defined as \(ident\)\mzninline{_imp_neg}.
			\item[\mixc] \glspl{reification} can be defined as \(ident\)\mzninline{_reif}.
		\end{description}

	\item If \(ident\) is a \microzinc{} function with an expression body \(E\), then copy of the function can be made that is evaluated in the desired context:\ctxeval{E}{ctx}.
		
	\item If \(ctx\) is \posc{} or \negc{}, then change \(ctx\) to \mixc{} and return to step 1.

	\item Finally, if non of the earlier steps were successful, then the compilation fails.
		Note that this can only occurr when a solver-level predicate does not have an \gls{reification}.
\end{enumerate}

The (Access) and (ITE) rules show the context inference for array access and if-then-else expressions respectively.
Their inner expressions are evaluated in \(\changepos{}ctx\).
The inner expressions cannot be simply be evaluated in \(ctx\), because it is not yet certain which expression will be chosen.
This is important for when \(ctx\) is \rootc{}, since we, at compile time, say which expression will hold globally.
We will revisit this issue in \cref{subsec:half-?root}.

Finally, the (Compr) and (Arr) rules show simple inference rules for array construction expressions.
If such an expression is evaluated in the context \(ctx\), then its members can be evaluated in the same context \(ctx\).

\begin{figure*}
  \centering
  \begin{prooftree}
		\hypo{\ctxeval{\texttt{let \{ }I\texttt{ \} in } e}{ctx}}
		\infer1[(Let)]{\ctxeval{e}{ctx}, \ctxitem{I} }
  \end{prooftree} \\
  \bigskip
  \begin{prooftree}
		\hypo{\ctxitem{I \texttt{; constraint } e }}
		\infer1[(Con)]{\ctxeval{e}{\rootc},~\ctxitem{I}}
  \end{prooftree} \\
  \bigskip
  \begin{prooftree}
		\hypo{\ctxitem{I \texttt{; } T: x \texttt{ = } e }}
		\hypo{\text{collectCtx}(x) = [ctx_{1}, \ldots, ctx_{n}]}
		\infer2[(Assign)]{\ctxeval{x}{\text{join}([ctx_{1}, \ldots, ctx_{n}])},~\ctxitem{I}}
  \end{prooftree} \\
  \bigskip
  \begin{prooftree}
		\hypo{\ctxitem{I \texttt{; } \texttt{tuple(}\ldots\texttt{):}~x \texttt{ = (} e_{1}, \ldots, e_{n}\texttt{)}}}
		\hypo{\text{collectCtx}(x) = \tuple{ctx_{1}, \ldots, ctx_{n}}}
		\infer2[(TupC)]{\ctxeval{e_{1}}{ctx_{1}}, \ldots, \ctxeval{e_{n}}{ctx_{n}}, ~\ctxitem{I}} 
  \end{prooftree} \\
  \bigskip
  \begin{prooftree}
		\hypo{\ctxitem{I \texttt{; (} T_{1}: x_{1}, \ldots, T_{n}: x_{n} \texttt{) = } e }}
		\infer[no rule]1{\text{collectCtx}(x_{1}) = [ctx^{1}_{1}, \ldots, ctx^{1}_{k}], \ldots, \text{collectCtx}(x_{n}) = [ctx^{n}_{1}, \ldots, ctx^{n}_{l}]}
		\infer1[(TupD)]{\ctxeval{e}{\tuple{\text{join}\left(\left[ctx^{1}_{1}, \ldots, ctx^{1}_{k}\right]\right), \ldots, \text{join}\left(\left[ctx^{n}_{1}, \ldots, ctx^{n}_{l}\right]\right)}},~\ctxitem{I}}
  \end{prooftree} \\
  \bigskip
  \begin{prooftree}
		\hypo{\ctxitem{I \texttt{; } T: x}}
		\infer1[(Decl)]{}
  \end{prooftree} \\
  \bigskip
  \begin{prooftree}
		\hypo{\ctxitem{\epsilon{}}}
		\infer1[(Item0)]{}
  \end{prooftree}
	\caption{\label{fig:half-analysis-it} Context inference rules for \microzinc\ let-expressions.}
\end{figure*}

\Cref{fig:half-analysis-it} shows the inference rules for let expressions and their inner items.
The first rule, (Let), propagates the context in which the expression is evaluated, \(ctx\), directly to the \mzninline{in}-expression.
Thereafter, the analysis will continue by iterating over its inner items.
This is described using the newly introduced syntax \ctxitem{I}.
Note that the \(ctx\) of the let-expression itself, is irrelevant for the analysis of its inner items.

The inference for \constraint{} items is described by the (Con) rule.
Since \microzinc{} implements strict semantics, the \constraint{} can be assumed to hold globally.
And, unlike \minizinc{}, the \constraint{} is not dependent on the context of the let-expression.
The \constraint{}'s expression is evaluated in \rootc context.

The (Assign) rule reasons about declarations that have a right hand side.
The expression that is assigned to the identifier must evaluated in the combined context of its usages.
As previously discussed, the contexts in which the identifier was used can be retrieved using the ``collectCtx'' function.
These contexts are then combined using a ``join'' function.
This function repeatedly applies the symmetric join operation described by \cref{fig:half-join}.
The right hand expression of the item is then evaluated in the resulting context.

\begin{figure*}
	\begin{center}
		\begin{tabular}{r | c c c c}
			join & \rootc & \posc & \negc & \mixc \\
			\hline
			\rootc & \rootc & \rootc & \rootc & \rootc \\ 
			\posc & \rootc & \posc & \mixc & \mixc \\ 
			\negc & \rootc & \mixc & \negc & \mixc \\ 
			\mixc & \rootc & \mixc & \mixc & \mixc \\ 
		\end{tabular}
	\end{center}
	\caption{\label{fig:half-join} A table showing the result of joining two contexts.}
\end{figure*}

(TupC) and (TupD) handle the context inference during the construction and destructuring of tuples respectively.
The context of the individual members of tuples is tracked separately.
This means that individual members of a tuple, like the value and the partiality of a \minizinc{} expression, may be evaluated in different contexts.

Finally, the (Decl) and (Item0) rules describe two base cases in the inference.
The declaration item of a \variable{} does not further the context, and does not depend on it.
It merely triggers the creation of a new \variable{}.
The (Item0) rule is triggered when there are no more inner items in the let-expression.

\subsection{Potentially \rootc{}}%
\label{subsec:half-?root}

In the previous section, we briefly discussed the context transformations for the (Access) and (ITE) rules in \cref{fig:half-analysis-expr}.
Different from the rules described, when an array access or if-then-else expression is found in \rootc{} context, it often makes sense to evaluate its sub-expression in \rootc context as well.
It is, however, not always safe to do so.

\begin{example}
\label{ex:half-maybe-root}

	For example, consider the following \microzinc{} fragment.

	\begin{mzn}
		constraint if b then F(x, y, z) else G(x, y, z) endif;
	\end{mzn}

	In this case, since only one side of the if-then-else expression is evaluated, the compiler can output calls to the \rootc{} variant of the functions.
	This will enforce the constraint in the most efficient way.

	Things, however, change when the situation gets more complex.
	Consider the following \microzinc{} fragment.

	\begin{mzn}
		let {
			var bool: p = F(x, y, z);
			var bool: q = G(x, y, z);
			constraint if b then p else q endif;
			var bool: ret = bool_or(p, r);
		} in ret;
	\end{mzn}

	One side of the if-then-else expression is not also used in a disjunction.
	If \mzninline{b} evaluates to \mzninline{true}, then \mzninline{p} is evaluated in \rootc{} context, and \mzninline{p} can take the value \mzninline{true} in the disjunction.
	Otherwise, \mzninline{q} is evaluated in \rootc{} context, and \mzninline{p} in the disjunction must be evaluated in \posc{} context.
	It is, therefore, not safe to assume that all sides of the if-then-else expressions are evaluated in \rootc{} context.
\end{example}

Using the \changepos{} transformation for sub-expression contexts is safe, but it might place a large burden on the \solver{}.
The solver is likely to perform better when the direct constraint predicate is used.

To detect situation where the sub-expression are only used in an array access or if-then-else expression we introduce the \mayberootc{} context.
This context functions as a \emph{weak} \rootc{} context.
If it is joined with any other context, then it acts as \posc{}.
The extended join operation is shown in \cref{fig:half-maybe-join}.
Otherwise, it will act as a normal \rootc{} context.

\begin{figure*}
	\begin{center}
		\begin{tabular}{r | c c c c c}
			join & \rootc & \mayberootc & \posc & \negc & \mixc \\
			\hline
			\rootc & \rootc & \rootc & \rootc & \rootc & \rootc \\ 
			\mayberootc & \rootc & \mayberootc & \posc & \mixc & \mixc \\ 
			\posc & \rootc & \posc & \posc & \mixc & \mixc \\ 
			\negc & \rootc & \mixc & \mixc & \negc & \mixc \\ 
			\mixc & \rootc & \mixc & \mixc & \mixc & \mixc \\ 
		\end{tabular}
	\end{center}
	\caption{\label{fig:half-maybe-join} The join context operation extended with \mayberootc{}.}
\end{figure*}

\begin{figure*}
  \centering
  \begin{prooftree}
		\hypo{\ctxeval{x\texttt{[}i\texttt{]}}{\rootc}}
		\infer1[(Access-R)]{\ctxeval{x}{\mayberootc}}
  \end{prooftree} \\
  \bigskip
  \begin{prooftree}
		\hypo{\ctxeval{\texttt{if }b\texttt{ then } e_{1} \texttt{ else } e_{2} \texttt{ endif}}{\rootc}}
		\infer1[(ITE-R)]{\ctxeval{e_{1}}{\mayberootc},~\ctxeval{e_{2}}{\mayberootc}}
  \end{prooftree}
	\caption{\label{fig:half-analysis-maybe-root} Updated context inference rules for \mayberootc{}.}
\end{figure*}

\Cref{fig:half-analysis-maybe-root} shows the additional inference rules for array access and if-then-else expressions.
Looking back at \cref{ex:half-maybe-root}, these additional rules and updated join operation will ensure that the first case will correctly use \rootc{} context calls.
For the second case, however, it detects that \mzninline{p} is used in both \posc{} and \mayberootc{} context.
Therefore, it will output the \posc{} call for the right hand side of \mzninline{p}, even when \mzninline{b} evaluates to \mzninline{true}.
At compile time, this is only correct context to use.
We will, however, discuss the dynamically adjusting of contexts during flattening in \cref{subsec:half-dyn-context}.

\section{Flattening and Half Reification}%
\label{sec:half-flattening}

During the flattening process the contexts assigned to the different expressions can be used directly to determine if and how a expression has to be reified.

\jip{TODO: Add example of flattening with \gls{half-reif}}

The flattening with \gls{half-reif} does, however, interact with some of the optimisations used during the flattening process.
Most importantly, \gls{half-reif} has to be considered when using \gls{cse}.
In \cref{subsec:half-cse} we will discuss how \gls{cse} can be adjusted to handle \gls{half-reif}.

As shown in \jip{insert reference}, a consequence of the use of \gls{half-reif} is that it might form so called \emph{implication chains}.
This happens when the right hand side of an implication is half reifed and a new Boolean variable is created to represent the variable.
Instead, we could have directly posted the half-reified constraint using the left hand side of the implication as its control variable.
In \cref{subsec:half-compress} we present a new post-processing method, \emph{chain compression}, that can be used to eliminate these implication chains.

\subsection{Common Sub-expression Elimination}%
\label{subsec:half-cse}

When using full \gls{reification}, all \glspl{reification} are stored in the \gls{cse} table.
This ensure that if we see the same expression is reified twice, then the resulting \variable{} would be reusing.
This avoids that the solver has to enforce the same functional relationship twice.

If the flattener uses \gls{half-reif}, in addition to full \gls{reification}, then \gls{cse} needs to ensure not just that the expressions are equivalent, but also that the context of the two expressions are compatible.
For example, if an expression was first found in a \posc{} context and later found in a \mixc{} context, then the resulting \gls{half-reif} from the first cannot be used for the second expression.
In general:

\begin{itemize}

	\item The flattening result of a \posc{} context, a \gls{half-reif}, can only be reused if the same expression is again found in \posc{} context.

	\item The flattening result of a \negc{} context, a \gls{half-reif} with its negation pushed inwards, can only be reused if the same expression is again found in \negc{} context.
	
	\item The flattening result of a \mixc{} context, a \gls{reification}, can be reused in \posc{}, \negc{}, and \mixc{} context.
		Since we assume that the result of a flattening an expression in \negc{} context pushes the negation inwards, the \gls{reification} does, however, need to be negated.

	\item If the expression was already flattened in \rootc{} context, then any repeated usage of the expression can be assumed to take the value \mzninline{true} (or \mzninline{false} in \negc{} context).

\end{itemize}

When considering these compatibility rules, the result of flattening would be highly dependent on the order in which expressions are seen by the flattener.
It would always be better to encounter the expression in a context that results in a reusable expression, \eg{} \mixc{}, before seeing the same expression in another context, \eg{} \posc{}.
This avoids creating both a full \gls{reification} and a \gls{half-reif} of the same expression.

In the \microzinc{} interpreter, this problem is resolved by only keeping the result of their \emph{joint} context.
The context recorded in the \gls{cse} table and the found context are joint using the join operator, as described in \cref{fig:half-join}.
If this context is different from the recorded context, then the expression is re-evaluated in the joint context and its result kept in the \gls{cse} table.
All usages of the previously recorded result is replaced by the new result.
Because of dependency tracking of the constraints that define variables, we can be sure that all \variables{} and \constraints{} created in defining the earlier version are correctly removed.

Because the expression itself is changed when a negation is moved inwards, it may not always be clear when the same expression is used in both \posc{} and negc{} context.
This problem is solved by introducing a canonical form for expressions where negations can be pushed inwards.
In this form the result of flattening an expression and its negation are collected in the same place within the \gls{cse} table.
If it is found that for an expression that is about to be half reified there already exists an \gls{half-reif} for its negation, then we instead evaluate the expression in mixed context, reifying the expression and replacing the existing half reified expression.

This canonical form for expressions and their negations can also be used for the expressions in other contexts.
Using the canonical form we can now also be sure that we never create a full \gls{reification} for both an expression and its negation.
Instead, when one is created, the negation of the resulting \variable{} can directly be used as the result of reifying its negation.
Moreover, this mechanism also allows us to detect when an expression and its negation occur in \rootc{} context.
This is simple way to detect conflicts between \constraints{} and, by extend, prove that the constraint model is unsatisfiable.
Clearly, a \constraint{} and its negation cannot both hold at the same time.

\subsection{Dynamic Context Switching}%
\label{subsec:half-dyn-context}

\subsection{Chain compression}%
\label{subsec:half-compress}

As shown in \cref{ex:hr-half}, flattening with half reification will in many cases result in implication chains: \mzninline{b1 -> b2 /\ b2 -> c}, where \texttt{b2} has no other occurrences.
In this case the conjunction can be replaced by \mzninline{b1 -> c} and \texttt{b2} can be removed from the model.
The case shown in the example can be generalised to

\begin{mzn}
	b1 -> b2 /\ forall(i in N)(b2 -> c[i])
\end{mzn}

\noindent{}which, if \texttt{b2} has no other usage in the instance, can be resolved to

\begin{mzn}
	forall(i in N)(b1 -> c[i])
\end{mzn}

\noindent{}after which \texttt{b1} can be removed from the model.


An algorithm to remove these chains of implications is best visualised through the use of an implication graph.
An implication graph \(\tuple{V,E}\) is a directed graph where the vertices \(V\) represent the variables in the instance and an edge \(\tuple{x,y} \in E\) represents the presence of an implication \mzninline{x -> y} in the instance.
Additionally, for the benefit of the algorithm, a vertex is marked when it is used in other constraints in the constraint model.
The goal of the algorithm is now to identify and remove vertices that are not marked and have only one incoming edge.
\Cref{alg:half-compression} provides a formal specification of the chain compression method in pseudo code.

\begin{algorithm}
	\KwIn{An implication constraint graph \(G=\tuple{V, E}\) and a set \(M
	\subseteq{} V\) of vertices used in other constraints.}

	\KwOut{An equisatisfiable graph \(G'=\tuple{V', E'}\) where chained
	implications have been removed.}

	\(V' \longleftarrow V\)\;
	\(E' \longleftarrow E\)\;
	\For{\(x \in V\)} {
		\If{\(x \not\in M\) \textbf{ and }\(\left|\left\{\tuple{a,x}| \tuple{a,x} \in E\right\}\right| = 1\)}{
			\For{\(\tuple{x, b} \in E\)}{
				\(E' \longleftarrow E' \cup \{ \tuple{a,b} \} \)\;
				\(E' \longleftarrow E' \backslash \{ \tuple{x,b} \} \)\;
			}
			\(E' \longleftarrow E' \backslash \{ \tuple{a,x} \} \)\;
			\(V' \longleftarrow V' \backslash \{ x \} \)\;
		}
	}
	\(G' \longleftarrow \tuple{V', E'}\)\;
	\caption{\label{alg:half-compression} Implication chain compression algorithm}
\end{algorithm}

The algorithm can be further improved by considering implied conjunctions.
These can be split up into multiple implications:

\begin{mzn}
	b -> forall(x in N)(x)
\end{mzn}

\noindent{}is equivalent to

\begin{mzn}
	forall(x in N)(b -> x)
\end{mzn}

Adopting this transformation both simplifies a complicated constraint and possibly allows for the further compression of implication chains.
It should however be noted that although this transformation can result in an increase in the number of constraints, it generally increases the propagation efficiency.

To adjust the algorithm to simplify implied conjunctions more introspection from the \minizinc{} compiler is required.
The compiler must be able to tell if a variable is (only) a control variable of a reified conjunction and what the elements of that conjunction are.
In the case where a variable has one incoming edge, but it is marked as used in other constraint, we can now check if it is only a control variable for a reified conjunction and perform the transformation in this case.

\section{Experiments}
\label{sec:half-experiments}

We now present experimental evaluation of the presented \gls{half-reif} techniques.
First, to show the benefit of implementing propagators for half-reified constraint, we compare their performance against their decompositions.
To do this, we recreate two experiments presented by Feydy et al.\ in the original \gls{half-reif} paper in a modern \gls{cp} solver, \gls{chuffed}.
In the experiment, we use propagators implemented according to the principles described in this paper.
No new algorithm has been devised to perform the propagation.
The propagator of the original constraint is merely adjusted to influence and watch a control \variable{}.

Additionally, we assess the effects of automatically detecting and introducing \glspl{half-reif} during the flattening process. We flatten and solve 

A description of the used computational environment, \minizinc{} instances, and versioned software has been included in \cref{ch:benchmarks}.

\subsection{Propagators}
\label{sec:half-exp-prop}

Our first experiment considers the \gls{qcp-max} quasi-group completion problem.
In this problem, we need to decide the value of an \((n \times n)\) matrix of integer \variables, with domains \mzninline{1..n}.
The aim of the problem is to create as many rows and columns where all \variables{} take a unique value.
In each instance certain values have already been fixed.
It is, thus, not always possible for all rows and columns to contain only distinct values.

In \minizinc{} counting the number of rows/columns with all different values can be accomplished by reifying the \mzninline{all_different} constraint.
Since the goal of the problem is to maximise the number of \mzninline{all_different} \constraints{} that hold, these constraints are never forced to be \mzninline{false}.
This means these constraints in a \posc{} context and can be half-reified.

\Cref{tab:half-qcp} shows the comparison of two solving configurations in \gls{chuffed} for the \gls{qcp-max} problem.
The results are grouped based on their size of the instance.
For each group we show the number of instances solved by the configuration and the average time used for this process.

The first configuration uses a newly created propagator for half-reified \mzninline{all_different} \constraints{}.
This propagator is an adjusted version from the existing bounds consistent \mzninline{all_different} propagator in chuffed.
The implementation of the propagator was already split into parts that \emph{check} the violation of the constraint and parts that \emph{prune} the \glspl{domain} of \variables{}.
Therefore, the transformation described in \cref{sec:half-propagation} can be directly applied.
Since \gls{chuffed} is a \gls{lcg} \solver{}, the explanations created by the propagator have to be adjusted as well.
These adjustments happen in a similar fashion to the adjustments of the general algorithm: explanations used for the violation of the \constraint{} can now be used to set the control variable to \mzninline{false} and the explanations given to prune a variable are appended by requirement that the control variable is \mzninline{true}.

The second configuration uses the following decomposition for the \mzninline{all_different} constraint.

\begin{mzn}
	predicate all_different(array[int] of var int: x) =
		forall(i,j in index_set(x) where i < j)(
			x[i] != x[j]
		);
\end{mzn}

The \mzninline{!=} constraints produced by this redefinition are reified.
Their conjunction, then represent the reification of the \mzninline{all_different} constraint.

\begin{table}
	\begin{center}
		\input{assets/table/half_qcp}

		\caption{\label{tab:half-qcp} \gls{qcp-max} problems: number of solved instances and average time (in seconds) with a 300s timeout.}

  \end{center}
\end{table}

The results in \cref{tab:half-qcp} show that the usage of the specialised propagator has a significant advantage over the use of the decomposition.
Although it only allows us to solve a single extra instance, there is a significant reduction in solving time for most instances.
Note that the qcp-15 instances are the only exception.
It appears that none of the instances in this group proved to be a real challenge to either method and we see similar solve times between the two methods.

For our second experiment we consider a variation on the prize collecting travelling salesman problem \autocite{balas-1989-pctsp} referred to as \emph{prize collecting path}.
In the problem we are given a graph with weighted edges, both positive and negative.
The aim of the problem is to find the optimal acyclic path from a given start node that maximises the weights on the path.
It is not required to visit every node.

In this experiment we can show how \gls{half-reif} can reduce the overhead of handling partial functions correctly.
The \minizinc{} model for this problem contains a unsafe array lookup \mzninline{pos[next[i]]}, where the domain of \mzninline{next[i]} is larger than the index set of \mzninline{pos}.
We compare safe decomposition of this \mzninline{element} constraint against a propagator of its \gls{half-reif}.
The decomposition creates a new variable that takes the value of the index only when it is within the index set of the array.
Otherwise, it will set its surrounding context to \mzninline{false}.
The \gls{half-reif} implicitly performs the same task by setting its control \variable{} to \mzninline{false} whenever the result of the \mzninline{element} constraint does not match the value of the index variable.
Again, for the implementation of the propagator of the \gls{half-reif} constraint we adjust the regular propagator as described above.

\begin{table}[tb]
	\begin{center}

		\input{assets/table/half_prize}

		\caption{\label{tab:half-prize} Prize collecting paths: number of solved instances and average time (in seconds) and with a 300s timeout.}
  \end{center}
\end{table}

The results of the experiment are shown in \cref{tab:half-prize}.
Although the performance on smaller instances is similar, the dedicated propagator consistently outperforms the usage of the decomposition.
The difference in performance becomes more pronounced in the bigger instances.
In the 32-4-8 group, we even see that usage of the propagator allows us to solve an additional three instances.

\subsection{Decomposition experiments}
\label{sec:half-exp-decomp}

To verify the effectiveness of the half reification implementation within the \minizinc{} distribution we compare the results of the current version of the \minizinc{} translator (rev.\jip{add revision}) against the equivalent version for which we have implemented half reification.
We use the model instances used by the \minizinc{} challenges \autocite{stuckey-2010-challenge,stuckey-2014-challenge} from 2019 and 2020. The performance of the generated \flatzinc{} models will be tested using Gecode, flattened with its own library, and Gurobi and CBC, flattened with the linear library.

\begin{table} [tb]
  \caption{\label{tab:hr-flat-results} Flattening results: Average changes in the
    generated the \flatzinc{} models}
  \begin{center}
    \begin{tabular}{|l|r||r|r|r||r|}
      \hline
      Library & Nr. Instances & Full Reifications
              & Constraints   & Variables         & Chains Compressed                     \\
      \hline
      Gecode  & 274           & -38.19\%          & -6.29\%           & -8.66\% & 21.35\% \\
      \hline
      Linear  & 346           & - 33.11\%         & -13.77\%          & -3.70\% & 11.63\% \\
      \hline
    \end{tabular}
  \end{center}
\end{table}
\jip{Better headers for \cref{tab:hr-flat-results} and update with current results}

\Cref{tab:hr-flat-results} shows the average change on the number of full reification, constraints, and variables between the \flatzinc\ models generated by the different versions of the translator using the different libraries.
We find that the number full reifications is reduced by a significant amount.
Together with the chain compression mechanism this has a positive effect on the number of constraints and the number of variables.

\jip{Add something regarding the chain compression. Is this the right
  statistic? (Compressions in terms of reifications)}

	We ran our experiments on a computer with a 3.40GHz Intel i7-3770 CPU and 16Gb of memory running the Ubuntu 16.04.3 LTS operating system.

\jip{Scatter plot of the runtimes + discussion!}


\section{Summary}
\label{sec:half-summary}