Index: /reasoner/consTranslation.tex
===================================================================
--- /reasoner/consTranslation.tex	(revision 148)
+++ /reasoner/consTranslation.tex	(revision 149)
@@ -190,7 +190,4 @@
 In the first case (lines \ref{algTranslateCompoundDeclarationTranslateSlotsStart}-\ref{algTranslateCompoundDeclarationTranslateSlotsMid}), we can rely on the compound variable $v$ and its nested variables representing all slots even refined ones\footnote{This also holds for $slots^-(v)$ if the parent type of $v$ is not excluded.} (cf. Section \ref{sectNotationCompounds}). Thus, in line \ref{algTranslateCompoundDeclarationTranslateSlotsV}, we call Algorithm \ref{algTranslateDeclaration} for slot $s$ and its annotations with the variable corresponding to $s$ and the access expression for $s$ recorded in $\variableMapping$. In the second case (lines \ref{algTranslateCompoundDeclarationTranslateSlotsMid}-\ref{algTranslateCompoundDeclarationTranslateSlotsEnd}), we use the type structure as fallback, i.e., we translate constraints without knowledge about the actual type of the variables. In line \ref{algTranslateCompoundDeclarationTranslateSlotsT}, we call Algorithm \ref{algTranslateDeclaration} for a type-based transformation of the slot declaration $d$ and its annotations, i.e., without slot variable but with accessor expression for $s$ recorded in $\variableMapping$.
 
-Then, if we are not reasoning in incremental mode, we translate the default values specified by annotation assignments nested in $t$ in line \ref{algTranslateCompoundDeclarationCompoundAssignments}. In line \ref{algTranslateCompoundDeclarationSelf}, we determine the actual expression $e_f$ for \IVML{self}, i.e., either the access expression $ca$ if given or the declaration $d$. Then, due to their specific priorities, we first translate all eval constraints defined along the type hierarchy for $t$ in lines \ref{algTranslateCompoundDeclarationEvalStart}-\ref{algTranslateCompoundDeclarationEvalEnd}. Afterwards, we include all remaining compound constraints, i.e., type constraints and annotation constraints in lines \ref{algTranslateCompoundDeclarationAllStart}-\ref{algTranslateCompoundDeclarationAllEnd}.
-
-
 \begin{algorithm}[H]
   \SetAlgoLined
@@ -213,14 +210,16 @@
   }
   \leIf{$ca \neq \undef$}{$e_f\assng ca$}{$e_f\assng d$}\label{algTranslateCompoundDeclarationSelf}
-\MISSING{Register constraints for creating compound constraints (value is constraint value) }\;
-  $eval \assng \setWithFlat{allEvalConstraints(r)}{r\in allRefines^+(t) \text{ } \setminus \text{ } excludedTypes(t)}$\;\label{algTranslateCompoundDeclarationEvalStart}
-  $add(\otherConstraints, \setWith{attach(\createConstraint{\varSubstitutionSelfVarMapping{c}{e_f}}, currentType(\variableMapping))}{c\in eval}, true, v)$\;\label{algTranslateCompoundDeclarationEvalEnd}
-  $cmp \assng \setWithFlat{allCompoundConstraints(r)}{r\in allRefines^+(t) \text{ } \setminus \text{ } excludedTypes(t)}$\;\label{algTranslateCompoundDeclarationAllStart}
-  $add(\otherConstraints, \setWith{attach(\createConstraint{\varSubstitutionSelfVarMapping{c}{e_f}}, currentType(\variableMapping))}{c\in cmp}, true, v)$\;\label{algTranslateCompoundDeclarationAllEnd}
-
+  $t_r \assng allRefines^+(t) \text{ } \setminus \text{ } excludedTypes(t)$\;
+  $t_c \assng currentType(\variableMapping)$\;
+  $eval \assng \setWithFlat{allEvalConstraints(r)}{r\in t_r}$\;\label{algTranslateCompoundDeclarationEvalStart}
+  $add(\otherConstraints, \setWith{attach(\createConstraint{\varSubstitutionSelfVarMapping{c}{e_f}}, t_c)}{c\in eval}, true, v)$\;\label{algTranslateCompoundDeclarationEvalEnd}
+  $cmp \assng \setWithFlat{allCmpConstraints(r)}{r\in t_r}$\;\label{algTranslateCompoundDeclarationAllStart}
+  $add(\otherConstraints, \setWith{register(v, attach(\createConstraint{\varSubstitutionSelfVarMapping{c}{e_f}}), t_c)}{c\in cmp}, true, v)$\;\label{algTranslateCompoundDeclarationAllEnd}
  \caption{Translating compound content (\IVML{translateCompoundContent}).}\label{algTranslateCompoundContent}
 \end{algorithm}
 
