Index: /reasoner/reasoner.tex =================================================================== --- /reasoner/reasoner.tex (revision 78) +++ /reasoner/reasoner.tex (revision 79) @@ -181,5 +181,5 @@ A \emph{constraint} is a Boolean expression that must always evaluate to $true$. Otherwise, reasoning shall either fail or, after a change of at least one of the involved variables, the constraint shall be re-evaluated potentially wiping out previous reasoning errors for that constraint. A constraint consists of expressions, that can evaluate to values of some type supported by IVML. These expressions can be used to determine the default value of variables. -Moreover, \emph{Constraint} is an IVML type, indicating that a variable actually holds a constraint. From the reasoning point of view, a constraint stored as a value in a constraint variable is evaluated as any other constraint. However, the value in such a variable may, as for all other variables, be undefined, frozen, or re-defined (once per project scope) implying that the old constraint must be discarded or even replaced by the new constraint value and considered by the reasoning process. +Moreover, \IVML{Constraint} is an IVML type, indicating that a variable actually holds a constraint. From the reasoning point of view, a constraint stored as a value in a constraint variable is evaluated as any other constraint. However, the value in such a variable may, as for all other variables, be undefined, frozen, or re-defined (once per project scope) implying that the old constraint must be discarded or even replaced by the new constraint value and considered by the reasoning process. We define two basic functions for constraints: $isConstraint(t)$ indicates whether type $t$ is a constraint type. $isAssignmentConstraint(c)$ indicates whether constraint $c$ is supposed to change the value of a variable through an assignment, e.g., for an integer variable \IVML{x} in IVML notation \IVML{x = 25;}. @@ -325,9 +325,11 @@ \newcommand\problemRecords[0]{m} -The reasoner performs forward reasoning, i.e., it identifies relevant constraints (according to the reasoning mode), translates the constraints, evaluates them in a loop until all constraints are processed and adjusts/extends the constraint set upon variable value changes. Figure \ref{figStructure} shows the call graph of the reasoner algorithms and the sections where we will discuss them in more detail. This section introduces the top-level reasoning algorithms, in particular the main reasoning loop in Section \ref{sectTopLevelMainReasoningLoop}, the global variable mapping structure used during the translation in Section \ref{sectVarMapping}, the top-level constraint translation in Section \ref{sectTopLevelConstraintsTranslation}, the top-level constraint evaluation in Section \ref{sectTopLevelConstraintsEvaluation} and the re-scheduling of constraints while evaluation in Section \ref{sectTopLevelConstraintsRescheduling}. The constraint translation will be discussed in detailed in Section \ref{sectTranslation}. +The reasoner performs forward reasoning, i.e., it identifies relevant constraints (according to the reasoning mode), translates the constraints, evaluates them in a loop until all constraints are processed and adjusts/extends the constraint set upon variable value changes. Figure \ref{figStructure} shows the call graph of the reasoner algorithms and the sections where we will discuss them in more detail. Some algorithms call others recursively due to the potentially recursive structure of some IVML types, in particular compounds and containers. Algorithm \ref{algAddConstraint} and \ref{algComposeExpression} appear disconnected, but are called by most of the translation algorithms to populate the constraint base and to compose complex constraints from recursive nesting of containers and compounds. + +This section introduces the top-level reasoning algorithms, in particular the main reasoning loop in Section \ref{sectTopLevelMainReasoningLoop}, the global variable mapping structure used during the translation in Section \ref{sectVarMapping}, the top-level constraint translation in Section \ref{sectTopLevelConstraintsTranslation}, the top-level constraint evaluation in Section \ref{sectTopLevelConstraintsEvaluation} and the re-scheduling of constraints while evaluation in Section \ref{sectTopLevelConstraintsRescheduling}. The algorithms for constraint translation will be discussed in detailed in Section \ref{sectTranslation}. \begin{figure}[ht] \center -\includegraphics[scale=0.50]{figures/structure.eps} +\includegraphics[scale=0.40]{figures/structure.eps} \caption{Structuring blocks, algorithms and sections.} \label{figStructure} @@ -693,14 +695,4 @@ Algorithm \ref{algTranslateCompoundContainer} creates constraints for compound values utilized in compounds, e.g., through a container initialize, in IVML 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, nested constraints, annotation assignments etc. are scheduled to the constraint base, i.e., these compounds would remain uninitialized and their constraints not considered. -Algorithm \ref{algTranslateCompoundContainer} solves this by creating all-quantized constraints over all elements of the container, mostly be reusing Algorithm \ref{algRegisterCompoundMapping} to create a compound mapping and Algorithm \ref{algTranslateCompoundContent} to translate the compound content. Initially, we a local variable $l$ as later iterator variable for the quantifier expressions. Then, we create a prefix expression $e$ of the quantor constraint expression, i.e., we determine in line \ref{algTranslateDefaultsCompoundContainerInitE} the access expression to the collection either using $ca$ or 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$ is not the same as the type of the declaration $u)$, we must consider that the slot $s$ only exists for the specific refined type $t$. Then, the instantiation shall apply only to container elements of type $t$ (or of refined types), i.e., we insert in line \ref{algTranslateDefaultsCompoundContainerCast} an element selection by projecting the container to all elements of type $t$ (and refined types). - -Now we create a context for the container on the stack of $\variableMapping$. In contrast to compound translations, we also register the prefix expression $e$ and the iterator variable $l$. As for compounds, we create now the compound mapping using Algorithm \ref{algTranslateCompoundContent}. Please note that slot access now happens via the iterator variable $l$, while annotation access happens through $ca$. Specifying $t$ also as target type avoids unnecessary type casts here. Then, we call Algorithm \ref{algTranslateCompoundContent} to translate the compound slots, implying translation of annotations as well as recursion over further compounds and containers. - - - -\TBD{Recursive case.} - -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. - \begin{algorithm}[H] \SetAlgoLined @@ -722,4 +714,35 @@ \caption{Translating constraints for compound containers (\IVML{translateCompoundContainer}).}\label{algTranslateCompoundContainer} \end{algorithm} + +Algorithm \ref{algTranslateCompoundContainer} targets this by creating all-quantized constraints over all elements of the container, mostly be reusing Algorithm \ref{algRegisterCompoundMapping} to create a compound mapping and Algorithm \ref{algTranslateCompoundContent} to translate the compound content. Initially, we a local variable $l$ as later iterator variable for the quantifier expressions. Then, we create a prefix expression $e$ of the quantor constraint expression, i.e., we determine in line \ref{algTranslateDefaultsCompoundContainerInitE} the access expression to the collection either using $ca$ or 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$ is not the same as the type of the declaration $u)$, we must consider that the slot $s$ only exists for the specific refined type $t$. Then, the instantiation shall apply only to container elements of type $t$ (or of refined types), i.e., we insert in line \ref{algTranslateDefaultsCompoundContainerCast} an element selection by projecting the container to all elements of type $t$ (and refined types). + +Now we create a context for the container on the stack of $\variableMapping$. In contrast to compound translations, we also register the prefix expression $e$ and the iterator variable $l$. This will be taken up by the $add$ operation, which completes the full constraint from the given information on the stack, i.e., the full creation of the constraint is prepared but not shown in Algorithm \ref{algRegisterCompoundMapping}. As for compounds, we create now the compound mapping using Algorithm \ref{algTranslateCompoundContent}. Please note that slot access now happens via the iterator variable $l$, while annotation access happens through $ca$. Specifying $t$ also as target type avoids unnecessary type casts here. Then, we call Algorithm \ref{algTranslateCompoundContent} to translate the compound slots, implying translation of annotations as well as recursion over further compounds and containers. + +By storing constraint information on the stack of $\variableMapping$ and assembling the information in one place, we can even handle recursive compound containers, which leads to a recursive creation of constraints. The formula below indicates the constraint that we must create in case of a compound container nested into a compound container. +% +$$ +\underbrace{\underbrace{ca}_{1: ca}\rightarrow \IVML{flatten}}_{1:e}\rightarrow\IVML{forAll}(\underbrace{l}_{1:l}|\underbrace{\underbrace{l.s}_{2: ca}\rightarrow\IVML{flatten}}_{2:e}\rightarrow\IVML{forAll}(\underbrace{l_2}_{2:l}|\varSubstitutionOtherVarMapping{c}{l_2})) +$$ +% +In the first iteration, we start with $ca$ (indicated by $1:ca$, may also be some $d$) and append flatten/typeSelect as needed to form $e$ (indicated by $1:e$, i.e., recursion level and parameter/variable name). In the first iteration, we also create a temporary variable $l$ as iterator variable. We store $l$ and $e$ on the stack of $\variableMapping$ and pass $l$ on as accessor to the translation of compound content in Algorithm \ref{algTranslateCompoundContent}. There, we create an accessor for a slot, let's say $s$, i.e. $l.s$, which is then passed on in line \ref{algTranslateCompoundDeclarationTranslateSlotsV} or \ref{algTranslateCompoundDeclarationTranslateSlotsT}, respectively, to the translation of declarations in Algorithm \ref{algTranslateDeclaration}. As a further compound container is nested into the initial compound container, we end up again in Algorithm \ref{algTranslateCompoundContainer}. Now $l.s$ is considered as accessor (indicated by $2:ca$), flatten(typeSelect are added as needed to form $e$ (now $2:e$), which is stored along with the temporary iterator variable $l_2$ on the stack. If we now want to create a constraint $c$ in this context, we perform a variable substitution in particular injecting $l_2$ as $ca$ into $c$ and pass $\varSubstitutionOtherVarMapping{c}{l_2}$ on to the $add$ algorithm (details in Section \ref{algAddConstraints}). As a first step, the $add$ algorithm executes Algorithm \ref{algComposeExpression}, which composes the full constraint. + +Let us assume that $stack(\variableMapping)$ returns the contex frames of the stack starting with the top frame, $container(s)$ returns the container expression assigned to context frame $s$ and $iterator(s)$ the iterator variable for $s$. The, Algorithm \ref{algComposeExpression} creates a constraint of the form shown above inside out, starting with $c$ after correct variable substition. For each stack element that has a container (we assume also an iterator variable) assigned, which is not the case for context frames created for compounds, we surround the actual $c$ by an all-quantor, running over $container(s)$ using $iterator(s)$ as iterator variable and $c$ as quantor expression. + +\begin{algorithm}[H] + \SetAlgoLined + \KwIn{constraint $c$} + \KwOut{composed constraint $c$} + \KwData{variable mapping $\variableMapping$} + + \ForAll{$s \iterAssng stack(\variableMapping)$} { + \If{$container(s) \neq \undef$} { + $c \assng \createExpression{container(s)\rightarrow\IVML{forAll}(iterator(s)|c)}$\; + } + } + \Return $c$\; + \caption{Composing constraints from $\variableMapping$ (\IVML{composeExpression}).}\label{algComposeExpression} +\end{algorithm} + +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. @@ -946,5 +969,5 @@ \item Try to figure out whether a certain \textbf{constraint (type) is actually needed} for reasoning and avoid its translation/creation wherever feasible. \TBD{Can we move the decision about keeping a constraint from adding it to the constraint base before constraint creation. However, this requires changes/additional alternatives for different code parts.}. Thus, don't re-process or filter certain constraint types at the end (done in the initial version for default and derived type constraints), as this implies iterating multiple times over the (partial) constraint base and re-creating/throwing away constraint instances in memory. \item \TBD{Avoid storing constraints that can be \textbf{processed immediately}, e.g., default constraints without dependencies. However, if a default constraint fails, it must be added to the constraint basis for later possible re-evaluation if dependent values become available/right.} - \item For identifying whether constraints are already in the constraint base, use a \textbf{fast look-up structure} instead of an iteration over the constraint base. Although the initial implementation utilized here reference equality (faster than the equals method), the current lookup structure is significantly faster (approx. 600 ms on large models, at that time around 25\% of runtime) than the original approach trading off execution speed for (peek) memory. Here a lookup structure based on reference equality could further speed up reasoning, which, however, may in the end be slower than the built in collections due to JIT compilation and JVM optimization effects. + \item For identifying whether constraints are already in the constraint base, use a \textbf{fast look-up structure} instead of an iteration over the constraint base. Although the initial implementation utilized here reference equality (faster than the equals method), the current lookup structure is significantly faster (approx. 600 ms on large models, at that time around 25\% of runtime) than the original approach trading off execution speed for (peek) memory. Here a lookup structure based on reference equality could further speed up reasoning, which, however, may in the end be slower than the built in collections due to JIT compilation and JVM optimization effects. This is even true for the stack-based variable mapping $\variableMapping$, which performs as fast as a flat map, which may roughly serve for the main purpose of $\variableMapping$, but not for composing complex constraints from nested compunds and containers. \item Incremental reasoning using a \textbf{stored constraint base} may speed up reasoning but only achieves this through large memory allocations. Ensure initializing the model through default constraints so that the actual stored constraint base only contains really needed constraint types, i.e., no default constraints and, if possible, no constraints for which all depending variables are already frozen. \item \textbf{Reuse visitor instances} if applied more than once, in particular reasoners with more complex internal data structures such as maps or lists. This required some refactoring of the IVML model implementation.