Merge remote-tracking branch 'origin/master'

# Conflicts:
#	ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java
#	ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/InteractiveModeController.java

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

@@ -22,7 +22,8 @@ sequentPattern : antec=semiSeqPattern? ARROW succ=semiSeqPattern? #sequentArrow
 semiSeqPattern : termPattern (',' termPattern)*;
 
 termPattern :
-      termPattern MUL termPattern                               #mult
+   '(' quantifier=(EXISTS|FORALL) boundVars+=(SID|ID|DONTCARE)+  skope=termPattern ')' bindClause?  #quantForm
+    |  termPattern MUL termPattern                              #mult
     | <assoc=right> termPattern op=(DIV|MOD) termPattern        #divMod
     | termPattern op=(PLUS|MINUS) termPattern                   #plusMinus
     | termPattern op=(LE|GE|LEQ|GEQ) termPattern                #comparison
@@ -53,12 +54,6 @@ bindClause : ('\\as' | ':') SID;
 DONTCARE: '?' | '_' | '█';
 DIGITS : DIGIT+ ;
 fragment DIGIT : [0-9] ;
-SID: '?' [_a-zA-Z0-9\\]+ ;
-ID : [a-zA-Z\\_] ([_a-zA-Z0-9\\])*
-   | 'update-application'
-   | 'parallel-upd'
-   | 'elem-update'
-   ;
 
 ARROW : '⇒' | '==>';
 STARDONTCARE: '...' | '…';
@@ -78,8 +73,16 @@ OR: '|' ;
 IMP: '->';
 MOD:'%';
 XOR:'^';
-FORALL: '\forall' | '∀';
-EXISTS: '\exists';
+NOT :'!';
+FORALL: '\\forall' | '∀';
+EXISTS: '\\exists';
+SID: '?' [_a-zA-Z0-9\\]+ ;
+ID : [a-zA-Z\\_] ([_a-zA-Z0-9\\])*
+   | 'update-application'
+   | 'parallel-upd'
+   | 'elem-update'
+   ;
+
 
 COMMENT: '//' ~[\n\r]* -> channel(HIDDEN);
 WS: [\n\f\r\t ] -> channel(HIDDEN);

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

@@ -31,6 +31,13 @@ public abstract class MatchPatternDualVisitor<T, S> extends MatchPatternBaseVisi
 
     public abstract T visitSequentArrow(MatchPatternParser.SequentArrowContext ctx, S peek);
 
