From da98f424bce5af8eda5a49efc595a8864a9b88c2 Mon Sep 17 00:00:00 2001 From: Sarah Grebing Date: Fri, 1 Jun 2018 12:19:41 +0200 Subject: [PATCH] bugfix matcher --- DockFX/build.gradle | 32 + .../psdbg/parser/ast/MatchExpression.java | 2 +- .../formal/psdbg/termmatcher/MatchPattern.g4 | 88 --- .../termmatcher/MatchPatternDualVisitor.java | 183 ----- .../psdbg/termmatcher/MatcherFacade.java | 108 --- .../formal/psdbg/termmatcher/MatcherImpl.java | 657 ------------------ .../formal/psdbg/termmatcher/Matchings.java | 94 --- .../psdbg/termmatcher/OwnFunctionContext.java | 37 - .../iti/formal/psdbg/termmatcher/Utils.java | 51 -- .../psdbg/termmatcher/mp/MatchPath.java | 179 ----- .../psdbg/termmatcher/mp/MatchPathFacade.java | 64 -- .../psdbg/termmatcher/package-info.java | 4 - .../psdbg/termmatcher/MatcherFacadeTest.java | 310 --------- .../psdbg/termmatcher/TestComplexMatch.java | 38 - .../psdbg/termmatcher/TestUpdateMatch.java | 37 - .../formal/psdbg/termmatcher/goodmatches.txt | 2 - .../psdbg/termmatcher/javacomplex/Simple.java | 41 -- .../psdbg/termmatcher/javacomplex/project.key | 2 - .../psdbg/termmatcher/javasimple/Test.java | 17 - .../psdbg/termmatcher/javasimple/project.key | 2 - .../kit/iti/formal/psdbg/termmatcher/test.key | 41 -- .../interpreter/matcher/KeyMatcherFacade.java | 21 +- .../interpreter/matcher/KeyTermMatcher.java | 5 +- .../matcher/KeyMatcherFacadeTest.java | 9 + ui/build.gradle | 2 + .../gui/controls/FileReloadingService.java | 2 +- .../formal/psdbg/gui/controls/ProofTree.java | 7 +- .../psdbg/gui/controls/ScriptController.java | 6 +- .../psdbg/examples/contraposition/script.kps | 17 +- 29 files changed, 80 insertions(+), 1978 deletions(-) delete mode 100644 matcher/src/main/antlr/edu/kit/iti/formal/psdbg/termmatcher/MatchPattern.g4 delete mode 100644 matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/MatchPatternDualVisitor.java delete mode 100644 matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/MatcherFacade.java delete mode 100644 matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/MatcherImpl.java delete mode 100644 matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/Matchings.java delete mode 100644 matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/OwnFunctionContext.java delete mode 100644 matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/Utils.java delete mode 100644 matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/mp/MatchPath.java delete mode 100644 matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/mp/MatchPathFacade.java delete mode 100644 matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/package-info.java delete mode 100644 matcher/src/test/java/edu/kit/iti/formal/psdbg/termmatcher/MatcherFacadeTest.java delete mode 100644 matcher/src/test/java/edu/kit/iti/formal/psdbg/termmatcher/TestComplexMatch.java delete mode 100644 matcher/src/test/java/edu/kit/iti/formal/psdbg/termmatcher/TestUpdateMatch.java delete mode 100644 matcher/src/test/resources/edu/kit/iti/formal/psdbg/termmatcher/goodmatches.txt delete mode 100644 matcher/src/test/resources/edu/kit/iti/formal/psdbg/termmatcher/javacomplex/Simple.java delete mode 100644 matcher/src/test/resources/edu/kit/iti/formal/psdbg/termmatcher/javacomplex/project.key delete mode 100644 matcher/src/test/resources/edu/kit/iti/formal/psdbg/termmatcher/javasimple/Test.java delete mode 100644 matcher/src/test/resources/edu/kit/iti/formal/psdbg/termmatcher/javasimple/project.key delete mode 100644 matcher/src/test/resources/edu/kit/iti/formal/psdbg/termmatcher/test.key diff --git a/DockFX/build.gradle b/DockFX/build.gradle index 8580ab13..082f7000 100644 --- a/DockFX/build.gradle +++ b/DockFX/build.gradle @@ -1,2 +1,34 @@ group = 'org.dockfx' description = 'DockFX' + +// apply plugin: 'io.franzbecker.gradle-lombok' +//apply plugin: 'java' +//apply plugin: 'java-library' +//apply plugin: 'idea' + +/*sourceCompatibility = 1.8 +targetCompatibility = 1.8 +tasks.withType(JavaCompile) { + options.encoding = 'UTF-8' +} + +repositories { + mavenLocal() + maven { url "http://repo.maven.apache.org/maven2" } + maven { url "http://dl.bintray.com/jerady/maven" } + maven { url "https://oss.sonatype.org/content/repositories/snapshots/" } +} + + +dependencies { + compile group: 'commons-cli', name: 'commons-cli', version: '1.4' + compile group: 'com.google.guava', name: 'guava', version: '25.0-jre' + compile group: 'commons-io', name: 'commons-io', version: '2.6' + compile group: 'commons-lang', name: 'commons-lang', version: '2.6' + compile group: 'org.apache.logging.log4j', name: 'log4j-api', version: '2.11.0' + compile group: 'org.apache.logging.log4j', name: 'log4j-core', version: '2.11.0' + testCompile group: 'junit', name: 'junit', version: '4.12' + //compileOnly group: 'org.projectlombok', name: 'lombok', version: '1.16.20' + compileOnly files("$rootDir/lombok-edge.jar") +}*/ + diff --git a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/MatchExpression.java b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/MatchExpression.java index 43e08c4e..1a437dfd 100644 --- a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/MatchExpression.java +++ b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/MatchExpression.java @@ -41,7 +41,7 @@ import lombok.Data; public class MatchExpression extends Expression { //private Signature signature = new Signature(); private Expression pattern; - private boolean isDerivable; + private boolean isDerivable = false; @Deprecated private Expression derivableTerm; diff --git a/matcher/src/main/antlr/edu/kit/iti/formal/psdbg/termmatcher/MatchPattern.g4 b/matcher/src/main/antlr/edu/kit/iti/formal/psdbg/termmatcher/MatchPattern.g4 deleted file mode 100644 index 809f04f9..00000000 --- a/matcher/src/main/antlr/edu/kit/iti/formal/psdbg/termmatcher/MatchPattern.g4 +++ /dev/null @@ -1,88 +0,0 @@ -grammar MatchPattern; - -/* Examples for testing - -f(x) -f(x,y,g(y)) -X -?Y -_ -... -f(... ?X ...) -f(..., ?X) -f(..., ...?X...) -f(..., ... g(x) ...) -f(_, x, _, y, ... y ...) -*/ - -sequentPattern : antec=semiSeqPattern? ARROW succ=semiSeqPattern? #sequentArrow - | anywhere=semiSeqPattern #sequentAnywhere - ; - -semiSeqPattern : termPattern (',' termPattern)*; - -termPattern : - '(' quantifier=(EXISTS|FORALL) boundVars+=(SID|ID|DONTCARE)+ skope=termPattern ')' bindClause? #quantForm - | termPattern MUL termPattern #mult - | termPattern op=(DIV|MOD) termPattern #divMod - | termPattern op=(PLUS|MINUS) termPattern #plusMinus - | termPattern op=(LE|GE|LEQ|GEQ) termPattern #comparison - | termPattern op=(NEQ|EQ) termPattern #equality - | termPattern AND termPattern #and - | termPattern OR termPattern #or - | termPattern IMP termPattern #impl - | termPattern XOR termPattern #xor - | termPattern EQUIV termPattern #equivalence - | MINUS termPattern #exprNegate - | NOT termPattern #exprNot - | '(' termPattern ')' bindClause? #exprParen - | func=ID ( '(' termPattern (',' termPattern)* ')')? bindClause? #function - | DONTCARE bindClause? #dontCare - //| STARDONTCARE #starDontCare - | SID #schemaVar - | STARDONTCARE termPattern STARDONTCARE #anywhere - | DIGITS #number - // not working because of ambigue | left=termPattern op=(PLUS|MINUS|MUL|LE|GE|LEQ|GEQ|NEQ|EQ| AND|OR|IMP) right=termPattern #binaryOperation - ; - -/* -f(x), f(x,y,g(y)), X, ?Y, _, ..., f(... ?X ...), f(..., ?X), f(..., ...?X...), f(..., ... g(x) ...), f(_, x, _, y, ... y ...) -*/ - -bindClause : ('\\as' | ':') SID; - -DONTCARE: '?' | '_' | '█'; -DIGITS : DIGIT+ ; -fragment DIGIT : [0-9] ; - -ARROW : '⇒' | '==>'; -STARDONTCARE: '...' | '…'; -PLUS : '+' ; -MINUS : '-' ; -MUL : '*' ; -DIV : '/' ; -EQ : '=' ; -NEQ : '!=' ; -GEQ : '>=' ; -LEQ : '<=' ; -EQUIV : '<->'; -GE : '>' ; -LE : '<' ; -AND : '&' ; -OR: '|' ; -IMP: '->'; -MOD:'%'; -XOR:'^'; -NOT :'!'; -FORALL: '\\forall' | '∀'; -EXISTS: '\\exists'; -SID: '?' [_a-zA-Z0-9\\]+ ; -ID : [a-zA-Z\\_] ([_a-zA-Z0-9\\])* - | 'update-application' - | 'parallel-upd' - | 'elem-update' - ; - - -COMMENT: '//' ~[\n\r]* -> channel(HIDDEN); -WS: [\n\f\r\t ] -> channel(HIDDEN); diff --git a/matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/MatchPatternDualVisitor.java b/matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/MatchPatternDualVisitor.java deleted file mode 100644 index 01db89f7..00000000 --- a/matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/MatchPatternDualVisitor.java +++ /dev/null @@ -1,183 +0,0 @@ -package edu.kit.iti.formal.psdbg.termmatcher; - -import org.antlr.v4.runtime.ParserRuleContext; - -import java.util.Stack; - -public abstract class MatchPatternDualVisitor extends MatchPatternBaseVisitor { - private Stack stack = new Stack<>(); - - public final T accept(ParserRuleContext ctx, S arg) { - stack.push(arg); - T t = ctx.accept(this); - stack.pop(); - return t; - } - - @Override - 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 T visitQuantForm(MatchPatternParser.QuantFormContext ctx) { - return visitQuantForm(ctx, stack.peek()); - } - - public abstract T visitQuantForm(MatchPatternParser.QuantFormContext ctx, S peek); - - @Override - public final T visitSemiSeqPattern(MatchPatternParser.SemiSeqPatternContext ctx) { - return visitSemiSeqPattern(ctx, stack.peek()); - } - - protected abstract T visitSemiSeqPattern(MatchPatternParser.SemiSeqPatternContext ctx, S peek); - - @Override - public T visitNumber(MatchPatternParser.NumberContext ctx) { - return visitNumber(ctx, stack.peek()); - } - - @Override - public final T visitDontCare(MatchPatternParser.DontCareContext ctx) { - return visitDontCare(ctx, stack.peek()); - } - - public abstract T visitDontCare(MatchPatternParser.DontCareContext ctx, S peek); - - /*@Override - public final T visitStartDontCare(MatchPatternParser.StarDontCareContext ctx) { - return visitStartDontCare(ctx, stack.peek()); - } - - protected abstract T visitStartDontCare(MatchPatternParser.StartDontCareContext ctx, S peek); -*/ - @Override - public final T visitSchemaVar(MatchPatternParser.SchemaVarContext ctx) { - return visitSchemaVar(ctx, stack.peek()); - } - - protected abstract T visitSchemaVar(MatchPatternParser.SchemaVarContext ctx, S peek); - - @Override - public final T visitFunction(MatchPatternParser.FunctionContext ctx) { - return visitFunction(ctx, stack.peek()); - } - - @Override - public final T visitAnywhere(MatchPatternParser.AnywhereContext ctx) { - return visitAnywhere(ctx, stack.peek()); - } - - protected abstract T visitAnywhere(MatchPatternParser.AnywhereContext ctx, S peek); - - protected abstract T visitFunction(MatchPatternParser.FunctionContext ctx, S peek); - - protected abstract T visitNumber(MatchPatternParser.NumberContext ctx, S peek); - - @Override - public T visitPlusMinus(MatchPatternParser.PlusMinusContext ctx) { - return visitPlusMinus(ctx, stack.peek()); - } - - - protected abstract T visitPlusMinus(MatchPatternParser.PlusMinusContext ctx, S peek); - - @Override - public T visitMult(MatchPatternParser.MultContext ctx) { - return visitMult(ctx, stack.peek()); - } - - protected abstract T visitMult(MatchPatternParser.MultContext ctx, S peek); - - @Override - public T visitComparison(MatchPatternParser.ComparisonContext ctx) { - return visitComparison(ctx, stack.peek()); - } - - protected abstract T visitComparison(MatchPatternParser.ComparisonContext ctx, S peek); - - @Override - public T visitOr(MatchPatternParser.OrContext ctx) { - return visitOr(ctx, stack.peek()); - } - - protected abstract T visitOr(MatchPatternParser.OrContext ctx, S peek); - - @Override - public T visitExprNot(MatchPatternParser.ExprNotContext ctx) { - return visitExprNot(ctx, stack.peek()); - } - - public abstract T visitExprNot(MatchPatternParser.ExprNotContext ctx, S peek); - - @Override - public T visitExprNegate(MatchPatternParser.ExprNegateContext ctx) { - return visitExprNegate(ctx, stack.peek()); - } - - public abstract T visitExprNegate(MatchPatternParser.ExprNegateContext ctx, S peek); - - @Override - public T visitExprParen(MatchPatternParser.ExprParenContext ctx) { - return visitExprParen(ctx, stack.peek()); - } - - public abstract T visitExprParen(MatchPatternParser.ExprParenContext ctx, S peek); - - - @Override - public T visitImpl(MatchPatternParser.ImplContext ctx) { - return visitImpl(ctx, stack.peek()); - } - - protected abstract T visitImpl(MatchPatternParser.ImplContext ctx, S peek); - - @Override - public T visitDivMod(MatchPatternParser.DivModContext ctx) { - return visitDivMod(ctx, stack.peek()); - } - - protected abstract T visitDivMod(MatchPatternParser.DivModContext ctx, S peek); - - @Override - public T visitAnd(MatchPatternParser.AndContext ctx) { - return visitAnd(ctx, stack.peek()); - } - - protected abstract T visitAnd(MatchPatternParser.AndContext ctx, S peek); - - @Override - public T visitXor(MatchPatternParser.XorContext ctx) { - return visitXor(ctx, stack.peek()); - } - - protected abstract T visitXor(MatchPatternParser.XorContext ctx, S peek); - - @Override - public T visitEquality(MatchPatternParser.EqualityContext ctx) { - return visitEquality(ctx, stack.peek()); - } - - protected abstract T visitEquality(MatchPatternParser.EqualityContext ctx, S peek); - - @Override - public T visitEquivalence(MatchPatternParser.EquivalenceContext ctx) { - return visitEquivalence(ctx, stack.peek()); - } - - protected abstract T visitEquivalence(MatchPatternParser.EquivalenceContext ctx, S peek); -} - - - diff --git a/matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/MatcherFacade.java b/matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/MatcherFacade.java deleted file mode 100644 index cc911d3c..00000000 --- a/matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/MatcherFacade.java +++ /dev/null @@ -1,108 +0,0 @@ -package edu.kit.iti.formal.psdbg.termmatcher; - -import de.uka.ilkd.key.java.Services; -import de.uka.ilkd.key.logic.Semisequent; -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 edu.kit.iti.formal.psdbg.termmatcher.MatchPatternLexer; -import edu.kit.iti.formal.psdbg.termmatcher.MatchPatternParser; -import edu.kit.iti.formal.psdbg.termmatcher.mp.MatchPathFacade; -import org.antlr.v4.runtime.CharStream; -import org.antlr.v4.runtime.CharStreams; -import org.antlr.v4.runtime.CommonTokenStream; -import org.apache.logging.log4j.LogManager; -import org.apache.logging.log4j.Logger; - -import java.io.StringReader; - -/** - * A facade for capturing everything we want to do with matchers. - * - * @author Alexander Weigl - * @author S.Grebing - */ -public class MatcherFacade { - private static Logger logger = LogManager.getLogger(MatcherFacade.class); - - public static Matchings matches(String pattern, Term keyTerm, Services services) { - MatcherImpl matcher = new MatcherImpl(services); - matcher.setCatchAll(false); - - - MatchPatternParser mpp = getParser(pattern); - MatchPatternParser.TermPatternContext ctx = mpp.termPattern(); - return matcher.accept(ctx, MatchPathFacade.createRoot(keyTerm)); - } - - - /** - * Returns a {@link MatchPatternParser} for the given input pattern. - * - * @param pattern - * @return - */ - public static MatchPatternParser getParser(String pattern) { - return getParser(CharStreams.fromString(pattern)); - } - - public static MatchPatternParser getParser(CharStream stream) { - return new MatchPatternParser(new CommonTokenStream(new MatchPatternLexer(stream))); - } - - /** - * Match a semisequent against a sequent - * - * @param pattern Semisequent pattern e.g. f(x), f(x) - * @param semiSeq Concrete KeY Semisequent - * @param catchAll - * @param services - * @return Matchings - */ - public static Matchings matches(String pattern, Semisequent semiSeq, boolean catchAll, Services services) { - MatchPatternParser mpp = getParser(pattern); - MatchPatternParser.SemiSeqPatternContext ctx = mpp.semiSeqPattern(); - MatcherImpl matcher = new MatcherImpl(services); - matcher.setCatchAll(catchAll); - Matchings m = matcher.accept(ctx, MatchPathFacade.createRoot(semiSeq)); - return m; - } - - - /** - * Match a sequent pattern against a concrete sequent - * - * @param pattern e.g., f(x) ==> f(y) - * @param sequent - * @param services - * @return - */ - public static Matchings matches(String pattern, Sequent sequent, boolean catchAll, Services services) { - MatchPatternParser mpp = getParser(pattern); - MatchPatternParser.SequentPatternContext ctx = mpp.sequentPattern(); - logger.info("Matching \n" + pattern + "\n" + sequent.toString()); - if (mpp.getNumberOfSyntaxErrors() != 0) { - logger.info("Invalid pattern syntax '{}' no matches returned.", pattern); - return new Matchings(); - } - - MatcherImpl matcher = new MatcherImpl(services); - matcher.setCatchAll(catchAll); - Matchings m = matcher.accept(ctx, MatchPathFacade.create(sequent)); - return m; - } - - /** - * Like {@link #matches(String, Sequent, Services)} but allows to use - * MatcherImpl#isCatchAll. - * - * @param pattern - * @param sequent - * @param services - * @return - */ - public static Matchings matches(String pattern, Sequent sequent, Services services) { - return matches(pattern, sequent, true, services); - } -} diff --git a/matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/MatcherImpl.java b/matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/MatcherImpl.java deleted file mode 100644 index 322422c9..00000000 --- a/matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/MatcherImpl.java +++ /dev/null @@ -1,657 +0,0 @@ -package edu.kit.iti.formal.psdbg.termmatcher; - -import com.google.common.collect.Sets; -import de.uka.ilkd.key.java.Services; -import de.uka.ilkd.key.logic.*; -import de.uka.ilkd.key.logic.op.QuantifiableVariable; -import edu.kit.iti.formal.psdbg.termmatcher.MatchPatternLexer; -import edu.kit.iti.formal.psdbg.termmatcher.MatchPatternParser; -import edu.kit.iti.formal.psdbg.termmatcher.mp.MatchPath; -import lombok.Getter; -import lombok.RequiredArgsConstructor; -import lombok.Setter; -import org.antlr.v4.runtime.CommonToken; -import org.antlr.v4.runtime.Token; -import org.key_project.util.collection.ImmutableArray; - -import java.util.*; -import java.util.stream.Collectors; -import java.util.stream.IntStream; -import java.util.stream.Stream; - -import static edu.kit.iti.formal.psdbg.termmatcher.mp.MatchPathFacade.*; - -/** - * Matchpattern visitor visits the matchpatterns of case-statements - * - * @author Alexander Weigl - * @author S. Grebing - */ -@RequiredArgsConstructor -class MatcherImpl extends MatchPatternDualVisitor { - static final Matchings NO_MATCH = new Matchings(); - - static final Matchings EMPTY_MATCH = Matchings.singleton("EMPTY_MATCH", null); - - static final Map EMPTY_VARIABLE_ASSIGNMENT = EMPTY_MATCH.first(); - @Getter - private final Services services; - Random random = new Random(42L); - /* - * Reduce two matchinfos - * - * @param m1 - * @param m2 - * @return - * - protected static List reduceConform(List m1, List m2) { - if (m1 == null || m2 == null) return null; //"null" is equivalent to NO_MATCH - - List res = new ArrayList<>(); - boolean oneMatch = false; - for (MatchInfo minfo1 : m1) { - for (MatchInfo minfo2 : m2) { - - Set intersection = new HashSet<>(minfo1.matchedForms); - intersection.retainAll(minfo2.matchedForms); - if (!intersection.isEmpty()) continue; - HashMap h3 = reduceConform(minfo1.matching, minfo2.matching); - - if (h3 != null) { - Set union = new HashSet<>(minfo1.matchedForms); - union.addAll(minfo2.matchedForms); - res.add(new MatchInfo(h3, union)); - oneMatch = true; - } - } - } - return oneMatch ? res : null; - } - */ - private List 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; - - 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; - } - - /** - * 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) return m2; - if (m2 == EMPTY_MATCH) 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; - } - - - /** - * Transform a number term into an int value. - *

- * i.e. Z(1(2(3(#)))) ==> 123 - * - * @param zTerm - * @return - */ - public static int transformToNumber(Term zTerm) { - List integ = MatcherImpl.transformHelper(new ArrayList<>(), zTerm); - int dec = 10; - int output = integ.get(0); - for (int i = 1; i < integ.size(); i++) { - Integer integer = integ.get(i); - output += integer * dec; - dec = dec * 10; - } - return output; - } - - private static List transformHelper(List l, Term sub) { - if (sub.op().name().toString().equals("#")) { - return l; - } else { - l.add(Integer.parseUnsignedInt(sub.op().name().toString())); - return transformHelper(l, sub.sub(0)); - } - } - - /** - * Visit '_' - * - * @param ctx - * @param peek - * @return - */ - @Override - public Matchings visitDontCare(MatchPatternParser.DontCareContext ctx, MatchPath peek) { - if (peek != null) { - return handleBindClause(ctx.bindClause(), peek, EMPTY_MATCH); - } else { - return NO_MATCH; - } - } - - /** - * Visit a Schema Variable - * - * @param ctx - * @param peek - * @return - */ - @Override - protected Matchings visitSchemaVar(MatchPatternParser.SchemaVarContext ctx, MatchPath peek) { - if (peek != null) { - return Matchings.singleton(ctx.getText(), peek); - } else { - return NO_MATCH; - } - } - - /** - * Visit a '...'MatchPath'...' structure - * - * @param ctx - * @param peek - * @return - */ - @Override - protected Matchings visitAnywhere(MatchPatternParser.AnywhereContext ctx, MatchPath peek) { - Matchings m = new Matchings(); - subTerms((MatchPath.MPTerm) peek).forEach(sub -> { - Matchings s = accept(ctx.termPattern(), sub); - m.addAll(s); - }); - return m; - } - - /** - * Visit a function and predicate symbol without a sequent arrow - * - * @param ctx - * @param path - * @return - */ - @Override - protected Matchings visitFunction(MatchPatternParser.FunctionContext ctx, MatchPath path) { - //System.out.format("Match: %25s with %s %n", peek, ctx.toInfoString(new MatchPatternParser(null))); - String expectedFunction = ctx.func.getText(); - Term peek = ((MatchPath.MPTerm) path).getUnit(); - boolean sameName = expectedFunction.equals("?") - || expectedFunction.equals("_") - || peek.op().name().toString().equals(expectedFunction); - boolean sameArity = ctx.termPattern().size() == peek.arity(); - if (sameName && sameArity) { - Matchings m = IntStream.range(0, peek.arity()) - .mapToObj(i -> (Matchings) - accept(ctx.termPattern(i), create(path, i))) - .reduce(MatcherImpl::reduceConform) - .orElse(EMPTY_MATCH); - return handleBindClause(ctx.bindClause(), path, m); - } - return NO_MATCH; - } - - /** - * @param ctx - * @param t - * @param m - * @return - */ - private Matchings handleBindClause(MatchPatternParser.BindClauseContext ctx, MatchPath t, Matchings m) { - if (!catchAll && ctx == null) { - return m; - } - - if (m.equals(NO_MATCH)) { - return m; - } - - // double ? for anonymous matchings - final String name = ctx != null - ? ctx.SID().getText() - : "??_" + getRandomNumber(); - - Matchings mNew = Matchings.singleton(name, t); - return this.reduceConform(m, mNew); - } - - - @Override - protected Matchings visitNumber(MatchPatternParser.NumberContext ctx, MatchPath path) { - //we are at a number - Term peek = ((MatchPath.MPTerm) path).getUnit(); - if (peek.op().name().toString().equals("Z")) { - ImmutableArray subs = peek.subs(); - int transformedString = transformToNumber(peek.sub(0)); - if (Integer.parseUnsignedInt(ctx.DIGITS().getText()) == transformedString) { - return EMPTY_MATCH; - } else { - return NO_MATCH; - } - } else { - return NO_MATCH; - } - - - } - - /** - * Visit a sequent pattern 'f(x) ==> f(x)', 'f(x) ==>' or '==> f(x)' - * - * @param ctx - * @param peek - * @return - */ - @Override - public Matchings visitSequentAnywhere(MatchPatternParser.SequentAnywhereContext ctx, MatchPath peek) { - MatchPath.MPSequent seq = (MatchPath.MPSequent) peek; - MatchPatternParser.SemiSeqPatternContext patternCtx = ctx.anywhere; - - Matchings ret = new Matchings(); - Matchings antecMatches = accept(patternCtx, createAntecedent(seq)); - Matchings succMatches = accept(patternCtx, createSuccedent(seq)); - - //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.MPSequent seq = (MatchPath.MPSequent) peek; - - //NPE - Matchings mAntec = ctx.antec != null - ? accept(ctx.antec, createAntecedent(seq)) - : EMPTY_MATCH; - - Matchings mSucc = ctx.succ != null - ? accept(ctx.succ, createSuccedent(seq)) - : 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) { - MatchPath.MPSemiSequent sseq = (MatchPath.MPSemiSequent) peek; - Semisequent ss = (Semisequent) peek.getUnit(); - if (ss.isEmpty()) { - return ctx.termPattern().size() == 0 - ? EMPTY_MATCH - : NO_MATCH; - } - - List sequentFormulas = - IntStream.range(0, ss.size()) - .mapToObj(pos -> create(sseq, pos)) - .collect(Collectors.toList()); - - List patterns = ctx.termPattern(); - - HashMap> - map = new HashMap<>(); - - //cartesic product of pattern and top-level terms - for (MatchPatternParser.TermPatternContext tctx : patterns) { - map.put(tctx, new HashMap<>()); - for (MatchPath.MPSequentFormula sf : sequentFormulas) { - Matchings temp = accept(tctx, create(sf)); - if (!temp.equals(NO_MATCH)) - map.get(tctx).put(sf.getUnit(), temp); - } - } - - List matchings = new ArrayList<>(); - reduceDisjoint(map, patterns, matchings); - Matchings ret = new Matchings(); - //.filter(x -> !x.equals(EMPTY_MATCH)) - matchings.forEach(ret::addAll); - return ret; - } - - /** - * @param map - * @param patterns - * @param matchings - */ - private void reduceDisjoint(HashMap> map, - List patterns, - List 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> map, - List patterns, - List matchings, - int currentPatternPos, - Matchings ret, - Set chosenSequentFormulas) { - if (currentPatternPos >= patterns.size()) { // end of selection process is reached - matchings.add(ret); - return; - } - - MatchPatternParser.TermPatternContext currentPattern = patterns.get(currentPatternPos); - Sets.SetView 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()), - ctx.termPattern(0), ctx.termPattern(1), peek); - } - - protected Matchings visitBinaryOperation(String keyOpName, MatchPatternParser.TermPatternContext right, MatchPatternParser.TermPatternContext left, MatchPath peek) { - //create new functioncontext object and set fields accordingly - OwnFunctionContext func = new OwnFunctionContext(left); - //MatchPatternParser.FunctionContext func = new MatchPatternParser.FunctionContext(left); - //func.func = new CommonToken(MatchPatternLexer.ID, keyOpName); - - func.func = new CommonToken(MatchPatternLexer.ID, keyOpName); - //right is added as first argument, left as second - func.termPattern().add(right); - func.termPattern().add(left); - - return accept(func, peek); - } - - @Override - public Matchings visitQuantForm(MatchPatternParser.QuantFormContext ctx, MatchPath peek) { - Term toMatch = (Term) peek.getUnit(); - if (!toMatch.op().toString().equals(convert(ctx.quantifier.getType()))) { - return NO_MATCH; - } - if (toMatch.boundVars().size() != ctx.boundVars.size()) { - return NO_MATCH; - } - - Matchings match = EMPTY_MATCH; - - for (int i = 0; i < ctx.boundVars.size(); i++) { - Token qfPattern = ctx.boundVars.get(i); - QuantifiableVariable qv = toMatch.boundVars().get(i); - - if (qfPattern.getType() == MatchPatternLexer.DONTCARE) { - //match = reduceConform(match, Matchings.singleton(qfPattern.getText(), new MatchPath.MPQuantifiableVarible(peek, qv, i))); - match = reduceConform(match, EMPTY_MATCH); - continue; - } - if (qfPattern.getType() == MatchPatternLexer.SID) { - TermFactory tf = new TermFactory(new HashMap<>()); - TermBuilder tb = new TermBuilder(tf, services); - Term termQVariable = tb.var(qv); - - match = reduceConform(match, Matchings.singleton(qfPattern.getText(), - new MatchPath.MPTerm(peek, termQVariable, -i))); - } else { - if (!qv.name().toString().equals(qfPattern.getText())) { - return NO_MATCH; - } - match = reduceConform(match, EMPTY_MATCH); - } - } - - - Matchings fromTerm = accept(ctx.skope, create(peek, 0)); - Matchings retM = reduceConform(fromTerm, match); - retM.forEach(stringMatchPathMap -> { - stringMatchPathMap.forEach((s, matchPath) -> { - if (matchPath instanceof MatchPath.MPQuantifiableVariable) { - - //create term from variablename and put instead into map - } - } - - ); - }); - return handleBindClause(ctx.bindClause(), peek, retM); - } - - @Override - protected Matchings visitMult(MatchPatternParser.MultContext ctx, MatchPath peek) { - return visitBinaryOperation("mul", ctx.termPattern(0), ctx.termPattern(1), peek); - } - - @Override - protected Matchings visitComparison(MatchPatternParser.ComparisonContext ctx, MatchPath peek) { - return visitBinaryOperation(convert(ctx.op.getType()), ctx.termPattern(0), ctx.termPattern(1), peek); - } - - @Override - protected Matchings visitOr(MatchPatternParser.OrContext ctx, MatchPath peek) { - return visitBinaryOperation("or", ctx.termPattern(0), ctx.termPattern(1), peek); - } - - @Override - public Matchings visitExprNot(MatchPatternParser.ExprNotContext ctx, MatchPath peek) { - return visitBinaryOperation("not", ctx.termPattern(), ctx, peek); - } - - @Override - public Matchings visitExprNegate(MatchPatternParser.ExprNegateContext ctx, MatchPath peek) { - return visitUnaryOperation("sub", ctx.termPattern(), peek); - } - - private String convert(int op) { - switch (op) { - case MatchPatternParser.PLUS: - return "add"; - case MatchPatternParser.MINUS: - return "sub"; - case MatchPatternParser.MUL: - return "mul"; - case MatchPatternParser.DIV: - return "div"; - case MatchPatternParser.LE: - return "lt"; - case MatchPatternParser.LEQ: - return "leq"; - case MatchPatternParser.EQ: - return "equals"; - case MatchPatternParser.GE: - return "gt"; - case MatchPatternParser.GEQ: - return "geq"; - case MatchPatternParser.IMP: - return "imp"; - case MatchPatternParser.AND: - return "and"; - case MatchPatternParser.OR: - return "or"; - case MatchPatternParser.FORALL: - return "all"; - case MatchPatternParser.EXISTS: - return "exists"; - - default: - throw new UnsupportedOperationException("The operator " + op + "is not known"); - } - - - } - - - @Override - public Matchings visitExprParen(MatchPatternParser.ExprParenContext ctx, MatchPath peek) { - return handleBindClause(ctx.bindClause(), peek, accept(ctx.termPattern(), peek)); - } - - private Matchings visitUnaryOperation(String unaryOp, - MatchPatternParser.TermPatternContext ctx, - MatchPath peek) { - MatchPatternParser.FunctionContext func = new MatchPatternParser.FunctionContext(ctx); - func.termPattern().add(ctx); - func.func = new CommonToken(MatchPatternLexer.ID, unaryOp); - return accept(func, peek); - } - - @Override - protected Matchings visitImpl(MatchPatternParser.ImplContext ctx, MatchPath peek) { - return visitBinaryOperation("imp", ctx.termPattern(0), ctx.termPattern(1), peek); - } - - @Override - protected Matchings visitDivMod(MatchPatternParser.DivModContext ctx, MatchPath peek) { - return visitBinaryOperation(convert(ctx.op.getType()), ctx.termPattern(0), ctx.termPattern(1), peek); - } - - @Override - protected Matchings visitAnd(MatchPatternParser.AndContext ctx, MatchPath peek) { - return visitBinaryOperation("and", ctx.termPattern(0), ctx.termPattern(1), peek); - } - - @Override - protected Matchings visitXor(MatchPatternParser.XorContext ctx, MatchPath peek) { - return visitBinaryOperation("xor", ctx.termPattern(0), ctx.termPattern(1), peek); - } - - @Override - protected Matchings visitEquality(MatchPatternParser.EqualityContext ctx, MatchPath peek) { - return visitBinaryOperation("equals", ctx.termPattern(0), ctx.termPattern(1), peek); - } - - @Override - protected Matchings visitEquivalence(MatchPatternParser.EquivalenceContext ctx, MatchPath peek) { - return visitBinaryOperation("equiv", ctx.termPattern(0), ctx.termPattern(1), peek); - } - - private Stream subTerms(MatchPath.MPTerm peek) { - ArrayList list = new ArrayList<>(); - subTerms(list, peek); - return list.stream(); - } - - private void subTerms(ArrayList list, MatchPath.MPTerm peek) { - list.add(peek); - for (int i = 0; i < peek.getUnit().arity(); i++) { - subTerms(list, create(peek, i)); - } - } - - public int getRandomNumber() { - return Math.abs(random.nextInt()); - } -} -/* private Matchings reduceConformQuant(Matchings fromTerm, Matchings match) { - Matchings ret = new Matchings(); - Map quantifiedVarMap = match.first(); - - System.out.println("quantifiedVarMap = " + quantifiedVarMap); - - List> list = fromTerm.stream().filter( - map -> map.entrySet().stream().allMatch( - entry -> { - System.out.println("entry = " + entry); - if (entry.getValue() != null) { - MatchPath mp = (MatchPath) entry.getValue(); - Term mterm = (Term) mp.getUnit(); - if (quantifiedVarMap.containsKey(entry.getKey())) { - QuantifiableVariable unit = (QuantifiableVariable) quantifiedVarMap.get(entry.getKey()).getUnit(); - return unit.name().toString(). - equals(mterm.op().name().toString()); - } else { - - return true; - } - } else { - //in this case we have an empty match, however, we may have bound quantVars, we need to add them - System.out.println("entry.getKey() = " + entry.getKey()); - return true; - } - } - ) -).collect(Collectors.toList()); - - ret.addAll(list); - return ret; - }*/ \ No newline at end of file diff --git a/matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/Matchings.java b/matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/Matchings.java deleted file mode 100644 index e51bffda..00000000 --- a/matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/Matchings.java +++ /dev/null @@ -1,94 +0,0 @@ -package edu.kit.iti.formal.psdbg.termmatcher; - -import com.google.common.collect.Sets; -import edu.kit.iti.formal.psdbg.termmatcher.mp.MatchPath; - -import java.util.*; - -public class Matchings extends TreeSet> { - public Matchings() { - super(new VariableAssignmentComparator()); - } - - public Matchings(TreeMap m) { - this(); - add(m); - } - - 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; - } - -} - -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; - } - - 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(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/matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/OwnFunctionContext.java b/matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/OwnFunctionContext.java deleted file mode 100644 index 39c2cdc2..00000000 --- a/matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/OwnFunctionContext.java +++ /dev/null @@ -1,37 +0,0 @@ -package edu.kit.iti.formal.psdbg.termmatcher; - -import edu.kit.iti.formal.psdbg.termmatcher.MatchPatternParser; -import org.antlr.v4.runtime.Token; -import org.antlr.v4.runtime.tree.TerminalNode; - -import java.util.ArrayList; -import java.util.List; - -public class OwnFunctionContext extends MatchPatternParser.FunctionContext { - - public List termPattern = new ArrayList<>(); - - public OwnFunctionContext(MatchPatternParser.TermPatternContext ctx) { - super(ctx); - } - - public void setFunc(Token func) { - super.func = func; - - } - - public TerminalNode ID() { - return super.ID(); - } - - @Override - public List termPattern() { - return termPattern; - } - - @Override - public MatchPatternParser.TermPatternContext termPattern(int i) { - return termPattern.get(i); - } - -} diff --git a/matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/Utils.java b/matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/Utils.java deleted file mode 100644 index 25f858ca..00000000 --- a/matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/Utils.java +++ /dev/null @@ -1,51 +0,0 @@ -package edu.kit.iti.formal.psdbg.termmatcher; - -import de.uka.ilkd.key.logic.Term; -import de.uka.ilkd.key.logic.op.Equality; -import de.uka.ilkd.key.logic.op.Junctor; -import de.uka.ilkd.key.logic.op.Operator; - -public class Utils { - /** - * Rewrite toString() representation of Term to a parsable version - * - * @param formula - * @return parsable Stringversion of Term - */ - @Deprecated - public static String toPrettyTerm(Term formula) { - StringBuilder sb = new StringBuilder(); - - Operator op = formula.op(); - - //ugly if/else - if (op.equals(Junctor.IMP)) { - sb.append("(" + toPrettyTerm(formula.sub(0)) + ") -> (" + toPrettyTerm(formula.sub(1)) + ")"); - } else { - if (op.equals(Junctor.AND)) { - sb.append("(" + toPrettyTerm(formula.sub(0)) + ") & (" + toPrettyTerm(formula.sub(1)) + ")"); - } else { - if (op.equals(Junctor.OR)) { - sb.append("(" + toPrettyTerm(formula.sub(0)) + ") | (" + toPrettyTerm(formula.sub(1)) + ")"); - } else { - if (op.equals(Equality.EQV)) { - sb.append("(" + toPrettyTerm(formula.sub(0)) + ") <-> (" + toPrettyTerm(formula.sub(1)) + ")"); - } else { - if (op.equals(Equality.EQUALS)) { - sb.append("(" + toPrettyTerm(formula.sub(0)) + ") = (" + toPrettyTerm(formula.sub(1)) + ")"); - } else { - if (op.equals(Junctor.NOT)) { - sb.append("(!" + toPrettyTerm(formula.sub(0)) + ")"); - } else { - sb.append(formula.toString()); - } - } - } - } - } - } - - return sb.toString(); - } - -} diff --git a/matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/mp/MatchPath.java b/matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/mp/MatchPath.java deleted file mode 100644 index 453cfc99..00000000 --- a/matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/mp/MatchPath.java +++ /dev/null @@ -1,179 +0,0 @@ -package edu.kit.iti.formal.psdbg.termmatcher.mp; - -import de.uka.ilkd.key.logic.*; -import de.uka.ilkd.key.logic.op.QuantifiableVariable; -import lombok.Data; -import lombok.EqualsAndHashCode; - -/** - * @author Alexander Weigl - * @version 1 (24.08.17) - */ -@Data -@EqualsAndHashCode(of = {"unit"}) -public abstract class MatchPath { - public static final int SEQUENT_FORMULA_ROOT = -1; - public static final int POSITION_ANTECEDENT = -2; - public static final int POSITION_SUCCEDENT = -3; - - private final MatchPath parent; - private final T unit; - private final int posInParent; - - private MatchPath(MatchPath parent, T unit, int pos) { - posInParent = pos; - this.unit = unit; - this.parent = parent; - } - - public abstract PosInOccurrence pio(); - - - public Sequent getSequent() { - if (getParent() != null) - return getParent().getSequent(); - return null; - } - - public SequentFormula getSequentFormula() { - if (getParent() != null) - return getParent().getSequentFormula(); - return null; - } - - public abstract int depth(); - - public String toString() { - return unit.toString(); - } - - public static final class MPQuantifiableVariable extends MatchPath { - - public MPQuantifiableVariable(MatchPath parent, QuantifiableVariable unit, int pos) { - super(parent, unit, pos); - } - - @Override - public PosInOccurrence pio() { - return null; - } - - @Override - public Sequent getSequent() { - return null; - } - - @Override - public SequentFormula getSequentFormula() { - return null; - } - - @Override - public int depth() { - return getParent().depth() + 1; - } - } - - public static class MPTerm extends MatchPath { - public MPTerm(MatchPath parent, Term unit, int pos) { - super(parent, unit, pos); - } - - @Override - public PosInOccurrence pio() { - if(getParent()==null) return null; - PosInOccurrence pio = getParent().pio(); - if(getPosInParent()==SEQUENT_FORMULA_ROOT) - return pio; - return pio.down(getPosInParent()); - } - - @Override - public int depth() { - return getUnit().depth(); - } - } - - public static class MPSequentFormula extends MatchPath { - MPSequentFormula(MatchPath parent, SequentFormula unit, int pos) { - super(parent, unit, pos); - } - - @Override - public PosInOccurrence pio() { - return new PosInOccurrence(getUnit(), PosInTerm.getTopLevel(), - getParent().getPosInParent() == POSITION_ANTECEDENT - ); - } - - @Override - public Sequent getSequent() { - if (getParent() != null) - return getParent().getSequent(); - return null; - } - - @Override - public SequentFormula getSequentFormula() { - return getUnit(); - } - - @Override - public int depth() { - return getUnit().formula().depth(); - } - } - - public static class MPSequent extends MatchPath { - MPSequent(Sequent unit) { - super(null, unit, SEQUENT_FORMULA_ROOT); - } - - @Override - public int depth() { - return 0; - } - - @Override - public PosInOccurrence pio() { - return null; - } - - @Override - public Sequent getSequent() { - return getUnit(); - } - - @Override - public SequentFormula getSequentFormula() { - return null; - } - } - - public static class MPSemiSequent extends MatchPath { - MPSemiSequent(MPSequent parent, Semisequent unit, boolean antec) { - super(parent, unit, antec ? POSITION_ANTECEDENT : POSITION_SUCCEDENT); - } - - @Override - public int depth() { - return 1; - } - - @Override - public PosInOccurrence pio() { - return null; - } - - @Override - public Sequent getSequent() { - if (getParent() == null) return null; - return getParent().getSequent(); - } - - @Override - public SequentFormula getSequentFormula() { - return null; - } - } -} diff --git a/matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/mp/MatchPathFacade.java b/matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/mp/MatchPathFacade.java deleted file mode 100644 index f04fe4ea..00000000 --- a/matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/mp/MatchPathFacade.java +++ /dev/null @@ -1,64 +0,0 @@ -package edu.kit.iti.formal.psdbg.termmatcher.mp; - -import de.uka.ilkd.key.logic.Semisequent; -import de.uka.ilkd.key.logic.Sequent; -import de.uka.ilkd.key.logic.Term; - -/** - * @author Alexander Weigl - * @version 1 (27.08.17) - */ -public class MatchPathFacade { - public static MatchPath.MPTerm create(MatchPath path, int subTerm) { - return new MatchPath.MPTerm(path, path.getUnit().sub(subTerm), subTerm); - } - - public static MatchPath.MPSequentFormula create(MatchPath.MPSemiSequent ss, int pos) { - return new MatchPath.MPSequentFormula(ss, ss.getUnit().get(pos), pos); - } - - public static MatchPath.MPSemiSequent create(MatchPath.MPSequent s, boolean antec) { - MatchPath.MPSemiSequent mp = new MatchPath.MPSemiSequent( - s, antec - ? s.getUnit().antecedent() - : s.getUnit().succedent(), - antec); - return mp; - } - - public static MatchPath.MPSequent create(Sequent s) { - return new MatchPath.MPSequent(s); - } - - public static MatchPath.MPTerm create(MatchPath.MPSequentFormula sf) { - return new MatchPath.MPTerm(sf, sf.getUnit().formula(), MatchPath.SEQUENT_FORMULA_ROOT); - } - - public static MatchPath.MPSemiSequent createSuccedent(MatchPath.MPSequent sequent) { - return create(sequent, false); - } - - public static MatchPath.MPSemiSequent createAntecedent(MatchPath.MPSequent sequent) { - return create(sequent, true); - } - - /** - * only for testing - * - * @param keyTerm - * @return - */ - public static MatchPath createRoot(Term keyTerm) { - return new MatchPath.MPTerm(null, keyTerm, MatchPath.SEQUENT_FORMULA_ROOT); - } - - /** - * only for testing - * - * @param semiSeq - * @return - */ - public static MatchPath createRoot(Semisequent semiSeq) { - return new MatchPath.MPSemiSequent(null, semiSeq, true); - } -} diff --git a/matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/package-info.java b/matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/package-info.java deleted file mode 100644 index d3562215..00000000 --- a/matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/package-info.java +++ /dev/null @@ -1,4 +0,0 @@ -/** - * - */ -package edu.kit.iti.formal.psdbg.termmatcher; \ No newline at end of file diff --git a/matcher/src/test/java/edu/kit/iti/formal/psdbg/termmatcher/MatcherFacadeTest.java b/matcher/src/test/java/edu/kit/iti/formal/psdbg/termmatcher/MatcherFacadeTest.java deleted file mode 100644 index 5ded9d22..00000000 --- a/matcher/src/test/java/edu/kit/iti/formal/psdbg/termmatcher/MatcherFacadeTest.java +++ /dev/null @@ -1,310 +0,0 @@ -package edu.kit.iti.formal.psdbg.termmatcher; - -import de.uka.ilkd.key.control.DefaultUserInterfaceControl; -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.logic.sort.Sort; -import de.uka.ilkd.key.parser.DefaultTermParser; -import de.uka.ilkd.key.parser.ParserException; -import de.uka.ilkd.key.pp.AbbrevMap; -import de.uka.ilkd.key.proof.io.ProblemLoaderException; -import org.junit.Assert; -import org.junit.Before; -import org.junit.Test; - -import java.io.File; -import java.io.Reader; -import java.io.StringReader; - -public class MatcherFacadeTest { - private final static DefaultTermParser dtp = new DefaultTermParser(); - private Services services; - private AbbrevMap abbrev; - private NamespaceSet namespace; - - @Before - public void loadKeyEnv() throws ProblemLoaderException { - String file = getClass().getResource("test.key").toExternalForm().substring(5); - - KeYEnvironment env = - KeYEnvironment.load(new File(file)); - services = env.getServices(); - namespace = env.getServices().getNamespaces(); - abbrev = new AbbrevMap(); - } - - @Test - public void error() throws ParserException { - // shouldMatch("h2(2,3) = 0", - // "?X=0", "[{?X= h2(2,3)}]"); - - String s = "[{?X=h2(Z(2(#)),Z(3(#)))}]"; - shouldMatchSeq("h2(2,3) = 0 ==>", - "?X=0 ==>", s); - - shouldMatchSeq("h2(2,3) = 0 ==> p, !p", - "?X=0 ==>", s); - - shouldMatchSeq("2 >= 1, h2(1,2) = h2(2,3), h2(2,3) = 0 ==> p, !p", - "?X=0 ==>", s); - } - - @Test - public void matches() throws Exception { - System.out.println("QuantifierMatching"); - shouldMatchForm("\\forall int i; \\exists int j; fint2(j,i)", "(\\forall i (\\exists j _))"); - - shouldMatchForm("fint2(1,i)", "fint2(1,i)"); - - shouldMatchForm("\\exists int i; fint2(1,i)", "(\\exists _ ?Term)"); - - shouldMatchForm("\\exists int i; fint2(1,i)", "(\\exists ?X _)"); - shouldMatchForm("\\exists int i; fint2(1,i)", "(\\exists ?X (fint2(1,?X)))"); - - - shouldMatchForm("\\exists int i; \\exists int j; fint2(j,i)", "(\\exists i (\\exists j _))"); - - - shouldMatchForm("\\exists int i; \\exists int j; fint2(j,i)", "(\\exists i (\\exists j _))"); - - shouldMatchForm("\\exists int i; \\exists int j; fint2(j,i)", "(\\exists _ (\\exists j _))"); - - shouldMatchForm("\\exists int i; \\exists int j; fint2(j,i)", "(\\exists _ (\\exists _ _))"); - - shouldMatchForm("\\exists int i; \\exists int j; fint2(j,i)", "(\\exists i _)"); - - shouldMatchForm("\\exists int i; fint2(1,i)", "(\\exists i fint2(1,i))"); - - shouldMatchForm("\\exists int i; fint2(1,i)", "(\\exists ?X fint2(1,?X))"); - - shouldMatchForm("\\exists int i; \\exists int j; (fint2(i, j) -> fint2(j, i))", "(\\exists i (\\exists j (fint2(i, j) -> fint2(j, i))))"); - shouldMatch("f(a)", "_"); - shouldMatch("f(a)", "?X", "[{?X=f(a)}]"); - shouldMatch("h(a,a)", "h(?X,?X)", "[{?X=a}]"); - shouldMatch("h(a,b)", "h(?X,?X)", "[]"); - shouldMatch("f(a)", "f(a)"); - shouldMatchForm("pred(a)", "_"); - shouldMatchForm("pred(a)", "...?X...", "[{?X=a}, {?X=pred(a)}]"); - shouldMatchForm("pred(f(a))", "pred(...?X...)", "[{?X=a}, {?X=f(a)}]"); - shouldMatch("i+j", "add(?X,?Y)", "[{?X=i, ?Y=j}]"); - shouldMatch("i+j", "?X+?Y", "[{?X=i, ?Y=j}]"); - shouldMatchForm("p & q", "p & ?X", "[{?X=q}]"); - shouldMatchForm("p & q", "?X & q", "[{?X=p}]"); - shouldMatch("123", "13", "[]"); - shouldMatch("10203", "10203", "[{EMPTY_MATCH=null}]"); - shouldMatch("1*j", "1 + ?Y", "[]"); - shouldMatch("1*j", "1 * ?Y", "[{?Y=j}]"); - - //does not match - shouldMatch("1*j", "?Y * 1", "[{?Y=j}]"); - - } - - @Test - public void testBindContext() throws ParserException { - //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("g(f(a))", "g( (...a...):?Q ): ?Y", - "[{EMPTY_MATCH=null, ?Q=f(a), ?Y=g(f(a))}]"); - - shouldMatch("f(f(g(a)))", "f( (... g( (...a...):?Q ) ...) : ?R) : ?Y", - "[{EMPTY_MATCH=null, ?Q=a, ?Y=f(f(g(a))), ?R=f(g(a))}]"); - } - - - private void shouldMatch(String key, String pattern) throws ParserException { - Term term = parseKeyTerm(key); - Matchings m = MatcherFacade.matches(pattern, term, services); - System.out.println(m); - } - - private void shouldMatch(String key, String pattern, String exp) throws ParserException { - Term term = parseKeyTerm(key); - Matchings m = MatcherFacade.matches(pattern, term, services); - System.out.println(m); - Assert.assertEquals(exp, m.toString()); - } - - private void shouldMatchForm(String form, String pattern) throws ParserException { - Term formula = parserFormula(form); - Matchings m = MatcherFacade.matches(pattern, formula, services); - System.out.println(m); - } - - private void shouldMatchForm(String form, String pattern, String exp) throws ParserException { - Term formula = parserFormula(form); - Matchings m = MatcherFacade.matches(pattern, formula, services); - System.out.println(m); - Assert.assertEquals(exp, m.toString()); - } - - public Term parseKeyTerm(String term) throws ParserException { - Reader in = new StringReader(term); - Sort sort = Sort.ANY; - /* - Services services = new Services(new JavaProfile()); - AbbrevMap abbrev = new AbbrevMap(); - NamespaceSet namespace = services.getNamespaces(); - - Sort Int = new SortImpl(new Name("int")); - Sort bool = new SortImpl(new Name("boolean")); - - namespace.functions().add(new LogicVariable(new Name("p"), bool)); - namespace.functions().add(new LogicVariable(new Name("q"), bool)); - namespace.functions().add(new Function(new Name("g"), Int)); - namespace.functions().add(new Function(new Name("f"), Int)); - namespace.functions().add(new Function(new Name("h"), Int)); - - namespace.functions().add(new Function(new Name("a"), Int)); - namespace.functions().add(new Function(new Name("b"), Int)); - namespace.functions().add(new Function(new Name("c"), Int)); - */ - - return dtp.parse(in, sort, services, namespace, abbrev); - } - - public Term parserFormula(String form) throws ParserException { - Reader in = new StringReader(form); - Sort sort = Sort.FORMULA; - return dtp.parse(in, sort, services, namespace, abbrev); - } - - @Test - public void semiSeqTest() throws Exception { - 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)", "[]"); - 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(a), pred(b) ==>", "pred(a), pred(b)", "[{EMPTY_MATCH=null}]"); - shouldMatchSemiSeq("pred(a), pred(b) ==> qpred(a,b)", "pred(a), pred(b) ==> ", "[{EMPTY_MATCH=null}]"); - shouldMatchSemiSeq("pred(a), pred(b) ==> qpred(a,b)", "pred(?X), pred(?Y)", "[{?X=a, ?Y=b}, {?X=b, ?Y=a}]"); - - shouldMatchSemiSeq("pred(b), pred(a) ==>", "pred(...?X...), pred(f(?X))", "[]"); - shouldMatchSemiSeq("pred(b), pred(a) ==>", "pred(...?X...), pred(...?Y...)", "[{?X=a, ?Y=b}, {?X=b, ?Y=a}]"); - - shouldMatchSemiSeq("intPred(fint(i+j)) ==>", "intPred(...add(?X, ?y)...)"); - - } - - private void shouldMatchSemiSeq(String s, String s1, String exp) throws ParserException { - Sequent term = parseSeq(s); - Matchings m = MatcherFacade.matches(s1, term, services); - System.out.println(m); - Assert.assertEquals(exp, m.toString()); - } - - private void shouldMatchSemiSeq(String s, String s1) throws ParserException { - Sequent term = parseSeq(s); - Matchings m = MatcherFacade.matches(s1, term, services); - System.out.println(m); - } - - private Sequent parseSeq(String s) throws ParserException { - Reader in = new StringReader(s); - return dtp.parseSeq(in, services, namespace, abbrev); - } - - - // Sollverhalten: Wenn es keinen Variablenbinder gibt, aber z.B. '_' oder '...', - // und positiv auf den Ausdruck gematcht wird, - // dann soll der Term des Matchs in Form von anonymen Variablen gebunden werden - - @Test - public void seqTest() throws Exception { - shouldMatchSeq("i <= 10 ==>", - "i <= ?X ==>", - "[{??_=leq(i,Z(0(1(#)))), ?X=Z(0(1(#))), ??_=i}]"); - - shouldMatchSeq("==> (\\forall int i; \\exists int j; fint2(j,i)) , pred(a)", - "==> (\\forall i (\\exists j _))", - "[{??_=exists{j:int}(fint2(j,i)), ??_=all{i:int}(exists{j:int}(fint2(j,i))), ??_=fint2(j,i)}]"); - - shouldMatchSeq("pred(a) ==> pred(a), pred(b)", - " ==> _", - "[{??_=pred(a)}, {??_=pred(b)}]"); - - shouldMatchSeq("pred(a) ==> pred(a), pred(b)", - "==>", - "[{EMPTY_MATCH=null}]"); - shouldMatchSeq("pred(a) ==> pred(a), pred(b)", - "_ ==> ", - "[{??_=pred(a)}]"); - shouldMatchSeq("pred(a) ==> pred(a), pred(b)", - "_ ==> _", - "[{??_=pred(b), ??_=pred(a)}, {??_=pred(a), ??_=pred(a)}]"); - shouldMatchSeq("==> pred(a)", - "==>", - "[{EMPTY_MATCH=null}]"); - shouldMatchSeq("pred(a) ==> ", - "==>", - "[{EMPTY_MATCH=null}]"); - - - shouldMatchSeq("pred(a), pred(b) ==> pred(b)", - "pred(?X), pred(?Z) ==> pred(?Y)", - "[{??_=pred(a), ?X=b, ?Y=b, ??_=pred(b), ?Z=a, ??_=pred(b)}, {?X=a, ??_=pred(a), ?Y=b, ??_=pred(b), ?Z=b, ??_=pred(b)}]"); - //"[{?X=a, ?Y=b, ?Z=b}, {?X=b, ?Y=b, ?Z=a}]"); - - shouldMatchSeq("pred(a), pred(b) ==> pred(b)", - "pred(?X), pred(?Z) ==> pred(?X)", - "[{??_=pred(a), ?X=b, ??_=pred(b), ?Z=a, ??_=pred(b)}]"); -// "[{?X=b, ?Z=a}]"); - - shouldMatchSeq("pred(a), pred(b) ==> pred(b)", - "pred(?X), pred(?Z) ==>", - "[{??_=pred(a), ?X=b, ?Z=a, ??_=pred(b)}, {?X=a, ??_=pred(a), ?Z=b, ??_=pred(b)}]"); -// "[{?X=a, ?Z=b}, {?X=b, ?Z=a}]"); - - shouldMatchSeq( - "pred(f(a)), pred(b) ==> pred(b)", - "pred(?X), pred(?Z) ==>", - "[{??_=pred(f(a)), ?X=b, ?Z=f(a), ??_=pred(b)}, {?X=f(a), ??_=pred(f(a)), ?Z=b, ??_=pred(b)}]"); -// "[{?X=b, ?Z=f(a)}, {?X=f(a), ?Z=b}]"); - - shouldMatchSeq( - "pred(f(a)), pred(b) ==> pred(b)", - "pred(...?X...) ==>", - "[{??_=pred(b), ?X=b}, {?X=a, ??_=pred(f(a))}, {?X=f(a), ??_=pred(f(a))}]"); -// "[{?X=a}, {?X=b}, {?X=f(a)}]"); - - shouldMatchSeq( - "fint2(1,2), fint2(2,3), !p ==> pred(a), p", - "fint2(1, ?X), fint2(?X, ?Y) ==> p", - "[{??_=fint2(Z(2(#)),Z(3(#))), ?X=Z(2(#)), ?Y=Z(3(#)), ??_=fint2(Z(1(#)),Z(2(#))), ??_=p}]"); -// "[{EMPTY_MATCH=null, ?X=Z(2(#)), ?Y=Z(3(#))}]"); - shouldMatchSeq("2 >= 1, h2(1,2) = h2(2,3), h2(2,3) = 0 ==> p, !p", - "?X=0 ==>", - "[{?X=h2(Z(2(#)),Z(3(#))), ??_=equals(h2(Z(2(#)),Z(3(#))),Z(0(#)))}]"); -// "[{?X=h2(Z(2(#)),Z(3(#)))}]"); - - shouldMatchSeq("pred(a) <-> pred(b), pred(a), pred(b) ==> p", - "?X <-> ?Y ==> ", - "[{?X=pred(a), ?Y=pred(b), ??_=equiv(pred(a),pred(b))}]"); -// "[{?X=pred(a), ?Y=pred(b)}]"); - } - - private void shouldMatchSeq(String seq, String seqPattern, String exp) throws ParserException { - Sequent sequent = parseSeq(seq); - Matchings m = MatcherFacade.matches(seqPattern, sequent, services); - System.out.println(m); - Assert.assertEquals(removeNumbersInBinders(m), exp); - } - - private String removeNumbersInBinders(Matchings m) { - String matchingsAsString = m.toString(); - String toCheck = matchingsAsString.replaceAll("\\?\\?_\\d+=", "??_="); - String toCheck2 = toCheck.replaceAll("\\?\\?_-\\d+=", "??_="); - return toCheck2; - } - - private void shouldMatchSeq(String seq, String seqPattern) throws ParserException { - Sequent sequent = parseSeq(seq); - Matchings m = MatcherFacade.matches(seqPattern, sequent, services); - System.out.println(m); - } -} \ No newline at end of file diff --git a/matcher/src/test/java/edu/kit/iti/formal/psdbg/termmatcher/TestComplexMatch.java b/matcher/src/test/java/edu/kit/iti/formal/psdbg/termmatcher/TestComplexMatch.java deleted file mode 100644 index 63b47c43..00000000 --- a/matcher/src/test/java/edu/kit/iti/formal/psdbg/termmatcher/TestComplexMatch.java +++ /dev/null @@ -1,38 +0,0 @@ -package edu.kit.iti.formal.psdbg.termmatcher; - - -import de.uka.ilkd.key.api.KeYApi; -import de.uka.ilkd.key.api.ProofApi; -import de.uka.ilkd.key.api.ProofManagementApi; -import de.uka.ilkd.key.logic.Sequent; -import de.uka.ilkd.key.proof.init.ProofInputException; -import de.uka.ilkd.key.proof.io.ProblemLoaderException; -import org.junit.Test; - -import java.io.File; -import java.util.regex.Pattern; - -/* - shouldMatchSeq("seqPerm(seqDef{int u;}(0, result_1.length, any::select(heapAfter_copyArray_0, result_1, arr(u))), seqDef{int u;}(0, result_0.length, any::select(heapAfter_copyArray_0, result_0, arr(u))))", - "seqPerm(?X, ?Y)"); - */ -public class TestComplexMatch { - @Test - public void test() throws ProblemLoaderException, ProofInputException { - ProofManagementApi a = KeYApi.loadFromKeyFile(new File("src/test/resources/edu/kit/iti/formal/psdbg/termmatcher/javacomplex/project.key")); - ProofApi pa = a.startProof(a.getProofContracts().get(3)); - Sequent sequent = pa.getProof().root().sequent(); - System.out.println(sequent); - /* Matchings result = MatcherFacade.matches("... update-application(_, ?X) ...", sequent, false); - System.out.println(result); - String exp = normalize("\\<{exc=null;try { result=self.foo(_x)@Test;} catch (java.lang.Throwable e) { exc=e; } }\\> (and(and(and(gt(result,Z(0(#))),java.lang.Object::(heap,self)),equals(exc,null)),all{f:Field}(all{o:java.lang.Object}(or(or(elementOf(o,f,allLocs),and(not(equals(o,null)),not(equals(boolean::select(heapAtPre,o,java.lang.Object::),TRUE)))),equals(any::select(heap,o,f),any::select(heapAtPre,o,f)))))))"); - String x = normalize(result.iterator().next().get("?X").getUnit().toString().replace("\n", " ")); - Assert.assertEquals(exp, x);*/ - } - - private String normalize(String s) { - Pattern re = Pattern.compile("\\s+"); - return re.matcher(s).replaceAll(" "); - } - -} diff --git a/matcher/src/test/java/edu/kit/iti/formal/psdbg/termmatcher/TestUpdateMatch.java b/matcher/src/test/java/edu/kit/iti/formal/psdbg/termmatcher/TestUpdateMatch.java deleted file mode 100644 index 04f82f53..00000000 --- a/matcher/src/test/java/edu/kit/iti/formal/psdbg/termmatcher/TestUpdateMatch.java +++ /dev/null @@ -1,37 +0,0 @@ -package edu.kit.iti.formal.psdbg.termmatcher; - -import de.uka.ilkd.key.api.KeYApi; -import de.uka.ilkd.key.api.ProofApi; -import de.uka.ilkd.key.api.ProofManagementApi; -import de.uka.ilkd.key.java.Services; -import de.uka.ilkd.key.logic.Sequent; -import de.uka.ilkd.key.proof.init.ProofInputException; -import de.uka.ilkd.key.proof.io.ProblemLoaderException; -import org.junit.Assert; -import org.junit.Test; - -import java.io.File; -import java.util.regex.Pattern; - -public class TestUpdateMatch { - @Test - public void test() throws ProblemLoaderException, ProofInputException { - ProofManagementApi a = KeYApi.loadFromKeyFile(new File("src/test/resources/edu/kit/iti/formal/psdbg/termmatcher/javasimple/project.key")); - ProofApi pa = a.startProof(a.getProofContracts().get(0)); - Sequent sequent = pa.getProof().root().sequent(); - System.out.println(sequent); - Matchings result = MatcherFacade.matches("... update-application(_, ?X) ...", - sequent, false, null); - System.out.println(result); - String exp = normalize("\\<{exc=null;try { result=self.foo(_x)@Test;} catch (java.lang.Throwable e) { exc=e; } }\\> (and(and(and(gt(result,Z(0(#))),java.lang.Object::(heap,self)),equals(exc,null)),all{f:Field}(all{o:java.lang.Object}(or(or(elementOf(o,f,allLocs),and(not(equals(o,null)),not(equals(boolean::select(heapAtPre,o,java.lang.Object::),TRUE)))),equals(any::select(heap,o,f),any::select(heapAtPre,o,f)))))))"); - String x = normalize(result.iterator().next().get("?X").getUnit().toString().replace("\n", " ")); - Assert.assertEquals(exp, x); - } - - private String normalize(String s) { - Pattern re = Pattern.compile("\\s+"); - return re.matcher(s).replaceAll(" "); - } - - -} diff --git a/matcher/src/test/resources/edu/kit/iti/formal/psdbg/termmatcher/goodmatches.txt b/matcher/src/test/resources/edu/kit/iti/formal/psdbg/termmatcher/goodmatches.txt deleted file mode 100644 index 0b6a11a4..00000000 --- a/matcher/src/test/resources/edu/kit/iti/formal/psdbg/termmatcher/goodmatches.txt +++ /dev/null @@ -1,2 +0,0 @@ -p >>> _ -p >>> ?X \ No newline at end of file diff --git a/matcher/src/test/resources/edu/kit/iti/formal/psdbg/termmatcher/javacomplex/Simple.java b/matcher/src/test/resources/edu/kit/iti/formal/psdbg/termmatcher/javacomplex/Simple.java deleted file mode 100644 index 94a91765..00000000 --- a/matcher/src/test/resources/edu/kit/iti/formal/psdbg/termmatcher/javacomplex/Simple.java +++ /dev/null @@ -1,41 +0,0 @@ - public final class Simple { - - - boolean b1; - boolean b2; - - /*@ public normal_behavior - @ ensures \dl_seqPerm(\dl_array2seq(\result), \old(\dl_array2seq(aarr))); - @ assignable \everything; - */ - public int[] transitive(int[] aarr){ - aarr = Simple.copyArray(aarr); - sort(aarr); - int[] barr = Simple.copyArray(aarr); - - if(b1){barr = Simple.copyArray(aarr);} - if(b2){log(barr);} - return barr; - } - - /*@ public normal_behavior - @ ensures \dl_seqPerm(\dl_array2seq(a), \old(\dl_array2seq(a))); - @ assignable a[*]; - */ - public void sort(int[] a){}; - - /*@ public normal_behavior - @ ensures (\forall int i; 0 <= i < input.length; input[i] == \result[i]) - @ && \result.length == input.length; - @ ensures \fresh(\result); - @ ensures \dl_seqPerm(\dl_array2seq(\result), \dl_array2seq(input)); - @ assignable \nothing; - */ - public /*@helper@*/ static int[] copyArray(int[] input){} - - /*@ public normal_behavior - @ assignable \strictly_nothing; - */ - public void log(int[] a){}; - -} diff --git a/matcher/src/test/resources/edu/kit/iti/formal/psdbg/termmatcher/javacomplex/project.key b/matcher/src/test/resources/edu/kit/iti/formal/psdbg/termmatcher/javacomplex/project.key deleted file mode 100644 index b84b1a5e..00000000 --- a/matcher/src/test/resources/edu/kit/iti/formal/psdbg/termmatcher/javacomplex/project.key +++ /dev/null @@ -1,2 +0,0 @@ -\javaSource ""; -\chooseContract \ No newline at end of file diff --git a/matcher/src/test/resources/edu/kit/iti/formal/psdbg/termmatcher/javasimple/Test.java b/matcher/src/test/resources/edu/kit/iti/formal/psdbg/termmatcher/javasimple/Test.java deleted file mode 100644 index c2eeb1e2..00000000 --- a/matcher/src/test/resources/edu/kit/iti/formal/psdbg/termmatcher/javasimple/Test.java +++ /dev/null @@ -1,17 +0,0 @@ -public class Test{ - - - - /*@ public normal_behavior - @ requires x >= 0; - @ ensures \result >0; - @*/ - public int foo(int x){ - if(x > 0){ - x--; - }else{ - x++; - } - return x++; - } -} \ No newline at end of file diff --git a/matcher/src/test/resources/edu/kit/iti/formal/psdbg/termmatcher/javasimple/project.key b/matcher/src/test/resources/edu/kit/iti/formal/psdbg/termmatcher/javasimple/project.key deleted file mode 100644 index b84b1a5e..00000000 --- a/matcher/src/test/resources/edu/kit/iti/formal/psdbg/termmatcher/javasimple/project.key +++ /dev/null @@ -1,2 +0,0 @@ -\javaSource ""; -\chooseContract \ No newline at end of file diff --git a/matcher/src/test/resources/edu/kit/iti/formal/psdbg/termmatcher/test.key b/matcher/src/test/resources/edu/kit/iti/formal/psdbg/termmatcher/test.key deleted file mode 100644 index 46563ed1..00000000 --- a/matcher/src/test/resources/edu/kit/iti/formal/psdbg/termmatcher/test.key +++ /dev/null @@ -1,41 +0,0 @@ -// This file is part of KeY - Integrated Deductive Software Design -// -// Copyright (C) 2001-2011 Universitaet Karlsruhe (TH), Germany -// Universitaet Koblenz-Landau, Germany -// Chalmers University of Technology, Sweden -// Copyright (C) 2011-2013 Karlsruhe Institute of Technology, Germany -// Technical University Darmstadt, Germany -// Chalmers University of Technology, Sweden -// -// The KeY system is protected by the GNU General -// Public License. See LICENSE.TXT for details. -// - -// Input file for KeY standalone prover version 0.497 -\sorts { - S; -} - -\functions { - S a; S b; S c; - int i; int j; - S f(S); - S g(S); - S h(S, S); - int h2(int, int); - int fint(int); - -} - -\predicates { - p; - q; - pred(S); - qpred(S, S); - intPred(int); - fint2(int, int); -} - -\problem { - (p -> q) -> !q -> !p -} diff --git a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/KeyMatcherFacade.java b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/KeyMatcherFacade.java index ef2d1ae6..eb5448c9 100644 --- a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/KeyMatcherFacade.java +++ b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/KeyMatcherFacade.java @@ -1,26 +1,18 @@ package edu.kit.iti.formal.psdbg.interpreter.matcher; import de.uka.ilkd.key.control.KeYEnvironment; -import de.uka.ilkd.key.java.Services; -import de.uka.ilkd.key.logic.*; -import de.uka.ilkd.key.logic.op.AbstractSortedOperator; -import de.uka.ilkd.key.logic.op.QuantifiableVariable; -import de.uka.ilkd.key.logic.sort.Sort; -import de.uka.ilkd.key.macros.scripts.ScriptException; +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 edu.kit.iti.formal.psdbg.parser.ast.Operator; -import edu.kit.iti.formal.psdbg.parser.ast.Signature; import lombok.Builder; import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.Logger; -import org.key_project.util.collection.ImmutableArray; import java.io.Reader; import java.io.StringReader; import java.util.ArrayList; import java.util.List; -import java.util.function.Function; @Builder public class KeyMatcherFacade { @@ -29,14 +21,17 @@ public class KeyMatcherFacade { private final KeYEnvironment environment; private final Sequent sequent; + private static Logger loggerConsole = LogManager.getLogger("console"); public Matchings matches(String pattern) { + Matchings ret; if(pattern.contains("==>")) { - return matchesSequent(pattern); + ret = matchesSequent(pattern); } else { - return matchesTerm(pattern); + ret = matchesTerm(pattern); } - + loggerConsole.info("Pattern: {} against Sequent: {} matches as {}", pattern, this.sequent, ret); + return ret; } private Matchings matchesTerm(String pattern) { 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 cb1a5fe7..de72269c 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 @@ -204,8 +204,9 @@ public class KeyTermMatcher extends KeyTermBaseVisitor { // if(pattern.equals(subject1.getUnit())) // return EmptyMatch.INSTANCE; // return Matchings.singleton(pattern.toString(), subject1); - if(pattern.op().equals(((Term) subject1.getUnit()).op())) { - for (int i = 0; i < subject.getUnit().subs().size(); i++) { +// if(pattern.op().equals(((Term) subject1.getUnit()).op())) { + if(pattern.op().name().equals(((Term) subject1.getUnit()).op().name())) { + 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)); 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 84c479a3..3903a37b 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 @@ -59,6 +59,15 @@ public class KeyMatcherFacadeTest { @Test public void matchSeq() throws Exception { //atm missing is catching the toplevel formula + shouldMatch("!q==>p,!p","!q ==> p", "[{}]"); + shouldMatch("!p ,p ==> q", "!p ==> q", "[{}]"); + shouldMatch("!q ,p ==> q", "!p ==> q", "{NOMATCH}"); + shouldMatch("!q==>p,!p","!q ==> p", "[{}]"); + shouldMatch("!p ,p ==> q", "!p ==> q", "[{}]"); + shouldMatch("!q ,p ==> q", "!p ==> q", "{NOMATCH}"); + + + shouldMatch(" ==> !p, p,!q", "==> ?Z, !(?Z)", "[{?Z=p}]"); shouldMatch("==> pred(a)", "==> pred(?)"); diff --git a/ui/build.gradle b/ui/build.gradle index 5bc76cad..b6177c4c 100644 --- a/ui/build.gradle +++ b/ui/build.gradle @@ -31,6 +31,8 @@ dependencies { compile group: 'org.antlr', name: 'antlr4', version: '4.7' antlr group: 'org.antlr', name: 'antlr4', version: '4.7' + //compile files("$rootDir/DockFX/build/libs/DockFX.jar") + compile project(':rt-key') compile project(':DockFX') compile project(':lint') diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/FileReloadingService.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/FileReloadingService.java index 17cca96e..9d79523e 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/FileReloadingService.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/FileReloadingService.java @@ -36,7 +36,7 @@ public class FileReloadingService extends TimerTask { try { wService = FileSystems.getDefault().newWatchService(); timer = new Timer("filereloading", true); - timer.schedule(this, 500, 500); + // timer.schedule(this, 500, 500); } catch (IOException e) { LOGGER.error(e); CONSOLE_LOGGER.error("Auto-reloading is not available. See log file for more details"); diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ProofTree.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ProofTree.java index cb4057d0..cd4539f3 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ProofTree.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ProofTree.java @@ -111,9 +111,10 @@ public class ProofTree extends BorderPane { public ProofTree(DebuggerMain main) { Utils.createWithFXML(this); //TODO remove this hack for a better solution - main.getModel().debuggerFrameworkProperty().addListener((p, n, m) -> { - treeCreation = new TreeTransformationScript(m.getPtreeManager()); - }); + //main.getModel().debuggerFrameworkProperty().addListener((p, n, m) -> { + // treeCreation = new TreeTransformationScript(m.getPtreeManager()); + //}); + treeCreation = new TreeTransformationKey(); treeProof.setCellFactory(this::cellFactory); root.addListener(o -> init()); diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptController.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptController.java index e05a0f1d..14c194d7 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptController.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptController.java @@ -95,6 +95,7 @@ public class ScriptController { } private void updateSavePoints() { + try{ Optional ms = getMainScript().find(getCombinedAST()); if (ms.isPresent()) { List list = ms.get().getBody().stream() @@ -103,8 +104,9 @@ public class ScriptController { .map(SavePoint::new) .collect(Collectors.toList()); mainScriptSavePoints.setAll(list); - loggerConsole.info("Found savepoints: " + list); - } + // loggerConsole.info("Found savepoints: " + list); + }}catch (Exception e){} + } /* diff --git a/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/script.kps b/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/script.kps index 110e3b53..f891c583 100644 --- a/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/script.kps +++ b/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/script.kps @@ -1,3 +1,19 @@ +script full(){ + impRight; + impRight; + impLeft; + cases { + case match `!q ==> p`: + notLeft; + notRight; + close; + auto; + + case match `q==>!p`: + notLeft; + closeAntec; + } +} script autoScript(){ __STRICT_MODE := true; @@ -11,7 +27,6 @@ script interactive(){ impLeft; //after execution of this script, manual interaction can be performed } - script interactive_with_match(){ impRight; impRight; -- GitLab