-As stated above, we defer all constraint translation work to a recursive execution of Algorithm \ref{algTranslateDeclaration}. However, correctly initializing compounds can be tricky, as both, default slot values and compound initializer expressions, i.e., complex value assignments to compounds must be considered while reasoning. We solve this as follows: Algorithm \ref{algTranslateDeclaration} is triggered by a compound variable declaration. If a default value for the compound variable is defined, Algorithm \ref{algTranslateDeclaration} creates a respective constraint and then continues with the creation of the slot defaults and the compound constraints in Algorithm \ref{algTranslateCompoundContent}. Mixing both happens behind the scenes through the constraint evaluator: Assigning a value to a compound variable (or a slot) causes the creation of a compound instance with the desired values for the specified slots. The following assignment constraints for the default values are executed if no other value has been assigned (otherwise they are ignored) and finally removed by the main constraint evaluation loop in Algorithm \ref{algEvalLoop}. Dependent default values are evaluated as soon as the required variables have values assigned.
+Then, if we are not reasoning in incremental mode, we translate the default values specified by annotation assignments nested in $t$ in line \ref{algTranslateCompoundDeclarationCompoundAssignments}. In line \ref{algTranslateCompoundDeclarationSelf}, we determine the actual expression $e_f$ for \IVML{self}, i.e., either the access expression $ca$ if given or the declaration $d$. Then, due to their specific priorities, we first translate all eval constraints defined along the type hierarchy for $t$ in lines \ref{algTranslateCompoundDeclarationEvalStart}-\ref{algTranslateCompoundDeclarationEvalEnd}. Finally, we include all remaining compound constraints, i.e., type constraints and constraints in annotation assignments in lines \ref{algTranslateCompoundDeclarationAllStart}-\ref{algTranslateCompoundDeclarationAllEnd} and register them with the constraint variable for constraint-rescheduling (the $register$ operation returns the constraint passed in, cf. Algorithm \ref{algRegisterConstraint}). 
+
+As stated above, we defer most constraint translation work to a recursive execution of Algorithm \ref{algTranslateDeclaration}. However, correctly initializing compounds can be tricky, as default slot values, slot value assignment constraints, default (partial) compound initializer expressions as well as (partial) compound initializer assignment constraints can be mixed. While re-assignments of the same slot in the same scope is forbidden, partial compound initializers and slot assignments can be mixed as long as no re-assignments occur. This happens behind the scenes in the constraint evaluator: Assigning a value to a compound variable (or a slot) causes the creation of a compound value instance with the desired values for the specified slots. Subsequent assignment constraints are executed if no other value has been assigned and, finally, removed by the main constraint evaluation loop in Algorithm \ref{algEvalLoop}. Dependent default values are deferred until all used variables and slots are defined.
 
 \subsection{Container types}\label{sectContainerDefaults}
@@ -475,5 +474,5 @@
         $c \assng \createConstraintConstraint{\varSubstitutionSelfVarMapping{c}{f}}$\;
         $add(\otherConstraints, \set{c}, \neg isConst(c), v)$\;
-        $registerConstraint(v, c)$\;
+        $register(v, c)$\;
       }
  \caption{Creating constraints for constraint variables (\IVML{createConstraintVariableConstraint}).}\label{algCreateConstraintVariableConstraint}
@@ -512,5 +511,5 @@
   $c = composeExpression(\variableMapping, c)$\;
     \If{$check$}{
-          \ForAll{d\iterAssng check(rightSide(c), \variableMapping)} {
+          \ForAll{$d\iterAssng check(rightSide(c), \variableMapping)$} {
               $createConstraintVariableConstraint(d, \undef, \undef)$\;
           }
@@ -559,4 +558,5 @@
   \KwIn{variable $v$, constraint expression $c$}
   \KwData{other constraints $\otherConstraints$, relevant constraints $\relevantConstraintVariables$}, relevant constraints copy $base_{\relevantConstraintVariables}$
+  \KwOut{$c$}
  
   \If{$v \neq \undef$}{
@@ -568,7 +568,8 @@
        }
    } 
-
- \caption{Registering constraints originating fom constraint variables (\IVML{registerConstraint}).}\label{algRegisterConstraint}
-\end{algorithm}
-%
-Recording happens only if $v$ is defined, which may not be the case if this algorithm is called while processing container values. Then, we recorder the relation of the variable $v$ to its 
+  \Return $c$\;
+
+ \caption{Registering constraints originating fom constraint variables (\textit{register}).}\label{algRegisterConstraint}
+\end{algorithm}
+%
+A constraint is registered\footnote{\IVML{registerConstraint} in the implementation} only if $v$ is defined, which may not be the case if this algorithm is called while processing container values. Then, we recorder the relation of the variable $v$ to its 
Index: /reasoner/notation.tex
===================================================================
--- /reasoner/notation.tex	(revision 148)
+++ /reasoner/notation.tex	(revision 149)
@@ -174,5 +174,5 @@
 %
 \begin{align*}
-all&CompoundConstraints(t) = \\
+all&CmpConstraints(t) = 
    &\setWith{constraints(s) \cup allAssignmentConstraints(s)}{s \in allRefines^+(t)}
 \end{align*}