Add --assumpre option to assume the precondition when unfolding

Implies(pre, f(x) = body)

becomes, with (--assumepre):

And(pre, f(x) = body)

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)
 

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
           }

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

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()