From 00b29af50b4c66199ac0f2eb336d159cb7dc38b4 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Tue, 19 May 2015 13:42:51 +0200
Subject: [PATCH] Crop preconditions when printing
---
src/main/scala/leon/verification/DefaultTactic.scala | 4 ++--
src/main/scala/leon/verification/InductionTactic.scala | 5 ++++-
src/main/scala/leon/verification/Tactic.scala | 7 +++++++
3 files changed, 13 insertions(+), 3 deletions(-)
diff --git a/src/main/scala/leon/verification/DefaultTactic.scala b/src/main/scala/leon/verification/DefaultTactic.scala
index 415f4edaa..a1cb99a49 100644
--- a/src/main/scala/leon/verification/DefaultTactic.scala
+++ b/src/main/scala/leon/verification/DefaultTactic.scala
@@ -33,8 +33,8 @@ class DefaultTactic(vctx: VerificationContext) extends Tactic(vctx) {
case ((fi @ FunctionInvocation(tfd, args), pre), path) =>
val pre2 = replaceFromIDs((tfd.params.map(_.id) zip args).toMap, pre)
val vc = implies(and(precOrTrue(fd), path), pre2)
-
- VC(vc, fd, VCKinds.Info(VCKinds.Precondition, s"call $fi"), this).setPos(fi)
+ val fiS = exprToShortString(fi)
+ VC(vc, fd, VCKinds.Info(VCKinds.Precondition, s"call $fiS"), this).setPos(fi)
}
case None =>
diff --git a/src/main/scala/leon/verification/InductionTactic.scala b/src/main/scala/leon/verification/InductionTactic.scala
index 27facb188..4fc868f9e 100644
--- a/src/main/scala/leon/verification/InductionTactic.scala
+++ b/src/main/scala/leon/verification/InductionTactic.scala
@@ -77,7 +77,10 @@ class InductionTactic(vctx: VerificationContext) extends DefaultTactic(vctx) {
val vc = implies(and(CaseClassInstanceOf(cct, arg.toVariable), precOrTrue(fd), path), implies(andJoin(subCases), replace((tfd.params.map(_.toVariable) zip args).toMap, pre)))
- VC(vc, fd, VCKinds.Info(VCKinds.Precondition, "call $fi, ind. on $arg / ${cct.classDef.id}"), this).setPos(fi)
+ // Crop the call to display it properly
+ val fiS = exprToShortString(fi)
+
+ VC(vc, fd, VCKinds.Info(VCKinds.Precondition, "call $fiS, ind. on ($arg : ${cct.classDef.id)}"), this).setPos(fi)
}
}
diff --git a/src/main/scala/leon/verification/Tactic.scala b/src/main/scala/leon/verification/Tactic.scala
index 7462818fb..0571e3242 100644
--- a/src/main/scala/leon/verification/Tactic.scala
+++ b/src/main/scala/leon/verification/Tactic.scala
@@ -31,4 +31,11 @@ abstract class Tactic(vctx: VerificationContext) {
protected def collectWithPC[T](f: PartialFunction[Expr, T])(expr: Expr): Seq[(T, Expr)] = {
CollectorWithPaths(f).traverse(expr)
}
+
+ protected def exprToShortString(e: Expr) = {
+ // Crop the call to display it properly
+ val eS = e.toString
+ val s = eS.takeWhile(_ != '\n').take(35)
+ if (s == eS) s else s ++ " ..."
+ }
}
--
GitLab