Index: /reasoner/reasoner.tex
===================================================================
--- /reasoner/reasoner.tex	(revision 119)
+++ /reasoner/reasoner.tex	(revision 120)
@@ -1086,15 +1086,14 @@
 }
 
-When assigning a value to a variable, the right side may be a complex expression determining the actual value of a collection or a compound. In both cases, the contained values may be constraint values (not handled in \ref{sectConstraintVariables}), but also deeply nested values may be constraint values, e.g., a constraint value in a compound in collection used in a compound.
-
+When unconditionally assigning a value to a variable, the right side may be a complex expression determining the actual value of a collection or a compound.  In both cases, the contained values may be constraint values (not handled in \ref{sectConstraintVariables}), but also deeply nested values may be constraint values, e.g., a constraint value in a compound in collection used in a compound. These constraints contribute to the initial constraint base and may cause certain value changes that cannot just be achieved as a consequance of changing values in constraint re-scheduling (cf. Section \ref{sectTopLevelConstraintsRescheduling}). As the $add$ function is also called as part of re-scheduling, dynamic constraints discovered there and their initializers and values are treated similarly.
 
 \begin{algorithm}[H]
   \KwIn{constraint sequence $s$, constraint $c$, perform initializers $check$}
   \KwData{top level and other constraints $\topLevelConstraints, \otherConstraints$, variable mapping $\variableMapping$, relevant constraints $\relevantConstraintsPerType$ , incremental flag $inc$, evals flag $inEvals$}
-  \If{$\neg inc \vee (inc \wedge \neg (isAssignment(c) \vee isFrozen(c)))$} {
-    $c = composeExpression(\variableMapping, c)$\;
+  $c = composeExpression(\variableMapping, c)$\;
     \If{$check$}{
           $\otherConstraints \assng \otherConstraints \addSeq check(rightSide(c), \variableMapping)$\;
     }
+    \If{$\closedCases{\neg isAssignment(c) \vee \neg isFrozen(c) & \text{if } inc\\ true & \text{else}}$}{
     \If{$inEvals \wedge (s=\otherConstraints \vee s = \topLevelConstraints)$} {
        $\topLevelConstraints = c \addSeq \topLevelConstraints$\;
@@ -1105,5 +1104,5 @@
       $\relevantConstraintsPerType \assng \relevantConstraintsPerType \cup \setWith{\mapEntry{v}{c}}{v\in variables(c)}$\; % assignConstraintsToVariables
      }
-   }
+    }
  \caption{Adds a constraint to the constraint base ($add$).}\label{algAddConstraint}
 \end{algorithm}
@@ -1154,5 +1153,10 @@
 \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 all known constraints (\MISSING{dynamic value type changes}) for a variable are identified and become subject to re-scheduling. The identification includes both, parent  (line \ref{algVarChangeRescheduleParents}) and nested (line \ref{algVarChangeRescheduleNested}) variables, which is in particular relevant to capture all relevant constraints for variables in compound and container values. These constraints are appended to the constraint $base$, not adding an individual constraint if it is already scheduled in the constraint $base$.
+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 $\relevantConstraintsPerType$, while now now irrelevant constraints are identified via $\relevantConstraintVariables$ and also removed from $\relevantConstraintVariables$ and $\relevantConstraintsPerType$. 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 $\relevantConstraintsPerType$, 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.}.
 
 \begin{algorithm}[H]
@@ -1165,10 +1169,7 @@
       $val_n \assng value(v)$\;
       \If{$val_n \neq val_o$} {
-	$rescheduleValueChange(v, v, true)$\;
-          \If{$isContainer(v)$} {
-    	    $createContainerValueConstraints(val_n, createParentEx(v), \undef, parent(decl(v)), v)$ \MISSING{!}\;
-           }
+	$rescheduleValueChange(v, v, true)$\; \label{algVarChangeRescheduleConstraintVariables}
           \If{$isValueTypeChange(v, val_n, val_o)$ \MISSING{!}} {
-             $rescheduleValueTypeChange(v, val_n, val_o)$ \MISSING{!}\;
+             $rescheduleValueTypeChange(v, val_n, val_o)$ \MISSING{!}\; \label{algVarChangeRescheduleValueTypeChange}
           }
       }
@@ -1176,4 +1177,6 @@
       $base \assng base \addSeqNoDupl \seqWith{\relevantConstraintsPerType[n]}{n\in allNested(v)}$\; \label{algVarChangeRescheduleNested}%constraintsForParent
 %      $base \assng base \addSeqNoDupl \bigcup_{c\in alNested(v)}\relevantConstraints[c]$\; \label{algVarChangeRescheduleNested}%constraintsForChilds, nested geht für alle variablen
+  }\ElseIf{$getMapping(\variableMapping, decl(v)) \neq \undef$}{
+     $registerMapping(\variableMapping, decl(v), v)$\;
   }
  \caption{Adjusting the constraint base (\IVML{notifyChanged}).}\label{algVarChange}