Commit 427e4177 authored by Sarah Grebing's avatar Sarah Grebing

Bugfix for emptyMatch on sequent

parent c8626559
...@@ -3,6 +3,7 @@ package edu.kit.formal.psdb.termmatcher; ...@@ -3,6 +3,7 @@ package edu.kit.formal.psdb.termmatcher;
import de.uka.ilkd.key.logic.SequentFormula; import de.uka.ilkd.key.logic.SequentFormula;
import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.Term;
import org.antlr.v4.runtime.Token; import org.antlr.v4.runtime.Token;
import org.key_project.util.collection.ImmutableArray;
import java.util.*; import java.util.*;
import java.util.stream.IntStream; import java.util.stream.IntStream;
...@@ -57,29 +58,40 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, Term> { ...@@ -57,29 +58,40 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, Term> {
} }
/** /**
* Visit '_' * Visit a semisequent pattern f(x), f(y)
*
* @param ctx * @param ctx
* @param peek * @param peek
* @return * @return
*/ */
@Override @Override
public Matchings visitDontCare(MatchPatternParser.DontCareContext ctx, Term peek) { protected Matchings visitSemiSeqPattern(MatchPatternParser.SemiSeqPatternContext ctx, Term peek) {
return null;
}
/*@Override
protected Matchings visitStartDontCare(MatchPatternParser.StarDontCareContext ctx, Term peek) {
if (peek != null) { if (peek != null) {
return EMPTY_MATCH; return EMPTY_MATCH;
} else { } else {
return NO_MATCH; return NO_MATCH;
} }
} }*/
/*@Override /**
protected Matchings visitStartDontCare(MatchPatternParser.StarDontCareContext ctx, Term peek) { * Visit '_'
*
* @param ctx
* @param peek
* @return
*/
@Override
public Matchings visitDontCare(MatchPatternParser.DontCareContext ctx, Term peek) {
if (peek != null) { if (peek != null) {
return EMPTY_MATCH; return EMPTY_MATCH;
} else { } else {
return NO_MATCH; return NO_MATCH;
} }
}*/ }
/** /**
* Visit a Schema Variable * Visit a Schema Variable
...@@ -239,20 +251,25 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, Term> { ...@@ -239,20 +251,25 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, Term> {
return NO_MATCH; return NO_MATCH;
} }
/**
* Visit a semisequent pattern f(x), f(y)
* @param ctx
* @param peek
* @return
*/
@Override @Override
protected Matchings visitSemiSeqPattern(MatchPatternParser.SemiSeqPatternContext ctx, Term peek) { protected Matchings visitNumber(MatchPatternParser.NumberContext ctx, Term peek) {
return null; //we are at a natural number
if (peek.op().name().toString().equals("Z")) {
ImmutableArray<Term> subs = peek.subs();
int transformedString = transformToNumber(peek.sub(0));
return EMPTY_MATCH;
} else {
return NO_MATCH;
}
} }
@Override private int transformToNumber(Term sub) {
protected Matchings visitNumber(MatchPatternParser.NumberContext ctx, Term peek) { int number = 0;
return null;
return 0;
} }
/** /**
......
...@@ -46,17 +46,16 @@ public class MatcherFacadeTest { ...@@ -46,17 +46,16 @@ public class MatcherFacadeTest {
shouldMatch("i+j", "add(?X,?Y)", "[{?X=i, ?Y=j}]"); shouldMatch("i+j", "add(?X,?Y)", "[{?X=i, ?Y=j}]");
shouldMatch("i+j", "?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", "p & ?X", "[{?X=q}]");
//shouldMatchForm("p & q", "?X & q", "[{?X=p}]"); shouldMatchForm("p & q", "?X & q", "[{?X=p}]");
//shouldMatch("1*j", "add(1,?Y)", "[{?Y=j}]"); System.out.println(parseKeyTerm("12004"));
shouldMatch("1", "1");
// shouldMatch("1*j", "1 + ?Y", "[]");
//shouldMatch("f(a) ==> f(a), f(b)" , "==> f(?X)", [{?X=a}]); //shouldMatch("f(a) ==> f(a), f(b)" , "==> f(?X)", [{?X=a}]);
//shouldMatch("f(a) ==> f(a), f(b)" , "f(a) ==> f(?X)", [{?X=a}]); //shouldMatch("f(a) ==> f(a), f(b)" , "f(a) ==> f(?X)", [{?X=a}]);
//shouldNotMatch("f(a) ==> f(a), f(b)" , "f(?X) ==> f(?X), f(a)"); //shouldNotMatch("f(a) ==> f(a), f(b)" , "f(?X) ==> f(?X), f(a)");
//shouldMatch("f(a) ==> f(a), f(b)" , "==>");
//shouldMatch("f(a) ==> f(a), f(b)" , "_ ==> _");
//shouldMatch("f(a) ==> f(a), f(b)" , " ==> _");
//shouldMatch("f(a) ==> f(a), f(b)" , "_ ==> ");
} }
...@@ -163,6 +162,13 @@ public class MatcherFacadeTest { ...@@ -163,6 +162,13 @@ public class MatcherFacadeTest {
shouldMatchSeq("==> pred(a)", "==>", "[{EMPTY_MATCH=null}]"); shouldMatchSeq("==> pred(a)", "==>", "[{EMPTY_MATCH=null}]");
shouldMatchSeq("pred(a) ==> ", "==>", "[{EMPTY_MATCH=null}]"); shouldMatchSeq("pred(a) ==> ", "==>", "[{EMPTY_MATCH=null}]");
shouldMatchSeq("pred(a) ==> pred(a), pred(b)", "==>", "[{EMPTY_MATCH=null}]");
shouldMatchSeq("pred(a) ==> pred(a), pred(b)", "_ ==> ", "[{EMPTY_MATCH=null}]");
//these two need to be checked I think
shouldMatchSeq("pred(a) ==> pred(a), pred(b)", "_ ==> _", "[{EMPTY_MATCH=null}, {EMPTY_MATCH=null}]");
shouldMatchSeq("pred(a) ==> pred(a), pred(b)", " ==> _", "[{EMPTY_MATCH=null}, {EMPTY_MATCH=null}]");
} }
private void shouldMatchSeq(String seq, String seqPattern, String exp) throws ParserException { private void shouldMatchSeq(String seq, String seqPattern, String exp) throws ParserException {
......
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