Commit 3129e863 authored by Sarah Grebing's avatar Sarah Grebing

Bugfix in deepcopy of goal nodes: showed itself wehn using variables declared...

Bugfix in deepcopy of goal nodes: showed itself wehn using variables declared before a try statement
parent e3b05097
Pipeline #20986 canceled with stages
...@@ -99,7 +99,6 @@ public class KeyInterpreter extends Interpreter<KeyData> { ...@@ -99,7 +99,6 @@ public class KeyInterpreter extends Interpreter<KeyData> {
logger.debug(String.format("Beginning of suspicion execution of %s", statements)); logger.debug(String.format("Beginning of suspicion execution of %s", statements));
GoalNode<KeyData> goalNode = getSelectedNode(); GoalNode<KeyData> goalNode = getSelectedNode();
pushState(new State<>(goalNode.deepCopy())); // copy for later prove pushState(new State<>(goalNode.deepCopy())); // copy for later prove
List<Visitor> backupExitListener = getExitListeners(), List<Visitor> backupExitListener = getExitListeners(),
backupEntryListener = getEntryListeners(); backupEntryListener = getEntryListeners();
try { try {
......
...@@ -454,13 +454,13 @@ public class Interpreter<T> extends DefaultASTVisitor<Object> ...@@ -454,13 +454,13 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
exitScope(casesStatement); exitScope(casesStatement);
return null; return null;
}*/ }*/
@Override /* @Override
public Object visit(TryCase TryCase) { public Object visit(TryCase TryCase) {
enterScope(TryCase); enterScope(TryCase);
//is handled by KeYInterpreter
exitScope(TryCase); exitScope(TryCase);
return false; return false;
} }*/
/** /**
* Evaluate a match in a specific goal * Evaluate a match in a specific goal
......
...@@ -29,7 +29,7 @@ public class GoalNode<T> { ...@@ -29,7 +29,7 @@ public class GoalNode<T> {
private boolean isClosed; private boolean isClosed;
/** /**
* This conctructur will be replaced with concrete one that uses projectedNode *
* *
* @param parent * @param parent
* @param data * @param data
...@@ -41,6 +41,12 @@ public class GoalNode<T> { ...@@ -41,6 +41,12 @@ public class GoalNode<T> {
this.data = data; this.data = data;
this.isClosed = isClosed; this.isClosed = isClosed;
} }
private GoalNode(GoalNode<T> parent, VariableAssignment assignments, T data, boolean isClosed) {
this.assignments = assignments.deepCopy();
this.parent = parent;
this.data = data;
this.isClosed = isClosed;
}
/** /**
* @param varname * @param varname
...@@ -104,8 +110,13 @@ public class GoalNode<T> { ...@@ -104,8 +110,13 @@ public class GoalNode<T> {
} }
public GoalNode<T> deepCopy() { public GoalNode<T> deepCopy() {
//TODO method does nothing helpful atm if (parent != null) {
return new GoalNode<T>(parent, data, isClosed); return new GoalNode<T>(parent.deepCopy(), data, isClosed);
} else {
return new GoalNode<T>(parent, assignments.deepCopy(), data, isClosed);
}
} }
public VariableAssignment enterScope(VariableAssignment va) { public VariableAssignment enterScope(VariableAssignment va) {
......
...@@ -280,7 +280,7 @@ public class ScriptArea extends BorderPane { ...@@ -280,7 +280,7 @@ public class ScriptArea extends BorderPane {
LOGGER.debug("ScriptArea.updateMainScriptMarker"); LOGGER.debug("ScriptArea.updateMainScriptMarker");
if (ms != null && filePath.get().getAbsolutePath().equals(ms.getSourceName())) { if (ms != null && filePath.get().getAbsolutePath().equals(ms.getSourceName())) {
System.out.println(ms); LOGGER.debug("ScriptArea.updateIdentifier"+ ms);
CharStream stream = CharStreams.fromString(codeArea.getText(), filePath.get().getAbsolutePath()); CharStream stream = CharStreams.fromString(codeArea.getText(), filePath.get().getAbsolutePath());
Optional<ProofScript> ps = ms.find(Facade.getAST(stream)); Optional<ProofScript> ps = ms.find(Facade.getAST(stream));
......
...@@ -217,7 +217,7 @@ public class SequentView extends CodeArea { ...@@ -217,7 +217,7 @@ public class SequentView extends CodeArea {
Match va = m.getMatchings().iterator().next(); Match va = m.getMatchings().iterator().next();
//System.out.println(va);//TODO remove //System.out.println(va);//TODO remove
for (MatchPath mp : va.values()) { for (MatchPath mp : va.values()) {
System.out.println(mp.pio()); System.out.println("SequentView"+ mp.pio());
highlightTerm(mp.pio()); highlightTerm(mp.pio());
} }
} }
......
...@@ -256,9 +256,9 @@ public class Utils { ...@@ -256,9 +256,9 @@ public class Utils {
alert.setTitle("Proof Closed"); alert.setTitle("Proof Closed");
alert.setHeaderText("The proof is closed"); alert.setHeaderText("The proof is closed");
alert.setContentText("The proof using " + scriptName + " is closed"); alert.setContentText("The proof using " + scriptName + " is closed");
alert.setWidth(400); alert.setWidth(500);
alert.setHeight(400); alert.setHeight(400);
alert.setResizable(true);
/*StringWriter sw = new StringWriter(); /*StringWriter sw = new StringWriter();
PrintWriter pw = new PrintWriter(sw); PrintWriter pw = new PrintWriter(sw);
ex.printStackTrace(pw); ex.printStackTrace(pw);
...@@ -318,7 +318,7 @@ public class Utils { ...@@ -318,7 +318,7 @@ public class Utils {
public static void intoClipboard(String s) { public static void intoClipboard(String s) {
Map<DataFormat, Object> map = Collections.singletonMap(DataFormat.PLAIN_TEXT, s); Map<DataFormat, Object> map = Collections.singletonMap(DataFormat.PLAIN_TEXT, s);
Clipboard.getSystemClipboard().setContent(map); Clipboard.getSystemClipboard().setContent(map);
System.err.println(s); logger.info("Clipboard "+s);
} }
/** /**
......
// Please select one of the following scripts. // Please select one of the following scripts.
// //
script testTry(){
cases{
try: impLeft;
default:
__KEY_MAX_STEPS:= 100;
impRight;
}
}
script testSMT(){ script testSMT(){
smt solver='Z3'; smt solver='Z3';
} }
......
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