Index: /reasoner/consTranslation.tex =================================================================== --- /reasoner/consTranslation.tex (revision 203) +++ /reasoner/consTranslation.tex (revision 204) @@ -45,5 +45,5 @@ \uIf{$isAnnotation(v)$}{\label{algTranslateDeclarationCreateACStart} %$ac\assng \closedCases{\IVMLMeta{acc}(d,a), & \text{if } ca = \undef \\ \IVMLMeta{acc}(ca,a), &\text{else}}$\;\label{algTranslateDeclarationTranslateAnnotationAccess} - $ac\assng \IVMLMeta{acc}(ca,a)$\;\label{algTranslateDeclarationTranslateAnnotationAccess} + $ac\assng \IVMLacc{ca}{a}$\;\label{algTranslateDeclarationTranslateAnnotationAccess} }\uElse{ $ac \assng \closedCases{ca, & \text{if } f \neq \undef \\ d, &\text{else}}$\; \label{algTranslateDeclarationTranslateUsualAccess} \label{algTranslateDeclarationTranslateSelf2} @@ -51,5 +51,5 @@ %\leIf{$\IVMLself{} \in var(e_d) \vee isOverridenSlot(d)$}{$c_{e_d} \assng \deferredDefaultConstraints$}{$c_{e_d} \assng \defaultConstraints$} \label{algTranslateDeclarationTranslateSelf3} $c_{e_d} \assng \closedCases{\deferredDefaultConstraints, & \text{if } var(e_d) \vee isOverridenSlot(d)\\ \defaultConstraints, &\text{else}}$\;\label{algTranslateDeclarationTranslateSelf3} - $add(c_{e_d}, \createDefaultConstraint{\varSubstitutionSelfVarMapping{\IVML{assign}(ac, e_d)}{f}}, true, v)$\; \label{algTranslateDeclarationTranslateDefault} + $add(c_{e_d}, \createDefaultConstraint{\varSubstitutionSelfVarMapping{\IVMLassign{ac}{e_d}}{f}}, true, v)$\; \label{algTranslateDeclarationTranslateDefault} }\label{algTranslateDeclarationDefaultEnd} @@ -82,5 +82,5 @@ \grayPara{ \patternDerivationLabel{\IVML{typedef } T \IVML{ with }(c); T\ v\IVML{;}}{\nonumber\\\bigcup_{\begin{matrix}\scriptstyle u\ \in\ \set{t\ \cup\ allBase(T)},\\\scriptstyle c\ \in\ constraints(u)\end{matrix}} \varSubstitution{c}{decl(u)=deref(u, v), \variableMapping}}{formDerivedDatatypeConstraints} - \patternDerivationLabel{\IVML{typedef } containerOf(T) \IVML{ with }(c); T\ v\IVML{;}}{\nonumber\\\bigcup_{\begin{matrix}\scriptstyle u\ \in\ \set{t\ \cup\ allBase(T)},\\\scriptstyle c\ \in\ constraints(u)\end{matrix}} \varSubstitution{v\rightarrow\IVML{forall(i:}c}{decl(u)=deref(u, i), \variableMapping}\IVML{)}}{formDerivedDatatypeConstraintsContainer} + \patternDerivationLabel{\IVML{typedef } containerOf(T) \IVML{ with }(c); T\ v\IVML{;}}{\nonumber\\\bigcup_{\begin{matrix}\scriptstyle u\ \in\ \set{t\ \cup\ allBase(T)},\\\scriptstyle c\ \in\ constraints(u)\end{matrix}} \varSubstitution{\IVMLforall{v}{i}{c}}{decl(u)=deref(u, i), \variableMapping}}{formDerivedDatatypeConstraintsContainer} } @@ -100,5 +100,6 @@ $cs \assng \bigcup_{t \in deref(allBase(t))} constraints(t)$\;\label{algTranslateDerivedDatatypeConstraintsCollectConstraints} \uIf{$isContainer(t)$}{\label{algTranslateDerivedDatatypeConstraintsTranslateCollectionStart} - $cs \assng \setWith{\createConstraint{\varSubstitutionOtherVarMapping{\IVML{forAll(i:}c\IVML{)}}{decl(t)=deref(t, i)}}}{c\in cs}$\; + %$cs \assng \setWith{\createConstraint{\varSubstitutionOtherVarMapping{\IVML{forAll(i:}c\IVML{)}}{decl(t)=deref(t, i)}}}{c\in cs}$\; + $cs \assng \setWith{\createConstraint{\varSubstitutionOtherVarMapping{\IVMLforall{d}{i}{c}}{decl(t)=deref(t, i)}}}{c\in cs}$\; }\Else{\label{algTranslateDerivedDatatypeConstraintsTranslateCollectionEnd}\label{algTranslateDerivedDatatypeConstraintsTranslateOtherStart} $cs \assng \setWith{\createConstraint{\varSubstitutionOtherVarMapping{c}{decl(t)=deref(t, d)}}}{c\in cs}$\; Index: /reasoner/notation.tex =================================================================== --- /reasoner/notation.tex (revision 203) +++ /reasoner/notation.tex (revision 204) @@ -141,8 +141,8 @@ 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|$\constraintWith{c}{\IVML{x}}$)} we denote \IVML{o->forall(x:$\constraintWith{c}{\IVML{x}}$)} to indicate an all-quantized expression over a collection \IVML{o} applying the iterator variable \IVML{x} to some constraint $\constraintWith{c}{\IVML{x}}$. +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{\IVMLassign{\IVML{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{assign} is the constructor for the assign operation defined by IVML. In an algorithm, we may generically denote $\createConstraint{\IVMLassign{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 $\IVMLforallSep{\IVML{o}}{\IVML{x}}{\IVML{|}}{\constraintWith{c}{\IVML{x}}}$ we denote $\IVMLforall{\IVML{o}}{\IVML{x}}{\constraintWith{c}{\IVML{x}}}$ to indicate an all-quantized expression over a collection \IVML{o} applying the iterator variable \IVML{x} to some constraint $\constraintWith{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)}}$. Index: /reasoner/reasoner.tex =================================================================== --- /reasoner/reasoner.tex (revision 203) +++ /reasoner/reasoner.tex (revision 204) @@ -21,6 +21,8 @@ \newcommand\IVMLnull[0]{\texttt{null}} \newcommand\IVMLMeta[1]{\texttt{#1}} %\underline{} -\newcommand\IVMLforalla[4]{#1\rightarrow\IVML{forall(}#2#3#4\IVML{(}} -\newcommand\IVMLforall[3]{\IVMLforall{#1}{#2}{:}{#3}} +\newcommand\IVMLforallSep[4]{#1\IVML{->forall(}#2#3#4\IVML{)}} +\newcommand\IVMLforall[3]{\IVMLforallSep{#1}{#2}{:}{#3}} +\newcommand\IVMLacc[2]{\IVMLMeta{acc}\IVML{(}#1,#2\IVML{)}} +\newcommand\IVMLassign[2]{\IVMLMeta{assign}\IVML{(}#1,#2\IVML{)}} \newcommand\addSet[0]{\cup} \newcommand\addSeq[0]{\oplus}