From f7f7ff1d9cee891c5a4f508d79b1a59659d16f88 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Tue, 6 Oct 2015 19:26:08 +0200
Subject: [PATCH] Use precOrTrue in Tactic
---
src/main/scala/leon/purescala/ExprOps.scala | 2 +-
src/main/scala/leon/verification/DefaultTactic.scala | 6 +++---
src/main/scala/leon/verification/InductionTactic.scala | 8 ++++----
src/main/scala/leon/verification/Tactic.scala | 6 ------
4 files changed, 8 insertions(+), 14 deletions(-)
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 6a994e454..84b1957b5 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -337,7 +337,7 @@ object ExprOps {
rec(initBinders, e)
}
- /** Returns the set of identifiers in an expression */
+ /** Returns the set of free variables in an expression */
def variablesOf(expr: Expr): Set[Identifier] = {
import leon.xlang.Expressions.LetVar
fold[Set[Identifier]] {
diff --git a/src/main/scala/leon/verification/DefaultTactic.scala b/src/main/scala/leon/verification/DefaultTactic.scala
index a00066ef1..6e90f0da4 100644
--- a/src/main/scala/leon/verification/DefaultTactic.scala
+++ b/src/main/scala/leon/verification/DefaultTactic.scala
@@ -14,7 +14,7 @@ class DefaultTactic(vctx: VerificationContext) extends Tactic(vctx) {
def generatePostconditions(fd: FunDef): Seq[VC] = {
(fd.postcondition, fd.body) match {
case (Some(post), Some(body)) =>
- val vc = implies(precOrTrue(fd), application(post, Seq(body)))
+ val vc = implies(fd.precOrTrue, application(post, Seq(body)))
Seq(VC(vc, fd, VCKinds.Postcondition).setPos(post))
case _ =>
Nil
@@ -31,7 +31,7 @@ class DefaultTactic(vctx: VerificationContext) extends Tactic(vctx) {
calls.map {
case ((fi @ FunctionInvocation(tfd, args), pre), path) =>
val pre2 = tfd.withParamSubst(args, pre)
- val vc = implies(and(precOrTrue(fd), path), pre2)
+ val vc = implies(and(fd.precOrTrue, path), pre2)
val fiS = sizeLimit(fi.asString, 40)
VC(vc, fd, VCKinds.Info(VCKinds.Precondition, s"call $fiS")).setPos(fi)
}
@@ -74,7 +74,7 @@ class DefaultTactic(vctx: VerificationContext) extends Tactic(vctx) {
calls.map {
case (e, correctnessCond) =>
- val vc = implies(precOrTrue(fd), correctnessCond)
+ val vc = implies(fd.precOrTrue, correctnessCond)
VC(vc, fd, eToVCKind(e)).setPos(e)
}
diff --git a/src/main/scala/leon/verification/InductionTactic.scala b/src/main/scala/leon/verification/InductionTactic.scala
index 74b7b99af..65f96a090 100644
--- a/src/main/scala/leon/verification/InductionTactic.scala
+++ b/src/main/scala/leon/verification/InductionTactic.scala
@@ -35,12 +35,12 @@ class InductionTactic(vctx: VerificationContext) extends DefaultTactic(vctx) {
val subCases = selectors.map { sel =>
replace(Map(arg.toVariable -> sel),
- implies(precOrTrue(fd), application(post, Seq(body)))
+ implies(fd.precOrTrue, application(post, Seq(body)))
)
}
val vc = implies(
- and(IsInstanceOf(arg.toVariable, cct), precOrTrue(fd)),
+ and(IsInstanceOf(arg.toVariable, cct), fd.precOrTrue),
implies(andJoin(subCases), application(post, Seq(body)))
)
@@ -72,12 +72,12 @@ class InductionTactic(vctx: VerificationContext) extends DefaultTactic(vctx) {
val subCases = selectors.map { sel =>
replace(Map(arg.toVariable -> sel),
- implies(precOrTrue(fd), tfd.withParamSubst(args, pre))
+ implies(fd.precOrTrue, tfd.withParamSubst(args, pre))
)
}
val vc = implies(
- andJoin(Seq(IsInstanceOf(arg.toVariable, cct), precOrTrue(fd), path) ++ subCases),
+ andJoin(Seq(IsInstanceOf(arg.toVariable, cct), fd.precOrTrue, path) ++ subCases),
tfd.withParamSubst(args, pre)
)
diff --git a/src/main/scala/leon/verification/Tactic.scala b/src/main/scala/leon/verification/Tactic.scala
index 98af8cde0..8f539708d 100644
--- a/src/main/scala/leon/verification/Tactic.scala
+++ b/src/main/scala/leon/verification/Tactic.scala
@@ -21,12 +21,6 @@ abstract class Tactic(vctx: VerificationContext) {
def generatePreconditions(function: FunDef): Seq[VC]
def generateCorrectnessConditions(function: FunDef): Seq[VC]
- // Helper functions
- protected def precOrTrue(fd: FunDef): Expr = fd.precondition match {
- case Some(pre) => pre
- case None => BooleanLiteral(true)
- }
-
protected def sizeLimit(s: String, limit: Int) = {
require(limit > 3)
// Crop the call to display it properly
--
GitLab