From c8626559501cd87f5f8a50eb50d46b6f5625151e Mon Sep 17 00:00:00 2001 From: Sarah Grebing Date: Mon, 21 Aug 2017 12:53:44 +0200 Subject: [PATCH] Bugfix for emptyMatch on sequent --- .../formal/psdb/termmatcher/MatchPattern.g4 | 24 ++- .../termmatcher/MatchPatternDualVisitor.java | 44 +++-- .../psdb/termmatcher/MatcherFacade.java | 55 +++++- .../formal/psdb/termmatcher/MatcherImpl.java | 164 +++++++++++++----- .../psdb/termmatcher/MatcherFacadeTest.java | 9 +- 5 files changed, 231 insertions(+), 65 deletions(-) diff --git a/src/main/antlr4/edu/kit/formal/psdb/termmatcher/MatchPattern.g4 b/src/main/antlr4/edu/kit/formal/psdb/termmatcher/MatchPattern.g4 index 4804b0f2..521d5a92 100644 --- a/src/main/antlr4/edu/kit/formal/psdb/termmatcher/MatchPattern.g4 +++ b/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 + | 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 diff --git a/src/main/java/edu/kit/formal/psdb/termmatcher/MatchPatternDualVisitor.java b/src/main/java/edu/kit/formal/psdb/termmatcher/MatchPatternDualVisitor.java index b9ac7b2a..63e12e34 100644 --- a/src/main/java/edu/kit/formal/psdb/termmatcher/MatchPatternDualVisitor.java +++ b/src/main/java/edu/kit/formal/psdb/termmatcher/MatchPatternDualVisitor.java @@ -12,6 +12,23 @@ public abstract class MatchPatternDualVisitor 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 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); } diff --git a/src/main/java/edu/kit/formal/psdb/termmatcher/MatcherFacade.java b/src/main/java/edu/kit/formal/psdb/termmatcher/MatcherFacade.java index 0767b767..1e20c27c 100644 --- a/src/main/java/edu/kit/formal/psdb/termmatcher/MatcherFacade.java +++ b/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, 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; + } + } } diff --git a/src/main/java/edu/kit/formal/psdb/termmatcher/MatcherImpl.java b/src/main/java/edu/kit/formal/psdb/termmatcher/MatcherImpl.java index 65a81d32..b52000b0 100644 --- a/src/main/java/edu/kit/formal/psdb/termmatcher/MatcherImpl.java +++ b/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 { if (!intersection.isEmpty()) continue; HashMap h3 = reduceConform(minfo1.matching, minfo2.matching); + if (h3 != null) { Set union = new HashSet<>(minfo1.matchedForms); union.addAll(minfo2.matchedForms); @@ -45,51 +47,15 @@ class MatcherImpl extends MatchPatternDualVisitor { private static HashMap reduceConform(HashMap h1, HashMap h2) { HashMap 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: , and m2: - * @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 h1 : m1) { - for (HashMap h2 : m2) { - HashMap 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 { } } + /*@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 { 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: , and m2: + * + * @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 h1 : m1) { + for (HashMap h2 : m2) { + HashMap 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 { 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 { 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 diff --git a/src/test/java/edu/kit/formal/psdb/termmatcher/MatcherFacadeTest.java b/src/test/java/edu/kit/formal/psdb/termmatcher/MatcherFacadeTest.java index 9c399e82..dec1e324 100644 --- a/src/test/java/edu/kit/formal/psdb/termmatcher/MatcherFacadeTest.java +++ b/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)...)"); } -- 2.26.2