diff --git a/library/lazy/package.scala b/library/lazy/package.scala
index f70aebb0f64549055fe7ecb8db24f070408d4e76..6e47d8be74cb89c69ba52c42a30d6203692df09a 100644
--- a/library/lazy/package.scala
+++ b/library/lazy/package.scala
@@ -12,9 +12,8 @@ object $ {
}
@library
-case class $[T](f: Unit => T) { // leon does not support call by name as of now
+case class $[T](f: Unit => T) { // leon does not support call by name as of now
lazy val value = f(())
- def * = f(())
- def isEvaluated = true // for now this is a dummy function, but it will be made sound when leon supports mutable fields.
+ def * = f(())
+ def isEvaluated = true // for now this is a dummy function, but it will be made sound when leon supports mutable fields.
}
-
diff --git a/src/main/scala/leon/laziness/LazinessEliminationPhase.scala b/src/main/scala/leon/laziness/LazinessEliminationPhase.scala
index 39d2e95ce7c29092bb90ee6af087b6ae3dbacfc4..daa7aa18b29595c393824c108fdd483eb812a95a 100644
--- a/src/main/scala/leon/laziness/LazinessEliminationPhase.scala
+++ b/src/main/scala/leon/laziness/LazinessEliminationPhase.scala
@@ -135,7 +135,7 @@ object LazinessEliminationPhase extends TransformationPhase {
if (fd.annotations.contains("axiom"))
fd.addFlag(Annotation("library", Seq()))
}
- val functions = Seq() // Seq("--functions=Rotate@rotateLem")
+ val functions = Seq() // Seq("--functions=rotate-time")
val solverOptions = if(debugSolvers) Seq("--debug=solver") else Seq()
val ctx = Main.processOptions(Seq("--solvers=smt-cvc4") ++ solverOptions ++ functions)
val report = AnalysisPhase.run(ctx)(prog)
diff --git a/src/main/scala/leon/laziness/LazyClosureConverter.scala b/src/main/scala/leon/laziness/LazyClosureConverter.scala
index a54835407d5671dbc6a2a7a5ed323924158e3635..1b5ee63260a4551829e2dac867e9b1b01a17075f 100644
--- a/src/main/scala/leon/laziness/LazyClosureConverter.scala
+++ b/src/main/scala/leon/laziness/LazyClosureConverter.scala
@@ -204,7 +204,8 @@ class LazyClosureConverter(p: Program, closureFactory: LazyClosureFactory) {
Seq(ValDef(param1), ValDef(param2)))
fun.body = Some(param1.toVariable)
val resid = FreshIdentifier("res", param1Type)
- val postbody = Not(SubsetOf(FiniteSet(Set(resid.toVariable), param1Type), param2.toVariable))
+ val postbody = Not(ElementOfSet(resid.toVariable, param2.toVariable))
+ /*SubsetOf(FiniteSet(Set(resid.toVariable), param1Type), param2.toVariable)*/
fun.postcondition = Some(Lambda(Seq(ValDef(resid)), postbody))
fun.addFlag(Annotation("axiom", Seq()))
(tname -> fun)
@@ -228,8 +229,9 @@ class LazyClosureConverter(p: Program, closureFactory: LazyClosureFactory) {
val narg = nargs(0) // there must be only one argument here
val baseType = unwrapLazyType(narg.getType).get
val tname = typeNameWOParams(baseType)
- val adtType = AbstractClassType(closureFactory.absClosureType(tname), getTypeParameters(baseType))
- SubsetOf(FiniteSet(Set(narg), adtType), st(tname))
+ //val adtType = AbstractClassType(closureFactory.absClosureType(tname), getTypeParameters(baseType))
+ //SubsetOf(FiniteSet(Set(narg), adtType), st(tname))
+ ElementOfSet(narg, st(tname))
}, false)
mapNAryOperator(args, op)
diff --git a/testcases/lazy-datastructures/RealTimeQueue-transformed.scala b/testcases/lazy-datastructures/RealTimeQueue-transformed.scala
index f690cc86bf5c6d7fcea967426362ac8dc1a3aad7..7eb26b58071e2acdab089fe919ec3f5cfdf36a17 100644
--- a/testcases/lazy-datastructures/RealTimeQueue-transformed.scala
+++ b/testcases/lazy-datastructures/RealTimeQueue-transformed.scala
@@ -1,4 +1,3 @@
-//import leon.lazyeval._
package leon
import lang._
import annotation._
@@ -40,9 +39,9 @@ object RealTimeQueue {
case class SNil[T]() extends LList[T]
- // TODO: closures are not ADTs since two closures with same arguments are not necessarily equal but
+ // TODO: closures are not ADTs since two closures with same arguments are not necessarily equal but
// ADTs are equal. This creates a bit of problem in checking if a closure belongs to a set or not.
- // However, currently we are assuming that such problems do not happen.
+ // However, currently we are assuming that such problems do not happen.
// A solution is to pass around a dummy id that is unique for each closure.
abstract class LazyLList[T]
@@ -65,7 +64,7 @@ object RealTimeQueue {
}) || LList$isEmpty[T](evalLazyLList[T](l, st)._1)
}
- // an assertion: closures created by evaluating a closure will result in unevaluated closure
+ // an assertion: closures created by evaluating a closure will result in unevaluated closure
@library
def lemmaLazy[T](l: LazyLList[T], st: Set[LazyLList[T]]): Boolean = {
Set[LazyLList[T]](l).subsetOf(st) || {
@@ -122,9 +121,9 @@ object RealTimeQueue {
res._1 != SNil[T]() &&
res._3 <= 4
case _ => true
- }) // &&
+ }) // &&
// (res._1 match {
- // case SCons(_, tail) =>
+ // case SCons(_, tail) =>
// Set[LazyLList[T]](cl).subsetOf(st) || !Set[LazyLList[T]](tail).subsetOf(res._2)
// case _ => true
// })
@@ -154,18 +153,18 @@ object RealTimeQueue {
// things to prove:
// (a0) prove that pre implies post for 'rotate' (this depends on the assumption on eval)
- // (a) Rotate closure creations satisfy the preconditions of 'rotate' (or)
- // for the preconditions involving state, the state at the Rotate invocation sites (through eval)
+ // (a) Rotate closure creations satisfy the preconditions of 'rotate' (or)
+ // for the preconditions involving state, the state at the Rotate invocation sites (through eval)
// satisfy the preconditions of 'rotate'
// (b) If we verify that preconditoins involving state hold at creation time,
- // then we can assume them for calling time only if the preconditions are monotonic
+ // then we can assume them for calling time only if the preconditions are monotonic
// with respect to inclusion of relation of state (this also have to be shown)
// Note: using both captured and calling context is possible but is more involved
// (c) Assume that 'eval' ensures the postcondition of 'rotate'
// (d) Moreover we can also assume that the preconditons of rotate hold whenever we use a closure
// proof of (a)
- // (i) for stateless invariants this can be proven by treating lazy eager,
+ // (i) for stateless invariants this can be proven by treating lazy eager,
// so not doing this here
// monotonicity of isConcrete
@@ -191,7 +190,7 @@ object RealTimeQueue {
} holds
// proof that the precondition isConcrete(f, st) holds for closure creation in 'createQueue' function
- // @ important use and instantiate monotonicity of
+ // @ important use and instantiate monotonicity of
def rotateClosureLemma2[T](f: LazyLList[T], sch: LazyLList[T], st: Set[LazyLList[T]]): Boolean = {
require(streamScheduleProperty[T](f, sch, st)) // && ssize[T](sch) == (ssize[T](f) - r.size) + BigInt(1))
val dres4 = evalLazyLList[T](sch, st);
@@ -217,11 +216,11 @@ object RealTimeQueue {
}
} holds
- // part(c) assume postconditon of 'rotate' in closure invocation time and also
- // the preconditions of 'rotate' if necesssary, and prove the properties of the
- // methods that invoke closures
+ // part(c) assume postconditon of 'rotate' in closure invocation time and also
+ // the preconditions of 'rotate' if necesssary, and prove the properties of the
+ // methods that invoke closures
- // proving specifications of 'rotate' (only state specifications are interesting)
+ // proving specifications of 'rotate' (only state specifications are interesting)
def rotate[T](f: LazyLList[T], r: List[T], a: LazyLList[T], st: Set[LazyLList[T]]): (LList[T], Set[LazyLList[T]], BigInt) = {
require(r.size == ssize[T](f) + BigInt(1) && isConcrete(f, st))
val dres = evalLazyLList[T](f, st);
diff --git a/testcases/lazy-datastructures/RealTimeQueue.scala b/testcases/lazy-datastructures/RealTimeQueue.scala
index e3f4618cf5ad49dbdd03135dd85d2e4002756df4..587716d6d946a8bec9e35a2a542ca46947ffbd8a 100644
--- a/testcases/lazy-datastructures/RealTimeQueue.scala
+++ b/testcases/lazy-datastructures/RealTimeQueue.scala
@@ -92,7 +92,7 @@ object RealTimeQueue {
val rot = $(rotate(tail, r1, $(newa))) //this creates a lazy rotate operation
SCons[T](x, rot)
}
- } ensuring (res => res.size == ssize(f) + r.size + ssize(a) && res.isCons &&
+ } ensuring (res => res.size == ssize(f) + r.size + ssize(a) && res.isCons &&
time <= 30)
// TODO: make newa into sch to avoid a different closure category