Multi Sets

key.core/src/main/antlr4/JmlLexer.g4

@@ -266,6 +266,7 @@ MAP_UPDATE:  '\\map_update';  //KeY extension, not official JML
 MAX: '\\max';
 E_MEASURED_BY: '\\measured_by' -> type(MEASURED_BY);
 MIN: '\\min';
+MSET: '\\mset';  //KeY extension, not official JML
 NEWELEMSFRESH: '\\new_elems_fresh';  //KeY extension, not official JML
 NEW_OBJECTS: '\\new_objects';  //KeY extension, not official JML
 NONNULLELEMENTS: '\\nonnullelements';

key.core/src/main/antlr4/JmlParser.g4

@@ -383,7 +383,7 @@ sequence
 
 mapExpression: MAP_GET | MAP_OVERRIDE | MAP_UPDATE | MAP_REMOVE | IN_DOMAIN | DOMAIN_IMPLIES_CREATED | MAP_SIZE | MAP_SINGLETON | IS_FINITE;
 fpOperator: FP_ABS | FP_INFINITE | FP_NAN | FP_NEGATIVE | FP_NICE | FP_NORMAL | FP_POSITIVE | FP_SUBNORMAL;
-quantifier: FORALL | EXISTS | MIN | MAX | NUM_OF | PRODUCT | SUM;
+quantifier: FORALL | EXISTS | MIN | MAX | NUM_OF | PRODUCT | SUM | MSET;
 infinite_union_expr: LPAREN UNIONINF (boundvarmodifiers)? quantifiedvardecls SEMI (predicate SEMI)* storeref RPAREN;
 specquantifiedexpression: LPAREN quantifier (boundvarmodifiers)? quantifiedvardecls SEMI (expression SEMI)? expression RPAREN;
 oldexpression: (PRE LPAREN expression RPAREN | OLD LPAREN expression (COMMA IDENT)? RPAREN);

key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeYConverter.java

@@ -23,6 +23,7 @@
 import de.uka.ilkd.key.java.expression.literal.*;
 import de.uka.ilkd.key.java.expression.operator.*;
 import de.uka.ilkd.key.java.expression.operator.adt.*;
+import de.uka.ilkd.key.java.expression.operator.mset.*;
 import de.uka.ilkd.key.java.recoderext.ImplicitFieldAdder;
 import de.uka.ilkd.key.java.recoderext.ImplicitIdentifier;
 import de.uka.ilkd.key.java.reference.*;
@@ -723,6 +724,47 @@ public SeqPut convert(de.uka.ilkd.key.java.recoderext.adt.SeqPut e) {
         return new SeqPut(children);
     }
 
+
+    public EmptyMSetLiteral convert(de.uka.ilkd.key.java.recoderext.mset.EmptyMSetLiteral e) {
+        return EmptyMSetLiteral.INSTANCE;
+    }
+
+    public MSetUnion convert(de.uka.ilkd.key.java.recoderext.mset.MSetUnion e) {
+        ExtList children = collectChildren(e);
+        return new MSetUnion(children);
+    }
+
+    public MSetSum convert(de.uka.ilkd.key.java.recoderext.mset.MSetSum e) {
+        ExtList children = collectChildren(e);
+        return new MSetSum(children);
+    }
+
+    public MSetDiff convert(de.uka.ilkd.key.java.recoderext.mset.MSetDiff e) {
+        ExtList children = collectChildren(e);
+        return new MSetDiff(children);
+    }
+
+    public MSetIntersect convert(de.uka.ilkd.key.java.recoderext.mset.MSetIntersect e) {
+        ExtList children = collectChildren(e);
+        return new MSetIntersect(children);
+    }
+
+    public MSetSingle convert(de.uka.ilkd.key.java.recoderext.mset.MSetSingle e) {
+        ExtList children = collectChildren(e);
+        return new MSetSingle(children);
+    }
+
+    public MSetMul convert(de.uka.ilkd.key.java.recoderext.mset.MSetMul e) {
+
+        return new MSetMul(collectChildren(e));
+    }
+
+    public MSetCard convert(de.uka.ilkd.key.java.recoderext.mset.MSetCard e) {
+
+        return new MSetCard(collectChildren(e));
+    }
+
+
     public EmptyMapLiteral convert(de.uka.ilkd.key.java.recoderext.adt.EmptyMapLiteral e) {
         return EmptyMapLiteral.INSTANCE;
     }

key.core/src/main/java/de/uka/ilkd/key/java/TypeConverter.java

@@ -111,6 +111,10 @@ public SeqLDT getSeqLDT() {
         return (SeqLDT) getLDT(SeqLDT.NAME);
     }
 
