From a3e2a7807b71a4aea037b8a42778a25235f4bef8 Mon Sep 17 00:00:00 2001 From: Sarah Grebing Date: Wed, 21 Mar 2018 10:15:38 +0100 Subject: [PATCH] Bugfix and modified testcases --- .../psdbg/interpreter/matcher/EmptyMatch.java | 55 +++++ .../psdbg/interpreter/matcher/KeYMatcher.java | 2 +- .../interpreter/matcher/KeyTermMatcher.java | 169 +++++----------- .../psdbg/interpreter/matcher/Match.java | 23 +++ .../psdbg/interpreter/matcher/Matchings.java | 91 +-------- .../interpreter/matcher/MutableMatchings.java | 191 ++++++++++++++++++ .../psdbg/interpreter/matcher/NoMatch.java | 52 +++++ .../matcher/KeyMatcherFacadeTest.java | 40 ++-- 8 files changed, 403 insertions(+), 220 deletions(-) create mode 100644 rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/EmptyMatch.java create mode 100644 rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/Match.java create mode 100644 rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/MutableMatchings.java create mode 100644 rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/NoMatch.java diff --git a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/EmptyMatch.java b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/EmptyMatch.java new file mode 100644 index 00000000..06cbaaae --- /dev/null +++ b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/EmptyMatch.java @@ -0,0 +1,55 @@ +package edu.kit.iti.formal.psdbg.interpreter.matcher; + +import java.util.*; +@Deprecated +public class EmptyMatch implements Matchings { + public static EmptyMatch INSTANCE = new EmptyMatch(); + // public static Matching EMPTY_MATCH_INSTANCE = new Matching(); + + private EmptyMatch() { + } + + @Override + public boolean isNoMatch() { + return false; + } + + @Override + public boolean isEmpty() { + return true; + } + + @Override + public void add(String binder, MatchPath term) { + //throw new IllegalStateException(); + + + } + + @Override + public void add(Match singleton) { + throw new IllegalStateException(); + } + + @Override + public void addAll(Collection matchings) { + throw new IllegalStateException(); + } + + @Override + public Collection getMatchings() { + ArrayList l = new ArrayList(); + l.add(new Match()); + return l; + } + + @Override + public Matchings reduceConform(Matchings other) { + return other; + } + + @Override + public String toString() { + return "{{}}"; + } +} diff --git a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/KeYMatcher.java b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/KeYMatcher.java index d7bb9faa..bc20e005 100644 --- a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/KeYMatcher.java +++ b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/KeYMatcher.java @@ -178,7 +178,7 @@ public class KeYMatcher implements MatcherApi { LOGGER.debug("currentState has no match= " + currentState.getData().getNode().sequent()); return Collections.emptyList(); } else { - Map firstMatch = m.first(); + Match firstMatch = m.getMatchings().iterator().next() ; VariableAssignment va = new VariableAssignment(null); for (String s : firstMatch.keySet()) { MatchPath matchPath = firstMatch.get(s); 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 29a191ce..9b149307 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 @@ -3,7 +3,8 @@ package edu.kit.iti.formal.psdbg.interpreter.matcher; import com.google.common.collect.Sets; import de.uka.ilkd.key.logic.*; import de.uka.ilkd.key.logic.op.*; -import org.antlr.v4.runtime.Token; +import lombok.Getter; +import lombok.Setter; import java.util.*; import java.util.stream.Collectors; @@ -11,39 +12,24 @@ import java.util.stream.IntStream; import java.util.stream.Stream; public class KeyTermMatcher extends KeyTermBaseVisitor { - static Matchings NO_MATCH; - //= new Matchings(); - - static Matchings EMPTY_MATCH; - //= Matchings.singleton("EMPTY_MATCH", null); - - static Map EMPTY_VARIABLE_ASSIGNMENT; - //= EMPTY_MATCH.first(); - Random random = new Random(42L); // MatchPath peek; - private List currentposition = new ArrayList<>(); - private boolean catchAll = false; + @Setter @Getter 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); - Matchings ret = new Matchings(); + Matchings ret = new MutableMatchings(); Matchings antecMatches = matchesSemisequent(MatchPathFacade.createAntecedent(seq), patternTerms); Matchings succMatches = matchesSemisequent(MatchPathFacade.createSuccedent(seq), patternTerms); - //if(!antecMatches.equals(EMPTY_MATCH)) + //if(!antecMatches.equals(EmptyMatch.INSTANCE)) ret.addAll(antecMatches); - //if(!succMatches.equals(EMPTY_MATCH)) + //if(!succMatches.equals(EmptyMatch.INSTANCE)) ret.addAll(succMatches); return ret; } @@ -51,20 +37,15 @@ public class KeyTermMatcher extends KeyTermBaseVisitor { public Matchings matchesSequent(Sequent sequent, Sequent pattern) { MatchPath.MPSequent mps = MatchPathFacade.create(sequent); - 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); + Matchings ms = matchesSemisequent(succPath, pattern.succedent()); + Matchings ma = matchesSemisequent(MatchPathFacade.createAntecedent(mps), pattern.antecedent()); + return ms.reduceConform(ma); } private Matchings matchesSemisequent(MatchPath.MPSemiSequent peek, Semisequent pattern) { List patterns = pattern.asList().stream().map(SequentFormula::formula).collect(Collectors.toList()); return matchesSemisequent(peek, patterns); - } @@ -73,9 +54,10 @@ public class KeyTermMatcher extends KeyTermBaseVisitor { Semisequent semiSeq = peek.getUnit(); if (semiSeq.isEmpty()) { if(patterns.isEmpty()){ - return Matchings.singleton("EMPTY_MATCH", null); + return MutableMatchings.emptySingleton(); } else { - return new Matchings(); + return NoMatch.INSTANCE; + //return new MutableMatchings(); } } HashMap> map = new HashMap<>(); @@ -89,15 +71,15 @@ public class KeyTermMatcher extends KeyTermBaseVisitor { map.put(subPatternTerm, new HashMap<>()); for (MatchPath.MPSequentFormula sf : sequentFormulas) { Matchings temp = visit(subPatternTerm, MatchPathFacade.create(sf)); - if (!temp.equals(NO_MATCH)) + if (!temp.isNoMatch()) map.get(subPatternTerm).put(sf.getUnit(), temp); } } List matchings = new ArrayList<>(); reduceDisjoint(map, patterns, matchings); - Matchings ret = new Matchings(); - //.filter(x -> !x.equals(EMPTY_MATCH)) + Matchings ret = new MutableMatchings(); + //.filter(x -> !x.equals(EmptyMatch.INSTANCE)) matchings.forEach(ret::addAll); return ret; } @@ -111,7 +93,7 @@ public class KeyTermMatcher extends KeyTermBaseVisitor { */ @DispatchOn(EllipsisOp.class) public Matchings visitEllipsisOp(Term pattern, MatchPath subject) { - Matchings matchings = new Matchings(); + Matchings matchings = new MutableMatchings(); subTerms((MatchPath.MPTerm) subject).forEach(sub -> { Matchings s = visit(pattern.sub(0), sub); matchings.addAll(s); @@ -133,10 +115,10 @@ public class KeyTermMatcher extends KeyTermBaseVisitor { if (name.equalsIgnoreCase("?")) { name = getRandomName(); } - Matchings mSingleton = Matchings.singleton(name, subject); + Matchings mSingleton = MutableMatchings.singleton(name, subject); return mSingleton; } else { - return NO_MATCH; + return NoMatch.INSTANCE; } } @@ -146,13 +128,13 @@ public class KeyTermMatcher extends KeyTermBaseVisitor { public Matchings visitQuantifier(Term pattern, MatchPath subject) { Term toMatch = (Term) subject.getUnit(); if (!toMatch.op().equals(pattern.op())) { - return NO_MATCH; + return NoMatch.INSTANCE; } if (toMatch.boundVars().size() != pattern.boundVars().size()) { - return NO_MATCH; + return NoMatch.INSTANCE; } - Matchings match = EMPTY_MATCH; + Matchings match = MutableMatchings.emptySingleton(); /* for (int i = 0; i < pattern.boundVars().size(); i++) { @@ -161,7 +143,7 @@ public class KeyTermMatcher extends KeyTermBaseVisitor { if (qfPattern.getType() == MatchPatternLexer.DONTCARE) { //match = reduceConform(match, Matchings.singleton(qfPattern.getText(), new MatchPath.MPQuantifiableVarible(peek, qv, i))); - match = reduceConform(match, EMPTY_MATCH); + match = reduceConform(match, EmptyMatch.INSTANCE); continue; } if (qfPattern.getType() == MatchPatternLexer.SID) { @@ -173,9 +155,9 @@ public class KeyTermMatcher extends KeyTermBaseVisitor { new MatchPath.MPTerm(peek, termQVariable, -i))); } else { if (!qv.name().toString().equals(qfPattern.getText())) { - return NO_MATCH; + return NoMatch.INSTANCE; } - match = reduceConform(match, EMPTY_MATCH); + match = reduceConform(match, EmptyMatch.INSTANCE); } } @@ -195,9 +177,9 @@ public class KeyTermMatcher extends KeyTermBaseVisitor { return handleBindClause(ctx.bindClause(), peek, retM); /* // Decision: Order of bounded vars - Matchings mm = new Matchings(); + Matchings mm = new MutableMatching(); if (term.getUnit().boundVars().size() != pattern.boundVars().size()) { - return NO_MATCH; + return NoMatch.INSTANCE; } Map mPaths = new HashMap<>(); @@ -218,7 +200,7 @@ public class KeyTermMatcher extends KeyTermBaseVisitor { mPaths.put(name, term); } else if (!pv.equals(bv)) { - return NO_MATCH; + return NoMatch.INSTANCE; } } return mm;*/ @@ -229,9 +211,9 @@ public class KeyTermMatcher extends KeyTermBaseVisitor { @DispatchOn(MatchBinderOp.class) public Matchings visitMatchBinderOp(Term pattern, MatchPath subject) { Matchings matchings = visit(pattern.sub(1), subject); - if (matchings != NO_MATCH) { + if (matchings != NoMatch.INSTANCE) { String name = pattern.sub(0).op().name().toString(); - for (Map a : matchings) { + for (Match a : matchings.getMatchings()) { a.put(name, subject); } } @@ -242,24 +224,29 @@ public class KeyTermMatcher extends KeyTermBaseVisitor { @Override protected Matchings defaultVisit(Term pattern, MatchPath subject1) { - Matchings m = new Matchings(); + Matchings m = MutableMatchings.emptySingleton(); + //Matchings m = new MutableMatchings(); MatchPath subject = (MatchPath) subject1; if (subject.getUnit().subs().size() != pattern.subs().size()) { - return NO_MATCH; + return NoMatch.INSTANCE; } - if(pattern.equals(subject1.getUnit())) - return EMPTY_MATCH; + // if(pattern.equals(subject1.getUnit())) + // return EmptyMatch.INSTANCE; // 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); - Matchings msub = visit(pt, MatchPathFacade.create(subject, i)); - - if (msub.equals(NO_MATCH)) { - return NO_MATCH; - } - m = reduceConform(m, msub); - } + if(pattern.op().equals(((Term) subject1.getUnit()).op())) { + for (int i = 0; i < subject.getUnit().subs().size(); i++) { + Term tt = subject.getUnit().sub(i); + Term pt = pattern.sub(i); + Matchings msub = visit(pt, MatchPathFacade.create(subject, i)); + + if (msub.equals(NoMatch.INSTANCE)) { + return NoMatch.INSTANCE; + } + m = m.reduceConform(msub); + } + } else { + return NoMatch.INSTANCE; + } return m; } @@ -291,62 +278,6 @@ public class KeyTermMatcher extends KeyTermBaseVisitor { //region Reductions - /** - * Reduce the matchings by eliminating non-compatible matchings. - * For example: - * m1: , and m2: - * - * @param m1 - * @param m2 - * @return - */ - protected static Matchings reduceConform(Matchings m1, Matchings m2) { - //shortcuts - if (m1 == NO_MATCH || m2 == NO_MATCH) return NO_MATCH; - if (m1 == EMPTY_MATCH || m1.size()==0) return m2; - if (m2 == EMPTY_MATCH || m2.size()==0) return m1; - - Matchings m3 = new Matchings(); - boolean oneMatch = false; - for (Map h1 : m1) { - for (Map h2 : m2) { - Map h3 = reduceConform(h1, h2); - if (h3 != null) { - //m3.add(h3); - if (!m3.contains(h3)) m3.add(h3); - oneMatch = true; - } - } - } - return oneMatch ? m3 : NO_MATCH; - } - - - private static HashMap reduceConform(Map h1, Map h2) { - HashMap listOfElementsofH1 = new HashMap<>(h1); - - for (String s1 : listOfElementsofH1.keySet()) { - - if (!s1.equals("EMPTY_MATCH") && h2.containsKey(s1)) { - if (h2.get(s1) instanceof MatchPath.MPQuantifiableVariable && - !((QuantifiableVariable) h2.get(s1).getUnit()).name().toString().equals(h1.get(s1).toString())) { - return null; - } - if (h1.get(s1) instanceof MatchPath.MPQuantifiableVariable && - !((QuantifiableVariable) h1.get(s1).getUnit()).name().toString().equals(h2.get(s1).toString())) { - return null; - } - - if (!h2.get(s1).equals(h1.get(s1))) { - return null; - } - - } - } - listOfElementsofH1.putAll(h2); - return listOfElementsofH1; - } - /* @param map * @param patterns @@ -355,7 +286,7 @@ public class KeyTermMatcher extends KeyTermBaseVisitor { private void reduceDisjoint(HashMap> map, List patterns, List matchings) { - reduceDisjoint(map, patterns, matchings, 0, EMPTY_MATCH, new HashSet<>()); + reduceDisjoint(map, patterns, matchings, 0, MutableMatchings.emptySingleton(), new HashSet<>()); } /** @@ -389,7 +320,7 @@ public class KeyTermMatcher extends KeyTermBaseVisitor { // the matchings for current pattern against the toplevel Matchings m = map.get(currentPattern).get(formula); //join them with the current Matchings - Matchings mm = reduceConform(m, ret); + Matchings mm = m.reduceConform(ret); chosenSequentFormulas.add(formula); // adding the formula, so other matchings can not choose it // recursion: choose the next matchings for the next pattern diff --git a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/Match.java b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/Match.java new file mode 100644 index 00000000..0e84511d --- /dev/null +++ b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/Match.java @@ -0,0 +1,23 @@ +package edu.kit.iti.formal.psdbg.interpreter.matcher; + +import java.util.TreeMap; + +public class Match extends TreeMap { + public Match() { + } + + public Match(Match h1) { + super(h1); + } + + public static Match singleton(String binder, MatchPath path) { + Match m = new Match(); + m.put(binder, path); + return m; + } + + public static Match empty() { + Match m = new Match(); + return m; + } +} diff --git a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/Matchings.java b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/Matchings.java index ef28bfea..e389f3c2 100644 --- a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/Matchings.java +++ b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/Matchings.java @@ -4,90 +4,19 @@ import com.google.common.collect.Sets; import java.util.*; -public class Matchings extends TreeSet> { - public Matchings() { - super(new VariableAssignmentComparator()); - } - - public Matchings(TreeMap m) { - this(); - add(m); - } +public interface Matchings { + public boolean isNoMatch(); + public boolean isEmpty(); - public static Matchings singleton(String name, MatchPath term) { - Matchings matchings = new Matchings(); - Map va = new TreeMap<>(); - va.put(name, term); - matchings.add(va); - return matchings; - } + public void add(String binder, MatchPath term); + public void add(Match singleton); + public void addAll(Collection matchings); -} + public Collection getMatchings(); -class VariableAssignmentComparator implements Comparator> { - /** - *
    - *
  1. both maps contains the same keys
    2. - *
  2. foreach key in lexi-order, the depth has to be greater
    3. - *
- * - * @return - */ - @Override - public int compare(Map o1, Map o2) { - if (isTrueSubset(o1.keySet(), o2.keySet())) { - return 1; - } - if (isTrueSubset(o2.keySet(), o1.keySet())) { - return -1; - } + public Matchings reduceConform(Matchings other); - if (!o1.keySet().equals(o2.keySet())) { - // different domains, - // there exists at least one variable that is not assign in the other - int cmp = Integer.compare(o1.size(), o2.size()); - if (cmp != 0) { - return cmp; - } else { - return compareVariableName(o1, o2); - } - } - - ArrayList keys = new ArrayList<>(Sets.intersection(o1.keySet(), o2.keySet())); - keys.sort(String::compareTo); // order of the traversal - keys.remove("EMPTY_MATCH"); - - for (String k : keys) { - int depthA = o1.get(k).depth(); - int depthB = o2.get(k).depth(); - int cmp = Integer.compare(depthA, depthB); - if (cmp != 0) - return cmp; - } - // all terms same depth: now let the lexi-order decide - for (String k : keys) { - int cmp = o1.get(k).toString().compareTo(o2.get(k).toString()); - if (cmp != 0) - return cmp; - } - return 0; + default void addAll(Matchings matches) { + addAll(matches.getMatchings()); } - - private int compareVariableName(Map o1, Map o2) { - return variableNames(o1).compareTo(variableNames(o2)); - } - - private String variableNames(Map va) { - return va.keySet().stream().reduce((a, b) -> a + '#' + b).orElse("#"); - } - - /** - * @param a - * @param b - * @return - */ - private boolean isTrueSubset(Set a, Set b) { - return b.containsAll(a) && !a.containsAll(b); - } - } \ No newline at end of file diff --git a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/MutableMatchings.java b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/MutableMatchings.java new file mode 100644 index 00000000..bfee15eb --- /dev/null +++ b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/MutableMatchings.java @@ -0,0 +1,191 @@ +package edu.kit.iti.formal.psdbg.interpreter.matcher; + +import com.google.common.collect.Sets; +import de.uka.ilkd.key.logic.SequentFormula; +import de.uka.ilkd.key.logic.Term; +import de.uka.ilkd.key.logic.op.QuantifiableVariable; + +import java.util.*; + +public class MutableMatchings implements Matchings { + public Set inner = new TreeSet<>(new VariableAssignmentComparator()); + + public static Matchings singleton(String name, MatchPath term) { + Matchings matchings = new MutableMatchings(); + matchings.add(name,term); + return matchings; + } + + public static Matchings emptySingleton() { + Matchings matchings = new MutableMatchings(); + matchings.add(Match.empty()); + return matchings; + } + + @Override + public boolean isNoMatch() { + return false; + } + + @Override + public boolean isEmpty() { + return false; + } + + @Override + public void add(String binder, MatchPath term) { + add(Match.singleton(binder, term)); + } + + @Override + public void add(Match matching) { + inner.add(matching); + } + + @Override + public void addAll(Collection matchings) { + inner.addAll(matchings); + } + + @Override + public Collection getMatchings() { + return inner; + } + + @Override + public String toString() { + return inner.toString(); + } + + /** + * Reduce the matchings by eliminating non-compatible matchings. + * For example: + * m1: , and m2: + * + * @param other + * @return + */ + @Override + public Matchings reduceConform(Matchings other) { + //shortcuts + if(other.isNoMatch()) return other.reduceConform(this); + if(other.isEmpty()) return other.reduceConform(this); + if(this.inner.size() == 0) return other; + MutableMatchings mother = (MutableMatchings) other; + + MutableMatchings m3 = new MutableMatchings(); + boolean oneMatch = false; + + for (Match h1 : inner) { + for (Match h2 : mother.inner) { + Match h3 = reduceConform(h1, h2); + if (h3 != null) { + if (!m3.inner.contains(h3)) + m3.add(h3); + oneMatch = true; + } + } + } + return oneMatch ? m3 : NoMatch.INSTANCE; + } + + + /** + * + * @param h1 + * @param h2 + * @return + */ + public static Match reduceConform(Match h1, Match h2) { + Match newMatch = new Match(h1); + + for (String s1 : newMatch.keySet()) { + if (h2.containsKey(s1)) { + if (h2.get(s1) instanceof MatchPath.MPQuantifiableVariable && + !((QuantifiableVariable) h2.get(s1).getUnit()).name().toString().equals(h1.get(s1).toString())) { + return null; + } + if (h1.get(s1) instanceof MatchPath.MPQuantifiableVariable && + !((QuantifiableVariable) h1.get(s1).getUnit()).name().toString().equals(h2.get(s1).toString())) { + return null; + } + + if (!h2.get(s1).equals(h1.get(s1))) { + return null; + } + } + } + newMatch.putAll(h2); + return newMatch; + } + + + +class VariableAssignmentComparator implements Comparator { + /** + *
    + *
  1. both maps contains the same keys
    2. + *
  2. foreach key in lexi-order, the depth has to be greater
    3. + *
+ * + * @return + */ + @Override + public int compare(Match o1, Match o2) { + if (isTrueSubset(o1.keySet(), o2.keySet())) { + return 1; + } + if (isTrueSubset(o2.keySet(), o1.keySet())) { + return -1; + } + + if (!o1.keySet().equals(o2.keySet())) { + // different domains, + // there exists at least one variable that is not assign in the other + int cmp = Integer.compare(o1.size(), o2.size()); + if (cmp != 0) { + return cmp; + } else { + return compareVariableName(o1, o2); + } + } + + ArrayList keys = new ArrayList<>(Sets.intersection(o1.keySet(), o2.keySet())); + keys.sort(String::compareTo); // order of the traversal + keys.remove("EMPTY_MATCH"); + + for (String k : keys) { + int depthA = o1.get(k).depth(); + int depthB = o2.get(k).depth(); + int cmp = Integer.compare(depthA, depthB); + if (cmp != 0) + return cmp; + } + // all terms same depth: now let the lexi-order decide + for (String k : keys) { + int cmp = o1.get(k).toString().compareTo(o2.get(k).toString()); + if (cmp != 0) + return cmp; + } + return 0; + } + + private int compareVariableName(Match o1, Match o2) { + return variableNames(o1).compareTo(variableNames(o2)); + } + + private String variableNames(Match va) { + return va.keySet().stream().reduce((a, b) -> a + '#' + b).orElse("#"); + } + + /** + * @param a + * @param b + * @return + */ + private boolean isTrueSubset(Set a, Set b) { + return b.containsAll(a) && !a.containsAll(b); + } + +} +} diff --git a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/NoMatch.java b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/NoMatch.java new file mode 100644 index 00000000..e804e737 --- /dev/null +++ b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/NoMatch.java @@ -0,0 +1,52 @@ +package edu.kit.iti.formal.psdbg.interpreter.matcher; + +import java.util.Collection; +import java.util.Collections; + +public class NoMatch implements Matchings { + public static NoMatch INSTANCE = new NoMatch(); + + private NoMatch() { + } + + @Override + public boolean isNoMatch() { + return true; + } + + @Override + public boolean isEmpty() { + return false; + } + + + @Override + public void add(String binder, MatchPath term) { + throw new IllegalStateException(); + } + + @Override + public void add(Match singleton) { + throw new IllegalStateException(); + } + + @Override + public void addAll(Collection matchings) { + throw new IllegalStateException(); + } + + @Override + public Collection getMatchings() { + return Collections.emptyList(); + } + + @Override + public Matchings reduceConform(Matchings other) { + return this; + } + + @Override + public String toString() { + return "{NOMATCH}"; + } +} 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 4df4967b..6b04e4a8 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 @@ -47,12 +47,11 @@ public class KeyMatcherFacadeTest { */ @Test public void matchTerms() throws Exception { - shouldMatchT("f(a)", "?"); - shouldMatchT("f(a)", "f(a)"); + System.out.println(shouldMatchT("f(a)", "?")); + System.out.println(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)", "[]"); } @@ -61,19 +60,22 @@ public class KeyMatcherFacadeTest { public void matchSeq() throws Exception { //atm missing is catching the toplevel formula //shouldMatch("==> pred(a)", "==> pred(?)", "[]"); + shouldMatch("2 >= 1, h2(1,2) = h2(2,3), h2(2,3) = 0 ==> p, !p", "?X=0 ==>", "[{?X=h2(Z(2(#)),Z(3(#)))}]"); - 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("h2(2,2) = 0 ==>p, !p", "?X=0 ==>", "[{?X=h2(Z(2(#)),Z(2(#)))}]"); - shouldMatch("p ==>", "p ==>", "[{EMPTY_MATCH=null}]"); + + shouldMatch("p ==>", "p ==>", "[{}]"); 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("==> p, q", "==> p, q","[{}]"); + shouldMatch("==> p, q", "==> q, p", "[{}]"); 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}]"); + shouldMatch("==>f(g(a))= 0", "==> f(...a...) = 0", "[{}]"); + + } @Test @@ -84,20 +86,20 @@ public class KeyMatcherFacadeTest { @Test public void testBindContext() throws Exception { - //shouldMatch("f(a)", "f(a) : ?Y", "[{?Y=f(a)}]"); + //how to deal with trying to match top-level, w.o. adding the type of the variable + shouldMatch("f(a)=0 ==> ", "(f(a)=0) : ?Y:Formula ==>", "[{?Y=equals(f(a),Z(0(#)))}]"); //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("==>f(g(a))= 0", "==> f((...a...):?G) = 0", "[{?G=g(a)}]"); + shouldMatch("==>f(f(g(a)))= 0", "==> f((...a...):?G) = 0", "[{?G=f(g(a))}]"); + shouldMatch("==>f(f(g(a)))= 0", "==> f((...g(...a...)...):?G) = 0", "[{?G=f(g(a))}]"); + shouldMatch("==>f(f(g(a)))= 0", "==> f((...g((...a...):?Q)...):?G) = 0", "[{?G=f(g(a)), ?Q=a}]"); + shouldMatch("pred(f(a)) ==>", "pred((...a...):?Q) ==>","[{?Q=f(a)}]"); + shouldMatch("p ==>", "(p):?X:Formula ==>", "[{?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)...):?G)):?Y = 0", "[{?G=f(g(a)), ?Q=a, ?Y=f(f(g(a)))}]"); // shouldMatch("f(f(g(a)))= 0 ==>", "f( (... g( (...a...):?Q ) ...) : ?R) : ?Y = 0 ==>", @@ -115,7 +117,7 @@ public class KeyMatcherFacadeTest { //region: helper private void shouldNotMatch(String s, String s1) throws Exception{ - Assert.assertTrue(shouldMatch(s, s1).size()==0); + Assert.assertTrue(shouldMatch(s, s1).getMatchings().size()==0); } private void shouldMatch(String keysequent, String pattern, String exp) throws Exception { -- 2.22.0