From 85505865998e060efbf334781a332493c2bab0eb Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Wed, 3 Jun 2015 11:56:08 +0200
Subject: [PATCH] Add --assumpre option to assume the precondition when
unfolding
Implies(pre, f(x) = body)
becomes, with (--assumepre):
And(pre, f(x) = body)
---
.../scala/leon/solvers/combinators/UnrollingSolver.scala | 9 +++++----
.../scala/leon/solvers/templates/TemplateGenerator.scala | 9 +++++++--
src/main/scala/leon/solvers/z3/FairZ3Component.scala | 3 ++-
src/main/scala/leon/solvers/z3/FairZ3Solver.scala | 3 ++-
4 files changed, 16 insertions(+), 8 deletions(-)
diff --git a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
index 1946d225d..7ab318038 100644
--- a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
@@ -10,15 +10,16 @@ import purescala.Constructors._
import purescala.Expressions._
import purescala.ExprOps._
-import z3.FairZ3Component.{optFeelingLucky, optUseCodeGen}
+import z3.FairZ3Component.{optFeelingLucky, optUseCodeGen, optAssumePre}
import templates._
import utils.Interruptible
import evaluators._
class UnrollingSolver(val context: LeonContext, program: Program, underlying: IncrementalSolver with Interruptible) extends Solver with Interruptible {
- val feelingLucky = context.findOptionOrDefault(optFeelingLucky)
- val useCodeGen = context.findOptionOrDefault(optUseCodeGen)
+ val feelingLucky = context.findOptionOrDefault(optFeelingLucky)
+ val useCodeGen = context.findOptionOrDefault(optUseCodeGen)
+ val assumePreHolds = context.findOptionOrDefault(optAssumePre)
private val evaluator : Evaluator = {
if(useCodeGen) {
@@ -61,7 +62,7 @@ class UnrollingSolver(val context: LeonContext, program: Program, underlying: In
def mkAnd(es: Expr*) = andJoin(es)
def mkEquals(l: Expr, r: Expr) = Equals(l, r)
def mkImplies(l: Expr, r: Expr) = implies(l, r)
- })
+ }, assumePreHolds)
val unrollingBank = new UnrollingBank(reporter, templateGenerator)
diff --git a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
index 3781cb3e5..209c6c3ab 100644
--- a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
@@ -14,7 +14,8 @@ import purescala.Constructors._
import evaluators._
-class TemplateGenerator[T](val encoder: TemplateEncoder[T]) {
+class TemplateGenerator[T](val encoder: TemplateEncoder[T],
+ val assumePreHolds: Boolean) {
private var cache = Map[TypedFunDef, FunctionTemplate[T]]()
private var cacheExpr = Map[Expr, FunctionTemplate[T]]()
@@ -89,7 +90,11 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T]) {
val postHolds : Expr =
if(tfd.hasPrecondition) {
- Implies(prec.get, newPost)
+ if (assumePreHolds) {
+ And(prec.get, newPost)
+ } else {
+ Implies(prec.get, newPost)
+ }
} else {
newPost
}
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Component.scala b/src/main/scala/leon/solvers/z3/FairZ3Component.scala
index add51eb5f..f321d516d 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Component.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Component.scala
@@ -12,9 +12,10 @@ trait FairZ3Component extends LeonComponent {
val optFeelingLucky = LeonFlagOptionDef("feelinglucky","Use evaluator to find counter-examples early", false)
val optUseCodeGen = LeonFlagOptionDef("codegen", "Use compiled evaluator instead of interpreter", false)
val optUnrollCores = LeonFlagOptionDef("unrollcores", "Use unsat-cores to drive unrolling while remaining fair", false)
+ val optAssumePre = LeonFlagOptionDef("assumepre", "Assume precondition holds (pre && f(x) = body) when unfolding", false)
override val definedOptions: Set[LeonOptionDef[Any]] =
- Set(optEvalGround, optCheckModels, optFeelingLucky, optUseCodeGen, optUnrollCores)
+ Set(optEvalGround, optCheckModels, optFeelingLucky, optUseCodeGen, optUnrollCores, optAssumePre)
}
object FairZ3Component extends FairZ3Component
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index 8a845754b..c5a546850 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -32,6 +32,7 @@ class FairZ3Solver(val context : LeonContext, val program: Program)
val useCodeGen = context.findOptionOrDefault(optUseCodeGen)
val evalGroundApps = context.findOptionOrDefault(optEvalGround)
val unrollUnsatCores = context.findOptionOrDefault(optUnrollCores)
+ val assumePreHolds = context.findOptionOrDefault(optAssumePre)
protected val errors = new IncrementalBijection[Unit, Boolean]()
protected def hasError = errors.getB(()) contains true
@@ -142,7 +143,7 @@ class FairZ3Solver(val context : LeonContext, val program: Program)
def mkAnd(es: Z3AST*) = z3.mkAnd(es : _*)
def mkEquals(l: Z3AST, r: Z3AST) = z3.mkEq(l, r)
def mkImplies(l: Z3AST, r: Z3AST) = z3.mkImplies(l, r)
- })
+ }, assumePreHolds)
initZ3()
--
GitLab