Index: /reasoner/consRescheduling.tex =================================================================== --- /reasoner/consRescheduling.tex (revision 220) +++ /reasoner/consRescheduling.tex (revision 221) @@ -1,5 +1,5 @@ \section{Constraint Re-scheduling}\label{sectTopLevelConstraintsRescheduling} -When variable $v$ is changed as side effect of a constraint evaluation, modifications of the constraint base may be required, e.g., when the value of a constraint variable or the type of a compound value changes. If the value of a variable changes, Algorithm \ref{algVarChange} is called\footnote{In the implementation, the algorithm is a combination of a visitor and a listener in \class{RescheduleValueChangeVisitor.java}.}. +When configuration variable $v$ is changed as side effect of a constraint evaluation, modifications of the constraint base may be required, e.g., when the value of a constraint variable or the type of a compound value changes. Upon a value change, Algorithm \ref{algVarChange} is called\footnote{In the implementation, Algorithm \ref{algVarChange} is realized as a combination of a visitor and a listener in \class{RescheduleValueChangeVisitor.java}.}. \begin{algorithm}[H] @@ -8,5 +8,5 @@ \KwData{scope assignments $\scopeAssignments$, relevant constraints $\relevantConstraintsPerDeclaration$ and $\relevantConstraintVariables$} - \uIf{$\neg isLocal(v)$}{ + \uIf{$\neg isLocal(v)$}{\label{algVarChangeIsLocal} $addAssignment(\scopeAssignments, v)$\; \label{algVarChangeScope} %addScopeAssignment $val_n \assng value(v)$\; @@ -27,7 +27,9 @@ \end{algorithm} -At its core, Algorithm \ref{algVarChange} receives a value change in terms of the changed variable $v$ (including the new value) and the old value before the change $val_o$. The algorithm determines the kind of the change and either creates new constraints using the constraint translation introduced in Section \ref{sectTranslation} or adds dependent constraints for re-evaluation to the constraint base. Moreover, Algorithm \ref{algVarChange} must treat local variable changes, e.g. an iterator variable, in a specific way. As discussed in Section \ref{sectConstraintVariables}, the actual value of iterator variables must be recorded in $\variableMapping$ so that subsequent constraint translations can correct temporarily unbound variables in constraint values upon constraint variable changes. - -If the changed variable is not local, the change is relevant for re-scheduling related or dependent constraints. First, Algorithm \ref{algVarChange} registers in line \ref{algVarChangeScope} the change of $v$ within the actual project scope. This information is used by the expression evaluator to avoid illegal duplicate assignments within the same scope. If the value changed (lines \ref{algVarChangeRescheduleConstraintVariables}-\ref{algVarChangeRescheduleValueTypeChange}), this may involve a constraint variable or imply a value type change. If a (nested) constraint value changed, we call Algorithm \ref{algRescheduleConstraintValue} in line \ref{algVarChangeRescheduleConstraintVariables} to exchange the involved constraints. +Algorithm \ref{algVarChange} receives information about a value change in terms of the changed variable $v$ (already holding the new value) and the old value $val_o$ before the value change. If a configuration variable was changed, the algorithm determines the kind of the change and either creates new constraints using the constraint translation introduced in Section \ref{sectTranslation}, adds dependent constraints for re-evaluation to the constraint base, or removes superfluous constraints. If a local variable was changed, e.g., an iterator variable, Algorithm \ref{algVarChange} adjusts the variable mapping as discussed in Section \ref{sectConstraintVariables}. + +If a (non-local) configuration was changed (line \ref{algVarChangeIsLocal}), the value change is relevant for re-scheduling related or dependent constraints. Algorithm \ref{algVarChange} registers in line \ref{algVarChangeScope} the change of $v$ within the actual project scope. This information is used by the expression evaluator to avoid illegal duplicate assignments within the same scope. If the value changed (lines \ref{algVarChangeRescheduleConstraintVariables}-\ref{algVarChangeRescheduleValueTypeChange}), this may involve a constraint variable or imply a value type change. If the value of a (nested) constraint variable was changed, we call Algorithm \ref{algRescheduleConstraintValue} in line \ref{algVarChangeRescheduleConstraintVariables} to exchange the involved constraints. + +If the type of the value changed, we call Algorithm \ref{algTranslateValueTypeChange} to add or to remove related constraints (line \ref{algVarChangeRescheduleValueTypeChange}). Function $isValueTypeChange$ determines a value type change if $v$ is a compound variable, old and new value are given and their types differ: \begin{align*} @@ -35,7 +37,7 @@ \end{align*} -If the type of the value changed (see function $isValueTypeChange$ above), we call Algorithm \ref{algTranslateValueTypeChange} to add or to remove related constraints (line \ref{algVarChangeRescheduleValueTypeChange}). Both algorithms use the constraint translation from Section \ref{sectTranslation} to instantiate constraints if needed. Moreover, when the value of $v$ changes, the reasoner shall perform forward reasoning, i.e., check whether constraints using $v$ are still valid. Therefore, Algorithm \ref{algVarChange} consults the relevant constraints per declaration $\relevantConstraintsPerDeclaration$ and adds all registered constraints for all parent and nested variables to the constraint base (lines \ref{algVarChangeRescheduleParents}-\ref{algVarChangeRescheduleNested}), but only if the respective constraints are not already in the constraint base. - -If the changed variable is local and there is a mapping in $\variableMapping$, e.g., as the variable is used as iterator in the evaluation of a quantor expression, we adjust the variable mapping\footnote{A local decision variable wraps either a value (if the evaluation runs over constants) or a decision variable. To allow for (call-by-reference) evaluation on nested slots and attributes, this part actually refers to the wrapped decision variable (not detailed here).}. If the subsequent evaluation of the quantor expression causes a change of a variable, Algorithm \ref{algVarChange} will be called for that variable. If then either Algorithm \ref{algRescheduleConstraintValue} or Algorithm \ref{algTranslateValueTypeChange} is called, the involved constraint translations will consider the changed $\variableMapping$ in their variable substitutions and replace unbound iterator variables. +Both algorithms, Algorithm \ref{algRescheduleConstraintValue} and \ref{algTranslateValueTypeChange}, use the constraint translation from Section \ref{sectTranslation} to instantiate constraints if needed. + +In any case of a value change of $v$, the reasoner shall perform forward reasoning, i.e., check whether constraints using $v$ are still valid. Therefore, Algorithm \ref{algVarChange} consults the relevant constraints per declaration $\relevantConstraintsPerDeclaration$ and adds all registered constraints for all parent and nested variables to the constraint base (lines \ref{algVarChangeRescheduleParents}-\ref{algVarChangeRescheduleNested}), but only if the respective constraints are not already in the constraint base. \begin{algorithm}[H] @@ -62,4 +64,7 @@ \caption{Reschedule a value change (\IVML{rescheduleValueChange}).}\label{algRescheduleValueChange} \end{algorithm} + +If the changed variable is local and there is a mapping in $\variableMapping$, e.g., as the variable is used as iterator in the evaluation of a quantor expression, we adjust the variable mapping\footnote{A local decision variable wraps either a value (if the evaluation runs over constants) or a decision variable. To allow for (call-by-reference) evaluation on nested slots and attributes, this part actually refers to the wrapped decision variable (not detailed here).}. If the subsequent evaluation of the quantor expression causes a change of a variable, Algorithm \ref{algVarChange} will be called for that variable. If then either Algorithm \ref{algRescheduleConstraintValue} or Algorithm \ref{algTranslateValueTypeChange} is called, the involved constraint translations will consider the changed $\variableMapping$ in their variable substitutions and replace unbound iterator variables. + Algorithm \ref{algRescheduleValueChange} is responsible for re-scheduling constraint values from a given IVML value. The idea is to follow nested value structures recursively, to extract constraint values and to add them after variable substitution to the constraint base. Upon the first changed constraint value for the given variable, existing constraints shall be cleared from the reasoning data structures. Index: /reasoner/consTranslation.tex =================================================================== --- /reasoner/consTranslation.tex (revision 220) +++ /reasoner/consTranslation.tex (revision 221) @@ -10,5 +10,5 @@ %\emph{Top-level constraints} are defined using only top-level variables or fully qualifying accessor expressions. Top-level constraints include constraints in top-level eval blocks as well as constraints in top-level annotation assignment-blocks. Top-level constraints are ready for reasoning, i.e., they do not need further translation and can directly be taken over into the constraint base (Algorithm \ref{algTranslateConstraints}, lines \ref{algTranslateConstraintsAdd} - \ref{algTranslateConstraintsTopLevelEvals}). Annotation assignments are processed by Algorithm \ref{algTranslateAnnotationAssignments}. We use that algorithm also for translating annotation assignments in compound types. -Thus, the next step after the top-level constraint translation is the translation of variable declarations in Algorithm \ref{algTranslateDeclaration} (called by Algorithm \ref{algTranslateConstraints} in line \ref{algTranslateConstraintsTranslationDeclaration}). In Section \ref{sectTranslationDeclarationTypesDefaults}, we will detail Algorithm \ref{algTranslateConstraints}, which performs the translation of variable declarations and the creation of default value constraints, but also delegates further translations to subsequent algorithms (as indicated in Figure \ref{figStructure}). We will discuss the subsequent algorithms in the following sub-sections, namely derived types in Section \ref{sectDerivedTypes}, compound types in Section \ref{sectCompoundDefaults}, container types in Section \ref{sectContainerDefaults}, annotation assignments in Section \ref{sectAnnotationDefaults}, and, constraint variables in Section \ref{sectConstraintVariables}. Finally in Section \ref{sectContainerBase}, we introduce the support algorithms used for building the constraint base. As also shown in Figure \ref{figStructure}, the subsequent algorithms may recursively call Algorithm \ref{algTranslateConstraints} while translating nested types, such as compounds in compounds or compounds in containers. +Thus, the next step after the top-level constraint translation is the translation of variable declarations in Algorithm \ref{algTranslateDeclaration} (called by Algorithm \ref{algTranslateConstraints} in line \ref{algTranslateConstraintsTranslationDeclaration}). In Section \ref{sectTranslationDeclarationTypesDefaults}, we will detail Algorithm \ref{algTranslateConstraints}, which performs the translation of variable declarations and the creation of default value constraints, but also delegates further translations to subsequent algorithms (as indicated in Figure \ref{figStructure}). We will discuss the subsequent algorithms in the following sub-sections, namely derived types in Section \ref{sectDerivedTypes}, compound types in Section \ref{sectCompoundDefaults}, container types in Section \ref{sectContainerDefaults}, annotation assignments in Section \ref{sectAnnotationDefaults}, constraint variables in Section \ref{sectConstraintVariables}, and initializer expressions in Section \ref{sectInitEx}. Finally in Section \ref{sectConstraintBase}, we introduce the support algorithms used for building the constraint base. As also shown in Figure \ref{figStructure}, the subsequent algorithms may recursively call Algorithm \ref{algTranslateConstraints} while translating nested types, such as compounds in compounds or compounds in containers. \subsection{Variable Declarations}\label{sectTranslationDeclarationTypesDefaults} @@ -367,5 +367,5 @@ \subsubsection{Incremental Container Quantification}\label{sectContainerQuantification} -While $f(v, t)$ allows processing a container variable $v$, it is just one part in the translation of nested containers. In this section we discuss the quantification of constraints for nested container structures. As we collect the information for the quantification across various algorithms, we call this approach \textbf{incremental container quantification}. The actual quantification happens when adding constraints to the constraint base, i.e., in the $add$ function (cf. Algorithm \ref{algAddConstraint} in Section \ref{sectContainerBase}). +While $f(v, t)$ allows processing a container variable $v$, it is just one part in the translation of nested containers. In this section we discuss the quantification of constraints for nested container structures. As we collect the information for the quantification across various algorithms, we call this approach \textbf{incremental container quantification}. The actual quantification happens when adding constraints to the constraint base, i.e., in the $add$ function (cf. Algorithm \ref{algAddConstraint} in Section \ref{sectConstraintBase}). The basic idea of Pattern \ref{forContainerQuant} is that constraints defined on (used) element types must be lifted to the container level by all-quantification. However, containers may be nested, i.e., require nested quantification. While directly nested containers are handled by $f(v, t)$, nesting containers via compounds requires special care. @@ -576,5 +576,5 @@ In more details\footnote{In contrast to the implementation, we represent here two parameters for self value/expression by a single parameter and omit a parameter for the constraint parent.}, Algorithm \ref{algCreateConstraintVariableConstraint} takes a constraint expression (e.g., the default value of a constraint variable or a nested variable through Algorithm \ref{algTranslateDeclaration}), an optional expression $e_f$ representing \IVMLself{} and the constraint variable $v$ if available\footref{fnVariableNull}. Algorithm \ref{algCreateConstraintVariableConstraint} performs in line \ref{algCreateConstraintVariableConstraintCreate} a variable substitution with $\variableMapping$ and, if given, $e_f$, and turns the resulting expression into a (constraint variable) constraint. In line \ref{algCreateConstraintVariableConstraintAdd}, the algorithm adds the created constraint to the set of other constraints $\otherConstraints$ (disabling the analysis for complex values in case of constant constraints such as \IVML{true}). -%The third parameter of the $add$ function (will be discussed in Section \ref{sectContainerBase}) indicates whether the constraint be analyzed for complex value assignments that contain constraints as values for constraint variables. This is not required (and may sometimes lead to endless recursions) if the constraint here is a constant value. +%The third parameter of the $add$ function (will be discussed in Section \ref{sectConstraintBase}) indicates whether the constraint be analyzed for complex value assignments that contain constraints as values for constraint variables. This is not required (and may sometimes lead to endless recursions) if the constraint here is a constant value. In line \ref{algCreateConstraintVariableConstraintRegister}, the algorithm registers the relation between $v$ and the created constraint in $\relevantConstraintsPerDeclaration$ and $\relevantConstraintVariables$. %is recorded to enable efficient updates of the constraint base upon value changes (cf. Algorithm \ref{algVarChange}). @@ -607,19 +607,7 @@ In more details, we use $\variableMapping$ also during expression evaluation to track the actual values of (local) iterator variables within an additional stack frame created during the evaluation. We may apply the tracked values when assigning the new constraint value to the respective variable, but this would lead to unwanted dependencies between expression evaluator and reasoning. A second point in time when we can perform the variable substitution is the constraint re-scheduling, i.e., when the reasoner is informed that the value (including the initial default value) of a variable was changed. When the evaluation of the quantor assigns the new constraint value, the value change triggers the replacement of the old constraint by the new one in the constraint base. For the new constraint, the constraint translation must executed anyway, i.e., a variable substitution is performed. The variable substitution utilizes $\variableMapping$, i.e., also the stack frame for iterator variables added during the evaluation, and, thus, implicitly binds the iterator variables in the constraint to the correct values. Finally, the corrected constraint is assigned to the configuration variable so that further model operations such as saving the configuration use the actual (correct) constraint. For the time between triggering the assignment of a constraint value and the subsequent constraint re-scheduling, which effectively corrects the value and performs the final assignment, we accept constraints with unbound variables. This is not a problem per se, as no further constraint (sub-)expressions happen in this time span. -\subsection{Constraint base operations}\label{sectContainerBase}\label{sectConstraintBase} - -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 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 for initializer structures: +\subsection{Initializer Expressions}\label{sectInitEx} + +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. 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.}. The algorithms and transformations discussed so far focus on nested variables and types rather than such initializer structures. Let $ex$ be a constraint expression. Then the constraint translation realizes the following to translation patterns for initializer structures: \grayPara{ @@ -628,5 +616,52 @@ } -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$. +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{algCheckInit} extracts these constraints. This translation is called by the central $add$ function (cf. Section \ref{sectConstraintBase}), which will turn them into constraints using a respective variable substitution. + +\begin{algorithm}[H] + \SetAlgoLined + \KwIn{constraint expression $c$} + \KwOut{instantiated constraint variable constraints} + + $x \assng expr(c) \cup elements(c)$\;\label{algCheckInitX} + \Return $\seqWith{\closedCases{inits(e), & \text{if } isContainerInitializer(e) \\ + inits(e) & \text{if } isCompoundInitializer(e) \\ + inits(e), & \text{if } isContainer(type(e)) \\ + inits(e) & \text{if } isCompound(type(e)) \\ + e, &\text{if } isConstraint(e) \\ + value(e), &\text{if } isConstraintValue(e) \\ + e, &\text{if } isBoolean(e) \\ + \undef, &\text{else} + }}{e\in x}$\; + \caption{Translating initializer expressions (\IVML{inits}).}\label{algCheckInit} +\end{algorithm} +% +Algorithm \ref{algCheckInit}\footnote{The algorithm is called \IVML{check} in the implementation and realized in terms of a visitor.} determines the expressions/values contained in the constraint expression $c$. As the expression is supposed to be either an initializer or a complex value, either expressions or value (elements) are available, i.e., the local variable $x$ in line \ref{algCheckInitX} contains only instances of one kind. Algorithm \ref{algCheckInit} iterates over all elements $e$ in $x$ and returns as result the (potentially empty) sequence of contained and translated constraint expressions. If the contained element $e$ is an initializer or a complex value, the algorithm continues on the contained elements through recursion. If $e$ is a constraint expression (from an initializer), we take over $e$ into the result. If $e$ is a constraint value, we include the constraint stored in $e$ into the result. Finally, if the expression is a Boolean constant, we directly use the constant as constraint (expression). In any other case, the result for $e$ is undefined. +%\begin{align*} +%i&nits(c, \variableMapping) =\\ +% &\seqWith{\closedCases{inits(e, \variableMapping), & \text{if } isContainerInitializer(e) \\ +% inits(e, \variableMapping), & \text{if } isContainer(type(e)) \\ +% inits(e, \variableMapping) & \text{if } isCompoundInitializer(e) \\ +% inits(e, \variableMapping) & \text{if } isCompound(type(e)) \\ +% \createConstraint{\varSubstitutionVarMapping{e}}, &\text{if } isConstraint(e) \\ +% value(e), &\text{if } isConstraintValue(e) \\ +% e, &\text{if } isBoolean(e) \\ +% \emptySet, &\text{else} +% }}{e\in expr(c) \cup elements(c)} +%\end{align*} +% + +\subsection{Constraint base operations}\label{sectContainerBase}\label{sectConstraintBase} + +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 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 using Algorithm \ref{algCheckInit}. + \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} 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. @@ -638,5 +673,5 @@ $c \assng composeExpression(\variableMapping, c)$\; \label{algAddConstraintComposeExpression} \If{$check$}{ \label{algAddConstraintCheckStart} - \ForAll{$d\iterAssng check(rightSide(c), \variableMapping)$} { + \ForAll{$d\iterAssng inits(rightSide(c))~\setminus \undef$} { $createConstraintVariableConstraint(d, \undef, \undef)$\; \label{algAddConstraintCreateConstraintVariableConstraint} } @@ -654,5 +689,5 @@ \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}. +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}). Algorithm \ref{algCheckInit} 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] @@ -666,20 +701,4 @@ 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*} -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)) \\ - \createConstraint{\varSubstitutionVarMapping{e}}, &\text{if } isConstraint(e) \\ - value(e), &\text{if } isConstraintValue(e) \\ - e, &\text{if } isBoolean(e) \\ - \emptySet, &\text{else} - }}{e\in expr(c) \cup elements(c)} -\end{align*} -% 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.