Index: /reasoner/notation.tex =================================================================== --- /reasoner/notation.tex (revision 186) +++ /reasoner/notation.tex (revision 187) @@ -139,17 +139,20 @@ \IVML{Constraint} is an IVML type, indicating that a variable actually holds a constraint. $isConstraint(t)$ indicates whether type $t$ is a constraint type, From the reasoning point of view, a constraint stored in a constraint variable is extracted and evaluated as any other constraint. The value in such a variable may, as for all other variables, be undefined, re-defined (once per project scope), set to \IVMLnull{} or frozen, implying that the old constraint must be discarded, potentially replaced by the new constraint (value) and considered in the subsequent reasoning process. %$isAssignmentConstraint(c)$ indicates whether constraint $c$ is supposed to unconditionally change the value of a variable through an assignment, e.g., for an integer variable \IVML{x} the constraint \IVML{x = 25;} in IVML notation is an assignment Constraint. -During the constraint instantiation, variables must be substituted by other variables or expressions. Let $c$ be a constraint and \IVML{y} be some IVML variable. Then $\varSubstitution{c}{x = y}$ leads to the substitution of all variables named \IVML{x} by \IVML{y}. For example, if the constraint $c$ was before the substitution \IVML{x = 25}, it will be \IVML{y = 25} after the substitution. The right side of a substitution can be a variable or, more generally, an expression. Substitutions are transitive, i.e., in $\varSubstitution{c}{x=y,y=z}$ $x$ will be replaced by $z$. If the right side of a substitution is $\undef$, no substitution happens, e.g., in $\varSubstitution{c}{x = \undef}$. Substitutions can also be expressed in terms of a mapping to express multiple substitutions or to create up / reuse the substitution specification for several constraints. Let $\variableMapping=\set{\mapEntry{x}{e}}$ be a mapping, then $x$ is the variable to be replaced, $e$ the replacing variable/expression and $\varSubstitutionVarMapping{c}$ denotes the respective substitution. Both notations can be combined, e.g., to $\varSubstitutionOtherVarMapping{c}{x = y}$. - -During the constraint instantiation, also new constraints must be created. For this purpose, we use a specific notation to indicate constraint creation and the construction of sub-expressions. This notation combines algorithm elements, e.g., variables, carrying actual values/elements (written in mathematical notation) and IVML expression constructors (stated in teletype). For example, for creating the IVML constraint \IVML{x = 25;} we write $\createConstraint{\IVML{assign(x, 25)}}$. The angle brackets indicate a constraint creation, the contents of the brackets the creation of the expression making up the constraint. Here, \IVML{assng} is the constructor for the assign operation defined by IVML (actually implementing the assignment in \IVML{x = 25}) returning a Boolean value indicating whether the execution of the operation succeeded. In an algorithm, we may generically denote $\createConstraint{\IVML{assign}(x, 25)}$, with $x$ being determined by the algorithm. - - -As usual in IVML, we denote the creation of collection operations using the arrow and iterator notation. However, as we use the '$|$' symbol for variable substitutions, also using the same symbol in IVML quantor expressions may be confusing. Thus, we use in this document ':' instead of '$|$', e.g., we denote \IVML{forall(x:$c(x)$)} to indicate the construction of an all-quantized expression over a constraint using the quantor iterator variable $x$ instead of \IVML{forall(x|$c(x)$)}. In summary, let \IVML{o} be an IVML collection of Integers, then \IVML{o->forall(i:i>20);} requires that all values in $o$ must be greater than 20. To create such a constraint with $o$ being an algorithm variable, we denote $\createConstraint{o\IVML{->forall(i:i>20)}}$. - -To perform specific instantiations, the reasoning mechanism must classify constraints, in particular default value assignments over usual constraints. We indicate default value constraints by `$d$' in the constraint creation notation. For example, for creating a default constraint, we denote $\createDefaultConstraint{\IVML{assign}(x, 25)}$ for which the operation $\isDefaultConstraintName$ returns $true$. Further, we allow attaching additional information to a constraint, e.g., the type it was created for. Let $c$ be a constraint, then $attach(c, t)$ is an operation that attaches $t$ to constraint $c$ and returns $c$. The operation $attached(c)$ return the respective attachment. +During the constraint translation, variables must be substituted by other variables or expressions. Let $c$ be a constraint and \IVML{y} be some variable or, more generally, some expression. Then $\varSubstitution{c}{x = y}$ denotes the substitution of all variables named \IVML{x} by \IVML{y}. For example, if the constraint $c$ was \IVML{x = 25} before the substitution, then the result of $\varSubstitution{c}{x=y}$ with $y$ being a variable is \IVML{y = 25} after the substitution. Substitutions are transitive, i.e., in $\varSubstitution{c}{x=y,y=z}$ $x$ is ultimately replaced by $z$. If the right side of a substitution is $\undef$, no substitution happens, e.g., in $\varSubstitution{c}{x = \undef}$. Substitutions can also be expressed in terms of a mapping to express multiple substitutions or to reuse the substitution specification for several constraints. Let $\variableMapping=\set{\mapEntry{x}{e}}$ be a mapping, then $x$ is the variable to be replaced, $e$ the replacing variable/expression and $\varSubstitutionVarMapping{c}$ denotes a substitution based on the mappings in $\variableMapping$. Both notations can be combined, e.g., in $\varSubstitutionOtherVarMapping{c}{x = y}$. + +While constraint translation, also new constraints must be created. We use a specific notation to indicate constraint creation as well as the construction of sub-expressions. This notation combines algorithm elements, e.g., variables, carrying actual values/elements (written in mathematical notation) and IVML expression constructors (stated in teletype). For example, for creating the IVML constraint \IVML{x = 25;} for the IVML variable \IVML{x} we write $\createConstraint{\IVML{assign(x, 25)}}$\footnote{We rely on this form of notation as it is rather close to the implementation for which we aim to provide a detailed documentation here.}. The angle brackets indicate a constraint creation, the contents of the brackets the creation of the expression making up the constraint. Here, \IVML{assng} is the constructor for the assign operation defined by IVML. In an algorithm, we may generically denote $\createConstraint{\IVML{assign}(x, 25)}$, with $x$ being an algorithm variable controlled by the algorithm. + + +As usual in IVML, we denote collection operations using the arrow and iterator notation, which involves the $|$ symbol for separating iterator variables from iterator expressions. However, as we use in this document the '$|$' symbol for variable substitutions, also using the same symbol in IVML collection expressions may be confusing. Thus, we use in collection expressions in this document ':' instead of '$|$', e.g., instead of \IVML{o->forall(x|$c(\IVML{x})$)} we denote \IVML{o->forall(x:$c(\IVML{x})$)} to indicate an all-quantized expression over a collection \IVML{o} applying the iterator variable \IVML{x} to some constraint $c(\IVML{x})$. +%In summary, let \IVML{o} be an IVML collection of Integers, then \IVML{o->forall(i:i>20);} requires that all values in $o$ must be greater than 20. To create such a constraint with $o$ being an algorithm variable, we denote $\createConstraint{o\IVML{->forall(i:i>20)}}$. + +In some case, the reasoning mechanism must classify constraints, in particular to identify the assignment of default values. We indicate such default value assignment constraints by `$d$' in the constraint creation notation. For example, for creating a default assignment constraint, we denote $\createDefaultConstraint{\IVML{assign}(x, 25)}$. For such a constraint $c$ the function $\isDefaultConstraintName(c)$ returns $true$. Further, we allow attaching additional information to a constraint, e.g., the type it was created for. Let $c$ be a constraint, then $attach(c, t)$ is an operation that attaches $t$ to constraint $c$ and returns $c$. The operation $attached(c)$ return the respective attachment. %Similarly, we denote creating a constraint originating from a constraint variable by `$c$', e.g., $b \assng \createConstraintConstraint{\IVML{assign}(x, 25)}$ for which $\isConstraintConstraint{b} = true$ holds. -In some cases, constraints cannot be created in terms of a single step, i.e., sub-expressions are created iteratively. To indicate this, we denote the creation of an expression by $\createExpression{expr}$, e.g., $\createExpression{\IVML{add}(x, 25)}$ for the IVML expression \IVML{x + 25}. When creating expressions, in particular in an incremental fashion, sometimes a temporary (local) IVML variable is needed, e.g., for an IVML let-expression or a container iterator. We state the creation of such a variable by $\IVMLMeta{var}(t)$, i.e., request the creation of a temporary variable\footnote{We don't care for the variable name in this document.} of type $t$. For a variable $v=\IVMLMeta{var}(t)$ holds $isLocal(v) = true$. - -Before reasoning over the constraints given in an IVML project, several kinds of constraints must be transformed, in particular to instantiate constraints defined for types through qualifying access expressions based on top-level variables. To illustrate the transformations performed by an algorithm in this document, we apply constraint transformation patterns. A \emph{constraint transformation pattern} indicates how a certain IVML model fragment is instantiated to a corresponding constraint given in IVML constraint notation rather than the algorithm notation for creating constraints introduced in this section. The model fragment acting as prerequisite is given on the left side of the derivation symbol $\patternDerivationSymbol$, the corresponding constraint on the right side of $\patternDerivationSymbol$. In such a pattern, variable parts are given in italics to indicate the information flow between both sides. Constant parts are given in normal font, IVML syntax in \IVML{teletype}. One or more transformation patterns are displayed in a gray box. For example, the pattern below indicates that an IVML declaration for variable $v$ (with type $T$ and default value expression $deflt$) is translated into an assignment constraint, which assigns the (value of the) default expression $deflt$ to $v$. +Often, constraints cannot be created in a single step, i.e., a constraint must be created iteratively from sub-expressions. To indicate this, we denote the creation of an expression by $\createExpression{expr}$, e.g., $\createExpression{\IVML{add}(x, 25)}$ for the IVML expression \IVML{x + 25}. When creating container (iterator) expressions incrementally, also a notation for creating a temporary (local) IVML variable is needed. We state the creation of such a variable by $\IVMLMeta{var}(t)$ and indicate thereby the creation of a local variable\footnote{We don't care for the variable name in this document.} of type $t$. For a variable $v=\IVMLMeta{var}(t)$, $isLocal(v) = true$ holds. + +Before reasoning over the constraints given in an IVML project, several kinds of constraints must be transformed, in particular to instantiate constraints defined for types through qualifying access expressions based on top-level variables. To provide an overview of the transformations performed by an algorithm, we use constraint transformation patterns. The algorithm then applies constraint and expression creations as well as variable substitutions to realize the respective transformations. + +A \emph{constraint transformation pattern} indicates how a certain IVML model fragment is instantiated to a corresponding constraint given in IVML constraint notation rather than the algorithm notation for creating constraints introduced in this section. The model fragment acting as prerequisite is given on the left side of the derivation symbol $\patternDerivationSymbol$, the corresponding constraint on the right side of $\patternDerivationSymbol$. In such a pattern, variable parts are given in italics to indicate the information flow between both sides. Constant parts are given in normal font, IVML syntax in \IVML{teletype}. One or more transformation patterns are displayed in a gray box. For example, the pattern below indicates that an IVML declaration for variable $v$ (with type $T$ and default value expression $deflt$) is translated into an assignment constraint, which assigns the (value of the) default expression $deflt$ to $v$. \grayPara{