Index: /reasoner/consRescheduling.tex =================================================================== --- /reasoner/consRescheduling.tex (revision 161) +++ /reasoner/consRescheduling.tex (revision 162) @@ -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}\footnote{In the implementation, a combination of a visitor and a listener in \class{RescheduleValueChangeVisitor.java}.} is called. +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}.}. \begin{algorithm}[H] @@ -42,15 +42,27 @@ \KwIn{parent variable $v_p$, decision variable $v$, old value $val_o$, clear flag $clear$} - $t_n \assng type(value(v)))$\; - \uIf{$isConstraint(t_c)$} { - $rescheduleConstraintValue(v_p, v, clear)$\; - } \uElseIf{$isCompound(t_c)$}{ - $rescheduleCompoundValue(v, val_o)$\; - } \uElseIf{$isContainer(t_c)$}{ - $rescheduleContainerValue(v, val_o)$\; - } + $t_n \assng type(value(v)))$\; + \uIf{$isConstraint(t_n)$} {\label{algRescheduleContainerValueConsStart} + $rescheduleConstraintValue(v_p, v, clear)$\; \label{algRescheduleContainerValueConsEnd} + } \uElseIf{$isCompound(t_n)$}{ \label{algRescheduleContainerValueCompStart} + \ForAll{$s\iterAssng slots(value(v))$}{ + \If{$value(s) \neq \undef$}{ + $rescheduleValueChange(v, s, value(s), true)$\; + } + } \label{algRescheduleContainerValueCompEnd} + } \uElseIf{$isContainer(t_n) \wedge isContainer(type(val_o))$}{\label{algRescheduleContainerValueContStart} + $first \assng true$\; + \ForAll{$c \iterAssng elements(val_n), o \iterAssng elements(val_o)$} { + $rescheduleValueChange(v, c, o, first)$\; + $first \assng false$\; + } + }\label{algRescheduleContainerValueContEnd} \caption{Reschedule a value change (\IVML{rescheduleValueChange}).}\label{algRescheduleContainerValue} \end{algorithm} + +Algorithm \ref{algRescheduleContainerValue} 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. + +For this purpose, Algorithm \ref{algRescheduleContainerValue} receives the changed variable $v$, its optional parent variable $v_p$ (if $v$ is nested into $p$), the old value $val_o$ and a flag that indicates whether existing constraints shall be cleared within this call. If $val_n$ is a constraint, the algorithm calls Algorithm \ref{algRescheduleConstraintValue} (lines \ref{algRescheduleContainerValueConsStart}-\ref{algRescheduleContainerValueConsEnd}). If $val_n$ is a compound, the algorithm calls itself recursively for all slots that have a value assigned (lines \ref{algRescheduleContainerValueCompStart}-\ref{algRescheduleContainerValueCompEnd}). Finally, if $val_n$ is a container, the algorithm iterates over the elements in the new and the old value (assuming that at least all elements in $val_n$ are considered, eventually $val_o$ is $\undef$ then) and calls itself recursively for each pair (lines \ref{algRescheduleContainerValueContStart}-\ref{algRescheduleContainerValueContEnd}). Existing constraints are cleared only for the first element pair ($first$). \begin{algorithm}[H] @@ -59,11 +71,9 @@ \KwData{scope assignments $\scopeAssignments$, relevant constraints $\relevantConstraintsPerDeclaration$ and $\relevantConstraintVariables$} - \If{$isConstraint(type(v)$} { - $cs \assng obtainConstraints(v_p, clear, \undef)$ \MISSING{!}\; + $obtainConstraints(v_p, clear, \undef)$ \MISSING{!}\; $ex \assng getConstraintValueConstraintExpression(value(v))$ \MISSING{!}\; \If{$ex \neq \undef$}{ - \lIf{$cs = \undef \vee |cs|=0$}{$p\assng parent(decl(v))$}\lElse{$parent(cs[0])$} $ex_p \assng createParentExpression(v)$\; - $c \assng createConstraintVariableConstraint(ex, ex_p, \undef, p, v_p)$ \MISSING{!}\; + $c \assng createConstraintVariableConstraint(ex, ex_p, v_p)$\; $setValue(v, c)$\; $base \assng base \addSeq \otherConstraints$\; @@ -73,39 +83,38 @@ $\otherConstraints \assng \emptySet$\; } - } \caption{Reschedule a constraint value (\IVML{rescheduleConstraintValue}).}\label{algRescheduleConstraintValue} \end{algorithm} -\begin{algorithm}[H] - \SetAlgoLined - \KwIn{decision variable $v$, old value $val_o$} - \KwData{scope assignments $\scopeAssignments$, relevant constraints $\relevantConstraintsPerDeclaration$ and $\relevantConstraintVariables$} +%\begin{algorithm}[H] +% \SetAlgoLined +% \KwIn{decision variable $v$, old value $val_o$} +% \KwData{scope assignments $\scopeAssignments$, relevant constraints $\relevantConstraintsPerDeclaration$ and $\relevantConstraintVariables$} +% +% \If{$isCompound(v)$}{ +% \ForAll{$s\iterAssng slots(value(v))$}{ +% \If{$value(s) \neq \undef$}{ +% $rescheduleValueChange(s, s, value(s), true);$\; +% } +% } +% } +% \caption{Reschedule a compound value (\IVML{rescheduleCompoundValue}).}\label{algCompoundValue} +%\end{algorithm} - \If{$isCompound(v)$}{ - \ForAll{$s\iterAssng slots(value(v))$}{ - \If{$value(s) \neq \undef$}{ - $rescheduleValueChange(s, s, value(s), true);$\; - } - } - } - \caption{Reschedule a compound value (\IVML{rescheduleCompoundValue}).}\label{algCompoundValue} -\end{algorithm} +%\begin{algorithm}[H] +% \SetAlgoLined +% \KwIn{decision variable $v$, old value $val_o$} +% \KwData{scope assignments $\scopeAssignments$, relevant constraints $\relevantConstraintsPerDeclaration$ and $\relevantConstraintVariables$} +% +% $val_n \assng value(v))$\; +% \If{$isContainer(type(val_n)) \wedge isContainer(type(val_o))$}{ +% $first \assng true$\; +% \ForAll{$c \iterAssng elements(val_n), o \iterAssng elements(val_o)$} { +% $rescheduleValueChange(v, c, o, first)$\; +% $first \assng false$\; +% } +% } -\begin{algorithm}[H] - \SetAlgoLined - \KwIn{decision variable $v$, old value $val_o$} - \KwData{scope assignments $\scopeAssignments$, relevant constraints $\relevantConstraintsPerDeclaration$ and $\relevantConstraintVariables$} - - $val_n \assng value(v))$\; - \If{$isContainer(type(val_n)) \wedge isContainer(type(val_o))$}{ - $first \assng true$\; - \ForAll{$c \iterAssng elements(val_n), o \iterAssng elements(val_o)$} { - $rescheduleValueChange(v, c, o, first)$\; - $first \assng false$\; - } - } - - \caption{Reschedule a container value (\IVML{rescheduleContainerValue}).}\label{algContainerValue} -\end{algorithm} +% \caption{Reschedule a container value (\IVML{rescheduleContainerValue}).}\label{algContainerValue} +%\end{algorithm} \begin{algorithm}[H] Index: /reasoner/consTranslation.tex =================================================================== --- /reasoner/consTranslation.tex (revision 161) +++ /reasoner/consTranslation.tex (revision 162) @@ -489,5 +489,5 @@ } -In more details, Algorithm \ref{algCreateConstraintVariableConstraint} takes a constraint expression (e.g., the default value of a variable or a nested variable through Algorithm \ref{algTranslateDeclaration}), an optional expression $e_f$ representing \IVMLself{} and the variable $v$ the translation is applied to. 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$. 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. Finally, in line \ref{algCreateConstraintVariableConstraintRegister}, the relationship between the underlying variable $v$ and the constraint is recorded to enable efficient updates of the constraint base upon value change (cf. Algorithm \ref{algVarChange}). +In more details, Algorithm \ref{algCreateConstraintVariableConstraint}\footnote{Here we abstract two implementation parameters for the self value/expression into one parameter and omit the parameter indicating the parent instance of the constraint to be created.} takes a constraint expression (e.g., the default value of a variable or a nested variable through Algorithm \ref{algTranslateDeclaration}), an optional expression $e_f$ representing \IVMLself{} and the variable $v$ the translation is applied to. 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$. 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. Finally, in line \ref{algCreateConstraintVariableConstraintRegister}, the relationship between the underlying variable $v$ and the constraint is recorded to enable efficient updates of the constraint base upon value change (cf. Algorithm \ref{algVarChange}). \begin{algorithm}[H] @@ -529,4 +529,8 @@ 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 (\IVML{self} is currently not supported 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}. \begin{algorithm}[H] @@ -552,6 +556,4 @@ \end{algorithm} -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}. - %\begin{algorithm}[H] % \KwIn{constraint sequence $s$, constraint sequence $c$, perform initializers $check$} @@ -563,7 +565,7 @@ %\end{algorithm} -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}. - 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. % \begin{align*} @@ -580,9 +582,6 @@ \end{align*} % -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. 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. - -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. \begin{algorithm}[H] @@ -605,2 +604,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.