Commit d6247320 authored by Sarah Grebing's avatar Sarah Grebing

Matching of Semisequents interimstate

parent cc20826f
...@@ -4,13 +4,22 @@ import de.uka.ilkd.key.logic.Semisequent; ...@@ -4,13 +4,22 @@ import de.uka.ilkd.key.logic.Semisequent;
import de.uka.ilkd.key.logic.Sequent; import de.uka.ilkd.key.logic.Sequent;
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 edu.kit.formal.psdb.termmatcher.MatchPatternParser.SemiSeqPatternContext;
import org.antlr.v4.runtime.CharStream; import org.antlr.v4.runtime.CharStream;
import org.antlr.v4.runtime.CharStreams; import org.antlr.v4.runtime.CharStreams;
import org.antlr.v4.runtime.CommonTokenStream; import org.antlr.v4.runtime.CommonTokenStream;
import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableList;
import java.util.ArrayList; import java.util.ArrayList;
import java.util.Collections;
import java.util.HashMap;
import java.util.List; import java.util.List;
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.MatchInfo;
import static edu.kit.formal.psdb.termmatcher.MatcherImpl.NO_MATCH;
/** /**
* A facade for capturing everthing we want to do with matchers. * A facade for capturing everthing we want to do with matchers.
...@@ -22,7 +31,7 @@ public class MatcherFacade { ...@@ -22,7 +31,7 @@ public class MatcherFacade {
public static Matchings matches(String pattern, Term keyTerm) { public static Matchings matches(String pattern, Term keyTerm) {
MatcherImpl matcher = new MatcherImpl(); MatcherImpl matcher = new MatcherImpl();
MatchPatternParser mpp = getParser(pattern); MatchPatternParser mpp = getParser(pattern);
MatchPatternParser.TermPatternContext ctx = mpp.termPattern(); TermPatternContext ctx = mpp.termPattern();
return matcher.accept(ctx, keyTerm); return matcher.accept(ctx, keyTerm);
} }
...@@ -50,64 +59,66 @@ public class MatcherFacade { ...@@ -50,64 +59,66 @@ public class MatcherFacade {
public static Matchings matches(String pattern, Semisequent semiSeq) { public static Matchings matches(String pattern, Semisequent semiSeq) {
MatchPatternParser mpp = getParser(pattern); MatchPatternParser mpp = getParser(pattern);
MatchPatternParser.SemiSeqPatternContext ctx = mpp.semiSeqPattern(); SemiSeqPatternContext ctx = mpp.semiSeqPattern();
return matches(ctx, semiSeq); return matches(ctx, semiSeq);
} }
public static Matchings matches(MatchPatternParser.SemiSeqPatternContext pattern, Semisequent semiSeq) {
public static Matchings matches(SemiSeqPatternContext pattern, Semisequent semiSeq) {
MatcherImpl matcher = new MatcherImpl(); MatcherImpl matcher = new MatcherImpl();
ImmutableList<SequentFormula> allSequentFormulas = semiSeq.asList(); ImmutableList<SequentFormula> allSequentFormulas = semiSeq.asList();
List<MatchPatternParser.TermPatternContext> termPatternContexts = pattern.termPattern(); List<TermPatternContext> termPatternContexts = pattern.termPattern();
List<Matchings> allMatches = new ArrayList<>(); List<List<MatcherImpl.MatchInfo>> allMatches = new ArrayList<>();
for (MatchPatternParser.TermPatternContext termPatternContext : termPatternContexts) { for (TermPatternContext termPatternContext : termPatternContexts) {
Matchings m = new Matchings(); List<MatchInfo> m = new ArrayList<>();
for (SequentFormula form : allSequentFormulas) { for (SequentFormula form : allSequentFormulas) {
Matchings temp = matcher.accept(termPatternContext, form.formula()); Matchings temp = matcher.accept(termPatternContext, form.formula());
m.addAll(temp);
for (HashMap<String, Term> match : temp) {
m.add(new MatchInfo(match, Collections.singleton(form)));
}
} }
allMatches.add(m); allMatches.add(m);
} }
Matchings res = reduceCompatibleMatches(allMatches); List<MatchInfo> res = reduceCompatibleMatches(allMatches);
System.out.println("res = " + res); System.out.println("res = " + res);
return res;
if (res == null)
return NO_MATCH;
List<HashMap<String, Term>> resMap = res.stream().map(el -> el.matching).collect(Collectors.toList());
Matchings resMatchings = new Matchings();
resMatchings.addAll(resMap);
return resMatchings;
} }
//BiMap<Pair<SequentFormula, MatchPatternParser.TermPatternContext>, Matchings> formulaToMatchingInfo,
/** /**
* Reduce all matches to only comaptible matchings * Reduce all matches to only comaptible matchings
* @param allMatches * @param allMatches
* @return * @return
*/ */
private static Matchings reduceCompatibleMatches(List<Matchings> allMatches) { private static List<MatchInfo> reduceCompatibleMatches(List<List<MatchInfo>> allMatches) {
if (allMatches.size() == 2) { if (allMatches.size() == 2) {
return MatcherImpl.reduceConform(allMatches.get(0), allMatches.get(1)); return MatcherImpl.reduceConform(allMatches.get(0), allMatches.get(1));
} else { } else {
Matchings tmp = MatcherImpl.reduceConform(allMatches.get(0), allMatches.get(1)); List<MatchInfo> tmp = MatcherImpl.reduceConform(allMatches.get(0), allMatches.get(1));
List<Matchings> list = new ArrayList<>(); List<List<MatchInfo>> list = new ArrayList<>();
list.add(tmp); list.add(tmp);
list.addAll(allMatches.subList(2, allMatches.size())); list.addAll(allMatches.subList(2, allMatches.size()));
return reduceCompatibleMatches(list); return reduceCompatibleMatches(list);
} }
} }
/**
* Filter matchings s.t. only those remain, that fit the pattern
*
* @param allCompatibelMatchings
* @param pattern
* @return
*/
private static List<Matchings> filterMatchings(List<Matchings> allCompatibelMatchings, MatchPatternParser.SemiSeqPatternContext pattern) {
List<Matchings> ret = new ArrayList<>();
List<MatchPatternParser.TermPatternContext> termPatternContexts = pattern.termPattern();
return ret;
}
/** /**
* Match a sequent pattern against a concrete sequent * Match a sequent pattern against a concrete sequent
...@@ -119,7 +130,7 @@ public class MatcherFacade { ...@@ -119,7 +130,7 @@ public class MatcherFacade {
public static Matchings matches(String pattern, Sequent sequent) { public static Matchings matches(String pattern, Sequent sequent) {
MatcherImpl matcher = new MatcherImpl(); MatcherImpl matcher = new MatcherImpl();
MatchPatternParser mpp = getParser(pattern); MatchPatternParser mpp = getParser(pattern);
MatchPatternParser.SequentPatternContext ctx = mpp.sequentPattern(); SequentPatternContext ctx = mpp.sequentPattern();
Semisequent antec = sequent.antecedent(); Semisequent antec = sequent.antecedent();
Semisequent succ = sequent.succedent(); Semisequent succ = sequent.succedent();
......
package edu.kit.formal.psdb.termmatcher; package edu.kit.formal.psdb.termmatcher;
import de.uka.ilkd.key.logic.SequentFormula;
import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.Term;
import java.util.ArrayList; import java.util.*;
import java.util.HashMap;
import java.util.Stack;
import java.util.stream.IntStream; import java.util.stream.IntStream;
import java.util.stream.Stream; import java.util.stream.Stream;
...@@ -19,6 +18,41 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, Term> { ...@@ -19,6 +18,41 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, Term> {
private Stack<Term> termStack = new Stack<>(); private Stack<Term> termStack = new Stack<>();
protected static List<MatchInfo> reduceConform(List<MatchInfo> m1, List<MatchInfo> m2) {
if (m1 == null || m2 == null) return null; //"null" is equivalent to NO_MATCH
List<MatchInfo> res = new ArrayList<>();
boolean oneMatch = false;
for (MatchInfo minfo1 : m1) {
for (MatchInfo minfo2 : m2) {
Set<SequentFormula> intersection = new HashSet<>(minfo1.matchedForms);
intersection.retainAll(minfo2.matchedForms);
if (!intersection.isEmpty()) continue;
HashMap<String, Term> h3 = reduceConform(minfo1.matching, minfo2.matching);
if (h3 != null) {
Set<SequentFormula> union = new HashSet<>(minfo1.matchedForms);
union.addAll(minfo2.matchedForms);
res.add(new MatchInfo(h3, union));
oneMatch = true;
}
}
}
return oneMatch ? res : null;
}
private static HashMap<String, Term> reduceConform(HashMap<String, Term> h1, HashMap<String, Term> h2) {
HashMap<String, Term> h3 = new HashMap<>(h1);
for (String s1 : h3.keySet()) {
if (h2.containsKey(s1) && !h2.get(s1).equals(h1.get(s1))) {
return null;
}
}
h3.putAll(h2);
return h3;
}
/** /**
* Reduce the matchings by eliminating non-compatible matchings. * Reduce the matchings by eliminating non-compatible matchings.
* For example: * For example:
...@@ -53,17 +87,6 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, Term> { ...@@ -53,17 +87,6 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, Term> {
} }
}*/ }*/
private static HashMap<String, Term> reduceConform(HashMap<String, Term> h1, HashMap<String, Term> h2) {
HashMap<String, Term> h3 = new HashMap<>(h1);
for (String s1 : h3.keySet()) {
if (h2.containsKey(s1) && !h2.get(s1).equals(h1.get(s1))) {
return null;
}
}
h3.putAll(h2);
return h3;
}
/** /**
* Visit '_' * Visit '_'
* *
...@@ -173,6 +196,16 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, Term> { ...@@ -173,6 +196,16 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, Term> {
subTerms(list, s); subTerms(list, s);
} }
} }
public static class MatchInfo {
public HashMap<String, Term> matching;
public Set<SequentFormula> matchedForms;
public MatchInfo(HashMap<String, Term> m, Set<SequentFormula> f) {
matching = m;
matchedForms = f;
}
}
} }
/** /**
......
...@@ -42,8 +42,8 @@ public class MatcherFacadeTest { ...@@ -42,8 +42,8 @@ public class MatcherFacadeTest {
shouldMatch("f(a)", "f(a)"); shouldMatch("f(a)", "f(a)");
shouldMatchForm("pred(a)", "_"); shouldMatchForm("pred(a)", "_");
shouldMatchForm("pred(a)", "pred(?X)", "[{?X=a}]"); shouldMatchForm("pred(a)", "pred(?X)", "[{?X=a}]");
shouldMatchSemiSeq("pred(a), pred(b) ==>", "pred(?X), pred(?Y)"); shouldMatchSemiSeq("pred(a), pred(b) ==>", "pred(?X), pred(?Y)", "[{?X=a, ?Y=b}, {?X=b, ?Y=a}]");
shouldMatchSemiSeq("pred(a), pred(b) ==>", "pred(?X), pred(?X)", "[{?X=a}, {?X=b}]"); shouldMatchSemiSeq("pred(a), pred(b) ==>", "pred(?X), pred(?X)", "[]");
shouldMatchSemiSeq("pred(a), pred(f(a)) ==>", "pred(?X), pred(f(?X))", "[{?X=a}]"); shouldMatchSemiSeq("pred(a), pred(f(a)) ==>", "pred(?X), pred(f(?X))", "[{?X=a}]");
shouldMatchSemiSeq("pred(b), pred(f(a)) ==>", "pred(?X), pred(f(?X))", "[]"); shouldMatchSemiSeq("pred(b), pred(f(a)) ==>", "pred(?X), pred(f(?X))", "[]");
// shouldMatchSemiSeq("pred(a), pred(b) ==> qpred(a,b)", "pred(a), pred(b)"); // shouldMatchSemiSeq("pred(a), pred(b) ==> qpred(a,b)", "pred(a), pred(b)");
...@@ -85,12 +85,6 @@ public class MatcherFacadeTest { ...@@ -85,12 +85,6 @@ public class MatcherFacadeTest {
Assert.assertEquals(exp, m.toString()); Assert.assertEquals(exp, m.toString());
} }
private void shouldMatchSemiSeq(String s, String s1) throws ParserException {
Sequent term = parseSeq(s);
Matchings m = MatcherFacade.matches(s1, term);
System.out.println(m);
}
private void shouldMatchSemiSeq(String s, String s1, String exp) throws ParserException { private void shouldMatchSemiSeq(String s, String s1, String exp) throws ParserException {
Sequent term = parseSeq(s); Sequent term = parseSeq(s);
Matchings m = MatcherFacade.matches(s1, term); Matchings m = MatcherFacade.matches(s1, term);
...@@ -133,4 +127,10 @@ public class MatcherFacadeTest { ...@@ -133,4 +127,10 @@ public class MatcherFacadeTest {
Reader in = new StringReader(s); Reader in = new StringReader(s);
return dtp.parseSeq(in, services, namespace, abbrev); return dtp.parseSeq(in, services, namespace, abbrev);
} }
private void shouldMatchSemiSeq(String s, String s1) throws ParserException {
Sequent term = parseSeq(s);
Matchings m = MatcherFacade.matches(s1, term);
System.out.println(m);
}
} }
\ No newline at end of file
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