Skip to content
Snippets Groups Projects
Commit 85018eaf authored by Sebastian Krings's avatar Sebastian Krings
Browse files

fix null-pointer occurring if Rodin tries to restore serialised disprover reasoner input

parent dbf77a94
No related branches found
No related tags found
No related merge requests found
package de.prob.eventb.disprover.core; package de.prob.eventb.disprover.core;
import org.eventb.core.seqprover.IProofTreeNode;
import org.eventb.core.seqprover.IReasonerInput; import org.eventb.core.seqprover.IReasonerInput;
import org.eventb.core.seqprover.proofBuilder.ReplayHints; import org.eventb.core.seqprover.proofBuilder.ReplayHints;
...@@ -13,13 +12,6 @@ import org.eventb.core.seqprover.proofBuilder.ReplayHints; ...@@ -13,13 +12,6 @@ import org.eventb.core.seqprover.proofBuilder.ReplayHints;
* @author jastram * @author jastram
*/ */
public class DisproverReasonerInput implements IReasonerInput { public class DisproverReasonerInput implements IReasonerInput {
private final IProofTreeNode node;
public DisproverReasonerInput(IProofTreeNode node) {
this.node = node;
}
@Override @Override
public void applyHints(ReplayHints renaming) { public void applyHints(ReplayHints renaming) {
// TODO Auto-generated method stub // TODO Auto-generated method stub
...@@ -37,7 +29,4 @@ public class DisproverReasonerInput implements IReasonerInput { ...@@ -37,7 +29,4 @@ public class DisproverReasonerInput implements IReasonerInput {
return false; return false;
} }
public IProofTreeNode getProofTreeNode() {
return node;
}
} }
...@@ -70,7 +70,7 @@ public class DisproverReasoner implements IReasoner { ...@@ -70,7 +70,7 @@ public class DisproverReasoner implements IReasoner {
RodinDBException { RodinDBException {
Set<Predicate> hypotheses = new HashSet<Predicate>(); Set<Predicate> hypotheses = new HashSet<Predicate>();
for (Predicate predicate : sequent.visibleHypIterable()) { for (Predicate predicate : sequent.hypIterable()) {
hypotheses.add(predicate); hypotheses.add(predicate);
} }
Predicate goal = sequent.goal(); Predicate goal = sequent.goal();
...@@ -139,7 +139,7 @@ public class DisproverReasoner implements IReasoner { ...@@ -139,7 +139,7 @@ public class DisproverReasoner implements IReasoner {
@Override @Override
public IReasonerInput deserializeInput(final IReasonerInputReader reader) public IReasonerInput deserializeInput(final IReasonerInputReader reader)
throws SerializeException { throws SerializeException {
return null; return new DisproverReasonerInput();
} }
@Override @Override
......
...@@ -36,7 +36,7 @@ public class DisproverTacticProvider extends DefaultTacticProvider { ...@@ -36,7 +36,7 @@ public class DisproverTacticProvider extends DefaultTacticProvider {
public ITactic getTactic(IProofTreeNode node, String globalInput, public ITactic getTactic(IProofTreeNode node, String globalInput,
String[] inputs) { String[] inputs) {
IReasonerInput reasonerInput = new DisproverReasonerInput(node); IReasonerInput reasonerInput = new DisproverReasonerInput();
return BasicTactics.reasonerTac( return BasicTactics.reasonerTac(
Disprover.createDisproverReasoner(), reasonerInput); Disprover.createDisproverReasoner(), reasonerInput);
} }
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment