/* Copyright 2009-2014 EPFL, Lausanne */

package leon
package verification

import purescala.Definitions.FunDef

class VerificationReport(val fvcs: Map[FunDef, List[VerificationCondition]]) {
  import scala.math.Ordering.Implicits._
  val conditions : Seq[VerificationCondition] = fvcs.flatMap(_._2).toSeq.sortBy(vc => (vc.funDef.id.name, vc.kind.toString))

  lazy val totalConditions : Int = conditions.size

  lazy val totalTime : Double = conditions.foldLeft(0.0d)((t,c) => t + c.time.getOrElse(0.0d))

  lazy val totalValid : Int = conditions.count(_.value == Some(true))

  lazy val totalInvalid : Int = conditions.count(_.value == Some(false))

  lazy val totalUnknown : Int = conditions.count(_.value == None)

  def summaryString : String = if(totalConditions >= 0) {
    import utils.ASCIIHelpers._

    var t = Table("Verification Summary")

    t ++= conditions.map { vc =>
      val timeStr = vc.time.map(t => f"$t%-3.3f").getOrElse("")
      Row(Seq(
        Cell(vc.funDef.id.toString),
        Cell(vc.kind.name),
        Cell(vc.getPos),
        Cell(vc.status),
        Cell(vc.tacticStr),
        Cell(vc.solverStr),
        Cell(timeStr, align = Right)
      ))
    }

    t += Separator

    t += Row(Seq(
      Cell(f"total: $totalConditions%-4d   valid: $totalValid%-4d   invalid: $totalInvalid%-4d   unknown $totalUnknown%-4d", 6),
      Cell(f"$totalTime%7.3f", align = Right)
    ))

    t.render

  } else {
    "No verification conditions were analyzed."
  }
}