Commit c795e38a authored by Sarah Grebing's avatar Sarah Grebing
Browse files

Added termmatcher instead of key matcher

parent 7d9770fc
Pipeline #13339 failed with stage
in 2 minutes and 24 seconds
...@@ -3,6 +3,7 @@ package edu.kit.iti.formal.psdbg.interpreter; ...@@ -3,6 +3,7 @@ package edu.kit.iti.formal.psdbg.interpreter;
import de.uka.ilkd.key.api.ScriptApi; import de.uka.ilkd.key.api.ScriptApi;
import de.uka.ilkd.key.api.VariableAssignments; import de.uka.ilkd.key.api.VariableAssignments;
import de.uka.ilkd.key.logic.Name; import de.uka.ilkd.key.logic.Name;
import de.uka.ilkd.key.logic.SequentFormula;
import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.Term;
import de.uka.ilkd.key.logic.op.SchemaVariable; import de.uka.ilkd.key.logic.op.SchemaVariable;
import de.uka.ilkd.key.proof.ApplyStrategy; import de.uka.ilkd.key.proof.ApplyStrategy;
...@@ -14,19 +15,20 @@ import de.uka.ilkd.key.rule.Taclet; ...@@ -14,19 +15,20 @@ import de.uka.ilkd.key.rule.Taclet;
import de.uka.ilkd.key.rule.TacletApp; import de.uka.ilkd.key.rule.TacletApp;
import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode; import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode;
import edu.kit.iti.formal.psdbg.interpreter.data.KeyData; import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
import edu.kit.iti.formal.psdbg.parser.data.Value;
import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment; import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment;
import edu.kit.iti.formal.psdbg.parser.ast.Signature; import edu.kit.iti.formal.psdbg.parser.ast.Signature;
import edu.kit.iti.formal.psdbg.parser.ast.TermLiteral; import edu.kit.iti.formal.psdbg.parser.ast.TermLiteral;
import edu.kit.iti.formal.psdbg.parser.types.SimpleType;
import edu.kit.iti.formal.psdbg.parser.ast.Variable; import edu.kit.iti.formal.psdbg.parser.ast.Variable;
import edu.kit.iti.formal.psdbg.parser.data.Value;
import edu.kit.iti.formal.psdbg.parser.types.SimpleType;
import edu.kit.iti.formal.psdbg.parser.types.TermType;
import edu.kit.iti.formal.psdbg.parser.types.Type; import edu.kit.iti.formal.psdbg.parser.types.Type;
import edu.kit.iti.formal.psdbg.termmatcher.MatcherFacade;
import edu.kit.iti.formal.psdbg.termmatcher.Matchings;
import edu.kit.iti.formal.psdbg.termmatcher.mp.MatchPath;
import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableList;
import java.util.ArrayList; import java.util.*;
import java.util.List;
import java.util.Map;
import java.util.Set;
import java.util.regex.MatchResult; import java.util.regex.MatchResult;
import java.util.regex.Matcher; import java.util.regex.Matcher;
import java.util.regex.Pattern; import java.util.regex.Pattern;
...@@ -163,8 +165,8 @@ public class KeYMatcher implements MatcherApi<KeyData> { ...@@ -163,8 +165,8 @@ public class KeYMatcher implements MatcherApi<KeyData> {
* @param signature * @param signature
* @return * @return
*/ */
@Override //@Override
public List<VariableAssignment> matchSeq(GoalNode<KeyData> currentState, public List<VariableAssignment> matchSeqKeY(GoalNode<KeyData> currentState,
String term, String term,
Signature signature) { Signature signature) {
...@@ -189,6 +191,7 @@ public class KeYMatcher implements MatcherApi<KeyData> { ...@@ -189,6 +191,7 @@ public class KeYMatcher implements MatcherApi<KeyData> {
// System.out.println("Matching: "+term.toString()+"\n================\n"+currentState.getData().getNode().sequent()+"\n================\n"); // System.out.println("Matching: "+term.toString()+"\n================\n"+currentState.getData().getNode().sequent()+"\n================\n");
List<VariableAssignments> keyMatchResult = scrapi.matchPattern(term, currentState.getData().getNode().sequent(), keyAssignments); List<VariableAssignments> keyMatchResult = scrapi.matchPattern(term, currentState.getData().getNode().sequent(), keyAssignments);
//empty keyassignments //empty keyassignments
// System.out.println("Matched " + keyMatchResult.size() + " goals from " + currentState.toString() + " with pattern " + term); // System.out.println("Matched " + keyMatchResult.size() + " goals from " + currentState.toString() + " with pattern " + term);
List<VariableAssignment> transformedMatchResults = new ArrayList<>(); List<VariableAssignment> transformedMatchResults = new ArrayList<>();
...@@ -200,6 +203,31 @@ public class KeYMatcher implements MatcherApi<KeyData> { ...@@ -200,6 +203,31 @@ public class KeYMatcher implements MatcherApi<KeyData> {
} }
@Override
public List<VariableAssignment> matchSeq(GoalNode<KeyData> currentState, String data, Signature sig) {
System.out.println("State that will be matched " + currentState.getData().getNode().sequent() + " with pattern " + data);
System.out.println("Signature " + sig.toString());
Matchings m = MatcherFacade.matches(data, currentState.getData().getNode().sequent());
if (m.isEmpty()) {
return Collections.emptyList();
} else {
Map<String, MatchPath> firstMatch = m.first();
VariableAssignment va = new VariableAssignment(null);
for (String s : firstMatch.keySet()) {
MatchPath matchPath = firstMatch.get(s);
if (!s.equals("EMPTY_MATCH")) {
Term matched = (Term) matchPath.getUnit();
va.declare(s, new TermType());
va.assign(s, Value.from(from(matched)));
}
}
List<VariableAssignment> retList = new LinkedList();
System.out.println("Matched Variables " + va.toString());
retList.add(va);
return retList;
}
}
/** /**
* Transforms a KeY Variable Assignment into an assignment for the interpreter * Transforms a KeY Variable Assignment into an assignment for the interpreter
* *
...@@ -226,4 +254,8 @@ public class KeYMatcher implements MatcherApi<KeyData> { ...@@ -226,4 +254,8 @@ public class KeYMatcher implements MatcherApi<KeyData> {
private TermLiteral from(Term t) { private TermLiteral from(Term t) {
return new TermLiteral(t.toString()); return new TermLiteral(t.toString());
} }
private TermLiteral from(SequentFormula sf) {
return new TermLiteral(sf.toString());
}
} }
...@@ -5,6 +5,10 @@ script cpClosable(){ ...@@ -5,6 +5,10 @@ script cpClosable(){
impRight; impRight;
impRight; impRight;
cases{ cases{
case match `?X -> ?Y ==> not(?Z)`:
notLeft;
try: try:
notLeft; notLeft;
notRight; notRight;
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment