Commit a222dbe0 authored by Sarah Grebing's avatar Sarah Grebing

Quantifier Matching Testcases

parent bd990c81
Pipeline #16893 passed with stages
in 9 minutes and 21 seconds
......@@ -22,7 +22,7 @@ sequentPattern : antec=semiSeqPattern? ARROW succ=semiSeqPattern? #sequentArrow
semiSeqPattern : termPattern (',' termPattern)*;
termPattern :
'(' quantifier=(EXISTS|FORALL) boundVars+=(SID|ID)+ skope=termPattern ')' #quantForm
'(' quantifier=(EXISTS|FORALL) boundVars+=(SID|ID|DONTCARE)+ skope=termPattern ')' #quantForm
| termPattern MUL termPattern #mult
| <assoc=right> termPattern op=(DIV|MOD) termPattern #divMod
| termPattern op=(PLUS|MINUS) termPattern #plusMinus
......
......@@ -432,37 +432,38 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, MatchPath> {
return accept(func, peek);
}
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");
@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, EMPTY_MATCH);
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 reduceConformQuant(fromTerm, match);
}
@Override
......@@ -490,34 +491,42 @@ 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);
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";
case MatchPatternParser.FORALL:
return "all";
case MatchPatternParser.EXISTS:
return "exists";
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);
}
default:
throw new UnsupportedOperationException("The operator " + op + "is not known");
}
Matchings fromTerm = accept(ctx.skope, create(peek, 0));
return reduceConformQuant(fromTerm, match);
}
private Matchings reduceConformQuant(Matchings fromTerm, Matchings match) {
......
......@@ -54,8 +54,26 @@ 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))))");
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment