Equivalence in patterns

matcher/src/main/antlr4/edu/kit/formal/psdb/termmatcher/MatchPattern.g4

@@ -26,13 +26,12 @@ termPattern :
     | <assoc=right> termPattern op=(DIV|MOD) termPattern        #divMod
     | termPattern op=(PLUS|MINUS) termPattern                   #plusMinus
     | termPattern op=(LE|GE|LEQ|GEQ) termPattern                #comparison
-    | termPattern op=(NEQ|EQ) termPattern                 #equality
+    | termPattern op=(NEQ|EQ) termPattern                       #equality
     | termPattern AND termPattern                               #and
     | termPattern OR termPattern                                #or
     | termPattern IMP termPattern                               #impl
     | termPattern XOR termPattern                               #xor
-   // | termPattern EQUIV termPattern                             #equivalence
-    //|   termPattern EQUIV termPattern already covered by EQ/NEQ
+    | termPattern EQUIV termPattern                             #equivalence
     | MINUS termPattern                                         #exprNegate
     | NOT termPattern                                           #exprNot
     | '(' termPattern ')' bindClause?                                      #exprParen

matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/MatchPatternDualVisitor.java

@@ -85,6 +85,7 @@ public abstract class MatchPatternDualVisitor<T, S> extends MatchPatternBaseVisi
         return visitPlusMinus(ctx, stack.peek());
     }
 
+
     protected abstract T visitPlusMinus(MatchPatternParser.PlusMinusContext ctx, S peek);
 
     @Override
@@ -164,6 +165,13 @@ public abstract class MatchPatternDualVisitor<T, S> extends MatchPatternBaseVisi
     }
 
     protected abstract T visitEquality(MatchPatternParser.EqualityContext ctx, S peek);
+
+    @Override
+    public T visitEquivalence(MatchPatternParser.EquivalenceContext ctx) {
+        return visitEquivalence(ctx, stack.peek());
+    }
+
+    protected abstract T visitEquivalence(MatchPatternParser.EquivalenceContext ctx, S peek);
 }
     
 

matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/MatcherImpl.java

@@ -7,6 +7,7 @@ import de.uka.ilkd.key.logic.Term;
 import edu.kit.formal.psdb.termmatcher.MatchPatternLexer;
 import edu.kit.formal.psdb.termmatcher.MatchPatternParser;
 import edu.kit.iti.formal.psdbg.termmatcher.mp.MatchPath;
+import static edu.kit.iti.formal.psdbg.termmatcher.mp.MatchPathFacade.*;
 import lombok.Getter;
 import lombok.Setter;
 import org.antlr.v4.runtime.CommonToken;
@@ -17,8 +18,6 @@ import java.util.stream.Collectors;
 import java.util.stream.IntStream;
 import java.util.stream.Stream;
 
-import static edu.kit.iti.formal.psdbg.termmatcher.mp.MatchPathFacade.*;
-
 /**
  * Matchpattern visitor visits the matchpatterns of case-statements
  *
@@ -520,6 +519,11 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, MatchPath> {
         return visitBinaryOperation("equals", ctx.termPattern(0), ctx.termPattern(1), peek);
     }
 
+    @Override
+    protected Matchings visitEquivalence(MatchPatternParser.EquivalenceContext ctx, MatchPath peek) {
+        return visitBinaryOperation("equiv", ctx.termPattern(0), ctx.termPattern(1), peek);
+    }
+
     private Stream<MatchPath.MPTerm> subTerms(MatchPath.MPTerm peek) {
         ArrayList<MatchPath.MPTerm> list = new ArrayList<>();
         subTerms(list, peek);

rt-key/src/test/resources/edu/kit/iti/formal/psdbg/interpreter/contraposition/cutTest.kps

 script cutTest(){
-  cases{
+  cut `p <->q`;
+  //cases{
     //X:TERM :=`p`;
-    case match `==>?X -> ?Y`:
-        cut `?X`[?X \ Y];
+   // case match `==>?X -> ?Y`:
+   //     cut `?X`[?X \ Y];
 
-  }
+  //}
 }
\ No newline at end of file