+    @Override
+    public T visitQuantForm(MatchPatternParser.QuantFormContext ctx) {
+        return visitQuantForm(ctx, stack.peek());
+    }
+
+    public abstract T visitQuantForm(MatchPatternParser.QuantFormContext ctx, S peek);
+
     @Override
     public final T visitSemiSeqPattern(MatchPatternParser.SemiSeqPatternContext ctx) {
         return visitSemiSeqPattern(ctx, stack.peek());

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

@@ -4,12 +4,15 @@ import com.google.common.collect.Sets;
 import de.uka.ilkd.key.logic.Semisequent;
 import de.uka.ilkd.key.logic.SequentFormula;
 import de.uka.ilkd.key.logic.Term;
+import de.uka.ilkd.key.logic.op.QuantifiableVariable;
 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;
+import org.antlr.v4.runtime.Token;
 import org.key_project.util.collection.ImmutableArray;
 
 import java.util.*;
@@ -17,8 +20,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
  *
@@ -250,6 +251,7 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, MatchPath> {
         return this.reduceConform(m, mNew);
     }
 
+
     @Override
     protected Matchings visitNumber(MatchPatternParser.NumberContext ctx, MatchPath path) {
         //we are at a number
@@ -417,7 +419,7 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, MatchPath> {
     }
 
     protected Matchings visitBinaryOperation(String keyOpName, MatchPatternParser.TermPatternContext right, MatchPatternParser.TermPatternContext left, MatchPath peek) {
-        //create new functioncontext object and set fields accodringsly
+        //create new functioncontext object and set fields accordingly
         OwnFunctionContext func = new OwnFunctionContext(left);
         //MatchPatternParser.FunctionContext func = new MatchPatternParser.FunctionContext(left);
         //func.func = new CommonToken(MatchPatternLexer.ID, keyOpName);
@@ -430,6 +432,68 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, MatchPath> {
         return accept(func, peek);
     }
 
+    @Override
+    public Matchings visitQuantForm(MatchPatternParser.QuantFormContext ctx, MatchPath peek) {
+        Term toMatch = (Term) peek.getUnit();
+        if (!toMatch.op().toString().equals(convert(ctx.quantifier.getType()))) {
+            return NO_MATCH;
+        }
+        if (toMatch.boundVars().size() != ctx.boundVars.size()) {
+            return NO_MATCH;
+        }
+
+        Matchings match = EMPTY_MATCH;
+
+        for (int i = 0; i < ctx.boundVars.size(); i++) {
+            Token qfPattern = ctx.boundVars.get(i);
+            QuantifiableVariable qv = toMatch.boundVars().get(i);
+
+            if (qfPattern.getType() == MatchPatternLexer.DONTCARE) {
+                match = reduceConform(match, Matchings.singleton(qfPattern.getText(), new MatchPath.MPQuantifiableVarible(peek, qv, i)));
+                continue;
+            }
+            if (qfPattern.getType() == MatchPatternLexer.SID) {
+                match = reduceConform(match, Matchings.singleton(qfPattern.getText(), new MatchPath.MPQuantifiableVarible(peek, qv, i)));
+            } else {
+                if (!qv.name().toString().equals(qfPattern.getText())) {
+                    return NO_MATCH;
+                }
+                match = reduceConform(match, EMPTY_MATCH);
+            }
+        }
+
+
+        Matchings fromTerm = accept(ctx.skope, create(peek, 0));
+        //return handleBindClause(ctx.bindClause(), path, m);
+        Matchings retM = reduceConformQuant(fromTerm, match);
+        return handleBindClause(ctx.bindClause(), peek, retM);
+    }
+
+    @Override
+    protected Matchings visitMult(MatchPatternParser.MultContext ctx, MatchPath peek) {
+        return visitBinaryOperation("mul", ctx.termPattern(0), ctx.termPattern(1), peek);
+    }
+
+    @Override
+    protected Matchings visitComparison(MatchPatternParser.ComparisonContext ctx, MatchPath peek) {
+        return visitBinaryOperation(convert(ctx.op.getType()), ctx.termPattern(0), ctx.termPattern(1), peek);
+    }
+
+    @Override
+    protected Matchings visitOr(MatchPatternParser.OrContext ctx, MatchPath peek) {
+        return visitBinaryOperation("or", ctx.termPattern(0), ctx.termPattern(1), peek);
+    }
+
+    @Override
+    public Matchings visitExprNot(MatchPatternParser.ExprNotContext ctx, MatchPath peek) {
+        return visitBinaryOperation("not", ctx.termPattern(), ctx, peek);
+    }
+
+    @Override
+    public Matchings visitExprNegate(MatchPatternParser.ExprNegateContext ctx, MatchPath peek) {
+        return visitUnaryOperation("sub", ctx.termPattern(), peek);
+    }
+
     private String convert(int op) {
         switch (op) {
             case MatchPatternParser.PLUS:
@@ -456,6 +520,11 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, MatchPath> {
                 return "and";
             case MatchPatternParser.OR:
                 return "or";
+            case MatchPatternParser.FORALL:
+                return "all";
+            case MatchPatternParser.EXISTS:
+                return "exists";
+
             default:
                 throw new UnsupportedOperationException("The operator " + op + "is not known");
         }
@@ -463,30 +532,33 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, MatchPath> {
 
     }
 
-    @Override
-    protected Matchings visitMult(MatchPatternParser.MultContext ctx, MatchPath peek) {
-        return visitBinaryOperation("mul", ctx.termPattern(0), ctx.termPattern(1), peek);
+    private Matchings reduceConformQuant(Matchings fromTerm, Matchings match) {
+        Matchings ret = new Matchings();
+        Map<String, MatchPath> quantifiedVarMap = match.first();
+
+        List<Map<String, MatchPath>> list = fromTerm.stream().filter(
+                map -> map.entrySet().stream().allMatch(
+                        entry -> {
+                            if (entry.getValue() != null) {
+                                MatchPath mp = (MatchPath) entry.getValue();
+                                Term mterm = (Term) mp.getUnit();
+                                if (quantifiedVarMap.containsKey(entry.getKey())) {
+                                    return ((QuantifiableVariable) quantifiedVarMap.get(entry.getKey()).getUnit()).name().toString().
+                                            equals(mterm.op().name().toString());
+                                } else {
+                                    return true;
                                 }
-
-    @Override
-    protected Matchings visitComparison(MatchPatternParser.ComparisonContext ctx, MatchPath peek) {
-        return visitBinaryOperation(convert(ctx.op.getType()), ctx.termPattern(0), ctx.termPattern(1), peek);
+                            } else {
+                                return true;
                             }
-
-    @Override
-    protected Matchings visitOr(MatchPatternParser.OrContext ctx, MatchPath peek) {
-        return visitBinaryOperation("or", ctx.termPattern(0), ctx.termPattern(1), peek);
                         }
+                )
+        ).collect(Collectors.toList());
 
-    @Override
-    public Matchings visitExprNot(MatchPatternParser.ExprNotContext ctx, MatchPath peek) {
-        return visitBinaryOperation("not", ctx.termPattern(), ctx, peek);
+        ret.addAll(list);
+        return ret;
     }
 
-    @Override
-    public Matchings visitExprNegate(MatchPatternParser.ExprNegateContext ctx, MatchPath peek) {
-        return visitUnaryOperation("sub", ctx.termPattern(), peek);
-    }
 
     @Override
     public Matchings visitExprParen(MatchPatternParser.ExprParenContext ctx, MatchPath peek) {

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

@@ -5,14 +5,16 @@ import edu.kit.iti.formal.psdbg.termmatcher.mp.MatchPath;
 
 import java.util.*;
 
-/**
- * Class Matching contains a hashmap of string to term
- */
 public class Matchings extends TreeSet<Map<String, MatchPath>> {
     public Matchings() {
         super(new VariableAssignmentComparator());
     }
 
+    public Matchings(TreeMap<String, MatchPath> m) {
+        this();
+        add(m);
+    }
+
     public static Matchings singleton(String name, MatchPath term) {
         Matchings matchings = new Matchings();
         Map<String, MatchPath> va = new TreeMap<>();

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

 package edu.kit.iti.formal.psdbg.termmatcher.mp;
 
 import de.uka.ilkd.key.logic.*;
+import de.uka.ilkd.key.logic.op.QuantifiableVariable;
 import lombok.Data;
 import lombok.EqualsAndHashCode;
 
@@ -27,9 +28,18 @@ public abstract class MatchPath<T, P> {
 
     public abstract PosInOccurrence pio();
 
-    public abstract Sequent getSequent();
 
-    public abstract SequentFormula getSequentFormula();
+    public Sequent getSequent() {
+        if (getParent() != null)
+            return getParent().getSequent();
+        return null;
+    }
+
+    public SequentFormula getSequentFormula() {
+        if (getParent() != null)
+            return getParent().getSequentFormula();
+        return null;
+    }
 
     public abstract int depth();
 
@@ -37,18 +47,15 @@ public abstract class MatchPath<T, P> {
         return unit.toString();
     }
 
-    public static class MPTerm extends MatchPath<Term, Object> {
-        MPTerm(MatchPath<? extends Object, ?> parent, Term unit, int pos) {
+    public static final class MPQuantifiableVarible extends MatchPath<QuantifiableVariable, Object> {
+
+        public MPQuantifiableVarible(MatchPath<? extends Object, ?> parent, QuantifiableVariable unit, int pos) {
             super(parent, unit, pos);
         }
 
         @Override
         public PosInOccurrence pio() {
-            if(getParent()==null) return null;
-            PosInOccurrence pio = getParent().pio();
-            if(getPosInParent()==SEQUENT_FORMULA_ROOT)
-                return pio;
-            return pio.down(getPosInParent());
+            return null;
         }
 
         @Override
@@ -61,6 +68,26 @@ public abstract class MatchPath<T, P> {
             return null;
         }
 
+        @Override
+        public int depth() {
+            return getParent().depth() + 1;
+        }
+    }
+
+    public static class MPTerm extends MatchPath<Term, Object> {
+        MPTerm(MatchPath<? extends Object, ?> parent, Term unit, int pos) {
+            super(parent, unit, pos);
+        }
+
+        @Override
+        public PosInOccurrence pio() {
+            if(getParent()==null) return null;
+            PosInOccurrence pio = getParent().pio();
+            if(getPosInParent()==SEQUENT_FORMULA_ROOT)
+                return pio;
+            return pio.down(getPosInParent());
+        }
+
         @Override
         public int depth() {
             return getUnit().depth();

matcher/src/test/java/edu/kit/iti/formal/psdbg/termmatcher/MatcherFacadeTest.java

@@ -54,6 +54,29 @@ public class MatcherFacadeTest {
 
     @Test
     public void matches() throws Exception {
+        System.out.println("QuantifierMatching");
+        shouldMatchForm("\\forall int i; \\exists int j; fint2(j,i)", "(\\forall i (\\exists j _))");
+
+        shouldMatchForm("fint2(1,i)", "fint2(1,i)");
+
+        shouldMatchForm("\\exists int i; fint2(1,i)", "(\\exists _ _)");
+
+        shouldMatchForm("\\exists int i; \\exists int j; fint2(j,i)", "(\\exists i (\\exists j _))");
+
+
+        shouldMatchForm("\\exists int i; \\exists int j; fint2(j,i)", "(\\exists i (\\exists j _))");
+
+        shouldMatchForm("\\exists int i; \\exists int j; fint2(j,i)", "(\\exists _ (\\exists j _))");
+
+        shouldMatchForm("\\exists int i; \\exists int j; fint2(j,i)", "(\\exists _ (\\exists _ _))");
+
+        shouldMatchForm("\\exists int i; \\exists int j; fint2(j,i)", "(\\exists i _)");
+
+        shouldMatchForm("\\exists int i; fint2(1,i)", "(\\exists i fint2(1,i))");
+
+        shouldMatchForm("\\exists int i; fint2(1,i)", "(\\exists ?X fint2(1,?X))");
+
+        shouldMatchForm("\\exists int i; \\exists int j; (fint2(i, j) -> fint2(j, i))", "(\\exists i (\\exists j (fint2(i, j) -> fint2(j, i))))");
         shouldMatch("f(a)", "_");
         shouldMatch("f(a)", "?X", "[{?X=f(a)}]");
         shouldMatch("h(a,a)", "h(?X,?X)", "[{?X=a}]");
@@ -186,46 +209,97 @@ public class MatcherFacadeTest {
         return dtp.parseSeq(in, services, namespace, abbrev);
     }
 
-    @Test
-    public void seqTest() throws Exception {
-        //testcases for empty matches
-        shouldMatchSeq("pred(a) ==> pred(a), pred(b)", " ==> _", "[{EMPTY_MATCH=null}]");
-
-        shouldMatchSeq("pred(a) ==> pred(a), pred(b)", "==>", "[{EMPTY_MATCH=null}]");
-        shouldMatchSeq("pred(a) ==> pred(a), pred(b)", "_ ==> ", "[{EMPTY_MATCH=null}]");
-        shouldMatchSeq("pred(a) ==> pred(a), pred(b)", "_ ==> _", "[{EMPTY_MATCH=null}]");
-        shouldMatchSeq("==> pred(a)", "==>", "[{EMPTY_MATCH=null}]");
-        shouldMatchSeq("pred(a) ==> ", "==>", "[{EMPTY_MATCH=null}]");
 
+    // Sollverhalten: Wenn es keinen Variablenbinder gibt, aber z.B. '_' oder '...',
+    // und positiv auf den Ausdruck gematcht wird,
+    // dann soll der Term des Matchs in Form von anonymen Variablen gebunden werden
 
-        shouldMatchSeq("pred(a), pred(b) ==> pred(b)", "pred(?X), pred(?Z) ==> pred(?Y)", "[{?X=a, ?Y=b, ?Z=b}, {?X=b, ?Y=b, ?Z=a}]");
-        shouldMatchSeq("pred(a), pred(b) ==> pred(b)", "pred(?X), pred(?Z) ==> pred(?X)", "[{?X=b, ?Z=a}]");
-        shouldMatchSeq("pred(a), pred(b) ==> pred(b)", "pred(?X), pred(?Z) ==>", "[{?X=a, ?Z=b}, {?X=b, ?Z=a}]");
+    @Test
+    public void seqTest() throws Exception {
+        shouldMatchSeq("i <= 10 ==>",
+                "i <= ?X ==>",
+                "[{??_=leq(i,Z(0(1(#)))), ?X=Z(0(1(#))), ??_=i}]");
+
+        shouldMatchSeq("==> (\\forall int i; \\exists int j; fint2(j,i)) , pred(a)",
+                "==> (\\forall i (\\exists j _))",
+                "[{??_=exists{j:int}(fint2(j,i)), ??_=all{i:int}(exists{j:int}(fint2(j,i))), ??_=fint2(j,i)}]");
+
+        shouldMatchSeq("pred(a) ==> pred(a), pred(b)",
+                " ==> _",
+                "[{??_=pred(a)}, {??_=pred(b)}]");
+
+        shouldMatchSeq("pred(a) ==> pred(a), pred(b)",
+                "==>",
+                "[{EMPTY_MATCH=null}]");
+        shouldMatchSeq("pred(a) ==> pred(a), pred(b)",
+                "_ ==> ",
+                "[{??_=pred(a)}]");
+        shouldMatchSeq("pred(a) ==> pred(a), pred(b)",
+                "_ ==> _",
+                "[{??_=pred(b), ??_=pred(a)}, {??_=pred(a), ??_=pred(a)}]");
+        shouldMatchSeq("==> pred(a)",
+                "==>",
+                "[{EMPTY_MATCH=null}]");
+        shouldMatchSeq("pred(a) ==> ",
+                "==>",
+                "[{EMPTY_MATCH=null}]");
+
+
+        shouldMatchSeq("pred(a), pred(b) ==> pred(b)",
+                "pred(?X), pred(?Z) ==> pred(?Y)",
+                "[{??_=pred(a), ?X=b, ?Y=b, ??_=pred(b), ?Z=a, ??_=pred(b)}, {?X=a, ??_=pred(a), ?Y=b, ??_=pred(b), ?Z=b, ??_=pred(b)}]");
+        //"[{?X=a, ?Y=b, ?Z=b}, {?X=b, ?Y=b, ?Z=a}]");
+
+        shouldMatchSeq("pred(a), pred(b) ==> pred(b)",
+                "pred(?X), pred(?Z) ==> pred(?X)",
+                "[{??_=pred(a), ?X=b, ??_=pred(b), ?Z=a, ??_=pred(b)}]");
+//                "[{?X=b, ?Z=a}]");
+
+        shouldMatchSeq("pred(a), pred(b) ==> pred(b)",
+                "pred(?X), pred(?Z) ==>",
+                "[{??_=pred(a), ?X=b, ?Z=a, ??_=pred(b)}, {?X=a, ??_=pred(a), ?Z=b, ??_=pred(b)}]");
+//                "[{?X=a, ?Z=b}, {?X=b, ?Z=a}]");
 
         shouldMatchSeq(
                 "pred(f(a)), pred(b) ==> pred(b)",
                 "pred(?X), pred(?Z) ==>",
-                "[{?X=b, ?Z=f(a)}, {?X=f(a), ?Z=b}]");
+                "[{??_=pred(f(a)), ?X=b, ?Z=f(a), ??_=pred(b)}, {?X=f(a), ??_=pred(f(a)), ?Z=b, ??_=pred(b)}]");
+//                "[{?X=b, ?Z=f(a)}, {?X=f(a), ?Z=b}]");
 
         shouldMatchSeq(
                 "pred(f(a)), pred(b) ==> pred(b)",
                 "pred(...?X...) ==>",
-                "[{?X=a}, {?X=b}, {?X=f(a)}]");
+                "[{??_=pred(b), ?X=b}, {?X=a, ??_=pred(f(a))}, {?X=f(a), ??_=pred(f(a))}]");
+//                "[{?X=a}, {?X=b}, {?X=f(a)}]");
 
         shouldMatchSeq(
                 "fint2(1,2), fint2(2,3), !p ==> pred(a), p",
                 "fint2(1, ?X), fint2(?X, ?Y) ==> p",
-                "[{EMPTY_MATCH=null, ?X=Z(2(#)), ?Y=Z(3(#))}]");
-        shouldMatchSeq("2 >= 1, h2(1,2) = h2(2,3), h2(2,3) = 0 ==> p, !p", "?X=0 ==>", "[{?X=h2(Z(2(#)),Z(3(#)))}]");
-
-        shouldMatchSeq("pred(a) <-> pred(b), pred(a), pred(b) ==> p", "?X <-> ?Y ==> ", "[{?X=pred(a), ?Y=pred(b)}]");
+                "[{??_=fint2(Z(2(#)),Z(3(#))), ?X=Z(2(#)), ?Y=Z(3(#)), ??_=fint2(Z(1(#)),Z(2(#))), ??_=p}]");
+//                "[{EMPTY_MATCH=null, ?X=Z(2(#)), ?Y=Z(3(#))}]");
+        shouldMatchSeq("2 >= 1, h2(1,2) = h2(2,3), h2(2,3) = 0 ==> p, !p",
+                "?X=0 ==>",
+                "[{?X=h2(Z(2(#)),Z(3(#))), ??_=equals(h2(Z(2(#)),Z(3(#))),Z(0(#)))}]");
+//                "[{?X=h2(Z(2(#)),Z(3(#)))}]");
+
+        shouldMatchSeq("pred(a) <-> pred(b), pred(a), pred(b) ==> p",
+                "?X <-> ?Y ==> ",
+                "[{?X=pred(a), ?Y=pred(b), ??_=equiv(pred(a),pred(b))}]");
+//                "[{?X=pred(a), ?Y=pred(b)}]");
     }
 
     private void shouldMatchSeq(String seq, String seqPattern, String exp) throws ParserException {
         Sequent sequent = parseSeq(seq);