Activate the OverloadedOperatorHandler.java for Sequence datatype (#3398

)
KeYProject · Feb 20, 2024 · 1fb0c10 · 1fb0c10
2 parents b34b3cf + 83f0581
commit 1fb0c10
Show file tree

Hide file tree

Showing 2 changed files with 47 additions and 7 deletions.
diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/OverloadedOperatorHandler.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/OverloadedOperatorHandler.java
@@ -99,8 +99,8 @@ public OverloadedOperatorHandler(Services services, SpecMathMode specMathMode) {
         this.integerHandler = new IntegerHandler(services, specMathMode);
 
         handlers.add(new BinaryBooleanHandler(services));
-        // handlers.add(new SequenceHandler(services));
-        // handlers.add(new LocSetHandler(services));
+        handlers.add(new SequenceHandler(services));
+        handlers.add(new LocSetHandler(services));
         handlers.add(this.integerHandler);
         handlers.add(new FloatHandler(services));
         handlers.add(new DoubleHandler(services));
@@ -150,6 +150,9 @@ public SequenceHandler(Services services) {
         @Override
         public SLExpression build(JMLOperator op, SLExpression left, SLExpression right)
                 throws SLTranslationException {
+            if (right == null) {
+                return null;
+            }
             if (left.getTerm().sort() == ldtSequence.targetSort()
                     && right.getTerm().sort() == ldtSequence.targetSort()) {
                 if (op == JMLOperator.ADD) {
@@ -173,17 +176,20 @@ public LocSetHandler(Services services) {
         @Override
         public SLExpression build(JMLOperator op, SLExpression left, SLExpression right)
                 throws SLTranslationException {
+            if (right == null) {
+                return null;
+            }
             final var l = left.getTerm();
             final var r = right.getTerm();
             if (l.sort() == ldt.targetSort() && r.sort() == ldt.targetSort()) {
                 return switch (op) {
                 case ADD, BITWISE_OR -> new SLExpression(tb.union(l, r));
                 case SUBTRACT -> new SLExpression(tb.setMinus(l, r));
-                case BITWISE_AND -> new SLExpression(tb.intersect(l, r));
-                case LT -> new SLExpression(tb.subset(l, r));
-                case LTE -> new SLExpression(tb.and(tb.subset(l, r), tb.equals(l, r)));
-                case GT -> new SLExpression(tb.subset(r, l));
-                case GTE -> new SLExpression(tb.and(tb.subset(r, l), tb.equals(l, r)));
+                case MULT, BITWISE_AND -> new SLExpression(tb.intersect(l, r));
+                case LT -> new SLExpression(tb.and(tb.subset(l, r), tb.not(tb.equals(l, r))));
+                case LTE -> new SLExpression(tb.subset(l, r));
+                case GT -> new SLExpression(tb.and(tb.subset(r, l), tb.not(tb.equals(l, r))));
+                case GTE -> new SLExpression(tb.subset(r, l));
                 default -> null;
                 };
             }

diff --git a/key.core/src/test/java/de/uka/ilkd/key/speclang/jml/TestJMLTranslator.java b/key.core/src/test/java/de/uka/ilkd/key/speclang/jml/TestJMLTranslator.java
@@ -25,6 +25,8 @@
 import org.junit.jupiter.api.Assertions;
 import org.junit.jupiter.api.BeforeEach;
 import org.junit.jupiter.api.Test;
+import org.junit.jupiter.params.ParameterizedTest;
+import org.junit.jupiter.params.provider.CsvSource;
 
 import static java.lang.String.format;
 import static org.junit.jupiter.api.Assertions.*;
@@ -444,4 +446,36 @@ public void testCorrectImplicitThisResolution() {
             ProofSaver.printTerm(expected, services), ProofSaver.printTerm(result, services)));
     }
 
+    @ParameterizedTest
+    @CsvSource(value = {
+        "\\seq(1) + \\seq(2,3) : \\seq_concat(\\seq(1), \\seq(2,3))",
+        "\\locset(this.b) + \\locset(this.s) : \\set_union(\\locset(this.b), \\locset(this.s))",
+        "\\locset(this.b) | \\locset(this.s) : \\set_union(\\locset(this.b), \\locset(this.s))",
+        "\\locset(this.b) & \\locset(this.s) : \\intersect(\\locset(this.b), \\locset(this.s))",
+        "\\locset(this.b) * \\locset(this.s) : \\intersect(\\locset(this.b), \\locset(this.s))",
+        "\\locset(this.b) <= \\locset(this.s) : \\subset(\\locset(this.b), \\locset(this.s))",
+        "\\locset(this.b) < \\locset(this.s) : \\subset(\\locset(this.b), \\locset(this.s)) && \\locset(this.b) != \\locset(this.s)",
+        "\\locset(this.b) >= \\locset(this.s) : \\subset(\\locset(this.s), \\locset(this.b))",
+        "\\locset(this.b) > \\locset(this.s) : \\subset(\\locset(this.s), \\locset(this.b)) && \\locset(this.b) != \\locset(this.s)",
+    }, delimiter = ':')
+    public void testOperatorOverloading(String expression, String expected) {
+        Term tTrans = null, tExp = null;
+        try {
+            tTrans = jmlIO.parseExpression(expression);
+        } catch (Exception e) {
+            fail("Cannot parse " + expression, e);
+        }
+
+        try {
+            tExp = jmlIO.parseExpression(expected);
+        } catch (Exception e) {
+            fail("Cannot parse " + expected, e);
+        }
+
+        if (!tTrans.equalsModTermLabels(tExp)) {
+            // this gives nicer error
+            assertEquals(tExp, tTrans);
+        }
+    }
+
 }