%************************************************
\chapter{Mode Analysis and Half Reification}\label{ch:half_reif}
%************************************************

Discrete optimisation solvers solve constraint optimisation problems of the form
\(\min o \text{~subject to~} \wedge_{c \in C} c\), that is minimising an
objective \(o\) subject to an (existentially quantified) conjunction of
primitive constraints \(c\). But modelling languages such as OPL
\autocite{van-hentenryck-1999-opl}, Zinc/\minizinc\
\autocite{marriott-2008-zinc, nethercote-2007-minizinc} and Essence
\autocite{frisch-2007-essence} allow much more expressive problems to be
formulated. Modelling languages map the more expressive formulations to
existentially quantified conjunction through a combination of loop unrolling,
and flattening using reification.

\begin{example}\label{ex:hr-cons}
  Consider the following ``complex constraint'' written in \minizinc\ syntax

  \begin{mzn}
    constraint i <= 4 -> a[i] * x >= 6;
  \end{mzn}

  which requires that if \mzninline{i \leq 4} then the value in the
  \texttt{i}\(^{th}\) position of array \mzninline{a} multiplied by \mzninline{x}
  must be at least 6. This becomes the following existentially quantified
  conjunction through flattening and reification:\footnote{Actually the result
    is in \flatzinc\ but we show an equivalent \minizinc\ form for easy of
    readability.}

  \begin{mzn}
    constraint b1 <-> i <= 4;     % b1 holds iff i <= 4
    constraint element(i, a, t1); % t1 is the ith element of a
    constraint mult(t1, x, t2);   % t2 is t1 * x
    constraint b2 <-> t2 >= 6;    % b2 holds iff t2 >= 6
    constraint b1 -> b2           % b1 implies b2
  \end{mzn}

  The complex logic (implication) is encoded by ``reifying'' the arguments and
  in effect naming their truth value using new Boolean variables \texttt{b1} and
  \texttt{b2}. The term structure is encoded by ``flattening'' the terms and
  converting the functions to relations, introducing the new integer variables
  \texttt{t1} and \texttt{t2}. Note that the newly introduced variables are
  existentially quantified.
\end{example}

The translation given in the above example is well understood, but potentially
flawed, for three reasons. The first is that the flattening may not give the
intuitive meaning when functions are partial.

\begin{example}
  Suppose the array \texttt{a} has index set \mzninline{1..5}, but \texttt{i}
  takes the value \texttt{7}. The constraint \mzninline{element(i, a, t1)} will
  fail and no solution will be found. Intuitively if \mzninline{i = 7} the
  constraint should be trivially true.
\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

\begin{mzn}
/* t1 @\(\equiv\)@ */ a[7] = @\undefined{}@;
/* t2 @\(\equiv\)@ */ @\undefined{}@ * x = @\undefined{}@;
/* b2 @\(\equiv\)@ */ @\undefined{}@ >= 6 = @\undefined{}@;
/* b1 @\(\equiv\)@ */ 7 <= 4 = false;
false -> @\undefined{}@ = @\undefined{}@;
\end{mzn}

This is known as the \emph{strict} semantics
\autocite{frisch-2009-undefinedness} for modelling languages.

The usual choice for modeling partial functions in modelling languages is the
\emph{relational} semantics \autocite{frisch-2009-undefinedness}. In the
relational semantics the value \undefined\ percolates up through the term until it
reaches a Boolean subterm where it becomes \(\mzninline{false}\). For the example

\begin{mzn}
/* t1 @\(\equiv\)@ */ a[7] = @\undefined{}@;
/* t2 @\(\equiv\)@ */ @\undefined{}@ * x = @\undefined{}@;
/* b2 @\(\equiv\)@ */ @\undefined{}@ >= 6 = false;
/* b1 @\(\equiv\)@ */ 7 <= 4 = false;
false -> false = true;
\end{mzn}

But in order to implement the relational semantics, the translation of the
original complex constraint needs to be far more complex.

\begin{example}
  The \minizinc\ compiler unrolls, flattens, and reifies \minizinc\ models
  implementing the relational semantics. Assuming \texttt{i} takes values in the
  set \mzninline{1..8}, and \texttt{a} has an index set \mzninline{1..5}, its
  translation of the constraint in \cref{ex:hr-cons} is

  \begin{mzn}
    constraint b1 <-> i <= 4;   % b1 holds iff i <= 4
    constraint element(t3,a,t1);% t1 is the t3'th element of a
    constraint mult(t1,x,t2);   % t2 is t1 * x
    constraint b2 <-> t2 >= 6;  % b2 holds iff t2 >= 6
    constraint t3 in 1..5       % t3 in index set of a
    constraint b3 <-> i = t3;   % b3 holds iff i = t3
    constraint b3 <-> i <= 5;   % b3 holds iff i in index set of a
    constraint b4 <-> b2 /\ b3  % b4 holds iff b2 and b3 hold
    constraint b1 -> b4         % b1 implies b4
  \end{mzn}

  The translation forces the partial function application \texttt{element} to be
  ``safe'' since \texttt{t3} is constrained to only take values in the index set
  of \texttt{a}. The reified constraints defining \texttt{b3} force \texttt{t3}
  to equal \texttt{i} if and only if \texttt{i} takes a value in the index set
  of \texttt{a}.
  % Finally the Boolean
  % \(b4\) defines when the rhs condition holds \(b2\)
  % and the \element{} constraint was safe \(b3\).
\end{example}

A second weakness of reification, independent of the problems with partial
functions, 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 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 b1 <-> i <= 4;   % b1 holds iff i <= 4
    constraint minus(x,i,t1);   % t1 = x - i
    constraint b2 <-> all_different([i,t1,x]);
    constraint b1 -> b2         % 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 global constraints are not implemented because a reified constraint
\mzninline{b <-> pred(@\ldots{}@)} must also implement a propagator for
\mzninline{not pred(@\ldots{}@)} (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.

A third weakness of the full reification is that it may keep track of more
information than is required. In a typical finite domain 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}

Flattening with half-reification is an approach to mapping complex constraints
to existentially quantified conjunctions that improves upon all these weaknesses
of flattening with full reification.

\begin{itemize}
  \item Flattening with half reification can naturally produce the relational
        semantics when flattening partial functions in positive contexts.
  \item Half reified constraints add no burden to the solver writer; if they
        have a propagator for constraint \mzninline{pred(@\ldots{}@)} then they
        can straightforwardly construct a half reified propagator for
        \mzninline{b -> pred(@\ldots{}@)}.
  \item Half reified constraints \mzninline{b -> pred(@\ldots{}@)} can implement
        fully reified constraints without any loss of propagation strength
        (assuming reified constraints are negatable).
  \item Flattening with half reification can produce more efficient propagation
        when flattening complex constraints.
  \item Flattening with half reification can produce smaller linear models when
        used with a mixed integer programming solver.
\end{itemize}

Our conclusion is that propagation solvers \emph{only} need to provide half
reified version of all constraints. This does not burden the solver writer at
all, yet it provides more efficient translation of models, and more
expressiveness in using global constraints.

\section{Propagation Based Constraint Solving}

\jip{This section looks like background and should probably be moved}

We consider a typed set of variables \(\VV = \VV_I \cup \VV_B\) made up of
\emph{integer} variables, \(\VV_I\), and \emph{Boolean} variables, \(\VV_b\). We use
lower case letters such as \(x\) and \(y\) for integer variables and letters such as
\(b\) for Booleans.
%
A \gls{domain} \(D\) is a complete mapping from \(\VV\) to finite sets of integers
(for the variables in \(\VV_I\)) and to subsets of
\(\{\mzninline{true},\mzninline{false}\}\) (for the variables in \(\VV_b\)).
%
We can understand a \gls{domain} \(D\) as a formula
\(\wedge_{v \in \VV} (v \in D(v))\) stating for each variable \(v\) that its value
is in its domain. A \emph{false domain} \(D\) is a domain where
\(\exists_{v \in \VV} D(v) = \emptyset\), and corresponds to an unsatisfiable
formula.

Let \(D_1\) and \(D_2\) be domains and \(V\subseteq\VV\). We say that \(D_1\) is
\emph{stronger} than \(D_2\), written \(D_1 \sqsubseteq D_2\), if
\(D_1(v) \subseteq D_2(v)\) for all \(v \in \VV\).
%% and that \(D_1\) and \(D_2\)
%% are \emph{equivalent modulo \(V\)}, written \(D_1 =_V D_2\), if \(D_1(v) =
%% D_2(v)\)  for all \(v \in V\). \pjs{Equivelant modulo never used???}
%%
The \emph{intersection} of \(D_1\) and \(D_2\), denoted \(D_1 \sqcap D_2\), is defined
by the domain \(D_1(v) \cap D_2(v)\) for all \(v\in\VV\).
%
%We use \emph{range} notation:
%
%For integers \(l\) and \(u\), \(\range{l}{u}\) denotes the set of integers
%\(\{ d ~|~ l \leq d \leq u\}\).
%
We assume an \emph{initial domain} \(D_{init}\) such that all domains \(D\) that
occur will be stronger i.e.~\(D \sqsubseteq D_{init}\).


A \emph{valuation} \(\theta\) is a mapping of integer and Boolean variables to
correspondingly typed values, written
\(\{x_1 \mapsto d_1, \ldots, x_n \mapsto d_n, b_1 \mapsto u_1, \ldots, b_m \mapsto u_m\}\).
% PJS (not true unless \theta is in D)
% where \(d_i \in D(x_i)\) and \(A_j \in D(S_j)\).
We extend the valuation \(\theta\) to map expressions or constraints involving the
variables in the natural way. Let \(\vars\) be the function that returns the set
of variables appearing in an expression, constraint or valuation.

In an abuse of notation, we define a valuation \(\theta\) to be an element of a
domain \(D\), written \(\theta \in D\), if \(\theta(v) \in D(v)\) for all
\(v \in \vars(\theta)\).


%\paragraph{Constraints, Propagators and Propagation Solvers}

A constraint is a restriction placed on the allowable values for a set of
variables.
%% We shall be interested in constraints
%PJS over integer, set and Boolean variables.
%% over integer and set variables.
We define the \emph{solutions} of a constraint \(c\) to be the set of valuations
\(\theta\) that make that constraint true, i.e.
\(\solns(c) = \{ \theta \ |\ (\vars(\theta) = \vars(c))\ \wedge\ (\entails \theta(c))\}\)

%%MC check this para that my changes are ok
We associate with every constraint \(c\) a \emph{propagator} \(f_c\). A propagator
\(f_c\) is a monotonically decreasing function on domains that maintains solutions
of the constraint. That is, for all domains \(D \sqsubseteq D_{init}\):

\(f_c(D) \sqsubseteq D\) (decreasing), and
\(\{\theta\in D \,|\ \theta \in \solns(c)\} = \{\theta \in f_c(D)\,|\ \theta \in \solns(c)\}\)
(preserves solutions), and for domains
\(D_1 \sqsubseteq D_2 \sqsubseteq D_{init}\): \(f(D_1) \sqsubseteq f(D_2)\)
(monotonic). This is a weak restriction since, for example, the identity mapping
is a propagator for any constraint.

A domain \(D\) is \emph{domain consistent} for constraint \(c\) if
\(D(v) = \{ \theta(v)~|~\theta \in solns(c)~\wedge~\theta \in D \}\), for all
\(v \in vars(c)\).

A domain \(D\) is \emph{bounds(Z) consistent} for constraint \(c\) over variables
\(v_1, \ldots v_n\) if for each \(i \in \{1, \ldots, n\}\) there exists
\(\theta \in solns(c) \cap D\) s.t. \(\theta(v_i) = \min D(v_i)\) and
\(\min D(v_j) \leq \theta(v_j) \leq \max D(v_j), 1 \leq j \neq i \leq n\), and
similarly exists \(\theta \in solns(c) \cap D\) s.t. \(\theta(v_i) = \max D(v_i)\)
and \(\min D(v_j) \leq \theta(v_j) \leq \max D(v_j), 1 \leq j \neq i \leq n\). For
Boolean variables \(v\) we assume \(\mzninline{false} < \mzninline{true}\).

