Trying to verify LCS

src/main/scala/leon/Main.scala

@@ -193,6 +193,7 @@ object Main {
           new PreprocessingPhase(xlangF)
 
       val verification =
+        InstrumentationPhase andThen
         VerificationPhase andThen
         FixReportLabels.when(xlangF) andThen
         PrintReportPhase

src/main/scala/leon/invariant/util/TypeUtil.scala

@@ -27,7 +27,7 @@ object TypeUtil {
       case _ => None
     }
   }
- 
+
   def isSubclass(sub: ClassDef, sup: ClassDef) = {
     sub == sup || (sub.parent.isDefined && sub.parent.get.classDef == sup)
   }

src/main/scala/leon/laziness/ClosureConverter.scala

@@ -49,7 +49,8 @@ class ClosureConverter(p: Program, ctx: LeonContext,
     } else oldId
   }
 
-  val funMap = ProgramUtil.userLevelFunctions(p).map { fd =>
+  val funMap = ProgramUtil.userLevelFunctions(p).collect {
+    case fd if fd.hasBody =>
       val stparams =
         if (funsNeedStateTps(fd)) {
           // create fresh type parameters for the state

src/main/scala/leon/laziness/ClosureFactory.scala

@@ -106,7 +106,7 @@ class ClosureFactory(p: Program) {
      * Checks if the types of lambdas are not instantiations of one another.
      * This is currently not supported.
      */
-    lambdasList.groupBy { lop =>      
+    lambdasList.groupBy { lop =>
       val FunctionType(argts, _) = lop.getType
       argts.size
     }.foreach {
@@ -224,6 +224,7 @@ class ClosureFactory(p: Program) {
           case None =>
             throw new IllegalStateException(s"No lambda compatible with type: $t exists in the program")
           case Some((uninstType, absClass)) =>
+//            /println(s"Getting type arguments of unintstType: $uninstType instType: $ft")
             val ftparams = getTypeArguments(ft, uninstType).get
             // here, we have the guarantee that the `abstractType` wouldn't take any more type parameters than its corresponding function type
             AbstractClassType(absClass, ftparams)

src/main/scala/leon/laziness/HOInferencePhase.scala

@@ -25,7 +25,7 @@ object HOInferencePhase extends SimpleLeonPhase[Program, LazyVerificationReport]
   val dumpProgWOInstSpecs = true
   val dumpInstrumentedProgram = true
   val debugSolvers = false
-  val skipStateVerification = false
+  val skipStateVerification = true
   val skipResourceVerification = false
 
   val name = "Laziness Elimination Phase"

src/main/scala/leon/laziness/LazyInstrumenter.scala

@@ -21,45 +21,10 @@ class LazyInstrumenter(p: Program, ctx: LeonContext, clFactory: ClosureFactory,
   class MemExprInstrumenter(funMap: Map[FunDef, FunDef], serialInst: SerialInstrumenter)(implicit currFun: FunDef)
       extends ExprInstrumenter(funMap, serialInst)(currFun) {
 
-        //println("Instrumenting function: "+currFun)
     val costOfMemoization: Map[Instrumentation, Int] =
       Map(Time -> 1, Stack -> 1, Rec -> 1, TPR -> 1, Depth -> 1)
 
     lazy val stateParam = currFun.params.last.id.toVariable // this field should be valid when it is accessed
-    /*override def apply(e: Expr): Expr = {
-      if (isEvalFunction(currFun)) {
-        e match {
-          case MatchExpr(scr, mcases) =>
-            val ncases = mcases map {
-              case mc@MatchCase(pat@InstanceOfPattern(Some(bind), CaseClassType(ccd: CaseClassDef, tps)), guard, body) =>
-                // find the case class of a memoized function that is constructed
-                val memoCCs = collect[CaseClass]{
-                  case cc@CaseClass(CaseClassType(ccd, _),_) if clFactory.memoClosures(ccd) => Set(cc)
-                  case _ => Set()
-                }(body)
-                val instBody = transform(body)(Map())
-                val nbody = if(memoCCs.isEmpty){ // this case is not invoking a memoized function
-                  instBody
-                } else {
-                  if(memoCCs.size > 1)
-                    throw new IllegalStateException("More than one case class construction found in match case! "+mc)
-                  val memoClosure = memoCCs.head
-                  val bodyId = FreshIdentifier("bd", instBody.getType, true)
-                  val instExprs = instrumenters map { m =>
-                    IfExpr(ElementOfSet(memoClosure, stateParam),
-                      InfiniteIntegerLiteral(costOfMemoization(m.inst)),
-                      selectInst(bodyId.toVariable, m.inst))
-                  }
-                  Let(bodyId, instBody,
-                    Tuple(TupleSelect(bodyId.toVariable, 1) +: instExprs))
-                }
-                MatchCase(pat, guard, nbody)
-            }
-            MatchExpr(scr, ncases)
-        }
-      } else
-        super.apply(e)
-    }*/
 
     def memoClosureByName(name: String) = {
       clFactory.memoClasses.find{
@@ -77,9 +42,9 @@ class LazyInstrumenter(p: Program, ctx: LeonContext, clFactory: ClosureFactory,
         val (args, stExpr) =
           if(funManager.funsNeedStates(oldTarget)) {
             //remove the state argument
-            (f.args.dropRight(1), f.args.last)
+            (subeVals.dropRight(1), subeVals.last)
           } else
-            (f.args, stateParam)
+            (subeVals, stateParam)
         val cc = CaseClass(CaseClassType(ccdef, stateTps(stExpr)), args)
         val instId = FreshIdentifier("instd", instExpr.getType, true)
         val instExprs = instrumenters map { m =>

testcases/lazy-datastructures/withOrb/Esop15Benchmarks.scala

@@ -1,10 +1,11 @@
 package withorb
 
 import leon._
-import lazyeval._
 import lang._
 import annotation._
 import instrumentation._
+import mem._
+import higherorder._
 import collection._
 import invariant._
 
@@ -14,24 +15,83 @@ import invariant._
  * Decreasing the time bounds slightly will display counter-examples.
  */
 object Esop15Benchmarks {
-  sealed abstract class IStream
-  case class SCons(x: BigInt, tail: Lazy[IStream]) extends IStream
-  case class SNil() extends IStream
+  /*sealed abstract class Stream[T] {
+    lazy val tail = {
+      require(this != SNil())
+      this match {
+        case SCons(_, tailfun) => tailfun()
+      }
+    }
+  }*/
+  case class SCons[T](x: T, tail: ValOrSusp[T])
+
+  sealed abstract class ValOrSusp[T] {
+    def isCached = this match {
+      case Val(_) => true
+      case _ => get.cached
+    }
+
+    /*def isSusp = this match {
+      case Val(_) => false
+      case _ =>  true
+    }*/
 
-  sealed abstract class StreamPairs
-  case class PCons(pair: (BigInt, BigInt), tail: Lazy[StreamPairs]) extends StreamPairs
-  case class PNil() extends StreamPairs
+    lazy val get = {
+      this match {
+        case Val(x) => x
+        case Susp(f) => f()
+      }
+    }
+  }
+  case class Val[T](x: SCons[T]) extends ValOrSusp[T]
+  case class Susp[T](fun: () => SCons[T]) extends ValOrSusp[T]
 
-  def zipWith(xs: Lazy[IStream], ys: Lazy[IStream]): StreamPairs = {
-    (xs.value, ys.value) match {
-      case (SCons(x, xtail), SCons(y, ytail)) =>
-        PCons((x, y), $(zipWith(xtail, ytail)))
-      case _ =>
-        PNil()
+  lazy val fibstream: SCons[BigInt] =
+    SCons[BigInt](0, Val(SCons[BigInt](1, Val(SCons[BigInt](1, Susp(() => fibStreamGen))))))
+
+  def fibStreamGen: SCons[BigInt] = {
+    val fibs = this.fibstream
+    fibs match {
+      case s @ SCons(x, _) => zipWithFun((x: BigInt, y: BigInt) => x + y, fibs, s.tail.get)
     }
   } ensuring(_ => time <= ?)
 
-  def nextFib(x: BigInt, y: BigInt, n: BigInt): IStream = {
+  @invstate
+  def zipWithFun(f: (BigInt, BigInt) => BigInt, xs: SCons[BigInt], ys: SCons[BigInt]): SCons[BigInt] = {
+    require(xs.tail.isCached && ys.tail.isCached)
+    (xs, ys) match {
+      case (SCons(x, _), SCons(y, _)) =>
+        val xtail = xs.tail.get
+        val ytail = ys.tail.get
+        SCons[BigInt](f(x, y), Susp(() => zipWithFun(f, xtail, ytail)))
+    }
+  } ensuring { _ =>
+//    /if (isCached(xs, ys, inState[BigInt]))
+      time <= ?
+    //else true
+  }
+
+  /**
+   * Checks if `xs.tail` and `ys.tail` have been evaluated in the state `st`
+   */
+  /*def isCached(xs: SCons[BigInt], ys: SCons[BigInt], st: Set[Fun[BigInt]]) = {
+    (xs, ys) match {
+      case (SCons(_, _), SCons(_, _)) => (xs.tail.isCached withState st) && (ys.tail.isCached withState st)
+      case _ => true
+    }
+  }*/
+
+  def nthElem(n: BigInt, fibs: SCons[BigInt]): BigInt = {
+    require(n >= 0)
+    fibs match {
+      case SCons(x, _) =>
+        if (n == 0) x
+        else
+          nthElem(n - 1, fibs.tail.get)
+    }
+  } ensuring(_ => time <= ? * n + ?)
+
+  /*def nextFib(x: BigInt, y: BigInt, n: BigInt): IStream = {
     if (n <= 0)
       SNil()
     else {
@@ -55,4 +115,4 @@ object Esop15Benchmarks {
       case SNil() => BigInt(-1)
     }
   } ensuring(_ => time <= ? * n + ?) // you get a counter-example for 20*n + 20
-}
+*/ }