%************************************************
\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: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 $i \leq 4$ then the value in the $i^{th}$ position of
  array $a$ multiplied by $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 $b1$ and $b2$.
  The term structure is encoded by ``flattening'' the terms and converting the
  functions to relations, introducing the new integer variables $t1$ and $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 $a$ has index set 1..5, but $i$ takes the value 7. The
  constraint $\element(i,a,t1)$ will fail and no solution will be found.
  Intuitively if $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 $\bot$, and this $\bot$ function percolates up through every
expression to the top level conjunction, making the model unsatisfiable. For the
example $(t1\equiv)~ a[7] = \bot$, $(t2\equiv)~ \bot \times x = \bot$,
$(b2\equiv)~ \bot \geq 6 = \bot$, $(b1\equiv)~ 7 \leq 4 = \false$,
$\false \rightarrow \bot = \bot$. This is known as the \emph{strict} semantics
\autocite{frisch-2009-undefinedness} for modeling 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 $\bot$ percolates up through the term until it
reaches a Boolean subterm where it becomes $\false$. For the example
$(t1\equiv)~ a[7] = \bot$, $(t2\equiv)~ \bot \times x = \bot$,
$(b2\equiv)~ \bot \geq 6 = \false$, $(b1\equiv)~ 7 \leq 4 = \false$,
$\false \rightarrow \false = \true$. 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 $i$ takes values in the set
  1..8, and $a$ has an index set 1..5, its translation of the constraint in
  Example~\ref{ex: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 $\element$ to be
  ``safe'' since $t3$ is constrained to only take values in the index set of $a$.
  The reified constraints defining $b3$ force $t3$ to equal $i$ iff $i$ takes a
  value in the index set of $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: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 \alldiff, they do not define
    this form.}
\end{example}

Reified global constraints are not implemented because a reified constraint
$b \full c$ must also implement a propagator for $\neg c$ (in the case that
$b = \false$). While for some global constraints, e.g. \alldiff{}, 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 $b_1 \full i \leq 4$ will wake up whenever the upper bound of
$i$ changes in order to check whether it should set $b_1$ to $true$. But setting
$b_1$ to $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 linearize 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 $b1 \full i \leq 4$, where $i$ can take values in the domain $0..10$
  then its linearization 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 $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 linearization, which always allows that
  $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 $c$ then they can straightforwardly
        construct a half reified propagator for $b \half c$.
  \item Half reified constraints $b \half c$ 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.

\jip{Add a variation of this: Adding support for half reification to the linear
  library is more interesting and seems very worthwhile. Since the solvers using
  the linear library only support linear constraints, full reification is
  generally implemented using using the equivalence of two implications; for
  example, the full reification \(b \full x \le y \) is implemented by the
  linearisation of \((b \half x \le y) \land (\lnot b \half x > y)\). The half
  reification of the same constraint consist only of the first half of the
  conjunction.}

\section{Propagation Based Constraint Solving}

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 \emph{domain} $D$ is a complete mapping from $\VV$ to finite sets of integers
(for the variables in $\VV_I$) and to subsets of $\{\true,\false\}$ (for the
variables in $\VV_b$).
%
We can understand a 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 $\false < \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}