% A domain \(D\) is \emph{bounds(R) consistent} for constraint \(c\) if the same
% conditions as for bounds(Z) consistency hold except \(\theta \in solns(c')\) where
% \(c'\) is the \emph{real relaxation} of \(c\).

A domain \(D\) is \emph{bounds(R) consistent} for constraint \(c\) over integer
variables \(x_1, \ldots x_n\) and Boolean variables \(b_1, \ldots, b_m\) if \(c'\) is
the real relaxation of \(c\) (where \(x_1, \ldots, x_n\) can take real values,
rather than just integer values) and for each \(i \in \{1, \ldots, n\}\) there
exists \(\theta \in solns(c') \cap D\) s.t. \(\theta(x_i) = \min D(x_i)\) and
\(\min D(x_j) \leq \theta(x_j) \leq \max D(x_j), 1 \leq j \neq i \leq n\) and
\(\theta(b_j) \in D(b_j), 1 \leq j \leq m\), and similarly exists
\(\theta \in solns(c') \cap D\) s.t. \(\theta(x_i) = \max D(x_i)\) and
\(\min D(x_j) \leq \theta(x_j) \leq \max D(x_j), 1 \leq j \neq i \leq n\) and
\(\theta(b_j) \in D(b_j), 1 \leq j \leq m\). Also for each \(i in \{1,\ldots, m\}\)
and \(tf \in D(b_i)\) there exists \(\theta \in solns(c') \cap D\) s.t.
\(\theta(b_i) = tf\) and
\(\min D(x_j) \leq \theta(x_j) \leq \max D(x_j), 1 \leq j \leq n\) and
\(\theta(b_j) \in D(b_j), 1 \leq j \neq i \leq m\).

Note that we assume Booleans can only take Boolean values in the real
relaxation.

Note that for the pure Boolean constraints domain, bounds(Z) and bounds(R)
consistency coincide.

A propagator \(f_c\) is \(X\)-consistent if \(f(D)\) is always \(X\) consistent for \(c\),
where \(X\) could be domain, bounds(Z) or bounds(R).

A \emph{propagation solver} for a set of propagators \(F\) and current domain \(D\),
\(\solv(F,D)\), repeatedly applies all the propagators in \(F\) starting from domain
\(D\) until there is no further change in the resulting domain. \(\solv(F,D)\) is
the weakest domain \(D' \sqsubseteq D\) which is a fixpoint (i.e.~\(f(D') = D'\))
for all \(f \in F\). In other words, \(\solv(F,D)\) returns a new domain defined by
\( \solv(F,D) = \gfp(\lambda d.\iter(F,d))(D)\) where
\(\iter(F,D) = \bigsqcap_{f \in F} f(D)\), where \(\gfp\) denotes the greatest
fixpoint w.r.t \(\sqsubseteq\) lifted to functions.
% (We use the greatest fixpoint because we are coming down from a full domain,
% not going up from an empty one.)


\subsection{A Language of Constraints}\label{sec:hr-syntax}

\jip{This introduces a subset of \minizinc, but we can probably use \microzinc\
  instead.}

\newcommand{\nonterm}[1]{\textsc{#1}}
\newcommand{\subs}[1]{[\![ #1 ]\!] }
\newcommand{\flatc}{\nonterm{flatc}}
\newcommand{\flatt}{\nonterm{flatt}}
\newcommand{\new}{\textbf{new}~}
\newcommand{\evalb}{\nonterm{evala}}
\newcommand{\evali}{\nonterm{evali}}

Below is a grammar for a subset of \minizinc\, with enough complexity to
illustrate all the main challenges in flattening.

The \syntax{<cons>} nonterminal defines constraints (Boolean terms),
\syntax{<term>} defines integer terms, \syntax{<barray>} defines Boolean arrays,
and \syntax{<iarray>} defines integer arrays:

\begin{grammar}
  <cons> ::= "true" | "false" | <bvar> | <term> <relop> <term> | "not" <cons>
    \alt <cons> "/\\" <cons> | <cons> "\\/" <cons> | <cons> "->" <cons> | <cons> "<->" <cons>
    \alt "forall(" <barray> ")" | <barray> | <barray>"[" <term> "]"
    | pred(<term>, \ldots, <term>)
    \alt "if" <cons> "then" <cons> "else" <cons> "endif"
    \alt "let" "{"<decls> <ocons> "}" "in" <cons>

  <term> ::= <int> | <ivar> | <term> <arithop> <term> | <iarray>"[" <term> "]"
    \alt "sum(" <iarray> ")" \alt "if" <cons> "then" <term> "else" <term> "endif"
    \alt "bool2int(" <cons> ")" \alt "let" "{"<decls> <ocons> "}" "in" <term>

  <barray> ::= "[" <cons>, \ldots, <cons> "]" \alt "["<cons> "|" <ivar> "in" <term> ".." <term> "]"

  <iarray> ::= "[" <term>, \ldots, <term> "]" \alt "["<term> "|" <ivar> "in" <term> ".." <term> "]"

  <relop> ::= "==" | "<=" | "<" | "!=" | ">=" | ">"

  <arithop> ::= "+" | "-" | "*" | "div"
\end{grammar}

The grammar uses the symbols \syntax{<bvar>} for Boolean variables,
\syntax{<pred>} for names of predicates, \syntax{<int>} for integer constants,
and \syntax{<ivar>} for integer variables.

In the \texttt{let} constructs we make use of the nonterminal \syntax{<decls>}
for declarations. We define this below using \syntax{<idecls>} for integer
variable declarations, \syntax{<bdecls>} for Boolean variable declarations. We
use \syntax{<ocons>} for optional constraint items appearing in let
declarations. We also define \syntax{<args>} as a list of integer variable
declarations, an \syntax{<fndecl>} as either a predicate declaration or a
function declaration, \syntax{<solve>} as a solve directive either satisfaction
or an objective, and a model \syntax{<model>} as some declarations followed by
items followed by a solve item. Note that \syntax{<empty>} represents the empty
string.

\begin{grammar}
  <idecl> ::= "int" ":" <ivar> | "var" "int" ":" <ivar> | "var" <term> ".." <term> ":" <ivar>

  <bdecl> ::= "bool" ":" <ivar> | "var" "bool" ":" <ivar>

  <decls> ::= <idecls> [ "=" <term>] ";" <decls> | <bdecls> [ "=" <cons>] ";" <decls> | <empty>

  <ocons> ::= "constraint" <cons>  ";" <ocons> | <empty>

  <args> ::=  "int" ":" <ivar> ["," <args>] | "var" "int" ":" <ivar>  ["," <args>]

  <fndecl> ::=  "predicate" <pred> "(" <args> ")" "=" <cons> ";"
    \alt "function" "var" "int" ":" <func> "(" <args> ")" "=" <term> ";"

  <solve> ::= "satisfy" | "maximize" <term> | "minimize" <term>

  <model> ::=  <fndecl>* <decls> <ocons> "solve" <solve>

\end{grammar}

The main missing things are floats, long linear constraints, and set and array
variables. It misses many built-in operators and functions, but their treatment
is analogous to those we include. To simplify presentation, we assume all
predicate and function arguments are integers, but the translation can be
extended to arbitrary arguments in a straightforward way.

\subsection{Further Notation}

Given an expression \(e\) that contains the subexpression \(x\), we denote by
\(e\subs{x/y}\) the expression that results from replacing all occurrences of
subexpression \(x\) by expression \(y\). We will also use the notation for
multiple simultaneous replacements \(\subs{\bar{x}/\bar{y}}\) where each
\(x_i \in \bar{x}\) is replaced by the corresponding \(y_i \in \bar{y}\).

Given a \syntax{<cons>} term defining the constraints of the model we can split
its \syntax{<cons>} subterms as occurring in different kinds of places: root
contexts, positive contexts, negative contexts, and mixed contexts. A Boolean
subterm \(t\) of constraint \(c\) is in a \emph{root context} iff there is no
solution of \(c\subs{t/\mzninline{false}}\), that is \(c\) with subterm \(t\)
replaced by \(\mzninline{false}\).\footnote{For the definitions of context we
  assume that the subterm \(t\) is uniquely defined by its position in \(c\), so
  the replacement is of exactly one subterm.} Similarly, a subterm \(t\) of
constraint \(c\) is in a \emph{positive context} iff for any solution \(\theta\)
of \(c\) then \(\theta\) is also a solution of \(c\subs{t/\mzninline{true}}\);
and a \emph{negative context} iff for any solution \(\theta\) of \(c\) then
\(\theta\) is also a solution of \(c\subs{t/\mzninline{false}}\). The remaining
Boolean subterms of \(c\) are in \emph{mixed} contexts. While determining
contexts according to these definitions is hard, there are simple syntactic
rules which can determine the correct context for most terms, and the rest can
be treated as mixed.

Consider the constraint expression

\begin{mzn}
  constraint x > 0 /\ (i <= 4 -> x + bool2int(b) = 5);
\end{mzn}

then \mzninline{x > 0} is in the root context, \mzninline{i <= 4} is in a
negative context, \mzninline{x + bool2int(b) = 5} is in a positive context, and
\mzninline{b} is in a mixed context. If the last equality were \mzninline{x +
  bool2int(b) >= 5} then \mzninline{b} would be in a positive context.

We assume each integer variable \(x\) is separately declared with a finite initial
set of possible values \(D_{init}(x)\). We assume each array constant is
separately declared as a mapping \(\{ i \mapsto d~|~i \in \dom(a) \}\) where its
index set \(\dom(a)\) is a finite integer range. Given these initial declarations,
we can determine the set of possible values \(poss(t)\) of any term \(t\) in the
language as \(poss(t) = \{ \theta(t)~|~\theta \in D_{init} \}\). Note also while
it may be prohibitive to determine the set of possible values for any term \(t\),
we can efficiently determine a superset of these values by building a superset
for each subterm bottom up using approximation.

% Given a \cons{} term defining the constraints of the model we can split its
% \cons{} subterms as occurring in kinds of places: positive contexts, negative
% contexts, and mixed contexts. A Boolean subterm \(t\) of constraint \(c\), written
% \(c[t]\), is in a \emph{positive context} iff for any solution \(\theta\) of \(c\)
% then \(\theta\) is also a solution of \(c[\mzninline{true}]\), that is \(c\) with subterm \(t\)
% replaced by \(\mzninline{true}\). Similarly, a subterm \(t\) of constraint \(c\) is in a
% \emph{negative context} iff for any solution \(\theta\) of \(c\) then \(\theta\) is
% also a solution of \(c[\mzninline{false}]\). The remaining Boolean subterms of \(c\) are in
% mixed contexts.

% \begin{example}
%   Consider the constraint expression \(c\) \negspace
%   \begin{mzn}
%     constraint i <= 4 -> x + bool2int(b) = 5;
%   \end{mzn}
%   then \(i \leq 4\) is in a negative context, \(x + \texttt{bool2int}(b) = 5\) is
%   in a positive context, and \(b\) is in a mixed context. If the last equality
%   were \(x + \texttt{bool2int}(b) \geq 5\) then \(b\) would be in a positive
%   context. \qed
% \end{example}

% One can classify most contexts as positive or negative using a simple top-down
% analysis of the form of the expression. The remaining contexts can be
% considered mixed without compromising the correctness of the rest of the
% paper.

Our small language contains two partial functions: \mzninline{div} returns
\undefined\ if the divisor is zero, while \mzninline{a[i]} returns \undefined\
if the value of \mzninline{i} is outside the domain of \mzninline{a}. We can
categorise the \emph{safe} terms and constraints of the language, as those where
no \undefined\ can ever arise in any subterm. A term or constraint is
\emph{safe} if all its arguments are safe and: either the term is not a division
or array access; or it is a division term \mzninline{t1 div t2} and the set of
possible values of \mzninline{t_2} does not include 0, \mzninline{not 0 in
  dom(t2)}; or it is an array access term \mzninline{a[t]} and the set of
possible values of \mzninline{t} are included in the domain of \mzninline{a},
\mzninline{dom(t) subset dom(a)}.

\section{Flattening with Full Reification}
\label{sec:hr-translation}

Constraint problems formulated in \minizinc\ are solved by translating them to a
simpler, solver-specific subset of \minizinc, called \flatzinc. \flatzinc\
consists only of a sequence of variables declarations and a conjunction of
constraints. This section shows how to translate our extended \minizinc\ to
\flatzinc. The usual method for flattening complex formula of constraints is
full reification. Given a constraint \(c\) the \emph{full reified form} for
\(c\) is \(b \full c\), where \(b \not\in vars(c)\) is a Boolean variable naming
the satisfied state of the constraint \(c\).

% The complexities in the translation arise from the need to simultaneously (a)
% unroll array comprehensions (and other loops), (b) replace predicate and
% function applications by their body, and (c) flatten expressions.

% Once we take into account CSE, we cannot perform these separately.
% In order to have names for common subexpressions we need to flatten
% expressions.  And in order to take advantage of functions
% for CSE we cannot replace predicate and function applications without
% flattening to generate these names. And without replacing predicate and
% function application by their body we are unable to see all the loops to
% unroll.

\newcommand{\ctxt}{\ensuremath{\mathit{ctxt}}}
\newcommand{\rootc}{\textsl{root}}
\newcommand{\pos}{\textsl{pos}}
\newcommand{\negc}{\textsl{neg}}
\newcommand{\mix}{\textsl{mix}}
\newcommand{\cupp}{\ensuremath{\cup}\text{:=}~}
\newcommand{\posop}{\ensuremath{+}}
\newcommand{\negop}{\ensuremath{-}}
\newcommand{\fixed}{\textsf{fixed}}
\newcommand{\eval}{\textsf{eval}}

The translation algorithm presented below generates a flat model equivalent to
the original model as a global set of constraints \(S\). We ignore the
collection of variable declarations, which is also clearly important, but quite
straightforward. The translation uses full reification to create the model.

Common subexpression elimination is implemented using a technique similar to
\emph{hash-consing} in Lisp \autocite{allen-1978-lisp}. For simplicity we only
show syntactic CSE, which eliminates expressions that are identical after
parameter replacement. The extension to semantic CSE, using commutativity and
other equivalences, is well understood (see \autocite{rendl-2010-thesis} for a
detailed discussion) but makes the pseudo-code much longer.

The complex part of flattening arises in flattening the constraints, we shall
ignore the declarations part for flattening and assume that any objective
function term \mzninline{e} is replaced by a new variable \mzninline{obj} and a
constraint item \mzninline{constraint obj = e} which will then be flattened as
part of the model.

\subsection{Flattening Constraints}

Flattening a constraint \(c\) in context \ctxt, \(\flatc(c,\ctxt)\), returns a
Boolean literal \(b\) representing the constraint and as a side effect adds a
set of constraints (the flattening) \(S\) to the store such that
\(S \models b \full c\).

It uses the context (\(\ctxt\)) to decide how to translate, where possible
contexts are: \rootc, at the top level conjunction; \pos, positive context,
\negc, negative context, and \mix, mixed context. We use the context operations
\(\posop\) and \(\negop\) defined as:

\centerline{%
\begin{tabular}{ccc}
\(
\begin{array}{lcl}
\posop \rootc & = &\pos \\
\posop \pos & =& \pos \\
\posop \negc & =& \negc, \\
\posop \mix & =& \mix
\end{array}
\)
&~&
\(
\begin{array}{lcl}
\negop \rootc & = &\negc \\
\negop \pos & =& \negc \\
\negop \negc & =& \pos, \\
\negop \mix & =& \mix
\end{array}
\)
\end{tabular}
}

% \centerline{
% \begin{tabular}{ccccccc}
% \(
% \begin{array}{lcl}
% \posop \rootc & = &\pos \\
% \posop \pos & =& \pos
% \end{array}
% \)
% & ~~~ &
% \(
% \begin{array}{lcl}
% \posop \negc & =& \negc, \\
% \posop \mix & =& \mix
% \end{array}
% \)
% & ~~~ &
% \(
% \begin{array}{lcl}
% \negop \rootc & = &\negc \\
% \negop \pos & =& \negc
% \end{array}
% \)
% & ~~~ &
% \(
% \begin{array}{lcl}
% \negop \negc & =& \pos, \\
% \negop \mix & =& \mix
% \end{array}
% \)
% \end{tabular}
% }

% \(\negop\) and \(\posop\) as \(\negop \rootc = \negc\), \(\negop \pos = \negc\),
% \(\negop \negc = \pos\), \(\negop \mix = \mix\); and
% \(\posop \rootc = \pos\),
% \(\posop \pos = \pos\),
% \(\posop \negc = \negc\),
% \(\posop \mix = \mix\),

Note that flattening in a \mix\ context is the most restrictive case, and the
actual flattening rules only differentiate between \rootc\ and other contexts.
The importance of the \pos\ context is that \mzninline{let} expressions within a
\pos\ context can declare new variables. The important of the \negc\ context is
to track \pos\ context arising under double negations. Note that flattening in
the root context always returns a Boolean \mzninline{b} made equivalent to
\mzninline{true} by the constraints in \(S\). For succinctness we use the
notation \mzninline{@\new{}@ b} (or \mzninline{@\new{}@ v}) to introduce a fresh
Boolean (resp.\ integer) variable and return the name of the variable.

The Boolean result of flattening \(c\) is stored in a hash table, along with the
context and reused if an identical constraint expression is ever flattened
again. We retrieve the result of the previous flattening \(h\) and the previous
context \(prev\). If the expression previously appeared at the root then we
simply reuse the old value, since regardless of the new context the expression
must hold. If the new context is \rootc\ we reuse the old value but require it
to be \mzninline{true} in \(S\), and modify the hash table to record the
expression appears at the root. If the expression appeared in a mixed context we
simply reuse the old result since this is the most constrained context.
Similarly if the previous context is the same as the current one we reuse the
old result. In the remaining cases we set the context to \mix\ since the
remaining cases require at least both a \pos\ and \negc\ or a \mix\ context.
Note that if an expression introduces a fresh variable and it appears first in a
negative context and only later in the root context, the translation aborts.
This could be fixed in a preprocessing step that sorts expressions according to
their context.

The flattening proceeds by evaluating fixed Boolean expressions and returning
the value. We assume \fixed\ checks if an expression is fixed (determined during
\minizinc{}'s type analysis), and \eval\ evaluates a fixed expression. For
simplicity of presentation, we assume that fixed expressions are never undefined
(such as \mzninline{3 div 0}). We can extend the algorithms to handle this case,
but it complicates the presentation. Our implementation aborts in this
case.\pjs{CHECK and FIX!} While this does not agree with the relational
semantics it likely indicates a modelling error since a fixed part of the model
must be undefined. The abort forces the user to redefine the model to avoid
this.

For non-fixed expressions we treat each form in turn. Boolean literals and
variables are simply returned. Basic relational operations flatten their terms
using the function \flatt\, which for a term \(t\) returns a tuple
\(\tuple{v,b}\) of an integer variable/value \(v\) and a Boolean literal \(b\)
such that \(b \full (v = t)\) (described in detail below). The relational
operations then return a reified form of the relation.
% If in the root context this can be simplified.
The logical operators recursively flatten their arguments, passing in the
correct context. The logical array operators evaluate their array argument, then
create an equivalent term using \textsf{foldl} and either \mzninline{/\
}\xspace{}or \mzninline{\/} which is then flattened. A Boolean array lookup
flattens its arguments, and creates an \mzninline{element} constraint. If the
context is root this is simple, otherwise it creates a new index variable \(v'\)
guaranteed to only give correct answers, and uses this in the
\mzninline{element} constraint to avoid undefinedness. Built-in predicates abort
if not in the root context.\footnote{Using half reification this can be relaxed
  to also allow positive contexts.} They flatten their arguments and add an
appropriate built-in constraint. User defined predicate applications flatten
their arguments and then flatten a renamed copy of the body.\emph{if-then-else}
evaluates the condition (which must be fixed) and flattens the \emph{then} or
\emph{else} branch appropriately. \pjs{Use the same restriction, but explain its
  not all required} The handling of \mzninline{let} is the most complicated. The
expression is renamed with new copies of the let variables. We extract the
constraints from the \mzninline{let} expression using function \textsf{flatlet}
which returns the extracted constraint and a rewritten term (not used in this
case, but used in \flatt{}). The constraints returned by function
\textsf{flatlet} are then flattened. Finally if we are in the root context, we
ensure that the Boolean \(b\) returned must be \mzninline{true} by adding \(b\)
to \(S\).

{
\begin{tabbing}
xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill
\flatc(\(c\),\(\ctxt\)) \\
\> \(\tuple{h,prev}\) := hash[\(c\)]; \\
\> \textbf{if} (\(h \neq \undefined{}\)) \\
\>\> \textbf{if} (\(prev =\rootc\)) \textbf{return} \(h\)  \\
\>\> \textbf{if} (\(ctxt = \rootc\)) \(S\) \cupp \(\{ h \}\); hash[\(c\)] :=
\(\tuple{h,\rootc}\);  \textbf{return} \(h\)
\\
\>\> \textbf{if} (\(prev = \mix \vee prev = \ctxt\))
\textbf{return} \(h\)  \\
\>\> \(\ctxt\) := \(\mix\) \\
\> \textbf{if} (\(\fixed(c)\)) \(b\) := \(\eval(c)\) \\
\> \textbf{else} \\
\> \> \textbf{switch} \(c\) \\
%\> \> \textbf{case} \texttt{true}: \(b\) := \(\mzninline{true}\);\\
%\> \> \textbf{case} \texttt{false}: \(b\) := \(\mzninline{false}\);\\
\> \> \textbf{case} \(b'\) (\syntax{<bvar>}): \(b\) := \(b'\); \\
\> \> \textbf{case} \(t_1\) \(r\) \(t_2\) (\syntax{<relop>}):  \\
\>\>\> \(\tuple{v_1, b_1}\) := \(\flatt(t_1,\ctxt)\);
\(\tuple{v_2, b_2}\) := \(\flatt(t_2,\ctxt)\); \\
\> \> \> \(S\) \cupp  \(\{ \new b \full (b_1 \wedge b_2 \wedge \new b'), b'  \full v_1~r~v_2\}\) \\
\> \> \textbf{case} \texttt{not} \(c_1\):
\(b\) := \(\neg \flatc(c_1, \negop \ctxt)\) \\
\> \> \textbf{case} \(c_1\) \verb+/\+ \(c_2\):  \(S\) \cupp  \(\{ \new b \full (\flatc(c_1, \ctxt) \wedge \flatc(c_2, \ctxt))\}\)
\\
\>\> \textbf{case} \(c_1\) \verb+\/+ \(c_2\):
\(S\) \cupp \(\{ \new b \full (\flatc(c_1,\posop \ctxt) \vee \flatc(c_2,\posop \ctxt))\}\)
\\
\>\> \textbf{case} \(c_1\) \verb+->+ \(c_2\):
\(S\) \cupp  \(\{ \new b \full (\flatc(c_1,\negop \ctxt) \half \flatc(c_2,\posop \ctxt))\}\)
\\
\>\> \textbf{case} \(c_1\) \verb+<->+ \(c_2\):
\(S\) \cupp  \(\{ \new b \full (\flatc(c_1,\mix) \full
\flatc(c_2,\mix))\}\)
\\
\> \> \textbf{case} \texttt{forall(} \(ba\) \texttt{)}: \\
\> \> \> \textbf{let} \([c_1, \ldots, c_n] = \evalb(ba)\); \\
\> \> \> \textbf{foreach}(\(j \in 1..n\)) \(b_j\) := \(\flatc(c_j, \ctxt)\); \\
\>\>\> \(S\) \cupp \(\{ \new b \full \bigwedge_{j=1}^n b_j \}\) \\
\>\> \textbf{case} \texttt{exists(} \(ba\) \texttt{)}: \\
\> \> \> \textbf{let} \([c_1, \ldots, c_n] = \evalb(ba)\); \\
\> \> \> \textbf{foreach}(\(j \in 1..n\)) \(b_j\) := \(\flatc(c_j, +\ctxt)\); \\
\>\>\> \(S\) \cupp \(\{ \new b \full \bigvee_{j=1}^n b_j \}\) \\
\>\> \textbf{case} \([c_1, \ldots, c_n]\) \texttt{[} \(t\) \texttt{]}:  \\
\>\>\>
\textbf{foreach}(\(j \in 1..n\)) \(b_j\) := \(\flatc(c_j, \posop \ctxt)\); \\
\>\>\> \(\tuple{v, b_{n+1}}\) := \(\flatt(t, \ctxt)\); \\
%\>\>\> \(S\) \cupp
%\(\{ \new b \full (b_{n+1} \wedge \new b' \wedge \new b''),
%\mathit{safeelement}(v, [b_1, \ldots, b_n],  b'),
%b'' \full v \in \{1,..,n\} \} \) \\
\>\>\> \textbf{if} (\(\ctxt = \rootc\)) \(S\) \cupp \(\{\texttt{element}(v', [b_1, \ldots, b_n],
\mzninline{true})\}\); \(b\) := \(\mzninline{true}\)  \\
\>\>\> \textbf{else} \\
\>\>\>\> \(S\) \cupp
\(\{ \new b \full (b_{n+1} \wedge \new b' \wedge \new b''), \new v' \in \{1,
\ldots, n\},\) \\
\>\>\>\>\>\>\> \(\texttt{element}(v', [b_1, \ldots, b_n],  b'),
b'' \full v  = v', b'' \full v \in \{1,\ldots,n\} \} \)
\\
\>\> \textbf{case} \(p\) (\(t_1, \ldots, t_n\)) (\syntax{<pred>}) built-in predicate: \\
\> \> \> \textbf{foreach}(\(j \in 1..n\)) \(\tuple{v_j, b_j}\) := \(\flatt(t_j,\ctxt)\); \\
\> \> \> \textbf{if} (\(\ctxt \neq \rootc\)) \\
\> \> \> \> \textbf{if} (\(p\_reif\) does not exist) \textbf{abort} \\
\> \> \> \> \textbf{else} \(S\) \cupp \(\{ p\_reif(v_1,\ldots,v_n,\new b'),
\new b \Leftrightarrow b' \wedge \bigwedge_{j=1}^n b_j\}\) \\
\> \> \> \textbf{else} \\
\>\> \> \> \(b\) := \(\mzninline{true}\); \(S\) \cupp  \(\{ p(v_1, \ldots, v_n) %, \bigwedge_{j=1}^n b_j
\}\)
\\
\>\> \textbf{case} \(p\) (\(t_1, \ldots, t_n\)) (\syntax{<pred>}): user-defined predicate \\
\>\> \> \textbf{let} \(p(x_1, \ldots, x_n) = c_0\) be defn of \(p\) \\
\> \> \> \textbf{foreach}(\(j \in 1..n\)) \(\tuple{v_j, b_j}\) := \(\flatt(t_j,\ctxt)\); \\
\>\> \> \(\new b'\) := \(\flatc(c_0\subs{x_1/v_1, \ldots, x_n/v_n},\ctxt)\)
\\
\> \>\> \(S\) \cupp \(\{ \new b \Leftrightarrow b' \wedge \bigwedge_{j=1}^n
b_j\}\)
\\
\> \> \textbf{case} \texttt{if} \(c_0\) \texttt{then} \(c_1\) \texttt{else}
\(c_2\) \texttt{endif}:
% \\ \> \> \>
\textbf{if} (\(\eval(c_0)\)) \(b\) := \(\flatc(c_1,\ctxt)\) \textbf{else} \(b\) := \(\flatc(c_2,\ctxt)\) \\
\>\> \textbf{case} \texttt{let \{} \(d\) \texttt{\} in} \(c_1\): \\
\>\> \> \textbf{let} \(\bar{v}'\) be a renaming of variables \(\bar{v}\) defined
in \(d\) \\
\> \> \> \(\tuple{c',\_}\) := \(\textsf{flatlet}(d\subs{\bar{v}/\bar{v}'},
c_1\subs{\bar{v}/\bar{v}'},0,\ctxt)\) \\
\> \> \> \(b\) := \(\flatc(c',\ctxt)\);
\\
\> \> \textbf{endswitch} \\
\> \textbf{if} (\(\ctxt = \rootc\)) \(S\) \cupp \(\{ b \}\); \\
\> hash[\(c\)] := \(\tuple{b,\ctxt}\) \\
\> \textbf{return} \(b\)
\end{tabbing}
}

The function \evalb{} replaces an array comprehension by the resulting array.
Note that terms \(\mathit{lt}\) and \(\mathit{ut}\) must be fixed in a correct
\minizinc\ model.

\begin{tabbing}
xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill
\evalb(\(t\)) \\
\> \textbf{switch} \(t\) \\
\> \textbf{case}  \verb+[+ \(t_1, \ldots, t_n\) \verb+]+:
   \textbf{return} \verb+[+ \(t_1, \ldots, t_n\) \verb+]+
   \\
\> \textbf{case} \verb+[+ \(e\) \verb+|+ \(v\) \texttt{in} \(\mathit{lt}\) \texttt{..} \(\mathit{ut}\)
\verb+]+:
 \\ \> \>
\textbf{let} \(l = \eval(\mathit{lt})\), \(u = \eval(\mathit{ut})\)
 \\ \> \>
\textbf{return}  \verb+[+ \(e\subs{v/l}\),  \(e\subs{v/l+1}\),
\ldots \(e\subs{v/u}\) \verb+]+
\end{tabbing}

\subsection{Handling \texttt{let} Expressions}

Much of the handling of a \mzninline{let} is implemented by
\textsf{flatlet}\((d,c,t,\ctxt)\) which takes the declarations \(d\) inside the
\mzninline{let}, the constraint \(c\) or term \(t\) of the scope of the
\mzninline{let} expression, as well as the context type. First \textsf{flatlet}
replaces parameters defined in \(d\) by their fixed values. Then it collects in
\(c\) all the constraints that need to stay within the Boolean context of the
\mzninline{let}: the constraints arising from the variable and constraint items,
as well as the Boolean variable definitions. Integer variables that are defined
have their right hand side flattened, and a constraint equating them to the
right hand side \(t'\) added to the global set of constraints \(S\). If
variables are not defined and the context is negative or mixed the translation
aborts.

{%\small
\begin{tabbing}
xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill
\textsf{flatlet}(\(d\),\(c\),\(t\),\(\ctxt\)) \\
\> \textbf{foreach} (\(item \in d\)) \\
\> \> \textbf{switch} \(item\) \\
\> \> \textbf{case} \texttt{var bool :} \(b = c'\) : \= \kill
\> \> \textbf{case} \texttt{bool :} \(b = c'\) : \> \(d\) :=
\(d\subs{b/\eval(c')}\); \= \(c\) := \(c\subs{b/\eval(c')}\); \= \kill
%\> \> \textbf{case} \texttt{\(l\) .. \(u\) :} \(v = t'\) : \> \(d\) :=
%\(d\subs{v/\eval(t')}\); \> \(c\) := \(c\subs{v/\eval(t')}\); \> \(t\) := \(t\subs{v/\eval(t')}\) \\
\> \> \textbf{case} \texttt{int :} \(v = t'\) : \> \(d\) := \(d\subs{v/\eval(t')}\);
\> \(c\) := \(c\subs{v/\eval(t')}\); \> \(t\) := \(t\subs{v/\eval(t')}\)\\
\> \> \textbf{case} \texttt{bool :} \(b = c'\) : \> \(d\) :=
\(d\subs{b/\eval(c')}\); \> \(c\) := \(c\subs{b/\eval(c')}\); \> \(t\) := \(t\subs{b/\eval(c')}\)
\\
%\> \textbf{endfor} \\
\> \textbf{foreach} (\(item \in d\)) \\
\> \> \textbf{switch} \(item\) \\
%\> \> \textbf{case} \texttt{\(l\) .. \(u\) :} \(v = t'\) : \> \(c\) := \(c\) \verb+/\+ \(l\)
%\texttt{<=} \(v\) \verb+/\+ \(v\) \texttt{<=} \(u\) \\
\> \> \textbf{case} \texttt{var int :} \(v\) : \> \textbf{if} (\(\ctxt \in
\{\negc,\mix\}\)) \textbf{abort} \\
\> \> \textbf{case} \texttt{var int :} \(v = t'\) :
\> \(\tuple{v',b'}\) := \(\flatt(t',\ctxt)\);
\(S\) \cupp \(\{v = v'\}\); \(c\) := \(c\) \verb+/\+ \(b'\)
\\
\> \> \textbf{case} \texttt{var} \(l\) \texttt{..} \(u\) \texttt{:} \(v\) : \>
\textbf{if} (\(\ctxt \in
\{\negc,\mix\}\)) \textbf{abort} \textbf{else} \(c\) := \(c\)
\verb+/\+ \(l\) \texttt{<=} \(v\) \verb+/\+ \(v\) \texttt{<=} \(u\)
 \\
\> \> \textbf{case} \texttt{var} \(l\) \texttt{..} \(u\) \texttt{:} \(v = t'\) :
\> \(\tuple{v',b'}\) := \(\flatt(t',\ctxt)\);
\(S\) \cupp \(\{v = v'\}\); \\
\> \> \> \(c\) := \(c\) \verb+/\+ \(b'\)
\verb+/\+ \(l\) \texttt{<=} \(v\) \verb+/\+ \(v\) \texttt{<=} \(u\);
\\
\> \> \textbf{case} \texttt{var bool :} \(b\) : \> \textbf{if} (\(\ctxt \in
\{\negc,\mix\}\)) \textbf{abort} \\
\> \> \textbf{case} \texttt{var bool :} \(b = c'\) : \>
\(c\) := \(c\)
\verb+/\+ (\(b\) \verb+<->+ \(c'\)) \\
\> \> \textbf{case} \texttt{constraint} \(c'\) : \> \(c\) := \(c\)
\verb+/\+ \(c'\) \\
\> \> \textbf{endswitch} \\
\> \textbf{return} \(\tuple{c,t}\)
\end{tabbing}
}

\subsection{Flattening Integer Expressions}

\(\flatt(t,\ctxt)\) flattens an integer term \(t\) in context \(\ctxt\). It
returns a tuple \(\tuple{v,b}\) of an integer variable/value \(v\) and a Boolean
literal \(b\), and as a side effect adds constraints to \(S\) so that
\(S \models b \full (v = t)\). Note that again flattening in the root context
always returns a Boolean \(b\) made equivalent to \mzninline{true} by the
constraints in \(S\).

Flattening first checks if the same expression has been flattened previously and
if so returns the stored result. \flatt{} evaluates fixed integer expressions
and returns the result.
% For non-fixed integer expressions \(t\), if \(t\)
% is determined to be total, it changes the context to
% \(\rootc\) since this is safe.
For non-fixed integer expressions \(t\) each form is treated in turn. Simple
integer expressions are simply returned. Operators have their arguments
flattened and the new value calculated on the results. A safe form of division
is used, introducing a new variable \(v'2\) as the divisor which can never be
zero, and a new Boolean \(b'\) captures when the division is defined. Array
lookup flattens all the integer expressions involved and creates a
\mzninline{element} constraint with a new index variable \(v'\) which is
guaranteed to be in the domain of the array (\mzninline{1..n}), and a new
Boolean \(b'\) which captures when the lookup is safe. \pjs{This is not the
  usual ``lazy'' relational semantics!} \texttt{sum} expressions evaluate the
array argument, and then replace the sum by repeated addition using
\textsf{foldl} and flatten that. \emph{if-then-else} simply evaluates the
\emph{if} condition (which must be fixed) and flattens the \emph{then} or
\emph{else} branch appropriately. \pjs{Fix for variable conditions, or state we
  ignore them for simplicity!} Functions are simply handled by flattening each
of the arguments, the function body is then renamed to use the variables
representing the arguments, and the body is then flattened. Importantly, if the
function is declared total it is flattened \emph{in the root context}. Let
constructs are handled analogously to \flatc. We rename the scoped term \(t_1\)
to \(t'\) and collect the constraints in the definitions in \(c'\). The result
is the flattening of \(t'\), with \(b\) capturing whether anything inside the
let leads to failure.

\begin{tabbing}
xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill
\flatt(\(t\),\(\ctxt\)) \\
\> \(\tuple{h,b',prev}\) := hash[\(t\)]; \\
\> \textbf{if} (\(h \neq \undefined{}\)) \\
\>\> \textbf{if} (\(prev =\rootc\))
\textbf{return} \(\tuple{h,b'}\)  \\
\>\> \textbf{if} (\(ctxt = \rootc\)) \(S\) \cupp \(\{ b' \}\); hash[\(t\)] :=
\(\tuple{h,b',\rootc}\);  \textbf{return} \(\tuple{h,b'}\)
\\
\>\> \textbf{if} (\(prev = \mix \vee prev = \ctxt\))
\textbf{return} \(\tuple{h,b'}\)  \\
\>\> \(\ctxt\) := \(\mix\) \\
\> \textbf{if} (\(\fixed(t)\)) \(v\) := \(\eval(t)\); \(b\) := \(\mzninline{true}\) \\
\> \textbf{else} %\\
%% \> \> \textbf{if} (\(t\) is marked \emph{total}) \(\ctxt\) := \(\rootc\) \\
%\> \>
\textbf{switch} \(t\) \\
%\> \> \textbf{case} \(i\) (\intc): \(v\) := \(i\); \(b\) := \(\mzninline{true}\) \\
\> \> \textbf{case} \(v'\) (\syntax{<ivar>}):  \(v\) := \(v'\); \(b\) := \(\mzninline{true}\)\\
\> \> \textbf{case} \(t_1\) \(a\) \(t_2\) (\syntax{<arithop>}): \\
\> \> \>
\(\tuple{v_1,b_1}\) := \(\flatt(t_1,\ctxt)\);
\(\tuple{v_2,b_2}\) := \(\flatt(t_2,\ctxt)\); \\
\> \> \> \textbf{if} (\(a \not\equiv \texttt{div} \vee \ctxt = \rootc\))
\(S\) \cupp \(\{ \new b \full (b_1 \wedge b_2), a(v_1,v_2,\new v) \}\) \\
%\> \> \> \textbf{else} \(S\) \cupp \(\{ \new b \full (b_1 \wedge b_2 \wedge
%\new b'), \mathit{safediv}(v_1,v_2,\new v), b' \full v_2 \neq 0 \}\) \\
\> \> \> \textbf{else} \(S\) \cupp \(\{ \new b \full (b_1 \wedge b_2 \wedge
\new b'), \new v_2' \neq 0,\) \\
\> \> \> \> \> \>\>\> \(\texttt{div}(v_1,v_2',\new v), b' \full v_2 \neq 0, b' \full
v_2 = v_2' \}\) \\
\> \> \textbf{case} \([t_1, \ldots, t_n]\) \texttt{[} \(t_{0}\) \texttt{]}: \\
\> \> \>
\textbf{foreach}(\(j \in 0..n\)) \(\tuple{v_j, b_j}\) := \(\flatt(t_j,\ctxt)\); \\
%\>\> \> \(S\) :=
%\(\{ \new b \full (\new b' \wedge \bigwedge_{j=0}^n b_j),
%\mathit{safeelement}(v_{0}, [v_1, \ldots, v_n],  \new v),
%b' \full v_0 \in \{1,...,n\} \}\)
%\\
\>\>\> \textbf{if} (\(\ctxt \neq \rootc\)) \\
\>\>\>\> \(S\) \cupp
\(\{ \new b \full (\new b' \wedge \bigwedge_{j=0}^n b_j), \new v' \in \{1,
\ldots, n\},\) \\
\>\>\>\>\>\>\> \(\texttt{element}(v', [v_1, \ldots, v_n],  \new v),
b' \full v_0  = v', b' \full v_0 \in \{1,\ldots,n\} \} \)
\\
\>\>\> \textbf{else} \(S\) \cupp \(\{\new b, \texttt{element}(v', [v_1, \ldots, v_n],
\new v) \}\) \\
\> \> \textbf{case} \texttt{sum(} \(\mathit{ia}\) \texttt{)}: \\
\> \> \> \textbf{let} \([t_1, \ldots, t_n] = \evalb(ia)\); \\
\> \> \> \textbf{foreach}(\(j \in 1..n\)) \(\tuple{v_j, b_j}\) :=
\(\flatt(t_j,\ctxt)\); \\
\>\>\> \(S\) \cupp \(\{ \new b \full \bigwedge_{j=1}^n b_j,
                     \new v = \sum_{j=1}^n v_j \}\) \\
%\> \> \>
%\(\tuple{v,b}\) := \flatt(
%\textsf{foldl}(\(\evalb(ia)\), \texttt{0}, \texttt{+}), \(\ctxt\))
%\\
\> \> \textbf{case} \texttt{if} \(c_0\) \texttt{then} \(t_1\) \texttt{else}
\(t_2\) \texttt{endif}:
% \\ \> \> \>
\textbf{if} (\(eval(c_0)\)) \(\tuple{v,b}\) := \(\flatt(t_1,\ctxt)\) \textbf{else}
\(\tuple{v,b}\) := \(\flatt(t_2,\ctxt)\)
\\
\>\> \textbf{case} \texttt{bool2int(} \(c_0\) \texttt{)}:
 \(b_0\) := \(\flatc(c_0, \mix)\);
 \(S\) \cupp \(\{ \texttt{bool2int}(b_0, \new v), \new b \}\)  \\
\>\> \textbf{case} \(f\) (\(t_1, \ldots, t_n\)) (\syntax{<func>}): function \\
\> \> \> \textbf{foreach}(\(j \in 1..n\)) \(\tuple{v_j, b_j}\) := \(\flatt(t_j,\ctxt)\); \\
\>\> \> \textbf{let} \(f(x_1, \ldots, x_n) = t_0\) be defn of \(f\) \\
\> \> \> \textbf{if} (\(f\) is declared total) \(\ctxt' = \rootc\) \textbf{else}
\(\ctxt' = \ctxt\) \\
\>\> \> \(\tuple{v,b'}\) := \(\flatt(t_0\subs{x_1/v_1, \ldots, x_n/v_n},\ctxt')\) \\
\> \> \> \(S\) \cupp \(\{ \new b \full b' \wedge \bigwedge_{j=1}^n b_j \}\)
\\
%\> \> \> \textbf{THINK we can go bakc to the other one now?} \\
%\> \> \> \textbf{foreach}(\(j \in 1..n\)) \(\tuple{v_j, b_j}\) := \(\flatt(t_j,\ctxt)\); \\
%\> \> \> \textbf{foreach}(\(j \in 1..n\)) \(\new w_i\); \\
%\>\> \> \textbf{let} \(f(x_1, \ldots, x_n) = t'\) be defn of \(p\) \\
%\>\> \> \(\tuple{v,b}\) := \(\flatt(t'\subs{x_1/w_1, \ldots, x_n/w_n},\rootc)\)
%\\
%\>\> \> \(S\) \cupp \(\{ b \half (v_1=w_1 \wedge \ldots \wedge v_n=w_n)\}\)\\
\>\> \textbf{case} \texttt{let \{} \(d\) \texttt{\} in} \(t_1\): \\
\>\> \> \textbf{let} \(\bar{v}'\) be a renaming of variables \(\bar{v}\) defined
in \(d\) \\
\> \> \> \(\tuple{c',t'}\) := \(\textsf{flatlet}(d\subs{\bar{v}/\bar{v}'},\texttt{true},
t_1\subs{\bar{v}/\bar{v}'},\ctxt)\) \\
\>\> \> \(\tuple{v,b_1}\) := \(\flatt(t',\ctxt)\);
\(b_2\) := \(\flatc(c',\ctxt)\);
\(S\) \cupp \(\{ \new b \full (b_1 \wedge b_2)\}\)
\\
\> \> \textbf{endswitch} \\
\> \textbf{if} (\(\ctxt = \rootc\)) \(S\) \cupp \(\{ b \}\); \\
\> hash[\(t\)] := \(\tuple{v,b,\ctxt}\) \\
\> \textbf{return} \(\tuple{v,b}\)
\end{tabbing}

\begin{example}\label{ex:hr-flat}
  Consider the flattening of the expression

  \[
    a[x] + bool2int(x > y) - bool2int(x > z) \geq 4 \vee
    (a[x] \leq 2 \wedge x > y \wedge (x > z \rightarrow b))
  \]

  The different terms and subterms of the expression are illustrated and
  numbered as follows

  \[
    \xymatrix@R=1em@C=0.6em{
      &&&&&~\vee^{(0)} \ar[dll] \ar[drr] \\
      &&&~\geq^{(1)} \ar[dl] \ar[dr] &&&&~\wedge^{(2)} \ar[dl] \ar[drr] \\
      &&~-^{(3)} \ar[dl]\ar[dr] && 4 &&~\wedge^{(4)}  \ar[dl]\ar[dr] &&&
      \rightarrow^{(5)} \ar[d]\ar[dr] &&& \\
      &~+^{(6)} \ar[dr]\ar[dl] && bool2int^{(7)} \ar[d] &&
      \leq^{(8)}\ar[dr]\ar[d] &&~>^{(9)}\ar[dr]\ar[d] &&~>^{(10)}\ar[dr]\ar[d] &
      b  \\
      []^{(11)}\ar[dr]\ar[d] &&bool2int^{(12)}\ar[d] &~>^{(13)}\ar[dr]\ar[d] &&
      []^{(14)} \ar[dr]\ar[d] & 2 &x &y &x &z &&&&& \\
      a &x &~>^{(15)}\ar[dr]\ar[d]& x&z &a &x \\
      & & x & y && \\
    }
  \]

  Note that positions 0 is in the \rootc\ context, while position 10 is in a
  \negc\ context, positions 13 and 15 are in a \mix\ context, and the rest are
  in a \pos\ context.

  The result of flattening with full reification is:

  \begin{mzn}
    constraint b0 <-> b1 \/ b2;
    constraint b0;
    constraint b1 <-> b2 /\ b1';
    constraint b1' <-> v3 >= 4;
    constraint b2 <-> b4 /\ b5;
    constraint b3 <-> b6 /\ b7;
    constraint minus(v6, v7, v3);
    constraint b4 <-> b8 /\ b9;
    constraint b5 <-> (b10 -> b);
    constraint b6 <-> b11 /\ b12;
    constraint plus(v11, v12, v6);
    constraint b7;
    constraint bool2int(b10, v7);
    constraint b8 <-> b11 /\ b8'
    constraint b8' <-> v11 <= 2;
    constraint b9 <-> x > y;
    constraint b10 <-> x > z;
    constraint b11 <-> b11';
    constraint v11' in 1..n;
    constraint element(v11', a, v11);
    constraint b11' <-> v11' = x;
    constraint b11' <-> x in 1..n;
    constraint b12;
    constraint bool2int(b9, v12);
  \end{mzn}

  % \(b_0 \full b_1 \vee b_2\), \(b_0\),
  % \(b_1 \full b_2 \wedge b_1'\), \(b_1' \full v_3 \geq 4\),
  % \(b_2 \full b_4 \wedge b_5\),
  % \(b_3 \full b_6 \wedge b_7\), \(minus(v_6,v_7,v_3)\),
  % \(b_4 \full b_8 \wedge b_9\),
  % \(b_5 \full (b_{10} \rightarrow b)\),
  % \(b_6 \full b_{11} \wedge b_{12}\), \(plus(v_{11},v_{12},v_6)\),
  % \(b_7\), \(bool2int(b_{10},v_7)\),
  % \(b_8 \full b_{11} \wedge b'_8\), \(b'_8 \full v_{11} \leq 2\),
  % \(b_9 \full x > y\),
  % \(b_{10} \full x > z\),
  % \(b_{11} \full b'_{11}\), \(v'_{11} \in \{1, \ldots, n\}\),
  % \(element(v'_{11}, a, v_{11})\), \(b'_{11} \full
  % v'_{11} = x\), \(b'_{11} \full x \in \{1, \ldots, n\}\),
  % \(b_{12}\), \(bool2int(b_{9}, v_{12})\)
  where we use the position as underscore on the variable. Note that we use CSE
  to reuse variables from position 11 for position 14, position 9 for position
  15, and position 10 for position 13. We dont expand the array \(a\) for
  simplicity, we assume it has \(n\) entries. We can simplify the resulting
  formulae by removing always true literals and replacing equivalent literals,
  resulting in

  \begin{mzn}
    constraint b1 \/ b2;
    constraint b1 <-> b3 /\ b1';
    constraint b1' <-> v3 >= 4;
    constraint b2 <-> b4 /\ b5;
    constraint minus(v6, v7, v3);
    constraint b4 <-> b8 /\ b9;
    constraint b5 <-> (b10 -> b);
    constraint plus(v11, v12, v6);
    constraint bool2int(b10, v7);
    constraint b8 <-> b3 /\ b8'
    constraint b8' <-> v11 <= 2;
    constraint b9 <-> x > y;
    constraint b10 <-> x > z;
    constraint v11' in 1..n;
    constraint element(v11', a, v11);
    constraint b3 <-> v11' = x;
    constraint b3 <-> x in 1..n;
    constraint bool2int(b9, v12);
  \end{mzn}

  % \(b_1 \vee b_2\),
  % \(b_1 \full b_3 \wedge b_1'\), \(b_1' \full v_3 \geq 4\),
  % \(b_2 \full b_4 \wedge b_5\),
  % \(minus(v_6,v_7,v_3)\),
  % \(b_4 \full b_8 \wedge b_9\),
  % \(b_5 \full (b_{10} \rightarrow b)\),
  % \(plus(v_{11},v_{12},v_6)\),
  % \(bool2int(b_{10},v_7)\),
  % \(b_8 \full b_{3} \wedge b'_8\), \(b'_8 \full v_{11} \leq 2\),
  % \(b_9 \full x > y\),
  % \(b_{10} \full x > z\),
  % \(v'_{11} \in \{1, \ldots, n\}\), \(element(v'_{11}, a, v_{11})\), \(b_{3} \full
  % v'_{11} = x\), \(b_{3} \full x \in \{1, \ldots, n\}\),
  % \(bool2int(b_{9}, v_{12})\);
  a total of 18 primitive constraints and 14 intermediate variables introduced.
\end{example}
\jip{Maybe make this fit better}

% Since the constraint solver only deals with a flat conjunction of constraints,
% modelling languages that support more complex constraint forms need to
% \emph{flatten} them into a form acceptable to the solver. The usual method for
% flattening complex formula of constraints is full reification. Given a
% constraint \(c\) the \emph{full reified form} for \(c\) is \(b \full c\), where
% \(b \not\in vars(c)\) is a Boolean variable naming the satisfied state of the
% constraint \(c\).

%\newcommand{\new}{\textbf{new}~}
%\newcommand{\flatc}{\textsf{flatc}}
%\newcommand{\flatt}{\textsf{flatt}}
\newcommand{\safen}{\textsf{safen}}

% The pseudo-code for \flatc(\(b\),\(c\)) flattens a constraint expression \(c\) to be
% equal to \(b\), returning a set of constraints implementing \(b \full c\). We
% flatten a whole model \(c\) using \(\flatc(\mzninline{true}, c)\). In the pseudo-code the
% expressions \(\new b\) and \(\new v\) create a new Boolean and integer variable
% respectively.

% The code assumes there are reified versions of the basic relational
% constraints \(r\) available, as well as reified versions of the Boolean
% connectives. Flattening of arbitrary constraint predicates aborts if not at
% the top level of conjunction. The code handles unsafe terms by capturing them
% when they first arrive at a Boolean context using \safen.

% {\small
% \begin{tabbing}
% xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill
% \flatc(\(b\),\(c\)) \\
% \> \textbf{switch} \(c\) \\
% \> \textbf{case} \texttt{true}: \textbf{return} \(\{ b \}\) \\
% \> \textbf{case} \texttt{false}: \textbf{return} \(\{ \neg b \}\) \\
% \> \textbf{case} \(b'\) (\syntax{<bvar>}): \textbf{return} \(\{ b \full b' \}\) \\
% \> \textbf{case} \(t_1\) \(r\) \(t_2\) (\relop):  \textbf{return} \(\safen(b, \flatt(\new i_1, t_1) \cup \flatt(\new i_2, t_2)) \cup \{ b \full i_1~r~i_2 \}\) \\
% \> \textbf{case} \texttt{not} \(c_1\):
% \textbf{return} \(\flatc(\new b_1, c_1) \cup \{ b \full \neg b_1 \}\) \\
% \> \textbf{case} \(c_1\) \verb+/\+ \(c_2\): \=
% \textbf{if} (\(b \equiv \mzninline{true}\))  \textbf{return} \(\flatc(\mzninline{true}, c_1) \cup
%            \flatc(\mzninline{true}, c_2)\) \\
% \> \> \textbf{else} \textbf{return} \(\flatc(\new b_1, c_1) \cup
%            \flatc(\new b_2, c_2) \cup \{ b \full (b_1 \wedge b_2)\}\) \\
% xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill
% \> \textbf{case} \(c_1\) \verb+\/+ \(c_2\): \textbf{return} \(\flatc(\new b_1, c_1) \cup
%            \flatc(\new b_2, c_2) \cup \{ b \full (b_1 \vee
%            b_2)\}\) \\
% \> \textbf{case} \(c_1\) \verb+->+ \(c_2\): \textbf{return} \(\flatc(\new b_1, c_1) \cup
%            \flatc(\new b_2, c_2) \cup \{ b \full (b_1 \half
%            b_2)\}\) \\
% \> \textbf{case} \(c_1\) \verb+<->+ \(c_2\): \textbf{return} \(\flatc(\new b_1, c_1) \cup
%            \flatc(\new b_2, c_2) \cup \{ b \full (b_1 \full
%            b_2)\}\) \\
% \> \textbf{case} \(p\) (\(t_1, \ldots, t_n\)) (\syntax{<pred>}): \\
% \> \> \textbf{if} (\(b \equiv \mzninline{true}\)) \textbf{return} \(\safen(b,
% \cup_{j=1}^n \flatt(\new v_j, t_j)) \cup \{ p(v_1, \ldots, v_n) \}\) \\
% \> \> \textbf{else} \textbf{abort}
% \end{tabbing}
% }

%   The code \(\flatt(v,t)\) flattens an integer term \(t\), creating constraints
%   that equate the term with variable \(v\). It creates new variables to store
%   the values of subterms, replaces integer operations by their relational
%   versions, and array lookups by \element.

% \begin{tabbing}
% xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill
% \flatt(\(v\),\(t\)) \\
% \> \textbf{switch} \(t\) \\
% \> \textbf{case} \(i\) (\intc): \textbf{return} \(\{v = i\}\) \\
% \> \textbf{case} \(v'\) (\syntax{<ivar>}): \textbf{return} \(\{ v = v' \}\) \\
% \> \textbf{case} \(t_1\) \(a\) \(t_2\) (\syntax{<arithop>}):
% \textbf{return} \(\flatt(\new v_1, t_1) \cup \flatt(\new v_2, t_2) \cup \{ a(v_1, v_2, v) \}\) \\
% \> \textbf{case} \(a\) \texttt{[} \(t_1\) \texttt{]}:
% \textbf{return} \(\flatt(\new v_1, t_1) \cup \{ \texttt{element}(v_1, a, v) \}\) \\
% \> \textbf{case} \texttt{bool2int(} \(c_1\) \texttt{)}:
% \textbf{return} \(\flatc(\new b_1, c_1) \cup  \{ \texttt{bool2int}(b_1,v) \})\)
% \end{tabbing}

The procedure \safen(\(b, C\)) enforces the relational semantics for unsafe
expressions, by ensuring that the unsafe relational versions of partial
functions are made safe. Note that to implement the \emph{strict semantics} as
opposed to the relational semantics we just need to define \(\safen(b,C) = C\).
If \(b \equiv \mzninline{true}\) then the relational semantics and the strict
semantics coincide, so nothing needs to be done. The same is true if the set of
constraints \(C\) is safe. For \(div(x,y,z)\), the translation introduces a new
variable \(y'\) which cannot be 0, and equates it to \(y\) if \(y \neq 0\). The
constraint \(div(x,y',z)\) never reflects a partial function application. The
new variable \(b'\) captures whether the partial function application returns a
non \undefined{} value. For \mzninline{element(v, a, x)}, it introduces a new
variable \(v'\) which only takes values in \(\dom(a)\) and forces it to equal
\(v\) if \(v \in \dom(a)\). A partial function application forces
\(b = \mzninline{false}\) since it is the conjunction of the new variables
\(b'\). The \%HALF\% comments will be explained later.

\begin{tabbing}
xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill
\safen(\(b\),\(C\)) \\
\> \textbf{if} (\(b \equiv \mzninline{true}\)) \textbf{return} \(C\) \\
\> \textbf{if} (\(C\) is a set of safe constraints) \textbf{return} \(C\) \\
\> \(B\) := \(\emptyset\); \(S\) := \(\emptyset\)  \\
\> \textbf{foreach} \(c \in C\) \\
\> \> \textbf{if} (\(c \equiv div(x,y,z)\) and \(y\) can take value 0) \\
\> \> \> \(B\) := \(B \cup \{ \new b' \}\) \\
\> \> \> \(S\) := \(S \cup \{ \new y' \neq 0, b' \full y \neq 0, b' \full y
= y', div(x,y',z) \}\) \\
\> \> \> \%HALF\% \(S\) := \(S \cup \{ b' \full y \neq 0, b' \half
div(x,y,z)\}\) \\
\> \> \textbf{else if} \(c \equiv \mzninline{element(v, a, x)}\) and \(v\) can take a value outside the domain of \(a\)) \\
\> \> \> \(B\) := \(B \cup \{ \new b' \}\) \\
\> \> \> \(S\) := \(S \cup \{ \new v' \in \dom(a),
b' \full v \in \dom(a), b' \full v = v',
\mzninline{element(v', a, x)}\}\) \\
\> \> \> \%HALF\% \(S\) := \(S \cup \{ b' \full v \in \dom(a), b' \half
\mzninline{element(v, a, x)}\}\) \\
\> \> \textbf{else} \(S\) := \(S \cup \{c\}\) \\
\> \> \textbf{return} \(S \cup \{b \full \wedge_{b' \in B} b'
\})\)
\end{tabbing}

The flattening algorithms above can produce suboptimal results in special cases,
such as input with common subexpressions. Our implementation avoids generating
renamed-apart copies of already-generated constraints, but for simplicity of
presentation, we omit the algorithms we use to do this.

\section{Half Reification}
\label{sec:hr-halfreif}

Given a constraint \mzninline{pred(@\ldots{}@)}, the \emph{half-reified version}
of \mzninline{pred(@\ldots{}@)} is a constraint of the form \mzninline{b ->
  pred(@\ldots{}@)} where \(\mzninline{b} \not\in vars(c)\) is a Boolean
variable.

We can construct a propagator \(f_{\mzninline{b -> pred(@\ldots{}@)}}\) for the
half-reified version of \mzninline{pred(@\ldots{}@)}, \mzninline{b ->
  pred(@\ldots{}@)}, using the propagator \(f_{\mzninline{pred(@\ldots{}@)}}\)
for \mzninline{pred(@\ldots{}@)}.

\[
\begin{array}{rcll}
f_{b \half c}(D)(b) & = &  \{ \mzninline{false} \} \cap D(b) & \text{if~} f_c(D) \text{~is a false domain} \\
f_{b \half c}(D)(b) & = & D(b) & \text{otherwise} \\
f_{b \half c}(D)(v) & = & D(v) & \text{if~} v \in vars(c) \text{~and~} \mzninline{false} \in D(b) \\
f_{b \half c}(D)(v) & = & f_c(D)(v) & \text{if~} v \in vars(c)
\text{~and~} \mzninline{false} \not\in D(b)
\end{array}
\]

% In reality most propagator implementations for \(c\) can be thought of as
% a sequence of two propagators \(f_c = f_{prop(c)} \cdot f_{check(c)}\)
% where
% \[
% \begin{array}{rcll}
% f_{check(c)}(D)(v) & = & \emptyset & f_c(D) \text{~is a false domain} \\
% f_{check(c)}(D)(v) & = & D(v)      & \text{otherwise} \\
% f_{prop(c)}(D)(v)  & = & D         & \(D\) \text{~is a false domain} \\
% f_{prop(c)}(D)(v) & = & f_c(D)(v)      & \text{otherwise} \\
% \end{array}
% \]
% that is first we check whether constraint is satisfiable \(check(c)\)
% and if so we propagate changes in variable domains \(prop(c)\).

% \begin{example}
%   Most propagators check consistency before propagating: e.g.
%   \(\sum_i a_i x_i \leq a_0\) determines \(L = \sum_i min_D(a_i x_i) - a_0\) and
%   fails if \(L > 0\) before propagating \autocite{harveyschimpf}; Regin's domain
%   propagator \autocite{reginalldifferent} for \alldiff\(([x_1, \ldots, x_n])\)
%   determines a maximum matching between variables and values first, if this is
%   not of size \(n\) it fails before propagating; and the timetable
%   \texttt{cumulative} constraint~\autocite{cumulative} determines a profile of
%   necessary resource usage, and fails if this breaks the resource limit,
%   before considering propagation. \qed
% \end{example}

% Given this separation we can improve the definition of \(f_{b \half c}\) above by
% replacing the check ``\(f_c(D)\) is a false domain'' by ``\(f_{check(c)}(D)\) is a
% false domain''. In practice it means that the half-reified propagator can be
% implemented to only perform the checking part until \(D(b) = \{\mzninline{true}\}\), when it
% needs to perform both.

In practice most propagator implementations for \mzninline{pred(@\ldots{}@)}
first check whether \mzninline{pred(@\ldots{}@)} is satisfiable, before
continuing to propagate. For example, \mzninline{sum(i in N)(a[i] * x[i]) <= C}
determines \mzninline{L = sum(i in N)(lb(a[i] * x[i])) - C} and fails if
\mzninline{L > 0} before propagating; Regin's domain propagator for
\mzninline{all_different(X)} determines a maximum matching between variables and
values first, if this is not of size \mzninline{length(X)} it fails before
propagating; the timetable \texttt{cumulative} constraint determines a profile
of necessary resource usage, and fails if this breaks the resource limit, before
considering propagation. We can implement the propagator for
\(f_{\mzninline{b -> pred(@\ldots{}@)}}\) by only performing the checking part
until \(D(\texttt{b}) = \{\mzninline{true}\}\).

Half reification naturally encodes the relational semantics for partial function
applications in positive contexts. We associate a Boolean variable \mzninline{b}
with each Boolean term in an expression, and we ensure that all unsafe
constraints are half-reified using the variable of the nearest enclosing Boolean
term.

\begin{example}
  Consider flattening of the constraint of \cref{ex:hr-cons}. First we will convert
  it to an equivalent expression with only positive contexts

  \begin{mzn}
    i > 4 \/ a[i] * x >= 6
  \end{mzn}

  There are three Boolean terms: the entire constraint, \mzninline{i > 4} and
  \mzninline{a[i] * x >= 6}, which we name \mzninline{b0}, \mzninline{b1}, and
  \mzninline{b2} respectively. The flattened form using half reification is

  \begin{mzn}
    constraint b1 -> i > 4;
    constraint b2 -> element(i,a,t1);
    constraint mult(t1,x,t2);
    constraint b2 -> t2 >= 6;
    constraint b1 \/ b2;
  \end{mzn}

  The unsafe \mzninline{element} constraint is half reified with the name of its
  nearest enclosing Boolean term. Note that if \mzninline{i = 7} then the second
  constraint makes \mzninline{b2 = false}. Given this, the final constraint
  requires \mzninline{b1 = true}, which in turn requires \mzninline{i > 4}.
  Since this holds, the whole constraint is \mzninline{true} with no
  restrictions on \mzninline{x}.
\end{example}

Half reification can handle more constraint terms than full reification if we
assume that each global constraint predicate \(p\) is available in half-reified
form. Recall that this places no new burden on the solver implementer.

\begin{example}
  Consider the constraint of \cref{ex:hr-alldiff}. Half reification results in

  \begin{mzn}
    constraint b1 -> i > 4;
    constraint minus(i,x,t1);   % t1 = i - x
    constraint b2 -> all_different([i,t1,x]);
    constraint b1 \/ b2         % b1 or b2
  \end{mzn}

  We can easily modify any existing propagator for \mzninline{all_different} to
  support the half-reified form, hence this model is executable by our
  constraint solver.
\end{example}

Half reification can lead to more efficient constraint solving, since it does
not propagate unnecessarily.

\begin{example}\label{ex:hr-cumul}
  Consider the task decomposition of a \texttt{cumulative} constraint (see \eg\
  \autocite{schutt-2009-cumulative}) which includes constraints of the form

  \begin{mzn}
    constraint sum(i in Tasks where i != j) (
      bool2int(s[i] <= s[j] /\ s[i]+d[i] > s[j]) * r[i]
    ) <= L-r[j];
  \end{mzn}

  which requires that at the start time \mzninline{s[j]} of task \mzninline{j},
  the sum of resources \mzninline{r} used by it and by other tasks executing at
  the same time is less than the limit \mzninline{L}. Flattening with full
  reification produces constraints like this:

  \begin{mzn}
    constraint b1[i] <-> s[i] <= s[j];
    constraint plus(s[i],d[i],e[i]);     % e[i] = s[i] + d[i]
    constraint b2[i] <-> e[i] > s[j];
    constraint b3[i] <-> b1[i] /\ b2[i];
    constraint bool2int(b3[i], a[i]);    % a[i] = bool2int(b3[i])
    constraint sum(i in Tasks where i != j)( a[i] * r[i] ) <= L-r[j];
  \end{mzn}

  Whenever the start time of task \mzninline{i} is constrained so that it does
  not overlap time \mzninline{s[j]}, then \mzninline{b3[i]} is fixed to
  \mzninline{false} and \mzninline{a[i]} to 0, and the long linear sum is
  awoken. But this is useless, since it cannot cause failure.

  The Boolean expression appears in a negative context, and half-reification
  produces

  \begin{mzn}
    constraint b1[i] -> s[i] > s[j];
    constraint plus(s[i],d[i],e[i]);     % e[i] = s[i] + d[i]
    constraint b2[i] -> e[i] <= s[j];
    constraint b3[i] -> b1[i] \/ b2[i];
    constraint b4[i] <-> not b3[i];
    constraint bool2int(b4[i], a[i]);    % a[i] = bool2int(b4[i])
    constraint sum(i in Tasks where i != j)( a[i] * r[i] ) <= L-r[j];
  \end{mzn}

  which may seem to be more expensive since there are additional variables (the
  \mzninline{b4[i]}), but since both \mzninline{b4[i]} and \mzninline{a[i]} are
  implemented by views \autocite{schulte-2005-views}, there is no additional
  runtime overhead. This decomposition will only wake the linear constraint when
  some task \mzninline{i} is guaranteed to overlap time \mzninline{s[j]}.
\end{example}

\pjs{Add linearization example here!}

Half reification can cause propagators to wake up less frequently, since
variables that are fixed to \mzninline{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. We can reduce this
disadvantage by fully reifying Boolean connectives (which have low overhead)
where possible in the half reification. \pjs{Do we do this?}

\subsection{Flattening with Half Reification}

\newcommand{\halfc}{\textsf{halfc}}
\newcommand{\halft}{\textsf{halft}}
\newcommand{\halfnc}{\textsf{halfnc}}

We describe flattening using half reification in a manner analogous to
flattening using full reification. We concentrate once more on flattening
constraint items, although we shall treat objectives differently than the simple
rewriting used with full reification.

The procedure \(\halfc(b,\mzninline{pred(@\ldots{}@)})\) defined below returns a
set of constraints implementing the half-reification \mzninline{b ->
  pred(@\ldots{}@)}. We flatten a constraint item \mzninline{constraint
  pred(@\ldots{}@)} using
\(\halfc(\mzninline{true}, \mzninline{pred(@\ldots{}@)})\). The half-reification
flattening transformation uses half reification whenever it is in a positive
context. If it encounters a constraint \mzninline{c1} in a negative context, it
negates the constraint if it is safe, thus creating a new positive context. If
this is not possible, it defaults to the usual flattening approach using full
reification. Note how for conjunction it does not need to introduce a new
Boolean variable. Negating a constraint expression is done one operator at a
time, and is defined in the obvious way. For example, negating \mzninline{t1 <
  t2} yields \mzninline{t1 >= t2}, and negating \mzninline{c1 /\ c2} yields
\mzninline{not c1 \/ not c2}. Any negations on subexpressions will be processed
by recursive invocations of the algorithm.

\newcommand{\bnds}{\mathit{bnds}}
\newcommand{\sign}{\textsf{sign}}
\newcommand{\iabove}{\textsf{ub}}
\newcommand{\ibelow}{\textsf{lb}}
\newcommand{\iboth}{\textsf{both}}
\newcommand{\negaterel}{\textsf{negaterel}}

Halfreifying a constraint \(c\) in context \ctxt, \(\halfc(c,\ctxt)\), returns a
Boolean literal \(b\) representing the constraint and as a side effect adds a set
of constraints (the flattening) \(S\) to the store such that
\(S \models b \half c\). The half reification function is only called with
\(\ctxt = \rootc\) or \(\ctxt = \pos\) if negative or mixed contexts arise we use
\(\flatc\) instead. The procedure \(\halfc\) is very similar to \(\flatc\). The main
difference is that we use implication \((\half)\) to connect the Boolean literal
\(b\) of a constraint to its component parts, and use half reified versions of the
primitive constraints. We also can simplify most translations.

The treatment of common subexpressions is simpler. We use a separate hash table.
If the previous context was the \(\rootc\), or the same we simply reuse the old
value. The remaining case is when the new context is \(\rootc\) and the previous
was \(\pos\). Then we force the variable to hold and update the hash table for
both half and full reification. When we store the result we construct for half
reification we also add an entry to the full reification hash table if the
context is \(\rootc\), in case we meet the same term in a negative or mxed context
later.

The translation of relational operators is similar to \(\flatc\) except we use a
half reification specialized version of flattening terms \(\halft\). This takes as
an extra argument the \emph{bounds} of the term we are interested in, these
could be: \(\iabove\) we are only interested in the upper bound, \(\ibelow\) we are
only interested in the lower bound, or \(\iboth\) we are interested in both bounds
and interior values. For example for the constraint \(b \half x \leq y\) we are
only interested in the lower bound of \(x\) and the upper bound of \(y\) since these
are the only bounds that can cause failure.

Half reifying constaints of the form \(\texttt{not}~c\) is handled by the
procedure \(\halfnc\), which pushes the negation through operations where this is
safe to do so. We discuss it in detail later. Half reification of the Boolean
connectives is very similar to full reification, it treats \(c_1~\verb+->+~c_2\)
and \(\texttt{not}~c_1 \vee c_2\) and full reification for \(c_1~\verb+<->+~c_2\).
\texttt{forall} and \texttt{exists} are treated analogously to \verb+/\+ and
\verb+\/+.

Array lookup had to flatten the index term in a manner that is interested in
everything about its value (\(\iboth)\). The translation use a half reified
\mzninline{element} constraint which ensures safety, much simpler than in full
reification. All calls to built-in predicate \(p\) can be half reified assuming
we have the half reified version of the predicate \(p\_half\). Since this can be
created using the propagator for \(p\), this is a fair assumption.

User defined predicates, if-then-else-endif and let are treated analogously to
full reification.

\begin{tabbing}
xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill
\halfc(\(c\),\(\ctxt\)) \\
\> \(\tuple{h,prev}\) := hhash[\(c\)];  \\
\> \textbf{if} (\(h \neq \undefined{}\)) \\
\>\> \textbf{if} (\(prev =\rootc \vee prev = \ctxt\)) \textbf{return} \(h\)  \\
\>\> \(S\) \cupp \(\{ h \}\); hhash[\(c\)] :=
\(\tuple{h,\rootc}\); hash[\(c\)] :=
\(\tuple{h,\rootc}\); \textbf{return} \(h\)
\\
\> \textbf{if} (\(\fixed(c)\)) \(b\) := \(\eval(c)\) \\
\> \textbf{else} \\
\> \> \textbf{switch} \(c\) \\
%\> \> \textbf{case} \texttt{true}: \(b\) := \(\mzninline{true}\);\\
%\> \> \textbf{case} \texttt{false}: \(b\) := \(\mzninline{false}\);\\
\> \> \textbf{case} \(b'\) (\syntax{<bvar>}): \(b\) := \(b'\); \\
\> \> \textbf{case} \(t_1\) \(r\) \(t_2\) (\syntax{<relop>}):  \\
\> \> \> \textbf{switch} \(r\) \\
\> \> \> \textbf{case} \(\leq\), \(<\): \(\tuple{v_1, b_1}\) := \(\halft(t_1,\ctxt,\iabove)\);
\(\tuple{v_2, b_2}\) := \(\halft(t_2,\ctxt,\ibelow)\); \\
\> \> \> \textbf{case} \(\geq\), \(>\): \(\tuple{v_1, b_1}\) := \(\halft(t_1,\ctxt,\ibelow)\);
\(\tuple{v_2, b_2}\) := \(\halft(t_2,\ctxt,\iabove)\); \\
\> \> \> \textbf{case} \(=\), \(\neq\):  \(\tuple{v_1, b_1}\) := \(\halft(t_1,\ctxt,\iboth)\);
\(\tuple{v_2, b_2}\) := \(\halft(t_2,\ctxt,\iboth)\); \\
\> \> \> \textbf{endswitch} \\
\> \> \> \(S\) \cupp \(\{ \new b \half (b_1 \wedge b_2 \wedge \new b'),
                       b' \half v_1~r~v_2\}\) \\
\> \> \textbf{case} \texttt{not} \(c_1\):
\(b\) := \(\halfnc(c_1, \ctxt)\) \\
\> \> \textbf{case} \(c_1\) \verb+/\+ \(c_2\):  \(S\) \cupp  \(\{ \new b \half (\halfc(c_1, \ctxt) \wedge \halfc(c_2, \ctxt))\}\)
\\
\>\> \textbf{case} \(c_1\) \verb+\/+ \(c_2\):
\(S\) \cupp \(\{ \new b \half (\halfc(c_1,\posop \ctxt) \vee \halfc(c_2,\posop \ctxt))\}\)
\\
\>\> \textbf{case} \(c_1\) \verb+->+ \(c_2\):
\(S\) \cupp  \(\{ \new b \half (\halfnc(c_1, \posop \ctxt) \vee \halfc(c_2,\posop \ctxt))\}\)
\\
\>\> \textbf{case} \(c_1\) \verb+<->+ \(c_2\):
\(S\) \cupp  \(\{ \new b \half (\flatc(c_1,\mix) \full
\flatc(c_2,\mix))\}\)
\\
\> \> \textbf{case} \texttt{forall(} \(ba\) \texttt{)}: \\
\> \> \> \textbf{let} \([c_1, \ldots, c_n] = \evalb(ba)\); \\
\> \> \> \textbf{foreach}(\(j \in 1..n\)) \(b_j\) := \(\halfc(c_j, \ctxt)\); \\
\>\>\> \(S\) \cupp \(\{ \new b \half \bigwedge_{j=1}^n b_j \}\) \\
\>\> \textbf{case} \texttt{exists(} \(ba\) \texttt{)}: \\
\> \> \> \textbf{let} \([c_1, \ldots, c_n] = \evalb(ba)\); \\
\> \> \> \textbf{foreach}(\(j \in 1..n\)) \(b_j\) := \(\halfc(c_j, \posop\ctxt)\); \\
\>\>\> \(S\) \cupp \(\{ \new b \half \bigvee_{j=1}^n b_j \}\) \\
\>\> \textbf{case} \([c_1, \ldots, c_n]\) \texttt{[} \(t\) \texttt{]}:  \\
\>\>\>
\textbf{foreach}(\(j \in 1..n\)) \(b_j\) := \(\halfc(c_j, \posop \ctxt)\); \\
\>\>\> \(\tuple{v, b_{n+1}}\) := \(\halft(t, \ctxt, \iboth)\); \\
%\>\>\> \(S\) \cupp
%\(\{ \new b \full (b_{n+1} \wedge \new b' \wedge \new b''),
%\mathit{safeelement}(v, [b_1, \ldots, b_n],  b'),
%b'' \full v \in \{1,..,n\} \} \) \\
\>\>\> \textbf{if} (\(\ctxt = \rootc\))
\(S\) \cupp \(\{\texttt{element}(v, [b_1, \ldots, b_n], \mzninline{true}), \new b\}\) \\
\>\>\> \textbf{else}
\(S\) \cupp \(\{ \new b \half (b_{n+1} \wedge \new b'), b \half
\texttt{element}(v, [b_1, \ldots, b_n],  b') \}\) \\
%\>\>\> \textbf{else} \\
%\>\>\>\> \(S\) \cupp \(\{ \new b \full (b_{n+1} \wedge \new b' \wedge \new b''), \new v' \in \{1,
%\ldots, n\},\) \\
%\>\>\>\>\>\>\> \(\texttt{element}(v', [b_1, \ldots, b_n],  b'),
%b'' \full v  = v', b'' \full v \in \{1,..,n\} \} \)
%\\
\>\> \textbf{case} \(p\) (\(t_1, \ldots, t_n\)) (\syntax{<pred>}) built-in predicate: \\
\> \> \> \textbf{foreach}(\(j \in 1..n\)) \(\tuple{v_j, b_j}\) :=
\(\halft(t_j,\ctxt,\iboth)\); \\
\> \> \> \textbf{if} (\(\ctxt = \rootc\))
\(b\) := \(\mzninline{true}\); \(S\) \cupp  \(\{ p(v_1, \ldots, v_n) %, \bigwedge_{j=1}^n b_j
\}\)
\\
\>\>\> \textbf{else} %(\(\ctxt = \pos\)) \\ \> \> \> \>
\(S\) \cupp \(\{ p\_half(v_1,\ldots,v_n,\new b'),
\new b \half b' \wedge \bigwedge_{j=1}^n b_j\}\) \\
%\> \>\> \textbf{else} \\
%\> \> \> \> \textbf{if} (\(p\_reif\) does not exist) \textbf{abort} \\
%\> \> \> \> \textbf{else} \(S\) \cupp \(\{ p\_reif(v_1,\ldots,v_n,\new b'),
%\new b \half b' \wedge \bigwedge_{j=1}^n b_j\}\) \\
%\\
\>\> \textbf{case} \(p\) (\(t_1, \ldots, t_n\)) (\syntax{<pred>}): user-defined predicate \\
\>\> \> \textbf{let} \(p(x_1, \ldots, x_n) = c_0\) be defn of \(p\) \\
\> \> \> \textbf{foreach}(\(j \in 1..n\)) \(\tuple{v_j, b_j}\) :=
\(\halft(t_j,\ctxt, \iboth)\); \\
\>\> \> \(\new b'\) := \(\halfc(c_0\subs{x_1/v_1, \ldots, x_n/v_n},\ctxt)\)
\\
\> \>\> \(S\) \cupp \(\{ \new b \half b' \wedge \bigwedge_{j=1}^n
b_j\}\)
\\
\> \> \textbf{case} \texttt{if} \(c_0\) \texttt{then} \(c_1\) \texttt{else}
\(c_2\) \texttt{endif}:
% \\ \> \> \>
\textbf{if} (\(\eval(c_0)\)) \(b\) := \(\halfc(c_1,\ctxt)\) \textbf{else} \(b\) := \(\halfc(c_2,\ctxt)\) \\
\>\> \textbf{case} \texttt{let \{} \(d\) \texttt{\} in} \(c_1\): \\
\>\> \> \textbf{let} \(\bar{v}'\) be a renaming of variables \(\bar{v}\) defined
in \(d\) \\
\> \> \> \(\tuple{c',\_}\) := \(\textsf{flatlet}(d\subs{\bar{v}/\bar{v}'},
c_1\subs{\bar{v}/\bar{v}'},0,\ctxt)\) \\
\> \> \> \(b\) := \(\halfc(c',\ctxt)\);
\\
\> \> \textbf{endswitch} \\
\> \textbf{if} (\(\ctxt = \rootc\)) \(S\) \cupp \(\{ b \}\); \\
\> hhash[\(c\)] := \(\tuple{b,\ctxt}\); \textbf{if} (\(\ctxt =
\rootc\)) hash[\(c\)] := \(\tuple{b,\ctxt}\); \\
\> \textbf{return} \(b\)
\end{tabbing}

Since half reification has advantages rather than give up on using it when we
encounter a negation we instead try to effectively transform the term under the
negation as much as possible by pushing negations down. The procedure
\(\halfnc(c,\ctxt)\), returns a Boolean literal \(b\) representing the
constraint and as a side effect adds a set of constraints (the flattening) \(S\)
to the store such that \(S \models b \half \neg c\). The \(\ctxt\) argument
stores the context for the term \(\neg c\) and again is only ever \(\rootc\) or
\(\pos\).

The procedure \(\halfnc\) use the same hash table but stores and looks up on the
key \(\texttt{not}~c\). When negating a basic relation we first check that the
subterms are safe, that is cannot involve partial functions, if this is the case
we can negate the relational operation and continue using half reification on
the terms. If not we use full reification.

A term of the form \(\texttt{not}~c\) simply half reifies \(c\), the negations
cancel. Boolean connectives are inverted using De Morgan's laws when we can
still use half reification. Again full reification for \(c_1~\verb+<->+~c_2\) is
used after inserting the negation. \texttt{forall} and \texttt{exists} are
treated analogously to \verb+/\+ and \verb+\/+.

Array lookup and built-in predicates are handled by full reification. User
defined predicates use full reification on the terms (since they occur in a
negative or mixed context) and negated half reification on the body.
If-then-else-endif and let are handled straightforwardly although note that the
context passed to \(\textsf{flatlet}\) is either \(\negc\) or \(\mix\).

\begin{tabbing}
xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill
\halfnc(\(c\),\(\ctxt\)) \\
\> \(\tuple{h,prev}\) := hhash[\(\texttt{not}~c\)];\\
\> \textbf{if} (\(h \neq \undefined\)) \\
\>\> \textbf{if} (\(prev =\rootc \vee prev = \ctxt\)) \textbf{return} \(h\) \\
\>\> \(S\) \cupp \(\{ h \}\); hhash[\(\texttt{not}~c\)] :=
\(\tuple{h,\rootc}\); hash[\(\texttt{not}~c\)] :=
\(\tuple{h,\rootc}\); \textbf{return} \(h\)\\
\> \textbf{if} (\(\fixed(c)\)) \(b\) := \(\neg \eval(c)\) \\
\> \textbf{else} \\
\> \> \textbf{switch} \(c\) \\
%\> \> \textbf{case} \texttt{true}: \(b\) := \(\mzninline{true}\);\\
%\> \> \textbf{case} \texttt{false}: \(b\) := \(\mzninline{false}\);\\
\> \> \textbf{case} \(b'\) (\syntax{<bvar>}): \(S\) \cupp \(\{\new b \half \neg b'\}\); \\
\> \> \textbf{case} \(t_1\) \(r\) \(t_2\) (\syntax{<relop>}):  \\
\> \> \> \textbf{if} (\(t_1\) and \(t_2\) are safe) \\
\> \> \> \> \(r'\) := \(\negaterel(r)\) \\
\> \> \> \> \textbf{switch} \(r'\) \\
\> \> \> \> \textbf{case} \(\leq\), \(<\): \(\tuple{v_1, b_1}\) := \(\halft(t_1,\ctxt,\iabove)\);
\(\tuple{v_2, b_2}\) := \(\halft(t_2,\ctxt,\ibelow)\); \\
\> \> \> \> \textbf{case} \(\geq\), \(>\): \(\tuple{v_1, b_1}\) := \(\halft(t_1,\ctxt,\ibelow)\);
\(\tuple{v_2, b_2}\) := \(\halft(t_2,\ctxt,\iabove)\); \\
\> \> \> \> \textbf{case} \(=\), \(\neq\):  \(\tuple{v_1, b_1}\) := \(\halft(t_1,\ctxt,\iboth)\);
\(\tuple{v_2, b_2}\) := \(\halft(t_2,\ctxt,\iboth)\); \\
\> \> \> \> \textbf{endswitch} \\
\> \> \> \> \(S\) \cupp \(\{ \new b \half (b_1 \wedge b_2 \wedge \new b'),
                       b' \half v_1 r' v_2\}\) \\
\> \> \> \textbf{else} \\
\> \> \> \> \(\new b\) := \(\flatc(\texttt{not} (t_1~r~t_2), \negop \ctxt)\) \\
\> \> \textbf{case} \texttt{not} \(c_1\):
\(b\) := \(\halfc(c_1, \ctxt)\) \\
\> \> \textbf{case} \(c_1\) \verb+/\+ \(c_2\):  \(S\) \cupp  \(\{ \new b \half (\halfnc(c_1, \posop\ctxt) \vee \halfnc(c_2, \posop\ctxt))\}\)
\\
\>\> \textbf{case} \(c_1\) \verb+\/+ \(c_2\):
\(S\) \cupp \(\{ \new b \half (\halfnc(c_1, \ctxt) \wedge \halfnc(c_2, \ctxt))\}\)
\\
\>\> \textbf{case} \(c_1\) \verb+->+ \(c_2\):
\(S\) \cupp  \(\{ \new b \half (\halfc(c_1, \posop\ctxt) \vee \halfnc(c_2,\posop \ctxt))\}\)
\\
\>\> \textbf{case} \(c_1\) \verb+<->+ \(c_2\):
\(b\) := \(\flatc(\texttt{not}~c_1~\verb+<->+~c_2, \ctxt)\)
\\
\> \> \textbf{case} \texttt{forall(} \(ba\) \texttt{)}: \\
\> \> \> \textbf{let} \([c_1, \ldots, c_n] = \evalb(ba)\); \\
\> \> \> \textbf{foreach}(\(j \in 1..n\)) \(b_j\) := \(\halfnc(c_j, \posop \ctxt)\); \\
\>\>\> \(S\) \cupp \(\{ \new b \half \bigvee_{j=1}^n b_j \}\) \\
\>\> \textbf{case} \texttt{exists(} \(ba\) \texttt{)}: \\
\> \> \> \textbf{let} \([c_1, \ldots, c_n] = \evalb(ba)\); \\
\> \> \> \textbf{foreach}(\(j \in 1..n\)) \(b_j\) := \(\halfnc(c_j, \ctxt)\); \\
\>\>\> \(S\) \cupp \(\{ \new b \half \bigwedge_{j=1}^n b_j \}\) \\
\>\> \textbf{case} \([c_1, \ldots, c_n]\) \texttt{[} \(t\) \texttt{]}:  \\
\>\>\> \(b\) := \(\flatc(\texttt{not}~[c_1, \ldots, c_n]~\texttt{[}~t~\texttt{]}, \ctxt)\) \\
\>\> \textbf{case} \(p\) (\(t_1, \ldots, t_n\)) (\syntax{<pred>}) built-in predicate: \\
\> \> \> \(b\) := \(\flatc(\texttt{not}~p(t_1, \ldots, t_n), \ctxt)\) \\
\>\> \textbf{case} \(p\) (\(t_1, \ldots, t_n\)) (\syntax{<pred>}): user-defined predicate \\
\>\> \> \textbf{let} \(p(x_1, \ldots, x_n) = c_0\) be defn of \(p\) \\
\> \> \> \textbf{foreach}(\(j \in 1..n\)) \(\tuple{v_j, b_j}\) :=
\(\flatt(t_j,\negop \ctxt)\); \\
\>\> \> \(\new b'\) := \(\halfnc(c_0\subs{x_1/v_1, \ldots, x_n/v_n},\ctxt)\)
\\
\> \>\> \(S\) \cupp \(\{ \new b \half b' \wedge \bigwedge_{j=1}^n
b_j\}\)
\\
\> \> \textbf{case} \texttt{if} \(c_0\) \texttt{then} \(c_1\) \texttt{else}
\(c_2\) \texttt{endif}:
% \\ \> \> \>
\textbf{if} (\(\eval(c_0)\)) \(b\) := \(\halfnc(c_1,\ctxt)\) \textbf{else} \(b\) := \(\halfnc(c_2,\ctxt)\) \\
\>\> \textbf{case} \texttt{let \{} \(d\) \texttt{\} in} \(c_1\): \\
\>\> \> \textbf{let} \(\bar{v}'\) be a renaming of variables \(\bar{v}\) defined
in \(d\) \\
\> \> \> \(\tuple{c',\_}\) := \(\textsf{flatlet}(d\subs{\bar{v}/\bar{v}'},
c_1\subs{\bar{v}/\bar{v}'},0,\negop \ctxt)\) \\
\> \> \> \(b\) := \(\halfnc(c',\ctxt)\);
\\
\> \> \textbf{endswitch} \\
\> \textbf{if} (\(\ctxt = \rootc\)) \(S\) \cupp \(\{ b \}\); \\
\> hhash[\(\texttt{not}~c\)] := \(\tuple{b,\ctxt}\); \textbf{if}
(\(\ctxt = \rootc\)) hash[\(\texttt{not}~c\)] := \(\tuple{b,\ctxt}\) \\
\> \textbf{return} \(b\)
\end{tabbing}

\subsection{Flattening Integer Expressions with Half Reification}

We use a specialized procedure to flatten terms for half reification. The
procedure \(\halft(t, \ctxt, \bnds)\) flattens term \(t\) in context \(\ctxt\)
(which again can only be \(\rootc\) or \(\pos\)) when we are interested in
\(\bnds\) of term \(t\). It returns a pair \(\tuple{v,b}\) and adds constraints
to \(S\) that enforce that \(b \half v = t\). The third argument is there to
create accurate context information when we meet terms of the form
\(\texttt{bool2int(} \)c\( \texttt{)}\). It acts independently of the context.

We flatten objective functions \(e\) using this procedure also. The item
\mzninline{solve maximize e} using \(\halft(e, \rootc, \ibelow)\) since we are
interested only in the lower bounds of the expression (analogous to the
constraints we will place on the expression \(e > d\) for some constant \(d\)),
and similarly we flatten \mzninline{solve minimize e} is flattened using
\(\halft(e, \rootc, \iabove)\). The integer variable returned is used as the
objective in the flattened program.

The common subexpression handling is somewhat complicated. The hash table for
terms stores the variable \(h\) holding the results, the Boolean \(b'\)
determining if the constraints arising from partial functions, and the previous
context and bounds. If the previous context was root or the context are the same
we examine the bounds. If they are the same we reuse the result, otherwise we
set the \(\bnds\) to \(\iboth\) and reflatten since we require both bounds
(perhaps in different situations). Otherwise the new context is \(\rootc\) and
the previous \(\pos\), we force \(b'\) to be \mzninline{true} in \(S\), and then
reuse the result if the bounds are the same, or set \(\bnds\) to \(\iboth\) and
reflatten. We store the result found at the end of flattening, note that we only
need one entry: context can move from \pos\ to \rootc\ and bounds can move from
one of \(\iabove\) or \(\ibelow\) to \(\iboth\).

The case of arithmetic operators is interesting since we need to propagate the
interest in bounds. Addition leaves us interested in the same bounds of both
subterms, subtraction reverses the bound we are interested in for the second
argument. Multiplication is the most complex case. If one argument has a known
sign we can accurately determine the bounds of interest in the other argument,
otherwise we lose all information (\(\iboth\)). We assume \(\sign(t)\) returns
one of the context operators \(\posop\) if \(\forall d \in poss(t). d \geq 0\)
and \(\negop\) if \(\forall d \in poss(t). d \leq 0\), and returns \(\pm\)
otherwise. We extend the context operators to work on bounds information as
follows:

\centerline{
\begin{tabular}{ccc}
\(
\begin{array}{lcl}
\posop \iabove & = &\iabove \\
\posop \ibelow & =& \ibelow \\
\posop \iboth & =& \iboth, \\
\end{array}
\)
&~&
\(
\begin{array}{lcl}
\negop \iabove & = &\ibelow \\
\negop \ibelow & =& \iabove \\
\negop \iboth & =& \iboth, \\
\end{array}
\)
\end{tabular}
}

For simplicity division simply loses all information. The half reification is
simpler for the partial function \texttt{div} requiring only the half reified
constraint.

Array lookup is again simpler in half reification where we use half reified
\mzninline{element} constraint. Array sums and if-then-else-endif are
straightforward.

The treatment of \mzninline{bool2int} is the reason for the complex bounds
analysis. If we are only interested in the lower bound of
\mzninline{bool2int(c)} we can half reify \(c\) since it is in a positive
context. If we are only interested in the upper bound of \mzninline{bool2int(c)}
we can negatively half reify \(c\) since \(c\) in a negative context, otherwise
we need to use full reification. The treatment of functions and let constructs
is analogous to that in \(\flatt\).


\begin{tabbing}
xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill
\halft(\(t\),\(\ctxt\),\(\bnds\)) \\
\> \(\tuple{h,b',prev,pbnds}\) := hhash[\(t\)];  \\
\> \textbf{if} (\(h \neq \undefined{}\)) \\
\>\> \textbf{if} (\(prev =\rootc \vee prev = \ctxt\)) \\
\>\> \> \textbf{if} (\(pbnds = \bnds\)) \textbf{return} \(\tuple{h,b'}\)  \\
\>\> \> \textbf{else} \(\bnds\) := \(\iboth\) \\
\>\> \textbf{else} \\
\> \> \> \(S\) \cupp \(\{ b' \}\) \\
\> \> \> \textbf{if} (\(pbnds = \bnds\)) hhash[\(t\)] := \(\tuple{h,b',\rootc,\bnds}\); \textbf{return} \(\tuple{h,b'}\)
\\
\> \> \> \textbf{else} \(\bnds\) := \(\iboth\) \\
\> \textbf{if} (\(\fixed(t)\)) \(v\) := \(\eval(t)\); \(b\) := \(\mzninline{true}\) \\
\> \textbf{else} %\\
%% \> \> \textbf{if} (\(t\) is marked \emph{total}) \(\ctxt\) := \(\rootc\) \\
%\> \>
\textbf{switch} \(t\) \\
%\> \> \textbf{case} \(i\) (\intc): \(v\) := \(i\); \(b\) := \(\mzninline{true}\) \\
\> \> \textbf{case} \(v'\) (\syntax{<ivar>}):  \(v\) := \(v'\); \(b\) := \(\mzninline{true}\)\\
\> \> \textbf{case} \(t_1\) \(a\) \(t_2\) (\syntax{<arithop>}): \\
\> \> \> \textbf{switch} \(a\) \\
\> \> \> \textbf{case} \(+\):
\(\tuple{v_1,b_1}\) := \(\halft(t_1,\ctxt,\bnds)\);
\(\tuple{v_2,b_2}\) := \(\halft(t_2,\ctxt,\bnds)\); \\
\> \> \> \textbf{case} \(-\):
\(\tuple{v_1,b_1}\) := \(\halft(t_1,\ctxt,\bnds)\);
\(\tuple{v_2,b_2}\) := \(\halft(t_2,\ctxt,\negop \bnds)\); \\
\> \> \> \textbf{case} \(\times\): \\
\> \> \> \> \textbf{if} (\(\sign(t_2) \in \{\posop,\negop\}\))
\(\tuple{v_1,b_1}\) := \(\halft(t_1,\ctxt,\sign(t_2)~\bnds)\); \\
\> \> \> \> \textbf{else}
\(\tuple{v_1,b_1}\) := \(\halft(t_1,\ctxt,\iboth)\); \\
\> \> \> \> \textbf{if} (\(\sign(t_1) \in \{\posop,\negop\}\))
\(\tuple{v_2,b_2}\) := \(\halft(t_2,\ctxt,\sign(t_1)~\bnds)\); \\
\> \> \> \> \textbf{else}
\(\tuple{v_2,b_2}\) := \(\halft(t_2,\ctxt,\iboth)\); \\
\> \> \> \textbf{case} \(\texttt{div}\):
\(\tuple{v_1,b_1}\) := \(\halft(t_1,\ctxt,\iboth)\);
\(\tuple{v_2,b_2}\) := \(\halft(t_2,\ctxt,\iboth)\); \\
\> \> \> \textbf{endswitch} \\
\> \> \> \textbf{if} (\(a \not\equiv \texttt{div} \vee \ctxt = \rootc\))
\(S\) \cupp \(\{ \new b \half (b_1 \wedge b_2), a(v_1,v_2,\new v) \}\) \\
%\> \> \> \textbf{else} \(S\) \cupp \(\{ \new b \full (b_1 \wedge b_2 \wedge
%\new b'), \mathit{safediv}(v_1,v_2,\new v), b' \full v_2 \neq 0 \}\) \\
\> \> \> \textbf{else}
\(S\) \cupp \(\{ \new b \half (b_1 \wedge b_2 \wedge
\new b'), b' \half \texttt{div}(v_1,v_2,\new v), \}\) \\
\> \> \textbf{case} \([t_1, \ldots, t_n]\) \texttt{[} \(t_{0}\) \texttt{]}: \\
\> \> \>
\textbf{foreach}(\(j \in 0..n\)) \(\tuple{v_j, b_j}\) := \(\halft(t_j,\ctxt,\iboth)\); \\
%\>\> \> \(S\) :=
%\(\{ \new b \full (\new b' \wedge \bigwedge_{j=0}^n b_j),
%\mathit{safeelement}(v_{0}, [v_1, \ldots, v_n],  \new v),
%b' \full v_0 \in \{1,...,n\} \}\)
%\\
\>\>\> \textbf{if} (\(\ctxt = \rootc\))  \(S\) \cupp \(\{\new b, \texttt{element}(v', [v_1, \ldots, v_n],
\new v) \}\) \\
\>\>\> \textbf{else} \\
\>\>\>\> \(S\) \cupp
\(\{ \new b \half (\new b' \wedge \bigwedge_{j=0}^n b_j),
b' \half \texttt{element}(v_0, [v_1, \ldots, v_n],  \new v), \} \)
\\
\> \> \textbf{case} \texttt{sum(} \(\mathit{ia}\) \texttt{)}: \\
\> \> \> \textbf{let} \([t_1, \ldots, t_n] = \evalb(ia)\); \\
\> \> \> \textbf{foreach}(\(j \in 1..n\)) \(\tuple{v_j, b_j}\) :=
\(\halft(t_j,\ctxt,\bnds)\); \\
\>\>\> \(S\) \cupp \(\{ \new b \half \bigwedge_{j=1}^n b_j,
                     \new v = \sum_{j=1}^n v_j \}\) \\
%\> \> \>
%\(\tuple{v,b}\) := \flatt(
%\textsf{foldl}(\(\evalb(ia)\), \texttt{0}, \texttt{+}), \(\ctxt\))
%\\
\> \> \textbf{case} \texttt{if} \(c_0\) \texttt{then} \(t_1\) \texttt{else}
\(t_2\) \texttt{endif}:
\\ \> \> \>
\textbf{if} (\(eval(c_0)\)) \(\tuple{v,b}\) := \(\halft(t_1,\ctxt,\bnds)\) \textbf{else}
\(\tuple{v,b}\) := \(\halft(t_2,\ctxt,\bnds)\)
\\
\>\> \textbf{case} \texttt{bool2int(} \(c_0\) \texttt{)}: \\
\> \> \>  \textbf{if} \((\bnds = \ibelow\)) \(b_0\) := \(\halfc(c_0, \pos)\); \\
\> \> \>  \textbf{elseif} \((\bnds = \iabove\)) \(b'_0\) := \(\halfnc(c_0,
\pos)\); \(S\) \cupp \(\{\new b_0 \full \neg b'_0\}\) \\
\> \> \>  \textbf{else} \(b_0\) := \(\flatc(c_0, \mix)\); \\
\> \> \> \(S\) \cupp \(\{ \texttt{bool2int}(b_0, \new v), \new b \}\)  \\
\>\> \textbf{case} \(f\) (\(t_1, \ldots, t_n\)) (\syntax{<func>}): function \\
\> \> \> \textbf{foreach}(\(j \in 1..n\)) \(\tuple{v_j, b_j}\) := \(\halft(t_j,\ctxt,\iboth)\); \\
\>\> \> \textbf{let} \(f(x_1, \ldots, x_n) = t_0\) be defn of \(f\) \\
\> \> \> \textbf{if} (\(f\) is declared total) \(\ctxt' = \rootc\) \textbf{else}
\(\ctxt' = \ctxt\) \\
\>\> \> \(\tuple{v,b'}\) := \(\halft(t_0\subs{x_1/v_1, \ldots, x_n/v_n},\ctxt',\bnds)\) \\
\> \> \> \(S\) \cupp \(\{ \new b \half b' \wedge \bigwedge_{j=1}^n b_j \}\)
\\
\>\> \textbf{case} \texttt{let \{} \(d\) \texttt{\} in} \(t_1\): \\
\>\> \> \textbf{let} \(\bar{v}'\) be a renaming of variables \(\bar{v}\) defined
in \(d\) \\
\> \> \> \(\tuple{c',t'}\) := \(\textsf{flatlet}(d\subs{\bar{v}/\bar{v}'},\texttt{true},
t_1\subs{\bar{v}/\bar{v}'},\ctxt)\) \\
\>\> \> \(\tuple{v,b_1}\) := \(\halft(t',\ctxt,\bnds)\);
\(b_2\) := \(\halfc(c',\ctxt)\);
\(S\) \cupp \(\{ \new b \half (b_1 \wedge b_2)\}\)
\\
\> \> \textbf{endswitch} \\
\> \textbf{if} (\(\ctxt = \rootc\)) \(S\) \cupp \(\{ b \}\); \\
\> hhash[\(t\)] := \(\tuple{v,b,\ctxt, \bnds}\) \\
\> \textbf{return} \(\tuple{v,b}\)
\end{tabbing}


% Half reification of terms returns a set of constraints that enforce \(v = t\) if
% the term \(t\) is safe, and \(b \half v = t\) otherwise. The most complex case is
% \texttt{bool2int}\((c_1)\), which half-reifies \(c_1\) if it is in a positive
% context, negates \(c_1\) and half-reifies the result if \(c_1\) is safe and in a
% negative context, and uses full flattening otherwise.

\begin{example}\label{ex:hr-half}
  Now lets consider half reifying the expression of \cref{ex:hr-flat}.

  The result of flattening with half reification is:

  \begin{mzn}
    constraint b0 -> b1 \/ b2;
    constraint b0;
    constraint b1 -> b2 /\ b1';
    constraint b1' -> v3 >= 4;
    constraint b2 -> b4 /\ b5;
    constraint b4 -> b8 /\ b9;
    constraint b3 -> b6 /\ b7;
    constraint minus(v6, v7, v3);
    constraint b4 -> b8 /\ b9;
    constraint b5 -> (b10 \/ b);
    constraint b6 -> b11 /\ b12;
    constraint plus(v11, v12, v6);
    constraint b7;
    constraint bool2int(b13, v7);
    constraint b13 <-> not b10;
    constraint b8 -> b11 /\ b8';
    constraint b8' -> v11 <= 2;
    constraint b9 -> x > y;
    constraint b10 -> x <= z;
    constraint b11 -> b11';
    constraint b11' -> element(x, a, v11);
    constraint b12;
    constraint bool2int(b9, v12);
  \end{mzn}

  Note that again we use CSE to reuse variables from position 11 for position
  14, position 9 for position 15, and position 10 for position 13.

  Half reification is significantly different from full reification in the
  treatment of the partial function array access, as well as the treatment of
  the negated context at 10 and 13. The bounds analysis finds the positions 1,
  3, 6, 11 are only interested in upper bounds, while positions 7 and 14 are
  only interested in lower bounds. This means that the positions 13 and 15 are
  reified using \halfnc{} and \halfc{} respectively even though they occur under
  a \(bool2int\). \pjs{explain more!}

  We can simplify the resulting formulae by removing always true literals and
  replacing literals \(b'\), which only occur in chains \(b'' \half b'\),
  \(b' \half e_1\), \(b' \half e_2\) etc, by \(b''\) resulting in

  \begin{mzn}
    constraint b1 \/ b2;
    constraint b1 -> v3 >= 4;
    constraint minus(v6, v7, v3);
    constraint b2 -> b9;
    constraint b2 -> (b10 \/ b);
    constraint b1 -> b11;
    constraint plus(v11, v12, v6);
    constraint bool2int(b13, v7);
    constraint b13 <-> not b10;
    constraint b2 -> b11 /\ b8';
    constraint b8' -> v11 <= 2;
    constraint b9 -> x > y;
    constraint b10 -> x <= z;
    constraint b11 -> element(x, a, v11);
    constraint bool2int(b9, v12);
  \end{mzn}

  with 15 primitive constraints and 12 intermediate variables. This reduces the
  number of constraints by 3 and the number of intermediate variables by 2.
\end{example}

\pjs{Extend and add section in implementation} As presented the half reification
transformation will construct many implications of the form \(b \half b'\), note
that the constraint \(b \half b_1 \wedge \cdots \wedge b_n\) is equivalent to
\(b \half b_1, b \half b_2, \ldots, b \half b_n\). Just as in \cref{ex:hr-half}
above we can simplify the result of half reification. For each \(b'\) which
appears only on the right of one constraint of the form \(b \half b'\) and other
constraints of the form \(b' \half c_i\) we remove the first constraint and
replace the others by \(b \half c_i\).

\subsection{Full Reification using Half Reification}

Usually splitting a propagator into two will reduce the propagation strength. We
show that modelling \(b \full c\) for primitive constraint \(c\) using
half-reified propagators as \(b \half c, b \full \neg b', b' \half \neg c\) does
not do so.%lose propagation strength.

To do so independent of propagation strength, we define the behaviour of the
propagators of the half-reified forms in terms of the full reified propagator.

\[
  \begin{array}{rcll}
    f_{b \half c}(D)(b) & = & D(b) \cap ( \{ \mzninline{false} \} \cup f_{b \full c}(D)(b)) \\
    f_{b \half c}(D)(v) & = & D(v) & \texttt{if}~v \in vars(c),~\mzninline{false} \in D(b) \\
    f_{b \half c}(D)(v) & = & f_{b \full c}(D)(v) & \texttt{if}~v \in vars(c),~\text{otherwise}
  \end{array}
\]

and

\[
  \begin{array}{rcll}
    f_{b' \half \neg c}(D)(b') & = & D(b') & \texttt{if}~\{ \mzninline{false} \} \in f_{b \full c}(D)(b) \\
    f_{b' \half \neg c}(D)(b') & = & D(b') \cap \{ \mzninline{false}\} &  \text{otherwise}\\
    f_{b' \half \neg c}(D)(v) & = & D(v) & \texttt{if}~v \in vars(c),~\mzninline{false} \in D(b') \\
    f_{b' \half \neg c}(D)(v) & = & f_{b \full c}(D)(v) & \texttt{if}~v \in vars(c),~\text{otherwise}
  \end{array}
\]

These definitions are not meant describe implementations, only to define how the
half reified split versions of the propagator should act.

In order to prove the same behaviour of the split reification versions we must
assume that \(f_{b \full c}\) is \emph{reified-consistent} which is defined as
follows: suppose \(f_{b \full c}(D)(v) \neq D(v), v \not\equiv b\), then
\(f_{b \full c}(D)(b) \neq \{ \mzninline{false}, \mzninline{true}\}\). That is
if the propagator ever reduces the domain of some variable, then it must also
fix the Boolean variable \(b\). This is sensible since if \(b\) is not fixed
then every possible value of \(v\) is consistent with constraint \(b \full c\)
regardless of the domain \(D\). This is a very weak assumption, every
implementation of reified constraints we are aware of satisfies this property,
and indeed only a deliberately inaccurate propagator would not.

For the sake of simplicity of proving the following theorem we also assume
\(f_{b \full c}\) is an \emph{idempotent} propagator, that is forall
\(D \sqsubseteq D_{init}\):
\(f_{b \full c}(D) = f_{b \full c}(f_{b \full c}(D))\). We assume the propagator
\(f_{b' \full \neg b}\) is domain consistent, which is the usual case for such a
trivial propagator.

% Define
% \(f_{b \half c}(D) =_{vars(b \full c)} \solv(\{f_{b'' \full c}, f_{b \half b''} \}, D)\),
% that is the half-reified version propagates on all variables only in the
% forward direction of the implication, by introducing the hidden variable
% \(b''\) which prevents propagation in the other direction. We assume a domain
% consistent propagator for \(b \half b''\). Similarly define
% \(f_{b' \half \neg c}(D) =_{vars(b' \full c)} \solv(\{f_{b''' \full c}, f_{b' \half \neg b'''} \}, D)\)

\jip{There is a proof here, but I don't have a proof environment yet}
% \begin{theorem}
%   \(\forall D. \solv(\{ f_{b \full c}, f_{b' \full \neg b}\})(D) = \solv(\{ f_{b \half c}, f_{b' \half \neg c}, f_{b' \full \neg b}\}, D)\).
% \end{theorem}
% \begin{proof}
%   Let \(V = vars(c)\). First w.l.o.g. we only consider domains \(D\) at a fixpoint
%   of the propagators \(f_{b' \full \neg b}\), i.e.
%   \(D(b') = \{ \neg d ~|~ d \in D(b)\}\), since both \(\solv\) expressions include
%   \(f_{b' \full \neg b}\). Let
%   \(D' = \solv(\{ f_{b \full c}, f_{b' \full \neg b}\})(D)\), now since
%   \(f_{b \full c}\) and \(f_{b' \full \neg b}\) are idempotent and \(D\) is a fixpoint
%   of \(f_{b' \full \neg b}\), then \(D' = f_{b' \full \neg b}(f_{b \full c}(D))\).
%   Let
%   \(D'' = \solv(\{ f_{b \half c}, f_{b' \half \neg c}, f_{b' \full \neg b}\}, D)\).
%   The proof is by cases of \(D\).

%   \textbf{(a)} Suppose \(D(b) = \{\mzninline{true},\mzninline{false}\}\). \textbf{(a-i)} Suppose
%   \(f_{b \full c}(D) = D\). Then clearly \(f_{b \half c}(D) = D\) by definition, and
%   similarly \(f_{b' \half \neg c}(D) = D\). Hence \(D_1 = D_2 = D\). Note that since
%   \(f_{b \full c}\) is reified consistent, then \(f_{b \full c}(D) \neq D\) implies
%   that \(f_{b \full c}(D)(b) \neq \{ \mzninline{false}, \mzninline{true} \}\). \textbf{(a-ii)} Suppose
%   \(f_{b \full c}(D)(b) = \{ \mzninline{true} \}\). Let \(D_1 = f_{b' \half \neg c}(D)\), then
%   \(D_1(b') = \{ \mzninline{false} \}\) by definition and \(D_1(v) = D(v), v \not\equiv b'\).
%   Let \(D_2 = f_{b' \full \neg b}(D_1)\) then \(D_2(b)= \{ \mzninline{true} \}\) and
%   \(D_2(v) = D(v), v \not\in \{b,b'\}\). Then
%   \(D_3 = f_{b \half c}(D_2) = f_{b \full c}(D_2)\) by definition, and by
%   idempotence of \(f_{b \full c}\) and since \(D_2\) and \(D\) differ only on \(b\) and
%   \(b'\) this is a fixpoint of \(f_{b \full c}\) and
%   \(D_3(v) = f_{b \full c}(D)(v), v \not \equiv b'\). \(D_3\) is also a fixpoint of
%   \(f_{b \half c}\), \(f_{b' \full \neg b}\) and \(f_{b' \half \neg c}\) and hence
%   \(D'' = D_3\). But also \(D' = f_{b' \full \neg b}(f_{b \full c}(D)) = D_3\) since
%   \(D_3\) and \(f_{b \full c}(D)\) only differ on \(b'\). \textbf{(a-iii)} Suppose
%   \(f_{b \full c}(D)(b) = \{ \mzninline{false} \}\). Let \(D_1 = f_{b \half c}(D)\), then
%   \(D_1(b) = \{ \mzninline{false} \}\) by definition and \(D_1(v) = D(v), v \not\equiv b\). Let
%   \(D_2 = f_{b' \full \neg b}(D_1)\) then \(D_2(b')= \{ \mzninline{true} \}\) and
%   \(D_2(v) = D(v), v \not\in \{b,b'\}\). Then
%   \(D_3 = f_{b' \half \neg c}(D_2) = f_{b \full c}(D_2)\) by definition, and by
%   idempotence of \(f_{b \full c}\) and since \(D_2\) and \(D\) differ only on \(b\) and
%   \(b'\) this is a fixpoint for \(f_{b \half c}\), \(f_{b' \full \neg b}\) and
%   \(f_{b' \half \neg c}\) and hence \(D'' = D_3\). But also
%   \(D' = f_{b' \full \neg b}(f_{b \full c}(D)) = D_3\) since \(D_3\) and
%   \(f_{b \full c}(D)\) only differ on \(b'\).

%   \textbf{(b)} If \(D(b) = \{\mzninline{true}\}\) then clearly \(f_{b \full c}\) and
%   \(f_{b \half c}\) act identically on variables in \(vars(c)\).

%   \textbf{(c)} If \(D(b) = \{\mzninline{false}\}\) then \(D(b') = \{\mzninline{true}\}\) and clearly
%   \(f_{b \full c}\) and \(f_{b' \half \neg c}\) act identically on variables in
%   \(vars(c)\). \qed
% \end{proof}

The reason for the generality of the above theorem which defines the
half-reified propagation strength in terms of the full reified propagator is
that we can now show that for the usual notions of consistency, replacing a
fully reified propagator leads to the same propagation.

Note that the additional variable \(b'\) can be implemented as a view
\autocite{schulte-2005-views} in the solver and hence adds no overhead.

\jip{The corollary environment is also missing}
% \begin{corollary}
%   A domain (resp. bounds(Z), bounds(R)) consistent propagator for \(b \full c\)
%   propagates identically to domain (resp. bounds(Z), bounds(R)) consistent
%   propagators for \(b \half c\), \(b \full \neg b'\), \(b' \half \neg c\). \qed
% \end{corollary}


\section{Propagation and Half Reification}

\pjs{What happens to this section?} A propagation engine gains certain
advantages from half-reification, 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
\(b \full c\) by two half reified propagators
\(b \half c, b' \half \neg c, b' \full \neg b\). This does not lose propagation
strength. For Booleans appearing in a positive context we can make the the
propagator \(b' \half \neg c\) run at the lowest priority, since it will never
cause failure. Similarly in negative contexts we can make the propagator
\(b \half c\) run at the lowest priority. This means that Boolean variables are
still fixed at the same time, but there is less overhead.


\section{Implementation in the \glsentrytext{minizinc} Distribution}

Implementing half-reification within the \minizinc\ distribution consists of two
parts: the \minizinc\ compiler needs to be extended with an implementation of
the half-reification flattening algorithm as described in \cref{sec:hr-halfreif}
and for any target solver that supports half-reification its library needs to be
appended with definitions for the predicates that are half-reified. Because the
\minizinc\ language allows for the definition of new predicates, we allow any
predicate to have an implemented half-reification, not just the predicates
defined as \flatzinc\ builtins.

The implementation of half-reification in \minizinc\ requires little change to
the translator. As the translator was already aware of the context of
expressions, we can track the context of each expression using annotations to
the expressions, which are native to the \minizinc\ language. Through the use of
common subexpression elimination, we use the same generated \flatzinc\ for the
same expression and are able to update the context annotation if it should be
required. In the translator, reifications are delayed until the full model is
flattened because further processing might reveal that a constraint might not
need to be reified. Because of this delay, we know that if a reification still
has a positive context annotation, then we can use a half-reified version of
that constraint if it is available without having both a fully reified version
and a half-reified version of the same constraint. Note that this might not be
true if the flattening of the reifications requires the addition of a full
reification of which a half-reified version was already used. Because this
situation is so uncommon, no solution for this situation is implemented. Our
implementation currently does not implement the transformations shown in
\halfnc\, which push down negations to avoid negative context. Although this
would likely improve number of possible half-reifications, we believe that the
positive effects of half-reifications will already be noticeable without this
optimisation.

Our implementation currently targets various linear solvers, including Gurobi
\autocite{gurobi-2021-gurobi} and Cbc (Coin-or branch and cut)
\autocite{lougee-heimer-2003-coin}, and Gecode \autocite{gecode-2021-gecode}.
Adding support for half-reification to the solver's \minizinc\ library can be
done in multiple ways: half-reified predicates can be be declared as solver
builtins, a redefinition using the \minizinc\ language can be provided for the
half-reified constraint, or a combination of the two can be used. Because Gecode
has propagators for half-reified constraints we have declared the corresponding
predicates as solver builtins. Gecode provides half-reified propagators for
almost all \flatzinc\ builtins. The other targeted solvers use the linear
library. The linear library \jip{,as seen before + reference???,} already has
redefinition for their fully reified predicates, \mzninline{b <-> c}. These
generally consist of two parts which are equivalent to the implications
\mzninline{b -> c /\ not b -> not c}. Because of this, the implementations of
the half-reified version of the same predicates usually consist of using only
one of these two parts, which will eliminate the need of many constraints. We
added half-reified versions for all predicates for which a full reification was
provided.

\subsection{Implication Chain Compression}

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 \mzninline{b1 -> b2 /\
  forall(i in N)(b2 -> c[i])}, which, if \texttt{b2} has no other usage in the
instance, can be resolved to \mzninline{forall(i in N)(b1 -> c[i])} 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. The following
pseudo code provides a formal specification for this algorithm.

\newcommand{\setminusp}{\ensuremath{\setminus}\text{:=}~}
\begin{tabbing}
  xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill
  \textsf{compress}(\(V\), \(E\)) \\
  \> \textbf{foreach} (\(x \in V\)) \\
  \> \> \textbf{if} \(|\{\tuple{a,x}| \tuple{a,x} \in E\}| = 1\) \(\land\) \(\lnot\) marked(\(x\))  \\
  \> \> \> \textbf{foreach} (\(\tuple{x, b} \in E\)) \\
  \> \> \> \> \(E\) \cupp \(\{ \tuple{a,b} \}\) \\
  \> \> \> \> \(E\) \setminusp \(\{ \tuple{x,b} \}\) \\
  \> \> \> \(E\) \setminusp \(\{\tuple{a,x}\}\) \\
  \> \> \> \(V\) \setminusp \(\{x\}\) \\
\end{tabbing}

\jip{Here we could actually show an example using a drawn graph}

The algorithm can be further improved by considering implied conjunctions. These
can be split up into multiple implications: \mzninline{b -> forall(i in
  N)(bs[i])} is equivalent to \mzninline{forall(i in N)(b -> bs[i])}. 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}

We ran our experiments on a server cluster using an Intel Xeon 8260. Each run
had exclusive access to 1 core of the CPU and 4 GB of RAM\@. The experiments are
available \jip{Insert new link} has our experimental \minizinc\ instances and
the infrastructure that performs the benchmarks.

The first experiment considers ``QCP-max'' problems which are defined as
quasi-group completion problems where the \mzninline{all_different} constraints
are soft, and the aim is to satisfy as many of them as possible.

\begin{mzn}
int: n; % size
array[1..n,1..n] of 0..n: s; % 0 = unfixed 1..n = fixed

array[1..n,1..n] of var 1..n: q; % qcp array;

constraint forall(i,j in 1..n where s[i,j] > 0)(q[i,j] = s[i,j]);

solve maximize
    sum(i in 1..n)(bool2int(all_different([q[i,j] | j in 1..n]))) +
    sum(j in 1..n)(bool2int(all_different([q[i,j] | i in 1..n])));

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}

Note that this is not the same as requiring the maximum number of disequality
constraints to be satisfied. The \mzninline{all_different} constraints, while
apparently in a mixed context, are actually in a positive context, since the
maximisation in fact is implemented by inequalities forcing at least some number
to be true.

In \cref{tab:hr-qcp} we compare three different resulting programs on QCP-max
problems: full reification of the model above, using the
\mzninline{all_different} decomposition defined by the predicate shown
(\textsf{full}), half reification of the model using the
\mzninline{all_different} decomposition (\textsf{half}), and half reification
using a half-reified global \mzninline{all_different} (\textsf{half-g})
implementing arc consistency (thus having the same propagation strength as the
decomposition). \jip{is this still correct??} We use standard QCP examples from
the literature, and group them by size.
% and whether they are satisfiable or unsatisfiable as QCP problems.
We compare both a standard finite domain solver (FD) and a learning lazy clause
generation solver (FD + Explanations). We use the same fixed search strategy of
labeling the matrix in order left-to-right from highest to lowest value for all
approaches to minimize differences in search.

\begin{table} [tb] \begin{center}
\caption{\label{tab:hr-qcp} QCP-max problems:
Average time (in seconds), number of solved instances (300s timeout).}
\begin{tabular}{|l||rr|rr|rr|}
\hline
Instances & \multicolumn{2}{c|}{\textsf{half-g}} & \multicolumn{2}{c|}{\textsf{half}} & \multicolumn{2}{c|}{\textsf{full}} \\
\hline
\texttt{qcp-10} (x15) & 17.12 & 15 & 21.17 & 14 & 21.09 & 14 \\
\hline
\texttt{qcp-15} (x15) & 40.35 & 13 & 40.52 & 13 & 40.55 & 13 \\
\hline
\texttt{qcp-20} (x15) & 27.50 & 14 & 64.05 & 14 & 65.55 & 14 \\
\hline
\texttt{qcp-25} (x15) & 195.85 & 6 & 223.44 & 6 & 225.22 & 6 \\
\hline
\end{tabular}
\end{center}
\end{table}

\jip{adjust text to match new table}Half reification of the decomposition is
more efficient, principally because it introduces fewer Boolean variables, and
the direct implementation of the half reified constraint is more efficient
still. Note that learning can be drastically changed by the differences in the
model and \textsf{full} solves one more instance in \texttt{qcp-20}, thus
winning in that case. Apart from this instance, the half reified versions give
an almost uniform improvement.

The second experiment shows how half reification can reduce the overhead of
handling partial functions correctly. Consider the following model for
determining a prize collecting path, a simplified form of prize collecting
travelling salesman problem
\autocite{balas-1989-pctsp}, %shown in \cref{fig:hr-pct}
where the aim is define an acyclic path from node 1 along weighted edges to
collect the most weight. Not every node needs to be visited (\(pos[i] = 0\)).

\begin{mzn}
int: n; % size
array[1..n,0..n] of int: p; % prize for edge (i,j), p[i,0] = 0

array[1..n] of var 0..n: next; % next posn in tour
array[1..n] of var 0..n: pos;  % posn on node i in path, 0=notin
array[1..n] of var int: prize = [p[i,next[i]] | i in 1..n];
                               % prize for outgoing edge

constraint forall(i in 1..n)(
    (pos[i] = 0 <-> next[i] = 0) /\
    (next[i] > 1 -> pos[next[i]] = pos[i] + 1));

include "alldifferent_except_0.mzn";
constraint alldifferent_except_0(next) /\ pos[1] = 1;

solve minimize sum(i in 1..n)(prize[i]);
\end{mzn}

It uses the global constraint \mzninline{alldifferent_except_0} which constrains
each element in the \mzninline{next} array to be different or equal 0. The model
has one unsafe array lookup \mzninline{pos[next[i]]}. We compare using full
reification (\textsf{full}) and half reification (\textsf{half}) to model this
problem. Note that if we extend the \(pos\) array to have domain \(0..n\) then the
model becomes safe, by replacing its definition with the following two lines

\begin{mzn}
  array[0..n] of var 0..n: pos; % posn on node i in path, 0=notin
  constraint pos[0] = 0;
\end{mzn}

We also compare against this model (\textsf{extended}).

We use graphs with both positive and negative weights for the tests. The search
strategy fixes the \mzninline{next} variables in order of their maximum value.
First we note that \textsf{extended} is slightly better than \textsf{full}
because of the simpler translation, while \textsf{half} is substantially better
than \textsf{extended} since most of the half reified \texttt{element}
constraints become redundant. Learning increases the advantage because the half
reified formulation focuses on propagation which leads to failure which creates
more reusable nogoods.

\begin{table} [tb] \begin{center}
    \caption{\label{tab:hr-pctsp} Prize collecting paths: Average time (in seconds)
      and number of solved instances with a 300s timeout for various number of
      nodes.}
\begin{tabular}{|l||rr|rr|rr||rr|rr|rr|}
\hline
 & \multicolumn{6}{|c||}{FD} & \multicolumn{6}{|c|}{FD + Explanations} \\
Nodes  &
  \multicolumn{2}{|c|}{\textsf{full}} & \multicolumn{2}{|c|}{\textsf{half}} &
  \multicolumn{2}{|c|}{\textsf{extended}}& \multicolumn{2}{|c|}{\textsf{full}} &
  \multicolumn{2}{|c|}{\textsf{half}} & \multicolumn{2}{|c|}{\textsf{extended}}
  \\
\hline
15-3-5 (x 10) & 0.31&10& 0.25&10& 0.26&10 & 0.21&10 & 0.17&10 & 0.17&10 \\
\hline
18-3-6 (x 10) & 1.79&10& 1.37&10& 1.52&10 & 0.70&10 & 0.51&10 & 0.58&10 \\
\hline
20-4-5 (x 10) & 5.30&10& 4.04&10& 4.51&10 & 1.28&10 & 0.97&10 & 1.17&10 \\
\hline
24-4-6 (x 10) & 46.03&10& 34.00&10& 40.06&10 & 7.28&10 & 4.91&10 & 6.37&10 \\
\hline
25-5-5 (x 10) & 66.41&10& 50.70&10& 57.51&10 & 9.75&10 & 6.58&10 & 8.28&10 \\
\hline
28-4-7 (x 10) & 255.06&5& 214.24&8& 241.10&6 & 38.54&10 & 23.27&10 & 34.83&10 \\
\hline
30-5-6 (x 10) & 286.48&1& 281.00&2& 284.34&1 & 100.54&10 & 60.65&10 & 92.19&10\\
\hline
32-4-8 (x 10) & 300.00&0& 297.12&1& 300.00&0 & 229.86&5 & 163.73&10 & 215.16&8\\
\hline

%15-3-5 (x 10) & 0.31&10& 0.31&10& 0.26&10 & 0.21&10 & 0.19&10 & 0.17&10 \\
%\hline
%18-3-6 (x 10) & 1.79&10& 1.77&10& 1.52&10 & 0.70&10 & 0.57&10 & 0.58&10 \\
%\hline
%20-4-5 (x 10) & 5.30&10& 5.31&10& 4.51&10 & 1.28&10 & 1.13&10 & 1.17&10 \\
%\hline
%24-4-6 (x 10) & 46.03&10& 47.43&10& 40.06&10 & 7.28&10 & 6.00&10 & 6.37&10 \\
%\hline
%25-5-5 (x 10) & 66.41&10& 70.03&10& 57.51&10 & 9.75&10 & 8.57&10 & 8.28&10 \\
%\hline
%28-4-7 (x 10) & 255.06&5& 260.79&5& 241.10&6 & 38.54&10 & 28.05&10 & 34.83&10 \\
%\hline
%30-5-6 (x 10) & 286.48 &0& 287.33 &0& 284.34 &0 & 100.54&10 & 83.50&10 & 92.19&10 \\
%\hline
%32-4-8 (x 10) & 300.00 &0& 300.00 &0& 300.00 &0 & 229.86&5 & 187.40&9 & 215.16&8 \\
%\hline
\end{tabular}
\end{center}
\end{table}

In the final experiment we compare resource constrained project scheduling
problems (RCPSP) where the \texttt{cumulative} constraint is defined by the task
decomposition as in \cref{ex:hr-cumul} above, using both full reification and
half-reification. We use standard benchmark examples from PSPlib
\autocite{kolisch-1997-psplib}. \Cref{tab:hr-rcpsp} compares RCPSP instances
using \textsf{full} reification and \textsf{half} reification. We compare using
J30 instances (\textsf{J30} ) and instances due to Baptiste and Le Pape
(\textsf{BL}). Each line in the table shows the average run time and number of
solved instances. The search strategy tries to schedule the task with the
earliest possible start time. We find a small and uniform speedup for
\textsf{half} over \textsf{full} across the suites, which improves with
learning, again because learning is not confused by propagations that do not
lead to failure.

\begin{table} [tb] \caption{\label{tab:hr-rcpsp} RCPSP:
Average time (in seconds) and number of solved instances with a 300s timeout.}
\begin{center}
\begin{tabular}{|l||rr|rr||rr|rr|}
\hline
 & \multicolumn{4}{|c||}{FD} & \multicolumn{4}{|c|}{FD + Explanations} \\
  Instances &
  \multicolumn{2}{|c|}{\textsf{full}} & \multicolumn{2}{|c|}{\textsf{half}}
  & \multicolumn{2}{|c|}{\textsf{full}} & \multicolumn{2}{|c|}{\textsf{half}}\\
\hline
BL (x 40) & 277.2 & 5 & 269.3 & 5 & 17.1 & 39 & 15.4 & 39\\
\hline
J30 (x 480) & 116.1 & 300 & 114.3 & 304 & 16.9 & 463 & 12.9 & 468\\
\hline
\end{tabular}
\end{center}
\end{table}

\subsection{MiniZinc Challenge}

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{Related Work and Conclusion}\label{sec:hr-conclusion}
%=============================================================================%

Half reification on purely Boolean constraints is well understood, this is the
same as detecting the \emph{polarity} of a gate, and removing half of the
clausal representation of the circuit (see \eg\
\autocite{plaisted-1986-polarity}). The flattening of functions (partial or
total) and the calculation of polarity for Booleans terms inside
\texttt{bool2int} do not arise in pure Boolean constraints.

Half reified constraints have been used in constraint modelling but are
typically not visible as primitive constraints to users, or produced through
flattening. Indexicals \autocite{van-hentenryck-1992-indexicals} can be used to
implement reified constraints by specifying how to propagate a constraint,
propagate its negation, check disentailment, and check entailment, and this is
implemented in SICstus Prolog \autocite{carlsson-1997-sicstus}. A half reified
propagator simply omits entailment and propagating the negation.

Half reified constraints appear in some constraint systems, for example SCIP
\autocite{gamrath-2020-scip} supports half-reified real linear constraints of
the form \mzninline{b -> sum(i in N)(a[i] * x[i]) <= C} exactly because the
negation of the linear constraint \mzninline{sum(i in N)(a[i] * x[i]) > C} is
not representable in an LP solver so full reification is not possible.

While flattening is the standard approach to handle complex formula involving
constraints, there are a number of other approaches which propagate more
strongly. Schulte proposes a generic implementation of \mzninline{b <-> c}
propagating (the flattened form of) \mzninline{c} in a separate constraint space
which does not affect the original variables \autocite*{schulte-2000-deep};
entailment and disentailment of \mzninline{c} fix the \mzninline{b} variable
appropriately, although when \mzninline{b} is made \mzninline{false} the
implementation does not propagate \mzninline{not c}. This can also be
implemented using propagator groups \autocite{lagerkvist-2009-groups}. Brand and
Yap define an approach to propagating complex constraint formulae called
controlled propagation which ensures that propagators that cannot affect the
satisfiability are not propagated \autocite*{brand-2006-propagation}. They note
that for a formula without negation, they could omit half their control rules,
corresponding to the case for half reification of a positive context. Jefferson
et al.\ similarly define an approach to propagating positive constraint formulae
by using watch literal technology to only wake propagators for reified
constraints within the formula when they can affect the final result
\autocite*{jefferson-2010-connectives}. They use half reified propagators, which
they call the ``reifyimplied'' form of a constraint, in some of their constraint
models, though they do not compare half reified models against full reified
models. We can straightforwardly fit these stronger propagation approaches to
parts of a constraint formula into the flattening approach by treating the whole
formula as a predicate, and the implementation of the stronger propagation as
its propagator.

A passing contribution of this paper is a much simpler approach to enforcing the
relational semantics, by combining the ``safening'' of expressions with
flattening. The original approach of \autocite{frisch-2009-undefinedness} is a
source to source transformation without flattening and substantially more
complex.

We suggest that all finite domain constraint solvers should move to supporting
half-reified versions of all constraints. This imposes no further burden on
solver implementors, it allows more models to be solved, it can be used to
implement full reification, and it can allow translation to more efficient
models.