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

disprover: add hypotheses, goal and result to log

parent 43f35f3d
No related branches found
No related tags found
No related merge requests found
...@@ -70,16 +70,23 @@ public class DisproverReasoner implements IReasoner { ...@@ -70,16 +70,23 @@ public class DisproverReasoner implements IReasoner {
private ICounterExample evaluateSequent(final IProverSequent sequent, private ICounterExample evaluateSequent(final IProverSequent sequent,
final DisproverReasonerInput disproverInput, IProofMonitor pm) final DisproverReasonerInput disproverInput, IProofMonitor pm)
throws ProBException, RodinDBException, InterruptedException { throws ProBException, RodinDBException, InterruptedException {
Logger.info("Calling Disprover on Sequent");
Set<Predicate> hypotheses = new HashSet<Predicate>(); Set<Predicate> hypotheses = new HashSet<Predicate>();
for (Predicate predicate : sequent.hypIterable()) { for (Predicate predicate : sequent.hypIterable()) {
hypotheses.add(predicate); hypotheses.add(predicate);
Logger.info("Disprover: Sending Hypothesis: "
+ predicate.toString());
} }
Predicate goal = sequent.goal(); Predicate goal = sequent.goal();
Logger.info("Disprover: Sending Goal: " + goal.toString());
IEventBRoot root = getRoot(sequent); IEventBRoot root = getRoot(sequent);
ICounterExample counterExample = DisproverCommand.disprove( ICounterExample counterExample = DisproverCommand.disprove(
Animator.getAnimator(), hypotheses, goal, root, pm); Animator.getAnimator(), hypotheses, goal, root, pm);
Logger.info("Disprover: Result: " + counterExample.toString());
return counterExample; return counterExample;
} }
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment