Index: /reasoner/consRescheduling.tex =================================================================== --- /reasoner/consRescheduling.tex (revision 164) +++ /reasoner/consRescheduling.tex (revision 165) @@ -35,7 +35,7 @@ \end{align*} -If the type of the value changed (see function $isValueTypeChange$ above), we call Algorithm \ref{algRescheduleValueTypeChange} 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{algRescheduleValueTypeChange} is called, the involved constraint translations will consider the changed $\variableMapping$ in their variable substitutions and replace unbound iterator variables. +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. \begin{algorithm}[H] @@ -138,5 +138,14 @@ %\end{algorithm} -\MISSING{Text for Algorithm \ref{algTranslateValueTypeChange}, hint to impl \class{Resolver.java}, also obtainConstraints} +When the value of variable $v$ changes, also its actual type may change, in particular if $v$ is a compound variable. If the differing types also specify different constraints, the reasoner must adjust the constraint set accordingly. Moreover, a type change may also be caused when the value is changed from or to the IVML value \IVMLnull{} (different from $\undef$ / null of the implementing programming language). In these cases, a configed value is explicitly replaced by nothing (no configuration) or \IVMLnull{} is replaced by a certain value. Algorithm \ref{algTranslateValueTypeChange} handles these four cases\footnote{\label{fnVisibilityResolver}Due to technical reasons, in particular the visibility of involved attributes, this algorithm is realized in \class{Resolver.java} rather than \class{RescheduleValueChangeVisitor}.}, i.e., changing from / to \IVMLnull{} or changing the actual type up- or down the type hierarchy. Generally, all cases could be handled by first removing all existing constraints and then executing the constraint translation from Section \ref{sectTranslation}. However, this can lead to unnecessary creation of already scheduled or even successfully evaluated constraints, i.e., inefficient or even wrong reasoning situations. To avoid such transformations, Algorithm \ref{algTranslateValueTypeChange} operates on the difference among the involved types, i.e., in particular if the type changes along the refinement hierarchy, it identifies the types in between the old and the new type in the type hierarchy and either creates constraints or removes constraints according to the differnce. + +In details, Algorithm \ref{algTranslateValueTypeChange} receives the changed variable $v$, and, as already available in the caller, the new value $val_n$ and the old value $val_o$ of $v$. Algorithm \ref{algTranslateValueTypeChange} is only called (by Algorithm \ref{algVarChange} in line \ref{algVarChangeRescheduleValueTypeChange}) if the types of $val_o$ and $val_n$ differ, i.e., in particular not if the types are equal. As mentioned above, Algorithm \ref{algTranslateValueTypeChange} distinguishes four cases: + +\begin{enumerate} + \item The new value is \IVMLnull{} (lines \ref{algTranslateValueTypeChangeNewNullStart}-\ref{algTranslateValueTypeChangeNewNullEnd}): Due to the type change, an existing value was removed from the configuration, i.e., we must identify all constraints related to $v$ and remove them from the constraint base. This happens by calling Algorithm \ref{algObtainConstraints}. + \item The old value is \IVMLnull{} (lines \ref{algTranslateValueTypeChangeOldNullStart}-\ref{algTranslateValueTypeChangeNewNullStart}): The value of $v$ was removed before the value change and now $v$ is configured again, i.e., we can just add all constraints for $v$ calling the constraint transformation in terms of Algorithm \ref{algTranslateDeclaration}. However, as $v$ was initialized before, we can omit all initializing constraints and apply a transformation for incremental reasoning.To continue reasoning in the correct mode, we save first the $inc$ flag, change it to indicate incremental reasoning, call then the constraint translation and set $inc$ back to its saved value. + \item The old value is of a more general type than the new value (lines \ref{algTranslateValueTypeChangeOldHigherStart}-\ref{algTranslateValueTypeChangeOldHigherEnd}): In this case, we just have to add the constraints for the currently missing types between $t_o$ and $t_n$ in the type hierarchy. As the constraint translation allows excluding types from the translation, we just reverse the idea, i.e, we perform a constraint translation calling Algorithm \ref{algTranslateDeclaration}, but exclude $t_o$ and all its refined types. As the excluded types are internally transferred into a temporary context frame created during the translation in Algorithm \ref{algTranslateCompoundDeclaration}, we do not have to reset the type exclusion. Again we switch the translation to incremental mode as $v$ already has been configured with a value. + \item The new value is of a more general type than the old value (lines \ref{algTranslateValueTypeChangeOldLowerStart}-\ref{algTranslateValueTypeChangeOldLowerEnd}): The constraint base may now contain constraints for $v$ originating from more specific types than $t_n$. Therefore, we remove all constraints related to types below $t_n$ and in between $t_n$ and $t_o$ in the type hierarchy. This is achieved by Algorithm \ref{algObtainConstraints}, which provides a filter mechanism to remove only constraints that have attached one out of a given set of types (here, the difference between all refined types of $t_o$ and $t_n$). The required type information was attached to the constraints by Algorithm \ref{algTranslateCompoundContent} during a previous constraint translation. +\end{enumerate} \begin{algorithm}[H] @@ -145,25 +154,23 @@ \KwData{incremental flag $inc$, variable mapping $vm$} $t_n \assng type(val_n)$; $t_o \assng type(val_o)$\; - \uIf{$val_n = \IVMLnull{}$}{ - $obtainConstraints(v, true, null)$\; - }\uElseIf{$val_o = \IVMLnull{}$} { + \uIf{$val_n = \IVMLnull{}$}{ \label{algTranslateValueTypeChangeNewNullStart} + $obtainConstraints(v, true, \undef)$\; \label{algTranslateValueTypeChangeNewNullEnd} + }\uElseIf{$val_o = \IVMLnull{}$} { \label{algTranslateValueTypeChangeOldNullStart} $inc_o \assng inc$; $inc \assng true$\; - $translateDeclaration(decl(v), v, null)$\; - $inc \assng inc_o$\; - }\uElseIf{$\subTypeEqOf{t_o}{t_n}$} { - $t_r \assng allRefines^+(t_o) \setminus \set{t_n}$\; - $setTypeExcludes(\variableMapping, t_r)$\; + $translateDeclaration(decl(v), v, \undef)$\; + $inc \assng inc_o$\;\label{algTranslateValueTypeChangeOldNullEnd} + }\uElseIf{$\subTypeEqOf{t_o}{t_n}$} {\label{algTranslateValueTypeChangeOldHigherStart} + $setTypeExcludes(\variableMapping, allRefines^+(t_o))$\; $inc_o \assng inc$; $inc \assng true$\; - $translateDeclaration(decl(v), v, null)$\; - $inc \assng inc_o$\; - }\Else{ - $t_r \assng allRefines^+(t_o) \setminus \set{t_n}$\; - $obtainConstraints(v, true, r_t)$\; - } + $translateDeclaration(decl(v), v, \undef)$\; + $inc \assng inc_o$\;\label{algTranslateValueTypeChangeOldHigherEnd} + }\Else{\label{algTranslateValueTypeChangeOldLowerStart} + $obtainConstraints(v, true, allRefines^+(t_o) \setminus allRefines^+(t_n))$\; + }\label{algTranslateValueTypeChangeOldLowerEnd} \caption{Translate a value type change (\IVML{translateValueTypeChange}).}\label{algTranslateValueTypeChange} \end{algorithm} -During constraint re-scheduling, old constraints must be processed or even removed from the constraint base and the lookup structures ($\relevantConstraintVariables, \relevantConstraintsPerDeclaration$) as well as the problem records. Sometimes, as for the re-scheduling of type changes in Algorithm \ref{algRescheduleValueTypeChange}, even just a subset of constraints according to given types must be removed. Algorithm \ref{algObtainConstraints} performs these tasks. It receives the changed variable $v$, a $clear$ flag indicating whether the constraints for $v$ shall be removed as well as an optional set $f$ of (compound) types that acts as filter, i.e., only constraints attached to one of the types in that set are removed. First, Algorithm \ref{algObtainConstraints} obtains the relevant variables. Then, if enabled by $clear$, the algorithm removes the (filtered) constraints from the constraint base and the lookup data structures. The algorithm returns the constraints related to $v$ that were not cleared. +During constraint re-scheduling, old constraints must be processed or even removed from the constraint base and the lookup structures ($\relevantConstraintVariables, \relevantConstraintsPerDeclaration$) as well as the problem records. Sometimes, as for the re-scheduling of type changes in Algorithm \ref{algTranslateValueTypeChange}, even just a subset of constraints according to given types must be removed. Algorithm \ref{algObtainConstraints} performs these tasks. It receives the changed variable $v$, a $clear$ flag indicating whether the constraints for $v$ shall be removed as well as an optional set $f$ of (compound) types that acts as filter, i.e., only constraints attached to one of the types in that set are removed. First, Algorithm \ref{algObtainConstraints} obtains the relevant variables\footref{fnVisibilityResolver}. Then, if enabled by $clear$, the algorithm removes the (filtered) constraints from the constraint base and the lookup data structures. The algorithm returns the constraints related to $v$ that were not cleared. Typically, constraints that are related to $v$ for rescheduling can be identified easily via $\relevantConstraintVariables[v]$. However, if $v$ is nested in a container, i.e., represents some nested container element, the constraints may (for technical reasons) actually be related to (one of) the enclosing container variables. Thus, in lines \ref{algObtainConstraintsFindStart}-\ref{algObtainConstraintsFindEnd}, Algorithm \ref{algObtainConstraints} identifies the constraints $cs$ of the next enclosing variable (starting with $v$). If such a set exists and clearing is enabled (lines \ref{algObtainConstraintsClearStart}-\ref{algObtainConstraintsClearEnd}), the algorithm filters $cs$ if requested and removes then all constraints in $cs$ from the constraint base. If filtering is enabled, only those constraints are futher relevant that are attached\footnote{Types are attached to constraints during the translation of compound types in function $translateCmp$ of Algorithm \ref{algTranslateCompoundContent}.} to one of the types in $f$ (line \ref{algObtainConstraintsFilter}). Then the constraints in $cs$ are removed from the constraint $base$ (line \ref{algObtainConstraintsRemoveFromBase}), from the set of problem constraints indicating reasoning errors (line \ref{algObtainConstraintsRemoveFromProblemConstraints}), from the bi-directional constraint variable mapping $\relevantConstraintVariables$ (lines \ref{algObtainConstraintsRemoveFromConstraintVarsStart}-\ref{algObtainConstraintsRemoveFromConstraintVarsEnd}) and from the dependent constraints $\relevantConstraintsPerDeclaration$ (line \ref{algObtainConstraintsRemoveFromConstraintsPerDecl}). Finally, after clearing all constraints, $cs$ can be cleared as no remainng registered constraints are left over (line \ref{algObtainConstraintsClearResult}).