Index: /reasoner/reasoner.tex
===================================================================
--- /reasoner/reasoner.tex	(revision 118)
+++ /reasoner/reasoner.tex	(revision 119)
@@ -233,5 +233,5 @@
 As part of the constraint instantiation, variables must be replaced. Let $c=\createConstraint{\IVML{assign(x, 25)}}$ be a constraint and \IVML{y} be some IVML variable. Then $\varSubstitution{c}{x = y}$ leads to the substitution of all variables named \IVML{x} by \IVML{x}, i.e., for the example effectively to \IVML{y = 25}. If such substitutions are stored in a mapping, i.e., a $\variableMapping=\set{\mapEntry{e_s, e_t}}$ with $e_s$ being the expression to be replaced and $e_t$ the replacing expression, we can apply this mapping to a constraint $c$ using $\varSubstitutionVarMapping{c}$. Moreover, we can combine a specific mapping and already stored mappings using $\varSubstitutionOtherVarMapping{c}{x = y}$. Please note that such substitutions are transitive, i.e., if $\mapEntry{y}{z}\in \variableMapping$, $x$ will be replaced by $z$. If the right side of a substitution is $\undef$, no substitution happens, e.g., in $\varSubstitution{c}{x = \undef}$. As usual in IVML, we denote the creation of collection operations using the arrow and iterator notation. As we use the '$|$' symbol for variable substitutions, using the same symbol in some transformations in IVML quantor expressions would be confusing. Thus, we use in this document the respective syntax parts ':' as introduced for sets in Section \ref{sectGeneralNotation} instead of the syntactically correct '$|$', e.g., \IVML{forall(x:c(x))} instead of the correct IVML notation \IVML{forall(x|c(x))}. Let $c$ be an IVML collection of Integers, then \IVML{c->forall(i:i>20);} requires that all values in $c$ are greater than 20. To create such a constraint with $c$ being an algorithm variable, we denote $\createConstraint{c\IVML{->forall(i:i>20)}}$. 
 
