Quantifier Matching

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

@@ -22,7 +22,7 @@ sequentPattern : antec=semiSeqPattern? ARROW succ=semiSeqPattern? #sequentArrow
 semiSeqPattern : termPattern (',' termPattern)*;
 
 termPattern :
-   '(' (EXISTS|FORALL) (SID|ID)  termPattern ')'                #quantForm
+   '(' quantifier=(EXISTS|FORALL) boundVars+=(SID|ID)+  skope=termPattern ')'  #quantForm
     |  termPattern MUL termPattern                              #mult
     | <assoc=right> termPattern op=(DIV|MOD) termPattern        #divMod
     | termPattern op=(PLUS|MINUS) termPattern                   #plusMinus

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);
@@ -488,6 +490,64 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, MatchPath> {
         return visitUnaryOperation("sub", ctx.termPattern(), peek);
     }
 
+    @Override
+    public Matchings visitQuantForm(MatchPatternParser.QuantFormContext ctx, MatchPath peek) {
+        Term toMatch = (Term) peek.getUnit();
+        if (!toMatch.op().toString().equals(ctx.quantifier.getText().substring(1))) {
+            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.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 reduceConformQuant(fromTerm, match);
+    }
+
+    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;
+                                }
+                            } else {
+                                return true;
+                            }
+                        }
+                )
+        ).collect(Collectors.toList());
+
+        ret.addAll(list);
+        return ret;
+    }
+
+
     @Override
     public Matchings visitExprParen(MatchPatternParser.ExprParenContext ctx, MatchPath peek) {
         return handleBindClause(ctx.bindClause(), peek, accept(ctx.termPattern(), 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,7 +54,11 @@ public class MatcherFacadeTest {
 
     @Test
     public void matches() throws Exception {
-        shouldMatchForm("\\exists int i; \\exists int j; (fint2(i, j) -> fint2(j, i))", "\\exists int i; \\exists int j; (fint2(i, j) -> fint2(j, i))");
+        shouldMatchForm("fint2(1,i)", "fint2(1,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}]");