From 85018eaf05c4c12727e8f5f443d186b2e6d9d7de Mon Sep 17 00:00:00 2001
From: Sebastian Krings <sebastian@krin.gs>
Date: Tue, 14 May 2013 16:09:13 +0200
Subject: [PATCH] fix null-pointer occurring if Rodin tries to restore
serialised disprover reasoner input
---
.../eventb/disprover/core/DisproverReasonerInput.java | 11 -----------
.../disprover/core/internal/DisproverReasoner.java | 4 ++--
.../eventb/disprover/ui/DisproverTacticProvider.java | 2 +-
3 files changed, 3 insertions(+), 14 deletions(-)
diff --git a/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/DisproverReasonerInput.java b/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/DisproverReasonerInput.java
index 67dc3d73..b5ea4b4d 100644
--- a/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/DisproverReasonerInput.java
+++ b/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/DisproverReasonerInput.java
@@ -1,6 +1,5 @@
package de.prob.eventb.disprover.core;
-import org.eventb.core.seqprover.IProofTreeNode;
import org.eventb.core.seqprover.IReasonerInput;
import org.eventb.core.seqprover.proofBuilder.ReplayHints;
@@ -13,13 +12,6 @@ import org.eventb.core.seqprover.proofBuilder.ReplayHints;
* @author jastram
*/
public class DisproverReasonerInput implements IReasonerInput {
-
- private final IProofTreeNode node;
-
- public DisproverReasonerInput(IProofTreeNode node) {
- this.node = node;
- }
-
@Override
public void applyHints(ReplayHints renaming) {
// TODO Auto-generated method stub
@@ -37,7 +29,4 @@ public class DisproverReasonerInput implements IReasonerInput {
return false;
}
- public IProofTreeNode getProofTreeNode() {
- return node;
- }
}
diff --git a/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/internal/DisproverReasoner.java b/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/internal/DisproverReasoner.java
index 33182f24..0d92a9fc 100644
--- a/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/internal/DisproverReasoner.java
+++ b/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/internal/DisproverReasoner.java
@@ -70,7 +70,7 @@ public class DisproverReasoner implements IReasoner {
RodinDBException {
Set<Predicate> hypotheses = new HashSet<Predicate>();
- for (Predicate predicate : sequent.visibleHypIterable()) {
+ for (Predicate predicate : sequent.hypIterable()) {
hypotheses.add(predicate);
}
Predicate goal = sequent.goal();
@@ -139,7 +139,7 @@ public class DisproverReasoner implements IReasoner {
@Override
public IReasonerInput deserializeInput(final IReasonerInputReader reader)
throws SerializeException {
- return null;
+ return new DisproverReasonerInput();
}
@Override
diff --git a/de.prob.eventb.disprover.ui/src/de/prob/eventb/disprover/ui/DisproverTacticProvider.java b/de.prob.eventb.disprover.ui/src/de/prob/eventb/disprover/ui/DisproverTacticProvider.java
index ef32b314..4a7f8d2f 100644
--- a/de.prob.eventb.disprover.ui/src/de/prob/eventb/disprover/ui/DisproverTacticProvider.java
+++ b/de.prob.eventb.disprover.ui/src/de/prob/eventb/disprover/ui/DisproverTacticProvider.java
@@ -36,7 +36,7 @@ public class DisproverTacticProvider extends DefaultTacticProvider {
public ITactic getTactic(IProofTreeNode node, String globalInput,
String[] inputs) {
- IReasonerInput reasonerInput = new DisproverReasonerInput(node);
+ IReasonerInput reasonerInput = new DisproverReasonerInput();
return BasicTactics.reasonerTac(
Disprover.createDisproverReasoner(), reasonerInput);
}
--
GitLab