Dekker1/dekker-phd-thesis
Archived
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Work on the automatic HR analysis

Browse Source
This commit is contained in:
Jip J. Dekker 2021-06-07 12:09:00 +10:00
parent 953f3c8735
commit 2af1fe99a0
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
3 changed files with 287 additions and 31 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
assets/shorthands.tex
View File

@ -35,4 +35,9 @@
\newcommand{\changepos}{\ensuremath{+}}
\newcommand{\changeneg}{\ensuremath{-}}
% -- Analysis shorthands
\newcommand{\ctxeval}[2]{\ensuremath{\mathbb{M}\left(#2\right)\left\|~#1~\right\|}}
\newcommand{\ctxfunc}[2]{\ensuremath{\mathbb{F}\left(#2\right)\left\|~#1~\right\|}}
\newcommand{\ctxitem}[1]{\ensuremath{\mathbb{m}\left\|~#1~\right\|}}
\newcommand{\undefined}{\ensuremath{\bot}}

2
chapters/3_rewriting.tex
View File

@ -432,7 +432,7 @@ suitable alpha renaming.
\end{figure*}
The rules in \cref{fig:4-rewrite-to-nzn-calls} handle function calls. The first
rule (Call) evaluates a function call expression in the context of a \microzinc\
rule, (Call), evaluates a function call expression in the context of a \microzinc\
program \(\Prog{}\) and \nanozinc\ program \(\Env{}\). The rule evaluates the
function body \(\ptinline{E}\) where the formal parameters \(p_{i}\) are
substituted by the call arguments \(a_{i}\).\footnote{We use

275
chapters/4_half_reif.tex
View File

@ -2,6 +2,12 @@
\chapter{Half Reification}\label{ch:half-reif}
%************************************************
\noindent{}In this chapter we investigate the notion of \gls{half-reif} as introduced by Feydy et al.\ \autocite*{feydy-2011-half-reif}.
We show that in modern \gls{cp} still benefit from the use of half-reified propagators.
We also discuss the advantages of the use of \gls{half-reif} when writing decompositions and introduce a new version of the linearisation library that enjoys these advantages.
We introduce methods to automatically detect when a expression in a \minizinc\ model can be half-reified, enabling the modellers to enjoy the advantages of half-reification without having to introduce them manually.
Finally, we discuss the effect of half-reification on earlier discussed flattening methods.
\section{Introduction to Half Reification}
The complex expressions language used in \cmls{}, such as \minizinc{}, often require the use of \gls{reification} in the flattening process to reach a solver level constraint model.
@ -192,7 +198,8 @@ Only full \gls{reification} can be used for expressions in that are in this cont
This occurs, for example, when using an exclusive or expression in a constraint.
The value that one side must take directly depends on the value that the other side takes.
Each side can thus be forced to be true or false.
The \mixc{} context can also be used as a ``fall back'' context; if it cannot be determined if an expression is in a \posc{} or \negc{} context, then it is always safe to say the expression is in a \mixc{} context.
The \mixc{} context can also be used as a ``fall back'' context.
If it cannot be determined if an expression is in a \posc{} or \negc{} context, then it is always safe to say the expression is in a \mixc{} context.
When taking into account the possible undefinedness of an expression, every expression in a \minizinc{} model has two different contexts: the context in which the expression itself occurs, its \emph{value context}, and the context in which the partiality of the expression is captured, its \emph{partiality context}.
As described in \cref{subsec:back-mzn-partial}, \minizinc{} uses relational semantics of partial values.
@ -200,9 +207,46 @@ This means that if a function does not have a result, then its nearest enclosing
In practice, this means that a condition that tests if the function will return a value is added to the nearest enclosing Boolean expression.
The \emph{partiality} context is the context in which this condition is placed.
We now specify two context transformations that will be used in further algorithms to transition between different contexts: \changepos{} and \changeneg{}.
The transformations have the following behaviour:
The context of an expression cannot always be determined by merely considering \minizinc\ expressions top-down.
Expressions bound to a variable can be used multiple times in expressions that influence their context.
\begin{example}
Consider the following \minizinc\ fragment.
\begin{mzn}
constraint let {
var bool: x = pred(a, b, c);
} in y -> x /\ x -> z;
\end{mzn}
The predicate call \mzninline{pred(a, b, c)} is bound to the variable \mzninline{x}.
The call is in \posc\ context, and can be half-reified, if the variable \mzninline{x} is only used in \posc{} context.
Although this is the case in the left side of the conjunction, the other side uses \mzninline{x} in a \negc{} context.
This means that \mzninline{pred(a, b, c)} is in a \mixc{} context, and must fully reified.
\end{example}
Note that an alternative approach for this example would be to replace the identifier with its definition.
It would then be possible half-reify the call and the negation of the call.
Although this would increase the use of \gls{half-reif}, it should be noted that the propagation of these two \glspl{half-reif} would be equivalent to propagating the full \gls{reification} of the call.
In this scenario, we prefer to create the full \gls{reification} as it decreases the number of \variables{} and \constraint{} in the model.
\subsection{Automated analysis}%
\label{subsec:half-automated}
In the architecture introduced in \cref{ch:rewriting}, contexts of the expressions can be determined automatically.
The analysis is best performed during the compilation process from \minizinc{} to \microzinc{}, instead of during the \microzinc{} interpretation, since it requires knowledge about all usages of certain \variable{} at the same time.
Without loss of generality we can define the context analysis process for \microzinc{} models.
This has the advantage that the value and partiality have already been explicitly separated and no longer requires special handling.
We describe the context analysis performed on the \microzinc{} syntax in the form of inference rules.
The full set of rules appears in \cref{fig:half-analysis-expr,fig:half-analysis-it}.
Each rules describe how an expression is found in a context \(ctx\), above the line, changes the context of subordinate expressions, below the line.
The syntax \ctxeval{e}{ctx} is used to assert that the expression \(e\) is evaluated in the context \(ctx\).
We now specify two context transformations that will be used in further algorithms to transition between different contexts: \changepos{} and \changeneg{}.
The behaviour of these transformations is shown in \cref{fig:half-ctx-trans}.
\begin{figure*}
\begin{center}
\begin{tabular}{ccc}
\(
\begin{array}{lcl}
@ -222,8 +266,217 @@ The transformations have the following behaviour:
\end{array}
\)
\end{tabular}
\end{center}
\caption{\label{fig:half-ctx-trans} Definitions of the \changepos{} and \changeneg{} context transitions.}
\end{figure*}
\begin{figure*}
\centering
\begin{prooftree}
\hypo{\ctxeval{x}{ctx}}
\infer1[(Ident)]{\text{pushCtx}(x, ctx)}
\end{prooftree} \\
\bigskip
\begin{prooftree}
\hypo{\ctxeval{ident\texttt{(} e_{1}, \ldots, e_{n} \texttt{)}}{ctx}}
\hypo{\text{argCtx}(ident, ctx) = \tuple{ ctx'_{1}, \ldots, ctx'_{n}}}
\infer2[(Call)]{\ctxfunc{ident}{ctx},~\ctxeval{e_{1}}{ctx'_{1}},~\ldots,~ \ctxeval{e_{n}}{ctx'_{n}}}
\end{prooftree} \\
\bigskip
\begin{prooftree}
\hypo{\ctxeval{x\texttt{[}i\texttt{]}}{ctx}}
\infer1[(Access)]{\ctxeval{x}{\changepos{}ctx}}
\end{prooftree} \\
\bigskip
\begin{prooftree}
\hypo{\ctxeval{\texttt{if }b\texttt{ then } e_{1} \texttt{ else } e_{2} \texttt{ endif}}{ctx}}
\infer1[(ITE)]{\ctxeval{e_{1}}{\changepos{}ctx},~\ctxeval{e_{2}}{\changepos{}ctx}}
\end{prooftree} \\
\bigskip
\begin{prooftree}
\hypo{\ctxeval{\texttt{[}e~\texttt{|}~G\texttt{]}}{ctx}}
\infer1[(Compr)]{\ctxeval{e}{ctx}}
\end{prooftree} \\
\bigskip
\begin{prooftree}
\hypo{\ctxeval{\texttt{[}e_{1}, \ldots, e_{n}\texttt{]}}{ctx}}
\infer1[(Arr)]{\ctxeval{e_{1}}{ctx}, \ldots, \ctxeval{e_{n}}{ctx}}
\end{prooftree}
\caption{\label{fig:half-analysis-expr} Context inference rules for \microzinc\ expressions.}
\end{figure*}
\Cref{fig:half-analysis-expr} shows the inference rules for all \microzinc{} expressions, apart from let expressions.
The first rule, (Ident), is unique in the sense that the context of an identifier does not directly affects any sub-expressions.
Instead every context in which the identifier are found are collected and will be processed when evaluating the corresponding declaration.
Note that the presented inference rules do not have any explicit state object.
Instead, we introduce the functions ``pushCtx'' and ``collectCtx''.
These functions track and combine the contexts in which an value is used in an implicit global state.
Most changes in the context of \microzinc{} expressions stem from the consequent (Call) rule.
A call expression can change the context in which its arguments should be evaluated.
As an input to the inference process, a ``argCtx'' function is used to give the context of the arguments of a function, given the function itself and the context of the call.
A definition for this function for the \minizinc\ operators can be found in \cref{alg:arg-ctx}.\footnote{We use \minizinc\ operator syntax instead of \microzinc{} identifiers for brevity and clarity.}
Although a standard definition for the ``argMax'' function may cover the most common cases, it does not cover user-defined functions stemming from \minizinc{}.
To address this issue, we introduce the \minizinc{} annotations \mzninline{promise_ctx_monotone} and \mzninline{promise_ctx_antitone} to represent the operations \changepos{} and \changeneg{} respectively.
When a function argument is annotated with one of these annotations, the context of the argument in a call in context \(ctx\) is transformed with the operation coressponding to the annotation (\eg\ \(\changepos{}ctx\) or \(\changeneg{}ctx\)).
If a function argument is not annotated, then the argument is evaluated in \mixc context.
\begin{example}
Consider the following user-defined \minizinc\ implementation of a logical implication.
\begin{mzn}
predicate impli(var bool: x ::promise_ctx_antitone, var bool: y ::promise_ctx_monotone) =
not x \/ y;
\end{mzn}
The annotations placed on the argument of the \mzninline{impli} function will apply the same context transformations as a direct \minizinc\ implication, as shown in \cref{alg:arg-ctx}.
In term of context analysis, this function now is equivalent to the \minizinc implication operator.
\end{example}
\begin{algorithm}
\KwData{A \minizinc\ operator \(op\) and calling context \(ctx\)}
\KwResult{A tuple containing the contexts of the arguments \(\tuple{ctx_{1}, \ldots{}, ctx_{n}}\)}
\Switch{op}{
\Case{\mzninline{ not }}{
\Return{\tuple{\changeneg{}ctx}}
}
\Case{\mzninline{ \/ }, \mzninline{+ }}{
\Return{\tuple{\changepos{}ctx, \changepos{}ctx}}
}
\Case{\mzninline{ -> }, \mzninline{< }, \mzninline{<= }}{
\Return{\tuple{\changeneg{}ctx, \changepos{}ctx}}
}
\Case{\mzninline{ > }, \mzninline{>= }, \mzninline{- }}{
\Return{\tuple{\changepos{}ctx, \changeneg{}ctx}}
}
\Case{\mzninline{ <-> }, \mzninline{xor }, \mzninline{* }}{
\Return{\tuple{\mixc, \mixc}}
}
\Case{\mzninline{ /\ }}{
\Return{\tuple{ctx, ctx}}
}
\Other{
\Return{\tuple{\mixc, \ldots, \mixc}}
}
}
\caption{\label{alg:arg-ctx} Definition of the \emph{argCtx} function for \minizinc\ operators.}
\end{algorithm}
The context in which the result of a call expression is used must also be considered.
The (Call) rule, therefore, introduces the \ctxfunc{ident}{ctx} syntax.
This syntax is used to declare that the compiler must introduce a \microzinc\ function variant that flattens the function call to \(ident\) in the context \(ctx\).
This means that if \(ctx\) is \rootc{}, the compiler can use the the function as defined.
Otherwise, the compiler follows the following steps to try to introduce the most compatible variant of the function:
\begin{enumerate}
\item If a direct definition for \(ctx\) definition exists, then use this definition.
\begin{description}
\item[\posc] \glspl{half-reif} can be defined as \(ident\)\mzninline{_imp}.
\item[\negc] negations of \glspl{half-reif} can be defined as \(ident\)\mzninline{_imp_neg}.
\item[\mixc] \glspl{reification} can be defined as \(ident\)\mzninline{_reif}.
\end{description}
\item If \(ident\) is a \microzinc{} function with an expression body \(E\), then copy of the function can be made that is evaluated in the desired context:\ctxeval{E}{ctx}.
\item If \(ctx\) is \posc{} or \negc{}, then change \(ctx\) to \mixc{} and return to step 1.
\item Finally, if non of the earlier steps were successful, then the compilation fails.
Note that this can only occurr when a solver-level predicate does not have an \gls{reification}.
\end{enumerate}
The (Access) and (ITE) rules show the context inference for array access and if-then-else expressions respectively.
Their inner expressions are evaluated in \(\changepos{}ctx\).
The inner expressions cannot be simply be evaluated in \(ctx\), because it is not yet certain which expression will be chosen.
This is important for when \(ctx\) is \rootc{}, since we, at compile time, say which expression will hold globally.
We will revisit this issue in \cref{subsec:half-?root}.
Finally, the (Compr) and (Arr) rules show simple inference rules for array construction expressions.
If such an expression is evaluated in the context \(ctx\), then its members can be evaluated in the same context \(ctx\).
\begin{figure*}
\centering
\begin{prooftree}
\hypo{\ctxeval{\texttt{let \{ }I\texttt{ \} in } e}{ctx}}
\infer1[(Let)]{\ctxeval{e}{ctx}, \ctxitem{I} }
\end{prooftree} \\
\bigskip
\begin{prooftree}
\hypo{\ctxitem{I \texttt{; constraint } e }}
\infer1[(Con)]{\ctxeval{e}{\rootc},~\ctxitem{I}}
\end{prooftree} \\
\bigskip
\begin{prooftree}
\hypo{\ctxitem{I \texttt{; } T: x \texttt{ = } e }}
\hypo{\text{collectCtx}(x) = [ctx_{1}, \ldots, ctx_{n}]}
\infer2[(Assign)]{\ctxeval{x}{\text{join}([ctx_{1}, \ldots, ctx_{n}])},~\ctxitem{I}}
\end{prooftree} \\
\bigskip
\begin{prooftree}
\hypo{\ctxitem{I \texttt{; } \texttt{tuple(}\ldots\texttt{):}~x \texttt{ = (} e_{1}, \ldots, e_{n}\texttt{)}}}
\hypo{\text{collectCtx}(x) = \tuple{ctx_{1}, \ldots, ctx_{n}}}
\infer2[(TupC)]{\ctxeval{e_{1}}{ctx_{1}}, \ldots, \ctxeval{e_{n}}{ctx_{n}}, ~\ctxitem{I}}
\end{prooftree} \\
\bigskip
\begin{prooftree}
\hypo{\ctxitem{I \texttt{; (} T_{1}: x_{1}, \ldots, T_{n}: x_{n} \texttt{) = } e }}
\infer[no rule]1{\text{collectCtx}(x_{1}) = [ctx^{1}_{1}, \ldots, ctx^{1}_{k}], \ldots, \text{collectCtx}(x_{n}) = [ctx^{n}_{1}, \ldots, ctx^{n}_{l}]}
\infer1[(TupD)]{\ctxeval{e}{\tuple{\text{join}\left(\left[ctx^{1}_{1}, \ldots, ctx^{1}_{k}\right]\right), \ldots, \text{join}\left(\left[ctx^{n}_{1}, \ldots, ctx^{n}_{l}\right]\right)}},~\ctxitem{I}}
\end{prooftree} \\
\bigskip
\begin{prooftree}
\hypo{\ctxitem{I \texttt{; } T: x}}
\infer1[(Decl)]{}
\end{prooftree} \\
\bigskip
\begin{prooftree}
\hypo{\ctxitem{\epsilon{}}}
\infer1[(Item0)]{}
\end{prooftree}
\caption{\label{fig:half-analysis-it} Context inference rules for \microzinc\ let-expressions.}
\end{figure*}
\Cref{fig:half-analysis-it} shows the inference rules for let expressions and their inner items.
The first rule, (Let), propagates the context in which the expression is evaluated, \(ctx\), directly to the \mzninline{in}-expression.
Thereafter, the analysis will continue by iterating over its inner items.
This is described using the newly introduced syntax \ctxitem{I}.
Note that the \(ctx\) of the let-expression itself, is irrelevant for the analysis of its inner items.
The inference for \constraint{} items is described by the (Con) rule.
Since \microzinc{} implements strict semantics, the \constraint{} can be assumed to hold globally.
And, unlike \minizinc{}, the \constraint{} is not dependent on the context of the let-expression.
The \constraint{}'s expression is evaluated in \rootc context.
The (Assign) rule reasons about declarations that have a right hand side.
The expression that is assigned to the identifier must evaluated in the combined context of its usages.
As previously discussed, the contexts in which the identifier was used can be retrieved using the ``collectCtx'' function.
These contexts are then combined using a ``join'' function.
This function repeatedly applies the symmetric join operation described by \cref{fig:half-join}.
The right hand expression of the item is then evaluated in the resulting context.
\begin{figure*}
\begin{center}
\begin{tabular}{r | c c c c}
join & \rootc & \posc & \negc & \mixc \\
\hline
\rootc & \rootc & \rootc & \rootc & \rootc \\
\posc & \rootc & \posc & \mixc & \mixc \\
\negc & \rootc & \mixc & \negc & \mixc \\
\mixc & \rootc & \mixc & \mixc & \mixc \\
\end{tabular}
\end{center}
\caption{\label{fig:half-join} A table showing the result of joining two contexts.}
\end{figure*}
\subsection{Potentially \rootc{}}%
\label{subsec:half-?root}
\jip{TODO:\ Insert algorithm that attaches the context to the different expressions}
\section{Flattening and Half Reification}%
\label{sec:half-flattening}
@ -269,22 +522,20 @@ When considering these compatibility rules, the result of flattening would be hi
It would always be better to encounter the expression in a context that results in a reusable expression, \eg{} \mixc{}, before seeing the same expression in another context, \eg{} \posc{}.
This avoids creating both a full \gls{reification} and a \gls{half-reif} of the same expression.
In the \microzinc{} interpreter, this problem is resolved by only keeping the result of the \emph{most compatible} context.
If an expression is found another time in another context that is compatible with more contexts, then only the result of evaluating this context is kept in the \gls{cse} table.
Every usage of the less compatible, is replaced by the newly created version.
In the \microzinc{} interpreter, this problem is resolved by only keeping the result of their \emph{joint} context.
The context recorded in the \gls{cse} table and the found context are joint using the join operator, as described in \cref{fig:half-join}.
If this context is different from the recorded context, then the expression is re-evaluated in the joint context and its result kept in the \gls{cse} table.
All usages of the previously recorded result is replaced by the new result.
Because of dependency tracking of the constraints that define variables, we can be sure that all \variables{} and \constraints{} created in defining the earlier version are correctly removed.
In addition, if the same expression is found in both \posc{} and \negc{} context, then we would create both the \gls{half-reif} of the expression and its negation.
The propagation of these two \glspl{half-reif} would be equivalent to propagating the full \gls{reification} of the same expression.
It is therefore better to actually create the full \gls{reification} as it would be able to be reused during flattening.
Because the expression itself is changed when a negation is moved inwards, it may not always be clear when the same expression is used in both \posc{} and negc{} context.
This problem is solved by introducing a canonical form for expressions where negations can be pushed inwards.
In this form the result of flattening an expression and its negation are collected in the same place within the \gls{cse} table.
If it is found that for an expression that is about to be half reified there already exists an \gls{half-reif} for its negation, then we instead evaluate the expression in mixed context, reifying the expression and replacing the existing half reified expression.
This canonical form for expressions and their negations can also be used for the expressions in other contexts.
Using the canonical form we can now also be sure that we never create a full \gls{reification} for both an expression and its negation.
Instead, when one is created, the negation of the resulting \variable{} releasises its negation.
Instead, when one is created, the negation of the resulting \variable{} can directly be used as the result of reifying its negation.
Moreover, this mechanism also allows us to detect when an expression and its negation occur in \rootc{} context.
This is simple way to detect conflicts between \constraints{} and, by extend, prove that the constraint model is unsatisfiable.
Clearly, a \constraint{} and its negation cannot both hold at the same time.