Index: /reasoner/reasoner.tex
===================================================================
--- /reasoner/reasoner.tex	(revision 29)
+++ /reasoner/reasoner.tex	(revision 30)
@@ -116,5 +116,5 @@
   \item Constraints related to compound types used in collections $\collectionCompoundConstraints$.
   \item Top-level constraints $\topLevelConstraints$
-  \item TBD{check: $\assignedAttributeConstraints, \unresolvedConstraints$}
+  \item TBD{check: $\assignedAttributeConstraints$}
 \end{itemize}
 Further, the algorithm maintains a global variable mapping $\variableMapping$, a map of already processed variables to accessors so that later processed complex expressions can be substituted with the correct accessors.
@@ -140,5 +140,5 @@
           $translateDeclarationDefaults(d, decision(cfg, d), \undef, inc)$\;
       }
-      $\topLevelConstraints \assng\seqWith{constraints(e)}{e\in evals(p)} \addSeq constraints(p)$\;
+      $addConstraints(\topLevelConstraints,\seqWith{constraints(e)}{e\in evals(p)} \addSeq constraints(p), true)$\;
       \ForAll{a \iterAssng assignments(p)}{
           $translateAnnotationAssignments(a, \undef, \undef)$\;
@@ -253,5 +253,5 @@
               \lIf{$ ca == \undef $}{$\constraintVariablesConstraints \assng \constraintVariablesConstraints \cup (\createConstraint{dflt}, v)$}
           }\Else{
-              $dfltS \assng dfltS \cup \createDefaultConstraint{\IVML{assign}(\closedCases{ca, & \text{if } dfltS == \defaultConstraints \\ d, &\text{else}}, deflt)}$\;
+              $addConstraint(dfltS, \createDefaultConstraint{\IVML{assign}(\closedCases{ca, & \text{if } dfltS == \defaultConstraints \\ d, &\text{else}}, deflt)})$\;
           }
       }
@@ -270,5 +270,5 @@
 
   $cs \assng \bigcup_{t \in allBase(type(d))} constraints(t)$\;
-  $\derivedTypeConstraints \assng \derivedTypeConstraints \cup \setWith{\createInternalConstraint{c|_{decl(c)=d}}}{c\in cs}$\;
+  $addConstraints(\derivedTypeConstraints, \setWith{\createInternalConstraint{c|_{decl(c)=d}}}{c\in cs}, true)$\;
  \caption{Translating constraints for derived types (\IVML{translateDerivedDatatypeConstraints}).}\label{algTranslateDerivedDatatypeConstraints}
 \end{algorithm}
@@ -282,5 +282,5 @@
 
   $cs \assng \bigcup_{t \in allBase(t} constraints(t)$\;
-  $\derivedTypeConstraints \assng \derivedTypeConstraints \cup \setWith{\createConstraint{\closedCases{d, & \text{if } ca = \undef \\ ca, &\text{else}}\rightarrow\IVML{forAll}(i|\text{ }c|_{decl(c)=d})}}{c \in cs}$\;
+  $addConstraints(\derivedTypeConstraints, \setWith{\createConstraint{\closedCases{d, & \text{if } ca = \undef \\ ca, &\text{else}}\rightarrow\IVML{forAll}(i|\text{ }c|_{decl(c)=d})}}{c \in cs}, true)$\;
  \caption{Translating constraints for derived collection types (\IVML{translateCollectionDerivedDatatypeConstraints}).}\label{algTranslateCollectionDerivedDatatypeConstraints}
 \end{algorithm}
@@ -297,5 +297,5 @@
 
   $a \assng annotations(decision(cfg, d))$\;
-  $\defaultAnnotationConstraints \assng \defaultAnnotationConstraints \cup \setWith{\createDefaultConstraint{\IVML{assign}(\closedCases{\IVMLMeta{acc}(d,r), & \text{if } ca = \undef \\ \IVMLMeta{acc}(ca,r), &\text{else}}, default(r))}}{r\in a}$\; 
+  $addConstraints(\defaultAnnotationConstraints, \setWith{\createDefaultConstraint{\IVML{assign}(\closedCases{\IVMLMeta{acc}(d,r), & \text{if } ca = \undef \\ \IVMLMeta{acc}(ca,r), &\text{else}}, default(r))}}{r\in a}, false)$\; 
  \caption{Translating annotation defaults (\IVML{translateAnnotationDefaults}).}\label{algTranslateAnnotationDefaults}
 \end{algorithm}
@@ -360,10 +360,10 @@
   \ForAll{s \iterAssng slots(v)} { %actual slots
       \If{$isConstraintContainer(type(s))$} {
-          $\constraintVariablesConstraints \assng \constraintVariablesConstraints \cup \setWith{\createConstraint{value(e)|_{\IVMLself =d, \variableMapping}}}{e \in elements(value(s))}$\;
+          $addConstraints(\constraintVariablesConstraints, \setWith{\createConstraint{value(e)|_{\IVMLself =d, \variableMapping}}}{e \in elements(value(s))}, true)$\;
       }
       \If{$isConstraint(type(s)) \wedge default(s) \neq \undef$}{
-          $\constraintVariablesConstraints \assng \constraintVariablesConstraints \cup \set{\createConstraint{default(s)|_{\IVMLself =d, \variableMapping}}}$\;
-      }
-     $\compoundConstraints \assng \compoundConstraints \cup translateCollectionCompoundConstraints(s, v, \variableMapping[s])$\;
+          $addConstraints(\constraintVariablesConstraints, \set{\createConstraint{default(s)|_{\IVMLself =d, \variableMapping}}}, true)$\;
+      }
+     $addConstraints(\compoundConstraints, translateCollectionCompoundConstraints(s, v, \variableMapping[s]), true)$\;
   }
   \If{$\neg inc$} {
@@ -372,6 +372,6 @@
       }
   }
-  $\compoundConstraints \assng \compoundConstraints \cup \setWith{\createConstraint{c|_{\IVMLself =d, \variableMapping}}}{c\in allCompoundConstraints(t, false)}$\;
-  $\compoundEvalConstraints \assng \compoundEvalConstraints \setWith{\createConstraint{c|_{vm}}}{c\in \bigcup_{r\in allRefines^+(t)} allEvalConstraints(r)}$\;
+  $addConstraints(\compoundConstraints, \setWith{\createConstraint{c|_{\IVMLself =d, \variableMapping}}}{c\in allCompoundConstraints(t, false)}, true)$\;
+  $addConstraints(\compoundEvalConstraints, \setWith{\createConstraint{c|_{vm}}}{c\in \bigcup_{r\in allRefines^+(t)} allEvalConstraints(r)}, true)$\;
 
  \caption{Translating annotation defaults (\IVML{translateCompoundDefaults}).}\label{algTranslateCompoundDefaults}
@@ -398,5 +398,5 @@
   \ForAll{$e \iterAssng ea$}{
       \ForAll{$d \iterAssng slots(a)$} {
-          $\assignmentConstraints \assng \assignmentConstraints \cup \set{translateAnnotationAssignment(e, d, ca)}$\;
+          $addConstraints(\assignmentConstraints, \set{translateAnnotationAssignment(e, d, ca)}, false)$\;
           \If{$isCompound(type(d))$} {
               \ForAll{$s \iterAssng slots(d)$} {
@@ -406,5 +406,5 @@
               \ForAll{$s \iterAssng slots(d)$} {
                   $b \assng translateAnnotationAssignment(e, s, c)$\;
-                  $\assignmentConstraints \assng \assignmentConstraints \cup \set{b}$\;
+                  $addConstraint(\assignmentConstraints, \set{b})$\;
               }
           }
@@ -432,5 +432,5 @@
   \KwData{deferred default constraints $\deferredDefaultConstraints$}
   \ForAll{$s \iterAssng \setWith{dfltSlots(u)}{u \in allRefines^+(t)}$}{
-      $\deferredDefaultConstraints \assng \deferredDefaultConstraints \cup \createDefaultConstraint{\IVML{typeSelect}(\IVML{flatten}(d), t)\rightarrow \IVML{forAll}(\IVMLMeta{var}(i,t)|\IVML{assign}(i.name(s), default(s)|_{\IVMLself =i, \variableMapping})}$\;
+      $addConstraint(\deferredDefaultConstraints, \createDefaultConstraint{\IVML{typeSelect}(\IVML{flatten}(d), t)\rightarrow \IVML{forAll}(\IVMLMeta{var}(i,t)|\IVML{assign}(i.name(s), default(s)|_{\IVMLself =i, \variableMapping})})$\;
    }
 
@@ -485,8 +485,22 @@
 First, the various constraint sets are composed starting with default constraints ($\defaultConstraints$) adding then the remaining constraints. After transferring the 
 
-\begin{align*}
-retrieve&CollectionConstraints(c, m) =\\ 
-             &\closedCases{checkContainerInitializer(c, \undef), & \text{if } isContainerInitializer(c) \\ checkCompoundInitializer(c, m) &\text{if } isCompoundInitializer(c)\\ \set{}, & \text{else}}
-\end{align*}
+\begin{algorithm}[H]
+  \KwIn{constraint sequence $s$, constraint $c$, perform initializers $check$}
+  \KwData{variable mapping $\variableMapping$}
+  \If{$check$}{
+      \If{$isContainerInitializer(c)$} {
+          $\collectionConstraints \assng \collectionConstraints \addSeq checkCompoundInitializer(c, m)$\;
+      }\ElseIf{$isCompoundInitializer(c)$}{
+          $\collectionConstraints \assng \collectionConstraints \addSeq checkCompoundInitializer(c, m)$\;
+      }
+  }
+  $s \assng s \addSeq c$\;
+ \caption{Records and analyzes a constraint (\IVML{addConstraint}).}\label{algAddConstraint}
+\end{algorithm}
+
+%\begin{align*}
+%retrieve&CollectionConstraints(c, m) =\\ 
+%             &\closedCases{checkContainerInitializer(c, \undef), & \text{if } isContainerInitializer(c) \\ checkCompoundInitializer(c, m) &\text{if } isCompoundInitializer(c)\\ \set{}, & \text{else}}
+%\end{align*}
 \begin{align*}
 checkContainerInitializer(c, m) = \seqWith{\closedCases{e|_m, & \text{if } m \ne \undef \\ e &\text{else}}}{e\in expr(c)}
@@ -497,4 +511,15 @@
 \end{align*}
 
+\TBD{Just here, as algorithm descriptions often utilize collection notation.}
+\begin{algorithm}[H]
+  \KwIn{constraint sequence $s$, constraint sequence $c$, perform initializers $check$}
+  \KwData{variable mapping $\variableMapping$}
+  \ForAll{d \iterAssng c} {
+      addConstraint(s, d, c);
+  }
+ \caption{Records and analyzes a constraint sequence.}\label{algAddConstraints}
+\end{algorithm}
+
+
 \begin{algorithm}[H]
   \SetAlgoLined
@@ -502,9 +527,5 @@
   \KwData{constraint $base$ , variable mapping $\variableMapping$ \TBD{join, reorder, beautify, leave out non-incremental on-the-fly}}
 
-  $c_s \assng c_s \addSeq \defaultConstraints \addSeq \deferredDefaultConstraints \addSeq \derivedTypeConstraints \addSeq\topLevelConstraints \addSeq \compoundEvalConstraints \addSeq \compoundConstraints \addSeq \constraintVariablesConstraints \addSeq \collectionCompoundConstraints$\;
-  \ForAll{$c \iterAssng c_s$} {
-      $retrieveCollectionConstraints(c, \variableMapping)$\;
-  }
-  $c_s \assng c_s \addSeq \collectionConstraints$\;
+  $c_s \assng c_s \addSeq \defaultConstraints \addSeq \deferredDefaultConstraints \addSeq \derivedTypeConstraints \addSeq\topLevelConstraints \addSeq \compoundEvalConstraints \addSeq \compoundConstraints \addSeq \constraintVariablesConstraints \addSeq \collectionCompoundConstraints \addSeq \collectionConstraints$\;
   $t \assng t \cup \setWith{\mapEntry{v}{c}}{v\in variables(c) \wedge c\in c_s}$\; % assignConstraintsToVariables
   $c_s \assng \setWith{c}{c\in c_s \wedge (\neg inc \vee (inc \wedge \neg isAssignmentConstraint(c)))}$\;
@@ -521,5 +542,4 @@
    $\defaultAnnotationConstraints \assng \set{}$\;
    $\assignedAttributeConstraints \assng \set{}$\;
-   $\unresolvedConstraints \assng \set{}$\;
 
  \caption{Translating constraints (\IVML{translateConstraints}).}\label{algTranslateConstraints}