From 77ba19c23a5b884c5987cea09dce752dbc1972a5 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Thu, 17 Sep 2015 17:07:05 +0200
Subject: [PATCH] FunDef.precOrTrue
---
src/main/scala/leon/purescala/Definitions.scala | 2 ++
src/main/scala/leon/purescala/FunctionClosure.scala | 2 +-
src/main/scala/leon/purescala/MethodLifting.scala | 2 +-
src/main/scala/leon/repair/Repairman.scala | 2 +-
.../leon/solvers/smtlib/SMTLIBCVC4QuantifiedTarget.scala | 4 ++--
.../scala/leon/solvers/smtlib/SMTLIBQuantifiedTarget.scala | 4 ++--
.../scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedTarget.scala | 2 +-
src/main/scala/leon/synthesis/ChooseInfo.scala | 2 +-
src/main/scala/leon/termination/Strengthener.scala | 2 +-
9 files changed, 12 insertions(+), 10 deletions(-)
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index 7a8056c6a..292af0cf8 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -391,6 +391,7 @@ object Definitions {
def precondition_=(oe: Option[Expr]) = {
fullBody = withPrecondition(fullBody, oe)
}
+ def precOrTrue = precondition getOrElse BooleanLiteral(true)
def postcondition = postconditionOf(fullBody)
def postcondition_=(op: Option[Expr]) = {
@@ -532,6 +533,7 @@ object Definitions {
def fullBody = cached(fd.fullBody)
def body = fd.body map cached
def precondition = fd.precondition map cached
+ def precOrTrue = cached(fd.precOrTrue)
def postcondition = fd.postcondition map cached
def hasImplementation = body.isDefined
diff --git a/src/main/scala/leon/purescala/FunctionClosure.scala b/src/main/scala/leon/purescala/FunctionClosure.scala
index 607e9aeb4..7f76beff8 100644
--- a/src/main/scala/leon/purescala/FunctionClosure.scala
+++ b/src/main/scala/leon/purescala/FunctionClosure.scala
@@ -82,7 +82,7 @@ class FunctionClosure extends TransformationPhase {
}
newFunDef.postcondition = freshPostcondition
- pathConstraints = fd.precondition.getOrElse(BooleanLiteral(true)) :: pathConstraints
+ pathConstraints = fd.precOrTrue :: pathConstraints
val freshBody = fd.body.map(body => introduceLets(body, fd2FreshFd + (fd -> ((newFunDef, extraValDefOldIds.map(_.toVariable))))))
newFunDef.body = freshBody
pathConstraints = pathConstraints.tail
diff --git a/src/main/scala/leon/purescala/MethodLifting.scala b/src/main/scala/leon/purescala/MethodLifting.scala
index f94272e9b..25b58c1dc 100644
--- a/src/main/scala/leon/purescala/MethodLifting.scala
+++ b/src/main/scala/leon/purescala/MethodLifting.scala
@@ -175,7 +175,7 @@ object MethodLifting extends TransformationPhase {
// Add precondition if the method was defined in a subclass
val pre = and(
classPre(fd),
- nfd.precondition.getOrElse(BooleanLiteral(true))
+ nfd.precOrTrue
)
nfd.fullBody = withPrecondition(nfd.fullBody, Some(pre))
diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index d38af251c..47dc7abac 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -137,7 +137,7 @@ class Repairman(ctx0: LeonContext, initProgram: Program, fd: FunDef, verifTimeou
val term = Terminating(fd.typed, fd.params.map(_.id.toVariable))
val guide = Guide(origBody)
- val pre = fd.precondition.getOrElse(BooleanLiteral(true))
+ val pre = fd.precOrTrue
val ci = ChooseInfo(
fd,
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedTarget.scala
index a7215bc97..b882bafe2 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedTarget.scala
@@ -47,7 +47,7 @@ trait SMTLIBCVC4QuantifiedTarget extends SMTLIBCVC4Target with SMTLIBQuantifiedT
val specAssert = tfd.postcondition map { post =>
val term = implies(
- tfd.precondition getOrElse BooleanLiteral(true),
+ tfd.precOrTrue,
application(post, Seq(FunctionInvocation(tfd, Seq())))
)
SMTAssert(toSMT(term)(Map()))
@@ -99,7 +99,7 @@ trait SMTLIBCVC4QuantifiedTarget extends SMTLIBCVC4Target with SMTLIBQuantifiedT
post <- tfd.postcondition
} {
val term = implies(
- tfd.precondition getOrElse BooleanLiteral(true),
+ tfd.precOrTrue,
application(post, Seq(tfd.applied))
)
try {
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedTarget.scala
index 0de742f5e..7aa281b67 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedTarget.scala
@@ -40,8 +40,8 @@ trait SMTLIBQuantifiedTarget extends SMTLIBTarget {
Seq(fi)
)
} getOrElse BooleanLiteral(true)
- val pre = tfd.precondition getOrElse BooleanLiteral(true)
- and(pre, post)
+
+ and(tfd.precOrTrue, post)
}
// We want to check if the negation of the vc is sat under inductive hyp.
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedTarget.scala
index 6c20b337d..0735b2396 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedTarget.scala
@@ -59,7 +59,7 @@ trait SMTLIBZ3QuantifiedTarget extends SMTLIBZ3Target with SMTLIBQuantifiedTarge
post <- tfd.postcondition
} {
val term = implies(
- tfd.precondition getOrElse BooleanLiteral(true),
+ tfd.precOrTrue,
application(post, Seq(tfd.applied))
)
try {
diff --git a/src/main/scala/leon/synthesis/ChooseInfo.scala b/src/main/scala/leon/synthesis/ChooseInfo.scala
index cd67adf98..5e36c593b 100644
--- a/src/main/scala/leon/synthesis/ChooseInfo.scala
+++ b/src/main/scala/leon/synthesis/ChooseInfo.scala
@@ -42,7 +42,7 @@ object ChooseInfo {
def extractFromFunction(ctx: LeonContext, prog: Program, fd: FunDef): Seq[ChooseInfo] = {
- val actualBody = and(fd.precondition.getOrElse(BooleanLiteral(true)), fd.body.get)
+ val actualBody = and(fd.precOrTrue, fd.body.get)
val term = Terminating(fd.typed, fd.params.map(_.id.toVariable))
val eFinder = new ExamplesFinder(ctx, prog)
diff --git a/src/main/scala/leon/termination/Strengthener.scala b/src/main/scala/leon/termination/Strengthener.scala
index dc3d08188..e6c53a472 100644
--- a/src/main/scala/leon/termination/Strengthener.scala
+++ b/src/main/scala/leon/termination/Strengthener.scala
@@ -35,7 +35,7 @@ trait Strengthener { self : RelationComparator =>
funDef.postcondition = Some(postcondition)
- val prec = matchToIfThenElse(funDef.precondition.getOrElse(BooleanLiteral(true)))
+ val prec = matchToIfThenElse(funDef.precOrTrue)
val body = matchToIfThenElse(funDef.body.get)
val post = matchToIfThenElse(postcondition)
val formula = implies(prec, application(post, Seq(body)))
--
GitLab