+    public MSetLDT getMSetLDT() {
+        return (MSetLDT) getLDT(MSetLDT.NAME);
+    }
+
     public SortLDT getSortLDT() {
         return (SortLDT) getLDT(SortLDT.NAME);
     }

key.core/src/main/java/de/uka/ilkd/key/java/abstraction/PrimitiveType.java

@@ -8,6 +8,7 @@
 
 import de.uka.ilkd.key.java.expression.Literal;
 import de.uka.ilkd.key.java.expression.literal.*;
+import de.uka.ilkd.key.java.expression.literal.EmptyMSetLiteral;
 import de.uka.ilkd.key.ldt.*;
 import de.uka.ilkd.key.logic.ProgramElementName;
 
@@ -57,6 +58,8 @@ public final class PrimitiveType implements Type {
         new PrimitiveType("\\map", EmptyMapLiteral.INSTANCE, MapLDT.NAME);
     public static final PrimitiveType JAVA_TYPE =
         new PrimitiveType("\\TYPE", NullLiteral.NULL, SortLDT.NAME);
+    public static final PrimitiveType JAVA_MSET =
+        new PrimitiveType("\\mset", EmptyMSetLiteral.INSTANCE, MSetLDT.NAME);
 
     public static final PrimitiveType PROGRAM_SV = new PrimitiveType("SV", null, null);
 

key.core/src/main/java/de/uka/ilkd/key/java/expression/literal/EmptyMSetLiteral.java

@@ -0,0 +1,44 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package de.uka.ilkd.key.java.expression.literal;
+
+import de.uka.ilkd.key.java.Services;
+import de.uka.ilkd.key.java.abstraction.KeYJavaType;
+import de.uka.ilkd.key.java.abstraction.PrimitiveType;
+import de.uka.ilkd.key.java.expression.Literal;
+import de.uka.ilkd.key.java.visitor.Visitor;
+import de.uka.ilkd.key.ldt.MSetLDT;
+
+import org.key_project.logic.Name;
+
+public class EmptyMSetLiteral extends Literal {
+
+    public static final EmptyMSetLiteral INSTANCE = new EmptyMSetLiteral();
+
+    private EmptyMSetLiteral() {}
+
+    @Override
+    public boolean equals(Object o) {
+        return o == this;
+    }
+
+    @Override
+    protected int computeHashCode() {
+        return System.identityHashCode(this);
+    }
+
+    public void visit(Visitor v) {
+        v.performActionOnEmptyMSetLiteral(this);
+    }
+
+
+    public KeYJavaType getKeYJavaType(Services javaServ) {
+        return javaServ.getJavaInfo().getKeYJavaType(PrimitiveType.JAVA_MSET);
+    }
+
+    @Override
+    public Name getLDTName() {
+        return MSetLDT.NAME;
+    }
+}

key.core/src/main/java/de/uka/ilkd/key/java/expression/literal/EmptySeqLiteral.java

@@ -34,7 +34,6 @@ public void visit(Visitor v) {
         v.performActionOnEmptySeqLiteral(this);
     }
 
-
     public KeYJavaType getKeYJavaType(Services javaServ) {
         return javaServ.getJavaInfo().getKeYJavaType(PrimitiveType.JAVA_SEQ);
     }

key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/mset/MSetCard.java

@@ -0,0 +1,49 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package de.uka.ilkd.key.java.expression.operator.mset;
+
+import de.uka.ilkd.key.java.Services;
+import de.uka.ilkd.key.java.abstraction.KeYJavaType;
+import de.uka.ilkd.key.java.abstraction.PrimitiveType;
+import de.uka.ilkd.key.java.expression.Operator;
+import de.uka.ilkd.key.java.reference.ExecutionContext;
+import de.uka.ilkd.key.java.visitor.Visitor;
+
+import org.key_project.util.ExtList;
+
+public class MSetCard extends Operator {
+
+    public MSetCard(ExtList children) {
+        super(children);
+    }
+
+
+    @Override
+    public int getPrecedence() {
+        return 0;
+    }
+
+    @Override
+    public void visit(Visitor v) {
+        v.performActionOnMSetCard(this);
+    }
+
+
+    @Override
+    public int getArity() {
+        return 1;
+    }
+
+
+    @Override
+    public KeYJavaType getKeYJavaType(Services javaServ, ExecutionContext ec) {
+        return javaServ.getJavaInfo().getKeYJavaType(PrimitiveType.JAVA_INT);
+    }
+
+
+    @Override
+    public int getNotation() {
+        return Operator.PREFIX;
+    }
+}

key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/mset/MSetDiff.java

@@ -0,0 +1,37 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package de.uka.ilkd.key.java.expression.operator.mset;
+
+import de.uka.ilkd.key.java.Expression;
+import de.uka.ilkd.key.java.expression.operator.BinaryOperator;
+import de.uka.ilkd.key.java.visitor.Visitor;
+
+import org.key_project.util.ExtList;
+
+public class MSetDiff extends BinaryOperator {
+    public MSetDiff(ExtList children) {
+        super(children);
+    }
+
+    public MSetDiff(Expression msetA, Expression msetB) {
+        super(msetA, msetB);
+    }
+
+
+
+    @Override
+    public void visit(Visitor v) {
+        v.performActionOnMSetDiff(this);
+    }
+
+    @Override
+    public int getPrecedence() {
+        return 0;
+    }
+
+    @Override
+    public int getNotation() {
+        return PREFIX;
+    }
+}

key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/mset/MSetIntersect.java

@@ -0,0 +1,39 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package de.uka.ilkd.key.java.expression.operator.mset;
+
+import de.uka.ilkd.key.java.Expression;
+import de.uka.ilkd.key.java.expression.operator.BinaryOperator;
+import de.uka.ilkd.key.java.visitor.Visitor;
+
+import org.key_project.util.ExtList;
+
+public class MSetIntersect extends BinaryOperator {
+
+
+    public MSetIntersect(ExtList children) {
+        super(children);
+    }
+
+    public MSetIntersect(Expression msetA, Expression msetB) {
+        super(msetA, msetB);
+    }
+
+
+
+    @Override
+    public void visit(Visitor v) {
+        v.performActionOnMSetIntersect(this);
+    }
+
+    @Override
+    public int getPrecedence() {
+        return 0;
+    }
+
+    @Override
+    public int getNotation() {
+        return PREFIX;
+    }
+}

key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/mset/MSetMul.java

@@ -0,0 +1,49 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package de.uka.ilkd.key.java.expression.operator.mset;
+
+import de.uka.ilkd.key.java.Services;
+import de.uka.ilkd.key.java.abstraction.KeYJavaType;
+import de.uka.ilkd.key.java.abstraction.PrimitiveType;
+import de.uka.ilkd.key.java.expression.Operator;
+import de.uka.ilkd.key.java.reference.ExecutionContext;
+import de.uka.ilkd.key.java.visitor.Visitor;
+
+import org.key_project.util.ExtList;
+
+public class MSetMul extends Operator {
+
+    public MSetMul(ExtList children) {
+        super(children);
+    }
+
+
+    @Override
+    public int getPrecedence() {
+        return 0;
+    }
+
+    @Override
+    public void visit(Visitor v) {
+        v.performActionOnMSetMul(this);
+    }
+
+    @Override
+    public int getArity() {
+        return 1;
+    }
+
+
+    @Override
+    public KeYJavaType getKeYJavaType(Services javaServ, ExecutionContext ec) {
+        return javaServ.getJavaInfo().getKeYJavaType(PrimitiveType.JAVA_INT);
+    }
+
+
+    @Override
+    public int getNotation() {
+        return Operator.PREFIX;
+    }
+
+}

key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/mset/MSetSingle.java

@@ -0,0 +1,43 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package de.uka.ilkd.key.java.expression.operator.mset;
+
+import de.uka.ilkd.key.java.Expression;
+import de.uka.ilkd.key.java.Services;
+import de.uka.ilkd.key.java.abstraction.KeYJavaType;
+import de.uka.ilkd.key.java.abstraction.PrimitiveType;
+import de.uka.ilkd.key.java.expression.Operator;
+import de.uka.ilkd.key.java.reference.ExecutionContext;
+import de.uka.ilkd.key.java.visitor.Visitor;
+
+import org.key_project.util.ExtList;
+
+public class MSetSingle extends Operator {
+
+    public MSetSingle(ExtList children) { super(children); }
+
+    public MSetSingle(Expression child) { super(child); }
+
+    public int getPrecedence() {
+        return 0;
+    }
+
+
+    public int getNotation() {
+        return PREFIX;
+    }
+
+
+    public void visit(Visitor v) {
+        v.performActionOnMSetSingle(this);
+    }
+
+    public int getArity() {
+        return 1;
+    }
+
+    public KeYJavaType getKeYJavaType(Services javaServ, ExecutionContext ec) {
+        return javaServ.getJavaInfo().getKeYJavaType(PrimitiveType.JAVA_MSET);
+    }
+}