Index: /reasoner/consRescheduling.tex =================================================================== --- /reasoner/consRescheduling.tex (revision 160) +++ /reasoner/consRescheduling.tex (revision 161) @@ -1,10 +1,5 @@ \section{Constraint Re-scheduling}\label{sectTopLevelConstraintsRescheduling} -When variable $v$ is changed as side effect of a constraint evaluation during reasoning, Algorithm \ref{algVarChange} is called. - - -If the changed variable is not local, i.e., neither a parameter of a user-defined function, an iterator of a container operation nor a local variable defined in a let-expression, the variable is relevant for re-scheduling. First, Algorithm \ref{algVarChange} registers in line \ref{algVarChangeScope} the change of $v$ within the actual project scope if the value of $v$ actually has been affected by reasoning. This scope information is used by the evaluator prior to a variable assignment to check for illegal duplicate assignments within the same scope. Then, if the value actually changed, we identify constraints that must be added to or removed from the constraint base. This may be due to nested constraint values (line \ref{algVarChangeRescheduleConstraintVariables}) in the new value as well as a type change of a compound value along the refinement hierarchy, which may require more or less constraints to be considered (line \ref{algVarChangeRescheduleValueTypeChange}). All these cases may affect the relevant constraints. When adding or removing constraints, new constraints are added to $\relevantConstraintVariables$ and $\relevantConstraintsPerDeclaration$, while now now irrelevant constraints are identified via $\relevantConstraintVariables$ and also removed from $\relevantConstraintVariables$ and $\relevantConstraintsPerDeclaration$. Finally , parent (line \ref{algVarChangeRescheduleParents}) and nested (line \ref{algVarChangeRescheduleNested}) constraints may need to be re-scheduled, too, if the related variables aside from constraint variables changed. This happens through a lookup to $\relevantConstraintsPerDeclaration$, implying that previously added / removed constraints due to value type changes are not re-scheduled. - -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 mapping\footnote{Technically, a local decision variable wraps either a value (if the evaluation runs over constants) or a decision variables. To allow for (call-by-reference) propagation on nested slots and attributes, changing the context registration actually refers to the actually wrapped decision variable, but this is not detailed here.}. +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}\footnote{In the implementation, a combination of a visitor and a listener in \class{RescheduleValueChangeVisitor.java}.} is called. \begin{algorithm}[H] @@ -13,11 +8,11 @@ \KwData{scope assignments $\scopeAssignments$, relevant constraints $\relevantConstraintsPerDeclaration$ and $\relevantConstraintVariables$} - \If{$\neg isLocal(v)$}{ + \uIf{$\neg isLocal(v)$}{ $addAssignment(\scopeAssignments, v)$\; \label{algVarChangeScope} %addScopeAssignment $val_n \assng value(v)$\; \If{$val_n \neq val_o$} { $rescheduleValueChange(v, v, true)$\; \label{algVarChangeRescheduleConstraintVariables} - \If{$isValueTypeChange(v, val_n, val_o)$ \MISSING{!}} { - $rescheduleValueTypeChange(v, val_n, val_o)$ \MISSING{!}\; \label{algVarChangeRescheduleValueTypeChange} + \If{$isValueTypeChange(v, val_n, val_o)$ } { + $rescheduleValueTypeChange(v, val_n, val_o)$\; \label{algVarChangeRescheduleValueTypeChange} } } @@ -30,4 +25,16 @@ \caption{Adjusting the constraint base (\IVML{notifyChanged}).}\label{algVarChange} \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. + +\begin{align*} +is&ValueTypeChange(v, val_n, val_o) = \\&\begin{cases} val_o \neq \undef \wedge~val_n \neq \undef \wedge~type(val_o) \neq type(val_n) & isCompound(type(v))\\ false & \text{else}\end{cases} +\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. \begin{algorithm}[H] @@ -46,5 +53,4 @@ \caption{Reschedule a value change (\IVML{rescheduleValueChange}).}\label{algRescheduleContainerValue} \end{algorithm} - \begin{algorithm}[H] @@ -102,2 +108,9 @@ \caption{Reschedule a container value (\IVML{rescheduleContainerValue}).}\label{algContainerValue} \end{algorithm} + +\begin{algorithm}[H] + \SetAlgoLined + \caption{Reschedule a value type change (\IVML{rescheduleValueTypeChange}).}\label{algRescheduleValueTypeChange} + \MISSING{Algorithm}\\ + +\end{algorithm}