From 5298e191f1dc600220e5839859cb124eb536fc87 Mon Sep 17 00:00:00 2001
From: Sebastian Krings <sebastian@krin.gs>
Date: Fri, 21 Jun 2013 16:02:51 +0200
Subject: [PATCH] comment out some debugging code
---
.../core/internal/DisproverReasoner.java | 25 +++++++++----------
1 file changed, 12 insertions(+), 13 deletions(-)
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 ae80cf02..74298a6e 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
@@ -33,7 +33,6 @@ import de.prob.eventb.translator.PredicateVisitor;
import de.prob.exceptions.ProBException;
import de.prob.logging.Logger;
import de.prob.prolog.output.PrologTermStringOutput;
-import de.prob.unicode.UnicodeTranslator;
public class DisproverReasoner implements IReasoner {
@@ -71,7 +70,7 @@ public class DisproverReasoner implements IReasoner {
private ICounterExample evaluateSequent(final IProverSequent sequent,
final DisproverReasonerInput disproverInput, IProofMonitor pm)
throws ProBException, RodinDBException, InterruptedException {
- Logger.info("Calling Disprover on Sequent");
+ // Logger.info("Calling Disprover on Sequent");
Set<Predicate> hypotheses = new HashSet<Predicate>();
StringBuilder hypothesesString = new StringBuilder();
@@ -81,23 +80,23 @@ public class DisproverReasoner implements IReasoner {
hypothesesString.append(" & ");
}
- if (hypothesesString.length() == 0) {
- Logger.info("Disprover: No Hypotheses");
- } else {
- hypothesesString.delete(hypothesesString.length() - 2,
- hypothesesString.length());
- Logger.info("Disprover: Sending Hypotheses: "
- + UnicodeTranslator.toAscii(hypothesesString.toString()));
- }
+ /*
+ * if (hypothesesString.length() == 0) {
+ * Logger.info("Disprover: No Hypotheses"); } else {
+ * hypothesesString.delete(hypothesesString.length() - 2,
+ * hypothesesString.length());
+ * Logger.info("Disprover: Sending Hypotheses: " +
+ * UnicodeTranslator.toAscii(hypothesesString.toString())); }
+ */
Predicate goal = sequent.goal();
- Logger.info("Disprover: Sending Goal: "
- + UnicodeTranslator.toAscii(predicateToProlog(goal)));
+ // Logger.info("Disprover: Sending Goal: "+
+ // UnicodeTranslator.toAscii(predicateToProlog(goal)));
IEventBRoot root = getRoot(sequent);
ICounterExample counterExample = DisproverCommand.disprove(
Animator.getAnimator(), hypotheses, goal, root, pm);
- Logger.info("Disprover: Result: " + counterExample.toString());
+ // Logger.info("Disprover: Result: " + counterExample.toString());
return counterExample;
}
--
GitLab