\newcommand{\nonterm}[1]{\textsc{#1}}

\newcommand{\cons}{\nonterm{cons}}
\newcommand{\intc}{\nonterm{int}}
\newcommand{\bvar}{\nonterm{bvar}}
\newcommand{\ivar}{\nonterm{ivar}}
\newcommand{\term}{\nonterm{term}}
\newcommand{\cname}{\nonterm{pred}}
\newcommand{\relop}{\nonterm{relop}}
\newcommand{\aop}{\nonterm{arithop}}
\newcommand{\arrayc}{\nonterm{array}}
\newcommand{\arrow}{$\longrightarrow$}
\newcommand{\vb}{$|$}

\label{sec:syntax}

%\newcommand{\cons}{\textsf{cons}}
%\newcommand{\intc}{\textsf{int}}
%\newcommand{\bvar}{\textsf{bvar}}
%\newcommand{\ivar}{\textsf{ivar}}
\newcommand{\aivar}{\nonterm{aivar}}
\newcommand{\abvar}{\nonterm{abvar}}
\newcommand{\avar}{\nonterm{avar}}
%\newcommand{\term}{\textsf{term}}
%\newcommand{\cname}{\textsf{pred}}
\newcommand{\fname}{\nonterm{func}}
%\newcommand{\relop}{\textsf{relop}}
%\newcommand{\aop}{\textsf{arithop}}
\newcommand{\arrayi}{\nonterm{iarray}}
\newcommand{\arrayb}{\nonterm{barray}}
\newcommand{\decli}{\nonterm{idecl}}
\newcommand{\declb}{\nonterm{bdecl}}
\newcommand{\decls}{\nonterm{decls}}
\newcommand{\argo}{\nonterm{arg}}
\newcommand{\args}{\nonterm{args}}
\newcommand{\itm}{\nonterm{item}}
\newcommand{\itms}{\nonterm{items}}
\newcommand{\model}{\nonterm{model}}
\newcommand{\solve}{\nonterm{solve}}
\newcommand{\optcons}{\nonterm{ocons}}
%\newcommand{\arrow}{$\rightarrow$}
%\newcommand{\vb}{$|$}
\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 \cons{} nonterminal defines constraints (Boolean terms), \term{} defines
integer terms, \arrayb{} defines Boolean arrays, and \arrayi{} defines integer
arrays:

\vspace{2mm}
\noindent
\begin{tabular}{rcl}
\cons{} & \arrow & \texttt{true} \vb{} \texttt{false} \vb{} \bvar{} \vb{} \term{} \relop{} \term{} \\
      & \arrow & \texttt{not} \cons{} \vb{} \cons{} \verb+/\+ \cons{} \vb{}
      \cons{} \verb+\/+ \cons{} \vb{}  \cons{} \verb+->+ \cons{}  \vb{}
      \cons{} \verb+<->+ \cons{} \\
      & \arrow & \texttt{forall(} \arrayb{} \texttt{)} \vb{}
      \texttt{exists(} \arrayb{} \texttt{)}
      \vb{}  \arrayb[\term{}]   \\
      & \arrow &
         \cname \texttt{(}\term{}, \ldots, \term{} \texttt{)} \vb{}  \texttt{if} \cons{} \texttt{then} \cons{} \texttt{else}
      \cons{} \texttt{endif} \\
      & \arrow & \texttt{let \{} \decls{} \optcons{} \texttt{\} in} \cons{} \\
\term{} & \arrow & \intc{} \vb{} \ivar{} \vb{} \term{} \aop{} \term{} \vb{}
\arrayi[\term{}] \vb{} \texttt{sum(} \arrayi \texttt{)}
\\
& \arrow & \texttt{if} \cons{} \texttt{then} \term{} \texttt{else}
      \term{} \texttt{endif} \vb{}
\texttt{bool2int(} \cons{} \texttt{)} \\
      & \arrow & \texttt{let \{} \decls{} \optcons{} \texttt{\} in} \term{} \\
\arrayb{} & \arrow & \verb+[+ \cons{}, \ldots, \cons{}
\verb+]+ \vb{} \verb+[+ \cons{} \verb+|+ \ivar{} \texttt{in} \term{} \texttt{..}
\term{} \verb+]+ \\
\arrayi{} & \arrow & \verb+[+ \term{}, \ldots, \term{} \verb+]+ \vb{}
 \verb+[+ \term{} \verb+|+ \ivar{} \texttt{in} \term{} \texttt{..}
\term{} \verb+]+ \\
\end{tabular}

\vspace{2mm}
The grammar uses the symbols
\bvar{} for Boolean variables,
\relop{} for relational operators
$\{$ \texttt{==}, \texttt{<=}, \texttt{<},
\texttt{!=}, \texttt{>=}, \texttt{>} $\}$,
\cname{} for names of predicates,
\intc{} for integer constants,
\ivar{} for integer variables, and
\aop{} for arithmetic operators
$\{$ \texttt{+}, \texttt{-}, \texttt{*}, \texttt{div} $\}$.

In the \texttt{let} constructs we make use of the nonterminal
\decls{} for declarations. We define this below using
\decli{} for integer variable declarations,
\declb{} for Boolean variable declarations.
We use \optcons{} for optional constraint items appearing in let declarations.
We also define  \args{} as a list of integer variable declarations,
an item \itm{} as either a predicate declaration,
a constraint or a function declaraions,
\itms{} as a list of items,
\solve{} as a solve directive either satisfaction or an objective,
and a model \model{} as
some declarations followed by items followed by a solve item.
Note that $\epsilon$ represents the empty string.

\vspace{2mm}
\noindent
\begin{tabular}{rcl}
\decli{} & \arrow & \texttt{int:} \ivar{}
\vb{} \texttt{var int:} \ivar{}
 \vb{}
%  \term{} \texttt{..} \term{} \texttt{:} \ivar \vb{}
\texttt{var} \term{} \texttt{..} \term{} \texttt{:} \ivar{}  \\
\declb{} & \arrow & \texttt{bool:} \bvar{}  \vb{} \texttt{var bool:} \bvar{} \\
\decls{} & \arrow &  $\epsilon$ \vb{} \decli{}\texttt{;} \decls{} \vb{} \decli{}
\texttt{=} \term{}\texttt{;} \decls{} \vb{}
\declb{}\texttt{;} \decls{} \vb{} \declb{} \texttt{=} \cons{}\texttt{;}
\decls{} \\
\optcons{} & \arrow & $\epsilon$ \vb{} \texttt{constraint} \cons{} \texttt{;}
\optcons{} \\
\args{} & \arrow & \texttt{var} \texttt{int:} \ivar{} \vb{}
\texttt{var} \texttt{int:} \ivar{}
 \texttt{,} \args{} \vb{} \texttt{int:} \ivar{} \vb{}
\texttt{int:} \ivar{}
 \texttt{,} \args{} \\
\itm{} & \arrow & \texttt{predicate} \cname \texttt{(} \args \texttt{)}  =
\cons{}\texttt{;} \vb{} \texttt{constraint} \cons{}\texttt{;} \vb{} \\
 & \arrow & \texttt{function} \texttt{var int :} \fname \texttt{(} \args{} \texttt{)}  =
\term{} \texttt{;}  \\ %\vb{} ~\\
%\args{} & \arrow & \decli{} \vb{} \decli{} \texttt{,} \args{} \\
\itms{} & \arrow & $\epsilon$ \vb{} \itm{} \itms{} \\
\solve{} & \arrow & \texttt{satisfy} \texttt{;} \vb{} \texttt{minimize}
\term{} \texttt{;} \vb{}
\texttt{maximize} \term \texttt{;} \\
\model{} & \arrow & \decls{} \itms{} \texttt{solve} \solve{} \\
\end{tabular}
\vspace{2mm}


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 \cons{} term defining the constraints of the model we can split its
\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/\false}$, that is $c$ with subterm $t$ replaced by $\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/\true}$; and a \emph{negative context} iff for any solution
$\theta$ of $c$ then $\theta$ is also a solution of $c\subs{t/\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 $x > 0$ is in the root context, $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.


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[\true]$, that is $c$ with subterm $t$
% replaced by $\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[\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: \texttt{div} returns $\bot$
if the divisor is zero, while $a[i]$ returns $\bot$ if the value of $i$ is
outside the domain of $a$. We can categorize the \emph{safe} terms and
constraints of the language, as those where no $\bot$ 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
$t_1 ~\texttt{div}~ t_2$ and the set of possible values of $t_2$ does not
include 0, $0 \not\in poss(t_2)$; or it is an array access term $a[t]$ and the
set of possible values of $t$ are included in the domain of $a$,
$poss(t) \subseteq \dom(a)$.

\section{Flattening with Full Reification}
\label{sec: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 $e$ is replaced by a new variable $obj$ and a constraint item
$\texttt{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 \texttt{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 $b$ made equivalent to $\true$ by
the constraints in $S$. For succinctness we use the notation $\new b$ ($\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
$\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.


\newcommand{\callbyvalue}[1]{#1}
\newcommand{\callbyunroll}[1]{}

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 \verb+/\+ or \verb+\/+
which is then flattened. A Boolean array lookup flattens its arguments, and
creates an $\mathit{element}$ constraint. If the context is root this is simple,
otherwise it creates a new index varaible $v'$ guaranteed to only give correct
answers, and uses this in the $\mathit{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. \callbyvalue{ User defined predicate applications flatten
  their arguments and then flatten a renamed copy of the body.} \callbyunroll{
  User defined predicate applications are replaced by a renamed and flattened
  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 resdtriction, but explain its not all required} The handling
of \texttt{let} is the most complicated. The expression is renamed with new
copies of the let variables. We extract the constraints from the \texttt{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 $\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 \bot$) \\
\>\> \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$ := $\true$;\\
%\> \> \textbf{case} \texttt{false}: $b$ := $\false$;\\
\> \> \textbf{case} $b'$ (\bvar): $b$ := $b'$; \\
\> \> \textbf{case} $t_1$ $r$ $t_2$ (\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],
\true)\}$; $b$ := $\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,..,n\} \} $
\\
\callbyvalue{
\>\> \textbf{case} $p$ ($t_1, \ldots, t_n$) (\cname) 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$ := $\true$; $S$ \cupp  $\{ p(v_1, \ldots, v_n) %, \bigwedge_{j=1}^n b_j
\}$
\\
\>\> \textbf{case} $p$ ($t_1, \ldots, t_n$) (\cname): 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\}$
\\
}
\callbyunroll{
\>\> \textbf{case} $p$ ($t_1, \ldots, t_n$) (\cname) built-in predicate: \\
\> \> \> \textbf{if} ($\ctxt \neq \rootc$) \textbf{abort} \\
\> \> \> \textbf{foreach}($j \in 1..n$) $\tuple{v_j, \_}$ := $\flatt(t_j,\rootc)$; \\
\>\> \> $b$ := $\true$; $S$ \cupp  $\{ p(v_1, \ldots, v_n)\}$
\\
\>\> \textbf{case} $p$ ($t_1, \ldots, t_n$) (\cname): user-defined predicate \\
\>\> \> \textbf{let} $p(x_1, \ldots, x_n) = c_0$ be defn of $p$ \\
\>\> \> $b$ := $\flatc(c_0\subs{x_1/t_1, \ldots, x_n/t_n},\ctxt)$
\\
}
\> \> \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 \texttt{let} is implemented by
\textsf{flatlet}$(d,c,t,\ctxt)$ which takes the declarations $d$ inside the
\texttt{let}, the constraint $c$ or term $t$ of the scope of the \texttt{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 \texttt{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 $\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 $\texttt{element}$
constraint with a new index variable $v'$ which is guaranteed to be in the
domain of the array ($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 tham for simplicity!} \callbyvalue{ 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}. } \callbyunroll{ Partial functions are simply
  handled by replacing the function application by the renamed body of the
  function. Total functions are more interesting. Each of the arguments is
  flattened, the function body is renamed to use the variables representing the
  arguments, and then the body is flattened \emph{in the root context}. The
  Boolean $b$ created simply represents whether all the arguments were defined,
  since the function itself is total. } 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 \bot$) \\
\>\> \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$ := $\true$ \\
\> \textbf{else} %\\
%% \> \> \textbf{if} ($t$ is marked \emph{total}) $\ctxt$ := $\rootc$ \\
%\> \>
\textbf{switch} $t$ \\
%\> \> \textbf{case} $i$ (\intc): $v$ := $i$; $b$ := $\true$ \\
\> \> \textbf{case} $v'$ (\ivar):  $v$ := $v'$; $b$ := $\true$\\
\> \> \textbf{case} $t_1$ $a$ $t_2$ (\aop): \\
\> \> \>
$\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,..,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 \}$  \\
\callbyvalue{
\>\> \textbf{case} $f$ ($t_1, \ldots, t_n$) (\fname): 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 \}$
\\
}
\callbyunroll{
\>\> \textbf{case} $f$ ($t_1, \ldots, t_n$) (\fname): partial function \\
\>\> \> \textbf{let} $f(x_1, \ldots, x_n) = t_0$ be defn of $f$ \\
\>\> \> $\tuple{v,b}$ := $\flatt(t_0\subs{x_1/t_1, \ldots, x_n/t_n},\ctxt)$
\\
\>\> \textbf{case} $f$ ($t_1, \ldots, t_n$) (\fname): declared total 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'$ be defn of $f$ \\
\>\> \> $\tuple{v,\_}$ := $\flatt(t'\subs{x_1/v_1, \ldots, x_n/v_n},\rootc)$ \\
\> \> \> $S$ \cupp $\{ \new b \full \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: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 in Figure~\ref{fig:tree}.
  \begin{figure}[t]
    $$
    \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 && \\
    }
    $$
    \caption{An expression to be flattened with non-leaf (sub-)terms
      numbered.\label{fig:tree}}
  \end{figure}
  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(\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'$ (\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 \true$)  \textbf{return} $\flatc(\true, c_1) \cup
%            \flatc(\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$) (\cname): \\
% \> \> \textbf{if} ($b \equiv \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'$ (\ivar): \textbf{return} $\{ v = v' \}$ \\
% \> \textbf{case} $t_1$ $a$ $t_2$ (\aop):
% \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 \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
$\bot$ value. For $\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 = \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 \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 \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',
\element(v',a,x)\}$ \\
\> \> \> \%HALF\% $S$ := $S \cup \{ b' \full v \in \dom(a), b' \half
\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:halfreif}

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

We can construct a propagator $f_{b \half c}$ for the half-reified version of
$c$, $b \half c$, using the propagator $f_c$ for $c$.
$$
\begin{array}{rcll}
f_{b \half c}(D)(b) & = &  \{ \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~} \false \in D(b) \\
f_{b \half c}(D)(v) & = & f_c(D)(v) & \text{if~} v \in vars(c)
\text{~and~} \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) = \{\true\}$, when it
% needs to perform both.

In practice most propagator implementations for $c$ first check whether $c$ is
satisfiable, before continuing to propagate. For example,
$\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; Regin's domain propagator 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; 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_{b \half c}$ by only
performing the checking part until $D(b) = \{\true\}$.

Half reification naturally encodes the relational semantics for partial function
applications in positive contexts. We associate a Boolean variable $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: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, $i > 4$ and
  $a[i] \times x \geq 6$, which we name $b_0$, $b_1$ and $b_2$ 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 $\element$ constraint is half reified with the name of its nearest
  enclosing Boolean term. Note that if $i = 7$ then the second constraint makes
  $b2 = \false$. Given this, the final constraint requires $b1 = \true$, which
  in turn requires $i > 4$. Since this holds, the whole constraint is $\true$
  with no restrictions on $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: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 \alldiff 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: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 $s[j]$ of task $j$, the sum of resources
  $r$ used by it and by other tasks executing at the same time is less than the
  limit $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 $i$ is constrained so that it does not overlap
  time $s[j]$, then $b3[i]$ is fixed to $\false$ and $a[i]$ to 0, and the long
  linear sum is awoken. But this is useless, since it cannot cause failure.

  % Half-reification of this expression which appears in a negative context produces
  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
  $b4[i]$), but since both $b4[i]$ and $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 $i$ is
  guaranteed to overlap time $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 $\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,c)$ defined below returns a set of constraints
implementing the half-reification $b \half c$. We flatten a constraint item
$\texttt{constraint}~ c$ using $\halfc(\true, c)$. The half-reification
flattening transformation uses half reification whenever it is in a positive
context. If it encounters a constraint $c_1$ 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 $t_1 < t_2$
yields $t_1 \geq t_2$, and negating $c_1$ \verb+/\+ $c_2$ yields
$\texttt{not}~ c_1$ \verb+\/+ \texttt{not}~ $c_2$. 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
\texttt{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 \bot$) \\
\>\> \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$ := $\true$;\\
%\> \> \textbf{case} \texttt{false}: $b$ := $\false$;\\
\> \> \textbf{case} $b'$ (\bvar): $b$ := $b'$; \\
\> \> \textbf{case} $t_1$ $r$ $t_2$ (\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], \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\} \} $
%\\
\callbyvalue{
\>\> \textbf{case} $p$ ($t_1, \ldots, t_n$) (\cname) built-in predicate: \\
\> \> \> \textbf{foreach}($j \in 1..n$) $\tuple{v_j, b_j}$ :=
$\halft(t_j,\ctxt,\iboth)$; \\
\> \> \> \textbf{if} ($\ctxt = \rootc$)
$b$ := $\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$) (\cname): 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\}$
\\
}
\callbyunroll{
\>\> \textbf{case} $p$ ($t_1, \ldots, t_n$) (\cname) built-in predicate: \\
\> \> \> \textbf{if} ($\ctxt \neq \rootc$) \textbf{abort} \\
\> \> \> \textbf{foreach}($j \in 1..n$) $\tuple{v_j, \_}$ := $\flatt(t_j,\rootc)$; \\
\>\> \> $b$ := $\true$; $S$ \cupp  $\{ p(v_1, \ldots, v_n)\}$
\\
\>\> \textbf{case} $p$ ($t_1, \ldots, t_n$) (\cname): user-defined predicate \\
\>\> \> \textbf{let} $p(x_1, \ldots, x_n) = c_0$ be defn of $p$ \\
\>\> \> $b$ := $\flatc(c_0\subs{x_1/t_1, \ldots, x_n/t_n},\ctxt)$
\\
}
\> \> \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 riefies $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 refication. 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 \bot$) \\
\>\> \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$ := $\true$;\\
%\> \> \textbf{case} \texttt{false}: $b$ := $\false$;\\
\> \> \textbf{case} $b'$ (\bvar): $S$ \cupp $\{\new b \half \neg b'\}$; \\
\> \> \textbf{case} $t_1$ $r$ $t_2$ (\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)$ \\
\callbyvalue{
\>\> \textbf{case} $p$ ($t_1, \ldots, t_n$) (\cname) built-in predicate: \\
\> \> \> $b$ := $\flatc(\texttt{not}~p(t_1, \ldots, t_n), \ctxt)$ \\
\>\> \textbf{case} $p$ ($t_1, \ldots, t_n$) (\cname): 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
\texttt{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 \texttt{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 $\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
\texttt{element} constraint. Array sums and if-then-else-endif are
straightforward.

The treatment of \texttt{bool2int} is the reason for the complex bounds
analysis. If we are only interested in the lower bound of $\texttt{bool2int}(c)$
we can half reify $c$ since it is in a positive context. If we are only
interested in the upper bound of $\texttt{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 \bot$) \\
\>\> \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$ := $\true$ \\
\> \textbf{else} %\\
%% \> \> \textbf{if} ($t$ is marked \emph{total}) $\ctxt$ := $\rootc$ \\
%\> \>
\textbf{switch} $t$ \\
%\> \> \textbf{case} $i$ (\intc): $v$ := $i$; $b$ := $\true$ \\
\> \> \textbf{case} $v'$ (\ivar):  $v$ := $v'$; $b$ := $\true$\\
\> \> \textbf{case} $t_1$ $a$ $t_2$ (\aop): \\
\> \> \> \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 \}$  \\
\callbyvalue{
\>\> \textbf{case} $f$ ($t_1, \ldots, t_n$) (\fname): 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:half}
  Now lets consider half reifying the expression of \cref{ex: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
Example~\ref{ex: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 modeling $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 ( \{ \false \} \cup f_{b \full c}(D)(b)) \\
f_{b \half c}(D)(v) & = & D(v) & \texttt{if}~ v \in vars(c),~\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}~  \{ \false \} \in f_{b \full c}(D)(b) \\
f_{b' \half \neg c}(D)(b') & = & D(b') \cap \{ \false\} &  \text{otherwise}\\
f_{b' \half \neg c}(D)(v) & = & D(v) & \texttt{if}~ v \in vars(c),~\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 \{ \false, \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) = \{\true,\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 \{ \false, \true \}$. \textbf{(a-ii)} Suppose
%   $f_{b \full c}(D)(b) = \{ \true \}$. Let $D_1 = f_{b' \half \neg c}(D)$, then
%   $D_1(b') = \{ \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)= \{ \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) = \{ \false \}$. Let $D_1 = f_{b \half c}(D)$, then
%   $D_1(b) = \{ \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')= \{ \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) = \{\true\}$ then clearly $f_{b \full c}$ and
%   $f_{b \half c}$ act identically on variables in $vars(c)$.

%   \textbf{(c)} If $D(b) = \{\false\}$ then $D(b') = \{\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 \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: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, \(b \full c\). These generally
consist of two parts which are equivalent to the implications
\(b \half c \land \lnot b \half \lnot 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 Example \ref{ex:half}, flattening with half reification will in many
cases result in implication chains: \((b \half b') \land (b' \half c)\), where
\(b'\) has no other occurrences. In this case the conjunction can be replaced by
\(b \half c\) and \(b'\) can be removed from the model. The case shown in the
example can be generalized to
\((b \half b') \land \left(\forall_{i \in N} b' \half c_i \right)\), which, if
\(b'\) has no other usage in the instance, can be resolved to
\(\forall_{i \in N} b \half c_i\) after which \(b'\) 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
\(x \half 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: \(b' \half \forall_{i \in N} b_i\)
is equivalent to \(\forall_{i \in N} (b' \half b_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 conjuction 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 \alldiff 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 \alldiff constraints, while
apparently in a mixed context, are actually in a positive context, since the
maximization in fact is implemented by inequalities forcing at least some number
to be true.

In Table~\ref{tab:qcp} we compare three different resulting programs on QCP-max
problems: full reification of the model above, using the \alldiff decomposition
defined by the predicate shown (\textsf{full}), half reification of the model
using the \alldiff decomposition (\textsf{half}), and half reification using a
half-reified global \alldiff (\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: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 Figure~\ref{fig: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 \texttt{alldifferent\_except\_0} which constrains
each element in the $next$ array to be different or equal 0. The model has one
unsafe array lookup $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 $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 focusses on propagation which leads to failure which creates more
reusable nogoods.

\begin{table} [tb] \begin{center}
\caption{\label{tab: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:cumul} above, using both full reification and
half-reification. We use standard benchmark examples from PSPlib
\autocite{kolisch-1997-psplib}. \Cref{tab: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: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 2012 until 2017.
Note that the instances that the instances without any reifications have been
excluded from the experiment as they would not experience any change. 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: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 table \ref{tab:flat_results} and update with current
results}

Table \ref{tab: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 compressions 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{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 modeling 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
$c$, %($prop(c)$),
propagate its negation,
%$prop(\neg c)$,
check disentailment, % $check(c)$,
and check entailment, %$check(\neg c)$,
and this is implemented in SICstus Prolog \autocite{carlsson-1997-sicstus}. A
half reified propagator simply omits entailment and propagating the negation.
% $prop(\neg c)$ and $check(\neg c)$. Half reification was briefly discussed in
% our earlier work \autocite{cp2009d}, in terms of its ability to reduce
% propagation.
Half reified constraints appear in some constraint systems, for example SCIP
\autocite{gamrath-2020-scip} supports half-reified real linear constraints of
the form $b \half \sum_i a_i x_i \leq a_0$ exactly because the negation of the
linear constraint $\sum_i a_i x_i > a_0$ 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 $b \full c$ propagating
(the flattened form of) $c$ in a separate constraint space which does not affect
the original variables \autocite*{schulte-2000-deep}; entailment and
disentailment of $c$ fix the $b$ variable appropriately, although when $b$ is
made $\false$ the implementation does not propagate $\neg 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.
