Index: /reasoner/consTranslation.tex =================================================================== --- /reasoner/consTranslation.tex (revision 206) +++ /reasoner/consTranslation.tex (revision 207) @@ -142,18 +142,17 @@ \end{itemize} -To handle slot interactions among constraints in the same compound correctly, a respective frame in $\variableMapping$ containing mappings for all slots to their access expressions must be created before any slot is translated. Thereby, $\variableMapping$ implicitly considers containing scopes as well as defined and shadowed variables. Moreover, compounds and, thus, constraints induced by compound types, may be nested in compounds and containers. By following the used types, the respective translation functions will be called recursively, i.e., Algorithm \ref{algTranslateDeclaration} for variables, Algorithm \ref{algTranslateCompoundDeclaration} for compound types as well as the translation of containers in Section \ref{sectContainerDefaults}. - -We will now focus on the second pattern and discuss the respective translation Algorithm \ref{algTranslateCompoundDeclaration}. The idea is to visit all slots and constraints in the compound type and its refined compound types, first for creating the variable mapping (Algorithm \ref{algRegisterCompoundMapping}), then for translating all constraints (Algorithm \ref{algTranslateCompoundContent}). In some situations, both steps must be carried out individually instead of a fixed sequence, e.g., to perform the translation of potentially inter-dependent compound slot default values between both steps as discussed for Algorithm \ref{algTranslateDeclaration}. As compound slots are nested variable declarations, Algorithm \ref{algTranslateDeclaration} is responsible for translating slots and their annotations. Akin to Algorithm \ref{algTranslateDeclaration}, default values of annotations (here given in terms of annotation assignments) are only turned into assignment constraints if the reasoner is not in incremental mode. Finally, eval blocks (due to evaluation priority) and then directly nested constraints and constraints in assignment blocks of a compound and all refined compound types are translated. - -If the value of a compound variable changes during reasoning, the value type may also change along the compound refinement hierarchy. Although constraint re-scheduling will be discussed in Section \ref{sectTopLevelConstraintsRescheduling}, we consider this topic already here to present a complete translation algorithm for compund types instead of refining the algorithm later in Section \ref{sectTopLevelConstraintsRescheduling}. Changing value types require adjusting the constraint base, i.e., more or less constraints must be considered dynamically while reasoning. However, when the actual type of a compound variable changes, executing the full constraint transformation for the new type is possible, but inefficent as already known constraints are added again to the constraint base. Moreover, constraints that are still in the constraint base, as they were not evaluated or not fulfilled so far, are duplicated and may cause multiple error messages for the same violation. Thus, it is desirable to transform just the differences between the involved types, i.e., to translate the constraints for all types in the refinement hierarchy between old and new value type. This requires knowledge about already processed types, type exclusion, as well as conditional creation and release of variable mapping context frames. We represent the conditional handling of context frames in terms of the compound translation mode already mentioned for Algorithm \ref{algTranslateDeclaration}, i.e., by constants that indicate to $REGISTER$ the variable mapping, to $TRANSLATE$ the constraints and $NONE$ for no operation (type is known or excluded and shall not be mapped or transformed). - -\begin{algorithm}[H] - \SetAlgoLined - \KwIn{declaration $d$, variable $v$, compound access $ca$, default value type $t$, mode $m$} +To correctly handle slot interactions among constraints in the same compound, a respective frame in $\variableMapping$ containing mappings for all slots to their access expressions must be created before any slot is translated. Thereby, $\variableMapping$ implicitly considers containing scopes as well as defined or shadowed variables. Moreover, compounds and, thus, constraints induced by compound types, may be nested in further compounds and containers. By following the used types, the respective translation functions will be called recursively, i.e., Algorithm \ref{algTranslateDeclaration} for variables, Algorithm \ref{algTranslateCompoundDeclaration} for compound types as well as the translation of containers in Section \ref{sectContainerDefaults}. + +As Pattern \ref{forCompoundDefault} is handled by Algorithm \ref{algTranslateDeclaration}, we will now focus on the remaining patterns, in particular on Pattern \ref{forCompoundSlot}. The idea for Algorithm \ref{algTranslateCompoundDeclaration} is to visit all slots and constraints in the compound type and its refined compound types in two phases. In the first phase, we create the variable accessor expressions (Algorithm \ref{algRegisterCompoundMapping}), and in the second phase we translate all constraints (Algorithm \ref{algTranslateCompoundContent}). In the remainder of this section, we discuss first Algorithm \ref{algTranslateCompoundDeclaration} and then its subsequent algorithms in Section \ref{sectionRegCompAcc} for Algorithm \ref{algRegisterCompoundMapping} and Section \ref{sectionTransComp} for Algorithm \ref{algTranslateCompoundContent}. + +When the value of a compound variable changes during reasoning, the value type may also change along the compound refinement hierarchy. Although constraint re-scheduling will be discussed in Section \ref{sectTopLevelConstraintsRescheduling}, we consider this topic already here to avoid a discussion of refined algorithms in Section \ref{sectTopLevelConstraintsRescheduling}. Changing value types require adjusting the constraint base, i.e., more or less constraints must be considered dynamically during reasoning. However, when the actual type of a compound variable changes, executing the full constraint transformation for the new type is inefficent as already known (potentially including successfully evaluated) constraints may be added again to the constraint base. Moreover, constraints that are still in the constraint base, as they were not evaluated or not fulfilled so far, are duplicated, slow down the constraint evaluation and may cause multiple error messages for the same failing constraint. Thus, it is desirable to transform just the differences of the involved types, i.e., to translate the constraints for all types in the refinement hierarchy ''between'' old and new value type. This requires knowledge about already processed types (handled by the type exclusion in $\variableMapping$ as well as conditional creation and release of context frames on $\variableMapping$. We express the conditional handling of context frames in terms of the compound translation mode, i.e., as already mentioned for Algorithm \ref{algTranslateDeclaration}, constants that indicate to $REGISTER$ the variable mapping, to $TRANSLATE$ the constraints and $NONE$ for no operation (type is known or excluded and shall not be mapped or transformed). + +\begin{algorithm}[H] + \SetAlgoLined + \KwIn{declaration $d$, variable $v$, compound access $ca$, default value type $t$, compound $mode$} \KwData{constraints $\otherConstraints$, variable mapping $\variableMapping$} $next \assng NONE$\; - \If{$\neg alreadyProcessed(\variableMapping, t)$} { - \If{$m = REGISTER$}{ + \If{$\neg alreadyProcessed(\variableMapping, t) \wedge mode = REGISTER$} { $pushContext(\variableMapping, d, v \neq \undef)$\; \label{algTranslateCompoundDeclarationPushContext} $transferTypeExcludes(\variableMapping, t)$\;\label{algTranslateCompoundDeclarationTransfer} @@ -161,5 +160,5 @@ $next \assng TRANSLATE$\; } - \If{$ m = TRANSLATE$}{ + \If{$mode = TRANSLATE$}{ $translateCompoundContent(d, v, t, ca)$\; $popContext(\variableMapping)$\; @@ -167,16 +166,19 @@ $next \assng NONE$\; } - } \Return{$next$} \caption{Translating compound declarations (\IVML{translateCompoundDeclaration}).}\label{algTranslateCompoundDeclaration} \end{algorithm} -Algorithm \ref{algTranslateCompoundDeclaration} integrates the creation of the variable mapping, the constraint translation and the additional functionality for compound value changes controlled by the compound translation mode. Variable mapping and constraint translation are realized by separate algorithms (Algorithms \ref{algRegisterCompoundMapping} and \ref{algTranslateCompoundContent}, respectively) to enable their re-use when translating compound containers (cf. Section \ref{sectCompoundDefaults}). In more details, Algorithm \ref{algTranslateCompoundDeclaration} takes a compound variable $v$ of declaration $d$, an optional compound accessor $ca$, the actual type $t$ as well as the desired compound translation mode $m$ and returns the compound mode for a subsequent call of Algorithm \ref{algTranslateCompoundDeclaration}. A type $t$ is processed only if $t$ was not marked as already processed or, implicitly, recording of processed types is disabled (cf. Section \ref{sectVarMapping}). If a type shall not processed, the next compound mode is $NONE$, indicating that no context frame was created that needs to be popped during $TRANSLATE$. - -If the variable mapping shall be registered for type $t$, Algorithm \ref{algTranslateCompoundDeclaration} pushes a new context frame for the compound type onto the variable mapping stack $\variableMapping$ (line \ref{algTranslateCompoundDeclarationPushContext}). In line \ref{algTranslateCompoundDeclarationTransfer}, it modifies the actual context frame by enabling (transferring) excluded types (for faster re-scheduling) and storing $t$ as current type. Then it registers all required compound mappings using Algorithm \ref{algRegisterCompoundMapping} (using a joint accessor expression to $d$ in case that $ca=\undef$). The next compound mode after a registration of variable mappings is $TRANSLATE$. - -If constraints shall be translated, Algorithm \ref{algTranslateCompoundDeclaration} calls Algorithm \ref{algTranslateCompoundContent}, pops the previously created context, records $t$ as processed and returns that no further compound translation ($NONE$) is needed for $t$. - -We detail now the variable mapping for compounds. Algorithm \ref{algRegisterCompoundMapping} visits all slots and annotations of a given compound type $t$, creates access expressions for them and registers them with the current context frame in the variable mapping $\variableMapping$. The access expressions $ca$ is optional and, if given, utilized as prefix to create access expressions for slots and annotations. If $ca$ is not given, $e_d$ is used instead, usually containing an expression to the variable declaration using $t$. Algorithm \ref{algRegisterCompoundMapping} iterates over all slots defined for the given compound type $t$ including shadowed ones along the refinement hierarchy starting at $t$. If a slot already has a local access expression mapping (line \ref{algRegisterCompoundMappingExMapping}), it is shadowed and we just use the already registered more specific expression. If no mapping exists, Algorithm \ref{algRegisterCompoundMapping} a respective accessor for slot $s$. If the compound access expression $ca$ is not given, Algorithm \ref{algRegisterCompoundMapping} creates a static accessor based on $e_d$. The created accessor $x$ is then registered with $\variableMapping$. Similarly, we register accessors for annotations of the current slot $s$ based on the accessor $x$ for $s$. Finally, the algorithm creates accessors for all annotations declared for the underlying compound variable (through $e_d$). +Algorithm \ref{algTranslateCompoundDeclaration} is the main entry point into the constraint translation for compound types. The algorithm supports the two phases mentioned above, namely 1) the creation the variable mapping for a compound as well as 2) translating the constraints in the compound based on the variable mapping. Typically, these two phases are executed in immediate sequence, i.e., no distinct phases would be needed. However, in some situations, such as in Algorithm \ref{algTranslateDeclaration}, further translations must be performed in between. The compound mode indicates the phase to be executed, i.e., $REGISTER$ for the first phase and $TRANSLATE$ for the second phase. Further, in constraint re-scheduling, some compound types may be excluded from translation to speed up reasoning, i.e., for a certain type, no context frame is created in the first phase and also no context frame shall be released in the second phase. For convenience, Algorithm \ref{algTranslateCompoundDeclaration} integrates the two phases with the type exclusion and the conditional cleanup. The phases are realized by subsequent algorithms (Algorithms \ref{algRegisterCompoundMapping} and \ref{algTranslateCompoundContent}, respectively) to enable their re-use for the translation of compound containers (cf. Section \ref{sectCompoundDefaults}). + +In more details, Algorithm \ref{algTranslateCompoundDeclaration} takes a compound variable $v$ of declaration $d$ ($v$ may be $\undef$ for type-only translations\footref{fnVariableNull}), an optional compound accessor $ca$, the actual (compound) type $t$ as well as the desired compound translation $mode$. The algorithm returns the follow-up compound mode for the second phase. In both phases, compound type $t$ is processed only if $t$ was not marked before as processed or excluded. If $t$ shall not be processed, the resulting follow-up compound mode is $NONE$, indicating that $TRANSLATE$ shall not be executed, i.e., also no context frame cleanup shall happen. + +In $REGISTER$ mode, i.e., the variable mapping shall be created for compound type $t$, Algorithm \ref{algTranslateCompoundDeclaration} pushes a new context frame onto the variable mapping stack $\variableMapping$ (line \ref{algTranslateCompoundDeclarationPushContext}). In line \ref{algTranslateCompoundDeclarationTransfer}, the algorithm transferring excluded types into the actual context frame (cf. Section \ref{sectVarMapping}). Then the algorithm registers all required compound mappings by calling Algorithm \ref{algRegisterCompoundMapping} using as accessor expression either $ca$ if given or $\createExpression{d}$. The follow-up compound mode after a creation of variable mappings is $TRANSLATE$. + +In $TRANSLATE$ mode, all constraints of compound type $t$ shall be translated. Therefore, Algorithm \ref{algTranslateCompoundDeclaration} calls Algorithm \ref{algTranslateCompoundContent}, pops the previously created context, records $t$ as processed and returns that no further compound translation is needed for $t$ ($NONE$) . + +\subsubsection{Registering Compound Accessor Expressions}\label{sectionRegCompAcc} + +We detail now the variable mapping for compound types. Algorithm \ref{algRegisterCompoundMapping} visits all slots and annotations of a given compound type $t$, creates access expressions for them and registers them with the current context frame in the variable mapping $\variableMapping$. The access expressions $ca$ is optional and, if given, utilized as prefix to create access expressions for slots and annotations. If $ca$ is not given, $e_d$ is used instead, usually containing an expression to the variable declaration using $t$. Algorithm \ref{algRegisterCompoundMapping} iterates over all slots defined for the given compound type $t$ including shadowed ones along the refinement hierarchy starting at $t$. If a slot already has a local access expression mapping (line \ref{algRegisterCompoundMappingExMapping}), it is shadowed and we just use the already registered more specific expression. If no mapping exists, Algorithm \ref{algRegisterCompoundMapping} a respective accessor for slot $s$. If the compound access expression $ca$ is not given, Algorithm \ref{algRegisterCompoundMapping} creates a static accessor based on $e_d$. The created accessor $x$ is then registered with $\variableMapping$. Similarly, we register accessors for annotations of the current slot $s$ based on the accessor $x$ for $s$. Finally, the algorithm creates accessors for all annotations declared for the underlying compound variable (through $e_d$). Given a complete mapping for compound type $t$, we can transform the constraints, i.e., apply Algorithm \ref{algTranslateCompoundContent}. As mentioned above, the algorithm first translates all default value expressions of slots, then the default values from annotation assignments, and, finally, the constraints in eval blocks with higher evaluation priority as well as the remaining nested constraints. When translating the default value expression for slots, Algorithm \ref{algTranslateCompoundContent} calls Algorithm \ref{algTranslateDeclaration}, and, thus, triggers a potentially recursive translation along the respective slot types, in particular in case of compound or container slots. @@ -204,4 +206,6 @@ \caption{Registering the compound mapping (\IVML{registerCompoundMapping}).}\label{algRegisterCompoundMapping} \end{algorithm} + +\subsubsection{Translating Compound Constraints}\label{sectionTransComp} Let