Changing some parameters and minor changes

library/annotation/package.scala

@@ -17,6 +17,8 @@ package object annotation {
   class extern     extends StaticAnnotation
   @ignore
   class inline     extends StaticAnnotation
+
+  // Orb annotations
   @ignore
   class monotonic  extends StaticAnnotation
   @ignore
@@ -27,4 +29,8 @@ package object annotation {
   class invstate extends StaticAnnotation
   @ignore
   class memoize extends StaticAnnotation
+  @ignore
+  class invisibleBody extends StaticAnnotation // do not unfold the body of the function
+  @ignore
+  class unfoldFactor(f: Int=0) extends StaticAnnotation // 0 implies no bound on unfolding
 }
\ No newline at end of file

src/main/scala/leon/invariant/engine/InferenceContext.scala

@@ -36,7 +36,7 @@ class InferenceContext(val initProgram: Program, val leonContext: LeonContext) {
   val dumpStats = false
 
   // the following options have default values
-  val vcTimeout = leonContext.findOption(optVCTimeout).getOrElse(15L) // in secs
+  val vcTimeout = leonContext.findOption(optVCTimeout).getOrElse(30L) // in secs
   val nlTimeout = leonContext.findOption(optNLTimeout).getOrElse(15L)
   val totalTimeout = leonContext.findOption(SharedOptions.optTimeout) // in secs
   val functionsToInfer = leonContext.findOption(SharedOptions.optFunctions)

src/main/scala/leon/invariant/engine/RefinementEngine.scala

@@ -70,7 +70,6 @@ class RefinementEngine(ctx: InferenceContext, prog: Program, ctrTracker: Constra
 
       //unroll each call in the head pointers and in toRefineCalls
       val callsToProcess = if (toRefineCalls.isDefined) {
-
         //pick only those calls that have been least unrolled
         val relevCalls = allheads.intersect(toRefineCalls.get)
         var minCalls = Set[Call]()
@@ -86,14 +85,12 @@ class RefinementEngine(ctx: InferenceContext, prog: Program, ctrTracker: Constra
           }
         })
         minCalls
-
       } else allheads
 
       if (verbose)
         reporter.info("Unrolling: " + callsToProcess.size + "/" + allheads.size)
 
       val unrolls = callsToProcess.foldLeft(Set[Call]())((acc, call) => {
-
         val calldata = formula.callData(call)
         val recInvokes = calldata.parents.count(_ == call.fi.tfd.fd)
         //if the call is not a recursive call, unroll it unconditionally
@@ -110,7 +107,7 @@ class RefinementEngine(ctx: InferenceContext, prog: Program, ctrTracker: Constra
             acc
           }
         }
-        //TODO: are there better ways of unrolling ??
+        //TODO: are there better ways of unrolling ?? Yes. Akask Lal "dag Inlining". Implement that!
       })
 
       //update the head functions
@@ -189,25 +186,29 @@ class RefinementEngine(ctx: InferenceContext, prog: Program, ctrTracker: Constra
   }
 
   def inilineCall(call: Call, formula: Formula) = {
-    //here inline the body and conjoin it with the guard
     val tfd = call.fi.tfd
     val callee = tfd.fd
-
-    //Important: make sure we use a fresh body expression here, and freshenlocals
-    val tparamMap = (callee.tparams zip tfd.tps).toMap
-    val newbody = freshenLocals(matchToIfThenElse(callee.body.get))
-    val freshBody = instantiateType(newbody, tparamMap, Map())
-    val calleeSummary =
-      Equals(getFunctionReturnVariable(callee), freshBody)
-    val argmap1 = formalToActual(call)
-    val inlinedSummary = ExpressionTransformer.normalizeExpr(replace(argmap1, calleeSummary), ctx.multOp)
-
-    if (this.dumpInlinedSummary)
-      println("Inlined Summary: " + inlinedSummary)
-
-    //conjoin the summary with the disjunct corresponding to the 'guard'
-    //note: the parents of the summary are the parents of the call plus the callee function
-    val calldata = formula.callData(call)
-    formula.conjoinWithDisjunct(calldata.guard, inlinedSummary, (callee +: calldata.parents))
+    if (callee.isBodyVisible) {
+      //here inline the body and conjoin it with the guard
+      //Important: make sure we use a fresh body expression here, and freshenlocals
+      val tparamMap = (callee.tparams zip tfd.tps).toMap
+      val newbody = freshenLocals(matchToIfThenElse(callee.body.get))
+      val freshBody = instantiateType(newbody, tparamMap, Map())
+      val calleeSummary =
+        Equals(getFunctionReturnVariable(callee), freshBody)
+      val argmap1 = formalToActual(call)
+      val inlinedSummary = ExpressionTransformer.normalizeExpr(replace(argmap1, calleeSummary), ctx.multOp)
+
+      if (this.dumpInlinedSummary)
+        println("Inlined Summary: " + inlinedSummary)
+
+      //conjoin the summary with the disjunct corresponding to the 'guard'
+      //note: the parents of the summary are the parents of the call plus the callee function
+      val calldata = formula.callData(call)
+      formula.conjoinWithDisjunct(calldata.guard, inlinedSummary, (callee +: calldata.parents))
+    } else {
+      if (verbose)
+        reporter.info(s"Not inlining ${call.fi}: body invisible!")
+    }
   }
 }

src/main/scala/leon/invariant/structure/FunctionUtils.scala

@@ -27,6 +27,7 @@ object FunctionUtils {
     lazy val compose = fd.annotations.contains("compose")
     lazy val isLibrary = fd.annotations.contains("library")
     lazy val isExtern = fd.annotations.contains("extern")
+    lazy val isBodyVisible =  !fd.annotations.contains("invisibleBody")
     lazy val hasFieldFlag = fd.flags.contains(IsField(false))
     lazy val hasLazyFieldFlag = fd.flags.contains(IsField(true))
     lazy val isUserFunction = !hasFieldFlag && !hasLazyFieldFlag

src/main/scala/leon/invariant/templateSolvers/NLTemplateSolver.scala

@@ -45,7 +45,7 @@ class NLTemplateSolver(ctx: InferenceContext, program: Program,
   val trackUnpackedVCCTime = false
 
   //print flags
-  val verbose = true
+  val verbose = false
   val printCounterExample = false
   val printPathToConsole = false
   val dumpPathAsSMTLIB = false
@@ -59,7 +59,7 @@ class NLTemplateSolver(ctx: InferenceContext, program: Program,
   private val farkasSolver = new FarkasLemmaSolver(ctx, program)
   private val startFromEarlierModel = true
   private val disableCegis = true
-  private val useIncrementalSolvingForVCs = true
+  private val useIncrementalSolvingForVCs = false
   private val useCVCToCheckVCs = true
   private val usePortfolio = false // portfolio has a bug in incremental solving
 

src/main/scala/leon/laziness/LazinessEliminationPhase.scala

@@ -37,6 +37,7 @@ import leon.verification._
 import PredicateUtil._
 import leon.invariant.engine._
 import LazyVerificationPhase._
+import utils._
 /**
  * TODO: Function names are assumed to be small case. Fix this!!
  */
@@ -93,14 +94,14 @@ object LazinessEliminationPhase extends TransformationPhase {
     if (dumpTypeCorrectProg)
       println("After rectifying types: \n" + ScalaPrinter.apply(typeCorrectProg))
 
-    val progWithPre = (new ClosurePreAsserter(typeCorrectProg)).apply
+    val progWithPre =  (new ClosurePreAsserter(typeCorrectProg)).apply
     if (dumpProgWithPreAsserts) {
       //println("After asserting closure preconditions: \n" + ScalaPrinter.apply(progWithPre))
       prettyPrintProgramToFile(progWithPre, ctx, "-withpre", uniqueIds = true)
     }
 
     // verify the contracts that do not use resources
-    val progWOInstSpecs = removeInstrumentationSpecs(progWithPre)
+    val progWOInstSpecs = InliningPhase.apply(ctx, removeInstrumentationSpecs(progWithPre))
     if (dumpProgWOInstSpecs) {
       //println("After removing instrumentation specs: \n" + ScalaPrinter.apply(progWOInstSpecs))
       prettyPrintProgramToFile(progWOInstSpecs, ctx, "-woinst")
@@ -110,7 +111,7 @@ object LazinessEliminationPhase extends TransformationPhase {
       checkSpecifications(progWOInstSpecs, checkCtx)
 
     // instrument the program for resources (note: we avoid checking preconditions again here)
-    val instrumenter = new LazyInstrumenter(typeCorrectProg, closureFactory)
+    val instrumenter = new LazyInstrumenter(InliningPhase.apply(ctx, typeCorrectProg), closureFactory)
     val instProg = instrumenter.apply
     if (dumpInstrumentedProgram) {
       //println("After instrumentation: \n" + ScalaPrinter.apply(instProg))

src/main/scala/leon/laziness/LazyClosureConverter.scala

@@ -251,8 +251,6 @@ class LazyClosureConverter(p: Program, ctx: LeonContext,
 
   /**
    * These are evalFunctions that do not affect the state.
-   * TODO: here we can avoid creating two calls to the function one
-   * with uninterpreted state and other with input state (since here both are equal)
    */
   val computeFunctions = evalFunctions.map {
     case (tname, evalfd) =>
@@ -267,6 +265,7 @@ class LazyClosureConverter(p: Program, ctx: LeonContext,
       val invoke = FunctionInvocation(TypedFunDef(evalfd, evalfd.tparams.map(_.tp)),
         Seq(param1.id.toVariable, uiState))
       fun.body = Some(TupleSelect(invoke, 1))
+      fun.addFlag(IsInlined)
       (tname -> fun)
   }.toMap
 
@@ -286,7 +285,8 @@ class LazyClosureConverter(p: Program, ctx: LeonContext,
     val fun = new FunDef(FreshIdentifier(closureConsName(tname)), tparamdefs,
       Seq(ValDef(param1), ValDef(param2)), param1Type)
     fun.body = Some(param1.toVariable)
-    // assert that the closure in unevaluated if useRefEquality is enabled
+    fun.addFlag(IsInlined)
+    // assert that the closure in unevaluated if useRefEquality is enabled! is this needed ?
     // not supported as of now
     /*if (refEq) {
       val resid = FreshIdentifier("res", param1Type)

src/main/scala/leon/laziness/LazyClosureFactory.scala

@@ -207,7 +207,6 @@ class LazyClosureFactory(p: Program) {
       val SetType(baseT) = stType.classDef.fields.find { fld => fld.id.name == fldname }.get.getType
       val param2 = FreshIdentifier("cl", baseT)
 
-      // TODO: as an optimization we can mark all these functions as inline and inline them at their callees
       val updateFun = new FunDef(FreshIdentifier("updState" + tn),
         state.tparams, Seq(ValDef(param1), ValDef(param2)), stType)
       // create a body for the updateFun:
@@ -221,6 +220,8 @@ class LazyClosureFactory(p: Program) {
       }
       val nst = CaseClass(stType, nargs)
       updateFun.body = Some(nst)
+      // add inline annotation of optimization
+      updateFun.addFlag(IsInlined)
       (tn -> updateFun)
     }.toMap
 }

testcases/lazy-datastructures/withOrb/RealTimeQueue.scala

@@ -28,15 +28,13 @@ object RealTimeQueue {
     def size: BigInt = {
       this match {
         case SNil()      => BigInt(0)
-        case SCons(x, t) => 1 + ssize(t)
+        case SCons(x, t) => 1 + (t*).size
       }
     } ensuring (_ >= 0)
   }
   case class SCons[T](x: T, tail: $[Stream[T]]) extends Stream[T]
   case class SNil[T]() extends Stream[T]
 
-  def ssize[T](l: $[Stream[T]]): BigInt = (l*).size
-
   def isConcrete[T](l: $[Stream[T]]): Boolean = {
     l.isEvaluated && (l* match {
       case SCons(_, tail) =>
@@ -45,9 +43,10 @@ object RealTimeQueue {
     })
   }
 
-   @invstate
+  @invisibleBody
+  @invstate
   def rotate[T](f: $[Stream[T]], r: List[T], a: $[Stream[T]]): Stream[T] = { // doesn't change state
-    require(r.size == ssize(f) + 1 && isConcrete(f))
+    require(r.size == (f*).size + 1 && isConcrete(f))
     (f.value, r) match {
       case (SNil(), Cons(y, _)) => //in this case 'y' is the only element in 'r'
         SCons[T](y, a)
@@ -82,7 +81,7 @@ object RealTimeQueue {
     def isEmpty = (f*).isEmpty
     def valid = {
       (firstUnevaluated(f) == firstUnevaluated(s)) &&
-        ssize(s) == ssize(f) - r.size //invariant: |s| = |f| - |r|
+        (s*).size == (f*).size - r.size //invariant: |s| = |f| - |r|
     }
   }
 
@@ -102,11 +101,11 @@ object RealTimeQueue {
     createQ(q.f, Cons(x, q.r), q.s)
   } ensuring (res => res.valid && time <= ?)
 
-  /*def dequeue[T](q: Queue[T]): Queue[T] = {
+  def dequeue[T](q: Queue[T]): Queue[T] = {
     require(!q.isEmpty && q.valid)
     q.f.value match {
       case SCons(x, nf) =>
         createQ(nf, q.r, q.s)
     }
-  } ensuring (res => res.valid && time <= ?)*/
+  } ensuring (res => res.valid && time <= ?)
 }