More work on automatic analysis

assets/shorthands.tex

@@ -32,6 +32,7 @@
 \newcommand{\posc}{\textit{pos}}
 \newcommand{\negc}{\textit{neg}}
 \newcommand{\mixc}{\textit{mix}}
+\newcommand{\mayberootc}{\textit{root?}}
 \newcommand{\changepos}{\ensuremath{+}}
 \newcommand{\changeneg}{\ensuremath{-}}
 

chapters/4_half_reif.tex

@@ -327,7 +327,10 @@ If a function argument is not annotated, then the argument is evaluated in \mixc
 	Consider the following user-defined \minizinc\ implementation of a logical implication.
 
 	\begin{mzn}
-		predicate impli(var bool: x ::promise_ctx_antitone, var bool: y ::promise_ctx_monotone) =
+		predicate impli(
+			var bool: x ::promise_ctx_antitone,
+			var bool: y ::promise_ctx_monotone
+		) =
 			not x \/ y;
 	\end{mzn}
 
@@ -462,7 +465,7 @@ The right hand expression of the item is then evaluated in the resulting context
 \begin{figure*}
 	\begin{center}
 		\begin{tabular}{r | c c c c}
-			join	& \rootc & \posc & \negc & \mixc \\
+			join & \rootc & \posc & \negc & \mixc \\
 			\hline
 			\rootc & \rootc & \rootc & \rootc & \rootc \\ 
 			\posc & \rootc & \posc & \mixc & \mixc \\ 
@@ -473,10 +476,96 @@ The right hand expression of the item is then evaluated in the resulting context
 	\caption{\label{fig:half-join} A table showing the result of joining two contexts.}
 \end{figure*}
 
+(TupC) and (TupD) handle the context inference during the construction and destructuring of tuples respectively.
+The context of the individual members of tuples is tracked separately.
+This means that individual members of a tuple, like the value and the partiality of a \minizinc{} expression, may be evaluated in different contexts.
+
+Finally, the (Decl) and (Item0) rules describe two base cases in the inference.
+The declaration item of a \variable{} does not further the context, and does not depend on it.
+It merely triggers the creation of a new \variable{}.
+The (Item0) rule is triggered when there are no more inner items in the let-expression.
 
 \subsection{Potentially \rootc{}}%
 \label{subsec:half-?root}
 
+In the previous section, we briefly discussed the context transformations for the (Access) and (ITE) rules in \cref{fig:half-analysis-expr}.
+Different from the rules described, when an array access or if-then-else expression is found in \rootc{} context, it often makes sense to evaluate its sub-expression in \rootc context as well.
+It is, however, not always safe to do so.
+
+\begin{example}
+\label{ex:half-maybe-root}
+
+	For example, consider the following \microzinc{} fragment.
+
+	\begin{mzn}
+		constraint if b then F(x, y, z) else G(x, y, z) endif;
+	\end{mzn}
+
+	In this case, since only one side of the if-then-else expression is evaluated, the compiler can output calls to the \rootc{} variant of the functions.
+	This will enforce the constraint in the most efficient way.
+
+	Things, however, change when the situation gets more complex.
+	Consider the following \microzinc{} fragment.
+
+	\begin{mzn}
+		let {
+			var bool: p = F(x, y, z);
+			var bool: q = G(x, y, z);
+			constraint if b then p else q endif;
+			var bool: ret = bool_or(p, r);
+		} in ret;
+	\end{mzn}
+
+	One side of the if-then-else expression is not also used in a disjunction.
+	If \mzninline{b} evaluates to \mzninline{true}, then \mzninline{p} is evaluated in \rootc{} context, and \mzninline{p} can take the value \mzninline{true} in the disjunction.
+	Otherwise, \mzninline{q} is evaluated in \rootc{} context, and \mzninline{p} in the disjunction must be evaluated in \posc{} context.
+	It is, therefore, not safe to assume that all sides of the if-then-else expressions are evaluated in \rootc{} context.
+\end{example}
+
+Using the \changepos{} transformation for sub-expression contexts is safe, but it might place a large burden on the \solver{}.
+The solver is likely to perform better when the direct constraint predicate is used.
+
+To detect situation where the sub-expression are only used in an array access or if-then-else expression we introduce the \mayberootc{} context.
+This context functions as a \emph{weak} \rootc{} context.
+If it is joined with any other context, then it acts as \posc{}.
+The extended join operation is shown in \cref{fig:half-maybe-join}.
+Otherwise, it will act as a normal \rootc{} context.
+
+\begin{figure*}
+	\begin{center}
+		\begin{tabular}{r | c c c c c}
+			join & \rootc & \mayberootc & \posc & \negc & \mixc \\
+			\hline
+			\rootc & \rootc & \rootc & \rootc & \rootc & \rootc \\ 
+			\mayberootc & \rootc & \mayberootc & \posc & \mixc & \mixc \\ 
+			\posc & \rootc & \posc & \posc & \mixc & \mixc \\ 
+			\negc & \rootc & \mixc & \mixc & \negc & \mixc \\ 
+			\mixc & \rootc & \mixc & \mixc & \mixc & \mixc \\ 
+		\end{tabular}
+	\end{center}
+	\caption{\label{fig:half-maybe-join} The join context operation extended with \mayberootc{}.}
+\end{figure*}
+
+\begin{figure*}
+  \centering
+  \begin{prooftree}
+		\hypo{\ctxeval{x\texttt{[}i\texttt{]}}{\rootc}}
+		\infer1[(Access-R)]{\ctxeval{x}{\mayberootc}}
+  \end{prooftree} \\
+  \bigskip
+  \begin{prooftree}
+		\hypo{\ctxeval{\texttt{if }b\texttt{ then } e_{1} \texttt{ else } e_{2} \texttt{ endif}}{\rootc}}
+		\infer1[(ITE-R)]{\ctxeval{e_{1}}{\mayberootc},~\ctxeval{e_{2}}{\mayberootc}}
+  \end{prooftree}
+	\caption{\label{fig:half-analysis-maybe-root} Updated context inference rules for \mayberootc{}.}
+\end{figure*}
+
+\Cref{fig:half-analysis-maybe-root} shows the additional inference rules for array access and if-then-else expressions.
+Looking back at \cref{ex:half-maybe-root}, these additional rules and updated join operation will ensure that the first case will correctly use \rootc{} context calls.
+For the second case, however, it detects that \mzninline{p} is used in both \posc{} and \mayberootc{} context.
+Therefore, it will output the \posc{} call for the right hand side of \mzninline{p}, even when \mzninline{b} evaluates to \mzninline{true}.
+At compile time, this is only correct context to use.
+We will, however, discuss the dynamically adjusting of contexts during flattening in \cref{subsec:half-dyn-context}.
 
 \section{Flattening and Half Reification}%
 \label{sec:half-flattening}
@@ -540,6 +629,9 @@ Moreover, this mechanism also allows us to detect when an expression and its neg
 This is simple way to detect conflicts between \constraints{} and, by extend, prove that the constraint model is unsatisfiable.
 Clearly, a \constraint{} and its negation cannot both hold at the same time.
 
+\subsection{Dynamic Context Switching}%
+\label{subsec:half-dyn-context}
+
 \subsection{Chain compression}%
 \label{subsec:half-compress}