From 46ab4b39e492d426cd1d835c91ef0e7e3a85bc7f Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Thu, 11 Mar 2021 13:03:12 +1100 Subject: [PATCH] Convert math context of the HR chapter --- chapters/5_half_reif.tex | 1932 +++++++++++++++++++------------------- 1 file changed, 966 insertions(+), 966 deletions(-) diff --git a/chapters/5_half_reif.tex b/chapters/5_half_reif.tex index 8af06ce..87297fd 100644 --- a/chapters/5_half_reif.tex +++ b/chapters/5_half_reif.tex @@ -3,9 +3,9 @@ %************************************************ 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 +\(\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 @@ -21,7 +21,7 @@ and flattening using reification. \end{mzn} which requires that if \mzninline{i \leq 4} then the value in the - \texttt{i}$^{th}$ position of array \mzninline{a} multiplied by \mzninline{x} + \texttt{i}\(^{th}\) position of array \mzninline{a} multiplied by \mzninline{x} must be at least 6. This becomes the following existentially quantified conjunction through flattening and reification:\footnote{Actually the result is in \flatzinc\ but we show an equivalent \minizinc\ form for easy of @@ -73,8 +73,8 @@ This is known as the \emph{strict} semantics 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 $\mzninline{false}$. For the example +relational semantics the value \(\bot\) percolates up through the term until it +reaches a Boolean subterm where it becomes \(\mzninline{false}\). For the example \begin{mzn} /* t1 @\(\equiv\)@ */ a[7] = ⊥; @@ -111,8 +111,8 @@ original complex constraint needs to be far more complex. to equal \texttt{i} if and only if \texttt{i} takes a value in the index set of \texttt{a}. % Finally the Boolean - % $b4$ defines when the rhs condition holds $b2$ - % and the \element{} constraint was safe $b3$. + % \(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 @@ -203,52 +203,52 @@ expressiveness in using global constraints. \jip{This section looks like background and should probably be moved} -We consider a typed set of variables $\VV = \VV_I \cup \VV_B$ made up of -\emph{integer} variables, $\VV_I$, and \emph{Boolean} variables, $\VV_b$. We use -lower case letters such as $x$ and $y$ for integer variables and letters such as -$b$ for Booleans. +We consider a typed set of variables \(\VV = \VV_I \cup \VV_B\) made up of +\emph{integer} variables, \(\VV_I\), and \emph{Boolean} variables, \(\VV_b\). We use +lower case letters such as \(x\) and \(y\) for integer variables and letters such as +\(b\) for Booleans. % -A \gls{domain} $D$ is a complete mapping from $\VV$ to finite sets of integers -(for the variables in $\VV_I$) and to subsets of -$\{\mzninline{true},\mzninline{false}\}$ (for the variables in $\VV_b$). +A \gls{domain} \(D\) is a complete mapping from \(\VV\) to finite sets of integers +(for the variables in \(\VV_I\)) and to subsets of +\(\{\mzninline{true},\mzninline{false}\}\) (for the variables in \(\VV_b\)). % -We can understand a \gls{domain} $D$ as a formula -$\wedge_{v \in \VV} (v \in D(v))$ stating for each variable $v$ that its value -is in its domain. A \emph{false domain} $D$ is a domain where -$\exists_{v \in \VV} D(v) = \emptyset$, and corresponds to an unsatisfiable +We can understand a \gls{domain} \(D\) as a formula +\(\wedge_{v \in \VV} (v \in D(v))\) stating for each variable \(v\) that its value +is in its domain. A \emph{false domain} \(D\) is a domain where +\(\exists_{v \in \VV} D(v) = \emptyset\), and corresponds to an unsatisfiable formula. -Let $D_1$ and $D_2$ be domains and $V\subseteq\VV$. We say that $D_1$ is -\emph{stronger} than $D_2$, written $D_1 \sqsubseteq D_2$, if -$D_1(v) \subseteq D_2(v)$ for all $v \in \VV$. -%% and that $D_1$ and $D_2$ -%% are \emph{equivalent modulo $V$}, written $D_1 =_V D_2$, if $D_1(v) = -%% D_2(v)$ for all $v \in V$. \pjs{Equivelant modulo never used???} +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$. +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\}$. +%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}$. +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 +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\}$. +\(\{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 +% 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)$. +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} @@ -258,52 +258,52 @@ 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))\}$ +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}$: +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)\}$ +\(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)$ +\(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{domain consistent} for constraint \(c\) if +\(D(v) = \{ \theta(v)~|~\theta \in solns(c)~\wedge~\theta \in D \}\), for all +\(v \in vars(c)\). -A domain $D$ is \emph{bounds(Z) consistent} for constraint $c$ over variables -$v_1, \ldots v_n$ if for each $i \in \{1, \ldots, n\}$ there exists -$\theta \in solns(c) \cap D$ s.t. $\theta(v_i) = \min D(v_i)$ and -$\min D(v_j) \leq \theta(v_j) \leq \max D(v_j), 1 \leq j \neq i \leq n$, and -similarly exists $\theta \in solns(c) \cap D$ s.t. $\theta(v_i) = \max D(v_i)$ -and $\min D(v_j) \leq \theta(v_j) \leq \max D(v_j), 1 \leq j \neq i \leq n$. For -Boolean variables $v$ we assume $\mzninline{false} < \mzninline{true}$. +A domain \(D\) is \emph{bounds(Z) consistent} for constraint \(c\) over variables +\(v_1, \ldots v_n\) if for each \(i \in \{1, \ldots, n\}\) there exists +\(\theta \in solns(c) \cap D\) s.t. \(\theta(v_i) = \min D(v_i)\) and +\(\min D(v_j) \leq \theta(v_j) \leq \max D(v_j), 1 \leq j \neq i \leq n\), and +similarly exists \(\theta \in solns(c) \cap D\) s.t. \(\theta(v_i) = \max D(v_i)\) +and \(\min D(v_j) \leq \theta(v_j) \leq \max D(v_j), 1 \leq j \neq i \leq n\). For +Boolean variables \(v\) we assume \(\mzninline{false} < \mzninline{true}\). -% A domain $D$ is \emph{bounds(R) consistent} for constraint $c$ if the same -% conditions as for bounds(Z) consistency hold except $\theta \in solns(c')$ where -% $c'$ is the \emph{real relaxation} of $c$. +% A domain \(D\) is \emph{bounds(R) consistent} for constraint \(c\) 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$. +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. @@ -311,17 +311,17 @@ 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 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. +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.) @@ -410,24 +410,24 @@ 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 an expression \(e\) that contains the subexpression \(x\), we denote by +\(e\subs{x/y}\) the expression that results from replacing all occurrences of +subexpression \(x\) by expression \(y\). We will also use the notation for multiple +simultaneous replacements \(\subs{\bar{x}/\bar{y}}\) where each \(x_i \in \bar{x}\) +is replaced by the corresponding \(y_i \in \bar{y}\). Given a \syntax{} term defining the constraints of the model we can split its \syntax{} subterms as occurring in different kinds of places: root contexts, positive contexts, negative contexts, and mixed contexts. A Boolean -subterm $t$ of constraint $c$ is in a \emph{root context} iff there is no -solution of $c\subs{t/\mzninline{false}}$, that is $c$ with subterm $t$ replaced by -$\mzninline{false}$.\footnote{For the definitions of context we assume that the subterm $t$ - is uniquely defined by its position in $c$, so the replacement is of exactly - one subterm.} Similarly, a subterm $t$ of constraint $c$ is in a -\emph{positive context} iff for any solution $\theta$ of $c$ then $\theta$ is -also a solution of $c\subs{t/\mzninline{true}}$; and a \emph{negative context} iff for any -solution $\theta$ of $c$ then $\theta$ is also a solution of $c\subs{t/\mzninline{false}}$. -The remaining Boolean subterms of $c$ are in \emph{mixed} contexts. While +subterm \(t\) of constraint \(c\) is in a \emph{root context} iff there is no +solution of \(c\subs{t/\mzninline{false}}\), that is \(c\) with subterm \(t\) replaced by +\(\mzninline{false}\).\footnote{For the definitions of context we assume that the subterm \(t\) + is uniquely defined by its position in \(c\), so the replacement is of exactly + one subterm.} Similarly, a subterm \(t\) of constraint \(c\) is in a +\emph{positive context} iff for any solution \(\theta\) of \(c\) then \(\theta\) is +also a solution of \(c\subs{t/\mzninline{true}}\); and a \emph{negative context} iff for any +solution \(\theta\) of \(c\) then \(\theta\) is also a solution of \(c\subs{t/\mzninline{false}}\). +The remaining Boolean subterms of \(c\) are in \emph{mixed} contexts. While determining contexts according to these definitions is hard, there are simple syntactic rules which can determine the correct context for most terms, and the rest can be treated as mixed. @@ -438,40 +438,40 @@ Consider the constraint expression constraint x > 0 /\ (i <= 4 -> x + bool2int(b) = 5); \end{mzn} -then \mzninline{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$ +then \mzninline{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 assume each integer variable \(x\) is separately declared with a finite initial +set of possible values \(D_{init}(x)\). We assume each array constant is +separately declared as a mapping \(\{ i \mapsto d~|~i \in \dom(a) \}\) where its +index set \(\dom(a)\) is a finite integer range. Given these initial declarations, +we can determine the set of possible values \(poss(t)\) of any term \(t\) in the +language as \(poss(t) = \{ \theta(t)~|~\theta \in D_{init} \}\). Note also while +it may be prohibitive to determine the set of possible values for any term \(t\), we can efficiently determine a superset of these values by building a superset for each subterm bottom up using approximation. % Given a \cons{} term defining the constraints of the model we can split its % \cons{} subterms as occurring in kinds of places: positive contexts, negative -% contexts, and mixed contexts. A Boolean subterm $t$ of constraint $c$, written -% $c[t]$, is in a \emph{positive context} iff for any solution $\theta$ of $c$ -% then $\theta$ is also a solution of $c[\mzninline{true}]$, that is $c$ with subterm $t$ -% replaced by $\mzninline{true}$. Similarly, a subterm $t$ of constraint $c$ is in a -% \emph{negative context} iff for any solution $\theta$ of $c$ then $\theta$ is -% also a solution of $c[\mzninline{false}]$. The remaining Boolean subterms of $c$ are in +% contexts, and mixed contexts. A Boolean subterm \(t\) of constraint \(c\), written +% \(c[t]\), is in a \emph{positive context} iff for any solution \(\theta\) of \(c\) +% then \(\theta\) is also a solution of \(c[\mzninline{true}]\), that is \(c\) with subterm \(t\) +% replaced by \(\mzninline{true}\). Similarly, a subterm \(t\) of constraint \(c\) is in a +% \emph{negative context} iff for any solution \(\theta\) of \(c\) then \(\theta\) is +% also a solution of \(c[\mzninline{false}]\). The remaining Boolean subterms of \(c\) are in % mixed contexts. % \begin{example} -% Consider the constraint expression $c$ \negspace +% 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 +% 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} @@ -480,16 +480,16 @@ for each subterm bottom up using approximation. % 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 +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)$. +\(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:hr-translation} @@ -499,9 +499,9 @@ 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$. +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 @@ -527,7 +527,7 @@ satisfied state of the constraint $c$. \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 +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. @@ -546,108 +546,108 @@ 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$. +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 +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: +\(\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$, +% \(\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 $\mzninline{true}$ by -the constraints in $S$. For succinctness we use the notation $\new b$ ($\new v$) +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 \(\mzninline{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 +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 +again. We retrieve the result of the previous flattening \(h\) and the previous +context \(prev\). If the expression previously appeared at the root then we simply reuse the old value, since regardless of the new context the expression must -hold. If the new context is $\rootc$ we reuse the old value but require it to be -$\mzninline{true}$ in $S$, and modify the hash table to record the expression appears at +hold. If the new context is \(\rootc\) we reuse the old value but require it to be +\(\mzninline{true}\) in \(S\), and modify the hash table to record the expression appears at the root. If the expression appeared in a mixed context we simply reuse the old result since this is the most constrained context. Similarly if the previous context is the same as the current one we reuse the old result. In the remaining -cases we set the context to $\mix$ since the remaining cases require at least -both a $\pos$ and $\negc$ or a $\mix$ context. Note that if an expression +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 +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 @@ -662,18 +662,18 @@ this. For non-fixed expressions we treat each form in turn. Boolean literals and variables are simply returned. Basic relational operations flatten their terms -using the function $\flatt$, which for a term $t$ returns a tuple $\tuple{v,b}$ -of an integer variable/value $v$ and a Boolean literal $b$ such that -$b \full (v = t)$ (described in detail below). The relational operations then +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 +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 @@ -688,227 +688,227 @@ 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 $\mzninline{true}$ by adding $b$ to $S$. +Finally if we are in the root context, we ensure that the Boolean \(b\) returned +must be \(\mzninline{true}\) by adding \(b\) to \(S\). { \begin{tabbing} xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill -\flatc($c$,$\ctxt$) \\ -\> $\tuple{h,prev}$ := hash[$c$]; \\ -\> \textbf{if} ($h \neq \bot$) \\ -\>\> \textbf{if} ($prev =\rootc$) \textbf{return} $h$ \\ -\>\> \textbf{if} ($ctxt = \rootc$) $S$ \cupp $\{ h \}$; hash[$c$] := -$\tuple{h,\rootc}$; \textbf{return} $h$ +\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{if} (\(prev = \mix \vee prev = \ctxt\)) +\textbf{return} \(h\) \\ +\>\> \(\ctxt\) := \(\mix\) \\ +\> \textbf{if} (\(\fixed(c)\)) \(b\) := \(\eval(c)\) \\ \> \textbf{else} \\ -\> \> \textbf{switch} $c$ \\ -%\> \> \textbf{case} \texttt{true}: $b$ := $\mzninline{true}$;\\ -%\> \> \textbf{case} \texttt{false}: $b$ := $\mzninline{false}$;\\ -\> \> \textbf{case} $b'$ (\syntax{}): $b$ := $b'$; \\ -\> \> \textbf{case} $t_1$ $r$ $t_2$ (\syntax{}): \\ -\>\>\> $\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{switch} \(c\) \\ +%\> \> \textbf{case} \texttt{true}: \(b\) := \(\mzninline{true}\);\\ +%\> \> \textbf{case} \texttt{false}: \(b\) := \(\mzninline{false}\);\\ +\> \> \textbf{case} \(b'\) (\syntax{}): \(b\) := \(b'\); \\ +\> \> \textbf{case} \(t_1\) \(r\) \(t_2\) (\syntax{}): \\ +\>\>\> \(\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,\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,\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} \(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{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''), +\textbf{foreach}(\(j \in 1..n\)) \(b_j\) := \(\flatc(c_j, \posop \ctxt)\); \\ +\>\>\> \(\tuple{v, b_{n+1}}\) := \(\flatt(t, \ctxt)\); \\ +%\>\>\> \(S\) \cupp +%\(\{ \new b \full (b_{n+1} \wedge \new b' \wedge \new b''), %\mathit{safeelement}(v, [b_1, \ldots, b_n], b'), -%b'' \full v \in \{1,..,n\} \} $ \\ -\>\>\> \textbf{if} ($\ctxt = \rootc$) $S$ \cupp $\{\texttt{element}(v', [b_1, \ldots, b_n], -\mzninline{true})\}$; $b$ := $\mzninline{true}$ \\ +%b'' \full v \in \{1,..,n\} \} \) \\ +\>\>\> \textbf{if} (\(\ctxt = \rootc\)) \(S\) \cupp \(\{\texttt{element}(v', [b_1, \ldots, b_n], +\mzninline{true})\}\); \(b\) := \(\mzninline{true}\) \\ \>\>\> \textbf{else} \\ -\>\>\>\> $S$ \cupp -$\{ \new b \full (b_{n+1} \wedge \new b' \wedge \new b''), \new v' \in \{1, -\ldots, n\},$ \\ -\>\>\>\>\>\>\> $\texttt{element}(v', [b_1, \ldots, b_n], b'), -b'' \full v = v', b'' \full v \in \{1,\ldots,n\} \} $ +\>\>\>\> \(S\) \cupp +\(\{ \new b \full (b_{n+1} \wedge \new b' \wedge \new b''), \new v' \in \{1, +\ldots, n\},\) \\ +\>\>\>\>\>\>\> \(\texttt{element}(v', [b_1, \ldots, b_n], b'), +b'' \full v = v', b'' \full v \in \{1,\ldots,n\} \} \) \\ \callbyvalue{% -\>\> \textbf{case} $p$ ($t_1, \ldots, t_n$) (\syntax{}) 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{case} \(p\) (\(t_1, \ldots, t_n\)) (\syntax{}) built-in predicate: \\ +\> \> \> \textbf{foreach}(\(j \in 1..n\)) \(\tuple{v_j, b_j}\) := \(\flatt(t_j,\ctxt)\); \\ +\> \> \> \textbf{if} (\(\ctxt \neq \rootc\)) \\ +\> \> \> \> \textbf{if} (\(p\_reif\) does not exist) \textbf{abort} \\ +\> \> \> \> \textbf{else} \(S\) \cupp \(\{ p\_reif(v_1,\ldots,v_n,\new b'), +\new b \Leftrightarrow b' \wedge \bigwedge_{j=1}^n b_j\}\) \\ \> \> \> \textbf{else} \\ -\>\> \> \> $b$ := $\mzninline{true}$; $S$ \cupp $\{ p(v_1, \ldots, v_n) %, \bigwedge_{j=1}^n b_j -\}$ +\>\> \> \> \(b\) := \(\mzninline{true}\); \(S\) \cupp \(\{ p(v_1, \ldots, v_n) %, \bigwedge_{j=1}^n b_j +\}\) \\ -\>\> \textbf{case} $p$ ($t_1, \ldots, t_n$) (\syntax{}): 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)$ +\>\> \textbf{case} \(p\) (\(t_1, \ldots, t_n\)) (\syntax{}): 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\}$ +\> \>\> \(S\) \cupp \(\{ \new b \Leftrightarrow b' \wedge \bigwedge_{j=1}^n +b_j\}\) \\ } \callbyunroll{% -\>\> \textbf{case} $p$ ($t_1, \ldots, t_n$) (\syntax{}) built-in predicate: \\ -\> \> \> \textbf{if} ($\ctxt \neq \rootc$) \textbf{abort} \\ -\> \> \> \textbf{foreach}($j \in 1..n$) $\tuple{v_j, \_}$ := $\flatt(t_j,\rootc)$; \\ -\>\> \> $b$ := $\mzninline{true}$; $S$ \cupp $\{ p(v_1, \ldots, v_n)\}$ +\>\> \textbf{case} \(p\) (\(t_1, \ldots, t_n\)) (\syntax{}) built-in predicate: \\ +\> \> \> \textbf{if} (\(\ctxt \neq \rootc\)) \textbf{abort} \\ +\> \> \> \textbf{foreach}(\(j \in 1..n\)) \(\tuple{v_j, \_}\) := \(\flatt(t_j,\rootc)\); \\ +\>\> \> \(b\) := \(\mzninline{true}\); \(S\) \cupp \(\{ p(v_1, \ldots, v_n)\}\) \\ -\>\> \textbf{case} $p$ ($t_1, \ldots, t_n$) (\syntax{}): 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} \(p\) (\(t_1, \ldots, t_n\)) (\syntax{}): 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{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{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$ +\> \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 +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+]+ +\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}$ +\> \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{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+]+ +\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} +\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 +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 +\(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')}$ +\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{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\) : \> +\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} \(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{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}$ +\> \textbf{return} \(\tuple{c,t}\) \end{tabbing} } \subsection{Flattening Integer Expressions} -$\flatt(t,\ctxt)$ flattens an integer term $t$ in context $\ctxt$. It returns a -tuple $\tuple{v,b}$ of an integer variable/value $v$ and a Boolean literal $b$, -and as a side effect adds constraints to $S$ so that -$S \models b \full (v = t)$. Note that again flattening in the root context -always returns a Boolean $b$ made equivalent to $\mzninline{true}$ by the constraints in -$S$. +\(\flatt(t,\ctxt)\) flattens an integer term \(t\) in context \(\ctxt\). It returns a +tuple \(\tuple{v,b}\) of an integer variable/value \(v\) and a Boolean literal \(b\), +and as a side effect adds constraints to \(S\) so that +\(S \models b \full (v = t)\). Note that again flattening in the root context +always returns a Boolean \(b\) made equivalent to \(\mzninline{true}\) by the constraints in +\(S\). Flattening first checks if the same expression has been flattened previously and if so returns the stored result. \flatt{} evaluates fixed integer expressions and returns the result. -% For non-fixed integer expressions $t$, if $t$ +% 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 +% \(\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 +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} @@ -923,136 +923,136 @@ simply evaluates the \emph{if} condition (which must be fixed) and flattens 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, + 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$ +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'}$ +\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$ := $\mzninline{true}$ \\ +\>\> \textbf{if} (\(prev = \mix \vee prev = \ctxt\)) +\textbf{return} \(\tuple{h,b'}\) \\ +\>\> \(\ctxt\) := \(\mix\) \\ +\> \textbf{if} (\(\fixed(t)\)) \(v\) := \(\eval(t)\); \(b\) := \(\mzninline{true}\) \\ \> \textbf{else} %\\ -%% \> \> \textbf{if} ($t$ is marked \emph{total}) $\ctxt$ := $\rootc$ \\ +%% \> \> \textbf{if} (\(t\) is marked \emph{total}) \(\ctxt\) := \(\rootc\) \\ %\> \> -\textbf{switch} $t$ \\ -%\> \> \textbf{case} $i$ (\intc): $v$ := $i$; $b$ := $\mzninline{true}$ \\ -\> \> \textbf{case} $v'$ (\syntax{}): $v$ := $v'$; $b$ := $\mzninline{true}$\\ -\> \> \textbf{case} $t_1$ $a$ $t_2$ (\syntax{}): \\ +\textbf{switch} \(t\) \\ +%\> \> \textbf{case} \(i\) (\intc): \(v\) := \(i\); \(b\) := \(\mzninline{true}\) \\ +\> \> \textbf{case} \(v'\) (\syntax{}): \(v\) := \(v'\); \(b\) := \(\mzninline{true}\)\\ +\> \> \textbf{case} \(t_1\) \(a\) \(t_2\) (\syntax{}): \\ \> \> \> -$\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{]}: \\ +\(\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), +\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\} \}$ +%b' \full v_0 \in \{1,...,n\} \}\) %\\ -\>\>\> \textbf{if} ($\ctxt \neq \rootc$) \\ -\>\>\>\> $S$ \cupp -$\{ \new b \full (\new b' \wedge \bigwedge_{j=0}^n b_j), \new v' \in \{1, -\ldots, n\},$ \\ -\>\>\>\>\>\>\> $\texttt{element}(v', [v_1, \ldots, v_n], \new v), -b' \full v_0 = v', b' \full v_0 \in \{1,\ldots,n\} \} $ +\>\>\> \textbf{if} (\(\ctxt \neq \rootc\)) \\ +\>\>\>\> \(S\) \cupp +\(\{ \new b \full (\new b' \wedge \bigwedge_{j=0}^n b_j), \new v' \in \{1, +\ldots, n\},\) \\ +\>\>\>\>\>\>\> \(\texttt{element}(v', [v_1, \ldots, v_n], \new v), +b' \full v_0 = v', b' \full v_0 \in \{1,\ldots,n\} \} \) \\ -\>\>\> \textbf{else} $S$ \cupp $\{\new b, \texttt{element}(v', [v_1, \ldots, v_n], -\new v) \}$ \\ -\> \> \textbf{case} \texttt{sum(} $\mathit{ia}$ \texttt{)}: \\ -\> \> \> \textbf{let} $[t_1, \ldots, t_n] = \evalb(ia)$; \\ -\> \> \> \textbf{foreach}($j \in 1..n$) $\tuple{v_j, b_j}$ := -$\flatt(t_j,\ctxt)$; \\ -\>\>\> $S$ \cupp $\{ \new b \full \bigwedge_{j=1}^n b_j, - \new v = \sum_{j=1}^n v_j \}$ \\ +\>\>\> \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$) +%\(\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{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{if} (\(eval(c_0)\)) \(\tuple{v,b}\) := \(\flatt(t_1,\ctxt)\) \textbf{else} +\(\tuple{v,b}\) := \(\flatt(t_2,\ctxt)\) \\ -\>\> \textbf{case} \texttt{bool2int(} $c_0$ \texttt{)}: - $b_0$ := $\flatc(c_0, \mix)$; - $S$ \cupp $\{ \texttt{bool2int}(b_0, \new v), \new b \}$ \\ +\>\> \textbf{case} \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$) (\syntax{}): function \\ -\> \> \> \textbf{foreach}($j \in 1..n$) $\tuple{v_j, b_j}$ := $\flatt(t_j,\ctxt)$; \\ -\>\> \> \textbf{let} $f(x_1, \ldots, x_n) = t_0$ be defn of $f$ \\ -\> \> \> \textbf{if} ($f$ is declared total) $\ctxt' = \rootc$ \textbf{else} -$\ctxt' = \ctxt$ \\ -\>\> \> $\tuple{v,b'}$ := $\flatt(t_0\subs{x_1/v_1, \ldots, x_n/v_n},\ctxt')$ \\ -\> \> \> $S$ \cupp $\{ \new b \full b' \wedge \bigwedge_{j=1}^n b_j \}$ +\>\> \textbf{case} \(f\) (\(t_1, \ldots, t_n\)) (\syntax{}): 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$) (\syntax{}): 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\)) (\syntax{}): 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$) (\syntax{}): 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{case} \(f\) (\(t_1, \ldots, t_n\)) (\syntax{}): 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)$ +%\> \> \> \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)\}$ +%\>\> \> \(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}$ +\> \textbf{if} (\(\ctxt = \rootc\)) \(S\) \cupp \(\{ b \}\); \\ +\> hash[\(t\)] := \(\tuple{v,b,\ctxt}\) \\ +\> \textbf{return} \(\tuple{v,b}\) \end{tabbing} \begin{example}\label{ex:hr-flat} Consider the flattening of the expression - $$ + \[ a[x] + bool2int(x > y) - bool2int(x > z) \geq 4 \vee (a[x] \leq 2 \wedge x > y \wedge (x > z \rightarrow b)) - $$ + \] The different terms and subterms of the expression are illustrated and numbered in \cref{fig:hr-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] \\ @@ -1066,13 +1066,13 @@ $S$ \cupp $\{ \new b \full (b_1 \wedge b_2)\}$ 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:hr-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. + 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: @@ -1103,25 +1103,25 @@ $S$ \cupp $\{ \new b \full (b_1 \wedge b_2)\}$ 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})$ + % \(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 + 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 @@ -1146,20 +1146,20 @@ $S$ \cupp $\{ \new b \full (b_1 \wedge b_2)\}$ 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})$; + % \(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} @@ -1168,23 +1168,23 @@ $S$ \cupp $\{ \new b \full (b_1 \wedge b_2)\}$ % 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$. +% constraint \(c\) the \emph{full reified form} for \(c\) is \(b \full c\), where +% \(b \not\in vars(c)\) is a Boolean variable naming the satisfied state of the +% constraint \(c\). %\newcommand{\new}{\textbf{new}~} %\newcommand{\flatc}{\textsf{flatc}} %\newcommand{\flatt}{\textsf{flatt}} \newcommand{\safen}{\textsf{safen}} -% The pseudo-code for \flatc($b$,$c$) flattens a constraint expression $c$ to be -% equal to $b$, returning a set of constraints implementing $b \full c$. We -% flatten a whole model $c$ using $\flatc(\mzninline{true}, c)$. In the pseudo-code the -% expressions $\new b$ and $\new v$ create a new Boolean and integer variable +% The pseudo-code for \flatc(\(b\),\(c\)) flattens a constraint expression \(c\) to be +% equal to \(b\), returning a set of constraints implementing \(b \full c\). We +% flatten a whole model \(c\) using \(\flatc(\mzninline{true}, c)\). In the pseudo-code the +% expressions \(\new b\) and \(\new v\) create a new Boolean and integer variable % respectively. % The code assumes there are reified versions of the basic relational -% constraints $r$ available, as well as reified versions of the Boolean +% 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. @@ -1192,94 +1192,94 @@ $S$ \cupp $\{ \new b \full (b_1 \wedge b_2)\}$ % {\small % \begin{tabbing} % xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill -% \flatc($b$,$c$) \\ -% \> \textbf{switch} $c$ \\ -% \> \textbf{case} \texttt{true}: \textbf{return} $\{ b \}$ \\ -% \> \textbf{case} \texttt{false}: \textbf{return} $\{ \neg b \}$ \\ -% \> \textbf{case} $b'$ (\syntax{}): \textbf{return} $\{ b \full b' \}$ \\ -% \> \textbf{case} $t_1$ $r$ $t_2$ (\relop): \textbf{return} $\safen(b, \flatt(\new i_1, t_1) \cup \flatt(\new i_2, t_2)) \cup \{ b \full i_1~r~i_2 \}$ \\ -% \> \textbf{case} \texttt{not} $c_1$: -% \textbf{return} $\flatc(\new b_1, c_1) \cup \{ b \full \neg b_1 \}$ \\ -% \> \textbf{case} $c_1$ \verb+/\+ $c_2$: \= -% \textbf{if} ($b \equiv \mzninline{true}$) \textbf{return} $\flatc(\mzninline{true}, c_1) \cup -% \flatc(\mzninline{true}, c_2)$ \\ -% \> \> \textbf{else} \textbf{return} $\flatc(\new b_1, c_1) \cup -% \flatc(\new b_2, c_2) \cup \{ b \full (b_1 \wedge b_2)\}$ \\ +% \flatc(\(b\),\(c\)) \\ +% \> \textbf{switch} \(c\) \\ +% \> \textbf{case} \texttt{true}: \textbf{return} \(\{ b \}\) \\ +% \> \textbf{case} \texttt{false}: \textbf{return} \(\{ \neg b \}\) \\ +% \> \textbf{case} \(b'\) (\syntax{}): \textbf{return} \(\{ b \full b' \}\) \\ +% \> \textbf{case} \(t_1\) \(r\) \(t_2\) (\relop): \textbf{return} \(\safen(b, \flatt(\new i_1, t_1) \cup \flatt(\new i_2, t_2)) \cup \{ b \full i_1~r~i_2 \}\) \\ +% \> \textbf{case} \texttt{not} \(c_1\): +% \textbf{return} \(\flatc(\new b_1, c_1) \cup \{ b \full \neg b_1 \}\) \\ +% \> \textbf{case} \(c_1\) \verb+/\+ \(c_2\): \= +% \textbf{if} (\(b \equiv \mzninline{true}\)) \textbf{return} \(\flatc(\mzninline{true}, c_1) \cup +% \flatc(\mzninline{true}, c_2)\) \\ +% \> \> \textbf{else} \textbf{return} \(\flatc(\new b_1, c_1) \cup +% \flatc(\new b_2, c_2) \cup \{ b \full (b_1 \wedge b_2)\}\) \\ % xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill -% \> \textbf{case} $c_1$ \verb+\/+ $c_2$: \textbf{return} $\flatc(\new b_1, c_1) \cup +% \> \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 +% 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 +% b_2)\}\) \\ +% \> \textbf{case} \(c_1\) \verb+<->+ \(c_2\): \textbf{return} \(\flatc(\new b_1, c_1) \cup % \flatc(\new b_2, c_2) \cup \{ b \full (b_1 \full -% b_2)\}$ \\ -% \> \textbf{case} $p$ ($t_1, \ldots, t_n$) (\syntax{}): \\ -% \> \> \textbf{if} ($b \equiv \mzninline{true}$) \textbf{return} $\safen(b, -% \cup_{j=1}^n \flatt(\new v_j, t_j)) \cup \{ p(v_1, \ldots, v_n) \}$ \\ +% b_2)\}\) \\ +% \> \textbf{case} \(p\) (\(t_1, \ldots, t_n\)) (\syntax{}): \\ +% \> \> \textbf{if} (\(b \equiv \mzninline{true}\)) \textbf{return} \(\safen(b, +% \cup_{j=1}^n \flatt(\new v_j, t_j)) \cup \{ p(v_1, \ldots, v_n) \}\) \\ % \> \> \textbf{else} \textbf{abort} % \end{tabbing} % } -% The code $\flatt(v,t)$ flattens an integer term $t$, creating constraints -% that equate the term with variable $v$. It creates new variables to store +% The code \(\flatt(v,t)\) flattens an integer term \(t\), creating constraints +% that equate the term with variable \(v\). It creates new variables to store % the values of subterms, replaces integer operations by their relational % versions, and array lookups by \element. % \begin{tabbing} % xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill -% \flatt($v$,$t$) \\ -% \> \textbf{switch} $t$ \\ -% \> \textbf{case} $i$ (\intc): \textbf{return} $\{v = i\}$ \\ -% \> \textbf{case} $v'$ (\syntax{}): \textbf{return} $\{ v = v' \}$ \\ -% \> \textbf{case} $t_1$ $a$ $t_2$ (\syntax{}): -% \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) \})$ +% \flatt(\(v\),\(t\)) \\ +% \> \textbf{switch} \(t\) \\ +% \> \textbf{case} \(i\) (\intc): \textbf{return} \(\{v = i\}\) \\ +% \> \textbf{case} \(v'\) (\syntax{}): \textbf{return} \(\{ v = v' \}\) \\ +% \> \textbf{case} \(t_1\) \(a\) \(t_2\) (\syntax{}): +% \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 +The procedure \safen(\(b, C\)) enforces the relational semantics for unsafe expressions, by ensuring that the unsafe relational versions of partial functions are made safe. Note that to implement the \emph{strict semantics} as -opposed to the relational semantics we just need to define $\safen(b,C) = C$. If -$b \equiv \mzninline{true}$ then the relational semantics and the strict semantics +opposed to the relational semantics we just need to define \(\safen(b,C) = C\). If +\(b \equiv \mzninline{true}\) then the relational semantics and the strict semantics coincide, so nothing needs to be done. The same is true if the set of -constraints $C$ is safe. For $div(x,y,z)$, the translation introduces a new -variable $y'$ which cannot be 0, and equates it to $y$ if $y \neq 0$. The -constraint $div(x,y',z)$ never reflects a partial function application. The new -variable $b'$ captures whether the partial function application returns a non -$\bot$ value. For \mzninline{element(v, a, x)}, it introduces a new variable $v'$ -which only takes values in $\dom(a)$ and forces it to equal $v$ if -$v \in \dom(a)$. A partial function application forces $b = \mzninline{false}$ since it is -the conjunction of the new variables $b'$. The \%HALF\% comments will be +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 \mzninline{element(v, a, x)}, it introduces a new variable \(v'\) +which only takes values in \(\dom(a)\) and forces it to equal \(v\) if +\(v \in \dom(a)\). A partial function application forces \(b = \mzninline{false}\) since it is +the conjunction of the new variables \(b'\). The \%HALF\% comments will be explained later. \begin{tabbing} xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill -\safen($b$,$C$) \\ -\> \textbf{if} ($b \equiv \mzninline{true}$) \textbf{return} $C$ \\ -\> \textbf{if} ($C$ is a set of safe constraints) \textbf{return} $C$ \\ -\> $B$ := $\emptyset$; $S$ := $\emptyset$ \\ -\> \textbf{foreach} $c \in C$ \\ -\> \> \textbf{if} ($c \equiv div(x,y,z)$ and $y$ can take value 0) \\ -\> \> \> $B$ := $B \cup \{ \new b' \}$ \\ -\> \> \> $S$ := $S \cup \{ \new y' \neq 0, b' \full y \neq 0, b' \full y -= y', div(x,y',z) \}$ \\ -\> \> \> \%HALF\% $S$ := $S \cup \{ b' \full y \neq 0, b' \half -div(x,y,z)\}$ \\ -\> \> \textbf{else if} \(c \equiv \mzninline{element(v, a, x)}\) and $v$ can take a value outside the domain of $a$) \\ -\> \> \> $B$ := $B \cup \{ \new b' \}$ \\ -\> \> \> $S$ := $S \cup \{ \new v' \in \dom(a), +\safen(\(b\),\(C\)) \\ +\> \textbf{if} (\(b \equiv \mzninline{true}\)) \textbf{return} \(C\) \\ +\> \textbf{if} (\(C\) is a set of safe constraints) \textbf{return} \(C\) \\ +\> \(B\) := \(\emptyset\); \(S\) := \(\emptyset\) \\ +\> \textbf{foreach} \(c \in C\) \\ +\> \> \textbf{if} (\(c \equiv div(x,y,z)\) and \(y\) can take value 0) \\ +\> \> \> \(B\) := \(B \cup \{ \new b' \}\) \\ +\> \> \> \(S\) := \(S \cup \{ \new y' \neq 0, b' \full y \neq 0, b' \full y += y', div(x,y',z) \}\) \\ +\> \> \> \%HALF\% \(S\) := \(S \cup \{ b' \full y \neq 0, b' \half +div(x,y,z)\}\) \\ +\> \> \textbf{else if} \(c \equiv \mzninline{element(v, a, x)}\) and \(v\) can take a value outside the domain of \(a\)) \\ +\> \> \> \(B\) := \(B \cup \{ \new b' \}\) \\ +\> \> \> \(S\) := \(S \cup \{ \new v' \in \dom(a), b' \full v \in \dom(a), b' \full v = v', -\mzninline{element(v', a, x)}\}$ \\ -\> \> \> \%HALF\% $S$ := $S \cup \{ b' \full v \in \dom(a), b' \half -\mzninline{element(v, a, x)}\}$ \\ -\> \> \textbf{else} $S$ := $S \cup \{c\}$ \\ -\> \> \textbf{return} $S \cup \{b \full \wedge_{b' \in B} b' -\})$ +\mzninline{element(v', a, x)}\}\) \\ +\> \> \> \%HALF\% \(S\) := \(S \cup \{ b' \full v \in \dom(a), b' \half +\mzninline{element(v, a, x)}\}\) \\ +\> \> \textbf{else} \(S\) := \(S \cup \{c\}\) \\ +\> \> \textbf{return} \(S \cup \{b \full \wedge_{b' \in B} b' +\})\) \end{tabbing} The flattening algorithms above can produce suboptimal results in special cases, @@ -1290,12 +1290,12 @@ presentation, we omit the algorithms we use to do this. \section{Half Reification} \label{sec:hr-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. +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$. -$$ +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) & = & \{ \mzninline{false} \} \cap D(b) & \text{if~} f_c(D) \text{~is a false domain} \\ f_{b \half c}(D)(b) & = & D(b) & \text{otherwise} \\ @@ -1303,38 +1303,38 @@ f_{b \half c}(D)(v) & = & D(v) & \text{if~} v \in vars(c) \text{~and~} \mzninlin f_{b \half c}(D)(v) & = & f_c(D)(v) & \text{if~} v \in vars(c) \text{~and~} \mzninline{false} \not\in D(b) \end{array} -$$ +\] -% In reality most propagator implementations for $c$ can be thought of as -% a sequence of two propagators $f_c = f_{prop(c)} \cdot f_{check(c)}$ +% 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) & = & 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)$. +% \] +% 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])$ +% \(\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 +% 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 +% Given this separation we can improve the definition of \(f_{b \half c}\) above by +% replacing the check ``\(f_c(D)\) is a false domain'' by ``\(f_{check(c)}(D)\) is a % false domain''. In practice it means that the half-reified propagator can be -% implemented to only perform the checking part until $D(b) = \{\mzninline{true}\}$, when it +% implemented to only perform the checking part until \(D(b) = \{\mzninline{true}\}\), when it % needs to perform both. In practice most propagator implementations for \mzninline{c} first check @@ -1346,8 +1346,8 @@ determines a maximum matching between variables and values first, if this is not of size \mzninline{length(X)} it fails before propagating; the timetable \texttt{cumulative} constraint determines a profile of necessary resource usage, and fails if this breaks the resource limit, before considering propagation. We -can implement the propagator for $f_{\mzninline{b -> c}}$ by only performing the -checking part until $D(\texttt{b}) = \{\mzninline{true}\}$. +can implement the propagator for \(f_{\mzninline{b -> c}}\) by only performing the +checking part until \(D(\texttt{b}) = \{\mzninline{true}\}\). Half reification naturally encodes the relational semantics for partial function applications in positive contexts. We associate a Boolean variable \texttt{b} with each @@ -1362,8 +1362,8 @@ half-reified using the variable of the nearest enclosing Boolean term. 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 + 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} @@ -1375,14 +1375,14 @@ half-reified using the variable of the nearest enclosing Boolean term. \end{mzn} The unsafe \mzninline{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 = \mzninline{false}$. Given this, the final constraint requires $b1 = \mzninline{true}$, which - in turn requires $i > 4$. Since this holds, the whole constraint is $\mzninline{true}$ - with no restrictions on $x$. + enclosing Boolean term. Note that if \(i = 7\) then the second constraint makes + \(b2 = \mzninline{false}\). Given this, the final constraint requires \(b1 = \mzninline{true}\), which + in turn requires \(i > 4\). Since this holds, the whole constraint is \(\mzninline{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 +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} @@ -1412,9 +1412,9 @@ not propagate unnecessarily. (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: + 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]; @@ -1425,8 +1425,8 @@ not propagate unnecessarily. 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 $\mzninline{false}$ and $a[i]$ to 0, and the long + Whenever the start time of task \(i\) is constrained so that it does not overlap + time \(s[j]\), then \(b3[i]\) is fixed to \(\mzninline{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 @@ -1444,16 +1444,16 @@ not propagate unnecessarily. \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 + \(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]$. + 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 $\mzninline{true}$ by full reification will never be fixed by +variables that are fixed to \(\mzninline{true}\) by full reification will never be fixed by half reification. This is advantageous, but a corresponding disadvantage is that variables that are fixed can allow the simplification of the propagator, and hence make its propagation faster. We can reduce this disadvantage by fully @@ -1472,18 +1472,18 @@ 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(\mzninline{true}, c)$. The half-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(\mzninline{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 +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 +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}} @@ -1493,192 +1493,192 @@ subexpressions will be processed by recursive invocations of the algorithm. \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 +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 +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 +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 +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 +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 +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$. +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 +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. +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$ +\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{if} (\(\fixed(c)\)) \(b\) := \(\eval(c)\) \\ \> \textbf{else} \\ -\> \> \textbf{switch} $c$ \\ -%\> \> \textbf{case} \texttt{true}: $b$ := $\mzninline{true}$;\\ -%\> \> \textbf{case} \texttt{false}: $b$ := $\mzninline{false}$;\\ -\> \> \textbf{case} $b'$ (\syntax{}): $b$ := $b'$; \\ -\> \> \textbf{case} $t_1$ $r$ $t_2$ (\syntax{}): \\ -\> \> \> \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{switch} \(c\) \\ +%\> \> \textbf{case} \texttt{true}: \(b\) := \(\mzninline{true}\);\\ +%\> \> \textbf{case} \texttt{false}: \(b\) := \(\mzninline{false}\);\\ +\> \> \textbf{case} \(b'\) (\syntax{}): \(b\) := \(b'\); \\ +\> \> \textbf{case} \(t_1\) \(r\) \(t_2\) (\syntax{}): \\ +\> \> \> \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))\}$ +\> \> \> \(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 (\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 (\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} \(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{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''), +\textbf{foreach}(\(j \in 1..n\)) \(b_j\) := \(\halfc(c_j, \posop \ctxt)\); \\ +\>\>\> \(\tuple{v, b_{n+1}}\) := \(\halft(t, \ctxt, \iboth)\); \\ +%\>\>\> \(S\) \cupp +%\(\{ \new b \full (b_{n+1} \wedge \new b' \wedge \new b''), %\mathit{safeelement}(v, [b_1, \ldots, b_n], b'), -%b'' \full v \in \{1,..,n\} \} $ \\ -\>\>\> \textbf{if} ($\ctxt = \rootc$) -$S$ \cupp $\{\texttt{element}(v, [b_1, \ldots, b_n], \mzninline{true}), \new b\}$ \\ +%b'' \full v \in \{1,..,n\} \} \) \\ +\>\>\> \textbf{if} (\(\ctxt = \rootc\)) +\(S\) \cupp \(\{\texttt{element}(v, [b_1, \ldots, b_n], \mzninline{true}), \new b\}\) \\ \>\>\> \textbf{else} -$S$ \cupp $\{ \new b \half (b_{n+1} \wedge \new b'), b \half -\texttt{element}(v, [b_1, \ldots, b_n], b') \}$ \\ +\(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\} \} $ +%\>\>\>\> \(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$) (\syntax{}) built-in predicate: \\ -\> \> \> \textbf{foreach}($j \in 1..n$) $\tuple{v_j, b_j}$ := -$\halft(t_j,\ctxt,\iboth)$; \\ -\> \> \> \textbf{if} ($\ctxt = \rootc$) -$b$ := $\mzninline{true}$; $S$ \cupp $\{ p(v_1, \ldots, v_n) %, \bigwedge_{j=1}^n b_j -\}$ +\>\> \textbf{case} \(p\) (\(t_1, \ldots, t_n\)) (\syntax{}) built-in predicate: \\ +\> \> \> \textbf{foreach}(\(j \in 1..n\)) \(\tuple{v_j, b_j}\) := +\(\halft(t_j,\ctxt,\iboth)\); \\ +\> \> \> \textbf{if} (\(\ctxt = \rootc\)) +\(b\) := \(\mzninline{true}\); \(S\) \cupp \(\{ p(v_1, \ldots, v_n) %, \bigwedge_{j=1}^n b_j +\}\) \\ -\>\>\> \textbf{else} %($\ctxt = \pos$) \\ \> \> \> \> -$S$ \cupp $\{ p\_half(v_1,\ldots,v_n,\new b'), -\new b \half b' \wedge \bigwedge_{j=1}^n b_j\}$ \\ +\>\>\> \textbf{else} %(\(\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{if} (\(p\_reif\) does not exist) \textbf{abort} \\ +%\> \> \> \> \textbf{else} \(S\) \cupp \(\{ p\_reif(v_1,\ldots,v_n,\new b'), +%\new b \half b' \wedge \bigwedge_{j=1}^n b_j\}\) \\ %\\ -\>\> \textbf{case} $p$ ($t_1, \ldots, t_n$) (\syntax{}): 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)$ +\>\> \textbf{case} \(p\) (\(t_1, \ldots, t_n\)) (\syntax{}): 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\}$ +\> \>\> \(S\) \cupp \(\{ \new b \half b' \wedge \bigwedge_{j=1}^n +b_j\}\) \\ } \callbyunroll{% -\>\> \textbf{case} $p$ ($t_1, \ldots, t_n$) (\syntax{}) built-in predicate: \\ -\> \> \> \textbf{if} ($\ctxt \neq \rootc$) \textbf{abort} \\ -\> \> \> \textbf{foreach}($j \in 1..n$) $\tuple{v_j, \_}$ := $\flatt(t_j,\rootc)$; \\ -\>\> \> $b$ := $\mzninline{true}$; $S$ \cupp $\{ p(v_1, \ldots, v_n)\}$ +\>\> \textbf{case} \(p\) (\(t_1, \ldots, t_n\)) (\syntax{}) built-in predicate: \\ +\> \> \> \textbf{if} (\(\ctxt \neq \rootc\)) \textbf{abort} \\ +\> \> \> \textbf{foreach}(\(j \in 1..n\)) \(\tuple{v_j, \_}\) := \(\flatt(t_j,\rootc)\); \\ +\>\> \> \(b\) := \(\mzninline{true}\); \(S\) \cupp \(\{ p(v_1, \ldots, v_n)\}\) \\ -\>\> \textbf{case} $p$ ($t_1, \ldots, t_n$) (\syntax{}): 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} \(p\) (\(t_1, \ldots, t_n\)) (\syntax{}): 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{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{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$ +\> \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$. +\(\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 +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 +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 +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+\/+. @@ -1686,122 +1686,122 @@ 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$. +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)$ \\ +\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$ := $\mzninline{true}$;\\ -%\> \> \textbf{case} \texttt{false}: $b$ := $\mzninline{false}$;\\ -\> \> \textbf{case} $b'$ (\syntax{}): $S$ \cupp $\{\new b \half \neg b'\}$; \\ -\> \> \textbf{case} $t_1$ $r$ $t_2$ (\syntax{}): \\ -\> \> \> \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{switch} \(c\) \\ +%\> \> \textbf{case} \texttt{true}: \(b\) := \(\mzninline{true}\);\\ +%\> \> \textbf{case} \texttt{false}: \(b\) := \(\mzninline{false}\);\\ +\> \> \textbf{case} \(b'\) (\syntax{}): \(S\) \cupp \(\{\new b \half \neg b'\}\); \\ +\> \> \textbf{case} \(t_1\) \(r\) \(t_2\) (\syntax{}): \\ +\> \> \> \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\}$ \\ +\> \> \> \> \(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))\}$ +\> \> \> \> \(\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 (\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\): +\(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} \(c_1\) \verb+<->+ \(c_2\): +\(b\) := \(\flatc(\texttt{not}~c_1~\verb+<->+~c_2, \ctxt)\) \\ -\> \> \textbf{case} \texttt{forall(} $ba$ \texttt{)}: \\ -\> \> \> \textbf{let} $[c_1, \ldots, c_n] = \evalb(ba)$; \\ -\> \> \> \textbf{foreach}($j \in 1..n$) $b_j$ := $\halfnc(c_j, \posop \ctxt)$; \\ -\>\>\> $S$ \cupp $\{ \new b \half \bigvee_{j=1}^n b_j \}$ \\ -\>\> \textbf{case} \texttt{exists(} $ba$ \texttt{)}: \\ -\> \> \> \textbf{let} $[c_1, \ldots, c_n] = \evalb(ba)$; \\ -\> \> \> \textbf{foreach}($j \in 1..n$) $b_j$ := $\halfnc(c_j, \ctxt)$; \\ -\>\>\> $S$ \cupp $\{ \new b \half \bigwedge_{j=1}^n b_j \}$ \\ -\>\> \textbf{case} $[c_1, \ldots, c_n]$ \texttt{[} $t$ \texttt{]}: \\ -\>\>\> $b$ := $\flatc(\texttt{not}~[c_1, \ldots, c_n]~\texttt{[}~t~\texttt{]}, \ctxt)$ \\ +\> \> \textbf{case} \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$) (\syntax{}) built-in predicate: \\ -\> \> \> $b$ := $\flatc(\texttt{not}~p(t_1, \ldots, t_n), \ctxt)$ \\ -\>\> \textbf{case} $p$ ($t_1, \ldots, t_n$) (\syntax{}): 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)$ +\>\> \textbf{case} \(p\) (\(t_1, \ldots, t_n\)) (\syntax{}) built-in predicate: \\ +\> \> \> \(b\) := \(\flatc(\texttt{not}~p(t_1, \ldots, t_n), \ctxt)\) \\ +\>\> \textbf{case} \(p\) (\(t_1, \ldots, t_n\)) (\syntax{}): 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\}$ +\> \>\> \(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{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{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$ +\> \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{)}$. +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 +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 +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 +terms stores the variable \(h\) holding the results, the Boolean \(b'\) determining if the constraints arising from partial functions, and the previous context and bounds. If the previous context was root or the context are the same we examine the bounds. If they are the same we reuse the result, otherwise we set the -$\bnds$ to $\iboth$ and reflatten since we require both bounds (perhaps in -different situations). Otherwise the new context is $\rootc$ and the previous -$\pos$, we force $b'$ to be $\mzninline{true}$ in $S$, and then reuse the result if the -bounds are the same, or set $\bnds$ to $\iboth$ and reflatten. We store the +\(\bnds\) to \(\iboth\) and reflatten since we require both bounds (perhaps in +different situations). Otherwise the new context is \(\rootc\) and the previous +\(\pos\), we force \(b'\) to be \(\mzninline{true}\) in \(S\), and then reuse the result if the +bounds are the same, or set \(\bnds\) to \(\iboth\) and reflatten. We store the result found at the end of flattening, note that we only need one entry: context -can move from $\pos$ to $\rootc$ and bounds can move from one of $\iabove$ or -$\ibelow$ to $\iboth$. +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 @@ -1809,28 +1809,28 @@ 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 +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} } @@ -1843,129 +1843,129 @@ Array lookup is again simpler in half reification where we use half reified 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 +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$. +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$ \\ +\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'}$ +\> \> \> \(S\) \cupp \(\{ b' \}\) \\ +\> \> \> \textbf{if} (\(pbnds = \bnds\)) hhash[\(t\)] := \(\tuple{h,b',\rootc,\bnds}\); \textbf{return} \(\tuple{h,b'}\) \\ -\> \> \> \textbf{else} $\bnds$ := $\iboth$ \\ -\> \textbf{if} ($\fixed(t)$) $v$ := $\eval(t)$; $b$ := $\mzninline{true}$ \\ +\> \> \> \textbf{else} \(\bnds\) := \(\iboth\) \\ +\> \textbf{if} (\(\fixed(t)\)) \(v\) := \(\eval(t)\); \(b\) := \(\mzninline{true}\) \\ \> \textbf{else} %\\ -%% \> \> \textbf{if} ($t$ is marked \emph{total}) $\ctxt$ := $\rootc$ \\ +%% \> \> \textbf{if} (\(t\) is marked \emph{total}) \(\ctxt\) := \(\rootc\) \\ %\> \> -\textbf{switch} $t$ \\ -%\> \> \textbf{case} $i$ (\intc): $v$ := $i$; $b$ := $\mzninline{true}$ \\ -\> \> \textbf{case} $v'$ (\syntax{}): $v$ := $v'$; $b$ := $\mzninline{true}$\\ -\> \> \textbf{case} $t_1$ $a$ $t_2$ (\syntax{}): \\ -\> \> \> \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{switch} \(t\) \\ +%\> \> \textbf{case} \(i\) (\intc): \(v\) := \(i\); \(b\) := \(\mzninline{true}\) \\ +\> \> \textbf{case} \(v'\) (\syntax{}): \(v\) := \(v'\); \(b\) := \(\mzninline{true}\)\\ +\> \> \textbf{case} \(t_1\) \(a\) \(t_2\) (\syntax{}): \\ +\> \> \> \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)$; \\ +\(\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)$; \\ +\(\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{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{]}: \\ +\(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), +\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\} \}$ +%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{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), \} $ +\>\>\>\> \(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 \}$ \\ +\> \> \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$) +%\(\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{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{if} (\(eval(c_0)\)) \(\tuple{v,b}\) := \(\halft(t_1,\ctxt,\bnds)\) \textbf{else} +\(\tuple{v,b}\) := \(\halft(t_2,\ctxt,\bnds)\) \\ -\>\> \textbf{case} \texttt{bool2int(} $c_0$ \texttt{)}: \\ -\> \> \> \textbf{if} $(\bnds = \ibelow$) $b_0$ := $\halfc(c_0, \pos)$; \\ -\> \> \> \textbf{elseif} $(\bnds = \iabove$) $b'_0$ := $\halfnc(c_0, -\pos)$; $S$ \cupp $\{\new b_0 \full \neg b'_0\}$ \\ -\> \> \> \textbf{else} $b_0$ := $\flatc(c_0, \mix)$; \\ -\> \> \> $S$ \cupp $\{ \texttt{bool2int}(b_0, \new v), \new b \}$ \\ +\>\> \textbf{case} \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$) (\syntax{}): 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} \(f\) (\(t_1, \ldots, t_n\)) (\syntax{}): 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{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}$ +\> \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 +% Half reification of terms returns a set of constraints that enforce \(v = t\) if +% the term \(t\) is safe, and \(b \half v = t\) otherwise. The most complex case is +% \texttt{bool2int}\((c_1)\), which half-reifies \(c_1\) if it is in a positive +% context, negates \(c_1\) and half-reifies the result if \(c_1\) is safe and in a % negative context, and uses full flattening otherwise. \begin{example}\label{ex:hr-half} @@ -2008,11 +2008,11 @@ $S$ \cupp $\{ \new b \half (b_1 \wedge b_2)\}$ 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!} + 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 + 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; @@ -2037,118 +2037,118 @@ $S$ \cupp $\{ \new b \half (b_1 \wedge b_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 +transformation will construct many implications of the form \(b \half b'\), note +that the constraint \(b \half b_1 \wedge \cdots \wedge b_n\) is equivalent to +\(b \half b_1, b \half b_2, \ldots, b \half b_n\). Just as in \cref{ex:hr-half} above we can simplify the result of half reification. For -each $b'$ which appears only on the right of one constraint of the form -$b \half b'$ and other constraints of the form $b' \half c_i$ we remove the -first constraint and replace the others by $b \half c_i$. +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 +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 ( \{ \mzninline{false} \} \cup f_{b \full c}(D)(b)) \\ f_{b \half c}(D)(v) & = & D(v) & \texttt{if}~v \in vars(c),~\mzninline{false} \in D(b) \\ f_{b \half c}(D)(v) & = & f_{b \full c}(D)(v) & \texttt{if}~v \in vars(c),~\text{otherwise} \end{array} -$$ +\] and -$$ +\[ \begin{array}{rcll} f_{b' \half \neg c}(D)(b') & = & D(b') & \texttt{if}~\{ \mzninline{false} \} \in f_{b \full c}(D)(b) \\ f_{b' \half \neg c}(D)(b') & = & D(b') \cap \{ \mzninline{false}\} & \text{otherwise}\\ f_{b' \half \neg c}(D)(v) & = & D(v) & \texttt{if}~v \in vars(c),~\mzninline{false} \in D(b') \\ f_{b' \half \neg c}(D)(v) & = & f_{b \full c}(D)(v) & \texttt{if}~v \in vars(c),~\text{otherwise} \end{array} -$$ +\] These definitions are not meant describe implementations, only to define how the half reified split versions of the propagator should act. In order to prove the same behaviour of the split reification versions we must -assume that $f_{b \full c}$ is \emph{reified-consistent} which is defined as -follows: suppose $f_{b \full c}(D)(v) \neq D(v), v \not\equiv b$, then -$f_{b \full c}(D)(b) \neq \{ \mzninline{false}, \mzninline{true}\}$. That is if the propagator ever +assume that \(f_{b \full c}\) is \emph{reified-consistent} which is defined as +follows: suppose \(f_{b \full c}(D)(v) \neq D(v), v \not\equiv b\), then +\(f_{b \full c}(D)(b) \neq \{ \mzninline{false}, \mzninline{true}\}\). That is if the propagator ever reduces the domain of some variable, then it must also fix the Boolean variable -$b$. This is sensible since if $b$ is not fixed then every possible value of $v$ -is consistent with constraint $b \full c$ regardless of the domain $D$. This is +\(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 +\(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)$, +% \(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)$ +% \(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)$. +% \(\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 \(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$. +% \(D'' = \solv(\{ f_{b \half c}, f_{b' \half \neg c}, f_{b' \full \neg b}\}, D)\). +% The proof is by cases of \(D\). -% \textbf{(a)} Suppose $D(b) = \{\mzninline{true},\mzninline{false}\}$. \textbf{(a-i)} Suppose -% $f_{b \full c}(D) = D$. Then clearly $f_{b \half c}(D) = D$ by definition, and -% similarly $f_{b' \half \neg c}(D) = D$. Hence $D_1 = D_2 = D$. Note that since -% $f_{b \full c}$ is reified consistent, then $f_{b \full c}(D) \neq D$ implies -% that $f_{b \full c}(D)(b) \neq \{ \mzninline{false}, \mzninline{true} \}$. \textbf{(a-ii)} Suppose -% $f_{b \full c}(D)(b) = \{ \mzninline{true} \}$. Let $D_1 = f_{b' \half \neg c}(D)$, then -% $D_1(b') = \{ \mzninline{false} \}$ by definition and $D_1(v) = D(v), v \not\equiv b'$. -% Let $D_2 = f_{b' \full \neg b}(D_1)$ then $D_2(b)= \{ \mzninline{true} \}$ and -% $D_2(v) = D(v), v \not\in \{b,b'\}$. Then -% $D_3 = f_{b \half c}(D_2) = f_{b \full c}(D_2)$ by definition, and by -% idempotence of $f_{b \full c}$ and since $D_2$ and $D$ differ only on $b$ and -% $b'$ this is a fixpoint of $f_{b \full c}$ and -% $D_3(v) = f_{b \full c}(D)(v), v \not \equiv b'$. $D_3$ is also a fixpoint of -% $f_{b \half c}$, $f_{b' \full \neg b}$ and $f_{b' \half \neg c}$ and hence -% $D'' = D_3$. But also $D' = f_{b' \full \neg b}(f_{b \full c}(D)) = D_3$ since -% $D_3$ and $f_{b \full c}(D)$ only differ on $b'$. \textbf{(a-iii)} Suppose -% $f_{b \full c}(D)(b) = \{ \mzninline{false} \}$. Let $D_1 = f_{b \half c}(D)$, then -% $D_1(b) = \{ \mzninline{false} \}$ by definition and $D_1(v) = D(v), v \not\equiv b$. Let -% $D_2 = f_{b' \full \neg b}(D_1)$ then $D_2(b')= \{ \mzninline{true} \}$ and -% $D_2(v) = D(v), v \not\in \{b,b'\}$. Then -% $D_3 = f_{b' \half \neg c}(D_2) = f_{b \full c}(D_2)$ by definition, and by -% idempotence of $f_{b \full c}$ and since $D_2$ and $D$ differ only on $b$ and -% $b'$ this is a fixpoint for $f_{b \half c}$, $f_{b' \full \neg b}$ and -% $f_{b' \half \neg c}$ and hence $D'' = D_3$. But also -% $D' = f_{b' \full \neg b}(f_{b \full c}(D)) = D_3$ since $D_3$ and -% $f_{b \full c}(D)$ only differ on $b'$. +% \textbf{(a)} Suppose \(D(b) = \{\mzninline{true},\mzninline{false}\}\). \textbf{(a-i)} Suppose +% \(f_{b \full c}(D) = D\). Then clearly \(f_{b \half c}(D) = D\) by definition, and +% similarly \(f_{b' \half \neg c}(D) = D\). Hence \(D_1 = D_2 = D\). Note that since +% \(f_{b \full c}\) is reified consistent, then \(f_{b \full c}(D) \neq D\) implies +% that \(f_{b \full c}(D)(b) \neq \{ \mzninline{false}, \mzninline{true} \}\). \textbf{(a-ii)} Suppose +% \(f_{b \full c}(D)(b) = \{ \mzninline{true} \}\). Let \(D_1 = f_{b' \half \neg c}(D)\), then +% \(D_1(b') = \{ \mzninline{false} \}\) by definition and \(D_1(v) = D(v), v \not\equiv b'\). +% Let \(D_2 = f_{b' \full \neg b}(D_1)\) then \(D_2(b)= \{ \mzninline{true} \}\) and +% \(D_2(v) = D(v), v \not\in \{b,b'\}\). Then +% \(D_3 = f_{b \half c}(D_2) = f_{b \full c}(D_2)\) by definition, and by +% idempotence of \(f_{b \full c}\) and since \(D_2\) and \(D\) differ only on \(b\) and +% \(b'\) this is a fixpoint of \(f_{b \full c}\) and +% \(D_3(v) = f_{b \full c}(D)(v), v \not \equiv b'\). \(D_3\) is also a fixpoint of +% \(f_{b \half c}\), \(f_{b' \full \neg b}\) and \(f_{b' \half \neg c}\) and hence +% \(D'' = D_3\). But also \(D' = f_{b' \full \neg b}(f_{b \full c}(D)) = D_3\) since +% \(D_3\) and \(f_{b \full c}(D)\) only differ on \(b'\). \textbf{(a-iii)} Suppose +% \(f_{b \full c}(D)(b) = \{ \mzninline{false} \}\). Let \(D_1 = f_{b \half c}(D)\), then +% \(D_1(b) = \{ \mzninline{false} \}\) by definition and \(D_1(v) = D(v), v \not\equiv b\). Let +% \(D_2 = f_{b' \full \neg b}(D_1)\) then \(D_2(b')= \{ \mzninline{true} \}\) and +% \(D_2(v) = D(v), v \not\in \{b,b'\}\). Then +% \(D_3 = f_{b' \half \neg c}(D_2) = f_{b \full c}(D_2)\) by definition, and by +% idempotence of \(f_{b \full c}\) and since \(D_2\) and \(D\) differ only on \(b\) and +% \(b'\) this is a fixpoint for \(f_{b \half c}\), \(f_{b' \full \neg b}\) and +% \(f_{b' \half \neg c}\) and hence \(D'' = D_3\). But also +% \(D' = f_{b' \full \neg b}(f_{b \full c}(D)) = D_3\) since \(D_3\) and +% \(f_{b \full c}(D)\) only differ on \(b'\). -% \textbf{(b)} If $D(b) = \{\mzninline{true}\}$ then clearly $f_{b \full c}$ and -% $f_{b \half c}$ act identically on variables in $vars(c)$. +% \textbf{(b)} If \(D(b) = \{\mzninline{true}\}\) then clearly \(f_{b \full c}\) and +% \(f_{b \half c}\) act identically on variables in \(vars(c)\). -% \textbf{(c)} If $D(b) = \{\mzninline{false}\}$ then $D(b') = \{\mzninline{true}\}$ and clearly -% $f_{b \full c}$ and $f_{b' \half \neg c}$ act identically on variables in -% $vars(c)$. \qed +% \textbf{(c)} If \(D(b) = \{\mzninline{false}\}\) then \(D(b') = \{\mzninline{true}\}\) and clearly +% \(f_{b \full c}\) and \(f_{b' \half \neg c}\) act identically on variables in +% \(vars(c)\). \qed % \end{proof} The reason for the generality of the above theorem which defines the @@ -2156,14 +2156,14 @@ 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 +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$ +% 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 +% propagators for \(b \half c\), \(b \full \neg b'\), \(b' \half \neg c\). \qed % \end{corollary} @@ -2179,12 +2179,12 @@ 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 +\(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 +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 +\(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. @@ -2263,14 +2263,14 @@ 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\}$ \\ + \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} @@ -2372,7 +2372,7 @@ determining a prize collecting path, a simplified form of prize collecting travelling salesman problem \autocite{balas-1989-pctsp}, %shown in \cref{fig:hr-pct} where the aim is define an acyclic path from node 1 along weighted edges to -collect the most weight. Not every node needs to be visited ($pos[i] = 0$). +collect the most weight. Not every node needs to be visited (\(pos[i] = 0\)). \begin{mzn} int: n; % size @@ -2397,7 +2397,7 @@ It uses the global constraint \mzninline{alldifferent_except_0} which constrains each element in the \mzninline{next} array to be different or equal 0. The model has one unsafe array lookup \mzninline{pos[next[i]]}. We compare using full reification (\textsf{full}) and half reification (\textsf{half}) to model this -problem. Note that if we extend the $pos$ array to have domain $0..n$ then the +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}