Commit 2bb44850 authored by Alexander Weigl's avatar Alexander Weigl

MatcherImpl rework

* Facade instances into MatcherImpl
* Simpler Implementation
* Ordering of Matchings
* Catch anonymous (not bounded) matches
parent eeff268d
Pipeline #13111 failed with stage
in 3 minutes and 11 seconds
......@@ -15,7 +15,9 @@ f(..., ... g(x) ...)
f(_, x, _, y, ... y ...)
*/
sequentPattern : antec=semiSeqPattern? ARROW succ=semiSeqPattern? | anywhere=semiSeqPattern;
sequentPattern : antec=semiSeqPattern? ARROW succ=semiSeqPattern? #sequentArrow
| anywhere=semiSeqPattern #sequentAnywhere
;
semiSeqPattern : termPattern (',' termPattern)*;
......
......@@ -186,12 +186,12 @@ public class SequentView extends CodeArea {
public boolean showSearchHighlights(String pattern) {
clearHighlight();
if (pattern.trim().isEmpty())
if (pattern.trim().isEmpty()) {
return false;
}
pattern = "(..." + pattern + "...) : ?COMPLETE";
if (node.get().sequent() != null) {
Matchings m = MatcherFacade.matches(pattern, node.get().sequent());
Matchings m = MatcherFacade.matches(pattern, node.get().sequent(), true);
if (m.size() == 0) return false;
for (Map<String, MatchPath> va : m) {
MatchPath<?> complete = va.get("?COMPLETE");
......
package edu.kit.formal.psdb.termmatcher;
import de.uka.ilkd.key.logic.Semisequent;
import de.uka.ilkd.key.logic.Sequent;
import de.uka.ilkd.key.logic.Term;
import lombok.Data;
import lombok.EqualsAndHashCode;
import lombok.ToString;
import org.key_project.util.collection.ImmutableList;
import org.key_project.util.collection.ImmutableSLList;
......@@ -12,8 +13,12 @@ import org.key_project.util.collection.ImmutableSLList;
* @version 1 (24.08.17)
*/
@Data
@EqualsAndHashCode(exclude = {"parent","posInParent"})
public class MatchPath<T> {
@EqualsAndHashCode(of = {"term"})
public abstract class MatchPath<T> {
public static final int ROOT = -1;
public static final int POSITION_ANTECEDENT = -2;
public static final int POSITION_SUCCEDENT = -3;
private final MatchPath<?> parent;
private final T term;
private final int posInParent;
......@@ -25,7 +30,7 @@ public class MatchPath<T> {
}
public static MatchPath<Term> createTermPath(MatchPath<Term> path, int i) {
return new MatchPath<>(path, path.getTerm().sub(i), i);
return new MatchPathTerm(path, path.getTerm().sub(i), i);
}
public ImmutableList<Integer> getPos() {
......@@ -36,12 +41,65 @@ public class MatchPath<T> {
}
}
public static <T> MatchPath<T> createRoot(T keyTerm) {
return new MatchPath<>(null, keyTerm, -1);
public static MatchPath<Term> createRoot(Term keyTerm) {
return new MatchPathTerm(null, keyTerm, -1);
}
public String toString() {
return term.toString();
}
public static MatchPathSemiSequent createSemiSequent(Sequent s, boolean antec) {
MatchPathSemiSequent mp = new MatchPathSemiSequent(
createSequent(s), antec ? s.antecedent() : s.succedent(), antec);
return mp;
}
private static MatchPathSequent createSequent(Sequent s) {
return new MatchPathSequent(s);
}
public static MatchPathSemiSequent createSuccedent(Sequent sequent) {
return createSemiSequent(sequent, false);
}
public static MatchPathSemiSequent createAntecedent(Sequent sequent) {
return createSemiSequent(sequent, true);
}
public abstract int depth();
public static class MatchPathTerm extends MatchPath<Term> {
public MatchPathTerm(MatchPath<?> parent, Term unit, int pos) {
super(parent, unit, pos);
}
@Override
public int depth() {
return getTerm().depth();
}
}
public static class MatchPathSequent extends MatchPath<Sequent> {
public MatchPathSequent(Sequent unit) {
super(null, unit, ROOT);
}
@Override
public int depth() {
return 0;
}
}
public static class MatchPathSemiSequent extends MatchPath<Semisequent> {
public MatchPathSemiSequent(MatchPathSequent parent, Semisequent unit, boolean antec) {
super(parent, unit, antec ? POSITION_ANTECEDENT : POSITION_SUCCEDENT);
}
@Override
public int depth() {
return 1;
}
}
}
package edu.kit.formal.psdb.termmatcher;
import org.antlr.v4.runtime.ParserRuleContext;
import java.util.Stack;
public abstract class MatchPatternDualVisitor<T, S> extends MatchPatternBaseVisitor<T> {
private Stack<S> stack = new Stack<>();
public final T accept(MatchPatternParser.TermPatternContext ctx, S arg) {
public final T accept(ParserRuleContext ctx, S arg) {
stack.push(arg);
T t = ctx.accept(this);
stack.pop();
......@@ -13,10 +15,20 @@ public abstract class MatchPatternDualVisitor<T, S> extends MatchPatternBaseVisi
}
@Override
public final T visitSequentPattern(MatchPatternParser.SequentPatternContext ctx) {
return visitSequentPattern(ctx, stack.peek());
public T visitSequentAnywhere(MatchPatternParser.SequentAnywhereContext ctx) {
return visitSequentAnywhere(ctx, stack.peek());
}
public abstract T visitSequentAnywhere(MatchPatternParser.SequentAnywhereContext ctx, S peek);
@Override
public T visitSequentArrow(MatchPatternParser.SequentArrowContext ctx) {
return visitSequentArrow(ctx, stack.peek());
}
public abstract T visitSequentArrow(MatchPatternParser.SequentArrowContext ctx, S peek);
@Override
public final T visitSemiSeqPattern(MatchPatternParser.SemiSeqPatternContext ctx) {
return visitSemiSeqPattern(ctx, stack.peek());
......@@ -66,8 +78,6 @@ public abstract class MatchPatternDualVisitor<T, S> extends MatchPatternBaseVisi
protected abstract T visitNumber(MatchPatternParser.NumberContext ctx, S peek);
protected abstract T visitSequentPattern(MatchPatternParser.SequentPatternContext ctx, S peek);
@Override
public T visitPlusMinus(MatchPatternParser.PlusMinusContext ctx) {
return visitPlusMinus(ctx, stack.peek());
......
......@@ -2,20 +2,14 @@ package edu.kit.formal.psdb.termmatcher;
import de.uka.ilkd.key.logic.Semisequent;
import de.uka.ilkd.key.logic.Sequent;
import de.uka.ilkd.key.logic.SequentFormula;
import de.uka.ilkd.key.logic.Term;
import edu.kit.formal.psdb.termmatcher.MatchPatternParser.SemiSeqPatternContext;
import org.antlr.v4.runtime.CharStream;
import org.antlr.v4.runtime.CharStreams;
import org.antlr.v4.runtime.CommonTokenStream;
import org.key_project.util.collection.ImmutableList;
import java.util.*;
import java.util.stream.Collectors;
import static edu.kit.formal.psdb.termmatcher.MatchPatternParser.SequentPatternContext;
import static edu.kit.formal.psdb.termmatcher.MatchPatternParser.TermPatternContext;
import static edu.kit.formal.psdb.termmatcher.MatcherImpl.*;
/**
* A facade for capturing everthing we want to do with matchers.
......@@ -26,11 +20,13 @@ import static edu.kit.formal.psdb.termmatcher.MatcherImpl.*;
public class MatcherFacade {
public static Matchings matches(String pattern, Term keyTerm) {
MatcherImpl matcher = new MatcherImpl();
matcher.setCatchAll(false);
MatchPatternParser mpp = getParser(pattern);
TermPatternContext ctx = mpp.termPattern();
return matcher.accept(ctx, MatchPath.createRoot(keyTerm));
}
/**
* Returns a {@link MatchPatternParser} for the given input pattern.
*
......@@ -50,12 +46,16 @@ public class MatcherFacade {
*
* @param pattern Semisequent pattern e.g. f(x), f(x)
* @param semiSeq Concrete KeY Semisequent
* @param catchAll
* @return Matchings
*/
public static Matchings matches(String pattern, Semisequent semiSeq) {
public static Matchings matches(String pattern, Semisequent semiSeq, boolean catchAll) {
MatchPatternParser mpp = getParser(pattern);
SemiSeqPatternContext ctx = mpp.semiSeqPattern();
return matches(ctx, semiSeq);
MatcherImpl matcher = new MatcherImpl();
matcher.setCatchAll(catchAll);
Matchings m = matcher.accept(ctx, new MatchPath.MatchPathSemiSequent(null, semiSeq, true));
return m;
}
......@@ -66,122 +66,24 @@ public class MatcherFacade {
* @param sequent
* @return
*/
public static Matchings matches(String pattern, Sequent sequent) {
MatcherImpl matcher = new MatcherImpl();
public static Matchings matches(String pattern, Sequent sequent, boolean catchAll) {
MatchPatternParser mpp = getParser(pattern);
SequentPatternContext ctx = mpp.sequentPattern();
Semisequent antec = sequent.antecedent();
Semisequent succ = sequent.succedent();
Matchings newMatching;
if (ctx.anywhere != null) {
//in this case we have a pattern without "==>"
SemiSeqPatternContext patternCtx = ctx.anywhere;
if (antec.isEmpty() & succ.isEmpty()) {
//Sonderbehandlung, falls beide EmptyMatch-> kein Thema aber ansonsten bevorzugung von Varzuweisungen
Matchings antecMatches = matches(patternCtx, antec);
Matchings succMatches = matches(patternCtx, succ);
Matchings ret = compareMatchings(antecMatches, succMatches);
newMatching = ret;
} else {
if (antec.isEmpty()) {
newMatching = matches(patternCtx, succ);
} else {
newMatching = matches(patternCtx, antec);
}
}
} else {
SemiSeqPatternContext antecPattern = ctx.antec;
SemiSeqPatternContext succPattern = ctx.succ;
Matchings mAntec = antecPattern == null ? MatcherImpl.EMPTY_MATCH : matches(antecPattern, antec);
Matchings mSucc = succPattern == null ? MatcherImpl.EMPTY_MATCH : matches(succPattern, succ);
newMatching = MatcherImpl.reduceConform(mAntec, mSucc);
}
return newMatching;
MatcherImpl matcher = new MatcherImpl();
matcher.setCatchAll(catchAll);
Matchings m = matcher.accept(ctx, new MatchPath.MatchPathSequent(sequent));
return m;
}
//BiMap<Pair<SequentFormula, MatchPatternParser.TermPatternContext>, Matchings> formulaToMatchingInfo,
/**
* Reduce all matches to only compatible matchings
* Like {@link #matches(String, Sequent)} but allows to use
* MatcherImpl#isCatchAll.
*
* @param allMatches
* @param pattern
* @param sequent
* @return
*/
private static List<MatchInfo> reduceCompatibleMatches(List<List<MatchInfo>> allMatches) {
if (allMatches.size() == 1) {
return allMatches.get(0);
}
if (allMatches.size() == 2) {
return MatcherImpl.reduceConform(allMatches.get(0), allMatches.get(1));
} else {
List<MatchInfo> tmp = MatcherImpl.reduceConform(allMatches.get(0), allMatches.get(1));
List<List<MatchInfo>> list = new ArrayList<>();
list.add(tmp);
list.addAll(allMatches.subList(2, allMatches.size()));
return reduceCompatibleMatches(list);
}
}
public static Matchings matches(SemiSeqPatternContext pattern, Semisequent semiSeq) {
MatcherImpl matcher = new MatcherImpl();
ImmutableList<SequentFormula> allSequentFormulas = semiSeq.asList();
List<TermPatternContext> termPatternContexts = pattern.termPattern();
List<List<MatcherImpl.MatchInfo>> allMatches = new ArrayList<>();
for (TermPatternContext termPatternContext : termPatternContexts) {
List<MatchInfo> m = new ArrayList<>();
for (SequentFormula form : allSequentFormulas) {
Matchings temp = matcher.accept(termPatternContext,
MatchPath.createRoot(form.formula()));
for (Map<String, MatchPath> match : temp) {
m.add(new MatchInfo(match, Collections.singleton(form)));
}
}
allMatches.add(m);
}
List<MatchInfo> res = reduceCompatibleMatches(allMatches);
if (res == null)
return NO_MATCH;
Set<Map<String, MatchPath>> resMap = res.stream()
.map(el -> el.matching)
.collect(Collectors.toSet());
//remove dups?
Matchings resMatchings = new Matchings();
resMatchings.addAll(resMap);
return resMatchings;
}
private static Matchings compareMatchings(Matchings antecMatches, Matchings succMatches) {
if (antecMatches.equals(EMPTY_MATCH) && succMatches.equals(EMPTY_MATCH)) {
return MatcherImpl.EMPTY_MATCH;
}
if (antecMatches.equals(NO_MATCH)) return succMatches;
if (succMatches.equals(NO_MATCH)) return antecMatches;
//bevorzuge antecmatch atm
if (!antecMatches.equals(EMPTY_MATCH)) {
return antecMatches;
} else {
return succMatches;
}
public static Matchings matches(String pattern, Sequent sequent) {
return matches(pattern, sequent,false);
}
}
package edu.kit.formal.psdb.termmatcher;
import com.google.common.collect.Sets;
import de.uka.ilkd.key.logic.Semisequent;
import de.uka.ilkd.key.logic.Sequent;
import de.uka.ilkd.key.logic.SequentFormula;
import de.uka.ilkd.key.logic.Term;
import edu.kit.formal.psdb.gui.controls.Utils;
import lombok.Getter;
import lombok.Setter;
import org.antlr.v4.runtime.CommonToken;
import org.apache.commons.lang.NotImplementedException;
import org.key_project.util.collection.ImmutableArray;
import org.key_project.util.collection.ImmutableList;
import java.util.*;
import java.util.stream.IntStream;
......@@ -19,16 +25,28 @@ import java.util.stream.Stream;
class MatcherImpl extends MatchPatternDualVisitor<Matchings, MatchPath> {
static final Matchings NO_MATCH = new Matchings();
static final Matchings EMPTY_MATCH = Matchings.singleton("EMPTY_MATCH", null);
static final Map<String, MatchPath> EMPTY_VARIABLE_ASSIGNMENT = EMPTY_MATCH.first();
private List<Integer> currentPosition = new ArrayList<>();
/**
* If true, we assume every term in the pattern has a binder.
* The binding names are generated.
*
* @see #handleBindClause(MatchPatternParser.BindClauseContext, MatchPath, Matchings)
*/
@Getter
@Setter
private boolean catchAll = false;
/*
* Reduce two matchinfos
*
* @param m1
* @param m2
* @return
*/
*
protected static List<MatchInfo> reduceConform(List<MatchInfo> m1, List<MatchInfo> m2) {
if (m1 == null || m2 == null) return null; //"null" is equivalent to NO_MATCH
......@@ -52,6 +70,7 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, MatchPath> {
}
return oneMatch ? res : null;
}
*/
private static HashMap<String, MatchPath> reduceConform(Map<String, MatchPath> h1, Map<String, MatchPath> h2) {
......@@ -98,18 +117,6 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, MatchPath> {
return oneMatch ? m3 : NO_MATCH;
}
/**
* Visit a semisequent pattern f(x), f(y)
*
* @param ctx
* @param peek
* @return
*/
@Override
protected Matchings visitSemiSeqPattern(MatchPatternParser.SemiSeqPatternContext ctx, MatchPath peek) {
return null;
}
/**
* Visit '_'
*
......@@ -193,7 +200,7 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, MatchPath> {
* @return
*/
private Matchings handleBindClause(MatchPatternParser.BindClauseContext ctx, MatchPath t, Matchings m) {
if (ctx == null) {
if (!catchAll && ctx == null) {
return m;
}
......@@ -201,7 +208,11 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, MatchPath> {
return m;
}
final String name = ctx.SID().getText();
// double ? for anonymous matchings
final String name = ctx != null
? ctx.SID().getText()
: "??" + Utils.getRandomName();
Matchings mNew = Matchings.singleton(name, t);
return this.reduceConform(m, mNew);
}
......@@ -262,11 +273,139 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, MatchPath> {
* @return
*/
@Override
protected Matchings visitSequentPattern(MatchPatternParser.SequentPatternContext ctx, MatchPath peek) {
throw new NotImplementedException("use the facade!");
public Matchings visitSequentAnywhere(MatchPatternParser.SequentAnywhereContext ctx, MatchPath peek) {
MatchPath<Sequent> seq = peek;
Sequent sequent = seq.getTerm();
MatchPatternParser.SemiSeqPatternContext patternCtx = ctx.anywhere;
Matchings ret = new Matchings();
Matchings antecMatches = accept(patternCtx, MatchPath.createAntecedent(sequent));
Matchings succMatches = accept(patternCtx, MatchPath.createSuccedent(sequent));
//if(!antecMatches.equals(EMPTY_MATCH))
ret.addAll(antecMatches);
//if(!succMatches.equals(EMPTY_MATCH))
ret.addAll(succMatches);
//if (ret.contains(EMPTY_VARIABLE_ASSIGNMENT) && ret.size() > 1)
// ret.remove(EMPTY_VARIABLE_ASSIGNMENT); // remove empty match if there is an other match
return ret;
}
@Override
public Matchings visitSequentArrow(MatchPatternParser.SequentArrowContext ctx, MatchPath peek) {
MatchPath<Sequent> seq = peek;
Sequent sequent = seq.getTerm();
//NPE
Matchings mAntec = ctx.antec != null
? accept(ctx.antec, MatchPath.createSemiSequent(sequent, true))
: EMPTY_MATCH;
Matchings mSucc = ctx.succ != null
? accept(ctx.succ, MatchPath.createSemiSequent(sequent, false))
: EMPTY_MATCH;
return MatcherImpl.reduceConform(mAntec, mSucc);
}
/**
* Visit a semisequent pattern f(x), f(y)
*
* @param ctx
* @param peek
* @return
*/
@Override
protected Matchings visitSemiSeqPattern(MatchPatternParser.SemiSeqPatternContext ctx, MatchPath peek) {
Semisequent ss = (Semisequent) peek.getTerm();
if (ss.isEmpty()) {
return ctx.termPattern().size() == 0
? EMPTY_MATCH
: NO_MATCH;
}
ImmutableList<SequentFormula> allSequentFormulas = ss.asList();
List<MatchPatternParser.TermPatternContext> patterns = ctx.termPattern();
HashMap<MatchPatternParser.TermPatternContext, Map<SequentFormula, Matchings>>
map = new HashMap<>();
//cartesic product of pattern and top-level terms
for (MatchPatternParser.TermPatternContext tctx : patterns) {
int i = 0;
map.put(tctx, new HashMap<>());
for (SequentFormula form : allSequentFormulas) {
Matchings temp = accept(tctx, new MatchPath.MatchPathTerm(peek, form.formula(), i++));
if (!temp.equals(NO_MATCH))
map.get(tctx).put(form, temp);
}
}
List<Matchings> matchings = new ArrayList<>();
reduceDisjoint(map, patterns, matchings);
Matchings ret = new Matchings();
matchings.stream()//.filter(x -> !x.equals(EMPTY_MATCH))
.forEach(ret::addAll);
return ret;
}
/**
* @param map
* @param patterns
* @param matchings
*/
private void reduceDisjoint(HashMap<MatchPatternParser.TermPatternContext, Map<SequentFormula, Matchings>> map,
List<MatchPatternParser.TermPatternContext> patterns,
List<Matchings> matchings) {
reduceDisjoint(map, patterns, matchings, 0, EMPTY_MATCH, new HashSet<>());
}
/**
* @param map
* @param patterns
* @param matchings
* @param currentPatternPos
* @param ret
* @param chosenSequentFormulas
*/
private void reduceDisjoint(HashMap<MatchPatternParser.TermPatternContext, Map<SequentFormula, Matchings>> map,
List<MatchPatternParser.TermPatternContext> patterns,
List<Matchings> matchings,
int currentPatternPos,
Matchings ret,
Set<SequentFormula> chosenSequentFormulas) {
if (currentPatternPos >= patterns.size()) { // end of selection process is reached
matchings.add(ret);
return;
}
MatchPatternParser.TermPatternContext currentPattern = patterns.get(currentPatternPos);
Sets.SetView<SequentFormula> topLevelFormulas =
Sets.difference(map.get(currentPattern).keySet(), chosenSequentFormulas);
if (topLevelFormulas.size() == 0) {
return; // all top level formulas has been chosen, we have no matches left
}
for (SequentFormula formula : topLevelFormulas) { // chose a toplevel formula
// 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);
chosenSequentFormulas.add(formula); // adding the formula, so other matchings can not choose it
// recursion: choose the next matchings for the next pattern
reduceDisjoint(map, patterns, matchings,
currentPatternPos + 1, mm, chosenSequentFormulas);
chosenSequentFormulas.remove(formula); // delete the formula, so it is free to choose, again
}
}
@Override
protected Matchings visitPlusMinus(MatchPatternParser.PlusMinusContext ctx, MatchPath peek) {
return visitBinaryOperation(convert(ctx.op.getType()),
......@@ -395,17 +534,8 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, MatchPath> {
list.add(peek);
for (int i = 0; i < peek.getTerm().arity(); i++) {
subTerms(list,
new MatchPath<Term>(peek, peek.getTerm().sub(i), i));
MatchPath.createTermPath(peek, i));
}
}
public static class MatchInfo {
public Map<String, MatchPath> matching;
public Set<SequentFormula> matchedForms;
public MatchInfo(Map<String, MatchPath> m, Set<SequentFormula> f) {
matching = m;
matchedForms = f;
}
}
}
package edu.kit.formal.psdb.termmatcher;
import java.util.ArrayList;
import java.util.Map;
import java.util.TreeMap;
import com.google.common.collect.Sets;
import java.util.*;
/**
* Class Matching contains a hashmap of string to term
*/
public class Matchings extends ArrayList<Map<String, MatchPath>> {
public class Matchings extends TreeSet<Map<String, MatchPath>> {
public Matchings() {
super(new VariableAssignmentComparator());
}
public static Matchings singleton(String name, MatchPath term) {
Matchings matchings = new Matchings();
Map<String, MatchPath> va = new TreeMap<>();
......@@ -15,4 +19,73 @@ public class Matchings extends ArrayList<Map<String, MatchPath>> {
matchings.add(va);
return matchings;
}
}
class VariableAssignmentComparator implements Comparator<Map<String, MatchPath>> {
/**
* <ol>
* <li>both maps contains the same keys</li>
* <li>foreach key in lexi-order, the depth has to be greater</li>
* </ol>
*
* @return
*/
@Override
public int compare(Map<String, MatchPath> o1, Map<String, MatchPath> 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<String> 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) {