Commit 0597ba77 authored by Sarah Grebing's avatar Sarah Grebing

Bug Fix: Representation of matched terms was not compatible with KeY representation

parent b08c1ba4
Pipeline #13567 failed with stage
in 2 minutes and 38 seconds
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
*/
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();
}
}
......@@ -25,6 +25,7 @@ import edu.kit.iti.formal.psdbg.parser.types.TermType;
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.Utils;
import edu.kit.iti.formal.psdbg.termmatcher.mp.MatchPath;
import org.key_project.util.collection.ImmutableList;
......@@ -223,6 +224,7 @@ public class KeYMatcher implements MatcherApi<KeyData> {
s = s.replaceFirst("\\?", "");
}
va.declare(s, new TermType());
va.assign(s, Value.from(from(matched)));
System.out.println("Variable " + s + " : " + Value.from(from(matched)));
......@@ -259,7 +261,8 @@ public class KeYMatcher implements MatcherApi<KeyData> {
}
private TermLiteral from(Term t) {
return new TermLiteral(t.toString());
//TODO rewrite operator
return new TermLiteral(Utils.toPrettyTerm(t));
}
private TermLiteral from(SequentFormula sf) {
......
script cutTest(){
cut `p`;
//cases{
// case match `==>?X -> ?Y`:
//auto step=2;
//cut `p`;
cases{
case match `==>?X -> ?Y`:
//auto steps=100;
//cut formula=`?X`[];
cut `?Y`[];
//}
}
//cut #2=`p`;
//auto steps=100;
}
\ No newline at end of file
......@@ -437,7 +437,7 @@ public class ScriptArea extends CodeArea {
SequentFormula seqForm = tap.getPio().sequentFormula();
//transform term to parsable string representation
String term = Utils.toPrettyTerm(seqForm.formula());
String term = edu.kit.iti.formal.psdbg.termmatcher.Utils.toPrettyTerm(seqForm.formula());
String text = getText();
......
package edu.kit.iti.formal.psdbg.gui.controls;
import de.uka.ilkd.key.logic.Term;
import de.uka.ilkd.key.logic.op.Equality;
import de.uka.ilkd.key.logic.op.IProgramMethod;
import de.uka.ilkd.key.logic.op.Junctor;
import de.uka.ilkd.key.logic.op.Operator;
import de.uka.ilkd.key.pp.ProgramPrinter;
import de.uka.ilkd.key.speclang.Contract;
import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode;
......@@ -245,37 +241,7 @@ public class Utils {
* @param formula
* @return parsable Stringversion of Term
*/
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();
}
/* public static String toPrettyTerm(Term formula) {
return KeYUtils.toPrettyTerm(formula);
}*/
}
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