Bugfix for emptyMatch on sequent

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

@@ -14,15 +14,36 @@ f(..., ...?X...)
 f(..., ... g(x) ...)
 f(_, x, _, y, ... y ...)
 */
+
+sequentPattern : antec=semiSeqPattern? ARROW succ=semiSeqPattern? | anywhere=semiSeqPattern;
+
 semiSeqPattern : termPattern (',' termPattern)*;
-sequentPattern : antec=semiSeqPattern? ARROW succ=semiSeqPattern?;
+
 termPattern :
 	   DONTCARE      #dontCare
 	 //| STARDONTCARE  #starDontCare
 	 | SID           #schemaVar
 	 | STARDONTCARE termPattern STARDONTCARE #anywhere
+	 | DIGITS #number
 	 | func=ID ( '(' termPattern (',' termPattern)* ')')? #function
+	 | left=termPattern op=(PLUS|MINUS|MUL|LE|GE|LEQ|GEQ|NEQ|EQ| AND|OR|IMP) right=termPattern #binaryOperation
 	 ;
+
+	 /*
+	       expression MUL expression #exprMultiplication
+         | <assoc=right> expression DIV expression #exprDivision
+         | expression op=(PLUS|MINUS) expression #exprLineOperators
+         | expression op=(LE|GE|LEQ|GEQ) expression #exprComparison
+         | expression op=(NEQ|EQ) expression  #exprEquality
+         | expression AND expression   #exprAnd
+         | expression OR expression    #exprOr
+         | expression IMP expression   #exprIMP
+         //|   expression EQUIV expression already covered by EQ/NEQ
+         | expression LBRACKET substExpressionList RBRACKET #exprSubst
+         | MINUS expression   #exprNegate
+         | NOT expression  #exprNot
+         | '(' expression ')' #exprParen
+	 */
 /*
 f(x), f(x,y,g(y)), X, ?Y, _, ..., f(... ?X ...), f(..., ?X), f(..., ...?X...), f(..., ... g(x) ...), f(_, x, _, y, ... y ...)
 */
@@ -49,6 +70,7 @@ GE : '>' ;
 LE : '<' ;
 AND : '&' ;
 OR: '|' ;
+IMP: '->';
 
 COMMENT: '//' ~[\n\r]* -> channel(HIDDEN);
 WS: [\n\f\r\t ] -> channel(HIDDEN);
\ No newline at end of file

src/main/java/edu/kit/formal/psdb/termmatcher/MatchPatternDualVisitor.java

@@ -12,6 +12,23 @@ public abstract class MatchPatternDualVisitor<T, S> extends MatchPatternBaseVisi
         return t;
     }
 
