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

further refactoring: move fetching hypothesis from rodin directly into the reasoner.

parent a229ca36
No related branches found
No related tags found
No related merge requests found
...@@ -48,16 +48,6 @@ public class DisproverReasonerInput implements IReasonerInput { ...@@ -48,16 +48,6 @@ public class DisproverReasonerInput implements IReasonerInput {
return node; return node;
} }
/**
* @param sequent
* , the sequent to prove
* @return the required Hypothesis, depending on {@link #mode}.
* @throws DisproverException
*/
public Iterable<Predicate> getHypotheses(IProverSequent sequent) {
return sequent.visibleHypIterable();
}
public int getMaxInt() { public int getMaxInt() {
return maxInt; return maxInt;
} }
......
...@@ -66,7 +66,7 @@ public class DisproverReasoner implements IReasoner { ...@@ -66,7 +66,7 @@ public class DisproverReasoner implements IReasoner {
RodinDBException { RodinDBException {
Set<Predicate> hypotheses = new HashSet<Predicate>(); Set<Predicate> hypotheses = new HashSet<Predicate>();
for (Predicate predicate : disproverInput.getHypotheses(sequent)) { for (Predicate predicate : sequent.visibleHypIterable()) {
hypotheses.add(predicate); hypotheses.add(predicate);
} }
Predicate goal = sequent.goal(); Predicate goal = sequent.goal();
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment