From 053c4545c66929148a4d9c5641bb288b5b6757bc Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Mon, 1 Jun 2015 16:42:13 +0200
Subject: [PATCH] Only generate one vc per function group in GroupedTactic
---
.../scala/leon/purescala/Extractors.scala | 1 -
.../scala/leon/synthesis/Synthesizer.scala | 1 -
.../scala/leon/utils/PreprocessingPhase.scala | 1 -
.../leon/verification/GroupedTactic.scala | 40 +++++++++++--------
4 files changed, 23 insertions(+), 20 deletions(-)
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index 0bacc4a72..9fb28e66d 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -6,7 +6,6 @@ package purescala
import Expressions._
import Common._
import Types._
-import Definitions._
import Constructors._
import ExprOps._
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 48624c809..4fa399f7a 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -10,7 +10,6 @@ import purescala.Expressions._
import purescala.Constructors._
import purescala.ScalaPrinter
import solvers._
-import solvers.z3._
import scala.concurrent.duration._
diff --git a/src/main/scala/leon/utils/PreprocessingPhase.scala b/src/main/scala/leon/utils/PreprocessingPhase.scala
index 7802d4509..60c270248 100644
--- a/src/main/scala/leon/utils/PreprocessingPhase.scala
+++ b/src/main/scala/leon/utils/PreprocessingPhase.scala
@@ -4,7 +4,6 @@ package leon
package utils
import purescala.Definitions.Program
-import purescala.ScalaPrinter
import purescala.{MethodLifting, CompleteAbstractDefinitions,CheckADTFieldsTypes}
import synthesis.{ConvertWithOracle, ConvertHoles}
diff --git a/src/main/scala/leon/verification/GroupedTactic.scala b/src/main/scala/leon/verification/GroupedTactic.scala
index 4a551a267..02da7e55b 100644
--- a/src/main/scala/leon/verification/GroupedTactic.scala
+++ b/src/main/scala/leon/verification/GroupedTactic.scala
@@ -3,6 +3,7 @@
package leon
package verification
+import leon.utils.NoPosition
import purescala.Expressions._
import purescala.ExprOps._
import purescala.Definitions._
@@ -12,23 +13,28 @@ class GroupedTactic(vctx: VerificationContext) extends Tactic(vctx) {
val description = "Default verification condition generation approach"
def generatePostconditions(fd: FunDef): Seq[VC] = {
- fd.postcondition map { post =>
- val perFunc = for {
- inComp <- vctx.program.callGraph.stronglyConnectedComponent(fd)
- p <- inComp.postcondition
- b <- inComp.body
- } yield {
- implies(
- precOrTrue(inComp),
- // @mk: Don't know which one is better. Inline the body, or have it as a fun. app?
- //application(p, Seq(b))
- application(p, Seq(FunctionInvocation(inComp.typedWithDef, inComp.params map { _.toVariable })))
- )
- }
-
- VC(andJoin(perFunc.toSeq), fd, VCKinds.Postcondition, this).setPos(post)
- }
- }.toSeq
+ // We collectively generate postconditions for a scc of the call graph.
+ // To not repeat vcs, we follow the convention to generate them for the first
+ // FunDef of the vcc according to unique name
+ val component = vctx.program.callGraph.stronglyConnectedComponent(fd).toSeq sortBy (_.id.uniqueName)
+ val perFunc:Seq[Expr] = for {
+ generator <- component.find( _.postcondition.isDefined).toSeq
+ if generator == fd
+ inComp <- component
+ p <- inComp.postcondition
+ b <- inComp.body
+ } yield { implies(
+ precOrTrue(inComp),
+ // @mk: Don't know which one is better. Inline the body, or have it as a fun. app?
+ //application(p, Seq(b))
+ application(p, Seq(FunctionInvocation(inComp.typedWithDef, inComp.params map { _.toVariable })))
+ )}
+
+ if (perFunc.nonEmpty)
+ Seq(VC(andJoin(perFunc.toSeq), fd, VCKinds.Postcondition, this).setPos(fd.postcondition.get))
+ else Nil
+
+ }
def generatePreconditions(fd: FunDef): Seq[VC] = {
fd.body match {
--
GitLab