Commit 54462912 authored by Sarah Grebing's avatar Sarah Grebing

Quantifier Matching Still one bug

parent a222dbe0
Pipeline #16897 failed with stages
in 117 minutes and 10 seconds
......@@ -441,6 +441,7 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, MatchPath> {
if (toMatch.boundVars().size() != ctx.boundVars.size()) {
return NO_MATCH;
}
Matchings match = EMPTY_MATCH;
for (int i = 0; i < ctx.boundVars.size(); i++) {
......@@ -448,7 +449,7 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, MatchPath> {
QuantifiableVariable qv = toMatch.boundVars().get(i);
if (qfPattern.getType() == MatchPatternLexer.DONTCARE) {
match = reduceConform(match, EMPTY_MATCH);
match = reduceConform(match, Matchings.singleton(qfPattern.getText(), new MatchPath.MPQuantifiableVarible(peek, qv, i)));
continue;
}
if (qfPattern.getType() == MatchPatternLexer.SID) {
......
......@@ -13,7 +13,7 @@ script split_from_quicksort_nice() {
cases{
case match `==> seqDef(_,_,_) = seqDef(_, _, _)`:
auto;
case match `==> \exists ...`: //hier sollten bessere branchnamen hin
case match `==> \exists iv (\exists jv _)`: //this should match
instantiate var=`iv` with=`i_0`;
instantiate var=`jv` with=`j_0`;
auto;
......
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