Index: /reasoner/reasoner.tex =================================================================== --- /reasoner/reasoner.tex (revision 76) +++ /reasoner/reasoner.tex (revision 77) @@ -613,8 +613,10 @@ $translateDefaultsCompoundsContainer(d, u)$\; }\label{algTranslateContainerDeclarationCompoundContainerDefaultsEnd} - \ForAll{$u \iterAssng used \setminus \setWith{allRefines(u)}{u \in used}$} {\label{algTranslateContainerDeclarationCompoundContainerUsedCompoundsStart} + $used \assng used \setminus \setWith{allRefines(u)}{u \in used}$\; + \lIf{$|used| = 0$}{$used \assng \set{base(contained(d))}$} + \ForAll{$u \iterAssng used$} {\label{algTranslateContainerDeclarationCompoundContainerUsedCompoundsStart} $add(\otherConstraints, translateCompoundContainer(u, t_n, d, ca), true)$\; }\label{algTranslateContainerDeclarationCompoundContainerUsedCompoundsEnd} - $add(\otherConstraints, translateCompoundContainer(d, v, ca, used), true)$\;\label{algTranslateContainerDeclarationCompoundContainerCompounds} + %$add(\otherConstraints, translateCompoundContainer(d, v, ca, used), true)$\;\label{algTranslateContainerDeclarationCompoundContainerCompounds} } \uIf{$isDerived(t_n)$}{ @@ -626,5 +628,7 @@ However, containers are different than usual variables as the may contain an arbitrary number of elements. Thus, for specifying a constraint over a container, we must apply all-quantification (the IVML \IVML{forAll} operation) for all constraints defined on contained types. Moreover, for nested collections we must apply the IMVL \IVML{flatten} operation to gain access to the individual elements, and for refined types even explicit IVML type casts using the \IVML{asType} operation to have access to specific operations, slots or annotations. -Algorithm \ref{algTranslateContainerDeclaration} performs the transformation for a container variable declaration $d$ of variable $v$, if nested with given access expression $ca$ and specific type $t$ (due to a known default value). First, we determine the innermost nested type $t_n$ and its base type $t_b$ (taking derived types into account) as well as the relevant value $val$. If $v$ is a constraint container, i.e., the innermost nested base type is a constraint, we collect and translate all constraints constituted by all (flattened) element values in line \ref{algTranslateContainerDeclarationConstraintContainer}. If $v$ is a compound container, i.e., the innermost nested base type is a compound, we try to derive as many relevant constraints as possible. Therefore, we determine the used contained compound types in line \ref{algTranslateContainerDeclarationUsedTypesDefault}. For all these types, we determine all default value constraints using Algorithm \ref{algTranslateDefaultsCompoundContainer} in lines \ref{algTranslateContainerDeclarationCompoundContainerDefaultsStart}-\ref{algTranslateContainerDeclarationCompoundContainerDefaultsEnd}. Moreover, for all used most specific compound types, we collect and instantiate all compound-related constraints using Algorithm \ref{algTranslateCompoundContainer2} in lines \ref{algTranslateContainerDeclarationCompoundContainerUsedCompoundsStart}-\ref{algTranslateContainerDeclarationCompoundContainerUsedCompoundsEnd}. As Algorithm \ref{algTranslateCompoundContainer2} takes all refined compounds into account, we leave out the refined types from the used containers in line \ref{algTranslateContainerDeclarationCompoundContainerUsedCompoundsStart}. For the remaining, not already translated compound types, we also apply Algorithm \ref{algTranslateCompoundContainer2}, here through Algorithm \ref{algTranslateCompoundContainer} (based on the configured value) in line \ref{algTranslateContainerDeclarationCompoundContainerCompounds}. Independently of constraint or compound container, we finally translate and collect all constraints stemming from derived type definitions in line \ref{algTranslateContainerDeclaration}. +Algorithm \ref{algTranslateContainerDeclaration} performs the transformation for a container variable declaration $d$ of variable $v$, if nested with given access expression $ca$ and specific type $t$ (due to a known default value). First, we determine the innermost nested type $t_n$ and its base type $t_b$ (taking derived types into account) as well as the relevant value $val$. If $v$ is a constraint container, i.e., the innermost nested base type is a constraint, we collect and translate all constraints constituted by all (flattened) element values in line \ref{algTranslateContainerDeclarationConstraintContainer}. If $v$ is a compound container, i.e., the innermost nested base type is a compound, we try to derive as many relevant constraints as possible. Therefore, we determine the used contained compound types in line \ref{algTranslateContainerDeclarationUsedTypesDefault}. For all these types, we determine all default value constraints using Algorithm \ref{algTranslateDefaultsCompoundContainer} in lines \ref{algTranslateContainerDeclarationCompoundContainerDefaultsStart}-\ref{algTranslateContainerDeclarationCompoundContainerDefaultsEnd}. Moreover, for all used most specific compound types (if there are none, we take the contained type of $d$ instead), we collect and instantiate all compound-related constraints using Algorithm \ref{algTranslateCompoundContainer2} in lines \ref{algTranslateContainerDeclarationCompoundContainerUsedCompoundsStart}-\ref{algTranslateContainerDeclarationCompoundContainerUsedCompoundsEnd}. As Algorithm \ref{algTranslateCompoundContainer2} takes all refined compounds into account, we leave out the refined types from the used containers in line \ref{algTranslateContainerDeclarationCompoundContainerUsedCompoundsStart}. +%For the remaining, not already translated compound types, we also apply Algorithm \ref{algTranslateCompoundContainer2}, here through Algorithm \ref{algTranslateCompoundContainer} (based on the configured value) in line \ref{algTranslateContainerDeclarationCompoundContainerCompounds}. +Independently of constraint or compound container, we finally translate and collect all constraints stemming from derived type definitions in line \ref{algTranslateContainerDeclaration}. We turn now to the algorithms that were used by Algorithm \ref{algTranslateContainerDeclaration}. @@ -632,5 +636,5 @@ Algorithm \ref{algTranslateDefaultsCompoundContainer} creates constraints for default value instantiation of compound values directly created in container initializers, e.g., in IVML something like \IVML{seq = \{\{i=1\}, \{i=2\}\}}, assuming that \IVML{seq} is a sequence of compounds, which have an integer slot \IVML{i}. As these compounds are created implicitly within a container initializer, so far no default value constraints are created and scheduled to the constraint base, i.e., these compounds would remain uninitialized. Algorithm \ref{algTranslateDefaultsCompoundContainer} solves this by creating all-quantized constraints over all elements of the container applying the default value expressions to the elements. Utilizing quantor constraints here implies that default initializations, which remain undefined if some dependent variables have not been determined so far, cause a re-evaluation for all elements of the container. Here, unfolding the implicit loop of such a quantor may be a solution, as then only individual constraints are triggered. However, this only works for sequences, as sets do not provide element-wise/index-based access and unfolding the constraint for a large container also may create a huge number of constraints. Currently, we stay with the compromise of creating a single quantized constraint for all slots with default values. -Algorithm \ref{algTranslateDefaultsCompoundContainer} creates the constraint in incremental fashion, considering several special cases but also allowing for optimization. Here, $d$ is a container variable declaration, $t$ the compound type to be processed, i.e., the innermost basic type of $type(d)$ or one of its refining compound types. For each constraint with default values of a given type, we create in line \ref{algTranslateDefaultsCompoundContainerInitE} an expression just holding the variable of the container $d$. If the container is nested, we flatten it in line \ref{algTranslateDefaultsCompoundContainerFlatten} as constraints only need to be created for the elements (no specific constraints can be attached to a container type except for derived values, which are handled by Algorithm \ref{algTranslateDeclaration}). If the actual type $t$ to be processed is not the same as the type of the declaration $type(d)$, we must consider that the slot $s$ only exists for the specific refined type $t$, i.e., the instantiation applies only to container elements of type $t$ (or of refined types), i.e., we insert in line \ref{algTranslateDefaultsCompoundContainerCast} a type selection \TBD{typeSelect, or kind?} operation projecting the container to all elements of type $t$. As preparation for creating the quantor constraint, we create in line \ref{algTranslateDefaultsCompoundContainerTemporary} the temporary iterator $i$ variable of type $t$ and substitute in line \ref{algTranslateDefaultsCompoundContainerSubst} the variables of the default value expression for $u$ according to the actual variable mapping, replacing also \IVMLself{} by $i$ (not slot $s$, which may be of any other type). Finally, we create in line \ref{algTranslateDefaultsCompoundContainerQuantor} the all-quantor for all typed elements $i$ assigning slot $s$ on $i$ the value defined by the substituted default value expression. +Algorithm \ref{algTranslateDefaultsCompoundContainer} creates the constraint in incremental fashion, considering several special cases but also allowing for optimization. Here, $d$ is a container variable declaration, $t$ the compound type to be processed, i.e., the innermost basic type of $type(d)$ or one of its refining compound types. For each constraint with default values of a given type, we create in line \ref{algTranslateDefaultsCompoundContainerInitE} an expression just holding the variable of the container $d$. If the container is nested, we flatten it in line \ref{algTranslateDefaultsCompoundContainerFlatten} as constraints only need to be created for the elements (no specific constraints can be attached to a container type except for derived values, which are handled by Algorithm \ref{algTranslateDeclaration}). If the actual type $t$ to be processed is not the same as the type of the declaration $type(d)$, we must consider that the slot $s$ only exists for the specific refined type $t$, i.e., the instantiation applies only to container elements of type $t$ (or of refined types), i.e., we insert in line \ref{algTranslateDefaultsCompoundContainerCast} an element selection by type kind projecting the container to all elements of type $t$ (and refined types). As preparation for creating the quantor constraint, we create in line \ref{algTranslateDefaultsCompoundContainerTemporary} the temporary iterator $i$ variable of type $t$ and substitute in line \ref{algTranslateDefaultsCompoundContainerSubst} the variables of the default value expression for $u$ according to the actual variable mapping, replacing also \IVMLself{} by $i$ (not slot $s$, which may be of any other type). Finally, we create in line \ref{algTranslateDefaultsCompoundContainerQuantor} the all-quantor for all typed elements $i$ assigning slot $s$ on $i$ the value defined by the substituted default value expression. \begin{algorithm}[H] @@ -644,5 +648,5 @@ } \uIf{$type(d)\neq t$} { - $e\assng\createExpression{\IVML{typeSelect}(e, t)}$\; \label{algTranslateDefaultsCompoundContainerCast} + $e\assng\createExpression{\IVML{selectByKind}(e, t)}$\; \label{algTranslateDefaultsCompoundContainerCast} } $i\assng\createExpression{\IVMLMeta{var}(t)}$\; \label{algTranslateDefaultsCompoundContainerTemporary} @@ -656,22 +660,26 @@ %----------------------------------------------------------------------------------------------------------------- -If $d$ is a container, we must translate and apply all constraints of compounds within that container \TBD{nested containers follow?} to $d$. As Algorithm \ref{algTranslateCompoundContainer} is used within different algorithms, we return the collected constraints here. -The relevant types to be considered includes the contained type of $d$ and the types of all elements. If the respective type is a compound, we perform the actual translation (cf. Algorithm \ref{algTranslateCompoundContainer2}). - -\begin{algorithm}[H] - \SetAlgoLined - \KwIn{declaration $d$, variable $v$, compound access $ca$, compound set $done$} - \KwOut{resulting constraints $c$} - - $c \assng \set$\; - $tc \assng contained(type(d))$\; - \ForAll{$t \iterAssng \set{tc} \cup \setWith{type(value(e))}{e\in allElements(v)}$}{ - \lIf{$isDerived(t)$}{$t \assng base(t)$} - \uIf{$isCompound(t) \wedge (done = \undef \vee done[t]=\undef)$}{ - $c \assng c \cup translateCompoundContainer(t, tc, d, ca)$\; - } - } - \caption{Translating compound constraints from a container (\IVML{translateCompoundContainer}).}\label{algTranslateCompoundContainer} -\end{algorithm} +In addition to the default value expression, we must also consider all constraints for a compound type used in a container. + +%Algorithm \ref{algTranslateCompoundContainer} is called in Algorithm \ref{algTranslateContainerDeclaration} line \ref{algTranslateContainerDeclarationCompoundContainerCompounds} as a fallback even if no relevant value for can be determined. + +%As Algorithm \ref{algTranslateCompoundContainer} is used within different algorithms, we return the collected constraints here. +%The relevant types to be considered includes the contained type of $d$ and the types of all elements. If the respective type is a compound, we perform the actual translation (cf. Algorithm \ref{algTranslateCompoundContainer2}). + +%\begin{algorithm}[H] +% \SetAlgoLined +% \KwIn{declaration $d$, variable $v$, compound access $ca$, compound set $done$} +% \KwOut{resulting constraints $c$} +% +% $c \assng \set$\; +% $tc \assng contained(type(d))$\; +% \ForAll{$t \iterAssng \set{tc} \cup \setWith{type(value(e))}{e\in allElements(v)}$}{ +% \lIf{$isDerived(t)$}{$t \assng base(t)$} +% \uIf{$isCompound(t) \wedge (done = \undef \vee done[t]=\undef)$}{ +% $c \assng c \cup translateCompoundContainer(t, tc, d, ca)$\; +% } +% } +% \caption{Translating compound constraints from a container (\IVML{translateCompoundContainer}).}\label{algTranslateCompoundContainer} +%\end{algorithm}