Migrated the pretty printing code from VerificationReport.scala to SelfPrettyPrinter.scala

src/main/scala/leon/purescala/SelfPrettyPrinter.scala

+package leon.purescala
+
+import leon.evaluators.StringTracingEvaluator
+import leon.purescala
+import purescala.Definitions.Program
+import leon.evaluators.StringTracingEvaluator
+import purescala.Expressions._
+import purescala.Types.StringType
+import leon.utils.DebugSectionSynthesis
+import leon.utils.DebugSectionVerification
+import leon.purescala.Quantification._
+import purescala.Constructors._
+import purescala.ExprOps._
+import purescala.Expressions.{Pattern, Expr}
+import purescala.Extractors._
+import purescala.TypeOps._
+import purescala.Types._
+import purescala.Common._
+import purescala.Expressions._
+import purescala.Definitions._
+import purescala.SelfPrettyPrinter
+import leon.solvers.{ HenkinModel, Model, SolverFactory }
+import leon.LeonContext
+import leon.evaluators
+
+/** This pretty-printer uses functions defined in Leon itself.
+  * If not pretty printing function is defined, return the default value instead
+  * @param The list of functions which should be excluded from pretty-printing (to avoid rendering counter-examples of toString methods using the method itself)
+  * @return a user defined string for the given typed expression. */
+object SelfPrettyPrinter {
+  def print(v: Expr, orElse: =>String, excluded: FunDef => Boolean = Set())(implicit ctx: LeonContext, program: Program): String = {
+    (program.definedFunctions find {
+      case fd if !excluded(fd) =>
+        fd.returnType == StringType && fd.params.length == 1 && TypeOps.isSubtypeOf(v.getType, fd.params.head.getType) && fd.id.name.toLowerCase().endsWith("tostring") &&
+        program.callGraph.transitiveCallees(fd).forall { fde => 
+          !purescala.ExprOps.exists( _.isInstanceOf[Choose])(fde.fullBody)
+        }
+    }) match {
+      case Some(fd) =>
+        //println("Found fd: " + fd.id.name)
+        val ste = new StringTracingEvaluator(ctx, program)
+        try {
+        val result = ste.eval(FunctionInvocation(fd.typed, Seq(v)))
+        
+        result.result match {
+          case Some((StringLiteral(res), _)) if res != "" =>
+            res
+          case _ =>
+            orElse
+        }
+        } catch {
+          case e: evaluators.ContextualEvaluator#EvalError =>
+            orElse
+        }
+      case None =>
+        orElse
+    }
+  }
+}
\ No newline at end of file

src/main/scala/leon/verification/VerificationCondition.scala

@@ -10,6 +10,7 @@ import leon.utils.Positioned
 import leon.evaluators.StringTracingEvaluator
 import leon.solvers._
 import leon.LeonContext
+import leon.purescala.SelfPrettyPrinter
 
 /** This is just to hold some history information. */
 case class VC(condition: Expr, fd: FunDef, kind: VCKind) extends Positioned {
@@ -63,7 +64,7 @@ case class VCResult(status: VCStatus, solvedWith: Option[Solver], timeMs: Option
         // is free to simplify
         val strings = cex.toSeq.sortBy(_._1.name).map {
           case (id, v) =>
-            (id.asString(context), VerificationReport.userDefinedString(v, PrettyPrinter(v))(vctx.context, vctx.program))
+            (id.asString(context), SelfPrettyPrinter.print(v, PrettyPrinter(v))(vctx.context, vctx.program))
         }
 
         if (strings.nonEmpty) {

src/main/scala/leon/verification/VerificationReport.scala

@@ -3,63 +3,28 @@
 package leon
 package verification
 
+import evaluators.StringTracingEvaluator
+import utils.DebugSectionSynthesis
+import utils.DebugSectionVerification
+import leon.purescala
 import purescala.Definitions.Program
-import leon.evaluators.StringTracingEvaluator
 import purescala.Expressions._
 import purescala.Types.StringType
-import leon.utils.DebugSectionSynthesis
-import leon.utils.DebugSectionVerification
-import leon.purescala.TypeOps
-
-import leon.purescala.Quantification._
+import purescala.TypeOps
+import purescala.Quantification._
 import purescala.Constructors._
 import purescala.ExprOps._
-import purescala.Expressions.Pattern
+import purescala.Expressions.{Pattern, Expr}
 import purescala.Extractors._
 import purescala.TypeOps._
 import purescala.Types._
 import purescala.Common._
 import purescala.Expressions._
 import purescala.Definitions._
+import purescala.SelfPrettyPrinter
 import leon.solvers.{ HenkinModel, Model, SolverFactory }
 
-object VerificationReport {
-  /** If it can be computed, returns a user defined string for the given expression
-    * @param The list of functions which should be excluded from pretty-printing (to avoid rendering counter-examples of toString methods using the method itself) */
-  def userDefinedString(v: Expr, orElse: =>String, excluded: FunDef => Boolean = Set())(ctx: LeonContext, program: Program): String = {
-    //println("Functions available:" + program.definedFunctions.map(fd => fd.id.name + "," + (fd.returnType == StringType) + ", " + (fd.params.length == 1) + "," + (fd.params.length == 1 && TypeOps.isSubtypeOf(v.getType, fd.params.head.getType)) + ", " + (if(fd.params.length == 1) fd.params.head.getType + " == " + v.getType else "")).mkString("\n"))
-    (program.definedFunctions find {
-      case fd if !excluded(fd) =>
-        fd.returnType == StringType && fd.params.length == 1 && TypeOps.isSubtypeOf(v.getType, fd.params.head.getType) && fd.id.name.toLowerCase().endsWith("tostring") &&
-        program.callGraph.transitiveCallees(fd).forall { fde => 
-          !purescala.ExprOps.exists( _.isInstanceOf[Choose])(fde.fullBody)
-        }
-    }) match {
-      case Some(fd) =>
-        //println("Found fd: " + fd.id.name)
-        val ste = new StringTracingEvaluator(ctx, program)
-        try {
-        val result = ste.eval(FunctionInvocation(fd.typed, Seq(v)))
-        
-        result.result match {
-          case Some((StringLiteral(res), _)) if res != "" =>
-            res
-          case _ =>
-            orElse
-        }
-        } catch {
-          case e: evaluators.ContextualEvaluator#EvalError =>
-            orElse
-        }
-      case None =>
-        //println("Function to render " + v + " not found")
-        orElse
-    }
-  }
-}
-
 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))
   }