From 9382c4cdc25d00713bb95ec4ed62286c4f439f53 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Fri, 21 Aug 2015 14:29:58 +0200
Subject: [PATCH] Mainly TerminationReport improvement
---
.../scala/leon/synthesis/ExamplesBank.scala | 12 ++---
.../leon/termination/ProcessingPipeline.scala | 2 -
.../leon/termination/TerminationPhase.scala | 2 +-
.../leon/termination/TerminationReport.scala | 48 +++++++++++--------
src/main/scala/leon/utils/ASCIIHelpers.scala | 3 +-
.../verification/VerificationReport.scala | 7 +--
6 files changed, 39 insertions(+), 35 deletions(-)
diff --git a/src/main/scala/leon/synthesis/ExamplesBank.scala b/src/main/scala/leon/synthesis/ExamplesBank.scala
index a0ed2936a..47b14d99b 100644
--- a/src/main/scala/leon/synthesis/ExamplesBank.scala
+++ b/src/main/scala/leon/synthesis/ExamplesBank.scala
@@ -22,9 +22,9 @@ case class ExamplesBank(valids: Seq[Example], invalids: Seq[Example]) {
evaluator.eval(functionInvocation(fd, ts.ins))
}
- val outInfo = (invalids.collect {
+ val outInfo = invalids.collect {
case InOutExample(ins, outs) => ins -> outs
- }).toMap
+ }.toMap
val callGraph = evaluator.fullCallGraph
@@ -50,15 +50,15 @@ case class ExamplesBank(valids: Seq[Example], invalids: Seq[Example]) {
def union(that: ExamplesBank) = {
ExamplesBank(
- distinctIns((this.valids union that.valids)),
- distinctIns((this.invalids union that.invalids))
+ distinctIns(this.valids union that.valids),
+ distinctIns(this.invalids union that.invalids)
)
}
private def distinctIns(s: Seq[Example]): Seq[Example] = {
- val insOuts = (s.collect {
+ val insOuts = s.collect {
case InOutExample(ins, outs) => ins -> outs
- }).toMap
+ }.toMap
s.map(_.ins).distinct.map {
case ins =>
diff --git a/src/main/scala/leon/termination/ProcessingPipeline.scala b/src/main/scala/leon/termination/ProcessingPipeline.scala
index 0dbdb9bd0..6e7da22ce 100644
--- a/src/main/scala/leon/termination/ProcessingPipeline.scala
+++ b/src/main/scala/leon/termination/ProcessingPipeline.scala
@@ -213,5 +213,3 @@ abstract class ProcessingPipeline(context: LeonContext, initProgram: Program) ex
}
}
}
-
-// vim: set ts=4 sw=4 et:
diff --git a/src/main/scala/leon/termination/TerminationPhase.scala b/src/main/scala/leon/termination/TerminationPhase.scala
index a9f7ef77b..fbfcde51e 100644
--- a/src/main/scala/leon/termination/TerminationPhase.scala
+++ b/src/main/scala/leon/termination/TerminationPhase.scala
@@ -30,6 +30,6 @@ object TerminationPhase extends LeonPhase[Program,TerminationReport] {
}
val endTime = System.currentTimeMillis
- new TerminationReport(results, (endTime - startTime).toDouble / 1000.0d)
+ new TerminationReport(ctx, results, (endTime - startTime).toDouble / 1000.0d)
}
}
diff --git a/src/main/scala/leon/termination/TerminationReport.scala b/src/main/scala/leon/termination/TerminationReport.scala
index f9dbb49a7..57c3c03ae 100644
--- a/src/main/scala/leon/termination/TerminationReport.scala
+++ b/src/main/scala/leon/termination/TerminationReport.scala
@@ -4,28 +4,38 @@ package leon
package termination
import purescala.Definitions._
+import utils.ASCIIHelpers._
+
+case class TerminationReport(ctx: LeonContext, results : Seq[(FunDef,TerminationGuarantee)], time : Double) {
-case class TerminationReport(results : Seq[(FunDef,TerminationGuarantee)], time : Double) {
def summaryString : String = {
- val sb = new StringBuilder
- sb.append("─────────────────────\n")
- sb.append(" Termination summary \n")
- sb.append("─────────────────────\n\n")
- for((fd,g) <- results) {
- val result = if (g.isGuaranteed) "\u2713" else "\u2717"
- val toPrint = g match {
- case LoopsGivenInputs(reason, args) =>
- "Non-terminating for call: " + args.mkString(fd.id+"(", ",", ")")
- case CallsNonTerminating(funDefs) =>
- "Calls non-terminating functions " + funDefs.map(_.id).mkString(",")
- case Terminates(reason) =>
- "Terminates (" + reason + ")"
- case _ => g.toString
+ var t = Table("Termination summary")
+
+ for ((fd, g) <- results) t += Row(Seq(
+ Cell(fd.id.asString(ctx)),
+ Cell {
+ val result = if (g.isGuaranteed) "\u2713" else "\u2717"
+ val verdict = g match {
+ case LoopsGivenInputs(reason, args) =>
+ "Non-terminating for call: " + args.mkString(fd.id + "(", ",", ")")
+ case CallsNonTerminating(funDefs) =>
+ "Calls non-terminating functions " + funDefs.map(_.id).mkString(",")
+ case Terminates(reason) =>
+ "Terminates (" + reason + ")"
+ case _ => g.toString
+ }
+ s"$result $verdict"
}
- sb.append(f"- ${fd.id.name}%-30s $result $toPrint%-30s\n")
- }
- sb.append(f"\n[Analysis time: $time%7.3f]\n")
- sb.toString
+ ))
+
+ t += Separator
+
+ t += Row(Seq(Cell(
+ f"Analysis time: $time%7.3f",
+ spanning = 2
+ )))
+
+ t.render
}
def evaluationString : String = {
diff --git a/src/main/scala/leon/utils/ASCIIHelpers.scala b/src/main/scala/leon/utils/ASCIIHelpers.scala
index 4cf63fe22..a2750e423 100644
--- a/src/main/scala/leon/utils/ASCIIHelpers.scala
+++ b/src/main/scala/leon/utils/ASCIIHelpers.scala
@@ -8,7 +8,7 @@ object ASCIIHelpers {
def ++(rs: Iterable[TableRow]): Table = copy(rows = rows ++ rs)
- def computeColumnSizes = {
+ private def computeColumnSizes = {
// First check constraints
var constraints = Map[(Int, Int), Int]()
@@ -121,7 +121,6 @@ object ASCIIHelpers {
case object Left extends Alignment
case object Right extends Alignment
-
case class Cell(v: Any, spanning: Int = 1, align: Alignment = Left) {
require(spanning >= 1)
diff --git a/src/main/scala/leon/verification/VerificationReport.scala b/src/main/scala/leon/verification/VerificationReport.scala
index 43f6aacb8..18ae32c89 100644
--- a/src/main/scala/leon/verification/VerificationReport.scala
+++ b/src/main/scala/leon/verification/VerificationReport.scala
@@ -3,12 +3,9 @@
package leon
package verification
-import VCKinds._
-import VCStatus._
+import purescala.Definitions.Program
-import purescala.Definitions.{FunDef, Program}
-
-case class VerificationReport(val program: Program, val results: Map[VC, Option[VCResult]]) {
+case class VerificationReport(program: Program, results: Map[VC, Option[VCResult]]) {
val vrs: Seq[(VC, VCResult)] = results.toSeq.sortBy { case (vc, _) => (vc.fd.id.name, vc.kind.toString) }.map {
case (vc, or) => (vc, or.getOrElse(VCResult.unknown))
--
GitLab