Index: /reasoner/consRescheduling.tex =================================================================== --- /reasoner/consRescheduling.tex (revision 223) +++ /reasoner/consRescheduling.tex (revision 224) @@ -58,5 +58,5 @@ \subsection{Configuration Variable Value Changes}\label{sectReSchedComp} -Algorithm \ref{algRescheduleValueChange} is responsible for re-scheduling constraint values contained in 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. +Algorithm \ref{algRescheduleValueChange} is responsible for re-scheduling constraint values contained in a given IVML value. Therefore, all contained constraints must be identified. As complex IVML values can be nested, the idea is to follow nested value structures recursively, to extract constraint values and to add them after variable substitution to the constraint base. \begin{algorithm}[H] @@ -81,15 +81,15 @@ }\label{algRescheduleValueChangeContEnd} - \caption{Reschedule a value change (\IVML{rescheduleValueChange}).}\label{algRescheduleValueChange} -\end{algorithm} - - -Algorithm \ref{algRescheduleValueChange} receives the changed variable $v$, its optional parent variable $v_p$ (if $v$ is nested into $p$), the old value $val_o$ and the flag $clear$ that indicates whether existing constraints shall be cleared within this call. For container variables, $clear$ shall only be true for the first element to avoid clearing again constraints for elements that already have been processed for the same container. - -If $val_n$ is a constraint, the algorithm calls in lines \ref{algRescheduleValueChangeConsStart}-\ref{algRescheduleValueChangeConsEnd} the algorithm for constraint value changes, i.e., Algorithm \ref{algRescheduleConstraintValue} (cf. Section \ref{sectReSchedConstr}). If $val_n$ is a compound, the algorithm calls itself recursively for all slots that have a value assigned (lines \ref{algRescheduleValueChangeCompStart}-\ref{algRescheduleValueChangeCompEnd}). 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{algRescheduleValueChangeContStart}-\ref{algRescheduleValueChangeContEnd}). Existing constraints are cleared only for the first element ($first$). + \caption{Reschedule a configuration value change (\IVML{rescheduleValueChange}).}\label{algRescheduleValueChange} +\end{algorithm} + + +Algorithm \ref{algRescheduleValueChange} receives the changed variable $v$, its optional parent variable $v_p$ (if $v$ is nested), the old value $val_o$ and $clear$, a flag that indicates whether existing constraints shall be cleared in this call. For container variables, $clear$ shall only be true for the first element to avoid accidentally clearing constraints for container elements that already have been processed. + +If $val_n$ is a constraint, the algorithm calls in lines \ref{algRescheduleValueChangeConsStart}-\ref{algRescheduleValueChangeConsEnd} the algorithm for constraint value changes, i.e., Algorithm \ref{algRescheduleConstraintValue} (cf. Section \ref{sectReSchedConstr}). If $val_n$ is a compound, the algorithm calls itself recursively for all slots that have a value assigned (lines \ref{algRescheduleValueChangeCompStart}-\ref{algRescheduleValueChangeCompEnd}). Finally, if $val_n$ is a container, the algorithm iterates over the elements in the new and the old value (at least all elements in $val_n$ are considered, eventually $val_o$ or $val_n$ is $\undef$) and calls itself recursively for each pair of old and new value (lines \ref{algRescheduleValueChangeContStart}-\ref{algRescheduleValueChangeContEnd}). Existing constraints are cleared only for the $first$ pair. \subsection{Constraint Value Changes}\label{sectReSchedConstr} -Algorithm \ref{algRescheduleConstraintValue} targets re-scheduling a constraint value. This involves replacing existing constraints for a given variable $v$ by a new constraint instantiated using variable substitution. In more details, Algorithm \ref{algRescheduleConstraintValue} receives the changed variable $v$, its optional parent variable $v_p$ and a flag whether existing constraints shall be cleared (if this function is called repeatedly on the same $v_p$, e.g., for all slots of a compound). +Algorithm \ref{algRescheduleConstraintValue} is called for a value of a constraint variable, i.e., the new constraint shall replace the old one in the constraint base. This involves instantiating the new constraint using variable substitution. In more details, Algorithm \ref{algRescheduleConstraintValue} receives the changed variable $v$, its optional parent variable $v_p$ and the flag $clear$, again indicating whether existing constraints shall be cleared in the current execution. \begin{algorithm}[H] @@ -98,5 +98,5 @@ \KwData{constraint base $base$, other constraints $\otherConstraints$ and relevant constraints per declaration $\relevantConstraintsPerDeclaration$} - $obtainConstraints(v_p, clear, \undef)$\; \label{algRescheduleConstraintValueClear} + $cleanupConstraints(v_p, clear, \undef)$\; \label{algRescheduleConstraintValueClear} $e \assng getConstraintValueExpression(value(v))$\; \If{$e \neq \undef$}{ @@ -114,5 +114,5 @@ \end{algorithm} -Algorithm \ref{algRescheduleConstraintValue} accesses the existing constraints of the parent variable and clears them in line \ref{algRescheduleConstraintValueClear} from the constraint base and $\relevantConstraintsPerDeclaration$ if requested using Algorithm \ref{algObtainConstraints}. Then it determines a constraint expression for the given value, i.e., it extracts a constraint or a constant boolean expression from the given value as shown below\footnote{For the implementation, constraint value and Boolean value are two differently typed instances that require different code to obtain a constraint expression.}: +Algorithm \ref{algRescheduleConstraintValue} accesses the existing constraints of the parent variable and (conditionally via $clear$) removes them in line \ref{algRescheduleConstraintValueClear} from the constraint base as well as from $\relevantConstraintsPerDeclaration$ using Algorithm \ref{algCleanupConstraints}. Then the algorithm determines a constraint expression for the given value, i.e., it extracts a constraint or a constant Boolean expression from the given value as shown below\footnote{For the implementation, constraint value and Boolean value are two differently typed instances that require different code to obtain a constraint expression.}: % \begin{align*} @@ -126,7 +126,38 @@ \end{align*} % - From the constraint expression $e$, the parent access expression $e_p$ and the parent variable $v_p$, Algorithm \ref{algRescheduleConstraintValue} creates in line \ref{algRescheduleConstraintValueCreateConstraint} a constraint by calling Algorithm \ref{algCreateConstraintVariableConstraint}. Algorithm \ref{algCreateConstraintVariableConstraint} performs the variable substitution, registers the constraint appropriately and adds the constraint to $\otherConstraints$ (as for the initial translations, to be cleared later). To correct constraints with unbound iterator variables, Algorithm \ref{algRescheduleConstraintValue} changes in line \ref{algRescheduleConstraintValueChangeValue} the value of $v$ in a way that avoids re-triggering the constraint re-scheduling Algorithm \ref{algVarChange}, i.e., prevents an accidental recursion. Finally, Algorithm \ref{algRescheduleConstraintValue} takes over the new constraint into the constraint base in line \ref{algRescheduleConstraintValueAdd}, corrects the constraint registration in $\relevantConstraintsPerDeclaration$ for $v$ and all its parents (lines \ref{algRescheduleConstraintValueCorrectStart}-\ref{algRescheduleConstraintValueCorrectEnd}) so so that future re-scheduling of dependent constraints can take the new constraint into account and clears $\otherConstraints$ in line \ref{algRescheduleConstraintValueClearCo} for future calls. - - + From the constraint expression $e$, the parent access expression $e_p$ and the parent variable $v_p$, Algorithm \ref{algRescheduleConstraintValue} creates in line \ref{algRescheduleConstraintValueCreateConstraint} a constraint by calling Algorithm \ref{algCreateConstraintVariableConstraint}. Algorithm \ref{algCreateConstraintVariableConstraint} performs the variable substitution, registers the constraint appropriately and adds the constraint to (the empty) $\otherConstraints$ as a side effect. Due to local variable changes registered in $\variableMapping$ by Algorithm \ref{algVarChange}, potentially unbound variables in container values (cf. Section \ref{sectConstraintVariables}) are bound by the substitution performed in Algorithm \ref{algRescheduleConstraintValue}. However, the final constraint variable value arising from this substitution must still be stored in $v$. This happens in line \ref{algRescheduleConstraintValueChangeValue} in a way that avoids re-triggering the constraint re-scheduling, i.e., prevents an accidentally unlimited recursion. Then, Algorithm \ref{algRescheduleConstraintValue} takes over the new constraint into the constraint base in line \ref{algRescheduleConstraintValueAdd}. It also adjusts the registered constraints in $\relevantConstraintsPerDeclaration$ for $v$ and all its parents (lines \ref{algRescheduleConstraintValueCorrectStart}-\ref{algRescheduleConstraintValueCorrectEnd}) so that future re-scheduling of dependent constraints takes the new constraint into account. Finally, the algorithm clears $\otherConstraints$ in line \ref{algRescheduleConstraintValueClearCo} for further (side-effect) calls of Algorithm \ref{algCreateConstraintVariableConstraint}. + +During constraint re-scheduling, superfluous constraints must be removed from the constraint base, the lookup structures ($\relevantConstraintVariables, \relevantConstraintsPerDeclaration$) as well as the problem records. As we will see in Section \ref{sectReSchedType}, sometimes even just a subset of constraints according to given types must be removed. Algorithm \ref{algCleanupConstraints} performs these support tasks. It receives the changed variable $v$ and a $clear$ flag indicating whether the constraints for $v$ shall be removed. Further, the algorithm may receive an optional set $f$ of (compound) types that acts as filter, i.e., only constraints having one of these types attached\footnote{Types are attached to constraints during the translation of compound types in function $translateCmp$ of Algorithm \ref{algTranslateCompoundContent}.} are removed. The algorithm returns all constraints related to $v$ if the $clear$ flag is $false$, else an empty set as the requested constraints were removed. + +First, Algorithm \ref{algCleanupConstraints} obtains the involved constraints from $v$ or one of the parents of $v$\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}.}. 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 container element, the constraints may (for technical reasons) actually be related to (one of) the enclosing container variables. Thus, in lines \ref{algCleanupConstraintsFindStart}-\ref{algCleanupConstraintsFindEnd}, Algorithm \ref{algCleanupConstraints} identifies the constraints $cs$ from the next enclosing variable (starting with $v$). If such a set exists and clearing is enabled (lines \ref{algCleanupConstraintsClearStart}-\ref{algCleanupConstraintsClearEnd}), the algorithm filters $cs$ if requested (line \ref{algCleanupConstraintsFilter}) and removes then all remaining constraints in $cs$ from the constraint $base$ (line \ref{algCleanupConstraintsRemoveFromBase}), from the set of problem constraints indicating reasoning errors (line \ref{algCleanupConstraintsRemoveFromProblemConstraints}), from the bi-directional constraint variable mapping $\relevantConstraintVariables$ (lines \ref{algCleanupConstraintsRemoveFromConstraintVarsStart}-\ref{algCleanupConstraintsRemoveFromConstraintVarsEnd}) and from the dependent constraints $\relevantConstraintsPerDeclaration$ (line \ref{algCleanupConstraintsRemoveFromConstraintsPerDecl}). Finally, after clearing all constraints, $cs$ can be cleared as no remainng registered constraints are left over (line \ref{algCleanupConstraintsClearResult}). + +\begin{algorithm}[H] + \SetAlgoLined + \KwIn{variable $v$, flag $clear$, filter type set $f$} + \KwData{constraint $base$, relevant constraints $\relevantConstraintVariables, \relevantConstraintsPerDeclaration$, problem records $m$} + \KwOut{persisting constraints of $v$ (if $\neg clear$)} + $i \assng v$; $cs \assng \undef$\; \label{algCleanupConstraintsFindStart} + \Repeat{$cs = \undef \wedge~i \neq \undef$}{ + $cs \assng \relevantConstraintVariables[i]$\; + $i \assng parent(i)$\; + }\label{algCleanupConstraintsFindEnd} + \If{$clear \wedge~cs \neq \undef$}{ \label{algCleanupConstraintsClearStart} + %filter for attached + \lIf{$f \neq \undef$} {$cs \assng \setWith{c}{c \in cs \wedge attached(c) \in f}$}\label{algCleanupConstraintsFilter} + %constraintBase.remove + $base \assng base \setminus cs$\; \label{algCleanupConstraintsRemoveFromBase} + %failedElements.remove + $m \assng m \setminus cs$\; \label{algCleanupConstraintsRemoveFromProblemConstraints} + %simpleAssignmentsFinder + $\relevantConstraintVariables \assng \relevantConstraintVariables \setminus cs$\;\label{algCleanupConstraintsRemoveFromConstraintVarsStart} + $\relevantConstraintVariables \assng \relevantConstraintVariables \setminus \setWithFlat{variables(v)}{c \in cs}$\;\label{algCleanupConstraintsRemoveFromConstraintVarsEnd} + %variablesMap + $\relevantConstraintsPerDeclaration \assng \relevantConstraintsPerDeclaration \setminus \setWith{\mapEntry{w}{c}}{w\in variables(c)}$\; \label{algCleanupConstraintsRemoveFromConstraintsPerDecl} + $cs \assng \emptySet$\label{algCleanupConstraintsClearResult} + }\label{algCleanupConstraintsClearEnd} + \Return $cs$\; + + \caption{Cleaning the constraint base (\IVML{cleanupConstraints}).}\label{algCleanupConstraints} +\end{algorithm} %\begin{algorithm}[H] @@ -164,14 +195,18 @@ \subsection{Value Type Changes}\label{sectReSchedType} -If 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: +If the value of compound variable $v$ changes, also its actual type may change along the refinement hierarchy. If the differing types also specify different constraints, the reasoner must adjust the constraint set accordingly. Moreover, a type change also happens when the value changes from or to the IVML value \IVMLnull{}. Then, a configed value is explicitly replaced by nothing (no configuration) or \IVMLnull{} is replaced by a value of a certain type. + +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. To avoid such transformations, we use an approach based on the difference among the involved types, i.e., in particular if the type changes along the refinement hierarchy, the approach identifies the types 'between' the old and the new type in the type hierarchy and either creates constraints or removes constraints according to the difference. For a changed variable $v$, the old value $val_o$ and the new value $val_n$, we must distinguish the following 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. + \item $val_n = \IVMLnull{}$: 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. + \item $val_o = \IVMLnull{}$: The value of $v$ was not configured before the value change and $v$ is configured after the value change, i.e., we can add all constraints for $v$ by calling Algorithm \ref{algTranslateDeclaration}. + \item $\subTypeOf{type(val_o)}{type(val_n)}$, i.e., $val_o$ is of a more general type than $val_n$: We just have to add the constraints for the currently missing types between $type(val_o)$ and $type(val_n)$ in the refinement hierarchy. As the constraint translation only allows for type exclusion, we reverse the selection, i.e, we exclude $allRefines^+(type(val_o))$. + \item $\subTypeOf{type(val_n)}{type(val_o)}$, i.e., $val_n$ is of a more general type than $val_o$: 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 between $type(val_n)$ and $type(val_o)$ in the type hierarchy. The required type information was attached to the constraints by Algorithm \ref{algTranslateCompoundContent} during a previous constraint translation. \end{enumerate} + +Algorithm \ref{algTranslateValueTypeChange}\footref{fnVisibilityResolver} receives the changed variable $v$, the new value $val_n$ and the old value $val_o$ of $v$. It is worth recalling that Algorithm \ref{algTranslateValueTypeChange} is only called (by Algorithm \ref{algVarChange} in line \ref{algVarChangeRescheduleValueTypeChange}) if the types of $val_o$ and $val_n$ really differ. The remainder of Algorithm \ref{algTranslateValueTypeChange} directly corresponds to the four cases above. + +If an existing value $val_o$ is being removed by setting it to \IVMLnull, lines \ref{algTranslateValueTypeChangeNewNullStart}-\ref{algTranslateValueTypeChangeNewNullEnd} remove the related constraints using Algorithm \ref{algCleanupConstraints}. If a deconfigured \IVMLnull{} value is replaced by a new value, lines \ref{algTranslateValueTypeChangeOldNullStart}-\ref{algTranslateValueTypeChangeNewNullStart} perform a full constraint translation adding all constraints for $val_n$. If $val_o$ is of a more general type than $val_n$, lines \ref{algTranslateValueTypeChangeOldHigherStart}-\ref{algTranslateValueTypeChangeOldHigherEnd} set the type excludes for all refined compounds of $val_o$ and, as the target value is already initialized, execute a constraint translation in incremental mode. As the excluded types are transferred into a temporary context frame created during the translation in Algorithm \ref{algTranslateCompoundDeclaration}, we do not have to reset the excluded types. Finally, $val_n$ is of a more general type than $val_o$, we cleanup the constraint base using Algorithm \ref{algCleanupConstraints} filtering out the types between the old and the new value type. \begin{algorithm}[H] @@ -181,9 +216,9 @@ $t_n \assng type(val_n)$; $t_o \assng type(val_o)$\; \uIf{$val_n = \IVMLnull{}$}{ \label{algTranslateValueTypeChangeNewNullStart} - $obtainConstraints(v, true, \undef)$\; \label{algTranslateValueTypeChangeNewNullEnd} + $cleanupConstraints(v, true, \undef)$\; \label{algTranslateValueTypeChangeNewNullEnd} }\uElseIf{$val_o = \IVMLnull{}$} { \label{algTranslateValueTypeChangeOldNullStart} - $inc_o \assng inc$; $inc \assng true$\; + %$inc_o \assng inc$; $inc \assng true$\; $translateDeclaration(decl(v), v, \undef)$\; - $inc \assng inc_o$\;\label{algTranslateValueTypeChangeOldNullEnd} + %$inc \assng inc_o$\;\label{algTranslateValueTypeChangeOldNullEnd} }\uElseIf{$\subTypeEqOf{t_o}{t_n}$} {\label{algTranslateValueTypeChangeOldHigherStart} $setTypeExcludes(\variableMapping, allRefines^+(t_o))$\; @@ -192,5 +227,5 @@ $inc \assng inc_o$\;\label{algTranslateValueTypeChangeOldHigherEnd} }\Else{\label{algTranslateValueTypeChangeOldLowerStart} - $obtainConstraints(v, true, allRefines^+(t_o) \setminus allRefines^+(t_n))$\; + $cleanupConstraints(v, true, allRefines^+(t_o) \setminus allRefines^+(t_n))$\; }\label{algTranslateValueTypeChangeOldLowerEnd} @@ -198,36 +233,2 @@ \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{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}). - -\begin{algorithm}[H] - \SetAlgoLined - \KwIn{variable $v$, flag $clear$, filter type set $f$} - \KwData{relevant constraints $\relevantConstraintVariables, \relevantConstraintsPerDeclaration$, problem records $m$} - \KwOut{persisting constraints of $v$ (if $\neg clear$)} - $i \assng v$; $cs \assng \undef$\; \label{algObtainConstraintsFindStart} - \Repeat{$cs = \undef \wedge~i \neq \undef$}{ - $cs \assng \relevantConstraintVariables[i]$\; - $i \assng parent(i)$\; - }\label{algObtainConstraintsFindEnd} - \If{$clear \wedge~cs \neq \undef$}{ \label{algObtainConstraintsClearStart} - %filter for attached - \lIf{$f \neq \undef$} {$cs \assng \setWith{c}{c \in cs \wedge attached(c) \in f}$}\label{algObtainConstraintsFilter} - %constraintBase.remove - $base \assng base \setminus cs$\; \label{algObtainConstraintsRemoveFromBase} - %failedElements.remove - $m \assng m \setminus cs$\; \label{algObtainConstraintsRemoveFromProblemConstraints} - %simpleAssignmentsFinder - $\relevantConstraintVariables \assng \relevantConstraintVariables \setminus cs$\;\label{algObtainConstraintsRemoveFromConstraintVarsStart} - $\relevantConstraintVariables \assng \relevantConstraintVariables \setminus \setWithFlat{variables(v)}{c \in cs}$\;\label{algObtainConstraintsRemoveFromConstraintVarsEnd} - %variablesMap - $\relevantConstraintsPerDeclaration \assng \relevantConstraintsPerDeclaration \setminus \setWith{\mapEntry{w}{c}}{w\in variables(c)}$\; \label{algObtainConstraintsRemoveFromConstraintsPerDecl} - $cs \assng \emptySet$\label{algObtainConstraintsClearResult} - }\label{algObtainConstraintsClearEnd} - \Return $cs$\; - - \caption{Obtaining and clearing constraints (\IVML{obtainConstraints}).}\label{algObtainConstraints} -\end{algorithm} - - Index: /reasoner/mainAlgorithms.tex =================================================================== --- /reasoner/mainAlgorithms.tex (revision 223) +++ /reasoner/mainAlgorithms.tex (revision 224) @@ -3,5 +3,5 @@ \center %\frame{ -\includegraphics[scale=0.52,trim={5.9cm 6.5cm 27.5cm 0.4cm},clip]{figures/structure.pdf} +\includegraphics[scale=0.55,trim={5.9cm 6cm 27.5cm 0.4cm},clip]{figures/structure.pdf} %} \caption{Overview of reasoning algorithms and sections.}