+    @Override
+    public final T visitSequentPattern(MatchPatternParser.SequentPatternContext ctx) {
+        return visitSequentPattern(ctx, stack.peek());
+    }
+
+    @Override
+    public final T visitSemiSeqPattern(MatchPatternParser.SemiSeqPatternContext ctx) {
+        return visitSemiSeqPattern(ctx, stack.peek());
+    }
+
+    protected abstract T visitSemiSeqPattern(MatchPatternParser.SemiSeqPatternContext ctx, S peek);
+
+    @Override
+    public T visitNumber(MatchPatternParser.NumberContext ctx) {
+        return visitNumber(ctx, stack.peek());
+    }
+
     @Override
     public final T visitDontCare(MatchPatternParser.DontCareContext ctx) {
         return visitDontCare(ctx, stack.peek());
@@ -33,31 +50,28 @@ public abstract class MatchPatternDualVisitor<T, S> extends MatchPatternBaseVisi
 
     protected abstract T visitSchemaVar(MatchPatternParser.SchemaVarContext ctx, S peek);
 
-    @Override
-    public final T visitAnywhere(MatchPatternParser.AnywhereContext ctx) {
-        return visitAnywhere(ctx, stack.peek());
-    }
-
-    protected abstract T visitAnywhere(MatchPatternParser.AnywhereContext ctx, S peek);
-
     @Override
     public final T visitFunction(MatchPatternParser.FunctionContext ctx) {
         return visitFunction(ctx, stack.peek());
     }
 
-    protected abstract T visitFunction(MatchPatternParser.FunctionContext ctx, S peek);
-
     @Override
-    public final T visitSemiSeqPattern(MatchPatternParser.SemiSeqPatternContext ctx) {
-        return visitSemiSeqPattern(ctx, stack.peek());
+    public T visitBinaryOperation(MatchPatternParser.BinaryOperationContext ctx) {
+        return visitBinaryOperation(ctx, stack.peek());
     }
 
-    protected abstract T visitSemiSeqPattern(MatchPatternParser.SemiSeqPatternContext ctx, S peek);
-
     @Override
-    public final T visitSequentPattern(MatchPatternParser.SequentPatternContext ctx) {
-        return visitSequentPattern(ctx, stack.peek());
+    public final T visitAnywhere(MatchPatternParser.AnywhereContext ctx) {
+        return visitAnywhere(ctx, stack.peek());
     }
 
+    protected abstract T visitAnywhere(MatchPatternParser.AnywhereContext ctx, S peek);
+
+    protected abstract T visitBinaryOperation(MatchPatternParser.BinaryOperationContext ctx, S peek);
+
+    protected abstract T visitFunction(MatchPatternParser.FunctionContext ctx, S peek);
+
+    protected abstract T visitNumber(MatchPatternParser.NumberContext ctx, S peek);
+
     protected abstract T visitSequentPattern(MatchPatternParser.SequentPatternContext ctx, S peek);
 }

src/main/java/edu/kit/formal/psdb/termmatcher/MatcherFacade.java

@@ -18,8 +18,7 @@ import java.util.stream.Collectors;
 
 import static edu.kit.formal.psdb.termmatcher.MatchPatternParser.SequentPatternContext;
 import static edu.kit.formal.psdb.termmatcher.MatchPatternParser.TermPatternContext;
-import static edu.kit.formal.psdb.termmatcher.MatcherImpl.MatchInfo;
-import static edu.kit.formal.psdb.termmatcher.MatcherImpl.NO_MATCH;
+import static edu.kit.formal.psdb.termmatcher.MatcherImpl.*;
 
 /**
  * A facade for capturing everthing we want to do with matchers.
@@ -101,7 +100,7 @@ public class MatcherFacade {
     //BiMap<Pair<SequentFormula, MatchPatternParser.TermPatternContext>, Matchings> formulaToMatchingInfo,
 
     /**
-     * Reduce all matches to only comaptible matchings
+     * Reduce all matches to only compatible matchings
      * @param allMatches
      * @return
      */
@@ -132,20 +131,60 @@ public class MatcherFacade {
      */
     public static Matchings matches(String pattern, Sequent sequent) {
         MatcherImpl matcher = new MatcherImpl();
+
         MatchPatternParser mpp = getParser(pattern);
+
         SequentPatternContext ctx = mpp.sequentPattern();
 
         Semisequent antec = sequent.antecedent();
         Semisequent succ = sequent.succedent();
 
-        SemiSeqPatternContext antecPattern = ctx.antec;
-        SemiSeqPatternContext succPattern = ctx.succ;
+        Matchings newMatching;
+
+        if (ctx.anywhere != null) {
+            //in this case we have a pattern without "==>"
+            SemiSeqPatternContext patternCtx = ctx.anywhere;
+
+            if (antec.isEmpty() & succ.isEmpty()) {
+                //Sonderbehandlung, falls beide EmptyMatch-> kein thema aber ansonsten bevorzugung von Varzuweisungen
+                Matchings antecMatches = matches(patternCtx, antec);
+                Matchings succMatches = matches(patternCtx, succ);
+                Matchings ret = compareMatchings(antecMatches, succMatches);
+                newMatching = ret;
+            } else {
+                if (antec.isEmpty()) {
+                    newMatching = matches(patternCtx, succ);
+                } else {
+                    newMatching = matches(patternCtx, antec);
+                }
 
-        Matchings mAntec = antecPattern == null ? MatcherImpl.EMPTY_MATCH : matches(antecPattern, antec);
-        Matchings mSucc = succPattern == null ? MatcherImpl.EMPTY_MATCH : matches(succPattern, succ);
+            }
+        } else {
+
+            SemiSeqPatternContext antecPattern = ctx.antec;
+            SemiSeqPatternContext succPattern = ctx.succ;
 
-        Matchings newMatching = MatcherImpl.reduceConform(mAntec, mSucc);
+            Matchings mAntec = antecPattern == null ? MatcherImpl.EMPTY_MATCH : matches(antecPattern, antec);
+            Matchings mSucc = succPattern == null ? MatcherImpl.EMPTY_MATCH : matches(succPattern, succ);
 
+            newMatching = MatcherImpl.reduceConform(mAntec, mSucc);
+        }
         return newMatching;
     }
+
+    private static Matchings compareMatchings(Matchings antecMatches, Matchings succMatches) {
+        if (antecMatches.equals(EMPTY_MATCH) && succMatches.equals(EMPTY_MATCH)) {
+            return MatcherImpl.EMPTY_MATCH;
+        }
+        if (antecMatches.equals(NO_MATCH)) return succMatches;
+        if (succMatches.equals(NO_MATCH)) return antecMatches;
+
+
+        //bevorzuge antecmatch atm
+        if (!antecMatches.equals(EMPTY_MATCH)) {
+            return antecMatches;
+        } else {
+            return succMatches;
+        }
+    }
 }

src/main/java/edu/kit/formal/psdb/termmatcher/MatcherImpl.java

@@ -2,6 +2,7 @@ package edu.kit.formal.psdb.termmatcher;
 
 import de.uka.ilkd.key.logic.SequentFormula;
 import de.uka.ilkd.key.logic.Term;
+import org.antlr.v4.runtime.Token;
 
 import java.util.*;
 import java.util.stream.IntStream;
@@ -31,6 +32,7 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, Term> {
                 if (!intersection.isEmpty()) continue;
 
                 HashMap<String, Term> h3 = reduceConform(minfo1.matching, minfo2.matching);
+
                 if (h3 != null) {
                     Set<SequentFormula> union = new HashSet<>(minfo1.matchedForms);
                     union.addAll(minfo2.matchedForms);
@@ -45,51 +47,15 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, Term> {
     private static HashMap<String, Term> reduceConform(HashMap<String, Term> h1, HashMap<String, Term> h2) {
         HashMap<String, Term> h3 = new HashMap<>(h1);
         for (String s1 : h3.keySet()) {
-            if (h2.containsKey(s1) && !h2.get(s1).equals(h1.get(s1))) {
+            if (!s1.equals("EMPTY_MATCH") && (h2.containsKey(s1) && !h2.get(s1).equals(h1.get(s1)))) {
                 return null;
             }
         }
+
         h3.putAll(h2);
         return h3;
     }
 
-    /**
-     * Reduce the matchings by eliminating non-compatible matchings.
-     * For example:
-     * m1: <X, f(y)>, <Y,g> and m2: <X, g> <Y, f(x)>
-     * @param m1
-     * @param m2
-     * @return
-     */
-    protected static Matchings reduceConform(Matchings m1, Matchings m2) {
-        //shortcuts
-        if (m1 == NO_MATCH || m2 == NO_MATCH) return NO_MATCH;
-        if (m1 == EMPTY_MATCH) return m2;
-        if (m2 == EMPTY_MATCH) return m1;
-
-        Matchings m3 = new Matchings();
-        boolean oneMatch = false;
-        for (HashMap<String, Term> h1 : m1) {
-            for (HashMap<String, Term> h2 : m2) {
-                HashMap<String, Term> h3 = reduceConform(h1, h2);
-                if (h3 != null) {
-                    m3.add(h3);
-                    oneMatch = true;
-                }
-            }
-        }
-        return oneMatch ? m3 : NO_MATCH;
-    }
-
-    /*@Override
-    protected Matchings visitStartDontCare(MatchPatternParser.StarDontCareContext ctx, Term peek) {
-        if (peek != null) {
-            return EMPTY_MATCH;
-        } else {
-            return NO_MATCH;
-        }
-    }*/
-
     /**
      * Visit '_'
      *
@@ -106,6 +72,15 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, Term> {
         }
     }
 
+    /*@Override
+    protected Matchings visitStartDontCare(MatchPatternParser.StarDontCareContext ctx, Term peek) {
+        if (peek != null) {
+            return EMPTY_MATCH;
+        } else {
+            return NO_MATCH;
+        }
+    }*/
+
     /**
      * Visit a Schema Variable
      *
@@ -138,6 +113,112 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, Term> {
         return m;
     }
 
+    @Override
+    protected Matchings visitBinaryOperation(MatchPatternParser.BinaryOperationContext ctx, Term peek) {
+        Token op = ctx.op;
+        String opToKeYName = convert(op.getType());
+
+        MatchPatternParser.TermPatternContext left = ctx.left;
+        MatchPatternParser.TermPatternContext right = ctx.right;
+
+        if (peek.op().name().toString().equals(opToKeYName)  // same name
+                && peek.arity() == 2   // we know that we are in binary term
+                ) {
+            Matchings lM = accept(left, peek.sub(0));
+            Matchings rM = accept(right, peek.sub(1));
+            Matchings ret = reduceConform(lM, rM);
+            return ret;
+            /*return IntStream.range(0, peek.arity())
+                    .mapToObj(i -> (Matchings) accept(ctx.termPattern(i), peek.sub(i)))
+                    .reduce(MatcherImpl::reduceConform)
+                    .orElse(NO_MATCH);*/
+        }
+        return NO_MATCH;
+
+
+    }
+
+    private String convert(int op) {
+
+        switch (op) {
+
+            case MatchPatternParser.PLUS:
+                return "add";
+
+            case MatchPatternParser.MINUS:
+                return "sub";
+
+            case MatchPatternParser.MUL:
+                return "mul";
+
+
+            case MatchPatternParser.DIV:
+                return "div";
+
+
+            case MatchPatternParser.LE:
+                return "lt";
+
+
+            case MatchPatternParser.LEQ:
+                return "leq";
+
+
+            case MatchPatternParser.EQ:
+                return "equals";
+
+            case MatchPatternParser.GE:
+                return "gt";
+
+            case MatchPatternParser.GEQ:
+                return "geq";
+
+            case MatchPatternParser.IMP:
+                return "imp";
+
+
+            case MatchPatternParser.AND:
+                return "and";
+
+            case MatchPatternParser.OR:
+                return "or";
+
+            default:
+                throw new UnsupportedOperationException("The operator " + op + "is not known");
+        }
+
+
+    }
+
+    /**
+     * Reduce the matchings by eliminating non-compatible matchings.
+     * For example:
+     * m1: <X, f(y)>, <Y,g> and m2: <X, g> <Y, f(x)>
+     *
+     * @param m1
+     * @param m2
+     * @return
+     */
+    protected static Matchings reduceConform(Matchings m1, Matchings m2) {
+        //shortcuts
+        if (m1 == NO_MATCH || m2 == NO_MATCH) return NO_MATCH;
+        if (m1 == EMPTY_MATCH) return m2;
+        if (m2 == EMPTY_MATCH) return m1;
+
+        Matchings m3 = new Matchings();
+        boolean oneMatch = false;
+        for (HashMap<String, Term> h1 : m1) {
+            for (HashMap<String, Term> h2 : m2) {
+                HashMap<String, Term> h3 = reduceConform(h1, h2);
+                if (h3 != null) {
+                    m3.add(h3);
+                    oneMatch = true;
+                }
+            }
+        }
+        return oneMatch ? m3 : NO_MATCH;
+    }
+
     /**
      * Visit a function and predicate symbol without a sequent arrow
      * @param ctx
@@ -153,7 +234,7 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, Term> {
             return IntStream.range(0, peek.arity())
                     .mapToObj(i -> (Matchings) accept(ctx.termPattern(i), peek.sub(i)))
                     .reduce(MatcherImpl::reduceConform)
-                    .orElse(NO_MATCH);
+                    .orElse(EMPTY_MATCH);
         }
         return NO_MATCH;
     }
@@ -169,6 +250,11 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, Term> {
         return null;
     }
 
+    @Override
+    protected Matchings visitNumber(MatchPatternParser.NumberContext ctx, Term peek) {
+        return null;
+    }
+
     /**
      * Visit a sequent pattern 'f(x) ==> f(x)', 'f(x) ==>' or '==> f(x)'
      * @param ctx

src/test/java/edu/kit/formal/psdb/termmatcher/MatcherFacadeTest.java

@@ -44,6 +44,10 @@ public class MatcherFacadeTest {
         shouldMatchForm("pred(a)", "...?X...", "[{?X=pred(a)}, {?X=a}]");
         shouldMatchForm("pred(f(a))", "pred(...?X...)", "[{?X=f(a)}, {?X=a}]");
         shouldMatch("i+j", "add(?X,?Y)", "[{?X=i, ?Y=j}]");
+        shouldMatch("i+j", "?X+?Y", "[{?X=i, ?Y=j}]");
+        shouldMatchForm("p & q", "p & ?X", "[{?X=q}]");
+        //shouldMatchForm("p & q", "?X & q", "[{?X=p}]");
+        //shouldMatch("1*j", "add(1,?Y)", "[{?Y=j}]");
 
 
         //shouldMatch("f(a) ==> f(a), f(b)" , "==> f(?X)", [{?X=a}]);
@@ -119,13 +123,14 @@ public class MatcherFacadeTest {
         shouldMatchSemiSeq("pred(a), pred(b) ==>", "pred(?X), pred(?X)", "[]");
         shouldMatchSemiSeq("pred(a), pred(f(a)) ==>", "pred(?X), pred(f(?X))", "[{?X=a}]");
         shouldMatchSemiSeq("pred(b), pred(f(a)) ==>", "pred(?X), pred(f(?X))", "[]");
-        shouldMatchSemiSeq("pred(a), pred(b) ==> qpred(a,b)", "pred(a), pred(b)");
+        shouldMatchSemiSeq("pred(a), pred(b) ==>", "pred(a), pred(b)", "[{EMPTY_MATCH=null}]");
+        shouldMatchSemiSeq("pred(a), pred(b) ==> qpred(a,b)", "pred(a), pred(b) ==> ", "[{EMPTY_MATCH=null}]");
         shouldMatchSemiSeq("pred(a), pred(b) ==> qpred(a,b)", "pred(?X), pred(?Y)", "[{?X=a, ?Y=b}, {?X=b, ?Y=a}]");
 
         shouldMatchSemiSeq("pred(b), pred(a) ==>", "pred(...?X...), pred(f(?X))", "[]");
         shouldMatchSemiSeq("pred(b), pred(a) ==>", "pred(...?X...), pred(...?Y...)", "[{?X=b, ?Y=a}, {?X=a, ?Y=b}]");
 
-        shouldMatchSemiSeq("intPred(fint(i+j))", "intPred(...add(?X, ?y)...)");
+        shouldMatchSemiSeq("intPred(fint(i+j)) ==>", "intPred(...add(?X, ?y)...)");
 
     }