From 1b7640ff616d041628716c63afe988bfce1c265b Mon Sep 17 00:00:00 2001 From: Sarah Grebing Date: Mon, 19 Mar 2018 09:34:32 +0100 Subject: [PATCH] Bugfix and added testcases --- .../interpreter/matcher/KeyTermMatcher.java | 48 +++++---- .../matcher/KeyMatcherFacadeTest.java | 102 ++++++++++++++++-- 2 files changed, 122 insertions(+), 28 deletions(-) diff --git a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/KeyTermMatcher.java b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/KeyTermMatcher.java index dd0fc5b2..29a191ce 100644 --- a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/KeyTermMatcher.java +++ b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/KeyTermMatcher.java @@ -11,13 +11,16 @@ import java.util.stream.IntStream; import java.util.stream.Stream; public class KeyTermMatcher extends KeyTermBaseVisitor { - 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 EMPTY_VARIABLE_ASSIGNMENT = EMPTY_MATCH.first(); + static Map 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 { 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 patternTerms) { MatchPath.MPSequent seq = MatchPathFacade.create(sequent); @@ -42,12 +51,12 @@ public class KeyTermMatcher extends KeyTermBaseVisitor { 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 { 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> map = new HashMap<>(); List sequentFormulas = @@ -238,6 +249,7 @@ public class KeyTermMatcher extends KeyTermBaseVisitor { } 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 { } //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 subTerms(MatchPath.MPTerm peek) { diff --git a/rt-key/src/test/java/edu/kit/iti/formal/psdbg/interpreter/matcher/KeyMatcherFacadeTest.java b/rt-key/src/test/java/edu/kit/iti/formal/psdbg/interpreter/matcher/KeyMatcherFacadeTest.java index 4b1af2ae..4df4967b 100644 --- a/rt-key/src/test/java/edu/kit/iti/formal/psdbg/interpreter/matcher/KeyMatcherFacadeTest.java +++ b/rt-key/src/test/java/edu/kit/iti/formal/psdbg/interpreter/matcher/KeyMatcherFacadeTest.java @@ -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 -- GitLab