Commit 1b7640ff authored by Sarah Grebing's avatar Sarah Grebing

Bugfix and added testcases

parent 3934685e
Pipeline #20276 failed with stages
in 3 minutes and 35 seconds
......@@ -11,13 +11,16 @@ import java.util.stream.IntStream;
import java.util.stream.Stream;
public class KeyTermMatcher extends KeyTermBaseVisitor<Matchings, MatchPath> {
static final Matchings NO_MATCH = new Matchings();
static Matchings NO_MATCH;
//= new Matchings();
static final Matchings EMPTY_MATCH = Matchings.singleton("EMPTY_MATCH", null);
static Matchings EMPTY_MATCH;
//= Matchings.singleton("EMPTY_MATCH", null);
static final Map<String, MatchPath> EMPTY_VARIABLE_ASSIGNMENT = EMPTY_MATCH.first();
static Map<String, MatchPath> EMPTY_VARIABLE_ASSIGNMENT;
//= EMPTY_MATCH.first();
private String randomName;
Random random = new Random(42L);
// MatchPath peek;
......@@ -25,6 +28,12 @@ public class KeyTermMatcher extends KeyTermBaseVisitor<Matchings, MatchPath> {
private boolean catchAll = false;
public KeyTermMatcher() {
NO_MATCH = new Matchings();
EMPTY_MATCH = Matchings.singleton("EMPTY_MATCH", null);
EMPTY_VARIABLE_ASSIGNMENT = EMPTY_MATCH.first();
}
public Matchings matchesToplevel(Sequent sequent, List<Term> patternTerms) {
MatchPath.MPSequent seq = MatchPathFacade.create(sequent);
......@@ -42,12 +51,12 @@ public class KeyTermMatcher extends KeyTermBaseVisitor<Matchings, MatchPath> {
public Matchings matchesSequent(Sequent sequent, Sequent pattern) {
MatchPath.MPSequent mps = MatchPathFacade.create(sequent);
Matchings ms = matchesSemisequent(
MatchPathFacade.createSuccedent(mps),
pattern.succedent());
Matchings ma = matchesSemisequent(
MatchPathFacade.createAntecedent(mps),
pattern.antecedent());
Matchings ms = new Matchings();
Matchings ma = new Matchings();
MatchPath.MPSemiSequent succPath = MatchPathFacade.createSuccedent(mps);
ms = matchesSemisequent(succPath, pattern.succedent());
ma = matchesSemisequent(MatchPathFacade.createAntecedent(mps), pattern.antecedent());
return reduceConform(ms, ma);
}
......@@ -63,9 +72,11 @@ public class KeyTermMatcher extends KeyTermBaseVisitor<Matchings, MatchPath> {
Semisequent semiSeq = peek.getUnit();
if (semiSeq.isEmpty()) {
return patterns.isEmpty()
? EMPTY_MATCH
: NO_MATCH;
if(patterns.isEmpty()){
return Matchings.singleton("EMPTY_MATCH", null);
} else {
return new Matchings();
}
}
HashMap<Term, Map<SequentFormula, Matchings>> map = new HashMap<>();
List<MatchPath.MPSequentFormula> sequentFormulas =
......@@ -238,6 +249,7 @@ public class KeyTermMatcher extends KeyTermBaseVisitor<Matchings, MatchPath> {
}
if(pattern.equals(subject1.getUnit()))
return EMPTY_MATCH;
// return Matchings.singleton(pattern.toString(), subject1);
for (int i = 0; i < subject.getUnit().subs().size(); i++) {
Term tt = subject.getUnit().sub(i);
Term pt = pattern.sub(i);
......@@ -253,15 +265,13 @@ public class KeyTermMatcher extends KeyTermBaseVisitor<Matchings, MatchPath> {
}
//region helper
private String getBindingName(Name name) {
if (name.toString().equals("?"))
return getRandomName();
return name.toString();
public String getRandomName() {
return "??_" + getRandomNumber();
}
public String getRandomName() {
return randomName;
private int getRandomNumber() {
return Math.abs(random.nextInt());
}
private Stream<MatchPath.MPTerm> subTerms(MatchPath.MPTerm peek) {
......
......@@ -5,6 +5,7 @@ import de.uka.ilkd.key.control.KeYEnvironment;
import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.logic.NamespaceSet;
import de.uka.ilkd.key.logic.Sequent;
import de.uka.ilkd.key.logic.Term;
import de.uka.ilkd.key.parser.DefaultTermParser;
import de.uka.ilkd.key.parser.ParserException;
import de.uka.ilkd.key.pp.AbbrevMap;
......@@ -40,18 +41,70 @@ public class KeyMatcherFacadeTest {
}
/**
* Actually testcases for KeyTermMatcher not for Facade
* @throws Exception
*/
@Test
public void matchTerms() throws Exception {
shouldMatchT("f(a)", "?");
shouldMatchT("f(a)", "f(a)");
shouldMatchT("f(a)", "?X", "[{?X=f(a)}]");
shouldMatchT("h(a,a)", "h(?X,?X)", "[{?X=a}]");
shouldMatchT("h(a,b)", "h(?X,?X)", "[]");
}
@Test
public void matchSeq() throws Exception {
shouldMatch("p ==>", "p ==>");
shouldMatch("==> pred(a), q", "==> pred(?X:S), q");
shouldMatch("==> p, q", "==> ?X:Formula");
shouldMatch("==> p, q", "==> p, q");
shouldMatch("==> p, q", "==> q, p");
shouldMatch("==> pred(a), q", "==> pred(?X)");
//atm missing is catching the toplevel formula
//shouldMatch("==> pred(a)", "==> pred(?)", "[]");
shouldMatch("h2(2,2) = 0 ==>p, !p", "?X=0 ==>", "[{EMPTY_MATCH=null, ?X=h2(Z(2(#)),Z(2(#)))}]");
shouldMatch("2 >= 1, h2(1,2) = h2(2,3), h2(2,3) = 0 ==> p, !p", "?X=0 ==>", "[{EMPTY_MATCH=null, ?X=Z(2(#))}, {EMPTY_MATCH=null, ?X=h2(Z(2(#)),Z(3(#)))}]");
shouldMatch("p ==>", "p ==>", "[{EMPTY_MATCH=null}]");
shouldMatch("==> pred(a), q", "==> pred(?X:S), q", "[{?X=a}]");
shouldMatch("==> p, q", "==> ?X:Formula", "[{?X=p}, {?X=q}]");
shouldMatch("==> p, q", "==> p, q","[{EMPTY_MATCH=null}]");
shouldMatch("==> p, q", "==> q, p", "[{EMPTY_MATCH=null}]");
shouldMatch("==> pred(a), q", "==> pred(?X)", "[{?X=a}]");
shouldMatch("h2(2,2) = 0 ==>", "?X=0 ==>", "[{?X=h2(Z(2(#)),Z(2(#)))}]");
shouldMatch("==>f(g(a))= 0", "==> f(...a...) = 0", "[{EMPTY_MATCH=null}]");
}
@Test
public void negativeMatchSeq() throws Exception {
shouldNotMatch("p==>", "==> p");
}
@Test
public void testBindContext() throws Exception {
//shouldMatch("f(a)", "f(a) : ?Y", "[{?Y=f(a)}]");
//shouldMatch("f(g(a))", "_ \\as ?Y", "[{?Y=f(g(a))}]");
//shouldMatch("i+i+j", "(?X + ?Y) : ?Z", "[{?X=add(i,i), ?Y=j, ?Z=add(add(i,i),j)}]");
shouldMatch("==>f(g(a))= 0", "==> f((...a...):?G) = 0", "[{?G=g(a), EMPTY_MATCH=null}]");
shouldMatch("==>f(f(g(a)))= 0", "==> f((...a...):?G) = 0", "[{?G=f(g(a)), EMPTY_MATCH=null}]");
shouldMatch("==>f(f(g(a)))= 0", "==> f((...g(...a...)...):?G) = 0", "[{?G=f(g(a)), EMPTY_MATCH=null}]");
shouldMatch("==>f(f(g(a)))= 0", "==> f((...g((...a...):?Q)...):?G) = 0", "[{?G=f(g(a)), EMPTY_MATCH=null, ?Q=a}]");
shouldMatch("pred(f(a)) ==>", "pred((...a...):?Q) ==>","[{EMPTY_MATCH=null, ?Q=f(a)}]");
shouldMatch("p ==>", "(p):?X:Formula ==>", "[{EMPTY_MATCH=null, ?X=p}]");
shouldMatch("pred(a) ==>", "(pred(?)):?X:Formula ==>");
shouldMatch("==>f(f(g(a)))= 0", "==> (f((...g((...a...):?Q)...):?G)):?Y = 0", "[{?G=f(g(a)), EMPTY_MATCH=null, ?Q=a, ?Y=f(f(g(a)))}]");
// shouldMatch("f(f(g(a)))= 0 ==>", "f( (... g( (...a...):?Q ) ...) : ?R) : ?Y = 0 ==>",
// "[{EMPTY_MATCH=null, ?Q=a, ?Y=f(f(g(a))), ?R=f(g(a))}]");
}
@Test
public void hasToplevelComma() throws Exception {
Assert.assertTrue(!KeyMatcherFacade.hasToplevelComma("a=b,c=d").isEmpty());
......@@ -60,12 +113,38 @@ public class KeyMatcherFacadeTest {
//region: helper
private void shouldMatch(String keysequent, String pattern) throws ParserException {
private void shouldNotMatch(String s, String s1) throws Exception{
Assert.assertTrue(shouldMatch(s, s1).size()==0);
}
private void shouldMatch(String keysequent, String pattern, String exp) throws Exception {
Matchings m = shouldMatch(keysequent, pattern);
System.out.println("m = " + m);
Assert.assertEquals(exp, m.toString());
}
private Matchings shouldMatch(String keysequent, String pattern) throws ParserException {
Sequent seq = parseKeySeq(keysequent);
KeyMatcherFacade.KeyMatcherFacadeBuilder builder = KeyMatcherFacade.builder().environment(keyenv);
KeyMatcherFacade kfm = builder.sequent(seq).build();
Matchings m = kfm.matches(pattern, null);
System.out.println(m);
return kfm.matches(pattern, null);
}
private Matchings shouldMatchT(String keyterm, String pattern) throws ParserException {
KeyTermMatcher ktm = new KeyTermMatcher();
Matchings m = ktm.visit(parseKeyTerm(pattern), MatchPathFacade.createRoot(parseKeyTerm(keyterm)));
return m;
}
private void shouldMatchT(String s, String s1, String exp) throws ParserException {
Matchings m = shouldMatchT(s, s1);
System.out.println("m = " + m);
Assert.assertEquals(m.toString(), exp);
}
public Sequent parseKeySeq(String seq) throws ParserException {
......@@ -73,6 +152,11 @@ public class KeyMatcherFacadeTest {
return dtp.parseSeq(in, services, namespace, abbrev);
}
public Term parseKeyTerm(String t) throws ParserException {
Reader in = new StringReader(t);
return dtp.parse(in, null, services, namespace, abbrev, true);
}
//endregion
......
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