Index: /reasoner/reasoner.tex =================================================================== --- /reasoner/reasoner.tex (revision 58) +++ /reasoner/reasoner.tex (revision 59) @@ -422,5 +422,5 @@ In more detail, Algorithm \ref{algTranslateDeclaration} first declares some local variables in line \ref{algTranslateDeclarationDecl}, including the actual type $t$ (to be overridden by the type of the default value expression if needed), the default value expression $dflt$, the actual set of default constraints ($\defaultConstraints$ or $\deferredDefaultConstraints$) to be utilized for adding the final constraint and the actual value of self $s$ (for compound types only). Then, if $t$ is a derived data type, constraints are translated and collected through Algorithm \ref{algTranslateDerivedDatatypeConstraints}. In non-incremental mode, i.e., we translate default value expressions to assignment constraints as well as the default constraints for annotations can then be translated using \ref{algTranslateAnnotationDefaults}. Due to potential type interferences with derived types, we determine then the actual type through the type of the default value expression if defined. If $t$ is a compound type, we set the value of self $v$ to the actual variable declaration $d$ and execute the specific translations for compound types using Algorithm \ref{algTranslateCompoundDeclaration}. If $t$ is a container type, we call \ref{algTranslateContainerDeclaration} instead. Otherwise, if there is a default value expression and reasoning is not in incremental mode, i.e., we shall translate default value expressions to assignment constraints, and if there is a compound accessor, we just have to schedule a replacement of \IVML{self} by the compound accessor. Remaining default constraints are taken over as defined as long as the reasoner is not operating incremental mode as there no default value assignments are needed. -If there is finally a default value expression to be recorded in the constraint base, we have to distinguish whether the actual variable is a usual or a constraint variable. In the first case, we turn the default value expression into an assignment expression, through the compound accessor if it currently represents \IVML{self}, the variable else. Then, we substitute \IVML{self} and the actual variable mapping on the default value expression. The actual variable is a constraint variable, we can just turn the default value into a constraint, add it to the set of other constraints $\otherConstraints$ and register the relevant variables for the new constraint and the causing variable $v$. For usual variables, turn the already created value assignment expression in $dflt$ into a default constraint and add it either to $\deferredDefaultConstraints$ the constraint may override a complete value assignment (\IVML{self} is used or $d$ is an overridden slot) or to the usual default constraints set $\defaultConstraints$. +If there is finally a default value expression to be recorded in the constraint base, we have to distinguish whether the actual variable is a constraint variable or an usual variable. In the first case, we apply Algorithm \ref{algCreateConstraintVariableConstraint} (cf. Section \ref{sectConstraintVariables}). In the second case, we turn the default value expression into an assignment expression, through the compound accessor if it currently represents \IVML{self}, or the variable. Then, we substitute \IVML{self} and the actual variable mapping on the complete constraint expression and turn the result into a default constraint. We either either it to $\deferredDefaultConstraints$ if the constraint may override a complete value assignment (\IVML{self} is used referring to another variable in the same compound or $d$ is an overridden slot that may accidentally be overriden by a complex compound value) or in all other cases to the usual default constraints set $\defaultConstraints$. \begin{algorithm}[H] @@ -449,8 +449,5 @@ $dflt \assng \varSubstitutionSelfVarMapping{dflt}{s}$\; \uIf{$isConstraint(type(d))$}{ - %\If{$ ca == \undef $ \TBD{really needed???}}{ - $add(\otherConstraints, \createConstraint{dflt}, true)$\; - $\relevantConstraints \assng \relevantConstraints \addMap \mapEntry{\createConstraint{dflt}}{v}$ - %} + $createConstraintVariableConstraint(dflt, s, v)$\; }\Else{ \lIf{$\IVMLself{} \in dflt \vee isOverridenSlot(d)$}{$dfltS \assng \deferredDefaultConstraints$}\lElse{$dfltS \assng \defaultConstraints$} @@ -505,4 +502,31 @@ \end{algorithm} +\subsection{Constraint variables}\label{sectConstraintVariables} + +Constraint variables can be created by taking the respective default/actual variable, performing the variable substitution with $\variableMapping$ and, if available, a respective value for \IVMLself, turning the resulting expression into a constraint and adding it to the set of other constraints $\otherConstraints$. Moreover, the relationship between the underlying variable $v$ and the constraint must be recorded for efficient update of the constraint base upon value change (cf. Algorithm \ref{algVarChange}). + +\begin{algorithm}[H] + \SetAlgoLined + \KwIn{constraint expression $c$, actual value for \IVMLself $s$, variable $v$} + \KwData{other constraints $\otherConstraints$, relevant constraints $\relevantConstraints$} + + $c \assng \createConstraint{\varSubstitutionSelfVarMapping{c}{s}}$\; + $add(\otherConstraints, \set{c}, true)$\; + \MISSING{map v to c for dynamic value type change}\; + $\relevantConstraints \assng \relevantConstraints \addMap \mapEntry{c}{v}$ + + + % $add(\otherConstraints, \set{\createConstraint{\varSubstitutionSelfVarMapping{default(s)}{d}}}, true)$\; + %$add(\otherConstraints, \createConstraint{dflt}, true)$\; + %$\relevantConstraints \assng \relevantConstraints \addMap \mapEntry{\createConstraint{dflt}}{v}$ + + + %\If{$isConstraint(type(s)) \wedge default(s) \neq \undef$}{ + %} + +% $cs \assng \bigcup_{t \in allBase(t} constraints(t)$\; +% $add(\topLevelConstraints, \setWith{\createConstraint{\closedCases{d, & \text{if } ca = \undef \\ ca, &\text{else}}\rightarrow\IVML{forAll}(i|\text{ }\varSubstitution{c}{decl(c)=d})}}{c \in cs}, true)$\; + \caption{Creating constraints for constraint variables (\IVML{createConstraintVariableConstraint}).}\label{algCreateConstraintVariableConstraint} +\end{algorithm} \subsection{Annotation default expressions}\label{sectAnnotationDefaults} @@ -583,7 +607,4 @@ $add(\otherConstraints, \setWith{\createConstraint{\varSubstitutionSelfVarMapping{value(e)}{d}}}{e \in elements(value(s))}, true)$\; } - %\If{$isConstraint(type(s)) \wedge default(s) \neq \undef$}{ - % $add(\otherConstraints, \set{\createConstraint{\varSubstitutionSelfVarMapping{default(s)}{d}}}, true)$\; - %} \If{$isContainer(type(s))$} { $add(\otherConstraints, translateContainerCompoundConstraints(s, v, \variableMapping[s]), true)$\;