setUnionUnfoldLeft {
\schemaVar \program Variable #v , #vLeftNew ;
\schemaVar \program NonSimpleExpression #nseLeft ;
\schemaVar \program Expression #eRight ;
\schemaVar \formula post ;
\find ( \modality{#allmodal}{.. #v = \set_union(#nseLeft, #eRight); ...}\endmodality ( post ) )
\varcond \replacewith ( \modality{#allmodal}{.. #typeof(#nseLeft) #vLeftNew=#nseLeft; #v = \set_union(#vLeftNew, #eRight); ...}\endmodality ( post ) )
\heuristics (simplify_prog )
\displayname "setUnionUnfold"
};defined in: adtProgramDecompositionRules.key Line: 15 Offset :4setUnionUnfoldRight {
\schemaVar \program Variable #v , #vRightNew ;
\schemaVar \program SimpleExpression #seLeft ;
\schemaVar \program NonSimpleExpression #nseRight ;
\schemaVar \formula post ;
\find ( \modality{#allmodal}{.. #v = \set_union(#seLeft, #nseRight); ...}\endmodality ( post ) )
\varcond \replacewith ( \modality{#allmodal}{.. #typeof(#nseRight) #vRightNew=#nseRight; #v = \set_union(#seLeft, #vRightNew); ...}\endmodality ( post ) )
\heuristics (simplify_prog )
\displayname "setUnionUnfold"
};defined in: adtProgramDecompositionRules.key Line: 28 Offset :4setIntersectUnfoldLeft {
\schemaVar \program Variable #v , #vLeftNew ;
\schemaVar \program NonSimpleExpression #nseLeft ;
\schemaVar \program Expression #eRight ;
\schemaVar \formula post ;
\find ( \modality{#allmodal}{.. #v = \intersect(#nseLeft, #eRight); ...}\endmodality ( post ) )
\varcond \replacewith ( \modality{#allmodal}{.. #typeof(#nseLeft) #vLeftNew=#nseLeft; #v = \intersect(#vLeftNew, #eRight); ...}\endmodality ( post ) )
\heuristics (simplify_prog )
\displayname "setIntersectUnfold"
};defined in: adtProgramDecompositionRules.key Line: 41 Offset :4setIntersectUnfoldRight {
\schemaVar \program Variable #v , #vRightNew ;
\schemaVar \program SimpleExpression #seLeft ;
\schemaVar \program NonSimpleExpression #nseRight ;
\schemaVar \formula post ;
\find ( \modality{#allmodal}{.. #v = \intersect(#seLeft, #nseRight); ...}\endmodality ( post ) )
\varcond \replacewith ( \modality{#allmodal}{.. #typeof(#nseRight) #vRightNew=#nseRight; #v = \intersect(#seLeft, #vRightNew); ...}\endmodality ( post ) )
\heuristics (simplify_prog )
\displayname "setIntersectUnfold"
};defined in: adtProgramDecompositionRules.key Line: 54 Offset :4setMinusUnfoldLeft {
\schemaVar \program Variable #v , #vLeftNew ;
\schemaVar \program NonSimpleExpression #nseLeft ;
\schemaVar \program Expression #eRight ;
\schemaVar \formula post ;
\find ( \modality{#allmodal}{.. #v = \set_minus(#nseLeft, #eRight); ...}\endmodality ( post ) )
\varcond \replacewith ( \modality{#allmodal}{.. #typeof(#nseLeft) #vLeftNew=#nseLeft; #v = \set_minus(#vLeftNew, #eRight); ...}\endmodality ( post ) )
\heuristics (simplify_prog )
\displayname "setMinusUnfold"
};defined in: adtProgramDecompositionRules.key Line: 67 Offset :4setMinusUnfoldRight {
\schemaVar \program Variable #v , #vRightNew ;
\schemaVar \program SimpleExpression #seLeft ;
\schemaVar \program NonSimpleExpression #nseRight ;
\schemaVar \formula post ;
\find ( \modality{#allmodal}{.. #v = \set_minus(#seLeft, #nseRight); ...}\endmodality ( post ) )
\varcond \replacewith ( \modality{#allmodal}{.. #typeof(#nseRight) #vRightNew=#nseRight; #v = \set_minus(#seLeft, #vRightNew); ...}\endmodality ( post ) )
\heuristics (simplify_prog )
\displayname "setMinusUnfold"
};defined in: adtProgramDecompositionRules.key Line: 80 Offset :4singletonUnfold {
\schemaVar \program Variable #v , #a , #vObjNew ;
\schemaVar \program NonSimpleExpression #nseObj ;
\schemaVar \formula post ;
\find ( \modality{#allmodal}{.. #v = \singleton(#nseObj.#a); ...}\endmodality ( post ) )
\varcond \replacewith ( \modality{#allmodal}{.. #typeof(#nseObj) #vObjNew=#nseObj; #v = \singleton(#vObjNew.#a); ...}\endmodality ( post ) )
\heuristics (simplify_prog )
\displayname "singletonUnfold"
};defined in: adtProgramDecompositionRules.key Line: 93 Offset :4singletonAssignment {
\schemaVar \program Variable #v , #a ;
\schemaVar \program SimpleExpression #seObj ;
\schemaVar \formula post ;
\find ( \modality{#allmodal}{.. #v = \singleton(#seObj.#a); ...}\endmodality ( post ) )
\replacewith ( { #v := singleton ( #seObj , #memberPVToField ( #a ) ) } \modality{#allmodal}{.. ...}\endmodality ( post ) )
\heuristics (simplify_prog )
\displayname "singletonAssignment"
};defined in: adtProgramDecompositionRules.key Line: 106 Offset :4allObjectsAssignment {
\schemaVar \program Variable #v , #a ;
\schemaVar \program Expression #eObj ;
\schemaVar \formula post ;
\find ( \modality{#allmodal}{.. #v = \all_objects(#eObj.#a); ...}\endmodality ( post ) )
\replacewith ( { #v := allObjects ( #memberPVToField ( #a ) ) } \modality{#allmodal}{.. ...}\endmodality ( post ) )
\heuristics (simplify_prog )
\displayname "allObjectsAssignment"
};defined in: adtProgramDecompositionRules.key Line: 118 Offset :4allFieldsUnfold {
\schemaVar \program Variable #v , #vObjNew ;
\schemaVar \program NonSimpleExpression #nseObj ;
\schemaVar \formula post ;
\find ( \modality{#allmodal}{.. #v = \all_fields(#nseObj); ...}\endmodality ( post ) )
\varcond \replacewith ( \modality{#allmodal}{.. #typeof(#nseObj) #vObjNew=#nseObj; #v = \all_fields(#vObjNew); ...}\endmodality ( post ) )
\heuristics (simplify_prog )
\displayname "allFieldsAssignment"
};defined in: adtProgramDecompositionRules.key Line: 130 Offset :4seqConcatUnfoldLeft {
\schemaVar \program Variable #v , #vLeftNew ;
\schemaVar \program NonSimpleExpression #nseLeft ;
\schemaVar \program Expression #eRight ;
\schemaVar \formula post ;
\find ( \modality{#allmodal}{.. #v = \seq_concat(#nseLeft, #eRight); ...}\endmodality ( post ) )
\varcond \replacewith ( \modality{#allmodal}{.. #typeof(#nseLeft) #vLeftNew=#nseLeft; #v = \seq_concat(#vLeftNew, #eRight); ...}\endmodality ( post ) )
\heuristics (simplify_prog )
\displayname "seqConcatUnfold"
};defined in: adtProgramDecompositionRules.key Line: 148 Offset :4seqConcatUnfoldRight {
\schemaVar \program Variable #v , #vRightNew ;
\schemaVar \program SimpleExpression #seLeft ;
\schemaVar \program NonSimpleExpression #nseRight ;
\schemaVar \formula post ;
\find ( \modality{#allmodal}{.. #v = \seq_concat(#seLeft, #nseRight); ...}\endmodality ( post ) )
\varcond \replacewith ( \modality{#allmodal}{.. #typeof(#nseRight) #vRightNew=#nseRight; #v = \seq_concat(#seLeft, #vRightNew); ...}\endmodality ( post ) )
\heuristics (simplify_prog )
\displayname "seqConcatUnfold"
};defined in: adtProgramDecompositionRules.key Line: 161 Offset :4seqGetUnfoldLeft {
\schemaVar \program Variable #v , #vLeftNew ;
\schemaVar \program NonSimpleExpression #nseLeft ;
\schemaVar \program Expression #eRight ;
\schemaVar \formula post ;
\find ( \modality{#allmodal}{.. #v = \seq_get(#nseLeft, #eRight); ...}\endmodality ( post ) )
\varcond \replacewith ( \modality{#allmodal}{.. #typeof(#nseLeft) #vLeftNew=#nseLeft; #v = \seq_get(#vLeftNew, #eRight); ...}\endmodality ( post ) )
\heuristics (simplify_prog )
\displayname "seqGetUnfold"
};defined in: adtProgramDecompositionRules.key Line: 174 Offset :4seqGetUnfoldRight {
\schemaVar \program Variable #v , #vRightNew ;
\schemaVar \program SimpleExpression #seLeft ;
\schemaVar \program NonSimpleExpression #nseRight ;
\schemaVar \formula post ;
\find ( \modality{#allmodal}{.. #v = \seq_get(#seLeft, #nseRight); ...}\endmodality ( post ) )
\varcond \replacewith ( \modality{#allmodal}{.. #typeof(#nseRight) #vRightNew=#nseRight; #v = \seq_get(#seLeft, #vRightNew); ...}\endmodality ( post ) )
\heuristics (simplify_prog )
\displayname "seqGetUnfold"
};defined in: adtProgramDecompositionRules.key Line: 187 Offset :4seqIndexOfUnfoldLeft {
\schemaVar \program Variable #v , #vLeftNew ;
\schemaVar \program NonSimpleExpression #nseLeft ;
\schemaVar \program Expression #eRight ;
\schemaVar \formula post ;
\find ( \modality{#allmodal}{.. #v = \indexOf(#nseLeft, #eRight); ...}\endmodality ( post ) )
\varcond \replacewith ( \modality{#allmodal}{.. #typeof(#nseLeft) #vLeftNew=#nseLeft; #v = \indexOf(#vLeftNew, #eRight); ...}\endmodality ( post ) )
\heuristics (simplify_prog )
\displayname "seqIndexOfUnfold"
};defined in: adtProgramDecompositionRules.key Line: 200 Offset :4seqIndexOfUnfoldRight {
\schemaVar \program Variable #v , #vRightNew ;
\schemaVar \program SimpleExpression #seLeft ;
\schemaVar \program NonSimpleExpression #nseRight ;
\schemaVar \formula post ;
\find ( \modality{#allmodal}{.. #v = \indexOf(#seLeft, #nseRight); ...}\endmodality ( post ) )
\varcond \replacewith ( \modality{#allmodal}{.. #typeof(#nseRight) #vRightNew=#nseRight; #v = \indexOf(#seLeft, #vRightNew); ...}\endmodality ( post ) )
\heuristics (simplify_prog )
\displayname "seqIndexOfUnfold"
};defined in: adtProgramDecompositionRules.key Line: 213 Offset :4seqSubUnfoldLeft {
\schemaVar \program Variable #v , #vLeftNew ;
\schemaVar \program NonSimpleExpression #nseLeft ;
\schemaVar \program Expression #eMiddle , #eRight ;
\schemaVar \formula post ;
\find ( \modality{#allmodal}{.. #v = \seq_sub(#nseLeft, #eMiddle, #eRight); ...}\endmodality ( post ) )
\varcond \replacewith ( \modality{#allmodal}{.. #typeof(#nseLeft) #vLeftNew=#nseLeft; #v = \seq_sub(#vLeftNew, #eMiddle, #eRight); ...}\endmodality ( post ) )
\heuristics (simplify_prog )
\displayname "seqSubUnfold"
};defined in: adtProgramDecompositionRules.key Line: 226 Offset :4seqSubUnfoldMiddle {
\schemaVar \program Variable #v , #vMiddleNew ;
\schemaVar \program SimpleExpression #seLeft ;
\schemaVar \program NonSimpleExpression #nseMiddle ;
\schemaVar \program Expression #eRight ;
\schemaVar \formula post ;
\find ( \modality{#allmodal}{.. #v = \seq_sub(#seLeft, #nseMiddle, #eRight); ...}\endmodality ( post ) )
\varcond \replacewith ( \modality{#allmodal}{.. #typeof(#nseMiddle) #vMiddleNew=#nseMiddle; #v = \seq_sub(#seLeft, #vMiddleNew, #eRight); ...}\endmodality ( post ) )
\heuristics (simplify_prog )
\displayname "seqSubUnfold"
};defined in: adtProgramDecompositionRules.key Line: 239 Offset :4seqSubUnfoldRight {
\schemaVar \program Variable #v , #vRightNew ;
\schemaVar \program SimpleExpression #seLeft , #seMiddle ;
\schemaVar \program NonSimpleExpression #nseRight ;
\schemaVar \formula post ;
\find ( \modality{#allmodal}{.. #v = \seq_sub(#seLeft, #seMiddle, #nseRight); ...}\endmodality ( post ) )
\varcond \replacewith ( \modality{#allmodal}{.. #typeof(#nseRight) #vRightNew=#nseRight; #v = \seq_sub(#seLeft, #seMiddle, #vRightNew); ...}\endmodality ( post ) )
\heuristics (simplify_prog )
\displayname "seqSubUnfold"
};defined in: adtProgramDecompositionRules.key Line: 254 Offset :4seqSingletonUnfold {
\schemaVar \program Variable #v , #vNew ;
\schemaVar \program NonSimpleExpression #nse ;
\schemaVar \formula post ;
\find ( \modality{#allmodal}{.. #v = \seq_singleton(#nse); ...}\endmodality ( post ) )
\varcond \replacewith ( \modality{#allmodal}{.. #typeof(#nse) #vNew=#nse; #v = \seq_singleton(#vNew); ...}\endmodality ( post ) )
\heuristics (simplify_prog )
\displayname "seqSingletonUnfold"
};defined in: adtProgramDecompositionRules.key Line: 267 Offset :4seqLengthUnfold {
\schemaVar \program Variable #v , #vNew ;
\schemaVar \program NonSimpleExpression #nse ;
\schemaVar \formula post ;
\find ( \modality{#allmodal}{.. #v = \seq_length(#nse); ...}\endmodality ( post ) )
\varcond \replacewith ( \modality{#allmodal}{.. #typeof(#nse) #vNew=#nse; #v = \seq_length(#vNew); ...}\endmodality ( post ) )
\heuristics (simplify_prog )
\displayname "seqLengthUnfold"
};defined in: adtProgramDecompositionRules.key Line: 280 Offset :4seqReverseUnfold {
\schemaVar \program Variable #v , #vNew ;
\schemaVar \program NonSimpleExpression #nse ;
\schemaVar \formula post ;
\find ( \modality{#allmodal}{.. #v = \seq_reverse(#nse); ...}\endmodality ( post ) )
\varcond \replacewith ( \modality{#allmodal}{.. #typeof(#nse) #vNew=#nse; #v = \seq_reverse(#vNew); ...}\endmodality ( post ) )
\heuristics (simplify_prog )
\displayname "seqReverseUnfold"
};defined in: adtProgramDecompositionRules.key Line: 293 Offset :4