Skip to content

P
ProofScriptParser
Commit da98f424 authored by Sarah Grebing's avatar Sarah Grebing
Browse files
Options

bugfix matcher

parent 2b65453d
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 80 additions and 1978 deletions
DockFX/build.gradle
View file @ da98f424
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")
}*/
lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/MatchExpression.java
View file @ da98f424
......@@ -41,7 +41,7 @@ import lombok.Data;
public class MatchExpression extends Expression<ScriptLanguageParser.MatchPatternContext> {
//private Signature signature = new Signature();
private Expression pattern;
private boolean isDerivable;
private boolean isDerivable = false;
@Deprecated
private Expression derivableTerm;
......
matcher/src/main/antlr/edu/kit/iti/formal/psdbg/termmatcher/MatchPattern.g4 deleted 100644 → 0
View file @ 2b65453d
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
| <assoc=right> 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);
matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/MatchPatternDualVisitor.java deleted 100644 → 0
View file @ 2b65453d
package edu.kit.iti.formal.psdbg.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(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);
}
matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/MatcherFacade.java deleted 100644 → 0
View file @ 2b65453d
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);
}
}
matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/Matchings.java deleted 100644 → 0
View file @ 2b65453d
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<Map<String, MatchPath>> {
public Matchings() {
super(new VariableAssignmentComparator());
}
public Matchings(TreeMap<String, MatchPath> m) {
this();
add(m);
}
public static Matchings singleton(String name, MatchPath term) {
Matchings matchings = new Matchings();
Map<String, MatchPath> va = new TreeMap<>();
va.put(name, term);
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) {
int cmp = o1.get(k).toString().compareTo(o2.get(k).toString());
if (cmp != 0)
return cmp;
}
return 0;
}
private int compareVariableName(Map<String, MatchPath> o1, Map<String, MatchPath> o2) {
return variableNames(o1).compareTo(variableNames(o2));
}
private String variableNames(Map<String, MatchPath> va) {
return va.keySet().stream().reduce((a, b) -> a + '#' + b).orElse("#");
}
/**
* @param a
* @param b
* @return
*/
private boolean isTrueSubset(Set<String> a, Set<String> b) {
return b.containsAll(a) && !a.containsAll(b);
}
}
\ No newline at end of file
matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/OwnFunctionContext.java deleted 100644 → 0
View file @ 2b65453d
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<MatchPatternParser.TermPatternContext> 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<MatchPatternParser.TermPatternContext> termPattern() {
return termPattern;
}
@Override
public MatchPatternParser.TermPatternContext termPattern(int i) {
return termPattern.get(i);
}
}
matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/Utils.java deleted 100644 → 0
View file @ 2b65453d
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();
}
}
matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/mp/MatchPath.java deleted 100644 → 0
View file @ 2b65453d
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<T, P> {
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<? extends P, ?> parent;
private final T unit;
private final int posInParent;
private MatchPath(MatchPath<? extends P, ?> 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<QuantifiableVariable, Object> {
public MPQuantifiableVariable(MatchPath<? extends Object, ?> parent, QuantifiableVariable unit, int pos) {
super(parent, unit, pos);
}
@Override
public PosInOccurrence pio() {
return null;
}