Index: /reasoner/consTranslation.tex =================================================================== --- /reasoner/consTranslation.tex (revision 159) +++ /reasoner/consTranslation.tex (revision 160) @@ -507,52 +507,64 @@ \subsection{Constraint base operations}\label{sectContainerBase} -In this section, we detail specific support operations to create and maintain the constraint based, most notably the $add$ function\footnote{\IVML{addConstraint} in the implementation, in this document $add$ for short due to layout reasons.}, which we used throughout this document to describe the individual translation algorithms. Besides adding a constraint $c$ to a given constraint sequence $s$, the $add$ function performs several important operations: +In this section, we discuss the support operations to create and maintain the constraint based, in particular the $add$ function\footnote{\IVML{addConstraint} in the implementation, in this document $add$ due to layout reasons.} and the $register$\footnote{\label{fnRegisterConstraint}\IVML{registerConstraint} in the implementation, akin to $add$ due to layout reasons.} function. We start with the $add$ function and continue with the $register$ function. + +The main functionality of $add$ is to append a constraint to the constraint base, more precisely one of the constraint sequences introduced at the beginning of Section \ref{sectTranslation}. Besides adding a constraint $c$ to a given constraint sequence $s$, the $add$ function performs the following operations. The algorithm: \begin{itemize} - \item It filters out irrelevant constraints, in particular simple (default value) assignment constraints during incremental reasoning, are assumed to be already processed during previous iterations. Also constraints with all variables frozen or local (used for iterator variables in quantors) are filtered out ($isFrozen(c)$) if enabled, e.g., to speed up runtime reasoning. - \item It serves as the central place to finally compose constraints for nested compound containers using Algorithm \ref{algComposeExpression} and the variable mapping $\variableMapping$. - \item It analyzes the given constraint $c$ for the use of compound or container initializers. As explained above, these structures only occur in value assignments and actually must be analyzed for constraint variables, which must be turned into individual constraints. We perform this through the two recursive helper operations for expressions $checkContainerInitializer$ and $checkCompoundInitializer$ and two similar helper functions for values $checkContainerValue$ and $checkCompoundValue$ shown below\footnote{The implementation utilizes a visitor for this purpose.}. - \item Appends the constraint to the given sequence, except for constraints from eval-blocks, which are prepended to the sequence of top-level constraints $\topLevelConstraints$ if the target sequence is other $\otherConstraints$ or top-level constraints $\topLevelConstraints$ in order to enforce the priority of eval-constraints. - \item Registers the constraint with its used variables to enable re-scheduling of constraints during reasoning in Algorithm \ref{algVarChange}. + \item Filters out actually irrelevant constraints according to the actual reasoning mode. For example, in incremental reasoning, simple (default value) assignment constraints reasoning are assumed to be already evaluated during a previous reasoning run. Also 'frozen constraints', i.e., constraints in which all variables are frozen or local (e.g., used as parameters in constraint functions, in let-expressions or as iterator variables in quantors) can be ignored, e.g., to speed up runtime reasoning. In the following, for a constraint $c$, $isFrozen(c)$ returns whether $c$ is defined only over local or frozen variables. + \item Serves as the central place to finally compose the constraints for nested compound containers using Algorithm \ref{algComposeExpression}. + \item Realizes central functionality for completing the constraint base with respect to compound or container initializers, which may contain constraint values that must be turned into constraints in the constraint base. These initializer structures may occur in two forms, as expressions or as constant values\footnote{Technically, we must make the distinction between expression and constant, as the IVML object model supports both types of elements and the IVML parser creates a constant value if all contained elements are constant or otherwise an initializer expression.}, and are typically used in assignment constraints. + \item Enacts the evaluation priority. Typically, constraints are added to the end, except for constraints in eval-blocks, which are prepended to enforce their specific evaluation priority. + \item Registers the given constraint with its used variables in the central structure $\relevantConstraintsPerDeclaration$ to enable re-scheduling of constraints upon value changes in Algorithm \ref{algVarChange}. \end{itemize} -Thus, the functiondoes not only add a given constraint, it completes it and scans it for further contained constraints. Let $ex$ be a constraint expression. Then we have to consider two specific assignment operations not transformed so far. +Let $ex$ be a constraint expression. Then Algorithm \ref{algAddConstraint} realizes the following to translation patterns: \grayPara{ \begin{gather*} \patternDerivation{v = \IVML{\{}\ldots, ex,\ldots\IVML{\}}}{\ldots, \varSubstitution{ex}{\variableMapping}, \ldots}\\ - \patternDerivation{v = \IVML{\{} s = ex \IVML{\}}}{\varSubstitution{ex}{\IVML{self}=v, \variableMapping}} + \patternDerivation{v = \IVML{\{} s = ex \IVML{\}}}{\varSubstitution{ex}{\variableMapping}}\\ \end{gather*} } -When unconditionally assigning a value to a variable, the right side may be a complex expression determining the actual value of a collection or a compound. In both cases, the contained values may be constraint values (not handled in \ref{sectConstraintVariables}), but also deeply nested values may be constraint values, e.g., a constraint value in a compound in collection used in a compound. These constraints contribute to the initial constraint base and may cause certain value changes that cannot just be achieved as a consequence of changing values in constraint re-scheduling (cf. Section \ref{sectTopLevelConstraintsRescheduling}). As the $add$ function is also called as part of re-scheduling, dynamic constraints discovered there and their initializers and values are treated similarly. - -\begin{algorithm}[H] - \KwIn{constraint sequence $s$, constraint $c$, perform initializers $check$, variable $v$} - \KwData{top level and other constraints $\topLevelConstraints, \otherConstraints$, variable mapping $\variableMapping$, relevant constraints $\relevantConstraintsPerDeclaration$ , incremental flag $inc$, evals flag $inEvals$} - - $c = composeExpression(\variableMapping, c)$\; - \If{$check$}{ +When assigning a value to a variable, the right side may be a complex initializer expression determining the actual value of a collection or a compound. The algorithms and transformations discussed so far focus on nested variables and types rather than such initializer expressions. Instead of defining a specific translation algorithm that must be called from different algorithms, we opted for integrating the translation with the central functionality of adding constraints to the constraint base. The first translation pattern targets containers and the second one compounds. In both patterns, constraint values may occur as (deeply nested) contained values. The translation applied in Algorithm \ref{algAddConstraint} extracts these constraints, performs a respective variable substitution (\IVML{self} is currently not supported here) and adds the result to the constraint base. + +\begin{algorithm}[H] + \KwIn{constraint sequence $s$, constraint $c$, $check$ flag, variable $v$} + \KwData{top-level $\topLevelConstraints$ and other constraints $\otherConstraints$, variable mapping $\variableMapping$, relevant constraints $\relevantConstraintsPerDeclaration$ , incremental flag $inc$, eval-block flag $inEvals$} + + $c \assng composeExpression(\variableMapping, c)$\; \label{algAddConstraintComposeExpression} + \If{$check$}{ \label{algAddConstraintCheckStart} \ForAll{$d\iterAssng check(rightSide(c), \variableMapping)$} { $createConstraintVariableConstraint(d, \undef, \undef)$\; } - $e\assng check(rightSide(c), \variableMapping)$ - $add(\otherConstraints, e, const(e) \neq \undef, v$\; - } - \If{$\closedCases{\neg isAssignment(c) \vee \neg isFrozen(c) & \text{if } inc\\ true & \text{else}}$}{ - \If{$inEvals \wedge (s=\otherConstraints \vee s = \topLevelConstraints)$} { - $\topLevelConstraints = c \addSeq \topLevelConstraints$\; + } \label{algAddConstraintCheckEnd} + \If{$\closedCases{\neg (isAssignment(c) \vee isFrozen(c)) & \text{if } inc\\ true & \text{else}}$}{\label{algAddConstraintAddStart} + \If{$inEvals \wedge (s=\otherConstraints \vee s = \topLevelConstraints)$} {\label{algAddConstraintAddPosStart} + $\topLevelConstraints = c \addSeq \topLevelConstraints$\;\label{algAddConstraintAddPrio} }\Else{ - $s \assng s \addSeq c$\; - } - \If{$\neg isSimpleConstraint(c)$}{ - $\relevantConstraintsPerDeclaration \assng \relevantConstraintsPerDeclaration \cup \setWith{\mapEntry{w}{c}}{w\in variables(c)}$\; % assignConstraintsToVariables - } - } + $s \assng s \addSeq c$\; \label{algAddConstraintAddNormal} + }\label{algAddConstraintAddPosEnd} + $\relevantConstraintsPerDeclaration \assng \relevantConstraintsPerDeclaration \cup \setWith{\mapEntry{w}{c}}{w\in variables(c)}$\; % assignConstraintsToVariables + }\label{algAddConstraintAddEnd} \caption{Adds a constraint to the constraint base ($add$).}\label{algAddConstraint} \end{algorithm} -To identify constraint variable values in containers and compounds, we define the following helper function: +Algorithm \ref{algAddConstraint} receives a target constraint sequence $s$, a constraint $c$ that shall be added to $s$, a flag which enables checking for constraint values and an optional variable $v$ the constraint shall be related to. For convenience, in some algorithms we also passed a set of constraints for adding instead of a single constraint. We just assume that then all given constraints are forwarded iteratively to Algorithm \ref{algAddConstraint}. + +%\begin{algorithm}[H] +% \KwIn{constraint sequence $s$, constraint sequence $c$, perform initializers $check$} +% \KwData{variable mapping $\variableMapping$} +% \ForAll{$d \iterAssng c$} { +% $add(s, d, c)$\; +% } +% \caption{Adds multiple constraints.}\label{algAddConstraints} +%\end{algorithm} + +For a single given constraint $c$, Algorithm \ref{algAddConstraint} completes in line \ref{algAddConstraintComposeExpression} the constraint expression by composing a potentially missing quantification prefix (cf. Algorithm \ref{algComposeExpression}). Then, if enabled, Algorithm \ref{algAddConstraint} checks the given constraint (lines \ref{algAddConstraintCheckStart}-\ref{algAddConstraintCheckEnd}). The $check$ function identifies recursively all constraint variable values in compounds and containers and returns the identified expressions as a sequence. All elements in that sequence are turned into constraint variable constraints using Algorithm \ref{algCreateConstraintVariableConstraint}. + +Depending on the reasoning mode, Algorithm \ref{algAddConstraint} determines then whether the constraint $c$ shall ultimately be added to the constraint base (lines \ref{algAddConstraintAddStart}-\ref{algAddConstraintAddEnd}). As mentioned above, in incremental reasoning, assignment constraints and frozen constraints can be left out. From a performance aspect, an alternative would be to determine this property before variable substitution and final constraint composition. However, we opted to defer this potential improvement, which would affect all transformation algorithms, to future work. If $c$ shall be added, the actual insertion position is determined in lines \ref{algAddConstraintAddPosStart}-\ref{algAddConstraintAddPosEnd}. If we are adding constraints from eval blocks (global flag $inEval$) and the target constraint sequence is the other $\otherConstraints$ or top-level constraints sequence $\topLevelConstraints$, we prepend the constraint to $\topLevelConstraints$ in line \ref{algAddConstraintAddPrio}. This prioritizes $c$ over all top-level constraints (even the other constraints), but not over default constraints (cf. Section \ref{sectTopLevelConstraintsTranslation}). Otherwise, we add $c$ to the end of the given sequence $s$ in line \ref{algAddConstraintAddNormal}. Finally, we register $c$ against all used variables in $\relevantConstraintsPerDeclaration$ to enable and speed up constraint re-scheduling. +% \begin{align*} check&(c, \variableMapping) =\\ @@ -561,39 +573,34 @@ check(e, \variableMapping) & \text{if } isCompoundInitializer(e) \\ check(e, \variableMapping) & \text{if } isCompound(type(e)) \\ - \createConstraintConstraint{\varSubstitutionVarMapping{e}}, &\text{if } isConstraint(e) \\ - \createConstraintConstraint{\varSubstitutionVarMapping{value(e)}}, &\text{if } isConstraintValue(e) \\ - \createConstraintConstraint{e}, &\text{if } Boolean(e) \\ + e, &\text{if } isConstraint(e) \\ + value(e), &\text{if } isConstraintValue(e) \\ + e, &\text{if } Boolean(e) \\ \emptySet, &\text{else} }}{e\in expr(c) \cup elements(c)} \end{align*} -The function $check$ either iterates over the constituting expressions if $c$ is a container or compound initializer or the contained values if $c$ is a container or compound value\footnote{Technically, we must make the distinction between initializer and constraint, as the IVML object model supports both types of elements here and the IVML parser creates a value if all contained elements are constant or otherwise an initializer expression}. If the contained element $e$ is a further container or compound initializer / iterator, then we continue iterating through recursion. If $e$ is a constraint expression (from an initializer), we apply the actual variable substitution and create a respective constraint. Similarly, for a constraint value $e$ obtained from a container or compound value. Finally, in case of container or compound values, we may have boolean constants, which can simply be turned into a constant constraint. - -%\begin{algorithm}[H] -% \KwIn{constraint sequence $s$, constraint sequence $c$, perform initializers $check$} -% \KwData{variable mapping $\variableMapping$} -% \ForAll{$d \iterAssng c$} { -% $add(s, d, c)$\; -% } -% \caption{Records and analyzes a constraint sequence.}\label{algAddConstraints} -%\end{algorithm} - -\begin{algorithm}[H] - \SetAlgoLined - \KwIn{variable $v$, constraint expression $c$} +% +The $check$ function\footnote{Realized as a visitor in the implementation.} either iterates over the constituting expressions if $c$ is a container or compound initializer or the contained values if $c$ is a container or compound value. If the contained element $e$ is a further container or compound initializer / iterator, then we continue iterating through recursion. If $e$ is a constraint expression (from an initializer), we apply the actual variable substitution and create a respective constraint. Similarly, for a constraint value $e$ obtained from a container or compound value. Finally, in case of container or compound values, we may have boolean constants, which can simply be turned into a constant constraint. + +For constraint re-scheduling upon changed values, a fast access to the actual constraint values assigned to constraint variables is required. Algorithm \ref{algRegisterConstraint} registers constraint variables\footref{fnRegisterConstraint} to enable queries for variables as well as constraints. Further, if enabled, Algorithm \ref{algRegisterConstraint} duplicates this information into the copy of the constraint base in order to enable reasoning based on stored constraints. + +As input, Algorithm \ref{algRegisterConstraint} receives a constraint $c$ and a variable $v$ to related the constraint to. For convenience, we allow that $v = \undef$, i.e., no registration happens. If $v$ is given, we map in line \ref{algRegisterConstraintC2V} $c$ to $v$ to ask for the variable a constraint is related to. Then, in line \ref{algRegisterConstraintV2C} we register the opposite direction. If a stored constraint base shall be recorded (lines \ref{algRegisterConstraintBaseCopyStart}-\ref{algRegisterConstraintBaseCopyEnd}), we repeat both registration steps on the copy of the constraint base. + +\begin{algorithm}[H] + \SetAlgoLined + \KwIn{variable $v$, constraint $c$} \KwData{other constraints $\otherConstraints$, relevant constraints $\relevantConstraintVariables$}, relevant constraints copy $base_{\relevantConstraintVariables}$ \KwOut{$c$} \If{$v \neq \undef$}{ - $\relevantConstraintVariables \assng \relevantConstraintVariables \addMap \mapEntry{c}{v}$\; - $\relevantConstraintVariables[v] \assng \relevantConstraintVariables[v] \cup \set{c}$\; - \If{$base_{\relevantConstraintVariables} \neq \undef$} { + $\relevantConstraintVariables \assng \relevantConstraintVariables \addMap \mapEntry{c}{v}$\;\label{algRegisterConstraintC2V} + $\relevantConstraintVariables[v] \assng \relevantConstraintVariables[v] \cup \set{c}$\;\label{algRegisterConstraintV2C} + \If{$base_{\relevantConstraintVariables} \neq \undef$} {\label{algRegisterConstraintBaseCopyStart} $base_{\relevantConstraintVariables} \assng base_{\relevantConstraintVariables} \addMap \mapEntry{c}{v}$\; $base_{\relevantConstraintVariables}[v] \assng base_{\relevantConstraintVariables}[v] \cup \set{c}$\; - } + }\label{algRegisterConstraintBaseCopyEnd} } \Return $c$\; - \caption{Registering constraints originating fom constraint variables (\textit{register}).}\label{algRegisterConstraint} -\end{algorithm} -% -A constraint is registered\footnote{\IVML{registerConstraint} in the implementation} only if $v$ is defined, which may not be the case if this algorithm is called while processing container values. Then, we recorder the relation of the variable $v$ to its + \caption{Registering constraint values (\textit{register}).}\label{algRegisterConstraint} +\end{algorithm} +%