From 22d32e7a5a3fe99a5f11a46668479f8232faa7d8 Mon Sep 17 00:00:00 2001
From: Sebastian Krings <sebastian@krin.gs>
Date: Thu, 6 Jun 2013 13:44:33 +0200
Subject: [PATCH] convert disprover log output to ascii
---
.../disprover/core/internal/DisproverReasoner.java | 14 +++++++++++---
1 file changed, 11 insertions(+), 3 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 ca5c5cce..90e22861 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
@@ -30,6 +30,7 @@ import de.prob.core.PrologException;
import de.prob.eventb.disprover.core.DisproverReasonerInput;
import de.prob.exceptions.ProBException;
import de.prob.logging.Logger;
+import de.prob.unicode.UnicodeTranslator;
public class DisproverReasoner implements IReasoner {
@@ -73,13 +74,20 @@ public class DisproverReasoner implements IReasoner {
Logger.info("Calling Disprover on Sequent");
Set<Predicate> hypotheses = new HashSet<Predicate>();
+ StringBuilder hypothesesString = new StringBuilder();
for (Predicate predicate : sequent.hypIterable()) {
hypotheses.add(predicate);
- Logger.info("Disprover: Sending Hypothesis: "
- + predicate.toString());
+ hypothesesString.append(predicate.toString());
+ hypothesesString.append(" & ");
}
+ 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: " + goal.toString());
+ Logger.info("Disprover: Sending Goal: "
+ + UnicodeTranslator.toAscii(goal.toString()));
IEventBRoot root = getRoot(sequent);
--
GitLab