Index: /reasoner/consTranslation.tex =================================================================== --- /reasoner/consTranslation.tex (revision 219) +++ /reasoner/consTranslation.tex (revision 220) @@ -609,37 +609,35 @@ \subsection{Constraint base operations}\label{sectContainerBase}\label{sectConstraintBase} -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: +In this section, we discuss the support operations to create and maintain the constraint base, in particular the $add$\footnote{The implementation method \IVML{addConstraint} is called here $add$ due to layout reasons.} and the $register$\footnote{\label{fnRegisterConstraint}The method \IVML{registerConstraint} is called here $register$ due to layout reasons.} function. + +The main purpose 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 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}. + \item Filters out irrelevant constraints due to the actual reasoning mode. For example, in incremental reasoning, simple (default value) assignment constraints are assumed to be already evaluated during a previous execution of the reasoner main loop. Similarly, constraints in which all relevant variables are either frozen or local (parameters in user-defined functions, variables defined in let-expressions or iterator variables in quantors) can be ignored. Below, for a constraint $c$, $isFrozen(c)$ returns whether $c$ exclusively uses local or frozen variables. + \item Performs the incremental quantification using Algorithm \ref{algComposeExpression}. + \item Completes the constraint base by analyzing compound or container initializers for constraint values that must be turned into constraints in the constraint base (akin to Section \ref{sectConstraintVariables}). 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 forms. The IVML parser creates a constant value if all contained elements are constant and otherwise an initializer expression.}. + \item Enacts the evaluation priority by adding eval-block constraints to the front and other constraints to the end of the constraint sequence $s$. + \item Registers the given constraint with its used variables in $\relevantConstraintsPerDeclaration$ to support the re-scheduling of constraints. \end{itemize} -Let $ex$ be a constraint expression. Then Algorithm \ref{algAddConstraint} realizes the following to translation patterns: +Let $ex$ be a constraint expression. Then Algorithm \ref{algAddConstraint} realizes the following to translation patterns for initializer structures: \grayPara{ - \patternDerivation{v = \IVML{\{}\ldots, ex,\ldots\IVML{\}}}{\ldots, \varSubstitution{ex}{\variableMapping}, \ldots} - \patternDerivation{v = \IVML{\{} s = ex \IVML{\}}}{\varSubstitution{ex}{\variableMapping}} + \patternDerivationLabel{v = \IVML{\{}\ldots, ex,\ldots\IVML{\}}}{\ldots, \varSubstitution{ex}{\variableMapping}, \ldots}{forInitContainer} + \patternDerivationLabel{v = \IVML{\{} s = ex \IVML{\}}}{\varSubstitution{ex}{\variableMapping}}{forInitCompound} } -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 (\IVMLself{} is handled by the expression evaluator here) and adds the result to the constraint base. - -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}. - -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}. +When assigning a value to a variable, the right side may be a complex initializer structure determining the actual value of a (nested) collection or a compound. The algorithms and transformations discussed so far focus on nested variables and types rather than such initializer structures. Instead of defining a specific translation algorithm that must be called from different algorithms, we opted for integrating the translation into the central $add$ function. Pattern \ref{forInitContainer} targets container and Pattern \ref{forInitCompound} compound initializers. In both patterns, constraints may occur as contained (nested) values. The translation in Algorithm \ref{algAddConstraint} extracts these constraints, performs a respective variable substitution (here, \IVMLself{} is handled implicitly by the expression evaluator due to technical reasons) and adds the result to sequence $s$. + +Algorithm \ref{algAddConstraint} receives the target constraint sequence $s$, a constraint $c$ that shall be added to $s$, a flag to enable checking $c$ for Pattern \ref{forInitContainer} or \ref{forInitCompound} as well as an optional variable $v$ the constraint shall be related to. For convenience, we allow passing in a set of constraints instead of a single constraint and assume Algorithm \ref{algAddConstraint} adds all given constraints. \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$} + \KwData{$\topLevelConstraints$ and $\otherConstraints$ constraint sequences, 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)$\; + $createConstraintVariableConstraint(d, \undef, \undef)$\; \label{algAddConstraintCreateConstraintVariableConstraint} } } \label{algAddConstraintCheckEnd} @@ -656,4 +654,6 @@ \end{algorithm} +For a given constraint $c$, Algorithm \ref{algAddConstraint} performs in line \ref{algAddConstraintComposeExpression} the incremental quantification (cf. Algorithm \ref{algComposeExpression}). Then, if enabled, Algorithm \ref{algAddConstraint} checks the given constraint for initializer structures (lines \ref{algAddConstraintCheckStart}-\ref{algAddConstraintCheckEnd}). The $check$ function recursively identifies all constraint variable values in initializer structures and returns the identified expressions as a sequence. In line \ref{algAddConstraintCreateConstraintVariableConstraint}, these expressions are turned into constraint variable constraints using Algorithm \ref{algCreateConstraintVariableConstraint}. + %\begin{algorithm}[H] % \KwIn{constraint sequence $s$, constraint sequence $c$, perform initializers $check$} @@ -665,17 +665,17 @@ %\end{algorithm} -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. - -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. +Depending on the reasoning mode, Algorithm \ref{algAddConstraint} determines in line \ref{algAddConstraintAddStart} whether the constraint $c$ shall ultimately be added to $s$ (lines \ref{algAddConstraintAddStart}-\ref{algAddConstraintAddEnd}). As mentioned above, in incremental reasoning, assignment constraints and frozen constraints can be skipped. From a performance point of view, an alternative would be to determine this property before variable substitution and final constraint composition. However, we opted to defer this potential improvement to future work, as this would affect all transformation algorithms. 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 $inEvals$) and the target constraint sequence is $\otherConstraints$ or $\topLevelConstraints$ (other or top-level constraints), 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$ with all used variables in $\relevantConstraintsPerDeclaration$, the global mapping linking a variable declaration to the constraints using the variable. + +The $check$ function\footnote{Realized as a visitor in the implementation.} iterates over the expressions/values contained in $c$. If the contained element $e$ is a container or compound initializer, the $check$ function continues iterating by recursion. If $e$ is a constraint expression (from an initializer), we apply the actual variable substitution and create a respective constraint. If $e$ is a constraint value, the result is the constraint stored in $e$. Finally, container or compound values can contain Boolean constants, that we directly can use as constant constraints. % \begin{align*} -check&(c, \variableMapping) =\\ +c&heck(c, \variableMapping) =\\ &\seqWith{\closedCases{check(e, \variableMapping), & \text{if } isContainerInitializer(e) \\ check(e, \variableMapping), & \text{if } isContainer(type(e)) \\ check(e, \variableMapping) & \text{if } isCompoundInitializer(e) \\ check(e, \variableMapping) & \text{if } isCompound(type(e)) \\ - e, &\text{if } isConstraint(e) \\ + \createConstraint{\varSubstitutionVarMapping{e}}, &\text{if } isConstraint(e) \\ value(e), &\text{if } isConstraintValue(e) \\ - e, &\text{if } Boolean(e) \\ + e, &\text{if } isBoolean(e) \\ \emptySet, &\text{else} }}{e\in expr(c) \cup elements(c)} @@ -683,5 +683,5 @@ % -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. +For efficient constraint re-scheduling, fast access to the constraints related to the changed variable is required. As introduced in Section \ref{sectTopLevelMainReasoningLoop}, $\relevantConstraintVariables$ is a bi-directional mapping between constraint values assigned to configured decision variables. Algorithm \ref{algRegisterConstraint} modifies/updates $\relevantConstraintVariables$ and, if enabled, also stores this information in the copy of the constraint base to enable incremental reasoning based on stored constraints. \begin{algorithm}[H] @@ -704,3 +704,3 @@ \end{algorithm} % -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. +As input, Algorithm \ref{algRegisterConstraint} receives a constraint $c$ and the variable $v$ the constraint shall be related to. For convenience, we allow that $v = \undef$, i.e., no registration happens. If $v$ is given, we map $c$ to $v$ in line \ref{algRegisterConstraintC2V}. 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.