From b754c03a5f507e78ec396d3a22e628f8b459bdab Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Thu, 5 Jun 2014 19:05:08 +0200
Subject: [PATCH] Proper handling of ASCII tables
---
src/main/scala/leon/utils/ASCIITable.scala | 122 ++++++++++++++++++
.../verification/VerificationReport.scala | 59 ++++-----
2 files changed, 145 insertions(+), 36 deletions(-)
create mode 100644 src/main/scala/leon/utils/ASCIITable.scala
diff --git a/src/main/scala/leon/utils/ASCIITable.scala b/src/main/scala/leon/utils/ASCIITable.scala
new file mode 100644
index 000000000..0daba6f96
--- /dev/null
+++ b/src/main/scala/leon/utils/ASCIITable.scala
@@ -0,0 +1,122 @@
+package leon.utils
+
+object ASCIITables {
+ case class Table(title: String, rows: Seq[TableRow] = Nil) {
+ def +(r: TableRow): Table = this ++ Seq(r)
+ def ++(rs: Iterable[TableRow]): Table = copy(rows = rows ++ rs)
+
+
+ def computeColumnSizes = {
+ // First check constraints
+ var constraints = Map[(Int, Int), Int]()
+
+ var cellsPerRow = 0
+ for((r, i) <- rows.zipWithIndex) r match {
+ case r @ Row(cells) =>
+ if (cellsPerRow > 0) {
+ assert(r.cellsSize == cellsPerRow, "Row $i has incompatible number of virtual cells (${r.cellsSize} v.s. $cellsPerRow")
+ } else {
+ cellsPerRow = r.cellsSize
+ constraints += (0, cellsPerRow-1) -> 80
+ }
+
+ var i = 0
+ for (c <- cells) {
+ val k = i -> (i+c.spanning-1)
+
+ val cols = constraints.getOrElse(k, 1)
+
+ val size = c.vString.size
+
+ constraints += k -> (cols max size)
+
+ i += c.spanning
+ }
+ case _ =>
+ }
+
+ // discharge constraints that are spanning
+ val toRemove = constraints.keySet.filter { case (from, to) => from != to }.toSeq.sortBy{ s => s._2 - s._1 }
+
+ for (k @ (from, to) <- toRemove) {
+ val min = constraints(k)
+
+ val parts = (from to to).map(i => constraints((i, i)))
+
+ var sum = parts.sum
+
+ if (sum < min) {
+ var remaining = min - sum
+
+ for ((s, i) <- parts.zipWithIndex.sortBy(- _._1)) {
+ val inc = Math.round(s*remaining*1d/sum).toInt
+ constraints += (from+i, from+i) -> (s + inc)
+ remaining -= inc
+ sum -= s
+ }
+ }
+
+ constraints -= k
+ }
+
+ (0 until cellsPerRow).map(i => constraints((i, i)))
+ }
+
+ def render: String = {
+ val colSizes = computeColumnSizes
+
+ val fullWidth = colSizes.sum + colSizes.size*2
+
+ val sb = new StringBuffer
+
+ sb append " ┌─"+("─"*title.size)+"─┐\n"
+ sb append "╔═╡ "+ title +" ╞" + ("═" * (fullWidth-title.size-5)) + "╗\n"
+ sb append "║ └─"+("─"*title.size)+"─┘" + (" " * (fullWidth-title.size-5)) + "║\n"
+
+ for (r <- rows) r match {
+ case Separator =>
+ sb append "╟" + ("┄" * fullWidth) + "╢\n"
+
+ case Row(cells) =>
+ sb append "║ "
+ var i = 0
+ for (c <- cells) {
+ if (i > 0) {
+ sb append " "
+ }
+ val size = (i to i+c.spanning-1).map(colSizes).sum + (c.spanning-1) * 2
+
+ if (c.align == Left) {
+ sb append ("%-"+size+"s").format(c.vString)
+ } else {
+ sb append ("%"+size+"s").format(c.vString)
+ }
+
+ i += c.spanning
+ }
+ sb append " ║\n"
+ }
+
+ sb append "╚" + ("═" * fullWidth) + "╝"
+
+ sb.toString
+ }
+ }
+
+ abstract class TableRow
+ case object Separator extends TableRow
+ case class Row(cells: Seq[Cell]) extends TableRow {
+ def cellsSize = {
+ cells.map(_.spanning).sum
+ }
+ }
+ sealed abstract class Alignment
+ case object Left extends Alignment
+ case object Right extends Alignment
+
+
+ case class Cell(v: Any, spanning: Int = 1, align: Alignment = Left) {
+ lazy val vString = v.toString
+ }
+
+}
diff --git a/src/main/scala/leon/verification/VerificationReport.scala b/src/main/scala/leon/verification/VerificationReport.scala
index 01b129d77..b884d229e 100644
--- a/src/main/scala/leon/verification/VerificationReport.scala
+++ b/src/main/scala/leon/verification/VerificationReport.scala
@@ -20,45 +20,32 @@ class VerificationReport(val fvcs: Map[FunDef, List[VerificationCondition]]) {
lazy val totalUnknown : Int = conditions.count(_.value == None)
def summaryString : String = if(totalConditions >= 0) {
- VerificationReport.infoHeader +
- conditions.map(VerificationReport.infoLine).mkString("\n", "\n", "\n") +
- VerificationReport.infoSep +
- ("║ total: %-4d valid: %-4d invalid: %-4d unknown %-4d " +
- (" " * 16) +
- " %7.3f ║\n").format(totalConditions, totalValid, totalInvalid, totalUnknown, totalTime) +
- VerificationReport.infoFooter
- } else {
- "No verification conditions were analyzed."
- }
-}
-
-object VerificationReport {
- def emptyReport : VerificationReport = new VerificationReport(Map())
-
- private def fit(str : String, maxLength : Int) : String = {
- if(str.length <= maxLength) {
- str
- } else {
- str.substring(0, maxLength - 1) + "…"
+ import utils.ASCIITables._
+
+ var t = Table("Verification Summary")
+
+ t ++= conditions.map { vc =>
+ val timeStr = vc.time.map(t => "%-3.3f".format(t)).getOrElse("")
+ Row(Seq(
+ Cell(vc.funDef.id.toString),
+ Cell(vc.kind),
+ Cell(vc.status),
+ Cell(vc.tacticStr),
+ Cell(vc.solverStr),
+ Cell(timeStr, align = Right)
+ ))
}
- }
- private val infoSep : String = "╟" + ("┄" * 83) + "╢\n"
- private val infoFooter : String = "╚" + ("═" * 83) + "╝"
- private val infoHeader : String = ". ┌─────────┐\n" +
- "╔═╡ Summary ╞" + ("═" * 71) + "╗\n" +
- "║ └─────────┘" + (" " * 71) + "║"
+ t += Separator
+
+ t += Row(Seq(
+ Cell(f"total: $totalConditions%-4d valid: $totalValid%-4d invalid: $totalInvalid%-4d unknown $totalUnknown%-4d", 5),
+ Cell(f"$totalTime%7.3f", align = Right)
+ ))
- private def infoLine(vc : VerificationCondition) : String = {
- val timeStr = vc.time.map(t => "%-3.3f".format(t)).getOrElse("")
+ t.render
- "║ %-25s %-9s %9s %-8s %-10s %-7s %7s ║".format(
- fit(vc.funDef.id.toString, 25),
- vc.kind,
- vc.getPos,
- vc.status,
- vc.tacticStr,
- vc.solverStr,
- timeStr)
+ } else {
+ "No verification conditions were analyzed."
}
}
--
GitLab