-For some purpose, the reasoning mechanism must classify constraints, in particular default value assignments over usual constraints. We indicate this information as a `$d$' in the constraint creation notation, e.g., for creating a default constraint, we denote $b \assng \createDefaultConstraint{\IVML{assign}(x, 25)}$ for which $\isDefaultConstraint{b} = true$ holds. Further, we allow attaching information to a constraint, e.g., the type it was created for. Let $c = attach(c, t)$ be an operation that attaches $t$ to constraint $c$ (and returns $c$) as well as $t = attached(c)$ return the respective attachment.
+For some purpose, the reasoning mechanism must classify constraints, in particular default value assignments over usual constraints. We indicate this information as a `$d$' in the constraint creation notation, e.g., for creating a default constraint, we denote $b \assng \createDefaultConstraint{\IVML{assign}(x, 25)}$ for which $\isDefaultConstraint{b} = true$ holds. In case of an assignment constraint $x = y$, i.e., $c=\createDefaultConstraint{\IVML{assign(}x, y\IVML{)}}$, $rightSide(c) = x$ else $\undef$. Further, we allow attaching additional information to a constraint, e.g., the type it was created for. Let $c = attach(c, t)$ be an operation that attaches $t$ to constraint $c$ (and returns $c$) as well as $t = attached(c)$ return the respective attachment.
 %Similarly, we denote creating a constraint originating from a constraint variable by `$c$', e.g., $b \assng \createConstraintConstraint{\IVML{assign}(x, 25)}$ for which $\isConstraintConstraint{b} = true$ holds.
 
@@ -1042,6 +1042,6 @@
 \begin{gather*}
    \patternDerivation{\IVML{Constraint } v = ex\IVML{;}}{\varSubstitution{ex}{\variableMapping}}\\
-   \patternDerivation{\IVML{containerOf(Constraint)} = \IVML{\{}ex_1 , \ldots, ex_n\IVML{\}}}{\varSubstitution{ex_1}{\variableMapping}, \ldots, \varSubstitution{ex_n}{\variableMapping}}\\
-   \patternDerivation{\IVML{Compound } C \IVML{ \{Constraint } v = ex \IVML{\}}\IVML{; } C v}{\varSubstitution{ex}{\IVML{self}=v, \variableMapping}}
+   \patternDerivation{\IVML{containerOf(Constraint)} v = \IVML{\{}ex_1 , \ldots, ex_n\IVML{\}}\IVML{;}}{\varSubstitution{ex_1}{\variableMapping}, \ldots, \varSubstitution{ex_n}{\variableMapping}}\\
+   \patternDerivation{\IVML{Compound } C = \IVML{ \{Constraint } s = ex \IVML{\}}\IVML{; } C v\IVML{;}}{\varSubstitution{ex}{\IVML{self}=v, \variableMapping}}
 \end{gather*}
 }
@@ -1072,8 +1072,20 @@
   \item It filters out irrelevant constraints, in particular simple (default value) assignment constraints during incremental reasoning, are assumed to be already processed during previous iterations. Also constraints with all variables frozen or local (used for iterator variables in quantors) are filtered out ($isFrozen(c)$) if enabled, e.g., to speed up runtime reasoning.
   \item It serves as the central place to finally compose constraints for nested compound containers using Algorithm \ref{algComposeExpression} and the variable mapping $\variableMapping$.
-  \item It analyzes the given constraint $c$ for the use of compound or container initializers. As explained above, these structures only occur in value assignments and actually must be analyzed for constraint variables, which must be turned into individual constraints. We perform this through the two recursive helper operations $checkContainerInitializer$ and $checkCompoundInitializer$ shown below.
+  \item It analyzes the given constraint $c$ for the use of compound or container initializers. As explained above, these structures only occur in value assignments and actually must be analyzed for constraint variables, which must be turned into individual constraints. We perform this through the two recursive helper operations for expressions $checkContainerInitializer$ and $checkCompoundInitializer$ and two similar helper functions for values $checkContainerValue$ and $checkCompoundValue$ shown below\footnote{The implementation utilizes a visitor for this purpose.}. 
   \item Appends the constraint to the given sequence, except for constraints from eval-blocks, which are prepended to the sequence of top-level constraints $\topLevelConstraints$ if the target sequence is other $\otherConstraints$ or top-level constraints $\topLevelConstraints$ in order to enforce the priority of eval-constraints.
   \item Registers the constraint with its used variables to enable re-scheduling of constraints during reasoning in Algorithm \ref{algVarChange}.
 \end{itemize}
+
+Thus, the functiondoes not only add a given constraint, it completes it and scans it for further contained constraints. Let $ex$ be a constraint expression. Then we have to consider two specific assignment operations not transformed so far.  
+
+\grayPara{
+\begin{gather*}
+   \patternDerivation{v = \IVML{\{}\ldots, ex,\ldots\IVML{\}}}{\ldots, \varSubstitution{ex}{\variableMapping}, \ldots}\\
+   \patternDerivation{v = \IVML{\{} s = ex \IVML{\}}}{\varSubstitution{ex}{\IVML{self}=v, \variableMapping}}
+\end{gather*}
+}
+
+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.
+
 
 \begin{algorithm}[H]
@@ -1083,9 +1095,5 @@
     $c = composeExpression(\variableMapping, c)$\;
     \If{$check$}{
-      \If{$isContainerInitializer(c)$} {
-          $\otherConstraints \assng \otherConstraints \addSeq checkCompoundInitializer(c, \variableMapping)$\;
-      }\ElseIf{$isCompoundInitializer(c)$}{
-          $\otherConstraints \assng \otherConstraints \addSeq checkCompoundInitializer(c, \variableMapping)$\;
-      }
+          $\otherConstraints \assng \otherConstraints \addSeq check(rightSide(c), \variableMapping)$\;
     }
     \If{$inEvals \wedge (s=\otherConstraints \vee s = \topLevelConstraints)$} {
@@ -1101,17 +1109,18 @@
 \end{algorithm}
 
-For constraint variables and constraint variable containers:
-%\begin{align*}
-%retrieve&ContainerConstraints(c, m) =\\ 
-%             &\closedCases{checkContainerInitializer(c, \undef), & \text{if } isContainerInitializer(c) \\ checkCompoundInitializer(c, m) &\text{if } isCompoundInitializer(c)\\ \setEmpty, & \text{else}}
-%\end{align*}
+To identify constraint variable values in containers and compounds, we define the following helper function:
 \begin{align*}
-check&ContainerInitializer(c, \variableMapping) =\\ &\seqWith{\closedCases{checkContainerInitializer(e), & \text{if } isContainerInitializer(e) \\ \createConstraintConstraint{\varSubstitutionVarMapping{e}}, &\text{else}}}{e\in expr(c)}
+check&(c, \variableMapping) =\\ 
+         &\seqWith{\closedCases{check(e, \variableMapping), & \text{if } isContainerInitializer(e) \\ 
+                                                  check(e, \variableMapping), & \text{if } isContainer(type(e)) \\
+                                                  check(e, \variableMapping) & \text{if } isCompoundInitializer(e) \\ 
+                                                  check(e, \variableMapping) & \text{if } isCompound(type(e)) \\ 
+                                                 \createConstraintConstraint{\varSubstitutionVarMapping{e}}, &\text{if } isConstraint(e) \\
+                                                 \createConstraintConstraint{\varSubstitutionVarMapping{value(e)}}, &\text{if } isConstraintValue(e) \\
+                                                 \createConstraintConstraint{e}, &\text{if } Boolean(e) \\
+                                                 \emptySet, &\text{else}
+         }}{e\in expr(c) \cup elements(c)}
 \end{align*}
-\begin{align*}
-check&CompoundInitializer(c, \variableMapping) =\\ 
-         &\seqWith{\closedCases{checkContainerInitializer(e, \variableMapping), & \text{if } isContainerInitializer(e) \\
-           checkCompoundInitializer(e, \variableMapping) &\text{if } isCompoundInitializer(e)\\ \setEmpty, & \text{else}}}{e\in expr(c)}
-\end{align*}
+The function $check$ 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\footnote{Technically, we must make the distinction between initializer and constraint, as the IVML object model supports both types of elements here and the IVML parser creates a value if all contained elements are constant or otherwise an initializer expression}. 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{algorithm}[H]
@@ -1494,4 +1503,5 @@
     \item \textbf{Avoid multipe variable substitutions} per constraint expressions, i.e., join variable substitutions wherever possible. Variable substitution copies the expression. Initially, performing a substitution multiple time on the same expression caused creating multiple copies of all nodes in memry, i.e., a follow-up copy usually was used instead of the original copy making the previous copies effectively superfluous. As sometimes multiple substitutions can only be avoided with additional (not straightforward) code, e.g., for a sequential call of Algorithm \ref{algTranslateCompoundDeclaration} and \ref{algTranslateDeclaration}, we revised the IVML expression copy mechanism to create instances of expression tree nodes only if a substitution happend, i.e., new expression trees are absolutely required.
     \item \textbf{Use instance pooling} if datastructures are temporarily used, e.g., variable accessors in expression evaluation or sets of compounds in reasoning (20-30 ms on larger models, at that time around 10\% of runtime).
+\item visitor is faster than (IVML-)instanceof
 \end{itemize}