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 67dc3d738b4cdfcbafd664759d60748daf16954c..b5ea4b4d54d892c2eb5becd305b60578952e8a7f 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 33182f247786cbc028ee13f7d28685a3e95dde8d..0d92a9fce10f6a4cb8d62ef811fefb02ffefbc10 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 ef32b314c486f00004fca7f726d6ed34184f2174..4a7f8d2fcc8f0d61e51139220aeaf41e9a8228ed 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); }