diff --git a/library/lazy/package.scala b/library/lazy/package.scala
index f329b589abb38457cd8f53e1ebe15209c311f201..7c0f575828c3bd96cb32c069c43e1444373075a5 100644
--- a/library/lazy/package.scala
+++ b/library/lazy/package.scala
@@ -1,32 +1,39 @@
/* Copyright 2009-2013 EPFL, Lausanne */
-package leon.lazyeval
+package leon
-import leon.annotation._
-import leon.lang._
+import annotation._
+import lang._
import scala.language.implicitConversions
import scala.annotation.StaticAnnotation
-@library
-object $ {
- def apply[T](f: => T) = new $(Unit => f)
- def eager[T](x: => T) = new $(Unit => x)
+package object lazyeval {
+
+ @library
+ def $[T](f: => T) = Lazy(Unit => f)
+ //def apply[T](f: => T) = new $(Unit => f)
+
+ @library
+ def eager[T](x: => T) = Lazy(Unit => x)
+
/**
* implicit conversion from eager evaluation to lazy evaluation
*/
+ @library
@inline
implicit def eagerToLazy[T](x: T) = eager(x)
/**
- * accessing in and out states.
+ * For accessing in and out states.
* Should be used only in ensuring.
- * TODO: enforce this.
*/
+ @library
@extern
- def inState[T] : Set[$[T]] = sys.error("inState method is not executable!")
+ def inState[T]: Set[Lazy[T]] = sys.error("inState method is not executable!")
+ @library
@extern
- def outState[T] : Set[$[T]] = sys.error("outState method is not executable")
+ def outState[T]: Set[Lazy[T]] = sys.error("outState method is not executable")
/**
* Helper class for invoking with a given state instead of the implicit state
@@ -34,30 +41,23 @@ object $ {
@library
case class WithState[T](v: T) {
@extern
- def withState[U](u: Set[$[U]]): T = sys.error("withState method is not executable!")
+ def withState[U](u: Set[Lazy[U]]): T = sys.error("withState method is not executable!")
@extern
- def withState[U, V](u: Set[$[U]], v: Set[$[V]]): T = sys.error("withState method is not executable!")
+ def withState[U, V](u: Set[Lazy[U]], v: Set[Lazy[V]]): T = sys.error("withState method is not executable!")
@extern
- def withState[U, V, W](u: Set[$[U]], v: Set[$[V]], w: Set[$[W]]): T = sys.error("withState method is not executable!")
+ def withState[U, V, W](u: Set[Lazy[U]], v: Set[Lazy[V]], w: Set[Lazy[W]]): T = sys.error("withState method is not executable!")
@extern
- def withState[U, V, W, X](u: Set[$[U]], v: Set[$[V]], w: Set[$[W]], x: Set[$[X]]): T = sys.error("withState method is not executable!")
+ def withState[U, V, W, X](u: Set[Lazy[U]], v: Set[Lazy[V]], w: Set[Lazy[W]], x: Set[Lazy[X]]): T = sys.error("withState method is not executable!")
// extend this to more arguments if needed
}
+ @library
@inline
implicit def toWithState[T](x: T) = new WithState(x)
- /* @library
- case class Mem[T](v: T) {
- @extern
- def isCached: Boolean = sys.error("not implemented!")
- }
- @inline
- implicit def toMem[T](x: T) = new Mem(x)*/
-
/**
* annotations for monotonicity proofs.
* Note implemented as of now.
@@ -67,72 +67,24 @@ object $ {
*/
@ignore
class monoproof(methodname: String) extends StaticAnnotation
-}
-
-@library
-case class $[T](f: Unit => T) {
- @extern
- lazy val value = {
- val x = f(())
- eval = true
- x
- }
- def * = f(())
-
- @ignore
- var eval = false // is this thread safe ?
-
- @extern
- def isEvaluated = eval
- @extern
- def isSuspension[T](f: T) : Boolean = sys.error("isSuspensionOf method is not executable")
-}
-
-/**
- * The following are set of methods meant for `Memoized` closures
- */
-@library
-object Mem {
- @inline
- implicit def toMem[T](x: T) = new Mem(x)
-
- /**
- * accessing in and out states of mems
- * Should be used only in ensuring.
- * TODO: enforce this.
- */
- @extern
- def inState[T] : Set[Mem[T]] = sys.error("inState method is not executable!")
-
- @extern
- def outState[T] : Set[Mem[T]] = sys.error("outState method is not executable")
-
- /**
- * Helper class for invoking with a given state instead of the implicit state
- */
@library
- case class memWithState[T](v: T) {
+ case class Lazy[T](f: Unit => T) {
@extern
- def withState[U](u: Set[Mem[U]]): T = sys.error("withState method is not executable!")
+ lazy val value = {
+ val x = f(())
+ eval = true
+ x
+ }
+ def * = f(())
- @extern
- def withState[U, V](u: Set[Mem[U]], v: Set[Mem[V]]): T = sys.error("withState method is not executable!")
+ @ignore
+ var eval = false // is this thread safe ?
@extern
- def withState[U, V, W](u: Set[Mem[U]], v: Set[Mem[V]], w: Set[Mem[W]]): T = sys.error("withState method is not executable!")
+ def isEvaluated = eval
@extern
- def withState[U, V, W, X](u: Set[Mem[U]], v: Set[Mem[V]], w: Set[Mem[W]], x: Set[Mem[X]]): T = sys.error("withState method is not executable!")
- // extend this to more arguments if needed
+ def isSuspension[T](f: T): Boolean = sys.error("isSuspensionOf method is not executable")
}
-
- @inline
- implicit def toWithState[T](x: T) = new memWithState(x)
-}
-
-@library
-case class Mem[T](v: T) {
- @extern
- def isCached: Boolean = sys.error("not implemented!")
}
\ No newline at end of file
diff --git a/library/mem/package.scala b/library/mem/package.scala
new file mode 100644
index 0000000000000000000000000000000000000000..416b737acae9b34287dc0f54ee3e6202fe72721e
--- /dev/null
+++ b/library/mem/package.scala
@@ -0,0 +1,56 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
+package leon
+
+import annotation._
+import lang._
+import scala.language.implicitConversions
+import scala.annotation.StaticAnnotation
+
+package object mem {
+
+ @library
+ @inline
+ implicit def toMem[T](x: T) = new Mem(x)
+
+ /**
+ * accessing in and out states of mems
+ * Should be used only in ensuring.
+ */
+ @library
+ @extern
+ def inState[T]: Set[Mem[T]] = sys.error("inState method is not executable!")
+
+ @library
+ @extern
+ def outState[T]: Set[Mem[T]] = sys.error("outState method is not executable")
+
+ /**
+ * Helper class for invoking with a given state instead of the implicit state
+ */
+ @library
+ case class memWithState[T](v: T) {
+ @extern
+ def withState[U](u: Set[Mem[U]]): T = sys.error("withState method is not executable!")
+
+ @extern
+ def withState[U, V](u: Set[Mem[U]], v: Set[Mem[V]]): T = sys.error("withState method is not executable!")
+
+ @extern
+ def withState[U, V, W](u: Set[Mem[U]], v: Set[Mem[V]], w: Set[Mem[W]]): T = sys.error("withState method is not executable!")
+
+ @extern
+ def withState[U, V, W, X](u: Set[Mem[U]], v: Set[Mem[V]], w: Set[Mem[W]], x: Set[Mem[X]]): T = sys.error("withState method is not executable!")
+ // extend this to more arguments if needed
+ }
+
+ @library
+ @inline
+ implicit def toWithState[T](x: T) = new memWithState(x)
+
+ @library
+ case class Mem[T](v: T) {
+ @extern
+ def isCached: Boolean = sys.error("not implemented!")
+ }
+}
\ No newline at end of file
diff --git a/library/stats/package.scala b/library/stats/package.scala
new file mode 100644
index 0000000000000000000000000000000000000000..17d6286b62c3e4de4be5d4c430ea74e26a3abef0
--- /dev/null
+++ b/library/stats/package.scala
@@ -0,0 +1,28 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+
+import leon.annotation._
+import java.lang.management._
+import scala.collection.JavaConversions._
+
+/**
+ * A collection of methods that can be used to collect run-time statistics about Leon programs.
+ * This is mostly used to test the resources properties of Leon programs
+ */
+package object stats {
+ @ignore
+ def timed[T](code: => T)(cont: Long => Unit): T = {
+ var t1 = System.currentTimeMillis()
+ val r = code
+ cont((System.currentTimeMillis() - t1))
+ r
+ }
+
+ @ignore
+ def withTime[T](code: => T): (T, Long) = {
+ var t1 = System.currentTimeMillis()
+ val r = code
+ (r, (System.currentTimeMillis() - t1))
+ }
+}
diff --git a/libtest/build.sbt b/libtest/build.sbt
new file mode 100644
index 0000000000000000000000000000000000000000..9e8ce202fd5b412d33ac2c8c4af85fbbfcaa78fc
--- /dev/null
+++ b/libtest/build.sbt
@@ -0,0 +1,17 @@
+name := "LazyBenchmarkExecution"
+
+version := "1.0"
+
+organization := "ch.epfl.lara"
+
+scalaVersion := "2.11.7"
+
+fork in run := true
+
+unmanagedJars in Compile += file("lib/macmemo.jar")
+
+javaOptions in run ++= Seq("-Xmx5G", "-Xms3G", "-Xss500M")
+
+scalacOptions ++= Seq("-optimise")
+
+libraryDependencies += "org.scala-lang" % "scala-reflect" % "2.11.5"
diff --git a/libtest/project/Build.scala b/libtest/project/Build.scala
new file mode 100644
index 0000000000000000000000000000000000000000..19f93de52fda4fc681b0fb28e0c97ca0593c0ebd
--- /dev/null
+++ b/libtest/project/Build.scala
@@ -0,0 +1,35 @@
+import sbt._
+import Keys._
+
+object BuildSettings {
+ val paradiseVersion = "2.1.0-M5"
+ val buildSettings = Defaults.defaultSettings ++ Seq(
+ resolvers += Resolver.sonatypeRepo("snapshots"),
+ resolvers += Resolver.sonatypeRepo("releases"),
+ addCompilerPlugin("org.scalamacros" % "paradise" % paradiseVersion cross CrossVersion.full)
+ )
+}
+
+object MyBuild extends Build {
+ import BuildSettings._
+
+ lazy val root = Project(
+ "root",
+ file("."),
+ settings = buildSettings
+ )
+
+// aggregate (macros, benchmarks)
+//
+// lazy val macros = Project(
+// "leon",
+// file("src/main/scala/leon"),
+// settings = buildSettings
+// )
+//
+// lazy val benchmarks = Project(
+// "benchmark",
+// file("src/main/scala/benchmarks"),
+// settings = buildSettings
+// ) dependsOn macros
+}
diff --git a/libtest/src/main/scala/leon/annotation/isabelle.scala b/libtest/src/main/scala/leon/annotation/isabelle.scala
new file mode 100644
index 0000000000000000000000000000000000000000..bfb4b39ec1499f270907a861c4d339d82a2d963d
--- /dev/null
+++ b/libtest/src/main/scala/leon/annotation/isabelle.scala
@@ -0,0 +1,31 @@
+package leon.annotation
+
+import scala.annotation.StaticAnnotation
+
+object isabelle {
+
+ @ignore
+ class typ(name: String) extends StaticAnnotation
+
+ @ignore
+ class constructor(name: String) extends StaticAnnotation
+
+ @ignore
+ class function(term: String) extends StaticAnnotation
+
+ @ignore
+ class script(name: String, source: String) extends StaticAnnotation
+
+ @ignore
+ class proof(method: String, kind: String = "") extends StaticAnnotation
+
+ @ignore
+ class fullBody() extends StaticAnnotation
+
+ @ignore
+ class noBody() extends StaticAnnotation
+
+ @ignore
+ class lemma(about: String) extends StaticAnnotation
+
+}
diff --git a/libtest/src/main/scala/leon/annotation/package.scala b/libtest/src/main/scala/leon/annotation/package.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a355a8557072fa277a025f97bb77ebff35302ce8
--- /dev/null
+++ b/libtest/src/main/scala/leon/annotation/package.scala
@@ -0,0 +1,43 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+
+import scala.annotation.StaticAnnotation
+import scala.language.experimental.macros
+
+package object annotation {
+ @ignore
+ class library extends StaticAnnotation
+ @ignore
+ class induct extends StaticAnnotation
+ @ignore
+ class traceInduct(name: String = "") extends StaticAnnotation
+ @ignore
+ class ignore extends StaticAnnotation
+ @ignore
+ class extern extends StaticAnnotation
+ @ignore
+ class inline extends StaticAnnotation
+ @ignore
+ class internal extends StaticAnnotation
+
+ // Orb annotations
+ @ignore
+ class monotonic extends StaticAnnotation
+ @ignore
+ class compose extends StaticAnnotation
+ @ignore
+ class axiom extends StaticAnnotation
+ @ignore
+ class invstate extends StaticAnnotation
+ @ignore
+ class memoize extends StaticAnnotation {
+ def macroTransform(annottees: Any*): Any = macro com.softwaremill.macmemo.memoizeMacro.impl
+ }
+ @ignore
+ class invisibleBody extends StaticAnnotation // do not unfold the body of the function
+ @ignore
+ class usePost extends StaticAnnotation // assume the post-condition while proving time bounds
+ @ignore
+ class unfoldFactor(f: Int=0) extends StaticAnnotation // 0 implies no bound on unfolding
+}
\ No newline at end of file
diff --git a/libtest/src/main/scala/leon/collection/List.scala b/libtest/src/main/scala/leon/collection/List.scala
new file mode 100644
index 0000000000000000000000000000000000000000..74a0f0c66e3bc23780076e16acdc6f7035c6986b
--- /dev/null
+++ b/libtest/src/main/scala/leon/collection/List.scala
@@ -0,0 +1,897 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon.collection
+
+import leon._
+import leon.lang._
+import leon.annotation._
+import leon.math._
+import leon.proof._
+
+@library
+@isabelle.typ(name = "List.list")
+sealed abstract class List[T] {
+
+ @isabelle.function(term = "Int.int o List.length")
+ def size: BigInt = (this match {
+ case Nil() => BigInt(0)
+ case Cons(h, t) => 1 + t.size
+ }) ensuring (_ >= 0)
+
+ def length = size
+
+ @isabelle.function(term = "List.list.set")
+ def content: Set[T] = this match {
+ case Nil() => Set()
+ case Cons(h, t) => Set(h) ++ t.content
+ }
+
+ @isabelle.function(term = "List.member")
+ def contains(v: T): Boolean = (this match {
+ case Cons(h, t) => h == v || t.contains(v)
+ case Nil() => false
+ }) ensuring { _ == (content contains v) }
+
+ @isabelle.function(term = "List.append")
+ def ++(that: List[T]): List[T] = (this match {
+ case Nil() => that
+ case Cons(x, xs) => Cons(x, xs ++ that)
+ }) ensuring { res =>
+ (res.content == this.content ++ that.content) &&
+ (res.size == this.size + that.size) &&
+ (that != Nil[T]() || res == this)
+ }
+
+ def head: T = {
+ require(this != Nil[T]())
+ val Cons(h, _) = this
+ h
+ }
+
+ def tail: List[T] = {
+ require(this != Nil[T]())
+ val Cons(_, t) = this
+ t
+ }
+
+ @isabelle.fullBody
+ def apply(index: BigInt): T = {
+ require(0 <= index && index < size)
+ if (index == BigInt(0)) {
+ head
+ } else {
+ tail(index-1)
+ }
+ }
+
+ @isabelle.function(term = "%xs x. x # xs")
+ def ::(t:T): List[T] = Cons(t, this)
+
+ @isabelle.function(term = "%xs x. xs @ [x]")
+ def :+(t:T): List[T] = {
+ this match {
+ case Nil() => Cons(t, this)
+ case Cons(x, xs) => Cons(x, xs :+ (t))
+ }
+ } ensuring(res => (res.size == size + 1) && (res.content == content ++ Set(t)))
+
+ @isabelle.function(term = "List.rev")
+ def reverse: List[T] = {
+ this match {
+ case Nil() => this
+ case Cons(x,xs) => xs.reverse :+ x
+ }
+ } ensuring (res => (res.size == size) && (res.content == content))
+
+ def take(i: BigInt): List[T] = { (this, i) match {
+ case (Nil(), _) => Nil[T]()
+ case (Cons(h, t), i) =>
+ if (i <= BigInt(0)) {
+ Nil[T]()
+ } else {
+ Cons(h, t.take(i-1))
+ }
+ }} ensuring { res =>
+ res.content.subsetOf(this.content) && (res.size == (
+ if (i <= 0) BigInt(0)
+ else if (i >= this.size) this.size
+ else i
+ ))
+ }
+
+ def drop(i: BigInt): List[T] = { (this, i) match {
+ case (Nil(), _) => Nil[T]()
+ case (Cons(h, t), i) =>
+ if (i <= BigInt(0)) {
+ Cons[T](h, t)
+ } else {
+ t.drop(i-1)
+ }
+ }} ensuring { res =>
+ res.content.subsetOf(this.content) && (res.size == (
+ if (i <= 0) this.size
+ else if (i >= this.size) BigInt(0)
+ else this.size - i
+ ))
+ }
+
+ def slice(from: BigInt, to: BigInt): List[T] = {
+ require(0 <= from && from <= to && to <= size)
+ drop(from).take(to-from)
+ }
+
+ def replace(from: T, to: T): List[T] = { this match {
+ case Nil() => Nil[T]()
+ case Cons(h, t) =>
+ val r = t.replace(from, to)
+ if (h == from) {
+ Cons(to, r)
+ } else {
+ Cons(h, r)
+ }
+ }} ensuring { (res: List[T]) =>
+ res.size == this.size &&
+ res.content == (
+ (this.content -- Set(from)) ++
+ (if (this.content contains from) Set(to) else Set[T]())
+ )
+ }
+
+ private def chunk0(s: BigInt, l: List[T], acc: List[T], res: List[List[T]], s0: BigInt): List[List[T]] = {
+ require(s > 0 && s0 >= 0)
+ l match {
+ case Nil() =>
+ if (acc.size > 0) {
+ res :+ acc
+ } else {
+ res
+ }
+ case Cons(h, t) =>
+ if (s0 == BigInt(0)) {
+ chunk0(s, t, Cons(h, Nil()), res :+ acc, s-1)
+ } else {
+ chunk0(s, t, acc :+ h, res, s0-1)
+ }
+ }
+ }
+
+ def chunks(s: BigInt): List[List[T]] = {
+ require(s > 0)
+
+ chunk0(s, this, Nil(), Nil(), s)
+ }
+
+ @isabelle.function(term = "List.zip")
+ def zip[B](that: List[B]): List[(T, B)] = { (this, that) match {
+ case (Cons(h1, t1), Cons(h2, t2)) =>
+ Cons((h1, h2), t1.zip(t2))
+ case _ =>
+ Nil[(T, B)]()
+ }} ensuring { _.size == (
+ if (this.size <= that.size) this.size else that.size
+ )}
+
+ @isabelle.function(term = "%xs x. removeAll x xs")
+ def -(e: T): List[T] = { this match {
+ case Cons(h, t) =>
+ if (e == h) {
+ t - e
+ } else {
+ Cons(h, t - e)
+ }
+ case Nil() =>
+ Nil[T]()
+ }} ensuring { res =>
+ res.size <= this.size &&
+ res.content == this.content -- Set(e)
+ }
+
+ def --(that: List[T]): List[T] = { this match {
+ case Cons(h, t) =>
+ if (that.contains(h)) {
+ t -- that
+ } else {
+ Cons(h, t -- that)
+ }
+ case Nil() =>
+ Nil[T]()
+ }} ensuring { res =>
+ res.size <= this.size &&
+ res.content == this.content -- that.content
+ }
+
+ def &(that: List[T]): List[T] = { this match {
+ case Cons(h, t) =>
+ if (that.contains(h)) {
+ Cons(h, t & that)
+ } else {
+ t & that
+ }
+ case Nil() =>
+ Nil[T]()
+ }} ensuring { res =>
+ res.size <= this.size &&
+ res.content == (this.content & that.content)
+ }
+
+ def padTo(s: BigInt, e: T): List[T] = { (this, s) match {
+ case (_, s) if s <= 0 =>
+ this
+ case (Nil(), s) =>
+ Cons(e, Nil().padTo(s-1, e))
+ case (Cons(h, t), s) =>
+ Cons(h, t.padTo(s-1, e))
+ }} ensuring { res =>
+ if (s <= this.size)
+ res == this
+ else
+ res.size == s &&
+ res.content == this.content ++ Set(e)
+ }
+
+ def find(e: T): Option[BigInt] = { this match {
+ case Nil() => None[BigInt]()
+ case Cons(h, t) =>
+ if (h == e) {
+ Some[BigInt](0)
+ } else {
+ t.find(e) match {
+ case None() => None[BigInt]()
+ case Some(i) => Some(i+1)
+ }
+ }
+ }} ensuring { res => !res.isDefined || (this.content contains e) }
+
+ def init: List[T] = {
+ require(!isEmpty)
+ ((this : @unchecked) match {
+ case Cons(h, Nil()) =>
+ Nil[T]()
+ case Cons(h, t) =>
+ Cons[T](h, t.init)
+ })
+ } ensuring ( (r: List[T]) =>
+ r.size == this.size - 1 &&
+ r.content.subsetOf(this.content)
+ )
+
+ def last: T = {
+ require(!isEmpty)
+ (this : @unchecked) match {
+ case Cons(h, Nil()) => h
+ case Cons(_, t) => t.last
+ }
+ } ensuring { this.contains _ }
+
+ def lastOption: Option[T] = { this match {
+ case Cons(h, t) =>
+ t.lastOption.orElse(Some(h))
+ case Nil() =>
+ None[T]()
+ }} ensuring { _.isDefined != this.isEmpty }
+
+ def headOption: Option[T] = { this match {
+ case Cons(h, t) =>
+ Some(h)
+ case Nil() =>
+ None[T]()
+ }} ensuring { _.isDefined != this.isEmpty }
+
+ def tailOption: Option[List[T]] = { this match {
+ case Cons(h, t) =>
+ Some(t)
+ case Nil() =>
+ None[List[T]]()
+ }} ensuring { _.isDefined != this.isEmpty }
+
+
+ def unique: List[T] = this match {
+ case Nil() => Nil()
+ case Cons(h, t) =>
+ Cons(h, t.unique - h)
+ }
+
+ def splitAt(e: T): List[List[T]] = split(Cons(e, Nil()))
+
+ def split(seps: List[T]): List[List[T]] = this match {
+ case Cons(h, t) =>
+ if (seps.contains(h)) {
+ Cons(Nil(), t.split(seps))
+ } else {
+ val r = t.split(seps)
+ Cons(Cons(h, r.head), r.tail)
+ }
+ case Nil() =>
+ Cons(Nil(), Nil())
+ }
+
+ def evenSplit: (List[T], List[T]) = {
+ val c = size/2
+ (take(c), drop(c))
+ }
+
+ def splitAtIndex(index: BigInt) : (List[T], List[T]) = { this match {
+ case Nil() => (Nil[T](), Nil[T]())
+ case Cons(h, rest) => {
+ if (index <= BigInt(0)) {
+ (Nil[T](), this)
+ } else {
+ val (left,right) = rest.splitAtIndex(index - 1)
+ (Cons[T](h,left), right)
+ }
+ }
+ }} ensuring { (res:(List[T],List[T])) =>
+ res._1 ++ res._2 == this &&
+ res._1 == take(index) && res._2 == drop(index)
+ }
+
+ def updated(i: BigInt, y: T): List[T] = {
+ require(0 <= i && i < this.size)
+ this match {
+ case Cons(x, tail) if i == 0 =>
+ Cons[T](y, tail)
+ case Cons(x, tail) =>
+ Cons[T](x, tail.updated(i - 1, y))
+ }
+ }
+
+ private def insertAtImpl(pos: BigInt, l: List[T]): List[T] = {
+ require(0 <= pos && pos <= size)
+ if(pos == BigInt(0)) {
+ l ++ this
+ } else {
+ this match {
+ case Cons(h, t) =>
+ Cons(h, t.insertAtImpl(pos-1, l))
+ case Nil() =>
+ l
+ }
+ }
+ } ensuring { res =>
+ res.size == this.size + l.size &&
+ res.content == this.content ++ l.content
+ }
+
+ def insertAt(pos: BigInt, l: List[T]): List[T] = {
+ require(-pos <= size && pos <= size)
+ if(pos < 0) {
+ insertAtImpl(size + pos, l)
+ } else {
+ insertAtImpl(pos, l)
+ }
+ } ensuring { res =>
+ res.size == this.size + l.size &&
+ res.content == this.content ++ l.content
+ }
+
+ def insertAt(pos: BigInt, e: T): List[T] = {
+ require(-pos <= size && pos <= size)
+ insertAt(pos, Cons[T](e, Nil()))
+ } ensuring { res =>
+ res.size == this.size + 1 &&
+ res.content == this.content ++ Set(e)
+ }
+
+ private def replaceAtImpl(pos: BigInt, l: List[T]): List[T] = {
+ require(0 <= pos && pos <= size)
+ if (pos == BigInt(0)) {
+ l ++ this.drop(l.size)
+ } else {
+ this match {
+ case Cons(h, t) =>
+ Cons(h, t.replaceAtImpl(pos-1, l))
+ case Nil() =>
+ l
+ }
+ }
+ } ensuring { res =>
+ res.content.subsetOf(l.content ++ this.content)
+ }
+
+ def replaceAt(pos: BigInt, l: List[T]): List[T] = {
+ require(-pos <= size && pos <= size)
+ if(pos < 0) {
+ replaceAtImpl(size + pos, l)
+ } else {
+ replaceAtImpl(pos, l)
+ }
+ } ensuring { res =>
+ res.content.subsetOf(l.content ++ this.content)
+ }
+
+ def rotate(s: BigInt): List[T] = {
+ if (isEmpty) {
+ Nil[T]()
+ } else {
+ drop(s mod size) ++ take(s mod size)
+ }
+ } ensuring { res =>
+ res.size == this.size
+ }
+
+ @isabelle.function(term = "List.null")
+ def isEmpty = this match {
+ case Nil() => true
+ case _ => false
+ }
+
+ def nonEmpty = !isEmpty
+
+ // Higher-order API
+ @isabelle.function(term = "%xs f. List.list.map f xs")
+ def map[R](f: T => R): List[R] = { this match {
+ case Nil() => Nil[R]()
+ case Cons(h, t) => f(h) :: t.map(f)
+ }} ensuring { _.size == this.size }
+
+ @isabelle.function(term = "%bs a f. List.foldl f a bs")
+ def foldLeft[R](z: R)(f: (R,T) => R): R = this match {
+ case Nil() => z
+ case Cons(h,t) => t.foldLeft(f(z,h))(f)
+ }
+
+ @isabelle.function(term = "%as b f. List.foldr f as b")
+ def foldRight[R](z: R)(f: (T,R) => R): R = this match {
+ case Nil() => z
+ case Cons(h, t) => f(h, t.foldRight(z)(f))
+ }
+
+ def scanLeft[R](z: R)(f: (R,T) => R): List[R] = { this match {
+ case Nil() => z :: Nil()
+ case Cons(h,t) => z :: t.scanLeft(f(z,h))(f)
+ }} ensuring { !_.isEmpty }
+
+ def scanRight[R](z: R)(f: (T,R) => R): List[R] = { this match {
+ case Nil() => z :: Nil[R]()
+ case Cons(h, t) =>
+ val rest@Cons(h1,_) = t.scanRight(z)(f)
+ f(h, h1) :: rest
+ }} ensuring { !_.isEmpty }
+
+ @isabelle.function(term = "List.bind")
+ def flatMap[R](f: T => List[R]): List[R] =
+ ListOps.flatten(this map f)
+
+ def filter(p: T => Boolean): List[T] = { this match {
+ case Nil() => Nil[T]()
+ case Cons(h, t) if p(h) => Cons(h, t.filter(p))
+ case Cons(_, t) => t.filter(p)
+ }} ensuring { res =>
+ res.size <= this.size &&
+ res.content.subsetOf(this.content) &&
+ res.forall(p)
+ }
+
+ def filterNot(p: T => Boolean): List[T] =
+ filter(!p(_)) ensuring { res =>
+ res.size <= this.size &&
+ res.content.subsetOf(this.content) &&
+ res.forall(!p(_))
+ }
+
+ def partition(p: T => Boolean): (List[T], List[T]) = { this match {
+ case Nil() => (Nil[T](), Nil[T]())
+ case Cons(h, t) =>
+ val (l1, l2) = t.partition(p)
+ if (p(h)) (h :: l1, l2)
+ else (l1, h :: l2)
+ }} ensuring { res =>
+ res._1 == filter(p) &&
+ res._2 == filterNot(p)
+ }
+
+ // In case we implement for-comprehensions
+ def withFilter(p: T => Boolean) = filter(p)
+
+ @isabelle.function(term = "%xs P. List.list_all P xs")
+ def forall(p: T => Boolean): Boolean = this match {
+ case Nil() => true
+ case Cons(h, t) => p(h) && t.forall(p)
+ }
+
+ @isabelle.function(term = "%xs P. List.list_ex P xs")
+ def exists(p: T => Boolean) = !forall(!p(_))
+
+ @isabelle.function(term = "%xs P. List.find P xs")
+ def find(p: T => Boolean): Option[T] = { this match {
+ case Nil() => None[T]()
+ case Cons(h, t) => if (p(h)) Some(h) else t.find(p)
+ }} ensuring { res => res match {
+ case Some(r) => (content contains r) && p(r)
+ case None() => true
+ }}
+
+ def groupBy[R](f: T => R): Map[R, List[T]] = this match {
+ case Nil() => Map.empty[R, List[T]]
+ case Cons(h, t) =>
+ val key: R = f(h)
+ val rest: Map[R, List[T]] = t.groupBy(f)
+ val prev: List[T] = if (rest isDefinedAt key) rest(key) else Nil[T]()
+ (rest ++ Map((key, h :: prev))) : Map[R, List[T]]
+ }
+
+ def takeWhile(p: T => Boolean): List[T] = { this match {
+ case Cons(h,t) if p(h) => Cons(h, t.takeWhile(p))
+ case _ => Nil[T]()
+ }} ensuring { res =>
+ (res forall p) &&
+ (res.size <= this.size) &&
+ (res.content subsetOf this.content)
+ }
+
+ def dropWhile(p: T => Boolean): List[T] = { this match {
+ case Cons(h,t) if p(h) => t.dropWhile(p)
+ case _ => this
+ }} ensuring { res =>
+ (res.size <= this.size) &&
+ (res.content subsetOf this.content) &&
+ (res.isEmpty || !p(res.head))
+ }
+
+ def count(p: T => Boolean): BigInt = { this match {
+ case Nil() => BigInt(0)
+ case Cons(h, t) =>
+ (if (p(h)) BigInt(1) else BigInt(0)) + t.count(p)
+ }} ensuring {
+ _ == this.filter(p).size
+ }
+
+ def indexWhere(p: T => Boolean): BigInt = { this match {
+ case Nil() => BigInt(-1)
+ case Cons(h, _) if p(h) => BigInt(0)
+ case Cons(_, t) =>
+ val rec = t.indexWhere(p)
+ if (rec >= 0) rec + BigInt(1)
+ else BigInt(-1)
+ }} ensuring {
+ _ >= BigInt(0) == (this exists p)
+ }
+
+
+ // Translation to other collections
+ def toSet: Set[T] = foldLeft(Set[T]()){
+ case (current, next) => current ++ Set(next)
+ }
+
+}
+
+@isabelle.constructor(name = "List.list.Cons")
+case class Cons[T](h: T, t: List[T]) extends List[T]
+
+@isabelle.constructor(name = "List.list.Nil")
+case class Nil[T]() extends List[T]
+
+object List {
+ @ignore
+ def apply[T](elems: T*): List[T] = {
+ var l: List[T] = Nil[T]()
+ for (e <- elems) {
+ l = Cons(e, l)
+ }
+ l.reverse
+ }
+
+ @library
+ def fill[T](n: BigInt)(x: T) : List[T] = {
+ if (n <= 0) Nil[T]
+ else Cons[T](x, fill[T](n-1)(x))
+ } ensuring(res => (res.content == (if (n <= BigInt(0)) Set.empty[T] else Set(x))) &&
+ res.size == (if (n <= BigInt(0)) BigInt(0) else n))
+}
+
+@library
+object ListOps {
+ @isabelle.function(term = "List.concat")
+ def flatten[T](ls: List[List[T]]): List[T] = ls match {
+ case Cons(h, t) => h ++ flatten(t)
+ case Nil() => Nil()
+ }
+
+ def isSorted(ls: List[BigInt]): Boolean = ls match {
+ case Nil() => true
+ case Cons(_, Nil()) => true
+ case Cons(h1, Cons(h2, _)) if(h1 > h2) => false
+ case Cons(_, t) => isSorted(t)
+ }
+
+ def sorted(ls: List[BigInt]): List[BigInt] = { ls match {
+ case Cons(h, t) => sortedIns(sorted(t), h)
+ case Nil() => Nil[BigInt]()
+ }} ensuring { isSorted _ }
+
+ private def sortedIns(ls: List[BigInt], v: BigInt): List[BigInt] = {
+ require(isSorted(ls))
+ ls match {
+ case Nil() => Cons(v, Nil())
+ case Cons(h, t) =>
+ if (v <= h) {
+ Cons(v, t)
+ } else {
+ Cons(h, sortedIns(t, v))
+ }
+ }
+ } ensuring { isSorted _ }
+
+ def toMap[K, V](l: List[(K, V)]): Map[K, V] = l.foldLeft(Map[K, V]()){
+ case (current, (k, v)) => current ++ Map(k -> v)
+ }
+}
+
+// 'Cons' Extractor
+object :: {
+ @library
+ def unapply[A](l: List[A]): Option[(A, List[A])] = l match {
+ case Nil() => None()
+ case Cons(x, xs) => Some((x, xs))
+ }
+}
+
+
+import ListOps._
+
+@library
+object ListSpecs {
+ def snocIndex[T](l: List[T], t: T, i: BigInt): Boolean = {
+ require(0 <= i && i < l.size + 1)
+ ((l :+ t).apply(i) == (if (i < l.size) l(i) else t)) because
+ (l match {
+ case Nil() => true
+ case Cons(x, xs) => if (i > 0) snocIndex[T](xs, t, i-1) else true
+ })
+ }.holds
+
+ @induct
+ @isabelle.lemma(about = "leon.collection.List.apply")
+ def consIndex[T](h: T, t: List[T], i: BigInt): Boolean = {
+ require(0 <= i && i < t.size + 1)
+ (h :: t).apply(i) == (if (i == 0) h else t.apply(i - 1))
+ }.holds
+
+ def reverseIndex[T](l: List[T], i: BigInt): Boolean = {
+ require(0 <= i && i < l.size)
+ (l.reverse.apply(i) == l.apply(l.size - 1 - i)) because
+ (l match {
+ case Nil() => true
+ case Cons(x,xs) => snocIndex(xs.reverse, x, i) && (if (i < xs.size) consIndex(x, xs, l.size - 1 - i) && reverseIndex[T](xs, i) else true)
+ })
+ }.holds
+
+ def snocLast[T](l: List[T], x: T): Boolean = {
+ ((l :+ x).last == x) because {
+ l match {
+ case Nil() => true
+ case Cons(y, ys) => {
+ ((y :: ys) :+ x).last ==| trivial |
+ (y :: (ys :+ x)).last ==| trivial |
+ (ys :+ x).last ==| snocLast(ys, x) |
+ x
+ }.qed
+ }
+ }
+ }.holds
+
+ def headReverseLast[T](l: List[T]): Boolean = {
+ require (!l.isEmpty)
+ (l.head == l.reverse.last) because {
+ val Cons(x, xs) = l;
+ {
+ (x :: xs).head ==| trivial |
+ x ==| snocLast(xs.reverse, x) |
+ (xs.reverse :+ x).last ==| trivial |
+ (x :: xs).reverse.last
+ }.qed
+ }
+ }.holds
+
+ def appendIndex[T](l1: List[T], l2: List[T], i: BigInt): Boolean = {
+ require(0 <= i && i < l1.size + l2.size)
+ ( (l1 ++ l2).apply(i) == (if (i < l1.size) l1(i) else l2(i - l1.size)) ) because {
+ l1 match {
+ case Nil() => true
+ case Cons(x,xs) =>
+ (i != BigInt(0)) ==> appendIndex[T](xs, l2, i - 1)
+ }
+ }
+ }.holds
+
+ @induct
+ def appendAssoc[T](l1: List[T], l2: List[T], l3: List[T]): Boolean = {
+ (l1 ++ l2) ++ l3 == l1 ++ (l2 ++ l3)
+ }.holds
+
+ @induct
+ def rightUnitAppend[T](l1: List[T]): Boolean = {
+ l1 ++ Nil() == l1
+ }.holds
+
+ // This follows immediately from the definition of `++` but we
+ // include it here anyway for completeness.
+ def leftUnitAppend[T](l1: List[T]): Boolean = {
+ Nil() ++ l1 == l1
+ }.holds
+
+ def snocIsAppend[T](l: List[T], t: T): Boolean = {
+ ( (l :+ t) == l ++ Cons[T](t, Nil()) ) because {
+ l match {
+ case Nil() => true
+ case Cons(x,xs) => snocIsAppend(xs,t)
+ }
+ }
+ }.holds
+
+ def snocAfterAppend[T](l1: List[T], l2: List[T], t: T): Boolean = {
+ ( (l1 ++ l2) :+ t == l1 ++ (l2 :+ t) ) because {
+ l1 match {
+ case Nil() => true
+ case Cons(x,xs) => snocAfterAppend(xs,l2,t)
+ }
+ }
+ }.holds
+
+ def snocReverse[T](l: List[T], t: T): Boolean = {
+ ( (l :+ t).reverse == Cons(t, l.reverse) ) because {
+ l match {
+ case Nil() => true
+ case Cons(x,xs) => snocReverse(xs,t)
+ }
+ }
+ }.holds
+
+ def reverseReverse[T](l: List[T]): Boolean = {
+ l.reverse.reverse == l because {
+ l match {
+ case Nil() => trivial
+ case Cons(x, xs) => {
+ (xs.reverse :+ x).reverse ==| snocReverse[T](xs.reverse, x) |
+ x :: xs.reverse.reverse ==| reverseReverse[T](xs) |
+ (x :: xs)
+ }.qed
+ }
+ }
+ }.holds
+
+ def reverseAppend[T](l1: List[T], l2: List[T]): Boolean = {
+ ( (l1 ++ l2).reverse == l2.reverse ++ l1.reverse ) because {
+ l1 match {
+ case Nil() => {
+ (Nil() ++ l2).reverse ==| trivial |
+ l2.reverse ==| rightUnitAppend(l2.reverse) |
+ l2.reverse ++ Nil() ==| trivial |
+ l2.reverse ++ Nil().reverse
+ }.qed
+ case Cons(x, xs) => {
+ ((x :: xs) ++ l2).reverse ==| trivial |
+ (x :: (xs ++ l2)).reverse ==| trivial |
+ (xs ++ l2).reverse :+ x ==| reverseAppend(xs, l2) |
+ (l2.reverse ++ xs.reverse) :+ x ==|
+ snocAfterAppend(l2.reverse, xs.reverse, x) |
+ l2.reverse ++ (xs.reverse :+ x) ==| trivial |
+ l2.reverse ++ (x :: xs).reverse
+ }.qed
+ }
+ }
+ }.holds
+
+ def snocFoldRight[A, B](xs: List[A], y: A, z: B, f: (A, B) => B): Boolean = {
+ ( (xs :+ y).foldRight(z)(f) == xs.foldRight(f(y, z))(f) ) because {
+ xs match {
+ case Nil() => true
+ case Cons(x, xs) => snocFoldRight(xs, y, z, f)
+ }
+ }
+ }.holds
+
+ def folds[A, B](xs: List[A], z: B, f: (B, A) => B): Boolean = {
+ val f2 = (x: A, z: B) => f(z, x)
+ ( xs.foldLeft(z)(f) == xs.reverse.foldRight(z)(f2) ) because {
+ xs match {
+ case Nil() => true
+ case Cons(x, xs) => {
+ (x :: xs).foldLeft(z)(f) ==| trivial |
+ xs.foldLeft(f(z, x))(f) ==| folds(xs, f(z, x), f) |
+ xs.reverse.foldRight(f(z, x))(f2) ==| trivial |
+ xs.reverse.foldRight(f2(x, z))(f2) ==|
+ snocFoldRight(xs.reverse, x, z, f2) |
+ (xs.reverse :+ x).foldRight(z)(f2) ==| trivial |
+ (x :: xs).reverse.foldRight(z)(f2)
+ }.qed
+ }
+ }
+ }.holds
+
+ def scanVsFoldLeft[A, B](l: List[A], z: B, f: (B, A) => B): Boolean = {
+ ( l.scanLeft(z)(f).last == l.foldLeft(z)(f) ) because {
+ l match {
+ case Nil() => true
+ case Cons(x, xs) => scanVsFoldLeft(xs, f(z, x), f)
+ }
+ }
+ }.holds
+
+ //// my hand calculation shows this should work, but it does not seem to be found
+ //def associative[T,U](l1: List[T], l2: List[T], f: List[T] => U, op: (U,U) => U) = {
+ // f(l1 ++ l2) == op(f(l1), f(l2))
+ //}
+ //
+ //def existsAssoc[T](l1: List[T], l2: List[T], p: T => Boolean) = {
+ // associative[T, Boolean](l1, l2, _.exists(p), _ || _ )
+ //}.holds
+ //
+ //def forallAssoc[T](l1: List[T], l2: List[T], p: T => Boolean) = {
+ // associative[T, Boolean](l1, l2, _.exists(p), _ && _ )
+ //}.holds
+
+ @induct
+ def scanVsFoldRight[A,B](l: List[A], z: B, f: (A,B) => B): Boolean = {
+ l.scanRight(z)(f).head == l.foldRight(z)(f)
+ }.holds
+
+ def appendContent[A](l1: List[A], l2: List[A]) = {
+ l1.content ++ l2.content == (l1 ++ l2).content
+ }.holds
+
+ def flattenPreservesContent[T](ls: List[List[T]]): Boolean = {
+ val f: (List[T], Set[T]) => Set[T] = _.content ++ _
+ ( flatten(ls).content == ls.foldRight(Set[T]())(f) ) because {
+ ls match {
+ case Nil() => true
+ case Cons(h, t) => {
+ flatten(h :: t).content ==| trivial |
+ (h ++ flatten(t)).content ==| appendContent(h, flatten(t)) |
+ h.content ++ flatten(t).content ==| flattenPreservesContent(t) |
+ h.content ++ t.foldRight(Set[T]())(f) ==| trivial |
+ f(h, Set[T]()) ++ t.foldRight(Set[T]())(f) ==| trivial |
+ (h :: t).foldRight(Set[T]())(f)
+ }.qed
+ }
+ }
+ }.holds
+
+ // A lemma about `append` and `updated`
+ def appendUpdate[T](l1: List[T], l2: List[T], i: BigInt, y: T): Boolean = {
+ require(0 <= i && i < l1.size + l2.size)
+ // induction scheme
+ (l1 match {
+ case Nil() => true
+ case Cons(x, xs) => if (i == 0) true else appendUpdate[T](xs, l2, i - 1, y)
+ }) &&
+ // lemma
+ ((l1 ++ l2).updated(i, y) == (
+ if (i < l1.size)
+ l1.updated(i, y) ++ l2
+ else
+ l1 ++ l2.updated(i - l1.size, y)))
+ }.holds
+
+ // a lemma about `append`, `take` and `drop`
+ def appendTakeDrop[T](l1: List[T], l2: List[T], n: BigInt): Boolean = {
+ //induction scheme
+ (l1 match {
+ case Nil() => true
+ case Cons(x, xs) => if (n <= 0) true else appendTakeDrop[T](xs, l2, n - 1)
+ }) &&
+ // lemma
+ ((l1 ++ l2).take(n) == (
+ if (n < l1.size) l1.take(n)
+ else if (n > l1.size) l1 ++ l2.take(n - l1.size)
+ else l1)) &&
+ ((l1 ++ l2).drop(n) == (
+ if (n < l1.size) l1.drop(n) ++ l2
+ else if (n > l1.size) l2.drop(n - l1.size)
+ else l2))
+ }.holds
+
+ // A lemma about `append` and `insertAt`
+ def appendInsert[T](l1: List[T], l2: List[T], i: BigInt, y: T): Boolean = {
+ require(0 <= i && i <= l1.size + l2.size)
+ (l1 match {
+ case Nil() => true
+ case Cons(x, xs) => if (i == 0) true else appendInsert[T](xs, l2, i - 1, y)
+ }) &&
+ // lemma
+ ((l1 ++ l2).insertAt(i, y) == (
+ if (i < l1.size) l1.insertAt(i, y) ++ l2
+ else l1 ++ l2.insertAt((i - l1.size), y)))
+ }.holds
+
+}
diff --git a/libtest/src/main/scala/leon/collection/package.scala b/libtest/src/main/scala/leon/collection/package.scala
new file mode 100644
index 0000000000000000000000000000000000000000..8a5ae170763909c20153f373915d6a4e9e726ca0
--- /dev/null
+++ b/libtest/src/main/scala/leon/collection/package.scala
@@ -0,0 +1,25 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+
+import leon.annotation._
+import leon.collection.List
+import leon.lang._
+import leon.lang.synthesis.choose
+
+package object collection {
+
+ @internal @library
+ def setToList[A](set: Set[A]): List[A] = choose {
+ (x: List[A]) => x.content == set
+ }
+
+ @library
+ def setForall[A](set: Set[A], p: A => Boolean): Boolean =
+ setToList(set).forall(p)
+
+ @library
+ def setExists[A](set: Set[A], p: A => Boolean): Boolean =
+ setToList(set).exists(p)
+
+}
diff --git a/libtest/src/main/scala/leon/instrumentation/package.scala b/libtest/src/main/scala/leon/instrumentation/package.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a6e7545c0b4ab2bae468b0cc6556f67784487b17
--- /dev/null
+++ b/libtest/src/main/scala/leon/instrumentation/package.scala
@@ -0,0 +1,24 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+
+import leon.annotation._
+import leon.lang._
+import scala.language.implicitConversions
+
+package object instrumentation {
+ @library
+ def time: BigInt = 0
+
+ @library
+ def stack: BigInt = 0
+
+ @library
+ def rec: BigInt = 0
+
+ @library
+ def depth: BigInt = 0
+
+ @library
+ def tpr: BigInt = 0
+}
diff --git a/libtest/src/main/scala/leon/invariant/package.scala b/libtest/src/main/scala/leon/invariant/package.scala
new file mode 100644
index 0000000000000000000000000000000000000000..0cc7919d0194a5dff25457c38db8cd00c78db8bd
--- /dev/null
+++ b/libtest/src/main/scala/leon/invariant/package.scala
@@ -0,0 +1,26 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+
+import leon.annotation._
+import leon.lang._
+import scala.language.implicitConversions
+
+package object invariant {
+ @library
+ def tmpl(templateFunc: BigInt => Boolean): Boolean = true
+ @library
+ def tmpl(templateFunc: (BigInt, BigInt) => Boolean): Boolean = true
+ @library
+ def tmpl(templateFunc: (BigInt, BigInt, BigInt) => Boolean): Boolean = true
+ @library
+ def tmpl(templateFunc: (BigInt, BigInt, BigInt, BigInt) => Boolean): Boolean = true
+ @library
+ def tmpl(templateFunc: (BigInt, BigInt, BigInt, BigInt, BigInt) => Boolean): Boolean = true
+
+ @library
+ def ? : BigInt = 0
+
+ @library
+ def ?(id: BigInt) = id
+}
diff --git a/libtest/src/main/scala/leon/lang/Dummy.scala b/libtest/src/main/scala/leon/lang/Dummy.scala
new file mode 100644
index 0000000000000000000000000000000000000000..41dbe4f90ccea298a17de70caa2f3d04ebdc0def
--- /dev/null
+++ b/libtest/src/main/scala/leon/lang/Dummy.scala
@@ -0,0 +1,3 @@
+package leon.lang
+
+case class Dummy[T]()
diff --git a/libtest/src/main/scala/leon/lang/Either.scala b/libtest/src/main/scala/leon/lang/Either.scala
new file mode 100644
index 0000000000000000000000000000000000000000..9cc2ea4e9537b424cbce6963e2a4038f3480d01a
--- /dev/null
+++ b/libtest/src/main/scala/leon/lang/Either.scala
@@ -0,0 +1,27 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon.lang
+
+import leon.annotation._
+
+/**
+ * @author Viktor
+ */
+@library
+sealed abstract class Either[A,B] {
+ def isLeft : Boolean
+ def isRight : Boolean
+ def swap : Either[B,A]
+}
+@library
+case class Left[A,B](content: A) extends Either[A,B] {
+ def isLeft = true
+ def isRight = false
+ def swap = Right[B,A](content)
+}
+@library
+case class Right[A,B](content: B) extends Either[A,B] {
+ def isLeft = false
+ def isRight = true
+ def swap = Left[B,A](content)
+}
\ No newline at end of file
diff --git a/libtest/src/main/scala/leon/lang/Map.scala b/libtest/src/main/scala/leon/lang/Map.scala
new file mode 100644
index 0000000000000000000000000000000000000000..aff6f26f80d5e4abc7d8fa70d3a6553ebdff1c17
--- /dev/null
+++ b/libtest/src/main/scala/leon/lang/Map.scala
@@ -0,0 +1,33 @@
+package leon.lang
+import leon.annotation._
+
+object Map {
+ @library
+ @isabelle.function(term = "Map.empty")
+ def empty[A,B] = Map[A,B]()
+
+ @ignore
+ def apply[A,B](elems: (A,B)*) = {
+ new Map[A,B](scala.collection.immutable.Map[A,B](elems : _*))
+ }
+}
+
+@ignore
+case class Map[A, B] (theMap: scala.collection.immutable.Map[A,B]) {
+ def apply(k: A): B = theMap.apply(k)
+ def ++(b: Map[A, B]): Map[A,B] = new Map (theMap ++ b.theMap)
+ def updated(k: A, v: B): Map[A,B] = new Map(theMap.updated(k, v))
+ def contains(a: A): Boolean = theMap.contains(a)
+ def isDefinedAt(a: A): Boolean = contains(a)
+
+ def +(kv: (A, B)): Map[A,B] = updated(kv._1, kv._2)
+ def +(k: A, v: B): Map[A,B] = updated(k, v)
+
+ def getOrElse(k: A, default: B): B = get(k).getOrElse(default)
+
+ def get(k: A): Option[B] = if (contains(k)) {
+ Some[B](apply(k))
+ } else {
+ None[B]()
+ }
+}
diff --git a/libtest/src/main/scala/leon/lang/Option.scala b/libtest/src/main/scala/leon/lang/Option.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a6f09db68f3fecc7ad8095506a49d21e4d8ac7ad
--- /dev/null
+++ b/libtest/src/main/scala/leon/lang/Option.scala
@@ -0,0 +1,84 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon.lang
+
+import leon.annotation._
+import leon.collection._
+
+@library
+@isabelle.typ(name = "Option.option")
+sealed abstract class Option[T] {
+
+ def get : T = {
+ require(this.isDefined)
+ (this : @unchecked) match {
+ case Some(x) => x
+ }
+ }
+
+ def getOrElse(default: T) = this match {
+ case Some(v) => v
+ case None() => default
+ }
+
+ def orElse(or: Option[T]) = { this match {
+ case Some(v) => this
+ case None() => or
+ }} ensuring {
+ _.isDefined == this.isDefined || or.isDefined
+ }
+
+ def isEmpty = this match {
+ case Some(v) => false
+ case None() => true
+ }
+
+ def nonEmpty = !isEmpty
+
+ def isDefined = !isEmpty
+
+
+ // Higher-order API
+ @isabelle.function(term = "%x f. Option.map_option f x")
+ def map[R](f: T => R) = { this match {
+ case None() => None[R]()
+ case Some(x) => Some(f(x))
+ }} ensuring { _.isDefined == this.isDefined }
+
+ @isabelle.function(term = "Option.bind")
+ def flatMap[R](f: T => Option[R]) = this match {
+ case None() => None[R]()
+ case Some(x) => f(x)
+ }
+
+ def filter(p: T => Boolean) = this match {
+ case Some(x) if p(x) => Some(x)
+ case _ => None[T]()
+ }
+
+ def withFilter(p: T => Boolean) = filter(p)
+
+ def forall(p: T => Boolean) = this match {
+ case Some(x) if !p(x) => false
+ case _ => true
+ }
+
+ def exists(p: T => Boolean) = !forall(!p(_))
+
+ // Transformation to other collections
+ def toList: List[T] = this match {
+ case None() => Nil[T]()
+ case Some(x) => List(x)
+ }
+
+ def toSet: Set[T] = this match {
+ case None() => Set[T]()
+ case Some(x) => Set(x)
+ }
+}
+
+@isabelle.constructor(name = "Option.option.Some")
+case class Some[T](v: T) extends Option[T]
+
+@isabelle.constructor(name = "Option.option.None")
+case class None[T]() extends Option[T]
diff --git a/libtest/src/main/scala/leon/lang/Rational.scala b/libtest/src/main/scala/leon/lang/Rational.scala
new file mode 100644
index 0000000000000000000000000000000000000000..1bcb679a0d4abf6b168117b2af819fa41e027315
--- /dev/null
+++ b/libtest/src/main/scala/leon/lang/Rational.scala
@@ -0,0 +1,85 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon.lang
+
+import leon.annotation._
+
+import scala.language.implicitConversions
+
+@library
+case class Rational(numerator: BigInt, denominator: BigInt) {
+
+ require(this.isRational)
+
+ def +(that: Rational): Rational = {
+ Rational(this.numerator*that.denominator + that.numerator*this.denominator, this.denominator*that.denominator)
+ } ensuring(res => res.isRational)
+
+ def -(that: Rational): Rational = {
+ Rational(this.numerator*that.denominator - that.numerator*this.denominator, this.denominator*that.denominator)
+ } ensuring(res => res.isRational)
+
+ def unary_- : Rational = {
+ Rational(-this.numerator, this.denominator)
+ } ensuring(res => res.isRational)
+
+ def *(that: Rational): Rational = {
+ Rational(this.numerator*that.numerator, this.denominator*that.denominator)
+ } ensuring(res => res.isRational)
+
+ def /(that: Rational): Rational = {
+ require(that.nonZero)
+ val newNumerator = this.numerator*that.denominator
+ val newDenominator = this.denominator*that.numerator
+ normalize(newNumerator, newDenominator)
+ } ensuring(res => res.isRational)
+
+ def reciprocal: Rational = {
+ require(this.nonZero)
+ normalize(this.denominator, this.numerator)
+ } ensuring(res => res.isRational)
+
+
+ def ~(that: Rational): Boolean = {
+ this.numerator*that.denominator == that.numerator*this.denominator
+ }
+
+ def <(that: Rational): Boolean = {
+ this.numerator*that.denominator < that.numerator*this.denominator
+ }
+
+ def <=(that: Rational): Boolean = {
+ this.numerator*that.denominator <= that.numerator*this.denominator
+ }
+
+ def >(that: Rational): Boolean = {
+ this.numerator*that.denominator > that.numerator*this.denominator
+ }
+
+ def >=(that: Rational): Boolean = {
+ this.numerator*that.denominator >= that.numerator*this.denominator
+ }
+
+ def nonZero: Boolean = {
+ numerator != 0
+ }
+
+ private def isRational: Boolean = denominator > 0
+
+ private def normalize(num: BigInt, den: BigInt): Rational = {
+ require(den != 0)
+ if(den < 0)
+ Rational(-num, -den)
+ else
+ Rational(num, den)
+ }
+}
+
+@library
+object Rational {
+
+ implicit def bigIntToRat(n: BigInt): Rational = Rational(n, 1)
+
+ def apply(n: BigInt): Rational = Rational(n, 1)
+
+}
diff --git a/libtest/src/main/scala/leon/lang/Real.scala b/libtest/src/main/scala/leon/lang/Real.scala
new file mode 100644
index 0000000000000000000000000000000000000000..9d600b3b6c584355dacfc10ed6d4d6b0c58fd631
--- /dev/null
+++ b/libtest/src/main/scala/leon/lang/Real.scala
@@ -0,0 +1,25 @@
+package leon.lang
+import leon.annotation._
+
+@ignore
+class Real {
+
+ def +(a: Real): Real = ???
+ def -(a: Real): Real = ???
+ def *(a: Real): Real = ???
+ def /(a: Real): Real = ???
+
+ def unary_- : Real = ???
+
+ def > (a: Real): Boolean = ???
+ def >=(a: Real): Boolean = ???
+ def < (a: Real): Boolean = ???
+ def <=(a: Real): Boolean = ???
+
+}
+
+@ignore
+object Real {
+ def apply(n: BigInt, d: BigInt): Real = ???
+ def apply(n: BigInt): Real = ???
+}
diff --git a/libtest/src/main/scala/leon/lang/Set.scala b/libtest/src/main/scala/leon/lang/Set.scala
new file mode 100644
index 0000000000000000000000000000000000000000..8f4595d33fada35acfa38435c3cd542116cf3cbd
--- /dev/null
+++ b/libtest/src/main/scala/leon/lang/Set.scala
@@ -0,0 +1,26 @@
+package leon.lang
+import leon.annotation._
+
+object Set {
+ @library
+ def empty[T] = Set[T]()
+
+ @ignore
+ def apply[T](elems: T*) = {
+ new Set[T](scala.collection.immutable.Set[T](elems : _*))
+ }
+}
+
+@ignore
+case class Set[T](val theSet: scala.collection.immutable.Set[T]) {
+ def +(a: T): Set[T] = new Set[T](theSet + a)
+ def ++(a: Set[T]): Set[T] = new Set[T](theSet ++ a.theSet)
+ def -(a: T): Set[T] = new Set[T](theSet - a)
+ def --(a: Set[T]): Set[T] = new Set[T](theSet -- a.theSet)
+ def size: BigInt = theSet.size
+ def contains(a: T): Boolean = theSet.contains(a)
+ def isEmpty: Boolean = theSet.isEmpty
+ def subsetOf(b: Set[T]): Boolean = theSet.subsetOf(b.theSet)
+ def &(a: Set[T]): Set[T] = new Set[T](theSet & a.theSet)
+}
+
diff --git a/libtest/src/main/scala/leon/lang/StrOps.scala b/libtest/src/main/scala/leon/lang/StrOps.scala
new file mode 100644
index 0000000000000000000000000000000000000000..723ce5be82d7a841c743640ba4f10284076c0dfe
--- /dev/null
+++ b/libtest/src/main/scala/leon/lang/StrOps.scala
@@ -0,0 +1,23 @@
+package leon.lang
+
+import leon.annotation._
+
+/**
+ * @author Mikael
+ */
+object StrOps {
+ @ignore
+ def concat(a: String, b: String): String = {
+ a + b
+ }
+ @ignore
+ def length(a: String): BigInt = {
+ BigInt(a.length)
+ }
+ @ignore
+ def substring(a: String, start: BigInt, end: BigInt): String = {
+ if(start > end || start >= length(a) || end <= 0) "" else a.substring(start.toInt, end.toInt)
+ }
+ @internal @library
+ def escape(s: String): String = s // Wrong definition, but it will eventually use StringEscapeUtils.escapeJava(s) at parsing and compile time.
+}
\ No newline at end of file
diff --git a/libtest/src/main/scala/leon/lang/package.scala b/libtest/src/main/scala/leon/lang/package.scala
new file mode 100644
index 0000000000000000000000000000000000000000..ab713a588e5451ba8ab61533d6037bd2bd572de8
--- /dev/null
+++ b/libtest/src/main/scala/leon/lang/package.scala
@@ -0,0 +1,85 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+
+import leon.annotation._
+import scala.language.implicitConversions
+
+package object lang {
+
+ implicit class BooleanDecorations(val underlying: Boolean) {
+ @inline
+ def holds : Boolean = {
+ underlying
+ } ensuring {
+ _ == true
+ }
+
+ @inline
+ def ==>(that: => Boolean): Boolean = {
+ if (underlying) that else true
+ }
+ }
+
+ @ignore def forall[A](p: A => Boolean): Boolean = sys.error("Can't execute quantified proposition")
+ @ignore def forall[A,B](p: (A,B) => Boolean): Boolean = sys.error("Can't execute quantified proposition")
+ @ignore def forall[A,B,C](p: (A,B,C) => Boolean): Boolean = sys.error("Can't execute quantified proposition")
+ @ignore def forall[A,B,C,D](p: (A,B,C,D) => Boolean): Boolean = sys.error("Can't execute quantified proposition")
+ @ignore def forall[A,B,C,D,E](p: (A,B,C,D,E) => Boolean): Boolean = sys.error("Can't execute quantified proposition")
+
+ @ignore
+ object InvariantFunction {
+ def invariant(x: Boolean): Unit = ()
+ }
+
+ @ignore
+ implicit def while2Invariant(u: Unit) = InvariantFunction
+
+ @ignore
+ def error[T](reason: java.lang.String): T = sys.error(reason)
+
+ @ignore
+ def old[T](value: T): T = value
+
+ @ignore
+ implicit class Passes[A,B](io : (A,B)) {
+ val (in, out) = io
+ def passes(tests : A => B ) : Boolean =
+ try { tests(in) == out } catch { case _ : MatchError => true }
+ }
+
+ @ignore
+ def byExample[A, B](in: A, out: B): Boolean = {
+ sys.error("Can't execute by example proposition")
+ }
+
+ implicit class SpecsDecorations[A](val underlying: A) {
+ @ignore
+ def computes(target: A) = {
+ underlying
+ } ensuring {
+ res => res == target
+ }
+
+ @ignore // Programming by example: ???[String] ask input
+ def ask[I](input : I) = {
+ underlying
+ } ensuring {
+ (res: A) => byExample(input, res)
+ }
+ }
+
+ @ignore
+ object BigInt {
+ def apply(b: Int): scala.math.BigInt = scala.math.BigInt(b)
+ def apply(b: String): scala.math.BigInt = scala.math.BigInt(b)
+
+ def unapply(b: scala.math.BigInt): scala.Option[Int] = {
+ if(b >= Integer.MIN_VALUE && b <= Integer.MAX_VALUE) {
+ scala.Some(b.intValue())
+ } else {
+ scala.None
+ }
+ }
+ }
+}
diff --git a/libtest/src/main/scala/leon/lang/synthesis/Oracle.scala b/libtest/src/main/scala/leon/lang/synthesis/Oracle.scala
new file mode 100644
index 0000000000000000000000000000000000000000..7af697638880232c9248cbe98e01e0327552bccb
--- /dev/null
+++ b/libtest/src/main/scala/leon/lang/synthesis/Oracle.scala
@@ -0,0 +1,33 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon.lang.synthesis
+
+import leon.annotation._
+import leon.lang._
+
+import scala.annotation._
+
+@implicitNotFound("No Oracle available for this source of non-determinism, please provide an implicit arg <: Oracle[T]")
+@ignore
+@library
+abstract class Oracle[T] {
+ def head: T = this match {
+ case Node(_, h, _) => h
+ case Leaf(h) => h
+ }
+
+ def left: Oracle[T] = this match {
+ case Node(l, _, _) => l
+ case Leaf(_) => this
+ }
+
+ def right: Oracle[T] = this match {
+ case Node(_, _, r) => r
+ case Leaf(_) => this
+ }
+}
+
+@ignore
+case class Node[T](l: Oracle[T], v: T, r: Oracle[T]) extends Oracle[T];
+@ignore
+case class Leaf[T](v: T) extends Oracle[T];
diff --git a/libtest/src/main/scala/leon/lang/synthesis/package.scala b/libtest/src/main/scala/leon/lang/synthesis/package.scala
new file mode 100644
index 0000000000000000000000000000000000000000..cb56992797715423aa1b0c45f94946778cb5780e
--- /dev/null
+++ b/libtest/src/main/scala/leon/lang/synthesis/package.scala
@@ -0,0 +1,41 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon.lang
+
+import leon.annotation._
+
+import scala.language.implicitConversions
+import scala.annotation.implicitNotFound
+
+package object synthesis {
+ @ignore
+ private def noImpl = throw new RuntimeException("Synthesis construct implementation not supported")
+
+ @ignore
+ def choose[A](predicate: A => Boolean): A = noImpl
+ @ignore
+ def choose[A, B](predicate: (A, B) => Boolean): (A, B) = noImpl
+ @ignore
+ def choose[A, B, C](predicate: (A, B, C) => Boolean): (A, B, C) = noImpl
+ @ignore
+ def choose[A, B, C, D](predicate: (A, B, C, D) => Boolean): (A, B, C, D) = noImpl
+ @ignore
+ def choose[A, B, C, D, E](predicate: (A, B, C, D, E) => Boolean): (A, B, C, D, E) = noImpl
+
+ @ignore
+ def ???[T]: T = noImpl
+
+ @ignore
+ def ?[T](e1: T): T = if(???[Boolean]) e1 else ???[T]
+
+ @ignore
+ def ?[T](e1: T, es: T*): T = noImpl
+
+ // Repair with Holes
+ @ignore
+ def ?: T = noImpl
+
+ @ignore
+ def withOracle[A, R](body: Oracle[A] => R): R = noImpl
+
+}
diff --git a/libtest/src/main/scala/leon/lang/xlang/package.scala b/libtest/src/main/scala/leon/lang/xlang/package.scala
new file mode 100644
index 0000000000000000000000000000000000000000..6f29c5d33e3fc8dff8a26d526cf7ef2c6f2f0837
--- /dev/null
+++ b/libtest/src/main/scala/leon/lang/xlang/package.scala
@@ -0,0 +1,13 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon.lang
+
+import leon.annotation._
+
+package object xlang {
+ @ignore
+ def waypoint[A](i: Int, expr: A): A = expr
+
+ @ignore
+ def epsilon[A](pred: (A) => Boolean): A = throw new RuntimeException("Implementation not supported")
+}
diff --git a/libtest/src/main/scala/leon/lazy/package.scala b/libtest/src/main/scala/leon/lazy/package.scala
new file mode 100644
index 0000000000000000000000000000000000000000..7c0f575828c3bd96cb32c069c43e1444373075a5
--- /dev/null
+++ b/libtest/src/main/scala/leon/lazy/package.scala
@@ -0,0 +1,90 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
+package leon
+
+import annotation._
+import lang._
+import scala.language.implicitConversions
+import scala.annotation.StaticAnnotation
+
+package object lazyeval {
+
+ @library
+ def $[T](f: => T) = Lazy(Unit => f)
+ //def apply[T](f: => T) = new $(Unit => f)
+
+ @library
+ def eager[T](x: => T) = Lazy(Unit => x)
+
+ /**
+ * implicit conversion from eager evaluation to lazy evaluation
+ */
+ @library
+ @inline
+ implicit def eagerToLazy[T](x: T) = eager(x)
+
+ /**
+ * For accessing in and out states.
+ * Should be used only in ensuring.
+ */
+ @library
+ @extern
+ def inState[T]: Set[Lazy[T]] = sys.error("inState method is not executable!")
+
+ @library
+ @extern
+ def outState[T]: Set[Lazy[T]] = sys.error("outState method is not executable")
+
+ /**
+ * Helper class for invoking with a given state instead of the implicit state
+ */
+ @library
+ case class WithState[T](v: T) {
+ @extern
+ def withState[U](u: Set[Lazy[U]]): T = sys.error("withState method is not executable!")
+
+ @extern
+ def withState[U, V](u: Set[Lazy[U]], v: Set[Lazy[V]]): T = sys.error("withState method is not executable!")
+
+ @extern
+ def withState[U, V, W](u: Set[Lazy[U]], v: Set[Lazy[V]], w: Set[Lazy[W]]): T = sys.error("withState method is not executable!")
+
+ @extern
+ def withState[U, V, W, X](u: Set[Lazy[U]], v: Set[Lazy[V]], w: Set[Lazy[W]], x: Set[Lazy[X]]): T = sys.error("withState method is not executable!")
+ // extend this to more arguments if needed
+ }
+
+ @library
+ @inline
+ implicit def toWithState[T](x: T) = new WithState(x)
+
+ /**
+ * annotations for monotonicity proofs.
+ * Note implemented as of now.
+ * Let foo be the method that has the annotation.
+ * The given name `methodname` should have the following form:
+ * m(arg1, ..., argn, substate-Set1,..., substate-Setn, superstate-Set1, ..., superstate-Setn)
+ */
+ @ignore
+ class monoproof(methodname: String) extends StaticAnnotation
+
+ @library
+ case class Lazy[T](f: Unit => T) {
+ @extern
+ lazy val value = {
+ val x = f(())
+ eval = true
+ x
+ }
+ def * = f(())
+
+ @ignore
+ var eval = false // is this thread safe ?
+
+ @extern
+ def isEvaluated = eval
+
+ @extern
+ def isSuspension[T](f: T): Boolean = sys.error("isSuspensionOf method is not executable")
+ }
+}
\ No newline at end of file
diff --git a/libtest/src/main/scala/leon/math/package.scala b/libtest/src/main/scala/leon/math/package.scala
new file mode 100644
index 0000000000000000000000000000000000000000..8eb5f347963f4599faeca8e1c58adda74b259aef
--- /dev/null
+++ b/libtest/src/main/scala/leon/math/package.scala
@@ -0,0 +1,18 @@
+package leon
+import leon.annotation._
+
+package object math {
+
+ @library
+ def min(i1: Int, i2: Int) = if (i1 <= i2) i1 else i2
+
+ @library
+ def max(i1: Int, i2: Int) = if (i1 >= i2) i1 else i2
+
+ @library
+ def min(i1: BigInt, i2: BigInt) = if (i1 <= i2) i1 else i2
+
+ @library
+ def max(i1: BigInt, i2: BigInt) = if (i1 >= i2) i1 else i2
+
+}
diff --git a/libtest/src/main/scala/leon/mem/package.scala b/libtest/src/main/scala/leon/mem/package.scala
new file mode 100644
index 0000000000000000000000000000000000000000..416b737acae9b34287dc0f54ee3e6202fe72721e
--- /dev/null
+++ b/libtest/src/main/scala/leon/mem/package.scala
@@ -0,0 +1,56 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
+package leon
+
+import annotation._
+import lang._
+import scala.language.implicitConversions
+import scala.annotation.StaticAnnotation
+
+package object mem {
+
+ @library
+ @inline
+ implicit def toMem[T](x: T) = new Mem(x)
+
+ /**
+ * accessing in and out states of mems
+ * Should be used only in ensuring.
+ */
+ @library
+ @extern
+ def inState[T]: Set[Mem[T]] = sys.error("inState method is not executable!")
+
+ @library
+ @extern
+ def outState[T]: Set[Mem[T]] = sys.error("outState method is not executable")
+
+ /**
+ * Helper class for invoking with a given state instead of the implicit state
+ */
+ @library
+ case class memWithState[T](v: T) {
+ @extern
+ def withState[U](u: Set[Mem[U]]): T = sys.error("withState method is not executable!")
+
+ @extern
+ def withState[U, V](u: Set[Mem[U]], v: Set[Mem[V]]): T = sys.error("withState method is not executable!")
+
+ @extern
+ def withState[U, V, W](u: Set[Mem[U]], v: Set[Mem[V]], w: Set[Mem[W]]): T = sys.error("withState method is not executable!")
+
+ @extern
+ def withState[U, V, W, X](u: Set[Mem[U]], v: Set[Mem[V]], w: Set[Mem[W]], x: Set[Mem[X]]): T = sys.error("withState method is not executable!")
+ // extend this to more arguments if needed
+ }
+
+ @library
+ @inline
+ implicit def toWithState[T](x: T) = new memWithState(x)
+
+ @library
+ case class Mem[T](v: T) {
+ @extern
+ def isCached: Boolean = sys.error("not implemented!")
+ }
+}
\ No newline at end of file
diff --git a/libtest/src/main/scala/leon/monads/state/State.scala b/libtest/src/main/scala/leon/monads/state/State.scala
new file mode 100644
index 0000000000000000000000000000000000000000..ad47c2464f54c9e40fc430528c561ad40032ac1f
--- /dev/null
+++ b/libtest/src/main/scala/leon/monads/state/State.scala
@@ -0,0 +1,215 @@
+package leon.monads.state
+
+import leon.collection._
+import leon.lang._
+import leon.annotation._
+import State._
+
+
+@library
+case class State[S, A](runState: S => (A, S)) {
+
+ /** Basic monadic methods */
+
+ // Monadic bind
+ @inline
+ def flatMap[B](f: A => State[S, B]): State[S, B] = {
+ State { s =>
+ val (a, newS) = runState(s)
+ f(a).runState(newS)
+ }
+ }
+
+ // All monads are also functors, and they define the map function
+ @inline
+ def map[B](f: A => B): State[S, B] = {
+ State { s =>
+ val (a, newS) = runState(s)
+ (f(a), newS)
+ }
+ }
+
+ @inline
+ def >>=[B](f: A => State[S, B]): State[S, B] = flatMap(f)
+
+ @inline
+ def >>[B](that: State[S, B]) = >>= ( _ => that )
+
+ @inline
+ // This is unfortunate, but implementing properly would just lead to an error
+ def withFilter(f: A => Boolean): State[S, A] = this
+
+ @inline
+ def eval(s: S) = runState(s)._1
+ @inline
+ def exec(s: S) = runState(s)._2
+
+ // eval with arguments flipped
+ @inline
+ def >:: (s: S) = eval(s)
+
+ def apply(s: S) = runState(s)
+
+}
+
+@library
+object State {
+
+ @inline
+ def get[A]: State[A, A] = State( a => (a, a) )
+
+ @inline
+ def gets[S, A](f: S => A): State[S, A] = for {
+ s <- get[S]
+ } yield f(s)
+
+ @inline
+ def put[S](s: S): State[S, Unit] = State { _ => ((), s) }
+
+ @inline
+ def modify[S](f: S => S): State[S, Unit] = for {
+ s <- get[S]
+ s2 <- put(f(s))
+ } yield s2
+
+ // Monadic unit
+ @inline
+ def unit[S, A](a: A): State[S, A] = State { s => (a, s) }
+
+ @inline
+ def state[S]: State[S, S] = State(s => (s, s))
+
+ @inline
+ // Left-to-right Kleisli composition of monads
+ def >=>[S, A, B, C](f: A => State[S, B], g: B => State[S, C], a: A): State[S, C] = {
+ for {
+ b <- f(a)
+ c <- g(b)
+ } yield c
+ }
+
+ /* Monadic-List functions */
+
+ def mapM[A, B, S](f: A => State[S, B], l: List[A]): State[S, List[B]] = {
+ l match {
+ case Nil() => unit(Nil[B]())
+ case Cons(x, xs) => for {
+ mx <- f(x)
+ mxs <- mapM(f,xs)
+ } yield mx :: mxs
+ }
+ }
+
+ def mapM_ [A, B, S] (f: A => State[S, B], l: List[A]): State[S, Unit] = {
+ l match {
+ case Nil() => unit(())
+ case Cons(x, xs) => for {
+ mx <- f(x)
+ mxs <- mapM_ (f, xs)
+ } yield ()
+ }
+ }
+
+ def sequence[S, A](l: List[State[S, A]]): State[S, List[A]] = {
+ l.foldRight[State[S, List[A]]](unit(Nil[A]())){
+ case (x, xs) => for {
+ v <- x
+ vs <- xs
+ } yield v :: vs
+ }
+ }
+
+ def filterM[S, A](f: A => State[S, Boolean], l: List[A]): State[S, List[A]] = {
+ l match {
+ case Nil() => unit(Nil[A]())
+ case Cons(x, xs) => for {
+ flg <- f(x)
+ rest <- filterM(f, xs)
+ } yield (if (flg) x :: rest else rest)
+ }
+ }
+
+ //(b -> a -> m b) -> b -> t a -> m b
+ def foldLeftM[S, A, B](f: (B, A) => State[S, B], z: B, l: List[A]): State[S, B] = {
+ l match {
+ case Nil() => unit(z)
+ case Cons(x, xs) =>
+ f(z, x) >>= ( z0 => foldLeftM(f,z0,xs) )
+ }
+ }
+
+ //(b -> a -> m b) -> b -> t a -> m ()
+ def foldLeftM_ [S, A](f: A => State[S, Unit], l: List[A]): State[S, Unit] = {
+ l match {
+ case Nil() => unit(())
+ case Cons(x, xs) =>
+ f(x) >> foldLeftM_ (f, xs)
+ }
+ }
+
+}
+
+@library
+object MonadStateLaws {
+ /* Monadic laws:
+ *
+ * return a >>= k = k a
+ * m >>= return = m
+ * m >>= (x -> k x >>= h) = (m >>= k) >>= h
+ *
+ * Note: We cannot compare State's directly because State contains an anonymous function.
+ * So we have to run them on an initial state.
+ */
+
+ def unitLeftId[A, B, S](a: A, k: A => State[S, B])(s: S): Boolean = {
+ (unit(a) >>= (k))(s) == k(a)(s)
+ }.holds
+
+ def unitRightId[S, A](m: State[S,A])(s:S): Boolean = {
+ (m >>= unit).runState(s) == m.runState(s)
+ }.holds
+
+ def assoc[S, A, B, C](m: State[S,A], k: A => State[S, B], h: B => State[S, C])(s: S) = {
+ (m >>= (x => k(x) >>= h)).runState(s) == (m >>= k >>= h).runState(s)
+ }.holds
+
+ /* This is the same as assoc, but proves in 42sec instead of 50ms!
+ def assoc2[S, A, B, C](m: State[S,A], k: A => State[S, B], h: B => State[S, C])(s: S) = {
+ val lhs = for {
+ x <- m
+ y <- for {
+ z <- k(x)
+ w <- h(z)
+ } yield w
+ } yield y
+
+ val rhs = for {
+ x <- m
+ y <- k(x)
+ z <- h(y)
+ } yield z
+
+ lhs.runState(s) == rhs.runState(s)
+ }.holds
+ */
+
+
+ /* The law connecting monad and functor instances:
+ *
+ * m >>= (return . f) = m map f
+ */
+
+ def mapToFlatMap[S, A, B](m: State[S, A], f: A => B)(s: S): Boolean = {
+ (m >>= (x => unit(f(x)))).runState(s) == (m map f).runState(s)
+ }.holds
+
+
+ /* Different theorems */
+
+ //@induct
+ //def mapMVsSequenceM[S, A, B](f: A => State[S, B], l: List[A])(s: S) = {
+ // mapM(f, l).runState(s) == sequence(l map f).runState(s)
+ //}.holds
+
+
+}
diff --git a/libtest/src/main/scala/leon/package.scala b/libtest/src/main/scala/leon/package.scala
new file mode 100644
index 0000000000000000000000000000000000000000..357010d11f8b1b4ae4fe0e9076a087029a0fd089
--- /dev/null
+++ b/libtest/src/main/scala/leon/package.scala
@@ -0,0 +1,23 @@
+import leon.annotation._
+import scala.annotation.elidable
+import scala.annotation.elidable._
+
+/**
+ * A collection of methods that can be used to collect run-time statistics about Leon programs.
+ * This is mostly used to test the resources properties of Leon programs
+ */
+package object leon {
+
+ /**
+ * Stubs of ensuring and require that do not check contracts.
+ * Enable this if you want running time statistics without executing contracts.
+ */
+ @ignore
+ implicit class Ensuring[A](private val self: A) extends AnyVal {
+ @inline
+ def ensuring(cond: A => Boolean): A = { self }
+ }
+
+ @ignore
+ def require(arg: => Boolean) {}
+}
diff --git a/libtest/src/main/scala/leon/par/package.scala b/libtest/src/main/scala/leon/par/package.scala
new file mode 100644
index 0000000000000000000000000000000000000000..5842210fce915df2c02a0f69b6000703c8865af9
--- /dev/null
+++ b/libtest/src/main/scala/leon/par/package.scala
@@ -0,0 +1,24 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis.choose
+
+package object par {
+
+ @library
+ @inline
+ def parallel[A,B](x: => A, y: => B) : (A,B) = {
+ (x,y)
+ }
+
+ @library
+ case class Task[A](c: A) {
+ def join: A = c
+ }
+
+ @library
+ def task[A](c: A) = Task(c)
+}
diff --git a/libtest/src/main/scala/leon/proof/Internal.scala b/libtest/src/main/scala/leon/proof/Internal.scala
new file mode 100644
index 0000000000000000000000000000000000000000..0962c371c670d2b08db797a9f24542195c78bac8
--- /dev/null
+++ b/libtest/src/main/scala/leon/proof/Internal.scala
@@ -0,0 +1,63 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+package leon.proof
+
+import leon.lang._
+import leon.annotation._
+
+/** Internal helper classes and methods for the 'proof' package. */
+object Internal {
+
+ /*** Helper classes for relational reasoning ***/
+ @library
+ case class WithRel[A, B](x: A, r: (A, B) => Boolean, prop: Boolean) {
+
+ /** Continue with the next relation. */
+ def ^^(y: B): RelReasoning[B] = {
+ require(prop ==> r(x, y))
+ RelReasoning(y, prop && r(x, y))
+ }
+
+ /** Add a proof. */
+ def ^^|(proof: Boolean): WithProof[A, B] = {
+ require(proof)
+ WithProof(x, r, proof, prop)
+ }
+
+ /** Short-hand for equational reasoning. */
+ def ==|(proof: Boolean): WithProof[A, A] = {
+ require(proof)
+ WithProof(x, _ == _, proof, prop)
+ }
+
+ def qed: Boolean = prop
+ }
+
+ @library
+ case class WithProof[A, B](
+ x: A, r: (A, B) => Boolean, proof: Boolean, prop: Boolean) {
+
+ /** Close a proof. */
+ def |[C](that: WithProof[B, C]): WithProof[B, C] = {
+ require(this.prop && this.proof ==> this.r(this.x, that.x))
+ WithProof(
+ that.x, that.r, that.proof,
+ this.prop && this.proof && this.r(this.x, that.x))
+ }
+
+ /** Close a proof. */
+ def |[C](that: WithRel[B, C]): WithRel[B, C] = {
+ require(this.prop && this.proof ==> this.r(this.x, that.x))
+ WithRel(
+ that.x, that.r,
+ this.prop && this.proof && this.r(this.x, that.x))
+ }
+
+ /** Close a proof. */
+ def |(that: RelReasoning[B]): RelReasoning[B] = {
+ require(this.prop && this.proof ==> this.r(this.x, that.x))
+ RelReasoning(
+ that.x,
+ this.prop && this.proof && this.r(this.x, that.x))
+ }
+ }
+}
diff --git a/libtest/src/main/scala/leon/proof/package.scala b/libtest/src/main/scala/leon/proof/package.scala
new file mode 100644
index 0000000000000000000000000000000000000000..3f097864964a8d2d724a8ec1256dd803c5c048c5
--- /dev/null
+++ b/libtest/src/main/scala/leon/proof/package.scala
@@ -0,0 +1,66 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+package leon
+
+import leon.annotation._
+import leon.lang._
+import scala.language.implicitConversions
+
+import leon.proof.Internal._
+
+package object proof {
+
+ @library
+ case class ProofOps(prop: Boolean) {
+ def because(proof: Boolean): Boolean = proof && prop
+ def neverHolds: Boolean = {
+ require(!prop)
+ !prop
+ }
+ }
+
+ @library
+ implicit def boolean2ProofOps(prop: Boolean): ProofOps = ProofOps(prop)
+
+ @library
+ def trivial: Boolean = true
+
+ @library
+ def by(proof: Boolean)(prop: Boolean): Boolean =
+ proof && prop
+
+ @library
+ def check(prop: Boolean): Boolean = {
+ require(prop)
+ prop
+ }
+
+ /**
+ * Relational reasoning.
+ *
+ * {
+ * ((y :: ys) :+ x).last ^^ _ == _ ^^| trivial |
+ * (y :: (ys :+ x)).last ==| trivial |
+ * (ys :+ x).last ==| snocLast(ys, x) |
+ * x
+ * }.qed
+ */
+ @library
+ case class RelReasoning[A](x: A, prop: Boolean) {
+
+ def ^^[B](r: (A, B) => Boolean): WithRel[A, B] = WithRel(x, r, prop)
+
+ /** Short-hand for equational reasoning. */
+ def ==|(proof: Boolean): WithProof[A, A] = {
+ require(proof)
+ WithProof(x, _ == _, proof, prop)
+ }
+
+ def qed: Boolean = prop
+ }
+
+ @library
+ implicit def any2RelReasoning[A](x: A): RelReasoning[A] =
+ RelReasoning(x, true)
+
+}
+
diff --git a/libtest/src/main/scala/leon/stats/package.scala b/libtest/src/main/scala/leon/stats/package.scala
new file mode 100644
index 0000000000000000000000000000000000000000..17d6286b62c3e4de4be5d4c430ea74e26a3abef0
--- /dev/null
+++ b/libtest/src/main/scala/leon/stats/package.scala
@@ -0,0 +1,28 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+
+import leon.annotation._
+import java.lang.management._
+import scala.collection.JavaConversions._
+
+/**
+ * A collection of methods that can be used to collect run-time statistics about Leon programs.
+ * This is mostly used to test the resources properties of Leon programs
+ */
+package object stats {
+ @ignore
+ def timed[T](code: => T)(cont: Long => Unit): T = {
+ var t1 = System.currentTimeMillis()
+ val r = code
+ cont((System.currentTimeMillis() - t1))
+ r
+ }
+
+ @ignore
+ def withTime[T](code: => T): (T, Long) = {
+ var t1 = System.currentTimeMillis()
+ val r = code
+ (r, (System.currentTimeMillis() - t1))
+ }
+}
diff --git a/run-benchs.sh b/run-benchs.sh
deleted file mode 100755
index f269ac5649d2d70489ce664f80808d43a96a4c55..0000000000000000000000000000000000000000
--- a/run-benchs.sh
+++ /dev/null
@@ -1,12 +0,0 @@
-./leon --lazy ./testcases/lazy-datastructures/RealTimeQueue.scala | tee RTQ.out
-./leon --lazy ./testcases/lazy-datastructures/BottomUpMegeSort.scala | tee MsortBU.out
-./leon --lazy ./testcases/lazy-datastructures/SortingnConcat.scala | tee Sort.out
-./leon --lazy ./testcases/lazy-datastructures/Esop15Benchmarks.scala | tee Esop.out
-./leon --lazy ./testcases/lazy-datastructures/Deque.scala --unfoldFactor=2 | tee RDQ.out
-./leon --lazy ./testcases/lazy-datastructures/LazyNumericalRep.scala --unfoldFactor=3 | tee Num.out
-./leon --lazy ./testcases/lazy-datastructures/conc/Conqueue.scala --unfoldFactor=3 | tee Conqueue.out
-./leon --lazy ./testcases/lazy-datastructures/memoization/Knapsack.scala | tee Knapsack.out
-./leon --lazy ./testcases/lazy-datastructures/memoization/WeightedScheduling.scala | tee Sched.out
-./leon --lazy ./testcases/lazy-datastructures/memoization/HammingMemoized.scala | tee Hamming.out
-./leon --lazy ./testcases/lazy-datastructures/memoization/PackratParsing.scala | tee Packrat.out
-
diff --git a/src/main/scala/leon/invariant/engine/CompositionalTimeBoundSolver.scala b/src/main/scala/leon/invariant/engine/CompositionalTimeBoundSolver.scala
index 1992607fa3dfed9e64ae4e920fd683e973f62f17..7713195169d4732fba1e2961b548a908516d16ec 100644
--- a/src/main/scala/leon/invariant/engine/CompositionalTimeBoundSolver.scala
+++ b/src/main/scala/leon/invariant/engine/CompositionalTimeBoundSolver.scala
@@ -45,7 +45,7 @@ class CompositionalTimeBoundSolver(ctx: InferenceContext, prog: Program, rootFd:
val origProg = prog
// add only rec templates for all functions
- val funToRecTmpl = origProg.definedFunctions.collect {
+ val funToRecTmpl = userLevelFunctions(origProg).collect {
case fd if fd.hasTemplate && fd == rootFd =>
fd -> recTmpl
case fd if fd.hasTemplate =>
@@ -54,7 +54,7 @@ class CompositionalTimeBoundSolver(ctx: InferenceContext, prog: Program, rootFd:
val recProg = assignTemplateAndCojoinPost(funToRecTmpl, origProg)
// add only tpr template for all functions
- val funToNonRecTmpl = origProg.definedFunctions.collect {
+ val funToNonRecTmpl = userLevelFunctions(origProg).collect {
case fd if fd.hasTemplate && fd == rootFd =>
fd -> tprTmpl
case fd if fd.hasTemplate =>
@@ -73,7 +73,7 @@ class CompositionalTimeBoundSolver(ctx: InferenceContext, prog: Program, rootFd:
case (Some(InferResult(true, Some(recModel), _)),
Some(InferResult(true, Some(tprModel), _))) =>
// create a new program by omitting the templates of the root function
- val funToTmpl = origProg.definedFunctions.collect {
+ val funToTmpl = userLevelFunctions(origProg).collect {
case fd if fd.hasTemplate && fd != rootFd =>
(fd -> fd.getTemplate)
}.toMap
@@ -83,14 +83,14 @@ class CompositionalTimeBoundSolver(ctx: InferenceContext, prog: Program, rootFd:
// construct the instantiated tpr bound and check if it monotonically decreases
val Operator(Seq(_, tprFun), _) = tprTmpl
- val tprFunInst = (new RealToInt()).mapRealToInt(
+ val tprFunInst = (new RealToInt()).mapExpr(
replace(tprModel.map { case (k, v) => (k.toVariable -> v) }.toMap, tprFun))
// TODO: this would fail on non-integers, handle these by approximating to the next bigger integer
// Upper bound on time time <= recFun * tprFun + tprFun
val (_, multFun) = MultFuncs.getMultFuncs(if (ctx.usereals) RealType else IntegerType)
val Operator(Seq(_, recFun), _) = recTmpl
- val recFunInst = (new RealToInt()).mapRealToInt(
+ val recFunInst = (new RealToInt()).mapExpr(
replace(recModel.map { case (k, v) => (k.toVariable -> v) }.toMap, recFun))
val timeUpperBound = ExpressionTransformer.normalizeMultiplication(
@@ -141,21 +141,6 @@ class CompositionalTimeBoundSolver(ctx: InferenceContext, prog: Program, rootFd:
}
}
- /*def combineMapsUsingConjunction(maps: List[Map[FunDef, Expr]], prog: Program) = {
- val combMap = new OrderedMultiMap[FunDef, Expr]
- maps.foreach {
- _.foreach {
- case (k, v) =>
- val origFun = functionByName(k.id.name, prog).get
- combMap.addBinding(origFun, v)
- }
- }
- combMap.foldLeft(Map[FunDef, Expr]()) {
- case (acc, (k, vs)) if vs.size == 1 => acc + (k -> vs(0))
- case (acc, (k, vs)) => acc + (k -> And(vs.toSeq))
- }
- }*/
-
def extractSeparateTemplates(funDef: FunDef): (Option[Expr], Option[Expr], Option[Expr], Seq[Expr]) = {
if (!funDef.hasTemplate) (None, None, None, Seq[Expr]())
else {
diff --git a/src/main/scala/leon/invariant/engine/InferenceContext.scala b/src/main/scala/leon/invariant/engine/InferenceContext.scala
index 48a45b048a33691f368242b63b45ae5bc062881c..c8020acb5f9ff6e3582a258fe0c8806745a533a5 100644
--- a/src/main/scala/leon/invariant/engine/InferenceContext.scala
+++ b/src/main/scala/leon/invariant/engine/InferenceContext.scala
@@ -45,9 +45,9 @@ class InferenceContext(val initProgram: Program, val leonContext: LeonContext) {
val statsSuffix = leonContext.findOption(optStatsSuffix).getOrElse("-stats" + FileCountGUID.getID)
val instrumentedProg = InstrumentationPhase(leonContext, initProgram)
- // convets qmarks to templates
+ // converts qmarks to templates
val qMarksRemovedProg = {
- val funToTmpl = instrumentedProg.definedFunctions.collect {
+ val funToTmpl = userLevelFunctions(instrumentedProg).collect {
case fd if fd.hasTemplate =>
fd -> fd.getTemplate
}.toMap
@@ -58,9 +58,7 @@ class InferenceContext(val initProgram: Program, val leonContext: LeonContext) {
val inferProgram = {
// convert nonlinearity to recursive functions
- nlelim(if (usereals)
- (new IntToRealProgram())(qMarksRemovedProg)
- else qMarksRemovedProg)
+ nlelim(if (usereals) (new IntToRealProgram())(qMarksRemovedProg) else qMarksRemovedProg)
}
// other utilities
diff --git a/src/main/scala/leon/invariant/engine/InferenceEngine.scala b/src/main/scala/leon/invariant/engine/InferenceEngine.scala
index 3e7f2fa3fe143c18ddbf4d4cc43294e9f824caa1..17c246b47c9cbca0dc70f2c8832ae9d8172d6180 100644
--- a/src/main/scala/leon/invariant/engine/InferenceEngine.scala
+++ b/src/main/scala/leon/invariant/engine/InferenceEngine.scala
@@ -140,9 +140,9 @@ class InferenceEngine(ctx: InferenceContext) extends Interruptible {
// not usef for now
/*val tempFactory = new TemplateFactory(Some(new TemplateEnumerator(ctx, startProg)),
startProg, ctx.reporter)*/
- startProg.definedFunctions.map(fd => fd -> getOrCreateTemplateForFun(fd)).toMap
+ userLevelFunctions(startProg).map(fd => fd -> getOrCreateTemplateForFun(fd)).toMap
} else
- startProg.definedFunctions.collect { case fd if fd.hasTemplate => fd -> fd.getTemplate }.toMap
+ userLevelFunctions(startProg).collect { case fd if fd.hasTemplate => fd -> fd.getTemplate }.toMap
val progWithTemplates = assignTemplateAndCojoinPost(funToTmpl, startProg)
var analyzedSet = Map[FunDef, InferenceCondition]()
@@ -191,7 +191,7 @@ class InferenceEngine(ctx: InferenceContext) extends Interruptible {
// now the templates of these functions will be replaced by inferred invariants
val invs = TemplateInstantiator.getAllInvariants(model.get, funsWithTemplates)
// collect templates of remaining functions
- val funToTmpl = prog.definedFunctions.collect {
+ val funToTmpl = userLevelFunctions(prog).collect {
case fd if !invs.contains(fd) && fd.hasTemplate =>
fd -> fd.getTemplate
}.toMap
diff --git a/src/main/scala/leon/invariant/factories/TemplateFactory.scala b/src/main/scala/leon/invariant/factories/TemplateFactory.scala
index ea0f0c63368aaaac74470811265b9f99d46ea883..110ac75cb47dd73d2f8b871faaa18105b5d1a825 100644
--- a/src/main/scala/leon/invariant/factories/TemplateFactory.scala
+++ b/src/main/scala/leon/invariant/factories/TemplateFactory.scala
@@ -30,7 +30,7 @@ object TemplateIdFactory {
}
def copyIdentifier(id: Identifier) : Identifier = {
- val freshid = FreshIdentifier(id.name, RealType, false)
+ val freshid = FreshIdentifier(id.name, id.getType, false)
ids += freshid
freshid
}
diff --git a/src/main/scala/leon/invariant/structure/LinearConstraintUtil.scala b/src/main/scala/leon/invariant/structure/LinearConstraintUtil.scala
index aee689be4bd1a1f89760272220e71132cbba8549..0f2c84350f95c9f5f3383a6bf55af3f5cfdf9500 100644
--- a/src/main/scala/leon/invariant/structure/LinearConstraintUtil.scala
+++ b/src/main/scala/leon/invariant/structure/LinearConstraintUtil.scala
@@ -204,7 +204,7 @@ object LinearConstraintUtil {
|| e.isInstanceOf[GreaterEquals])) => {
//check if the expression has real valued sub-expressions
- val isReal = hasReals(e1) || hasReals(e2)
+ val isReal = hasRealsOrTemplates(e1) || hasRealsOrTemplates(e2)
val (newe, newop) = e match {
case t: Equals => (Minus(e1, e2), Equals)
case t: LessEquals => (Minus(e1, e2), LessEquals)
diff --git a/src/main/scala/leon/invariant/templateSolvers/CegisSolver.scala b/src/main/scala/leon/invariant/templateSolvers/CegisSolver.scala
index a3eca287b0d221af93120b1578020e8baa7a5fc9..0465199421bf61a5721fad33e2a94795f6ef8406 100644
--- a/src/main/scala/leon/invariant/templateSolvers/CegisSolver.scala
+++ b/src/main/scala/leon/invariant/templateSolvers/CegisSolver.scala
@@ -120,8 +120,6 @@ class CegisCore(ctx: InferenceContext,
val spuriousTempIds = variablesOf(instFormula).intersect(TemplateIdFactory.getTemplateIds)
if (spuriousTempIds.nonEmpty)
throw new IllegalStateException("Found a template variable in instFormula: " + spuriousTempIds)
- if (hasReals(instFormula))
- throw new IllegalStateException("Reals in instFormula: " + instFormula)
//println("solving instantiated vcs...")
val solver1 = new ExtendedUFSolver(context, program)
@@ -158,16 +156,11 @@ class CegisCore(ctx: InferenceContext,
val solver2 = SimpleSolverAPI(new TimeoutSolverFactory(SolverFactory(() => new ExtendedUFSolver(context, program) with TimeoutSolver),
timeoutMillis - elapsedTime))
val (res1, newModel) = if (solveAsInt) {
- //convert templates to integers and solve. Finally, re-convert integer models for templates to real models
- val rti = new RealToInt()
- val intctr = rti.mapRealToInt(And(newctr, initRealCtr))
- val intObjective = rti.mapRealToInt(tempVarSum)
- val (res1, intModel) =
- if (minimizeSum)
- minimizeIntegers(intctr, intObjective)
- else
- solver2.solveSAT(intctr)
- (res1, rti.unmapModel(intModel))
+ val intctr = And(newctr, initRealCtr)
+ if (minimizeSum)
+ minimizeIntegers(intctr, tempVarSum)
+ else
+ solver2.solveSAT(intctr)
} else {
if (minimizeSum) {
minimizeReals(And(newctr, initRealCtr), tempVarSum)
diff --git a/src/main/scala/leon/invariant/templateSolvers/DisjunctChooser.scala b/src/main/scala/leon/invariant/templateSolvers/DisjunctChooser.scala
index b3a935124bbe609bc423e49404336fd7cf20ef7c..27d83ef562a671045d8c7091caa2437af8af0d3c 100644
--- a/src/main/scala/leon/invariant/templateSolvers/DisjunctChooser.scala
+++ b/src/main/scala/leon/invariant/templateSolvers/DisjunctChooser.scala
@@ -181,7 +181,7 @@ class DisjunctChooser(ctx: InferenceContext, program: Program, ctrTracker: Const
if (debugElimination && verifyInvariant) {
println("checking invariant for disjunct before elimination...")
checkInvariant(createAnd((lnctrs ++ temps).map(_.template)), leonctx, program)
- }
+ }
// for debugging
val debugger =
if (debugElimination && verifyInvariant) {
diff --git a/src/main/scala/leon/invariant/templateSolvers/ExistentialQuantificationSolver.scala b/src/main/scala/leon/invariant/templateSolvers/ExistentialQuantificationSolver.scala
index 5af100ed7037832291416229fc690b215a6acca4..a2ad660104332fdce5c436fae93dbbfc692f9724 100644
--- a/src/main/scala/leon/invariant/templateSolvers/ExistentialQuantificationSolver.scala
+++ b/src/main/scala/leon/invariant/templateSolvers/ExistentialQuantificationSolver.scala
@@ -33,7 +33,7 @@ import SolverUtil._
/**
* This class uses Farkas' lemma to try and falsify numerical disjuncts with templates provided one by one
*/
-class ExistentialQuantificationSolver(ctx: InferenceContext, program: Program,
+class ExistentialQuantificationSolver(ctx: InferenceContext, program: Program,
ctrTracker: ConstraintTracker, defaultEval: DefaultEvaluator) {
import NLTemplateSolver._
val reporter = ctx.reporter
@@ -41,9 +41,9 @@ class ExistentialQuantificationSolver(ctx: InferenceContext, program: Program,
var currentCtr: Expr = tru
private val farkasSolver = new FarkasLemmaSolver(ctx, program)
val disjunctChooser = new DisjunctChooser(ctx, program, ctrTracker, defaultEval)
-
- def getSolvedCtrs = currentCtr
-
+
+ def getSolvedCtrs = currentCtr
+
def generateCtrsForUNSAT(fd: FunDef, univModel: LazyModel, tempModel: Model) = {
// chooose a sat numerical disjunct from the model
val (lnctrs, temps, calls) =
@@ -53,11 +53,11 @@ class ExistentialQuantificationSolver(ctx: InferenceContext, program: Program,
updateCounterTime(chTime, "Disj-choosing-time", "disjuncts")
updateCumTime(chTime, "Total-Choose-Time")
}
- val disjunct = (lnctrs ++ temps)
+ val disjunct = (lnctrs ++ temps)
if (temps.isEmpty) {
//here ants ^ conseq is sat (otherwise we wouldn't reach here) and there is no way to falsify this path
(fls, disjunct, calls)
- } else
+ } else
(farkasSolver.constraintsForUnsat(lnctrs, temps), disjunct, calls)
}
@@ -68,7 +68,6 @@ class ExistentialQuantificationSolver(ctx: InferenceContext, program: Program,
val newPart = createAnd(newctrs)
val newSize = atomNum(newPart)
val currSize = atomNum(currentCtr)
-
Stats.updateCounterStats((newSize + currSize), "NLsize", "disjuncts")
if (verbose) reporter.info("# of atomic predicates: " + newSize + " + " + currSize)
@@ -86,7 +85,7 @@ class ExistentialQuantificationSolver(ctx: InferenceContext, program: Program,
(Some(false), Model.empty)
case Some(true) =>
currentCtr = combCtr
- //new model may not have mappings for all the template variables, hence, use the mappings from earlier models
+ //new model may not have mappings for all the template variables, hence, use the mappings from earlier models
(Some(true), completeWithRefModel(newModel, oldModel))
}
}
diff --git a/src/main/scala/leon/invariant/templateSolvers/FarkasLemmaSolver.scala b/src/main/scala/leon/invariant/templateSolvers/FarkasLemmaSolver.scala
index 62eabca927059aa61c54a341d5339385a5c26e42..96d57a83403a9f4b43a21de0173a4bd25adf1aeb 100644
--- a/src/main/scala/leon/invariant/templateSolvers/FarkasLemmaSolver.scala
+++ b/src/main/scala/leon/invariant/templateSolvers/FarkasLemmaSolver.scala
@@ -180,13 +180,11 @@ class FarkasLemmaSolver(ctx: InferenceContext, program: Program) {
//the final constraint is a conjunction of lambda constraints and disjunction of enabled and disabled parts
if (disableAnts) And(createAnd(lambdaCtrs), disabledPart)
else {
- //And(And(lambdaCtrs), enabledPart)
And(createAnd(lambdaCtrs), Or(enabledPart, disabledPart))
}
}
val ctrs = if (disableAnts) {
- //here conseqs are empty
createCtrs(None)
} else {
val Seq(head, tail @ _*) = conseqs
@@ -316,10 +314,8 @@ class FarkasLemmaSolver(ctx: InferenceContext, program: Program) {
}
val fullmodel = model ++ newassignments
if (this.verifyModel) {
- //println("Fullmodel: "+fullmodel)
- assert(evaluateRealFormula(replace(
- fullmodel.map { case (k, v) => (k.toVariable, v) }.toMap,
- nlctrs)))
+ val formula = replace(fullmodel.map { case (k, v) => (k.toVariable, v)}.toMap, nlctrs)
+ assert(evaluateRealFormula(formula))
}
(res, fullmodel)
case _ =>
diff --git a/src/main/scala/leon/invariant/templateSolvers/UniversalQuantificationSolver.scala b/src/main/scala/leon/invariant/templateSolvers/UniversalQuantificationSolver.scala
index bb39630784f3af54776b9f884acf1028c17cd139..b22f402ae5180edcb7efb5ec7e9997e9c1eaf174 100644
--- a/src/main/scala/leon/invariant/templateSolvers/UniversalQuantificationSolver.scala
+++ b/src/main/scala/leon/invariant/templateSolvers/UniversalQuantificationSolver.scala
@@ -2,6 +2,7 @@ package leon
package invariant.templateSolvers
import z3.scala._
+import purescala._
import purescala.Common._
import purescala.Definitions._
import purescala.Expressions._
@@ -245,8 +246,9 @@ class UniversalQuantificationSolver(ctx: InferenceContext, program: Program,
Stats.updateCounter(1, "disjuncts")
if (verbose) {
reporter.info("Candidate invariants")
- TemplateInstantiator.getAllInvariants(tempModel, ctrTracker.getFuncs).foreach(
- entry => reporter.info(entry._1.id + "-->" + entry._2))
+ TemplateInstantiator.getAllInvariants(tempModel, ctrTracker.getFuncs).foreach{
+ case(f, inv) => reporter.info(f.id + "-->" + PrettyPrinter(inv))
+ }
}
val modRefiner = new ModelRefiner(tempModel)
sat = modRefiner.nextCandidate match {
diff --git a/src/main/scala/leon/invariant/util/ExpressionTransformer.scala b/src/main/scala/leon/invariant/util/ExpressionTransformer.scala
index 5de31ddac39d0529ea1e715a747581df831ae198..716b977bf9efe379d451a4421ef6781ba3faccae 100644
--- a/src/main/scala/leon/invariant/util/ExpressionTransformer.scala
+++ b/src/main/scala/leon/invariant/util/ExpressionTransformer.scala
@@ -141,38 +141,6 @@ object ExpressionTransformer {
val (resvalue, valuecjs) = transform(value, true)
(resbody, (valuecjs + Equals(binder.toVariable, resvalue)) ++ bodycjs)
- //the value is a tuple in the following case
- /*case LetTuple(binders, value, body) =>
- //TODO: do we have to consider reuse of let variables ?
- val (resbody, bodycjs) = transform(body, true)
- val (resvalue, valuecjs) = transform(value, true)
- //here we optimize the case where resvalue itself has tuples
- val newConjuncts = resvalue match {
- case Tuple(args) => {
- binders.zip(args).map((elem) => {
- val (bind, arg) = elem
- Equals(bind.toVariable, arg)
- })
- }
- case _ => {
- //may it is better to assign resvalue to a temporary variable (if it is not already a variable)
- val (resvalue2, cjs) = resvalue match {
- case t: Terminal => (t, Seq())
- case _ => {
- val freshres = createTemp("tres", resvalue.getType, langContext).toVariable
- (freshres, Seq(Equals(freshres, resvalue)))
- }
- }
- var i = 0
- val cjs2 = binders.map((bind) => {
- i += 1
- Equals(bind.toVariable, TupleSelect(resvalue2, i))
- })
- (cjs ++ cjs2)
- }
- }
- (resbody, (valuecjs ++ newConjuncts) ++ bodycjs)*/
-
case _ => conjoinWithinClause(e, transform, insideFunction)
}
}
diff --git a/src/main/scala/leon/invariant/util/RealIntMap.scala b/src/main/scala/leon/invariant/util/RealIntMap.scala
new file mode 100644
index 0000000000000000000000000000000000000000..12ba7d97ceffc033b73e42a33ed8b49c65c30fff
--- /dev/null
+++ b/src/main/scala/leon/invariant/util/RealIntMap.scala
@@ -0,0 +1,111 @@
+package leon
+package invariant.util
+
+import purescala.Common._
+import purescala.Expressions._
+import purescala.ExprOps._
+import purescala.Types._
+import invariant.factories._
+import solvers._
+import TemplateIdFactory._
+
+/**
+ * An abstract class for mapping integer typed variables to reals and vice-versa.
+ * Note: this preserves the template identifier property
+ */
+abstract class IntRealMap {
+ var oldToNew = Map[Identifier, Identifier]()
+ var newToOld = Map[Identifier, Identifier]()
+
+ def mapLiteral(l: Literal[_]): Literal[_]
+ def unmapLiteral(l: Literal[_]): Literal[_]
+ def mapIdentifier(v: Identifier): Identifier
+
+ def mapExpr(inexpr: Expr): Expr = {
+ val transformer = (e: Expr) => e match {
+ case l : Literal[_] => mapLiteral(l)
+ case v@Variable(id) =>
+ Variable(oldToNew.getOrElse(id, {
+ val mid = mapIdentifier(id)
+ if (mid != id) {
+ oldToNew += (id -> mid)
+ newToOld += (mid -> id)
+ }
+ mid
+ }))
+ case _ => e
+ }
+ simplePostTransform(transformer)(inexpr)
+ }
+
+ def unmapModel(model: Model): Model = {
+ new Model(model.map {
+ case (key, value) if (newToOld.contains(key)) =>
+ (newToOld(key),
+ value match {
+ case l: Literal[_] => unmapLiteral(l)
+ case e => e
+ })
+ case other => other
+ }.toMap)
+ }
+
+ def mapModel(model: Model): Model = {
+ new Model(model.map {
+ case (k, v) if (oldToNew.contains(k)) =>
+ (oldToNew(k), v match {
+ case l: Literal[_] => mapLiteral(l)
+ case e => e
+ })
+ case other => other
+ }.toMap)
+ }
+}
+
+/**
+ * maps all real valued variables and literals to new integer variables/literals and
+ * performs the reverse mapping
+ */
+class RealToInt extends IntRealMap {
+
+ val bone = BigInt(1)
+ def mapLiteral(l: Literal[_]): Literal[_] = l match {
+ case FractionalLiteral(num, `bone`) => InfiniteIntegerLiteral(num)
+ case FractionalLiteral(_, _) => throw new IllegalStateException("Real literal with non-unit denominator")
+ case other => other
+ }
+
+ def unmapLiteral(l: Literal[_]): Literal[_] = l match {
+ case InfiniteIntegerLiteral(v) => FractionalLiteral(v.toInt, 1)
+ case other => other
+ }
+
+ def mapIdentifier(v: Identifier): Identifier =
+ if (v.getType == RealType) {
+ if (IsTemplateIdentifier(v)) freshIdentifier(v.name)
+ else FreshIdentifier(v.name, IntegerType, true)
+ } else v
+}
+
+/**
+ * Maps integer literal and identifiers to real literal and identifiers
+ */
+/*class IntToReal extends IntRealMap {
+
+ def mapLiteral(l: Literal[_]): Literal[_] = l match {
+ case InfiniteIntegerLiteral(v) => FractionalLiteral(v.toInt, 1)
+ case other => other
+ }
+
+ *//**
+ * Here, we return fractional literals for integer-valued variables,
+ * and leave to the client to handle them
+ *//*
+ def unmapLiteral(l: Literal[_]): Literal[_] = l
+
+ def mapIdentifier(v: Identifier): Identifier =
+ if (v.getType == IntegerType) {
+ if (IsTemplateIdentifier(v)) freshIdentifier(v.name, RealType)
+ else FreshIdentifier(v.name, RealType, true)
+ } else v
+}*/
\ No newline at end of file
diff --git a/src/main/scala/leon/invariant/util/RealToInt.scala b/src/main/scala/leon/invariant/util/RealToInt.scala
deleted file mode 100644
index 6c1860160f2bebc5bf0cb574b9c9934985246f45..0000000000000000000000000000000000000000
--- a/src/main/scala/leon/invariant/util/RealToInt.scala
+++ /dev/null
@@ -1,70 +0,0 @@
-package leon
-package invariant.util
-
-import purescala.Common._
-import purescala.Expressions._
-import purescala.ExprOps._
-import purescala.Types._
-import invariant.factories._
-import solvers._
-
-/**
- * maps all real valued variables and literals to new integer variables/literals and
- * performs the reverse mapping
- * Note: this should preserve the template identifier property
- */
-class RealToInt {
-
- val bone = BigInt(1)
- var realToIntId = Map[Identifier, Identifier]()
- var intToRealId = Map[Identifier, Identifier]()
-
- def mapRealToInt(inexpr: Expr): Expr = {
- val transformer = (e: Expr) => e match {
- case FractionalLiteral(num, `bone`) => InfiniteIntegerLiteral(num)
- case FractionalLiteral(_, _) => throw new IllegalStateException("Real literal with non-unit denominator")
- case v @ Variable(realId) if (v.getType == RealType) => {
- val newId = realToIntId.getOrElse(realId, {
- //note: the fresh identifier has to be a template identifier if the original one is a template identifier
- val freshId = if (TemplateIdFactory.IsTemplateIdentifier(realId))
- TemplateIdFactory.freshIdentifier(realId.name, IntegerType)
- else
- FreshIdentifier(realId.name, IntegerType, true)
-
- realToIntId += (realId -> freshId)
- intToRealId += (freshId -> realId)
- freshId
- })
- Variable(newId)
- }
- case _ => e
- }
- simplePostTransform(transformer)(inexpr)
- }
-
- def unmapModel(model: Model): Model = {
- new Model(model.map(pair => {
- val (key, value) = if (intToRealId.contains(pair._1)) {
- (intToRealId(pair._1),
- pair._2 match {
- case InfiniteIntegerLiteral(v) => FractionalLiteral(v.toInt, 1)
- case _ => pair._2
- })
- } else pair
- (key -> value)
- }).toMap)
- }
-
- def mapModel(model: Model): Model = {
- new Model(model.collect {
- case (k, FractionalLiteral(n, bone)) =>
- (realToIntId(k), InfiniteIntegerLiteral(n))
- case (k, v) =>
- if (realToIntId.contains(k)) {
- (realToIntId(k), v)
- } else {
- (k, v)
- }
- }.toMap)
- }
-}
\ No newline at end of file
diff --git a/src/main/scala/leon/invariant/util/RealValuedExprEvaluator.scala b/src/main/scala/leon/invariant/util/RealValuedExprEvaluator.scala
index d591de24533d0f26fdfaae35386a87d1b936b617..9fd5c324eab5719fe47981d807ed8005138e67ff 100644
--- a/src/main/scala/leon/invariant/util/RealValuedExprEvaluator.scala
+++ b/src/main/scala/leon/invariant/util/RealValuedExprEvaluator.scala
@@ -47,12 +47,14 @@ object RealValuedExprEvaluator {
case _ => throw new IllegalStateException("Not an evaluatable expression: " + expr)
}
- def evaluateRealPredicate(expr: Expr): Boolean = expr match {
- case Equals(a @ FractionalLiteral(_, _), b @ FractionalLiteral(_, _)) => isEQZ(evaluate(Minus(a, b)))
- case LessEquals(a @ FractionalLiteral(_, _), b @ FractionalLiteral(_, _)) => isLEZ(evaluate(Minus(a, b)))
- case LessThan(a @ FractionalLiteral(_, _), b @ FractionalLiteral(_, _)) => isLTZ(evaluate(Minus(a, b)))
- case GreaterEquals(a @ FractionalLiteral(_, _), b @ FractionalLiteral(_, _)) => isGEZ(evaluate(Minus(a, b)))
- case GreaterThan(a @ FractionalLiteral(n1, d1), b @ FractionalLiteral(n2, d2)) => isGTZ(evaluate(Minus(a, b)))
+ def evaluateRealPredicate(expr: Expr): Boolean = {
+ expr match {
+ case Equals(a @ FractionalLiteral(_, _), b @ FractionalLiteral(_, _)) => isEQZ(evaluate(Minus(a, b)))
+ case LessEquals(a @ FractionalLiteral(_, _), b @ FractionalLiteral(_, _)) => isLEZ(evaluate(Minus(a, b)))
+ case LessThan(a @ FractionalLiteral(_, _), b @ FractionalLiteral(_, _)) => isLTZ(evaluate(Minus(a, b)))
+ case GreaterEquals(a @ FractionalLiteral(_, _), b @ FractionalLiteral(_, _)) => isGEZ(evaluate(Minus(a, b)))
+ case GreaterThan(a @ FractionalLiteral(n1, d1), b @ FractionalLiteral(n2, d2)) => isGTZ(evaluate(Minus(a, b)))
+ }
}
def isEQZ(rlit: FractionalLiteral): Boolean = {
@@ -95,6 +97,9 @@ object RealValuedExprEvaluator {
case Not(arg) => !evaluateRealFormula(arg)
case BooleanLiteral(b) => b
case Operator(args, op) =>
- evaluateRealPredicate(op(args map evaluate))
+ op(args map evaluate) match {
+ case BooleanLiteral(b) => b
+ case p => evaluateRealPredicate(p)
+ }
}
}
diff --git a/src/main/scala/leon/invariant/util/TreeUtil.scala b/src/main/scala/leon/invariant/util/TreeUtil.scala
index 88dabc505faf476cef5e6fae516e6d90e093d676..df6f64b0c7eda9640a77de2b4b9d2bf847eccc4c 100644
--- a/src/main/scala/leon/invariant/util/TreeUtil.scala
+++ b/src/main/scala/leon/invariant/util/TreeUtil.scala
@@ -117,22 +117,23 @@ object ProgramUtil {
}
/**
- * For functions for which `funToTmpl` is not defined, their templates
- * will be removed
+ * For functions for which `funToTmpl` is not defined, their templates will be removed.
+ * Will only consider user-level functions.
*/
def assignTemplateAndCojoinPost(funToTmpl: Map[FunDef, Expr], prog: Program,
funToPost: Map[FunDef, Expr] = Map(), uniqueIdDisplay: Boolean = false): Program = {
- val funMap = functionsWOFields(prog.definedFunctions).foldLeft(Map[FunDef, FunDef]()) {
- case (accMap, fd) if fd.isTheoryOperation =>
- accMap + (fd -> fd)
+ val keys = funToTmpl.keySet ++ funToPost.keySet
+ val userLevelFuns = userLevelFunctions(prog).toSet
+ if(!keys.diff(userLevelFuns).isEmpty)
+ throw new IllegalStateException("AssignTemplate function called on library functions: "+ keys.diff(userLevelFuns))
+
+ val funMap = userLevelFuns.foldLeft(Map[FunDef, FunDef]()) {
case (accMap, fd) => {
val freshId = FreshIdentifier(fd.id.name, fd.returnType, uniqueIdDisplay)
- val newfd = new FunDef(freshId, fd.tparams, fd.params, fd.returnType)
- accMap.updated(fd, newfd)
+ accMap + (fd -> new FunDef(freshId, fd.tparams, fd.params, fd.returnType))
}
}
-
val mapExpr = mapFunctionsInExpr(funMap) _
for ((from, to) <- funMap) {
to.fullBody = if (!funToTmpl.contains(from)) {
@@ -185,17 +186,12 @@ object ProgramUtil {
newprog
}
- def updatePost(funToPost: Map[FunDef, Lambda], prog: Program,
- uniqueIdDisplay: Boolean = true, excludeLibrary: Boolean = true): Program = {
+ def updatePost(funToPost: Map[FunDef, Lambda], prog: Program, uniqueIdDisplay: Boolean = true): Program = {
- val funMap = functionsWOFields(prog.definedFunctions).foldLeft(Map[FunDef, FunDef]()) {
- case (accMap, fd) if fd.isTheoryOperation || fd.isLibrary || fd.isInvariant =>
- accMap + (fd -> fd)
- case (accMap, fd) => {
+ val funMap = userLevelFunctions(prog).foldLeft(Map[FunDef, FunDef]()) {
+ case (accMap, fd) =>
val freshId = FreshIdentifier(fd.id.name, fd.returnType, uniqueIdDisplay)
- val newfd = new FunDef(freshId, fd.tparams, fd.params, fd.returnType)
- accMap.updated(fd, newfd)
- }
+ accMap + (fd -> new FunDef(freshId, fd.tparams, fd.params, fd.returnType))
}
val mapExpr = mapFunctionsInExpr(funMap) _
for ((from, to) <- funMap) {
@@ -235,6 +231,15 @@ object ProgramUtil {
fds.filter(fd => fd.isRealFunction)
}
+ /**
+ * Functions that are not theory-operations or library methods that are not a part of the main unit
+ */
+ def userLevelFunctions(program: Program): Seq[FunDef] = {
+ program.units.flatMap { u =>
+ u.definedFunctions.filter(fd => !fd.isTheoryOperation && (u.isMainUnit || !(fd.isLibrary || fd.isInvariant)))
+ }
+ }
+
def translateExprToProgram(ine: Expr, currProg: Program, newProg: Program): Expr = {
var funCache = Map[String, Option[FunDef]]()
def funInNewprog(fn: String) =
@@ -340,16 +345,29 @@ object PredicateUtil {
*/
def hasReals(expr: Expr): Boolean = {
var foundReal = false
- simplePostTransform {
- case e => {
- if (e.getType == RealType)
+ postTraversal {
+ case e if e.getType == RealType =>
foundReal = true
- e
- }
+ case _ =>
}(expr)
foundReal
}
+ /**
+ * Checks if the expression has real valued sub-expressions.
+ */
+ def hasRealsOrTemplates(expr: Expr): Boolean = {
+ var found = false
+ postTraversal {
+ case Variable(id) if id.getType == RealType || TemplateIdFactory.IsTemplateIdentifier(id) =>
+ found = true
+ case e if e.getType == RealType =>
+ found = true
+ case _ =>
+ }(expr)
+ found
+ }
+
/**
* Checks if the expression has real valued sub-expressions.
* Note: important, <, <=, > etc have default int type.
@@ -358,12 +376,10 @@ object PredicateUtil {
*/
def hasInts(expr: Expr): Boolean = {
var foundInt = false
- simplePostTransform {
- case e: Terminal if (e.getType == Int32Type || e.getType == IntegerType) => {
+ postTraversal {
+ case e: Terminal if (e.getType == Int32Type || e.getType == IntegerType) =>
foundInt = true
- e
- }
- case e => e
+ case _ =>
}(expr)
foundInt
}
diff --git a/src/main/scala/leon/laziness/LazinessEliminationPhase.scala b/src/main/scala/leon/laziness/LazinessEliminationPhase.scala
index 9c1abab5381882451a3a0769b590301c94d4f81a..a3256232264b208b2e780f7bc9352c203cff0906 100644
--- a/src/main/scala/leon/laziness/LazinessEliminationPhase.scala
+++ b/src/main/scala/leon/laziness/LazinessEliminationPhase.scala
@@ -44,7 +44,6 @@ import java.io.
*/
object LazinessEliminationPhase extends TransformationPhase {
val dumpInputProg = false
- val debugLifting = false
val dumpLiftProg = false
val dumpProgramWithClosures = false
val dumpTypeCorrectProg = false
@@ -79,7 +78,7 @@ object LazinessEliminationPhase extends TransformationPhase {
// refEq is by default false
val nprog = LazyExpressionLifter.liftLazyExpressions(prog, ctx.findOption(optRefEquality).getOrElse(false))
if (dumpLiftProg)
- prettyPrintProgramToFile(nprog, ctx, "-lifted")
+ prettyPrintProgramToFile(nprog, ctx, "-lifted", true)
val funsManager = new LazyFunctionsManager(nprog)
val closureFactory = new LazyClosureFactory(nprog)
diff --git a/src/main/scala/leon/laziness/LazinessUtil.scala b/src/main/scala/leon/laziness/LazinessUtil.scala
index 903ef54e9959cc5165f2d3fdda4cedae8ad23186..79f6fae0b62b334948051146106626da07671008 100644
--- a/src/main/scala/leon/laziness/LazinessUtil.scala
+++ b/src/main/scala/leon/laziness/LazinessUtil.scala
@@ -69,14 +69,14 @@ object LazinessUtil {
def isLazyInvocation(e: Expr)(implicit p: Program): Boolean = e match {
case FunctionInvocation(TypedFunDef(fd, _), Seq(_)) =>
- fullName(fd)(p) == "leon.lazyeval.$.apply"
+ fullName(fd)(p) == "leon.lazyeval.$"
case _ =>
false
}
def isEagerInvocation(e: Expr)(implicit p: Program): Boolean = e match {
case FunctionInvocation(TypedFunDef(fd, _), Seq(_)) =>
- fullName(fd)(p) == "leon.lazyeval.$.eager"
+ fullName(fd)(p) == "leon.lazyeval.eager"
case _ =>
false
}
@@ -84,7 +84,7 @@ object LazinessUtil {
def isInStateCall(e: Expr)(implicit p: Program): Boolean = e match {
case FunctionInvocation(TypedFunDef(fd, _), Seq()) =>
val fn = fullName(fd)(p)
- (fn == "leon.lazyeval.$.inState" || fn == "leon.lazyeval.Mem.inState")
+ (fn == "leon.lazyeval.inState" || fn == "leon.mem.inState")
case _ =>
false
}
@@ -92,33 +92,33 @@ object LazinessUtil {
def isOutStateCall(e: Expr)(implicit p: Program): Boolean = e match {
case FunctionInvocation(TypedFunDef(fd, _), Seq()) =>
val fn = fullName(fd)(p)
- (fn == "leon.lazyeval.$.outState" || fn == "leon.lazyeval.Mem.outState")
+ (fn == "leon.lazyeval.outState" || fn == "leon.mem.outState")
case _ =>
false
}
def isEvaluatedInvocation(e: Expr)(implicit p: Program): Boolean = e match {
case FunctionInvocation(TypedFunDef(fd, _), Seq(_)) =>
- fullName(fd)(p) == "leon.lazyeval.$.isEvaluated"
+ fullName(fd)(p) == "leon.lazyeval.Lazy.isEvaluated"
case _ => false
}
def isSuspInvocation(e: Expr)(implicit p: Program): Boolean = e match {
case FunctionInvocation(TypedFunDef(fd, _), Seq(_, _)) =>
- fullName(fd)(p) == "leon.lazyeval.$.isSuspension"
+ fullName(fd)(p) == "leon.lazyeval.Lazy.isSuspension"
case _ => false
}
def isWithStateCons(e: Expr)(implicit p: Program): Boolean = e match {
case CaseClass(cct, Seq(_)) =>
val fn = fullName(cct.classDef)(p)
- (fn == "leon.lazyeval.$.WithState" || fn == "leon.lazyeval.Mem.memWithState")
+ (fn == "leon.lazyeval.WithState" || fn == "leon.mem.memWithState")
case _ => false
}
def isMemCons(e: Expr)(implicit p: Program): Boolean = e match {
case CaseClass(cct, Seq(_)) =>
- fullName(cct.classDef)(p) == "leon.lazyeval.Mem"
+ fullName(cct.classDef)(p) == "leon.mem.Mem"
case _ => false
}
@@ -130,31 +130,31 @@ object LazinessUtil {
case FunctionInvocation(TypedFunDef(fd, _), _) =>
val fn = fullName(fd)(p)
(fn == "leon.lazyeval.WithState.withState" ||
- fn == "leon.lazyeval.memWithState.withState")
+ fn == "leon.mem.memWithState.withState")
case _ => false
}
def isCachedInv(e: Expr)(implicit p: Program): Boolean = e match {
case FunctionInvocation(TypedFunDef(fd, _), Seq(_)) =>
- fullName(fd)(p) == "leon.lazyeval.Mem.isCached"
+ fullName(fd)(p) == "leon.mem.Mem.isCached"
case _ => false
}
def isValueInvocation(e: Expr)(implicit p: Program): Boolean = e match {
case FunctionInvocation(TypedFunDef(fd, _), Seq(_)) =>
- fullName(fd)(p) == "leon.lazyeval.$.value"
+ fullName(fd)(p) == "leon.lazyeval.Lazy.value"
case _ => false
}
def isStarInvocation(e: Expr)(implicit p: Program): Boolean = e match {
case FunctionInvocation(TypedFunDef(fd, _), Seq(_)) =>
- fullName(fd)(p) == "leon.lazyeval.$.*"
+ fullName(fd)(p) == "leon.lazyeval.Lazy.*"
case _ => false
}
def isLazyType(tpe: TypeTree): Boolean = tpe match {
case CaseClassType(CaseClassDef(cid, _, None, false), Seq(_)) =>
- cid.name == "$"
+ cid.name == "Lazy"
case _ => false
}
diff --git a/src/main/scala/leon/laziness/LazyExpressionLifter.scala b/src/main/scala/leon/laziness/LazyExpressionLifter.scala
index 96683d6114b2d58344b1d091098a431962cd1cb2..bed858694e3efff10742daf73f0638cec21b6ec3 100644
--- a/src/main/scala/leon/laziness/LazyExpressionLifter.scala
+++ b/src/main/scala/leon/laziness/LazyExpressionLifter.scala
@@ -61,8 +61,8 @@ object LazyExpressionLifter {
lazy val needsId = funsMan.callersnTargetOfLazyCons
var newfuns = Map[ExprStructure, (FunDef, ModuleDef)]()
- val fdmap = prog.definedFunctions.collect {
- case fd if !fd.isLibrary && !fd.isInvariant =>
+ val fdmap = ProgramUtil.userLevelFunctions(prog).collect {
+ case fd if fd.hasBody =>
val nname = FreshIdentifier(fd.id.name)
val nfd =
if (createUniqueIds && needsId(fd)) {
@@ -74,15 +74,14 @@ object LazyExpressionLifter {
(fd -> nfd)
}.toMap
- lazy val lazyFun = ProgramUtil.functionByFullName("leon.lazyeval.$.apply", prog).get
- lazy val valueFun = ProgramUtil.functionByFullName("leon.lazyeval.$.value", prog).get
+ lazy val lazyFun = ProgramUtil.functionByFullName("leon.lazyeval.$", prog).get
+ lazy val valueFun = ProgramUtil.functionByFullName("leon.lazyeval.Lazy.value", prog).get
var anchorDef: Option[FunDef] = None // a hack to find anchors
prog.modules.foreach { md =>
def exprLifter(inmem: Boolean)(fl: Option[FreeVarListIterator])(expr: Expr) = expr match {
- // is this $(e) where e is not a funtion
case finv @ FunctionInvocation(lazytfd, Seq(callByNameArg)) if isLazyInvocation(finv)(prog) =>
- val Lambda(Seq(), arg) = callByNameArg // extract the call-by-name parameter
+ val Lambda(Seq(), arg) = callByNameArg // extract the call-by-name parameter
arg match {
case _: FunctionInvocation =>
finv
@@ -116,11 +115,11 @@ object LazyExpressionLifter {
fvVars :+ fl.get.nextExpr
else fvVars
FunctionInvocation(lazytfd, Seq(Lambda(Seq(),
- FunctionInvocation(TypedFunDef(argfun, tparams), params))))
+ FunctionInvocation(TypedFunDef(argfun, tparams), params))))
}
// is the argument of eager invocation not a variable ?
- case finv @ FunctionInvocation(TypedFunDef(fd, Seq(tp)), cbn@Seq(Lambda(Seq(), arg))) if isEagerInvocation(finv)(prog) =>
+ case finv @ FunctionInvocation(TypedFunDef(fd, Seq(tp)), cbn @ Seq(Lambda(Seq(), arg))) if isEagerInvocation(finv)(prog) =>
val rootType = bestRealType(tp)
val ntps = Seq(rootType)
arg match {
@@ -129,7 +128,7 @@ object LazyExpressionLifter {
case _ =>
val freshid = FreshIdentifier("t", rootType)
Let(freshid, arg, FunctionInvocation(TypedFunDef(fd, ntps),
- Seq(Lambda(Seq(), freshid.toVariable))))
+ Seq(Lambda(Seq(), freshid.toVariable))))
}
// is this an invocation of a memoized function ?
@@ -169,8 +168,12 @@ object LazyExpressionLifter {
val nargs = args map rec(inmem || isMemCons(e)(prog))
exprLifter(inmem)(fliter)(op(nargs))
}
- nfd.fullBody = rec(false)(fd.fullBody)
- case _ => ;
+ if(fd.hasPrecondition)
+ nfd.precondition = Some(rec(true)(fd.precondition.get))
+ if (fd.hasPostcondition)
+ nfd.postcondition = Some(rec(true)(fd.postcondition.get))
+ nfd.body = Some(rec(false)(fd.body.get))
+ case fd =>
}
}
val progWithFuns = copyProgram(prog, (defs: Seq[Definition]) => defs.map {
diff --git a/src/main/scala/leon/laziness/LazyVerificationPhase.scala b/src/main/scala/leon/laziness/LazyVerificationPhase.scala
index dcc0384d73175de68d1c4984e594c275dbd3e99b..ac4f04faef23e903787792aaf74b40c96da872af 100644
--- a/src/main/scala/leon/laziness/LazyVerificationPhase.scala
+++ b/src/main/scala/leon/laziness/LazyVerificationPhase.scala
@@ -114,8 +114,9 @@ object LazyVerificationPhase {
val inferctx = new InferenceContext(p, ctxForInf)
val vcSolver = (funDef: FunDef, prog: Program) => new VCSolver(inferctx, prog, funDef)
- if (debugInferProgram)
+ if (debugInferProgram){
prettyPrintProgramToFile(inferctx.inferProgram, checkCtx, "-inferProg", true)
+ }
val results = (new InferenceEngine(inferctx)).analyseProgram(inferctx.inferProgram,
funsToCheck.map(InstUtil.userFunctionName), vcSolver, None)
diff --git a/src/main/scala/leon/transformations/InstProgSimplifier.scala b/src/main/scala/leon/transformations/InstProgSimplifier.scala
index ebb1abe008c066479c719fad4567399dfbe02939..56eecde2a89dc6f52cc966829417ba172d8f38ba 100644
--- a/src/main/scala/leon/transformations/InstProgSimplifier.scala
+++ b/src/main/scala/leon/transformations/InstProgSimplifier.scala
@@ -26,8 +26,14 @@ import invariant.util.LetTupleSimplification._
object ProgramSimplifier {
val debugSimplify = false
- def mapProgram(funMap: Map[FunDef, FunDef]): Map[FunDef, FunDef] = {
-
+ def apply(program: Program, instFuncs: Seq[FunDef]): Program = {
+ val funMap = ((userLevelFunctions(program) ++ instFuncs).distinct).foldLeft(Map[FunDef, FunDef]()) {
+ case (accMap, fd) => {
+ val freshId = FreshIdentifier(fd.id.name, fd.returnType)
+ val newfd = new FunDef(freshId, fd.tparams, fd.params, fd.returnType)
+ accMap + (fd -> newfd)
+ }
+ }
def mapExpr(ine: Expr, fd: FunDef): Expr = {
val replaced = simplePostTransform((e: Expr) => e match {
case FunctionInvocation(tfd, args) if funMap.contains(tfd.fd) =>
@@ -54,39 +60,13 @@ object ProgramSimplifier {
//copy annotations
from.flags.foreach(to.addFlag(_))
}
- funMap
- }
-
- def createNewFunDefs(program: Program): Map[FunDef, FunDef] = {
- val allFuncs = functionsWOFields(program.definedFunctions)
-
- allFuncs.foldLeft(Map[FunDef, FunDef]()) {
- case (accMap, fd) if fd.isTheoryOperation =>
- accMap + (fd -> fd)
- case (accMap, fd) => {
- //here we need not augment the return types
- val freshId = FreshIdentifier(fd.id.name, fd.returnType)
- val newfd = new FunDef(freshId, fd.tparams, fd.params, fd.returnType)
- accMap.updated(fd, newfd)
- }
- }
- }
-
- def createNewProg(mappedFuncs: Map[FunDef, FunDef], prog: Program): Program = {
- val newprog = copyProgram(prog, (defs: Seq[Definition]) => defs.map {
- case fd: FunDef if mappedFuncs.contains(fd) =>
- mappedFuncs(fd)
- case d => d
+ val newprog = copyProgram(program, (defs: Seq[Definition]) => defs.map {
+ case fd: FunDef if funMap.contains(fd) => funMap(fd)
+ case d => d
})
if (debugSimplify)
println("After Simplifications: \n" + ScalaPrinter.apply(newprog))
newprog
}
-
- def apply(program: Program): Program = {
- val newFuncs = createNewFunDefs(program)
- val mappedFuncs = mapProgram(newFuncs)
- createNewProg(mappedFuncs, program)
- }
}
\ No newline at end of file
diff --git a/src/main/scala/leon/transformations/NonlinearityEliminationPhase.scala b/src/main/scala/leon/transformations/NonlinearityEliminationPhase.scala
index 6d740de6aff8b077d271377740e86c7fa5d327ab..68b89227251439c35ca338bf19867a21112d4f72 100644
--- a/src/main/scala/leon/transformations/NonlinearityEliminationPhase.scala
+++ b/src/main/scala/leon/transformations/NonlinearityEliminationPhase.scala
@@ -100,13 +100,12 @@ class NonlinearityEliminator(skipAxioms: Boolean, domain: TypeTree) {
//TOOD: note associativity property of multiplication is not taken into account
def apply(program: Program): Program = {
-
//create a fundef for each function in the program
- val newFundefs = program.definedFunctions.map((fd) => {
- val newFunType = FunctionType(fd.tparams.map((currParam) => currParam.tp), fd.returnType)
+ val newFundefs = userLevelFunctions(program).map { fd =>
+ val newFunType = FunctionType(fd.tparams.map(_.tp), fd.returnType)
val newfd = new FunDef(FreshIdentifier(fd.id.name, newFunType, false), fd.tparams, fd.params, fd.returnType)
- (fd, newfd)
- }).toMap
+ (fd -> newfd)
+ }.toMap
//note, handling templates variables is slightly tricky as we need to preserve a*x as it is
val tmult = TypedFunDef(multFun, Seq())
@@ -135,49 +134,44 @@ class NonlinearityEliminator(skipAxioms: Boolean, domain: TypeTree) {
}
//create a body, pre, post for each newfundef
- newFundefs.foreach((entry) => {
- val (fd, newfd) = entry
-
- //add a new precondition
- newfd.precondition =
- if (fd.precondition.isDefined)
- Some(replaceFun(fd.precondition.get))
- else None
-
- //add a new body
- newfd.body = if (fd.hasBody) {
- //replace variables by constants if possible
- val simpBody = simplifyLets(fd.body.get)
- Some(replaceFun(simpBody))
- } else None
-
- //add a new postcondition
- newfd.postcondition = if (fd.postcondition.isDefined) {
- //we need to handle template and postWoTemplate specially
- val Lambda(resultBinders, _) = fd.postcondition.get
- val tmplExpr = fd.templateExpr
- val newpost = if (fd.hasTemplate) {
- val FunctionInvocation(tmpfd, Seq(Lambda(tmpvars, tmpbody))) = tmplExpr.get
- val newtmp = FunctionInvocation(tmpfd, Seq(Lambda(tmpvars,
- replaceFun(tmpbody, tmpvars.map(_.id).toSet))))
- fd.postWoTemplate match {
- case None =>
- newtmp
- case Some(postExpr) =>
- And(replaceFun(postExpr), newtmp)
- }
- } else
- replaceFun(fd.getPostWoTemplate)
-
- Some(Lambda(resultBinders, newpost))
- } else None
-
- fd.flags.foreach(newfd.addFlag(_))
- })
+ newFundefs.foreach {
+ case (fd, newfd) =>
+ //add a new precondition
+ newfd.precondition =
+ if (fd.precondition.isDefined)
+ Some(replaceFun(fd.precondition.get))
+ else None
+ //add a new body
+ newfd.body = if (fd.hasBody) {
+ //replace variables by constants if possible
+ val simpBody = simplifyLets(fd.body.get)
+ Some(replaceFun(simpBody))
+ } else None
+ //add a new postcondition
+ newfd.postcondition = if (fd.postcondition.isDefined) {
+ //we need to handle template and postWoTemplate specially
+ val Lambda(resultBinders, _) = fd.postcondition.get
+ val tmplExpr = fd.templateExpr
+ val newpost = if (fd.hasTemplate) {
+ val FunctionInvocation(tmpfd, Seq(Lambda(tmpvars, tmpbody))) = tmplExpr.get
+ val newtmp = FunctionInvocation(tmpfd, Seq(Lambda(tmpvars,
+ replaceFun(tmpbody, tmpvars.map(_.id).toSet))))
+ fd.postWoTemplate match {
+ case None =>
+ newtmp
+ case Some(postExpr) =>
+ And(replaceFun(postExpr), newtmp)
+ }
+ } else
+ replaceFun(fd.getPostWoTemplate)
+ Some(Lambda(resultBinders, newpost))
+ } else None
+ fd.flags.foreach(newfd.addFlag(_))
+ }
val transProg = copyProgram(program, (defs: Seq[Definition]) => {
defs.map {
- case fd: FunDef => newFundefs(fd)
- case d => d
+ case fd: FunDef if newFundefs.contains(fd) => newFundefs(fd)
+ case d => d
}
})
val newprog =
diff --git a/src/main/scala/leon/transformations/SerialInstrumentationPhase.scala b/src/main/scala/leon/transformations/SerialInstrumentationPhase.scala
index cee20aca2c56e6c7c17bc4dd9c5405fa49f77d85..7e60625c62e344792c3a5caa66b7a3b4045915e7 100644
--- a/src/main/scala/leon/transformations/SerialInstrumentationPhase.scala
+++ b/src/main/scala/leon/transformations/SerialInstrumentationPhase.scala
@@ -26,8 +26,10 @@ object InstrumentationPhase extends TransformationPhase {
val description = "Instruments the program for all counters needed"
def apply(ctx: LeonContext, program: Program): Program = {
- val instprog = new SerialInstrumenter(program)
- instprog.apply
+ val si = new SerialInstrumenter(program)
+ val instprog = si.apply
+ //println("Instrumented Program: "+ScalaPrinter.apply(instprog, purescala.PrinterOptions(printUniqueIds = true)))
+ instprog
}
}
@@ -36,6 +38,7 @@ class SerialInstrumenter(program: Program,
val debugInstrumentation = false
val exprInstFactory = exprInstOpt.getOrElse((x: Map[FunDef, FunDef], y: SerialInstrumenter, z: FunDef) => new ExprInstrumenter(x, y)(z))
+
val instToInstrumenter: Map[Instrumentation, Instrumenter] =
Map(Time -> new TimeInstrumenter(program, this),
Depth -> new DepthInstrumenter(program, this),
@@ -44,7 +47,7 @@ class SerialInstrumenter(program: Program,
TPR -> new TPRInstrumenter(program, this))
// a map from functions to the list of instrumentations to be performed for the function
- lazy val funcInsts = {
+ val funcInsts = {
var emap = MutableMap[FunDef, List[Instrumentation]]()
def update(fd: FunDef, inst: Instrumentation) {
if (emap.contains(fd))
@@ -59,7 +62,7 @@ class SerialInstrumenter(program: Program,
}
emap.toMap
}
- lazy val instFuncs = funcInsts.keySet //should we exclude theory operations ?
+ val instFuncs = funcInsts.keySet
def instrumenters(fd: FunDef) = funcInsts(fd) map instToInstrumenter.apply _
def instTypes(fd: FunDef) = funcInsts(fd).map(_.getType)
@@ -72,121 +75,118 @@ class SerialInstrumenter(program: Program,
def apply: Program = {
- //create new functions. Augment the return type of a function iff the postcondition uses
- //the instrumentation variable or if the function is transitively called from such a function
- //note: need not instrument fields
- val funMap = functionsWOFields(program.definedFunctions).foldLeft(Map[FunDef, FunDef]()) {
- case (accMap, fd: FunDef) if fd.isTheoryOperation =>
- accMap + (fd -> fd)
- case (accMap, fd) => {
+ if (instFuncs.isEmpty) program
+ else {
+ //create new functions. Augment the return type of a function iff the postcondition uses
+ //the instrumentation variable or if the function is transitively called from such a function
+ var funMap = Map[FunDef, FunDef]()
+ (userLevelFunctions(program) ++ instFuncs).distinct.foreach { fd =>
if (instFuncs.contains(fd)) {
val newRetType = TupleType(fd.returnType +: instTypes(fd))
// let the names of the function encode the kind of instrumentations performed
val freshId = FreshIdentifier(fd.id.name + "-" + funcInsts(fd).map(_.name).mkString("-"), newRetType)
val newfd = new FunDef(freshId, fd.tparams, fd.params, newRetType)
- accMap + (fd -> newfd)
+ funMap += (fd -> newfd)
} else {
//here we need not augment the return types but do need to create a new copy
val freshId = FreshIdentifier(fd.id.name, fd.returnType)
val newfd = new FunDef(freshId, fd.tparams, fd.params, fd.returnType)
- accMap + (fd -> newfd)
+ funMap += (fd -> newfd)
}
}
- }
- def mapExpr(ine: Expr): Expr = {
- simplePostTransform((e: Expr) => e match {
- case FunctionInvocation(tfd, args) if funMap.contains(tfd.fd) =>
- if (instFuncs.contains(tfd.fd))
- TupleSelect(FunctionInvocation(TypedFunDef(funMap(tfd.fd), tfd.tps), args), 1)
- else
- FunctionInvocation(TypedFunDef(funMap(tfd.fd), tfd.tps), args)
- case _ => e
- })(ine)
- }
+ def mapExpr(ine: Expr): Expr = {
+ simplePostTransform((e: Expr) => e match {
+ case FunctionInvocation(tfd, args) if funMap.contains(tfd.fd) =>
+ if (instFuncs.contains(tfd.fd))
+ TupleSelect(FunctionInvocation(TypedFunDef(funMap(tfd.fd), tfd.tps), args), 1)
+ else
+ FunctionInvocation(TypedFunDef(funMap(tfd.fd), tfd.tps), args)
+ case _ => e
+ })(ine)
+ }
- def mapBody(body: Expr, from: FunDef, to: FunDef) = {
- val res =
- if (from.isExtern) {
- // this is an extern function, we must only rely on the specs
- // so make the body empty
- NoTree(to.returnType)
- } else if (instFuncs.contains(from)) {
- //(new ExprInstrumenter(funMap, this)(from)(body))
- exprInstFactory(funMap, this, from)(body)
- } else
- mapExpr(body)
- res
- }
+ def mapBody(body: Expr, from: FunDef, to: FunDef) = {
+ val res =
+ if (from.isExtern) {
+ // this is an extern function, we must only rely on the specs
+ // so make the body empty
+ NoTree(to.returnType)
+ } else if (instFuncs.contains(from)) {
+ exprInstFactory(funMap, this, from)(body)
+ } else
+ mapExpr(body)
+ res
+ }
- def mapPost(pred: Expr, from: FunDef, to: FunDef) = {
- pred match {
- case Lambda(Seq(ValDef(fromRes)), postCond) if (instFuncs.contains(from)) =>
- val toResId = FreshIdentifier(fromRes.name, to.returnType, true)
- val newpost = postMap((e: Expr) => e match {
- case Variable(`fromRes`) =>
- Some(TupleSelect(toResId.toVariable, 1))
-
- case _ if funcInsts(from).exists(_.isInstVariable(e)) =>
- val inst = funcInsts(from).find(_.isInstVariable(e)).get
- Some(TupleSelect(toResId.toVariable, instIndex(from)(inst)))
-
- case _ =>
- None
- })(postCond)
- Lambda(Seq(ValDef(toResId)), mapExpr(newpost))
- case _ =>
- mapExpr(pred)
+ def mapPost(pred: Expr, from: FunDef, to: FunDef) = {
+ pred match {
+ case Lambda(Seq(ValDef(fromRes)), postCond) if (instFuncs.contains(from)) =>
+ val toResId = FreshIdentifier(fromRes.name, to.returnType, true)
+ val newpost = postMap((e: Expr) => e match {
+ case Variable(`fromRes`) =>
+ Some(TupleSelect(toResId.toVariable, 1))
+
+ case _ if funcInsts(from).exists(_.isInstVariable(e)) =>
+ val inst = funcInsts(from).find(_.isInstVariable(e)).get
+ Some(TupleSelect(toResId.toVariable, instIndex(from)(inst)))
+
+ case _ =>
+ None
+ })(postCond)
+ Lambda(Seq(ValDef(toResId)), mapExpr(newpost))
+ case _ =>
+ mapExpr(pred)
+ }
}
- }
- // Map the bodies and preconditions
- for ((from, to) <- funMap) {
- //copy annotations
- from.flags.foreach(to.addFlag(_))
- to.fullBody = from.fullBody match {
- case b @ NoTree(_) => NoTree(to.returnType)
- case Require(pre, body) =>
- //here 'from' does not have a postcondition but 'to' will always have a postcondition
- val toPost =
- Lambda(Seq(ValDef(FreshIdentifier("res", to.returnType))), BooleanLiteral(true))
- val bodyPre =
- Require(mapExpr(pre), mapBody(body, from, to))
- Ensuring(bodyPre, toPost)
-
- case Ensuring(Require(pre, body), post) =>
- Ensuring(Require(mapExpr(pre), mapBody(body, from, to)),
- mapPost(post, from, to))
-
- case Ensuring(body, post) =>
- Ensuring(mapBody(body, from, to), mapPost(post, from, to))
-
- case body =>
- val toPost =
- Lambda(Seq(ValDef(FreshIdentifier("res", to.returnType))), BooleanLiteral(true))
- Ensuring(mapBody(body, from, to), toPost)
+ // Map the bodies and preconditions
+ for ((from, to) <- funMap) {
+ //copy annotations
+ from.flags.foreach(to.addFlag(_))
+ to.fullBody = from.fullBody match {
+ case b @ NoTree(_) => NoTree(to.returnType)
+ case Require(pre, body) =>
+ //here 'from' does not have a postcondition but 'to' will always have a postcondition
+ val toPost =
+ Lambda(Seq(ValDef(FreshIdentifier("res", to.returnType))), BooleanLiteral(true))
+ val bodyPre =
+ Require(mapExpr(pre), mapBody(body, from, to))
+ Ensuring(bodyPre, toPost)
+
+ case Ensuring(Require(pre, body), post) =>
+ Ensuring(Require(mapExpr(pre), mapBody(body, from, to)),
+ mapPost(post, from, to))
+
+ case Ensuring(body, post) =>
+ Ensuring(mapBody(body, from, to), mapPost(post, from, to))
+
+ case body =>
+ val toPost =
+ Lambda(Seq(ValDef(FreshIdentifier("res", to.returnType))), BooleanLiteral(true))
+ Ensuring(mapBody(body, from, to), toPost)
+ }
}
- }
- val additionalFuncs = funMap.flatMap {
- case (k, _) =>
- if (instFuncs(k))
- instrumenters(k).flatMap(_.additionalfunctionsToAdd)
- else List()
- }.toList.distinct
-
- val newprog = copyProgram(program, (defs: Seq[Definition]) =>
- defs.map {
- case fd: FunDef if funMap.contains(fd) =>
- funMap(fd)
- case d => d
- } ++ additionalFuncs)
- if (debugInstrumentation)
- println("After Instrumentation: \n" + ScalaPrinter.apply(newprog))
-
- ProgramSimplifier(newprog)
+ val additionalFuncs = funMap.flatMap {
+ case (k, _) =>
+ if (instFuncs(k))
+ instrumenters(k).flatMap(_.additionalfunctionsToAdd)
+ else List()
+ }.toList.distinct
+
+ val newprog = copyProgram(program, (defs: Seq[Definition]) =>
+ defs.map {
+ case fd: FunDef if funMap.contains(fd) =>
+ funMap(fd)
+ case d => d
+ } ++ additionalFuncs)
+ if (debugInstrumentation)
+ println("After Instrumentation: \n" + ScalaPrinter.apply(newprog))
+
+ ProgramSimplifier(newprog, instFuncs.toSeq)
+ }
}
-
}
class ExprInstrumenter(funMap: Map[FunDef, FunDef], serialInst: SerialInstrumenter)(implicit currFun: FunDef) {
@@ -250,11 +250,9 @@ class ExprInstrumenter(funMap: Map[FunDef, FunDef], serialInst: SerialInstrument
val valexpr = TupleSelect(resvar, 1)
val instexprs = instrumenters.map { m =>
val calleeInst =
- if (serialInst.funcInsts(fd).contains(m.inst) &&
- fd.isUserFunction) {
- // ignoring fields here
+ if (serialInst.funcInsts(fd).contains(m.inst) && fd.isUserFunction) {
List(serialInst.selectInst(fd)(resvar, m.inst))
- } else List()
+ } else List() // ignoring fields here
//Note we need to ensure that the last element of list is the instval of the finv
m.instrument(e, subeInsts.getOrElse(m.inst, List()) ++ calleeInst, Some(resvar))
}
@@ -411,12 +409,6 @@ class ExprInstrumenter(funMap: Map[FunDef, FunDef], serialInst: SerialInstrument
case n @ Operator(ss, recons) =>
tupleify(e, ss, recons)
- /* case b @ BinaryOperator(s1, s2, recons) =>
- tupleify(e, Seq(s1, s2), { case Seq(s1, s2) => recons(s1, s2) })
-
- case u @ UnaryOperator(s, recons) =>
- tupleify(e, Seq(s), { case Seq(s) => recons(s) })
-*/
case t: Terminal =>
tupleify(e, Seq(), { case Seq() => t })
}
@@ -431,7 +423,6 @@ class ExprInstrumenter(funMap: Map[FunDef, FunDef], serialInst: SerialInstrument
val instExprs = instrumenters map { m =>
m.instrumentBody(newe,
selectInst(bodyId.toVariable, m.inst))
-
}
Let(bodyId, transformed,
Tuple(TupleSelect(bodyId.toVariable, 1) +: instExprs))
diff --git a/testcases/lazy-datastructures/Unproved/HammingProblem.scala b/testcases/lazy-datastructures/Unproved/HammingProblem.scala
deleted file mode 100644
index 79acc3ba6bd132a86efed9cc8c74a70a2dbe6a46..0000000000000000000000000000000000000000
--- a/testcases/lazy-datastructures/Unproved/HammingProblem.scala
+++ /dev/null
@@ -1,94 +0,0 @@
-import leon.lazyeval._
-import leon.lang._
-import leon.annotation._
-import leon.instrumentation._
-import leon.lazyeval.$.eagerToLazy
-import scala.math.BigInt.int2bigInt
-//import leon.invariant._
-
-/**
- * Not the required bound
- */
-object Hamming {
-
- sealed abstract class IList {
- def size: BigInt = {
- this match {
- case SNil() => BigInt(0)
- case SCons(x, t) => 1 + ssize(t)
- }
- } ensuring (_ >= 0)
- }
- case class SCons(x: BigInt, tail: $[IList]) extends IList
- case class SNil() extends IList
- def ssize(l: $[IList]): BigInt = (l*).size
-
- sealed abstract class List {
- def size: BigInt = {
- this match {
- case Cons(_, xs) => 1 + xs.size
- case _ => BigInt(0)
- }
- } ensuring (_ >= 0)
- }
- case class Cons(x: BigInt, tail: List) extends List
- case class Nil() extends List
-
- /**
- * The following implementation of Merge
- * produces a list with out duplicates
- */
- def merge(a: $[IList], b: $[IList]): IList = {
- require(a.isSuspension(mult _) && b.isSuspension(mult _))
- b.value match {
- case SNil() => a.value
- case bl @ SCons(x, xs) =>
- a.value match {
- case SNil() => bl
- case SCons(y, ys) =>
- if (x == y)
- SCons(x, $(merge(ys, xs)))
- else if (y < x)
- SCons(y, $(merge(ys, b)))
- else
- SCons(x, $(merge(a, xs)))
- }
- }
- } ensuring(_ => time <= 100)
-
- def mult(num: BigInt, l: IList): IList ={
- l match {
- case SNil() => SNil()
- case SCons(x, tail) => SCons(num*x, tail)
- }
- } ensuring(_ => time <= 20)
-
- def nextElems(n: BigInt): IList = {
- merge(merge($(mult(2, hamming(n-1))), $(mult(3, hamming(n-1)))),
- $(mult(5, hamming(n-1))))
- } //ensuring(_ => time <= )
-
- /**
- * 'n' is some constant that controls the size.
- * Note: the return list would have at least 'n' elements (and possibly more)
- * but is still finite
- */
- def hamming(n: BigInt): IList = {
- if (n <= 0)
- SNil()
- else
- SCons(1, $(nextElems(n)))
- }
-
- def kthHamming(k: BigInt, hstream: $[IList]): BigInt = {
- require(k >= 1)
- hstream.value match {
- case SCons(x, _) =>
- if(k == 1)
- x
- else kthHamming(k-1, hstream)
- case SNil() =>
- BigInt(-1)
- }
- } //ensuring(_ => time <= 40 * k + 40)
-}
diff --git a/testcases/lazy-datastructures/build.sbt b/testcases/lazy-datastructures/build.sbt
new file mode 100644
index 0000000000000000000000000000000000000000..ff26464c904443455179389615dcd4d5963986fb
--- /dev/null
+++ b/testcases/lazy-datastructures/build.sbt
@@ -0,0 +1,15 @@
+name := "LazyDataStructures"
+
+version := "1.0"
+
+organization := "ch.epfl.lara"
+
+scalaVersion := "2.11.7"
+
+fork in run := true
+
+javaOptions in run ++= Seq("-Xmx5G", "-Xms3G", "-Xss500M")
+
+scalacOptions ++= Seq("-optimise")
+
+unmanagedSourceDirectories in Compile ++= Seq("withOrb", "eager").map(dir => baseDirectory.value / dir)
diff --git a/testcases/lazy-datastructures/conc/Conqueue.scala b/testcases/lazy-datastructures/conc/Conqueue.scala
index 8e16fb1bc8cbb26cb8b462cc9e7cb74ac2120b95..360aef160c64cdd60406066fd4fbafbc9d43a4fc 100644
--- a/testcases/lazy-datastructures/conc/Conqueue.scala
+++ b/testcases/lazy-datastructures/conc/Conqueue.scala
@@ -1,11 +1,11 @@
package conc
-import leon.lazyeval._
-import leon.lang._
-import leon.math._
-import leon.annotation._
-import leon.instrumentation._
-import leon.lazyeval.$._
+import leon._
+import lazyeval._
+import lang._
+import math._
+import annotation._
+import instrumentation._
import ConcTrees._
@@ -42,7 +42,7 @@ object Conqueue {
}
case class Tip[T](t: Conc[T]) extends ConQ[T]
- case class Spine[T](head: Conc[T], createdWithSuspension: Bool, rear: $[ConQ[T]]) extends ConQ[T]
+ case class Spine[T](head: Conc[T], createdWithSuspension: Bool, rear: Lazy[ConQ[T]]) extends ConQ[T]
sealed abstract class Bool
case class True() extends Bool
@@ -51,7 +51,7 @@ object Conqueue {
/**
* Checks whether there is a zero before an unevaluated closure
*/
- def zeroPrecedesLazy[T](q: $[ConQ[T]]): Boolean = {
+ def zeroPrecedesLazy[T](q: Lazy[ConQ[T]]): Boolean = {
if (q.isEvaluated) {
q* match {
case Spine(Empty(), _, rear) =>
@@ -66,7 +66,7 @@ object Conqueue {
/**
* Checks whether there is a zero before a given suffix
*/
- def zeroPrecedesSuf[T](q: $[ConQ[T]], suf: $[ConQ[T]]): Boolean = {
+ def zeroPrecedesSuf[T](q: Lazy[ConQ[T]], suf: Lazy[ConQ[T]]): Boolean = {
if (q != suf) {
q* match {
case Spine(Empty(), _, rear) => true
@@ -81,7 +81,7 @@ object Conqueue {
* Everything until suf is evaluated. This
* also asserts that suf should be a suffix of the list
*/
- def concreteUntil[T](l: $[ConQ[T]], suf: $[ConQ[T]]): Boolean = {
+ def concreteUntil[T](l: Lazy[ConQ[T]], suf: Lazy[ConQ[T]]): Boolean = {
if (l != suf) {
l.isEvaluated && (l* match {
case Spine(_, cws, tail) =>
@@ -92,7 +92,7 @@ object Conqueue {
} else true
}
- def isConcrete[T](l: $[ConQ[T]]): Boolean = {
+ def isConcrete[T](l: Lazy[ConQ[T]]): Boolean = {
l.isEvaluated && (l* match {
case Spine(_, _, tail) =>
isConcrete(tail)
@@ -101,10 +101,10 @@ object Conqueue {
}
sealed abstract class Scheds[T]
- case class Cons[T](h: $[ConQ[T]], tail: Scheds[T]) extends Scheds[T]
+ case class Cons[T](h: Lazy[ConQ[T]], tail: Scheds[T]) extends Scheds[T]
case class Nil[T]() extends Scheds[T]
- def schedulesProperty[T](q: $[ConQ[T]], schs: Scheds[T]): Boolean = {
+ def schedulesProperty[T](q: Lazy[ConQ[T]], schs: Scheds[T]): Boolean = {
schs match {
case Cons(head, tail) =>
head* match {
@@ -120,7 +120,7 @@ object Conqueue {
}
}
- def strongSchedsProp[T](q: $[ConQ[T]], schs: Scheds[T]) = {
+ def strongSchedsProp[T](q: Lazy[ConQ[T]], schs: Scheds[T]) = {
q.isEvaluated && {
schs match {
case Cons(head, tail) =>
@@ -134,7 +134,7 @@ object Conqueue {
/**
* Note: if 'q' has a suspension then it would have a carry.
*/
- def pushUntilCarry[T](q: $[ConQ[T]]): $[ConQ[T]] = {
+ def pushUntilCarry[T](q: Lazy[ConQ[T]]): Lazy[ConQ[T]] = {
q* match {
case Spine(Empty(), _, rear) => // if we push a carry and get back 0 then there is a new carry
pushUntilCarry(rear)
@@ -145,11 +145,11 @@ object Conqueue {
}
}
- case class Queue[T](queue: $[ConQ[T]], schedule: Scheds[T]) {
+ case class Queue[T](queue: Lazy[ConQ[T]], schedule: Scheds[T]) {
val valid = strongSchedsProp(queue, schedule)
}
- def pushLeft[T](ys: Single[T], xs: $[ConQ[T]]): ConQ[T] = {
+ def pushLeft[T](ys: Single[T], xs: Lazy[ConQ[T]]): ConQ[T] = {
require(zeroPrecedesLazy(xs))
xs.value match {
case Tip(CC(_, _)) =>
@@ -167,7 +167,7 @@ object Conqueue {
// this procedure does not change state
@invstate
- def pushLeftLazy[T](ys: Conc[T], xs: $[ConQ[T]]): ConQ[T] = {
+ def pushLeftLazy[T](ys: Conc[T], xs: Lazy[ConQ[T]]): ConQ[T] = {
require(!ys.isEmpty && zeroPrecedesLazy(xs) &&
(xs* match {
case Spine(h, _, _) => h != Empty[T]()
@@ -214,7 +214,7 @@ object Conqueue {
* forall suf. suf*.head != Empty() ^ zeroPredsSuf(xs, suf) ^ concUntil(xs.tail.tail, suf) => concUntil(push(rear), suf)
*/
@invstate
- def pushLeftLazyLemma[T](ys: Conc[T], xs: $[ConQ[T]], suf: $[ConQ[T]]): Boolean = {
+ def pushLeftLazyLemma[T](ys: Conc[T], xs: Lazy[ConQ[T]], suf: Lazy[ConQ[T]]): Boolean = {
require(!ys.isEmpty && zeroPrecedesSuf(xs, suf) &&
(xs* match {
case Spine(h, _, _) => h != Empty[T]()
@@ -266,7 +266,7 @@ object Conqueue {
case _ =>
w.schedule
}
- val lq: $[ConQ[T]] = nq
+ val lq: Lazy[ConQ[T]] = nq
(lq, nsched)
} ensuring { res =>
// lemma instantiations
@@ -285,7 +285,7 @@ object Conqueue {
time <= 80
}
- def Pay[T](q: $[ConQ[T]], scheds: Scheds[T]): Scheds[T] = {
+ def Pay[T](q: Lazy[ConQ[T]], scheds: Scheds[T]): Scheds[T] = {
require(schedulesProperty(q, scheds) && q.isEvaluated)
scheds match {
case c @ Cons(head, rest) =>
@@ -341,7 +341,7 @@ object Conqueue {
}
// monotonicity lemmas
- def schedMonotone[T](st1: Set[$[ConQ[T]]], st2: Set[$[ConQ[T]]], scheds: Scheds[T], l: $[ConQ[T]]): Boolean = {
+ def schedMonotone[T](st1: Set[Lazy[ConQ[T]]], st2: Set[Lazy[ConQ[T]]], scheds: Scheds[T], l: Lazy[ConQ[T]]): Boolean = {
require(st1.subsetOf(st2) &&
(schedulesProperty(l, scheds) withState st1)) // here the input state is fixed as 'st1'
//induction scheme
@@ -359,18 +359,18 @@ object Conqueue {
} holds
@traceInduct
- def concreteMonotone[T](st1: Set[$[ConQ[T]]], st2: Set[$[ConQ[T]]], l: $[ConQ[T]]): Boolean = {
+ def concreteMonotone[T](st1: Set[Lazy[ConQ[T]]], st2: Set[Lazy[ConQ[T]]], l: Lazy[ConQ[T]]): Boolean = {
((isConcrete(l) withState st1) && st1.subsetOf(st2)) ==> (isConcrete(l) withState st2)
} holds
@traceInduct
- def concUntilMonotone[T](q: $[ConQ[T]], suf: $[ConQ[T]], st1: Set[$[ConQ[T]]], st2: Set[$[ConQ[T]]]): Boolean = {
+ def concUntilMonotone[T](q: Lazy[ConQ[T]], suf: Lazy[ConQ[T]], st1: Set[Lazy[ConQ[T]]], st2: Set[Lazy[ConQ[T]]]): Boolean = {
((concreteUntil(q, suf) withState st1) && st1.subsetOf(st2)) ==> (concreteUntil(q, suf) withState st2)
} holds
// suffix predicates and their properties (this should be generalizable)
- def suffix[T](q: $[ConQ[T]], suf: $[ConQ[T]]): Boolean = {
+ def suffix[T](q: Lazy[ConQ[T]], suf: Lazy[ConQ[T]]): Boolean = {
if (q == suf) true
else {
q* match {
@@ -381,7 +381,7 @@ object Conqueue {
}
}
- def properSuffix[T](l: $[ConQ[T]], suf: $[ConQ[T]]): Boolean = {
+ def properSuffix[T](l: Lazy[ConQ[T]], suf: Lazy[ConQ[T]]): Boolean = {
l* match {
case Spine(_, _, rear) =>
suffix(rear, suf)
@@ -393,7 +393,7 @@ object Conqueue {
* suf(q, suf) ==> suf(q.rear, suf.rear)
*/
@traceInduct
- def suffixTrans[T](q: $[ConQ[T]], suf: $[ConQ[T]]): Boolean = {
+ def suffixTrans[T](q: Lazy[ConQ[T]], suf: Lazy[ConQ[T]]): Boolean = {
suffix(q, suf) ==> ((q*, suf*) match {
case (Spine(_, _, rear), Spine(_, _, sufRear)) =>
// 'sufRear' should be a suffix of 'rear1'
@@ -405,7 +405,7 @@ object Conqueue {
/**
* properSuf(l, suf) ==> l != suf
*/
- def suffixDisequality[T](l: $[ConQ[T]], suf: $[ConQ[T]]): Boolean = {
+ def suffixDisequality[T](l: Lazy[ConQ[T]], suf: Lazy[ConQ[T]]): Boolean = {
require(properSuffix(l, suf))
suffixTrans(l, suf) && // lemma instantiation
((l*, suf*) match { // induction scheme
@@ -417,21 +417,21 @@ object Conqueue {
}.holds
@traceInduct
- def suffixCompose[T](q: $[ConQ[T]], suf1: $[ConQ[T]], suf2: $[ConQ[T]]): Boolean = {
+ def suffixCompose[T](q: Lazy[ConQ[T]], suf1: Lazy[ConQ[T]], suf2: Lazy[ConQ[T]]): Boolean = {
(suffix(q, suf1) && properSuffix(suf1, suf2)) ==> properSuffix(q, suf2)
} holds
// properties of 'concUntil'
@traceInduct
- def concreteUntilIsSuffix[T](l: $[ConQ[T]], suf: $[ConQ[T]]): Boolean = {
+ def concreteUntilIsSuffix[T](l: Lazy[ConQ[T]], suf: Lazy[ConQ[T]]): Boolean = {
concreteUntil(l, suf) ==> suffix(l, suf)
}.holds
// properties that extend `concUntil` to larger portions of the queue
@traceInduct
- def concUntilExtenLemma[T](q: $[ConQ[T]], suf: $[ConQ[T]], st1: Set[$[ConQ[T]]], st2: Set[$[ConQ[T]]]): Boolean = {
+ def concUntilExtenLemma[T](q: Lazy[ConQ[T]], suf: Lazy[ConQ[T]], st1: Set[Lazy[ConQ[T]]], st2: Set[Lazy[ConQ[T]]]): Boolean = {
((concreteUntil(q, suf) withState st1) && st2 == st1 ++ Set(suf)) ==>
(suf* match {
case Spine(_, _, rear) =>
@@ -441,12 +441,12 @@ object Conqueue {
} holds
@traceInduct
- def concUntilConcreteExten[T](q: $[ConQ[T]], suf: $[ConQ[T]]): Boolean = {
+ def concUntilConcreteExten[T](q: Lazy[ConQ[T]], suf: Lazy[ConQ[T]]): Boolean = {
(concreteUntil(q, suf) && isConcrete(suf)) ==> isConcrete(q)
} holds
@traceInduct
- def concUntilCompose[T](q: $[ConQ[T]], suf1: $[ConQ[T]], suf2: $[ConQ[T]]): Boolean = {
+ def concUntilCompose[T](q: Lazy[ConQ[T]], suf1: Lazy[ConQ[T]], suf2: Lazy[ConQ[T]]): Boolean = {
(concreteUntil(q, suf1) && concreteUntil(suf1, suf2)) ==> concreteUntil(q, suf2)
} holds
@@ -454,18 +454,18 @@ object Conqueue {
// - these are used in preconditions to derive the `zeroPrecedesLazy` property
@traceInduct
- def zeroPredSufConcreteUntilLemma[T](q: $[ConQ[T]], suf: $[ConQ[T]]): Boolean = {
+ def zeroPredSufConcreteUntilLemma[T](q: Lazy[ConQ[T]], suf: Lazy[ConQ[T]]): Boolean = {
(zeroPrecedesSuf(q, suf) && concreteUntil(q, suf)) ==> zeroPrecedesLazy(q)
} holds
@traceInduct
- def concreteZeroPredLemma[T](q: $[ConQ[T]]): Boolean = {
+ def concreteZeroPredLemma[T](q: Lazy[ConQ[T]]): Boolean = {
isConcrete(q) ==> zeroPrecedesLazy(q)
} holds
// properties relating `suffix` an `zeroPrecedesSuf`
- def suffixZeroLemma[T](q: $[ConQ[T]], suf: $[ConQ[T]], suf2: $[ConQ[T]]): Boolean = {
+ def suffixZeroLemma[T](q: Lazy[ConQ[T]], suf: Lazy[ConQ[T]], suf2: Lazy[ConQ[T]]): Boolean = {
require(suf* match {
case Spine(Empty(), _, _) =>
suffix(q, suf) && properSuffix(suf, suf2)
diff --git a/testcases/lazy-datastructures/eager/AmortizedQueue.scala b/testcases/lazy-datastructures/eager/AmortizedQueue.scala
new file mode 100644
index 0000000000000000000000000000000000000000..cdbb65727a009a4aed77514b904254a692f925b6
--- /dev/null
+++ b/testcases/lazy-datastructures/eager/AmortizedQueue.scala
@@ -0,0 +1,83 @@
+package eagerEval
+
+import leon._
+import invariant._
+import instrumentation._
+
+object AmortizedQueue {
+ sealed abstract class List {
+ val size: BigInt = this match {
+ case Nil() => 0
+ case Cons(_, xs) => 1 + xs.size
+ }
+ }
+ case class Cons(head: BigInt, tail: List) extends List
+ case class Nil() extends List
+
+ def concat(l1: List, l2: List): List = (l1 match {
+ case Nil() => l2
+ case Cons(x, xs) => Cons(x, concat(xs, l2))
+
+ }) ensuring (res => res.size == l1.size + l2.size && time <= ? * l1.size + ?)
+
+ def reverseRec(l1: List, l2: List): List = (l1 match {
+ case Nil() => l2
+ case Cons(x, xs) => reverseRec(xs, Cons(x, l2))
+ }) ensuring (res => l1.size + l2.size == res.size && time <= ? * l1.size + ?)
+
+ def listRev(l: List): List = {
+ reverseRec(l, Nil())
+ } ensuring (res => l.size == res.size && time <= ? * l.size + ?)
+
+ def removeLast(l: List): List = {
+ require(l != Nil())
+ l match {
+ case Cons(x, Nil()) => Nil()
+ case Cons(x, xs) => Cons(x, removeLast(xs))
+ case _ => Nil()
+ }
+ } ensuring (res => res.size <= l.size && tmpl((a, b) => time <= a * l.size + b))
+
+ case class Queue(front: List, rear: List) {
+ def qsize: BigInt = front.size + rear.size
+
+ def asList: List = concat(front, listRev(rear))
+
+ def isAmortized: Boolean = front.size >= rear.size
+
+ def isEmpty: Boolean = this match {
+ case Queue(Nil(), Nil()) => true
+ case _ => false
+ }
+
+ def amortizedQueue(front: List, rear: List): Queue = {
+ if (rear.size <= front.size)
+ Queue(front, rear)
+ else
+ Queue(concat(front, listRev(rear)), Nil())
+ }
+
+ def enqueue(elem: BigInt): Queue = ({
+ amortizedQueue(front, Cons(elem, rear))
+ }) ensuring (_ => time <= ? * qsize + ?)
+
+ def dequeue: Queue = {
+ require(isAmortized && !isEmpty)
+ front match {
+ case Cons(f, fs) => amortizedQueue(fs, rear)
+ case _ => Queue(Nil(), Nil())
+ }
+ } ensuring (_ => time <= ? * qsize + ?)
+
+ def head: BigInt = {
+ require(isAmortized && !isEmpty)
+ front match {
+ case Cons(f, _) => f
+ }
+ }
+
+ def reverse: Queue = { // this lets the queue perform deque operation (but they no longer have efficient constant time amortized bounds)
+ amortizedQueue(rear, front)
+ }
+ }
+}
diff --git a/testcases/lazy-datastructures/eager/BasicMergeSort.scala b/testcases/lazy-datastructures/eager/BasicMergeSort.scala
new file mode 100644
index 0000000000000000000000000000000000000000..481bbbbf061b3ca6bda3a72aee3744bb40252208
--- /dev/null
+++ b/testcases/lazy-datastructures/eager/BasicMergeSort.scala
@@ -0,0 +1,41 @@
+package eagerEval
+
+import leon._
+import lang._
+import collection._
+
+object MergeSort {
+
+ def merge[T](less: (T, T) => Boolean)(xs: List[T], ys: List[T]): List[T] = {
+ (xs, ys) match {
+ case (Nil(), _) => ys
+ case (_, Nil()) => xs
+ case (Cons(x, xtail), Cons(y, ytail)) =>
+ if (less(x, y))
+ x :: merge(less)(xtail, ys)
+ else
+ y :: merge(less)(xs, ytail)
+ }
+ } ensuring { res => res.content == xs.content ++ ys.content &&
+ res.size == xs.size + ys.size }
+
+ def split[T](list: List[T]): (List[T], List[T]) = {
+ list match {
+ case Nil() => (Nil(), Nil())
+ case Cons(x, Nil()) => (Cons(x, Nil()), Nil())
+ case Cons(x1, Cons(x2, xs)) =>
+ val (s1, s2) = split(xs)
+ (Cons(x1, s1), Cons(x2, s2))
+ }
+ }
+
+ def msort[T](less: (T, T) => Boolean)(l: List[T]): List[T] = {
+ l match {
+ case Nil() => Nil[T]()
+ case Cons(x, Nil()) => Cons(x, Nil())
+ case _ =>
+ val (first, second) = split(l)
+ merge(less)(msort(less)(first), msort(less)(second))
+ }
+ } ensuring { res => res.content == l.content && res.size == l.size }
+}
diff --git a/testcases/lazy-datastructures/eager/BigNums.scala b/testcases/lazy-datastructures/eager/BigNums.scala
new file mode 100644
index 0000000000000000000000000000000000000000..5d0271b0e354a578b4a43371e9b5dce087a4015a
--- /dev/null
+++ b/testcases/lazy-datastructures/eager/BigNums.scala
@@ -0,0 +1,79 @@
+package eagerEval
+
+import leon._
+import annotation._
+import invariant._
+import instrumentation._
+
+object BigNums {
+ sealed abstract class Digit
+ case class Zero() extends Digit {
+ @ignore
+ override def toString = "0"
+ }
+ case class One() extends Digit {
+ @ignore
+ override def toString = "1"
+ }
+
+ sealed abstract class BigNum
+ case class Cons(head: Digit, tail: BigNum) extends BigNum
+ case class Nil() extends BigNum
+
+ /**
+ * Time taken by the increment method
+ * The number of leading one's
+ */
+ def leadingOnes(l: BigNum) : BigInt = {
+ l match {
+ case Nil() => 1
+ case Cons(Zero(), tail) => 1
+ case Cons(_, tail) => 1 + leadingOnes(tail)
+ }
+ }
+
+ /**
+ * Total number of one's in the number
+ */
+ def numOnes(l: BigNum) : BigInt = {
+ l match {
+ case Nil() => 0
+ case Cons(Zero(), tail) => numOnes(tail)
+ case Cons(_, tail) => 1 + numOnes(tail)
+ }
+ }
+
+ /**
+ * Increments a number
+ */
+ def increment(l: BigNum) : BigNum = {
+ l match {
+ case Nil() => Cons(One(), l)
+ case Cons(Zero(), tail) => Cons(One(), tail)
+ case Cons(_, tail) =>
+ Cons(Zero(), increment(tail))
+ }
+ } ensuring (res => time <= ? * leadingOnes(l) + ? && leadingOnes(l) + numOnes(res) - numOnes(l) <= ?)
+
+ def firstDigit(l: BigNum): Digit = {
+ require(l != Nil())
+ l match {
+ case Cons(d, _) => d
+ }
+ }
+
+ /**
+ * Nop is the number of operations
+ */
+ def incrUntil(nop: BigInt, l: BigNum) : BigNum = {
+ if(nop == 0) l
+ else {
+ incrUntil(nop-1, increment(l))
+ }
+ } ensuring (res => time <= ? * nop + ? * numOnes(l) + ?)
+
+ def count(nop: BigInt) : BigNum = {
+ incrUntil(nop, Nil())
+ } ensuring (res => time <= ? * nop + ?)
+
+}
diff --git a/testcases/lazy-datastructures/lib/lazybenchmarkexecution_2.11-1.0.jar b/testcases/lazy-datastructures/lib/lazybenchmarkexecution_2.11-1.0.jar
new file mode 100644
index 0000000000000000000000000000000000000000..784f4db57ac44a6c8e78d491fe8280d5866b0663
Binary files /dev/null and b/testcases/lazy-datastructures/lib/lazybenchmarkexecution_2.11-1.0.jar differ
diff --git a/testcases/lazy-datastructures/lib/macmemo.jar b/testcases/lazy-datastructures/lib/macmemo.jar
new file mode 100644
index 0000000000000000000000000000000000000000..eacd3c002133ad6486d2c89eb63722ab088d2a6c
Binary files /dev/null and b/testcases/lazy-datastructures/lib/macmemo.jar differ
diff --git a/testcases/lazy-datastructures/memoization/FibonacciMemoized.scala b/testcases/lazy-datastructures/memoization/FibonacciMemoized.scala
index 77ef3233b600aaad91caef47838d27b67ecc2bbb..2780315c17ae7844e34a6b8a1be827d371f99578 100644
--- a/testcases/lazy-datastructures/memoization/FibonacciMemoized.scala
+++ b/testcases/lazy-datastructures/memoization/FibonacciMemoized.scala
@@ -1,8 +1,8 @@
-import leon.lazyeval._
-import leon.lazyeval.Mem._
-import leon.lang._
-import leon.annotation._
-import leon.instrumentation._
+import leon._
+import mem._
+import lang._
+import annotation._
+import instrumentation._
//import leon.invariant._
object FibMem {
diff --git a/testcases/lazy-datastructures/memoization/HammingMemoized.scala b/testcases/lazy-datastructures/memoization/HammingMemoized.scala
index 9c4ae4a0b875ac1cb8152b93e20d1b2830b329db..36f606b93437055f7bae7c7908f30cba9cee88d7 100644
--- a/testcases/lazy-datastructures/memoization/HammingMemoized.scala
+++ b/testcases/lazy-datastructures/memoization/HammingMemoized.scala
@@ -1,8 +1,9 @@
-import leon.lazyeval._
-import leon.lazyeval.Mem._
-import leon.lang._
-import leon.annotation._
-import leon.instrumentation._
+import leon._
+
+import mem._
+import lang._
+import annotation._
+import instrumentation._
/**
* A memoized version of the implementation of Hamming problem shown in
@@ -54,8 +55,8 @@ object Hamming {
require(n == 0 || n > 0 && depsEval(n - 1))
ham(n).v
} ensuring (res => {
- val in = Mem.inState[Data]
- val out = Mem.outState[Data]
+ val in = inState[Data]
+ val out = outState[Data]
(n == 0 || depsEvalMono(n-1, in, out)) && // instantiation
time <= 170
})
diff --git a/testcases/lazy-datastructures/memoization/Knapsack.scala b/testcases/lazy-datastructures/memoization/Knapsack.scala
index fc67c5b03657f048e06f1fc9ea89f5921eec89e1..44eadad05a0de6edba94c8796d668748cc0aaf49 100644
--- a/testcases/lazy-datastructures/memoization/Knapsack.scala
+++ b/testcases/lazy-datastructures/memoization/Knapsack.scala
@@ -1,8 +1,7 @@
-import leon.lazyeval._
-import leon.lazyeval.Mem._
-import leon.lang._
-import leon.annotation._
-import leon.instrumentation._
+import leon._
+import mem._
+import annotation._
+import instrumentation._
//import leon.invariant._
object Knapscak {
@@ -76,7 +75,7 @@ object Knapscak {
else {
Cons((i,ri), bottomup(i + 1, w, items))
}
- } ensuring(items.size <= 10 ==> time <= 500 * (w - i + 1))
+ } ensuring(_ => items.size <= 10 ==> time <= 500 * (w - i + 1))
/**
* Computes the list of optimal solutions of all weights up to 'w'
@@ -84,7 +83,7 @@ object Knapscak {
def knapSackSol(w: BigInt, items: IList) = {
require(w >= 0 && items.size <= 10) // the second requirement is only to keep the bounds linear for z3 to work
bottomup(0, w, items)
- } ensuring(time <= 500*w + 510)
+ } ensuring(_ => time <= 500*w + 510)
/**
* Lemmas of deps
diff --git a/testcases/lazy-datastructures/memoization/PackratParsing.scala b/testcases/lazy-datastructures/memoization/PackratParsing.scala
index f4feed46bcc41801d3ceaf4bb938fd55606500e2..b1b5f175b1162f80d05bb394cad39ce075feb4d7 100644
--- a/testcases/lazy-datastructures/memoization/PackratParsing.scala
+++ b/testcases/lazy-datastructures/memoization/PackratParsing.scala
@@ -1,5 +1,5 @@
-import leon.lazyeval._
-import leon.lazyeval.Mem._
+import leon._
+import leon.mem._
import leon.lang._
import leon.annotation._
import leon.instrumentation._
@@ -33,7 +33,6 @@ object PackratParsing {
string(i.toInt)
} ensuring(_ => time <= 1)
-
sealed abstract class Result {
/**
* Checks if the index in the result (if any) is
@@ -51,47 +50,52 @@ object PackratParsing {
@memoize
@invstate
def pAdd(i: BigInt): Result = {
- require(depsEval(i) &&
- pMul(i).isCached && pPrim(i).isCached &&
- resEval(i, pMul(i))) // lemma inst
-
+ require {
+ if (depsEval(i) && pMul(i).isCached && pPrim(i).isCached)
+ resEval(i, pMul(i))
+ else false
+ } // lemma inst
// Rule 1: Add <- Mul + Add
- pMul(i) match {
+ val v = pMul(i)
+ v match {
case Parsed(j) =>
if (j > 0 && lookup(j) == Plus()) {
pAdd(j - 1) match {
case Parsed(rem) =>
Parsed(rem)
case _ =>
- pMul(i) // Rule2: Add <- Mul
+ v // Rule2: Add <- Mul
}
- } else pMul(i)
+ } else v
case _ =>
- pMul(i)
+ v
}
- } ensuring (res => res.smallerIndex(i) && time <= 40)
+ } ensuring (res => res.smallerIndex(i) && time <= 26)
@memoize
@invstate
def pMul(i: BigInt): Result = {
- require(depsEval(i) && pPrim(i).isCached &&
- resEval(i, pPrim(i)) // lemma inst
- )
+ require {
+ if (depsEval(i) && pPrim(i).isCached)
+ resEval(i, pPrim(i)) // lemma inst
+ else false
+ }
// Rule 1: Mul <- Prim * Mul
- pPrim(i) match {
+ val v = pPrim(i)
+ v match {
case Parsed(j) =>
if (j > 0 && lookup(j) == Plus()) {
pMul(j - 1) match {
case Parsed(rem) =>
Parsed(rem)
case _ =>
- pPrim(i) // Rule2: Mul <- Prim
+ v // Rule2: Mul <- Prim
}
- } else pPrim(i)
+ } else v
case _ =>
- pPrim(i)
+ v
}
- } ensuring (res => res.smallerIndex(i) && time <= 40)
+ } ensuring (res => res.smallerIndex(i) && time <= 26)
@memoize
@invstate
@@ -106,14 +110,15 @@ object PackratParsing {
} else if (char == Open() && i > 0) {
pAdd(i - 1) match { // Rule 2: pPrim <- ( Add )
case Parsed(rem) =>
- Parsed(rem)
+ if (rem >= 0 && lookup(rem) == Close()) Parsed(rem - 1)
+ else NoParse()
case _ =>
NoParse()
}
} else NoParse()
- } ensuring (res => res.smallerIndex(i) && time <= 30)
+ } ensuring (res => res.smallerIndex(i) && time <= 28)
- @inline
+ //@inline
def depsEval(i: BigInt) = i == 0 || (i > 0 && allEval(i-1))
def allEval(i: BigInt): Boolean = {
@@ -138,7 +143,6 @@ object PackratParsing {
/**
* Instantiates the lemma `depsLem` on the result index (if any)
*/
- @inline
def resEval(i: BigInt, res: Result) = {
(res match {
case Parsed(j) =>
@@ -148,16 +152,38 @@ object PackratParsing {
})
}
- def invoke(i: BigInt): (Result, Result, Result) = {
- require(i == 0 || (i > 0 && allEval(i-1)))
- (pPrim(i), pMul(i), pAdd(i))
- } ensuring (res => {
- val in = Mem.inState[Result]
- val out = Mem.outState[Result]
+ def invokePrim(i: BigInt): Result = {
+ require(depsEval(i))
+ pPrim(i)
+ } ensuring {res =>
+ val in = inState[Result]
+ val out = outState[Result]
+ (if(i >0) evalMono(i-1, in, out) else true)
+ }
+
+ def invokeMul(i: BigInt): Result = {
+ require(depsEval(i))
+ invokePrim(i) match {
+ case _ => pMul(i)
+ }
+ } ensuring {res =>
+ val in = inState[Result]
+ val out = outState[Result]
+ (if(i >0) evalMono(i-1, in, out) else true)
+ }
+
+ def invoke(i: BigInt): Result = {
+ require(depsEval(i))
+ invokeMul(i) match {
+ case _ => pAdd(i)
+ }
+ } ensuring{ res =>
+ val in = inState[Result]
+ val out = outState[Result]
(if(i >0) evalMono(i-1, in, out) else true) &&
allEval(i) &&
- time <= 200
- })
+ time <= 189
+ }
/**
* Parsing a string of length 'n+1'.
@@ -166,11 +192,12 @@ object PackratParsing {
*/
def parse(n: BigInt): Result = {
require(n >= 0)
- if(n == 0) invoke(n)._3
+ if(n == 0) invoke(n)
else {
- val tailres = parse(n-1) // we parse the prefixes ending at 0, 1, 2, 3, ..., n
- invoke(n)._3
+ parse(n-1) match { // we parse the prefixes ending at 0, 1, 2, 3, ..., n
+ case _ => invoke(n)
+ }
}
} ensuring(_ => allEval(n) &&
- time <= 250*n + 250)
+ time <= 198*n + 192)
}
diff --git a/testcases/lazy-datastructures/memoization/WeightedScheduling.scala b/testcases/lazy-datastructures/memoization/WeightedScheduling.scala
index cf2fa7508ef1f3ffa9fe686a18278c3a270ef925..e640bd79e7fa7950e5b3dd01389c4bd84f734045 100644
--- a/testcases/lazy-datastructures/memoization/WeightedScheduling.scala
+++ b/testcases/lazy-datastructures/memoization/WeightedScheduling.scala
@@ -1,5 +1,5 @@
-import leon.lazyeval._
-import leon.lazyeval.Mem._
+import leon._
+import leon.mem._
import leon.lang._
import leon.annotation._
import leon.instrumentation._
@@ -69,7 +69,7 @@ object WeightedSched {
@memoize
def sched(jobIndex: BigInt): BigInt = {
require(depsEval(jobIndex) &&
- (jobIndex == 0 || prevCompatibleJob(jobIndex) >= 0)) //evalLem(prevCompatibleJob(jobIndex), jobIndex-1)))
+ (jobIndex == 0 || evalLem(prevCompatibleJob(jobIndex), jobIndex-1)))
val (st, fn, w) = jobInfo(jobIndex)
if(jobIndex == 0) w
else {
@@ -85,8 +85,8 @@ object WeightedSched {
require(depsEval(jobIndex))
sched(jobIndex)
} ensuring (res => {
- val in = Mem.inState[BigInt]
- val out = Mem.outState[BigInt]
+ val in = inState[BigInt]
+ val out = outState[BigInt]
(jobIndex == 0 || evalMono(jobIndex-1, in, out)) &&
time <= 150
})
diff --git a/testcases/lazy-datastructures/project/Build.scala b/testcases/lazy-datastructures/project/Build.scala
new file mode 100644
index 0000000000000000000000000000000000000000..4d96b683b440afe56a993d3790105a0092410165
--- /dev/null
+++ b/testcases/lazy-datastructures/project/Build.scala
@@ -0,0 +1,21 @@
+import sbt._
+import Keys._
+
+object BuildSettings {
+ val paradiseVersion = "2.1.0-M5"
+ val buildSettings = Defaults.defaultSettings ++ Seq(
+ resolvers += Resolver.sonatypeRepo("snapshots"),
+ resolvers += Resolver.sonatypeRepo("releases"),
+ addCompilerPlugin("org.scalamacros" % "paradise" % paradiseVersion cross CrossVersion.full)
+ )
+}
+
+object MyBuild extends Build {
+ import BuildSettings._
+
+ lazy val root = Project(
+ "root",
+ file("."),
+ settings = buildSettings
+ )
+}
diff --git a/testcases/lazy-datastructures/withOrb/BottomUpMegeSort.scala b/testcases/lazy-datastructures/withOrb/BottomUpMegeSort.scala
index 10a0047cf2813906ad084be22253b656d6fed512..71179a087cffb9fe6c2a465d5884953a2432725e 100644
--- a/testcases/lazy-datastructures/withOrb/BottomUpMegeSort.scala
+++ b/testcases/lazy-datastructures/withOrb/BottomUpMegeSort.scala
@@ -1,11 +1,12 @@
-package orb
+package withOrb
-import leon.lazyeval._
-import leon.lazyeval.$._
-import leon.lang._
-import leon.annotation._
-import leon.instrumentation._
-import leon.invariant._
+import leon._
+import lazyeval._
+import lang._
+import annotation._
+import instrumentation._
+import invariant._
+import stats._
/**
* TODO Multiple instantiations of type parameters is not supported yet,
@@ -43,10 +44,10 @@ object BottomUpMergeSort {
}
} ensuring (_ >= 0)
}
- case class SCons(x: BigInt, tail: $[IStream]) extends IStream
+ case class SCons(x: BigInt, tail: Lazy[IStream]) extends IStream
case class SNil() extends IStream
@inline
- def ssize(l: $[IStream]): BigInt = (l*).size
+ def ssize(l: Lazy[IStream]): BigInt = (l*).size
/**
* A list of suspensions
@@ -73,7 +74,7 @@ object BottomUpMergeSort {
}
} ensuring (_ >= 0)
}
- case class LCons(x: $[IStream], tail: LList) extends LList
+ case class LCons(x: Lazy[IStream], tail: LList) extends LList
case class LNil() extends LList
/**
@@ -109,14 +110,15 @@ object BottomUpMergeSort {
case _ =>
constructMergeTree(pairs(l))
}
- } ensuring (res => res.size <= 1 && res.fullSize == l.fullSize &&
+ } ensuring {res =>
+ res.size <= 1 && res.fullSize == l.fullSize &&
(res match {
case LCons(il, LNil()) =>
res.fullSize == ssize(il) // this is implied by the previous conditions
case _ => true
}) &&
res.valid &&
- time <= ? * l.size + ?)
+ time <= ? * l.size + ?}
/**
* A function that merges two sorted streams of integers.
@@ -125,7 +127,7 @@ object BottomUpMergeSort {
*/
@invisibleBody
@usePost
- def merge(a: $[IStream], b: $[IStream]): IStream = {
+ def merge(a: Lazy[IStream], b: Lazy[IStream]): IStream = {
require(((a*) != SNil() || b.isEvaluated) && // if one of the arguments is Nil then the other is evaluated
((b*) != SNil() || a.isEvaluated) &&
((a*) != SNil() || (b*) != SNil())) // at least one of the arguments is not Nil
@@ -142,22 +144,27 @@ object BottomUpMergeSort {
}
}
} ensuring (res => ssize(a) + ssize(b) == res.size &&
- time <= ? * res.size + ?) // note: res.size >= 1 // here stack is max of a and b
+ //time <= ? * res.size + ?) // note: res.size >= 1 // here stack is max of a and b
+ time <= 67 * res.size - 47) // Orb cannot infer this due to issues with CVC4 set solving !
/**
* Converts a list of integers to a list of streams of integers
*/
+ val nilStream: IStream = SNil()
+
@invisibleBody
def IListToLList(l: IList): LList = {
l match {
case INil() => LNil()
case ICons(x, xs) =>
- LCons(SCons(x, SNil()), IListToLList(xs))
+ LCons(SCons(x, nilStream), IListToLList(xs))
}
- } ensuring (res => res.fullSize == l.size &&
- res.size == l.size &&
- res.valid &&
- time <= ? * l.size + ?)
+ } ensuring { res =>
+ res.fullSize == l.size &&
+ res.size == l.size &&
+ res.valid &&
+ time <= ? * l.size + ?
+ }
/**
* Takes list of integers and returns a sorted stream of integers.
@@ -182,4 +189,50 @@ object BottomUpMergeSort {
case SCons(x, rest) => x
}
} ensuring (res => time <= ? * l.size + ?)
+
+ def kthMin(l: IStream, k: BigInt): BigInt = {
+ require(k >= 0)
+ l match {
+ case SCons(x, xs) =>
+ if (k == 0) x
+ else
+ kthMin(xs.value, k - 1)
+ case SNil() => BigInt(0)
+ }
+ } //ensuring (_ => time <= ? * (k * ssize(l)) + ? * k + ?)
+
+ @ignore
+ def main(args: Array[String]) {
+ //import eagerEval.MergeSort
+ import scala.util.Random
+ import scala.math.BigInt
+ import stats._
+ import collection._
+
+ println("Running merge sort test...")
+ val length = 3000000
+ val maxIndexValue = 100
+ val randomList = Random.shuffle((0 until length).toList)
+ val l1 = randomList.foldRight(List[BigInt]()){
+ case (i, acc) => BigInt(i) :: acc
+ }
+ val l2 = randomList.foldRight(INil(): IList){
+ case (i, acc) => ICons(BigInt(i), acc)
+ }
+ println(s"Created inputs of size (${l1.size},${l2.size}), starting operations...")
+ val sort2 = timed{ mergeSort(l2) }{t => println(s"Lazy merge sort completed in ${t/1000.0} sec") }
+ //val sort1 = timed{ MergeSort.msort((x: BigInt, y: BigInt) => x <= y)(l1) } {t => println(s"Eager merge sort completed in ${t/1000.0} sec") }
+ // sample 10 elements from a space of [0-100]
+ val rand = Random
+ var totalTime1 = 0L
+ var totalTime2 = 0L
+ for(i <- 0 until 10) {
+ val idx = rand.nextInt(maxIndexValue)
+ //val e1 = timed { sort1(idx) } { totalTime1 +=_ }
+ val e2 = timed { kthMin(sort2, idx) }{ totalTime2 += _ }
+ //println(s"Element at index $idx - Eager: $e1 Lazy: $e2")
+ //assert(e1 == e2)
+ }
+ println(s"Time-taken to pick first 10 minimum elements - Eager: ${totalTime1/1000.0}s Lazy: ${totalTime2/1000.0}s")
+ }
}
diff --git a/testcases/lazy-datastructures/withOrb/Concat.scala b/testcases/lazy-datastructures/withOrb/Concat.scala
index bd4978f6a4c6145470a3fd2983e8a4e27420a20c..b9653b5224a19298684e39bb6e3de401815cb40b 100644
--- a/testcases/lazy-datastructures/withOrb/Concat.scala
+++ b/testcases/lazy-datastructures/withOrb/Concat.scala
@@ -1,11 +1,13 @@
package withOrb
-import leon.lazyeval._
-import leon.lang._
-import leon.annotation._
-import leon.instrumentation._
-import leon.collection._
-import leon.invariant._
+import leon._
+import lazyeval._
+import lazyeval.Lazy._
+import lang._
+import annotation._
+import instrumentation._
+import collection._
+import invariant._
object Concat {
sealed abstract class LList[T] {
@@ -16,30 +18,60 @@ object Concat {
}
} ensuring (_ >= 0)
}
- case class SCons[T](x: T, tail: $[LList[T]]) extends LList[T]
+ case class SCons[T](x: T, tail: Lazy[LList[T]]) extends LList[T]
case class SNil[T]() extends LList[T]
- def ssize[T](l: $[LList[T]]): BigInt = (l*).size
+ def ssize[T](l: Lazy[LList[T]]): BigInt = (l*).size
- def concat[T](l1: List[T], l2: List[T]) : LList[T] = {
+ def concat[T](l1: List[T], l2: List[T]): LList[T] = {
l1 match {
case Cons(x, xs) => SCons(x, $(concat(xs, l2)))
- case Nil() => SNil[T]()
+ case Nil() => SNil[T]()
}
- } ensuring(_ => time <= ?)
+ } ensuring { _ => time <= ? }
- def kthElem[T](l: $[LList[T]], k: BigInt): Option[T] = {
- require(k >= 1)
+ def kthElem[T](l: Lazy[LList[T]], k: BigInt): Option[T] = {
+ require(k >= 0)
l.value match {
case SCons(x, xs) =>
- if (k == 1) Some(x)
+ if (k == 0) Some(x)
else
kthElem(xs, k - 1)
case SNil() => None[T]
}
- } ensuring (_ => time <= ? * k)
+ } ensuring (_ => time <= ? * k + ?)
- def concatnSelect[T](l1: List[T], l2: List[T], k: BigInt) : Option[T] = {
- require(k >= 1)
+ def concatnSelect[T](l1: List[T], l2: List[T], k: BigInt): Option[T] = {
+ require(k >= 0)
kthElem($(concat(l1, l2)), k)
- } ensuring (_ => time <= ? * k)
+ } ensuring (_ => time <= ? * k + ?)
+
+ @ignore
+ def main(args: Array[String]) = {
+ import stats._
+ println("Running concat test...")
+ val length = 1000000
+ val k = 10
+ val iterCount = 10
+ val l1 = (0 until length).foldRight(List[BigInt]()) {
+ case (i, acc) => i :: acc
+ }
+ val l2 = (0 until length).foldRight(List[BigInt]()) {
+ case (i, acc) => 2 * i :: acc
+ }
+ println("Created inputs, starting operations...")
+ def iterate[T](op: => BigInt) = {
+ var res = BigInt(0)
+ var i = iterCount
+ while (i > 0) {
+ res = op
+ i -= 1
+ }
+ res
+ }
+ val elem1 = timed { iterate((l1 ++ l2)(k)) } { t => println(s"Eager Concat completed in ${t / 1000.0} sec") }
+ println(s"$k th element of concatenated list: $elem1")
+ val elem2 = timed { iterate(concatnSelect(l1, l2, k).get) } { t => println(s"Lazy ConcatnSelect completed in ${t / 1000.0} sec") }
+ println(s"$k th element of concatenated list: $elem2")
+ assert(elem1 == elem2)
+ }
}
diff --git a/testcases/lazy-datastructures/withOrb/Deque.scala b/testcases/lazy-datastructures/withOrb/Deque.scala
index 6493eb8c8b2bef8b3955c31c71c8ffe4eedfb6f2..38daf01442f4b12d9b7c39f4e6abf8f3e677186a 100644
--- a/testcases/lazy-datastructures/withOrb/Deque.scala
+++ b/testcases/lazy-datastructures/withOrb/Deque.scala
@@ -1,13 +1,13 @@
-package orb
+package withOrb
-import leon.lazyeval._
-import leon.lazyeval.$._
-import leon.lang._
-import leon.annotation._
-import leon.collection._
-import leon.instrumentation._
-import leon.math._
-import leon.invariant._
+import leon._
+import lazyeval._
+import lang._
+import annotation._
+import collection._
+import instrumentation._
+import math._
+import invariant._
/**
* A constant time deque based on Okasaki's implementation: Fig.8.4 Pg. 112.
@@ -43,13 +43,13 @@ object RealTimeDeque {
}
} ensuring (_ >= 0)
}
- case class SCons[T](x: T, tail: $[Stream[T]]) extends Stream[T]
+ case class SCons[T](x: T, tail: Lazy[Stream[T]]) extends Stream[T]
case class SNil[T]() extends Stream[T]
@inline
- def ssize[T](l: $[Stream[T]]): BigInt = (l*).size
+ def ssize[T](l: Lazy[Stream[T]]): BigInt = (l*).size
- def isConcrete[T](l: $[Stream[T]]): Boolean = {
+ def isConcrete[T](l: Lazy[Stream[T]]): Boolean = {
l.isEvaluated && (l* match {
case SCons(_, tail) =>
isConcrete(tail)
@@ -58,12 +58,25 @@ object RealTimeDeque {
}
@invstate
- def revAppend[T](l1: $[Stream[T]], l2: $[Stream[T]]): $[Stream[T]] = {
+ def takeLazy[T](n: BigInt, l: Lazy[Stream[T]]): Stream[T] = {
+ require(isConcrete(l) && n >= 1 && ssize(l) >= n)
+ l.value match {
+ case SCons(x, tail) =>
+ if (n == 1)
+ SCons[T](x, SNil[T]())
+ else
+ SCons[T](x, $(takeLazy(n - 1, tail)))
+ }
+ } ensuring(res => res.size == n && res.isCons &&
+ time <= ?)
+
+ @invstate
+ def revAppend[T](l1: Lazy[Stream[T]], l2: Lazy[Stream[T]]): Lazy[Stream[T]] = {
require(isConcrete(l1) && isConcrete(l2))
l1.value match {
case SNil() => l2
case SCons(x, tail) =>
- val nt: $[Stream[T]] = SCons[T](x, l2)
+ val nt: Lazy[Stream[T]] = SCons[T](x, l2)
revAppend(tail, nt)
}
} ensuring(res => ssize(res) == ssize(l1) + ssize(l2) &&
@@ -72,7 +85,7 @@ object RealTimeDeque {
time <= ? * ssize(l1) + ?)
@invstate
- def drop[T](n: BigInt, l: $[Stream[T]]): $[Stream[T]] = {
+ def drop[T](n: BigInt, l: Lazy[Stream[T]]): Lazy[Stream[T]] = {
require(n >= 0 && isConcrete(l) && ssize(l) >= n)
if (n == 0) {
l
@@ -87,9 +100,9 @@ object RealTimeDeque {
time <= ? * n + ?)
@invstate
- def take[T](n: BigInt, l: $[Stream[T]]): $[Stream[T]] = {
+ def take[T](n: BigInt, l: Lazy[Stream[T]]): Lazy[Stream[T]] = {
require(n >= 0 && isConcrete(l) && ssize(l) >= n)
- val r: $[Stream[T]] =
+ val r: Lazy[Stream[T]] =
if (n == 0) {
SNil[T]()
} else {
@@ -105,20 +118,7 @@ object RealTimeDeque {
time <= ? * n + ?)
@invstate
- def takeLazy[T](n: BigInt, l: $[Stream[T]]): Stream[T] = {
- require(isConcrete(l) && n >= 1 && ssize(l) >= n)
- l.value match {
- case SCons(x, tail) =>
- if (n == 1)
- SCons[T](x, SNil[T]())
- else
- SCons[T](x, $(takeLazy(n - 1, tail)))
- }
- } ensuring(res => res.size == n && res.isCons &&
- time <= ?)
-
- @invstate
- def rotateRev[T](r: $[Stream[T]], f: $[Stream[T]], a: $[Stream[T]]): Stream[T] = {
+ def rotateRev[T](r: Lazy[Stream[T]], f: Lazy[Stream[T]], a: Lazy[Stream[T]]): Stream[T] = {
require(isConcrete(r) && isConcrete(f) && isConcrete(a) &&
{
val lenf = ssize(f)
@@ -135,7 +135,7 @@ object RealTimeDeque {
time <= ?)
@invstate
- def rotateDrop[T](r: $[Stream[T]], i: BigInt, f: $[Stream[T]]): Stream[T] = {
+ def rotateDrop[T](r: Lazy[Stream[T]], i: BigInt, f: Lazy[Stream[T]]): Stream[T] = {
require(isConcrete(r) && isConcrete(f) && i >= 0 && {
val lenf = ssize(f)
val lenr = ssize(r)
@@ -144,7 +144,7 @@ object RealTimeDeque {
})
val rval = r.value
if(i < 2 || rval == SNil[T]()) { // A bug in Okasaki implementation: we must check for: 'rval = SNil()'
- val a: $[Stream[T]] = SNil[T]()
+ val a: Lazy[Stream[T]] = SNil[T]()
rotateRev(r, drop(i, f), a)
} else {
rval match {
@@ -155,7 +155,7 @@ object RealTimeDeque {
} ensuring(res => res.size == (r*).size + (f*).size - i &&
res.isCons && time <= ?)
- def firstUneval[T](l: $[Stream[T]]): $[Stream[T]] = {
+ def firstUneval[T](l: Lazy[Stream[T]]): Lazy[Stream[T]] = {
if (l.isEvaluated) {
l* match {
case SCons(_, tail) =>
@@ -172,8 +172,8 @@ object RealTimeDeque {
case _ => true
}))
- case class Queue[T](f: $[Stream[T]], lenf: BigInt, sf: $[Stream[T]],
- r: $[Stream[T]], lenr: BigInt, sr: $[Stream[T]]) {
+ case class Queue[T](f: Lazy[Stream[T]], lenf: BigInt, sf: Lazy[Stream[T]],
+ r: Lazy[Stream[T]], lenr: BigInt, sr: Lazy[Stream[T]]) {
def isEmpty = lenf + lenr == 0
def valid = {
(firstUneval(f) == firstUneval(sf)) &&
@@ -192,8 +192,8 @@ object RealTimeDeque {
* the balance invariant, and restores the balance.
*/
@invisibleBody
- def createQueue[T](f: $[Stream[T]], lenf: BigInt, sf: $[Stream[T]],
- r: $[Stream[T]], lenr: BigInt, sr: $[Stream[T]]): Queue[T] = {
+ def createQueue[T](f: Lazy[Stream[T]], lenf: BigInt, sf: Lazy[Stream[T]],
+ r: Lazy[Stream[T]], lenr: BigInt, sr: Lazy[Stream[T]]): Queue[T] = {
require(firstUneval(f) == firstUneval(sf) &&
firstUneval(r) == firstUneval(sr) &&
(lenf == ssize(f) && lenr == ssize(r)) &&
@@ -220,15 +220,14 @@ object RealTimeDeque {
} ensuring(res => res.valid &&
time <= ?)
-
@invisibleBody
- def funeEqual[T](s1: $[Stream[T]], s2: $[Stream[T]]) = firstUneval(s1) == firstUneval(s2)
-
+ def funeEqual[T](s1: Lazy[Stream[T]], s2: Lazy[Stream[T]]) = firstUneval(s1) == firstUneval(s2)
+
/**
* Forces the schedules, and ensures that `firstUneval` equality is preserved
*/
@invisibleBody
- def force[T](tar: $[Stream[T]], htar: $[Stream[T]], other: $[Stream[T]], hother: $[Stream[T]]): $[Stream[T]] = {
+ def force[T](tar: Lazy[Stream[T]], htar: Lazy[Stream[T]], other: Lazy[Stream[T]], hother: Lazy[Stream[T]]): Lazy[Stream[T]] = {
require(funeEqual(tar, htar) && funeEqual(other, hother))
tar.value match {
case SCons(_, tail) => tail
@@ -236,8 +235,8 @@ object RealTimeDeque {
}
} ensuring (res => {
//lemma instantiations
- val in = $.inState[Stream[T]]
- val out = $.outState[Stream[T]]
+ val in = inState[Stream[T]]
+ val out = outState[Stream[T]]
funeMonotone(tar, htar, in, out) &&
funeMonotone(other, hother, in, out) && {
//properties
@@ -252,12 +251,12 @@ object RealTimeDeque {
* Forces the schedules in the queue twice and ensures the `firstUneval` property.
*/
@invisibleBody
- def forceTwice[T](q: Queue[T]): ($[Stream[T]], $[Stream[T]]) = {
+ def forceTwice[T](q: Queue[T]): (Lazy[Stream[T]], Lazy[Stream[T]]) = {
require(q.valid)
val nsf = force(force(q.sf, q.f, q.r, q.sr), q.f, q.r, q.sr) // forces q.sf twice
val nsr = force(force(q.sr, q.r, q.f, nsf), q.r, q.f, nsf) // forces q.sr twice
(nsf, nsr)
- } ensuring(time <= ?)
+ } ensuring(_ => time <= ?)
// the following properties are ensured, but need not be stated
/*ensuring (res => {
val nsf = res._1
@@ -270,10 +269,18 @@ object RealTimeDeque {
})*/
def empty[T] = {
- val nil: $[Stream[T]] = SNil[T]()
+ val nil: Lazy[Stream[T]] = SNil[T]()
Queue(nil, 0, nil, nil, 0, nil)
}
+ def head[T](q: Queue[T]): T = {
+ require(!q.isEmpty && q.valid)
+ (q.f.value, q.r.value) match {
+ case (SCons(x, _), _) => x
+ case (_, SCons(x, _)) => x
+ }
+ }
+
/**
* Adding an element to the front of the list
*/
@@ -317,14 +324,19 @@ object RealTimeDeque {
def reverse[T](q: Queue[T]): Queue[T] = {
require(q.valid)
Queue(q.r, q.lenr, q.sr, q.f, q.lenf, q.sf)
- } ensuring(q.valid && time <= ?)
+ } ensuring(_ => q.valid && time <= ?)
+
+ def snoc[T](x: T, q: Queue[T]): Queue[T] = {
+ require(q.valid)
+ reverse(cons(x, reverse(q)))
+ }
// Properties of `firstUneval`. We use `fune` as a shorthand for `firstUneval`
/**
* st1.subsetOf(st2) ==> fune(l, st2) == fune(fune(l, st1), st2)
*/
@traceInduct
- def funeCompose[T](l1: $[Stream[T]], st1: Set[$[Stream[T]]], st2: Set[$[Stream[T]]]): Boolean = {
+ def funeCompose[T](l1: Lazy[Stream[T]], st1: Set[Lazy[Stream[T]]], st2: Set[Lazy[Stream[T]]]): Boolean = {
require(st1.subsetOf(st2))
// property
(firstUneval(l1) withState st2) == (firstUneval(firstUneval(l1) withState st1) withState st2)
@@ -336,7 +348,7 @@ object RealTimeDeque {
* This is a kind of frame axiom for `fune` but is slightly different in that
* it doesn't require (st2 \ st1) to be disjoint from la and lb.
*/
- def funeMonotone[T](l1: $[Stream[T]], l2: $[Stream[T]], st1: Set[$[Stream[T]]], st2: Set[$[Stream[T]]]): Boolean = {
+ def funeMonotone[T](l1: Lazy[Stream[T]], l2: Lazy[Stream[T]], st1: Set[Lazy[Stream[T]]], st2: Set[Lazy[Stream[T]]]): Boolean = {
require((firstUneval(l1) withState st1) == (firstUneval(l2) withState st1) &&
st1.subsetOf(st2))
funeCompose(l1, st1, st2) && // lemma instantiations
@@ -351,4 +363,49 @@ object RealTimeDeque {
} else true) &&
(firstUneval(l1) withState st2) == (firstUneval(l2) withState st2) // property
} holds
+
+ @ignore
+ def main(args: Array[String]) {
+ //import eagerEval.AmortizedQueue
+ import scala.util.Random
+ import scala.math.BigInt
+ import stats._
+ import collection._
+
+ println("Running Deque test...")
+ val ops = 2000000
+ val rand = Random
+ // initialize to a queue with one element (required to satisfy preconditions of dequeue and front)
+ var rtd = empty[BigInt]
+ //var amq = AmortizedQueue.Queue(AmortizedQueue.Nil(), AmortizedQueue.Nil())
+ var totalTime1 = 0L
+ var totalTime2 = 0L
+ println(s"Testing amortized emphemeral behavior on $ops operations...")
+ for (i <- 0 until ops) {
+ if (!rtd.isEmpty) {
+ val h1 = head(rtd)
+ //val h2 = amq.head
+ //assert(h1 == h2, s"Eager head: $h2 Lazy head: $h1")
+ }
+ rand.nextInt(3) match {
+ case x if x == 0 => //add to rear
+ //println("Enqueue..")
+ rtd = timed { snoc(BigInt(i), rtd) } { totalTime1 += _ }
+ //amq = timed { amq.enqueue(BigInt(i)) } { totalTime2 += _ }
+ case x if x == 1 => // remove from front
+ if (!rtd.isEmpty) {
+ //if(i%100000 == 0)
+ //println("Dequeue..")
+ rtd = timed { tail(rtd) } { totalTime1 += _ }
+ //amq = timed { amq.dequeue } { totalTime2 += _ }
+ }
+ case x if x == 2 => // reverse
+ //if(i%100000 == 0)
+ //println("reverse..")
+ rtd = timed { reverse(rtd) } { totalTime1 += _ }
+ //amq = timed { amq.reverse } { totalTime2 += _ }
+ }
+ }
+ println(s"Ephemeral Amortized Time - Eager: ${totalTime2/1000.0}s Lazy: ${totalTime1/1000.0}s")
+ }
}
diff --git a/testcases/lazy-datastructures/withOrb/Esop15Benchmarks.scala b/testcases/lazy-datastructures/withOrb/Esop15Benchmarks.scala
index ee381e608d9301725586dffe5c20e391920583bb..45d520dcf67579ddccb94c3f2d95278a16896e93 100644
--- a/testcases/lazy-datastructures/withOrb/Esop15Benchmarks.scala
+++ b/testcases/lazy-datastructures/withOrb/Esop15Benchmarks.scala
@@ -1,12 +1,12 @@
-package lazybenchmarks
+package withorb
-import leon.lazyeval._
-import leon.lang._
-import leon.annotation._
-import leon.instrumentation._
-import leon.lazyeval.$._
-import leon.collection._
-import leon.invariant._
+import leon._
+import lazyeval._
+import lang._
+import annotation._
+import instrumentation._
+import collection._
+import invariant._
/**
* This file is the collection of programs in the ESOP 2015 paper.
@@ -15,14 +15,14 @@ import leon.invariant._
*/
object Esop15Benchmarks {
sealed abstract class IStream
- case class SCons(x: BigInt, tail: $[IStream]) extends IStream
+ case class SCons(x: BigInt, tail: Lazy[IStream]) extends IStream
case class SNil() extends IStream
sealed abstract class StreamPairs
- case class PCons(pair: (BigInt, BigInt), tail: $[StreamPairs]) extends StreamPairs
+ case class PCons(pair: (BigInt, BigInt), tail: Lazy[StreamPairs]) extends StreamPairs
case class PNil() extends StreamPairs
- def zipWith(xs: $[IStream], ys: $[IStream]): StreamPairs = {
+ 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)))
@@ -44,7 +44,7 @@ object Esop15Benchmarks {
SCons(0, SCons(1, $(nextFib(0, 1, n))))
}
- def nthFib(n: BigInt, fs: $[IStream]): BigInt = {
+ def nthFib(n: BigInt, fs: Lazy[IStream]): BigInt = {
require(n >= 0)
fs.value match {
case SCons(x, tail) =>
diff --git a/testcases/lazy-datastructures/withOrb/FibonacciMemoized.scala b/testcases/lazy-datastructures/withOrb/FibonacciMemoized.scala
index 89ce222e49424eb2f609a15952801f6562a447be..db9db04212e5ee2dcd98ac37fd11b95ba4d3c9b1 100644
--- a/testcases/lazy-datastructures/withOrb/FibonacciMemoized.scala
+++ b/testcases/lazy-datastructures/withOrb/FibonacciMemoized.scala
@@ -1,11 +1,12 @@
-package orb
+package withOrb
-import leon.lazyeval._
-import leon.lazyeval.Mem._
-import leon.lang._
-import leon.annotation._
-import leon.instrumentation._
-import leon.invariant._
+import leon._
+import mem._
+import lang._
+import annotation._
+import instrumentation._
+import invariant._
+import Mem._
object FibMem {
sealed abstract class IList
@@ -15,11 +16,16 @@ object FibMem {
@memoize
def fibRec(n: BigInt): BigInt = {
require(n >= 0)
- if(n <= 2)
- BigInt(1)
- else
- fibRec(n-1) + fibRec(n-2) // postcondition implies that the second call would be cached
- } ensuring(_ =>
- (n <= 2 || (fibRec(n-1).isCached &&
- fibRec(n-2).isCached)) && time <= ? * n + ?)
+ if (n <= 2)
+ BigInt(1)
+ else
+ fibRec(n - 1) + fibRec(n - 2) // postcondition implies that the second call would be cached
+ } ensuring (_ =>
+ (n <= 2 || (fibRec(n - 1).isCached &&
+ fibRec(n - 2).isCached)) && time <= ? * n + ?)
+
+ @ignore
+ def main(args: Array[String]) {
+ println("32nd fibonnacci number: " + fibRec(50))
+ }
}
diff --git a/testcases/lazy-datastructures/withOrb/HammingMemoized.scala b/testcases/lazy-datastructures/withOrb/HammingMemoized.scala
index 4b214ed9045b7875d01c1d4b8b046e2aa11cb772..65192934bb0f87128e9e6a8c8e64d436cd9ecd62 100644
--- a/testcases/lazy-datastructures/withOrb/HammingMemoized.scala
+++ b/testcases/lazy-datastructures/withOrb/HammingMemoized.scala
@@ -1,11 +1,11 @@
-package orb
+package withOrb
-import leon.lazyeval._
-import leon.lazyeval.Mem._
-import leon.lang._
-import leon.annotation._
-import leon.instrumentation._
-import leon.invariant._
+import leon._
+import mem._
+import lang._
+import annotation._
+import instrumentation._
+import invariant._
/**
* A memoized version of the implementation of Hamming problem shown in
@@ -13,8 +13,17 @@ import leon.invariant._
*/
object Hamming {
sealed abstract class IList
- case class Cons(x: BigInt, tail: IList) extends IList
- case class Nil() extends IList
+ case class Cons(x: BigInt, tail: IList) extends IList {
+ @ignore
+ override def toString: String = {
+ if(tail == Nil()) x.toString
+ else x.toString + "," + tail.toString
+ }
+ }
+ case class Nil() extends IList {
+ @ignore
+ override def toString = ""
+ }
case class Data(v: BigInt, i2: BigInt, i3: BigInt, i5: BigInt)
@@ -25,9 +34,9 @@ object Hamming {
if(n == BigInt(0)) Data(1, 0, 0, 0)
else {
val Data(x, i2, i3, i5) = ham(n-1)
- val a = ham(i2).i2 * 2
- val b = ham(i3).i3 * 3
- val c = ham(i5).i5 * 5
+ val a = ham(i2).v * 2
+ val b = ham(i3).v * 3
+ val c = ham(i5).v * 5
val (v, ni, nj, nk) = threeWayMerge(a, b, c, i2, i3, i5)
Data(v, ni, nj, nk)
}
@@ -57,8 +66,8 @@ object Hamming {
require(n == 0 || n > 0 && depsEval(n - 1))
ham(n).v
} ensuring (res => {
- val in = Mem.inState[Data]
- val out = Mem.outState[Data]
+ val in = inState[Data]
+ val out =outState[Data]
(n == 0 || depsEvalMono(n-1, in, out)) && // instantiation
time <= ?
})
@@ -86,4 +95,11 @@ object Hamming {
else if(b < c && b < a) (b, i2 , i3 + 1, i5 )
else/*if(c < a && c < b)*/(c, i2 , i3 , i5 + 1)
}
+
+ @ignore
+ def main(args: Array[String]) {
+ import collection._
+ val hlist = hammingList(100) // without memoization this will take too long
+ println("Hamming numbers: "+hlist)
+ }
}
diff --git a/testcases/lazy-datastructures/withOrb/Knapsack.scala b/testcases/lazy-datastructures/withOrb/Knapsack.scala
index e1645b545160e455e7878e23e4ce1292ef018b9a..8eb64d369dbe2ef198508103d4790ae51c37ef3a 100644
--- a/testcases/lazy-datastructures/withOrb/Knapsack.scala
+++ b/testcases/lazy-datastructures/withOrb/Knapsack.scala
@@ -1,11 +1,11 @@
-package orb
+package wihtOrb
-import leon.lazyeval._
-import leon.lazyeval.Mem._
-import leon.lang._
-import leon.annotation._
-import leon.instrumentation._
-import leon.invariant._
+import leon._
+import mem._
+import lang._
+import annotation._
+import instrumentation._
+import invariant._
object Knapscak {
sealed abstract class IList {
@@ -16,8 +16,17 @@ object Knapscak {
}
} ensuring(_ >= 0)
}
- case class Cons(x: (BigInt, BigInt), tail: IList) extends IList // a list of pairs of weights and values
- case class Nil() extends IList
+ case class Cons(x: (BigInt, BigInt), tail: IList) extends IList { // a list of pairs of weights and values
+ @ignore
+ override def toString: String = {
+ if(tail == Nil()) x.toString
+ else x.toString + "," + tail.toString
+ }
+ }
+ case class Nil() extends IList {
+ @ignore
+ override def toString = ""
+ }
def deps(i: BigInt, items: IList): Boolean = {
require(i >= 0)
@@ -78,7 +87,7 @@ object Knapscak {
else {
Cons((i,ri), bottomup(i + 1, w, items))
}
- } ensuring(items.size <= 10 ==> time <= ? * (w - i + 1))
+ } ensuring(_ => items.size <= 10 ==> time <= ? * (w - i + 1))
/**
* Computes the list of optimal solutions of all weights up to 'w'
@@ -86,7 +95,7 @@ object Knapscak {
def knapSackSol(w: BigInt, items: IList) = {
require(w >= 0 && items.size <= 10) // the second requirement is only to keep the bounds linear for z3 to work
bottomup(0, w, items)
- } ensuring(time <= ? * w + ?)
+ } ensuring(_ => time <= ? * w + ?)
/**
* Lemmas of deps
@@ -104,4 +113,20 @@ object Knapscak {
require(x >= 0 && y >= 0)
(x <= y && deps(y, items)) ==> deps(x, items)
} holds
+
+ @ignore
+ def main(args: Array[String]) {
+ import scala.util.Random
+ // pick some random weights and values
+ val weightsnValues1 = (1 to 10).foldRight(Nil(): IList){
+ case (i, acc) => Cons((i, i), acc)
+ }
+ val reslist1 = knapSackSol(100, weightsnValues1) // without memoization this will take too long
+ println("Optimal solutions: "+reslist1.toString)
+ val weightsnValues2 = ((1 to 10) zip (10 to 1 by -1)).foldRight(Nil(): IList){
+ case ((i, j), acc) => Cons((i, j), acc)
+ }
+ val reslist2 = knapSackSol(100, weightsnValues2)
+ println("Optimal solutions for set 2: "+reslist2.toString)
+ }
}
diff --git a/testcases/lazy-datastructures/withOrb/LazyNumericalRep.scala b/testcases/lazy-datastructures/withOrb/LazyNumericalRep.scala
index 47a42bfa1d6d891a843db9767ac94562bc343c0e..b3c5a205fd392de97bc653a5750698197b825239 100644
--- a/testcases/lazy-datastructures/withOrb/LazyNumericalRep.scala
+++ b/testcases/lazy-datastructures/withOrb/LazyNumericalRep.scala
@@ -1,16 +1,22 @@
-package orb
+package withOrb
-import leon.lazyeval._
-import leon.lang._
-import leon.annotation._
-import leon.instrumentation._
-import leon.lazyeval.$._
-import leon.invariant._
+import leon._
+import lazyeval._
+import lang._
+import annotation._
+import instrumentation._
+import invariant._
object DigitObject {
sealed abstract class Digit
- case class Zero() extends Digit
- case class One() extends Digit
+ case class Zero() extends Digit {
+ @ignore
+ override def toString = "0"
+ }
+ case class One() extends Digit {
+ @ignore
+ override def toString = "1"
+ }
}
import DigitObject._
@@ -19,13 +25,13 @@ object LazyNumericalRep {
sealed abstract class NumStream {
val isSpine: Boolean = this match {
case Spine(_, _, _) => true
- case _ => false
+ case _ => false
}
val isTip = !isSpine
}
case class Tip() extends NumStream
- case class Spine(head: Digit, createdWithSuspension: Bool, rear: $[NumStream]) extends NumStream
+ case class Spine(head: Digit, createdWithSuspension: Bool, rear: Lazy[NumStream]) extends NumStream
sealed abstract class Bool
case class True() extends Bool
@@ -34,7 +40,7 @@ object LazyNumericalRep {
/**
* Checks whether there is a zero before an unevaluated closure
*/
- def zeroPrecedeLazy[T](q: $[NumStream]): Boolean = {
+ def zeroPrecedeLazy[T](q: Lazy[NumStream]): Boolean = {
if (q.isEvaluated) {
q* match {
case Spine(Zero(), _, rear) =>
@@ -49,7 +55,7 @@ object LazyNumericalRep {
/**
* Checks whether there is a zero before a given suffix
*/
- def zeroPrecedeSuf[T](q: $[NumStream], suf: $[NumStream]): Boolean = {
+ def zeroPrecedeSuf[T](q: Lazy[NumStream], suf: Lazy[NumStream]): Boolean = {
if (q != suf) {
q* match {
case Spine(Zero(), _, rear) => true
@@ -64,7 +70,7 @@ object LazyNumericalRep {
* Everything until suf is evaluated. This
* also asserts that suf should be a suffix of the list
*/
- def concreteUntil[T](l: $[NumStream], suf: $[NumStream]): Boolean = {
+ def concreteUntil[T](l: Lazy[NumStream], suf: Lazy[NumStream]): Boolean = {
if (l != suf) {
l.isEvaluated && (l* match {
case Spine(_, cws, tail) =>
@@ -75,7 +81,7 @@ object LazyNumericalRep {
} else true
}
- def isConcrete[T](l: $[NumStream]): Boolean = {
+ def isConcrete[T](l: Lazy[NumStream]): Boolean = {
l.isEvaluated && (l* match {
case Spine(_, _, tail) =>
isConcrete(tail)
@@ -84,10 +90,10 @@ object LazyNumericalRep {
}
sealed abstract class Scheds
- case class Cons(h: $[NumStream], tail: Scheds) extends Scheds
+ case class Cons(h: Lazy[NumStream], tail: Scheds) extends Scheds
case class Nil() extends Scheds
- def schedulesProperty[T](q: $[NumStream], schs: Scheds): Boolean = {
+ def schedulesProperty[T](q: Lazy[NumStream], schs: Scheds): Boolean = {
schs match {
case Cons(head, tail) =>
head* match {
@@ -104,7 +110,7 @@ object LazyNumericalRep {
}
@invisibleBody
- def strongSchedsProp[T](q: $[NumStream], schs: Scheds) = {
+ def strongSchedsProp[T](q: Lazy[NumStream], schs: Scheds) = {
q.isEvaluated && {
schs match {
case Cons(head, tail) =>
@@ -119,7 +125,7 @@ object LazyNumericalRep {
* Note: if 'q' has a suspension then it would have a carry.
*/
@invisibleBody
- def pushUntilCarry[T](q: $[NumStream]): $[NumStream] = {
+ def pushUntilCarry[T](q: Lazy[NumStream]): Lazy[NumStream] = {
q* match {
case Spine(Zero(), _, rear) => // if we push a carry and get back 0 then there is a new carry
pushUntilCarry(rear)
@@ -130,12 +136,16 @@ object LazyNumericalRep {
}
}
- case class Number(digs: $[NumStream], schedule: Scheds) {
- val valid = strongSchedsProp(digs, schedule)
+ case class Number(digs: Lazy[NumStream], schedule: Scheds) {
+ def isEmpty = digs.value.isTip
+
+ def valid = strongSchedsProp(digs, schedule)
}
+ def emptyNum = Number(Tip(), Nil())
+
@invisibleBody
- def inc(xs: $[NumStream]): NumStream = {
+ def inc(xs: Lazy[NumStream]): NumStream = {
require(zeroPrecedeLazy(xs))
xs.value match {
case Tip() =>
@@ -149,11 +159,11 @@ object LazyNumericalRep {
@invisibleBody
@invstate
- def incLazy(xs: $[NumStream]): NumStream = {
+ def incLazy(xs: Lazy[NumStream]): NumStream = {
require(zeroPrecedeLazy(xs) &&
(xs* match {
case Spine(h, _, _) => h != Zero() // xs doesn't start with a zero
- case _ => false
+ case _ => false
}))
xs.value match {
case Spine(head, _, rear) => // here, rear is guaranteed to be evaluated by 'zeroPrecedeLazy' invariant
@@ -191,11 +201,11 @@ object LazyNumericalRep {
*/
@invisibleBody
@invstate
- def incLazyLemma[T](xs: $[NumStream], suf: $[NumStream]): Boolean = {
+ def incLazyLemma[T](xs: Lazy[NumStream], suf: Lazy[NumStream]): Boolean = {
require(zeroPrecedeSuf(xs, suf) &&
(xs* match {
case Spine(h, _, _) => h != Zero()
- case _ => false
+ case _ => false
}) &&
(suf* match {
case Spine(Zero(), _, _) =>
@@ -243,7 +253,7 @@ object LazyNumericalRep {
case _ =>
w.schedule
}
- val lq: $[NumStream] = nq
+ val lq: Lazy[NumStream] = nq
(lq, nsched)
} ensuring { res =>
// lemma instantiations
@@ -263,7 +273,7 @@ object LazyNumericalRep {
}
@invisibleBody
- def Pay[T](q: $[NumStream], scheds: Scheds): Scheds = {
+ def Pay[T](q: Lazy[NumStream], scheds: Scheds): Scheds = {
require(schedulesProperty(q, scheds) && q.isEvaluated)
scheds match {
case c @ Cons(head, rest) =>
@@ -331,8 +341,15 @@ object LazyNumericalRep {
} ensuring { res => res.valid && time <= ? }
+ def firstDigit(w: Number): Digit = {
+ require(!w.isEmpty)
+ w.digs.value match {
+ case Spine(d, _, _) => d
+ }
+ }
+
// monotonicity lemmas
- def schedMonotone[T](st1: Set[$[NumStream]], st2: Set[$[NumStream]], scheds: Scheds, l: $[NumStream]): Boolean = {
+ def schedMonotone[T](st1: Set[Lazy[NumStream]], st2: Set[Lazy[NumStream]], scheds: Scheds, l: Lazy[NumStream]): Boolean = {
require(st1.subsetOf(st2) &&
(schedulesProperty(l, scheds) withState st1)) // here the input state is fixed as 'st1'
//induction scheme
@@ -350,18 +367,18 @@ object LazyNumericalRep {
} holds
@traceInduct
- def concreteMonotone[T](st1: Set[$[NumStream]], st2: Set[$[NumStream]], l: $[NumStream]): Boolean = {
+ def concreteMonotone[T](st1: Set[Lazy[NumStream]], st2: Set[Lazy[NumStream]], l: Lazy[NumStream]): Boolean = {
((isConcrete(l) withState st1) && st1.subsetOf(st2)) ==> (isConcrete(l) withState st2)
} holds
@traceInduct
- def concUntilMonotone[T](q: $[NumStream], suf: $[NumStream], st1: Set[$[NumStream]], st2: Set[$[NumStream]]): Boolean = {
+ def concUntilMonotone[T](q: Lazy[NumStream], suf: Lazy[NumStream], st1: Set[Lazy[NumStream]], st2: Set[Lazy[NumStream]]): Boolean = {
((concreteUntil(q, suf) withState st1) && st1.subsetOf(st2)) ==> (concreteUntil(q, suf) withState st2)
} holds
// suffix predicates and their properties (this should be generalizable)
- def suffix[T](q: $[NumStream], suf: $[NumStream]): Boolean = {
+ def suffix[T](q: Lazy[NumStream], suf: Lazy[NumStream]): Boolean = {
if (q == suf) true
else {
q* match {
@@ -372,7 +389,7 @@ object LazyNumericalRep {
}
}
- def properSuffix[T](l: $[NumStream], suf: $[NumStream]): Boolean = {
+ def properSuffix[T](l: Lazy[NumStream], suf: Lazy[NumStream]): Boolean = {
l* match {
case Spine(_, _, rear) =>
suffix(rear, suf)
@@ -384,7 +401,7 @@ object LazyNumericalRep {
* suf(q, suf) ==> suf(q.rear, suf.rear)
*/
@traceInduct
- def suffixTrans[T](q: $[NumStream], suf: $[NumStream]): Boolean = {
+ def suffixTrans[T](q: Lazy[NumStream], suf: Lazy[NumStream]): Boolean = {
suffix(q, suf) ==> ((q*, suf*) match {
case (Spine(_, _, rear), Spine(_, _, sufRear)) =>
// 'sufRear' should be a suffix of 'rear1'
@@ -396,7 +413,7 @@ object LazyNumericalRep {
/**
* properSuf(l, suf) ==> l != suf
*/
- def suffixDisequality[T](l: $[NumStream], suf: $[NumStream]): Boolean = {
+ def suffixDisequality[T](l: Lazy[NumStream], suf: Lazy[NumStream]): Boolean = {
require(properSuffix(l, suf))
suffixTrans(l, suf) && // lemma instantiation
((l*, suf*) match { // induction scheme
@@ -408,21 +425,21 @@ object LazyNumericalRep {
}.holds
@traceInduct
- def suffixCompose[T](q: $[NumStream], suf1: $[NumStream], suf2: $[NumStream]): Boolean = {
+ def suffixCompose[T](q: Lazy[NumStream], suf1: Lazy[NumStream], suf2: Lazy[NumStream]): Boolean = {
(suffix(q, suf1) && properSuffix(suf1, suf2)) ==> properSuffix(q, suf2)
} holds
// properties of 'concUntil'
@traceInduct
- def concreteUntilIsSuffix[T](l: $[NumStream], suf: $[NumStream]): Boolean = {
+ def concreteUntilIsSuffix[T](l: Lazy[NumStream], suf: Lazy[NumStream]): Boolean = {
concreteUntil(l, suf) ==> suffix(l, suf)
}.holds
// properties that extend `concUntil` to larger portions of the queue
@traceInduct
- def concUntilExtenLemma[T](q: $[NumStream], suf: $[NumStream], st1: Set[$[NumStream]], st2: Set[$[NumStream]]): Boolean = {
+ def concUntilExtenLemma[T](q: Lazy[NumStream], suf: Lazy[NumStream], st1: Set[Lazy[NumStream]], st2: Set[Lazy[NumStream]]): Boolean = {
((concreteUntil(q, suf) withState st1) && st2 == st1 ++ Set(suf)) ==>
(suf* match {
case Spine(_, _, rear) =>
@@ -432,12 +449,12 @@ object LazyNumericalRep {
} holds
@traceInduct
- def concUntilConcreteExten[T](q: $[NumStream], suf: $[NumStream]): Boolean = {
+ def concUntilConcreteExten[T](q: Lazy[NumStream], suf: Lazy[NumStream]): Boolean = {
(concreteUntil(q, suf) && isConcrete(suf)) ==> isConcrete(q)
} holds
@traceInduct
- def concUntilCompose[T](q: $[NumStream], suf1: $[NumStream], suf2: $[NumStream]): Boolean = {
+ def concUntilCompose[T](q: Lazy[NumStream], suf1: Lazy[NumStream], suf2: Lazy[NumStream]): Boolean = {
(concreteUntil(q, suf1) && concreteUntil(suf1, suf2)) ==> concreteUntil(q, suf2)
} holds
@@ -446,19 +463,19 @@ object LazyNumericalRep {
@invisibleBody
@traceInduct
- def zeroPredSufConcreteUntilLemma[T](q: $[NumStream], suf: $[NumStream]): Boolean = {
+ def zeroPredSufConcreteUntilLemma[T](q: Lazy[NumStream], suf: Lazy[NumStream]): Boolean = {
(zeroPrecedeSuf(q, suf) && concreteUntil(q, suf)) ==> zeroPrecedeLazy(q)
} holds
@invisibleBody
@traceInduct
- def concreteZeroPredLemma[T](q: $[NumStream]): Boolean = {
+ def concreteZeroPredLemma[T](q: Lazy[NumStream]): Boolean = {
isConcrete(q) ==> zeroPrecedeLazy(q)
} holds
// properties relating `suffix` an `zeroPrecedeSuf`
- def suffixZeroLemma[T](q: $[NumStream], suf: $[NumStream], suf2: $[NumStream]): Boolean = {
+ def suffixZeroLemma[T](q: Lazy[NumStream], suf: Lazy[NumStream], suf2: Lazy[NumStream]): Boolean = {
require(suf* match {
case Spine(Zero(), _, _) =>
suffix(q, suf) && properSuffix(suf, suf2)
@@ -476,4 +493,43 @@ object LazyNumericalRep {
} else true) &&
zeroPrecedeSuf(q, suf2) // property
}.holds
+
+ @ignore
+ def main(args: Array[String]) {
+ //import eagerEval.BigNums
+ import scala.util.Random
+ import scala.math.BigInt
+ import stats._
+ import collection._
+
+ println("Running Numerical Representation test...")
+ val ops = 1000000
+ // initialize to a queue with one element (required to satisfy preconditions of dequeue and front)
+ //var bignum: BigNums.BigNum = BigNums.Nil()
+ var lazynum = emptyNum
+ var totalTime1 = 0L
+ var totalTime2 = 0L
+ println(s"Testing amortized emphemeral behavior on $ops operations...")
+ for (i <- 0 until ops) {
+ //println("Inc..")
+ //bignum = timed { BigNums.increment(bignum) } { totalTime1 += _ }
+ lazynum = timed { incAndPay(lazynum) } { totalTime2 += _ }
+ //val d1 = BigNums.firstDigit(bignum)
+ val d2 = firstDigit(lazynum)
+ //assert(d1.toString == d2.toString, s"Eager head: $d1 Lazy head: $d2")
+ }
+ println(s"Ephemeral Amortized Time - Eager: ${totalTime1 / 1000.0}s Lazy: ${totalTime2 / 1000.0}s") // this should be linear in length for both cases
+ // now, test worst-case behavior (in persitent mode if necessary)
+ val length = (1 << 22) - 1 // a number of the form: 2^{n-1}
+ //bignum = BigNums.Nil()
+ lazynum = emptyNum
+ for (i <- 0 until length) {
+ //bignum = BigNums.increment(bignum)
+ lazynum = incAndPay(lazynum)
+ }
+ //println(s"Number of leading ones of bignum: ${BigNums.leadingOnes(bignum)}")
+ //dequeue 1 element from both queues
+ //timed { BigNums.increment(bignum) } { t => println(s"Time for one eager increment in the worst case: ${t / 1000.0}s") }
+ timed { incAndPay(lazynum) } { t => println(s"Time for one lazy increment in the worst case: ${t / 1000.0}s") }
+ }
}
diff --git a/testcases/lazy-datastructures/withOrb/PackratParsing.scala b/testcases/lazy-datastructures/withOrb/PackratParsing.scala
index b9377da8ff6b0f3cb987dc32880b5216a90e9574..4cf2b81fea9a1a574acef30b0535a4596eceb46d 100644
--- a/testcases/lazy-datastructures/withOrb/PackratParsing.scala
+++ b/testcases/lazy-datastructures/withOrb/PackratParsing.scala
@@ -1,11 +1,11 @@
package orb
-import leon.lazyeval._
-import leon.lazyeval.Mem._
-import leon.lang._
-import leon.annotation._
-import leon.instrumentation._
-import leon.invariant._
+import leon._
+import mem._
+import lang._
+import annotation._
+import instrumentation._
+import invariant._
/**
* The packrat parser that uses the Expressions grammar presented in Bran Ford ICFP'02 paper.
@@ -22,7 +22,9 @@ object PackratParsing {
case class Digit() extends Terminal
/**
- * A mutable array of tokens returned by the lexer
+ * A mutable array of tokens returned by the lexer.
+ * The string of tokens is reversed i.e,
+ * string(legnth-1) represents the first char and string(0) represents the last char.
*/
@ignore
var string = Array[Terminal]()
@@ -33,7 +35,7 @@ object PackratParsing {
@extern
def lookup(i: BigInt): Terminal = {
string(i.toInt)
- } ensuring(_ => time <= 1)
+ } ensuring (_ => time <= 1)
sealed abstract class Result {
/**
@@ -43,7 +45,7 @@ object PackratParsing {
@inline
def smallerIndex(i: BigInt) = this match {
case Parsed(m) => m < i
- case _ => true
+ case _ => true
}
}
case class Parsed(rest: BigInt) extends Result
@@ -53,48 +55,53 @@ object PackratParsing {
@memoize
@invstate
def pAdd(i: BigInt): Result = {
- require(depsEval(i) &&
- pMul(i).isCached && pPrim(i).isCached &&
- resEval(i, pMul(i))) // lemma inst
-
+ require {
+ if (depsEval(i) && pMul(i).isCached && pPrim(i).isCached)
+ resEval(i, pMul(i)) // lemma inst
+ else false
+ }
// Rule 1: Add <- Mul + Add
- pMul(i) match {
+ val mulRes = pMul(i)
+ mulRes match {
case Parsed(j) =>
if (j > 0 && lookup(j) == Plus()) {
pAdd(j - 1) match {
case Parsed(rem) =>
Parsed(rem)
case _ =>
- pMul(i) // Rule2: Add <- Mul
+ mulRes // Rule2: Add <- Mul
}
- } else pMul(i)
+ } else mulRes
case _ =>
- pMul(i)
+ mulRes
}
- } ensuring (res => res.smallerIndex(i) && time <= ?)
+ } ensuring (res => res.smallerIndex(i) && time <= ?) // time <= 26
@invisibleBody
@memoize
@invstate
def pMul(i: BigInt): Result = {
- require(depsEval(i) && pPrim(i).isCached &&
- resEval(i, pPrim(i)) // lemma inst
- )
+ require{
+ if (depsEval(i) && pPrim(i).isCached)
+ resEval(i, pPrim(i)) // lemma inst
+ else false
+ }
// Rule 1: Mul <- Prim * Mul
- pPrim(i) match {
+ val primRes = pPrim(i)
+ primRes match {
case Parsed(j) =>
- if (j > 0 && lookup(j) == Plus()) {
+ if (j > 0 && lookup(j) == Times()) {
pMul(j - 1) match {
case Parsed(rem) =>
Parsed(rem)
case _ =>
- pPrim(i) // Rule2: Mul <- Prim
+ primRes // Rule2: Mul <- Prim
}
- } else pPrim(i)
+ } else primRes
case _ =>
- pPrim(i)
+ primRes
}
- } ensuring (res => res.smallerIndex(i) && time <= ?)
+ } ensuring (res => res.smallerIndex(i) && time <= ?) // time <= 26
@invisibleBody
@memoize
@@ -106,23 +113,24 @@ object PackratParsing {
if (i > 0)
Parsed(i - 1) // Rule1: Prim <- Digit
else
- Parsed(-1) // here, we can use -1 to convery that the suffix is empty
+ Parsed(-1) // here, we can use -1 to convey that the suffix is empty
} else if (char == Open() && i > 0) {
pAdd(i - 1) match { // Rule 2: pPrim <- ( Add )
case Parsed(rem) =>
- Parsed(rem)
+ if (rem >= 0 && lookup(rem) == Close()) Parsed(rem - 1)
+ else NoParse()
case _ =>
NoParse()
}
} else NoParse()
- } ensuring (res => res.smallerIndex(i) && time <= ?)
+ } ensuring (res => res.smallerIndex(i) && time <= ?) // time <= 28
//@inline
- def depsEval(i: BigInt) = i == 0 || (i > 0 && allEval(i-1))
+ def depsEval(i: BigInt) = i == 0 || (i > 0 && allEval(i - 1))
def allEval(i: BigInt): Boolean = {
require(i >= 0)
- (pPrim(i).isCached && pMul(i).isCached && pAdd(i).isCached) &&(
+ (pPrim(i).isCached && pMul(i).isCached && pAdd(i).isCached) && (
if (i == 0) true
else allEval(i - 1))
}
@@ -152,17 +160,51 @@ object PackratParsing {
})
}
- @invisibleBody
+ /*@invisibleBody
def invoke(i: BigInt): (Result, Result, Result) = {
- require(i == 0 || (i > 0 && allEval(i-1)))
+ require(i == 0 || (i > 0 && allEval(i - 1)))
(pPrim(i), pMul(i), pAdd(i))
} ensuring (res => {
- val in = Mem.inState[Result]
- val out = Mem.outState[Result]
- (if(i >0) evalMono(i-1, in, out) else true) &&
- allEval(i) &&
- time <= ?
- })
+ val in = inState[Result]
+ val out = outState[Result]
+ (if (i > 0) evalMono(i - 1, in, out) else true) &&
+ allEval(i) &&
+ time <= ?
+ })*/
+
+ def invokePrim(i: BigInt): Result = {
+ require(depsEval(i))
+ pPrim(i)
+ } ensuring { res =>
+ val in = inState[Result]
+ val out = outState[Result]
+ (if (i > 0) evalMono(i - 1, in, out) else true)
+ }
+
+ def invokeMul(i: BigInt): Result = {
+ require(depsEval(i))
+ invokePrim(i) match {
+ case _ => pMul(i)
+ }
+ } ensuring { res =>
+ val in = inState[Result]
+ val out = outState[Result]
+ (if (i > 0) evalMono(i - 1, in, out) else true)
+ }
+
+ @invisibleBody
+ def invoke(i: BigInt): Result = {
+ require(depsEval(i))
+ invokeMul(i) match {
+ case _ => pAdd(i)
+ }
+ } ensuring { res =>
+ val in = inState[Result]
+ val out = outState[Result]
+ (if (i > 0) evalMono(i - 1, in, out) else true) &&
+ allEval(i) &&
+ time <= ? // 189
+ }
/**
* Parsing a string of length 'n+1'.
@@ -172,11 +214,34 @@ object PackratParsing {
@invisibleBody
def parse(n: BigInt): Result = {
require(n >= 0)
- if(n == 0) invoke(n)._3
+ if (n == 0) invoke(n)
else {
- val tailres = parse(n-1) // we parse the prefixes ending at 0, 1, 2, 3, ..., n
- invoke(n)._3
+ parse(n - 1) match { // we parse the prefixes ending at 0, 1, 2, 3, ..., n
+ case _ =>
+ invoke(n)
+ }
}
- } ensuring(_ => allEval(n) &&
- time <= ? * n + ?)
+ } ensuring (_ => allEval(n) &&
+ time <= ? * n + ?) // 198 * n + 192
+
+ @ignore
+ def main(args: Array[String]) {
+ // note: we can run only one test in each run as the cache needs to be cleared between the tests,
+ // which is not currently supported by the api's
+ test1()
+ //test2()
+ }
+
+ @ignore
+ def test1() {
+ // list of tokens to parse. The list is reversed i.e, the first char is at the last index, the last char is at the first index.
+ string = Array(Plus(), Digit(), Times(), Close(), Digit(), Plus(), Digit(), Open()) // d * ( d + d ) +
+ println("Parsing Expression 1: " + parse(string.length - 1))
+ }
+
+ @ignore
+ def test2() {
+ string = Array(Times(), Digit(), Open()) // ( d *
+ println("Parsing Expression 2: " + parse(string.length - 1))
+ }
}
diff --git a/testcases/lazy-datastructures/withOrb/RealTimeQueue.scala b/testcases/lazy-datastructures/withOrb/RealTimeQueue.scala
index f0a78b4f2330e70be9285407c1265ccb00b4abb2..3eda466a8b6c3885d3c9ca34a3ebd15a58af3b83 100644
--- a/testcases/lazy-datastructures/withOrb/RealTimeQueue.scala
+++ b/testcases/lazy-datastructures/withOrb/RealTimeQueue.scala
@@ -1,12 +1,12 @@
-package orb
+package withOrb
-import leon.lazyeval._
-import leon.lazyeval.$._
-import leon.lang._
-import leon.annotation._
-import leon.collection._
-import leon.instrumentation._
-import leon.invariant._
+import leon._
+import lazyeval._
+import lang._
+import annotation._
+import collection._
+import instrumentation._
+import invariant._
object RealTimeQueue {
@@ -32,10 +32,10 @@ object RealTimeQueue {
}
} ensuring (_ >= 0)
}
- case class SCons[T](x: T, tail: $[Stream[T]]) extends Stream[T]
+ case class SCons[T](x: T, tail: Lazy[Stream[T]]) extends Stream[T]
case class SNil[T]() extends Stream[T]
- def isConcrete[T](l: $[Stream[T]]): Boolean = {
+ def isConcrete[T](l: Lazy[Stream[T]]): Boolean = {
l.isEvaluated && (l* match {
case SCons(_, tail) =>
isConcrete(tail)
@@ -45,7 +45,7 @@ object RealTimeQueue {
@invisibleBody
@invstate
- def rotate[T](f: $[Stream[T]], r: List[T], a: $[Stream[T]]): Stream[T] = { // doesn't change state
+ def rotate[T](f: Lazy[Stream[T]], r: List[T], a: Lazy[Stream[T]]): Stream[T] = { // doesn't change state
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'
@@ -56,12 +56,12 @@ object RealTimeQueue {
SCons[T](x, rot)
}
} ensuring (res => res.size == (f*).size + r.size + (a*).size && res.isCons &&
- time <= ?)
+ time <= ?)
/**
* Returns the first element of the stream that is not evaluated.
*/
- def firstUnevaluated[T](l: $[Stream[T]]): $[Stream[T]] = {
+ def firstUnevaluated[T](l: Lazy[Stream[T]]): Lazy[Stream[T]] = {
if (l.isEvaluated) {
l* match {
case SCons(_, tail) =>
@@ -77,7 +77,7 @@ object RealTimeQueue {
case _ => true
}))
- case class Queue[T](f: $[Stream[T]], r: List[T], s: $[Stream[T]]) {
+ case class Queue[T](f: Lazy[Stream[T]], r: List[T], s: Lazy[Stream[T]]) {
def isEmpty = (f*).isEmpty
def valid = {
(firstUnevaluated(f) == firstUnevaluated(s)) &&
@@ -86,7 +86,7 @@ object RealTimeQueue {
}
@inline
- def createQ[T](f: $[Stream[T]], r: List[T], s: $[Stream[T]]) = {
+ def createQ[T](f: Lazy[Stream[T]], r: List[T], s: Lazy[Stream[T]]) = {
s.value match {
case SCons(_, tail) => Queue(f, r, tail)
case SNil() =>
@@ -96,6 +96,18 @@ object RealTimeQueue {
}
}
+ def empty[T] = {
+ val a: Stream[T] = SNil()
+ Queue(a, Nil(), a)
+ }
+
+ def head[T](q: Queue[T]): T = {
+ require(!q.isEmpty && q.valid)
+ q.f.value match {
+ case SCons(x, _) => x
+ }
+ } //ensuring (res => res.valid && time <= ?)
+
def enqueue[T](x: T, q: Queue[T]): Queue[T] = {
require(q.valid)
createQ(q.f, Cons(x, q.r), q.s)
@@ -108,4 +120,57 @@ object RealTimeQueue {
createQ(nf, q.r, q.s)
}
} ensuring (res => res.valid && time <= ?)
+
+ @ignore
+ def main(args: Array[String]) {
+ //import eagerEval.AmortizedQueue
+ import scala.util.Random
+ import scala.math.BigInt
+ import stats._
+ import collection._
+
+ println("Running RTQ test...")
+ val ops = 10000000
+ val rand = Random
+ // initialize to a queue with one element (required to satisfy preconditions of dequeue and front)
+ var rtq = empty[BigInt]
+ //var amq = AmortizedQueue.Queue(AmortizedQueue.Nil(), AmortizedQueue.Nil())
+ var totalTime1 = 0L
+ var totalTime2 = 0L
+ println(s"Testing amortized emphemeral behavior on $ops operations...")
+ for (i <- 0 until ops) {
+ if (!rtq.isEmpty) {
+ val h1 = head(rtq)
+ //val h2 = amq.head
+ //assert(h1 == h2, s"Eager head: $h2 Lazy head: $h1")
+ }
+ rand.nextInt(2) match {
+ case x if x == 0 => //enqueue
+ // /if(i%100000 == 0) println("Enqueue..")
+ rtq = timed { enqueue(BigInt(i), rtq) } { totalTime1 += _ }
+ //amq = timed { amq.enqueue(BigInt(i)) } { totalTime2 += _ }
+ case x if x == 1 => //dequeue
+ if (!rtq.isEmpty) {
+ //if(i%100000 == 0) println("Dequeue..")
+ rtq = timed { dequeue(rtq) } { totalTime1 += _ }
+ //amq = timed { amq.dequeue } { totalTime2 += _ }
+ }
+ }
+ }
+ println(s"Ephemeral Amortized Time - Eager: ${totalTime2 / 1000.0}s Lazy: ${totalTime1 / 1000.0}s") // this should be linear in length for both cases
+ // now, test worst-case behavior (in persitent mode if necessary)
+ val length = (1 << 22) - 2 // a number of the form: 2^{n-2}
+ // reset the queues
+ rtq = empty[BigInt]
+ //amq = AmortizedQueue.Queue(AmortizedQueue.Nil(), AmortizedQueue.Nil())
+ // enqueue length elements
+ for (i <- 0 until length) {
+ rtq = enqueue(BigInt(0), rtq)
+ //amq = amq.enqueue(BigInt(0))
+ }
+ //println(s"Amortized queue size: ${amq.front.size}, ${amq.rear.size}")
+ //dequeue 1 element from both queues
+ //timed { amq.dequeue } { t => println(s"Time to dequeue one element from Amortized Queue in the worst case: ${t / 1000.0}s") }
+ timed { dequeue(rtq) } { t => println(s"Time to dequeue one element from RTQ in the worst case: ${t / 1000.0}s") }
+ }
}
diff --git a/testcases/lazy-datastructures/withOrb/SortingnConcat-orb.scala b/testcases/lazy-datastructures/withOrb/SortingnConcat.scala
similarity index 72%
rename from testcases/lazy-datastructures/withOrb/SortingnConcat-orb.scala
rename to testcases/lazy-datastructures/withOrb/SortingnConcat.scala
index 76f6bae6bba6e3d7f24a5741cbbd9c638642e29d..0f4c1151b72c4559be6a11c29aa7d854d881a28c 100644
--- a/testcases/lazy-datastructures/withOrb/SortingnConcat-orb.scala
+++ b/testcases/lazy-datastructures/withOrb/SortingnConcat.scala
@@ -1,10 +1,11 @@
package withOrb
-import leon.lazyeval._
-import leon.lang._
-import leon.annotation._
-import leon.instrumentation._
-import leon.invariant._
+import leon._
+import lazyeval._
+import lang._
+import annotation._
+import instrumentation._
+import invariant._
object SortingnConcat {
@@ -17,9 +18,9 @@ object SortingnConcat {
}
} ensuring (_ >= 0)
}
- case class SCons(x: BigInt, tail: $[LList]) extends LList
+ case class SCons(x: BigInt, tail: Lazy[LList]) extends LList
case class SNil() extends LList
- def ssize(l: $[LList]): BigInt = (l*).size
+ def ssize(l: Lazy[LList]): BigInt = (l*).size
sealed abstract class List {
def size: BigInt = this match {
@@ -60,18 +61,7 @@ object SortingnConcat {
}
} ensuring(res => time <= ?)
- def secondMin(l: $[LList]) : BigInt = {
- l.value match {
- case SCons(x, xs) =>
- xs.value match {
- case SCons(y, ys) => y
- case SNil() => x
- }
- case SNil() => BigInt(0)
- }
- } ensuring (_ => time <= ? * ssize(l) + ?)
-
-/* def kthMin(l: $[LList], k: BigInt): BigInt = {
+ def kthMin(l: Lazy[LList], k: BigInt): BigInt = {
require(k >= 1)
l.value match {
case SCons(x, xs) =>
@@ -80,5 +70,5 @@ object SortingnConcat {
kthMin(xs, k - 1)
case SNil() => BigInt(0)
}
- } ensuring (_ => time <= ? * k * ssize(l) + ? * k + ?)*/
+ } ensuring (_ => time <= ? * (k * ssize(l)) + ? * k + ?)
}
diff --git a/testcases/lazy-datastructures/withOrb/WeightedScheduling.scala b/testcases/lazy-datastructures/withOrb/WeightedScheduling.scala
index 74281ac66511eca27c394a62e4a7e5d88e3a3964..fc254279b27b8e7c0596deb1a4a3c276341a9333 100644
--- a/testcases/lazy-datastructures/withOrb/WeightedScheduling.scala
+++ b/testcases/lazy-datastructures/withOrb/WeightedScheduling.scala
@@ -1,20 +1,20 @@
package orb
-import leon.lazyeval._
-import leon.lazyeval.Mem._
-import leon.lang._
-import leon.annotation._
-import leon.instrumentation._
-import leon.invariant._
+import leon._
+import mem._
+import lang._
+import annotation._
+import instrumentation._
+import invariant._
object WeightedSched {
sealed abstract class IList {
def size: BigInt = {
this match {
case Cons(_, tail) => 1 + tail.size
- case Nil() => BigInt(0)
+ case Nil() => BigInt(0)
}
- } ensuring(_ >= 0)
+ } ensuring (_ >= 0)
}
case class Cons(x: BigInt, tail: IList) extends IList
case class Nil() extends IList
@@ -23,12 +23,14 @@ object WeightedSched {
* array of jobs
* (a) each job has a start time, finish time, and weight
* (b) Jobs are sorted in ascending order of finish times
+ * The first job should be (0,0,0) so that it acts as sentinel of every other job
*/
@ignore
var jobs = Array[(BigInt, BigInt, BigInt)]()
/**
* A precomputed mapping from each job i to the previous job j it is compatible with.
+ * The value of the first index could be anything.
*/
@ignore
var p = Array[Int]()
@@ -36,17 +38,17 @@ object WeightedSched {
@extern
def jobInfo(i: BigInt) = {
jobs(i.toInt)
- } ensuring(_ => time <= 1)
+ } ensuring (_ => time <= 1)
@extern
def prevCompatibleJob(i: BigInt) = {
BigInt(p(i.toInt))
- } ensuring(res => res >=0 && res < i && time <= 1)
+ } ensuring (res => res >= 0 && res < i && time <= 1)
@inline
def max(x: BigInt, y: BigInt) = if (x >= y) x else y
- def depsEval(i: BigInt) = i == 0 || (i > 0 && allEval(i-1))
+ def depsEval(i: BigInt) = i == 0 || (i > 0 && allEval(i - 1))
def allEval(i: BigInt): Boolean = {
require(i >= 0)
@@ -62,7 +64,7 @@ object WeightedSched {
} holds
@traceInduct
- def evalLem(x: BigInt, y: BigInt) = {
+ def evalLem(x: BigInt, y: BigInt) = {
require(x >= 0 && y >= 0)
(x <= y && allEval(y)) ==> allEval(x)
} holds
@@ -72,9 +74,9 @@ object WeightedSched {
@memoize
def sched(jobIndex: BigInt): BigInt = {
require(depsEval(jobIndex) &&
- (jobIndex == 0 || evalLem(prevCompatibleJob(jobIndex), jobIndex-1)))
+ (jobIndex == 0 || evalLem(prevCompatibleJob(jobIndex), jobIndex - 1)))
val (st, fn, w) = jobInfo(jobIndex)
- if(jobIndex == 0) w
+ if (jobIndex == 0) w
else {
// we may either include the head job or not:
// if we include the head job, we have to skip every job that overlaps with it
@@ -82,28 +84,50 @@ object WeightedSched {
val prevCompatVal = sched(prevCompatibleJob(jobIndex))
max(w + prevCompatVal, tailValue)
}
- } ensuring(_ => time <= ?)
+ } ensuring (_ => time <= ?)
@invisibleBody
def invoke(jobIndex: BigInt) = {
require(depsEval(jobIndex))
sched(jobIndex)
} ensuring (res => {
- val in = Mem.inState[BigInt]
- val out = Mem.outState[BigInt]
- (jobIndex == 0 || evalMono(jobIndex-1, in, out)) &&
+ val in = inState[BigInt]
+ val out = outState[BigInt]
+ (jobIndex == 0 || evalMono(jobIndex - 1, in, out)) &&
time <= ?
})
@invisibleBody
def schedBU(jobi: BigInt): IList = {
require(jobi >= 0)
- if(jobi == 0) {
- Cons(invoke(jobi), Nil())
+ if (jobi == 0) {
+ Cons(invoke(jobi), Nil())
} else {
- val tailRes = schedBU(jobi-1)
+ val tailRes = schedBU(jobi - 1)
Cons(invoke(jobi), tailRes)
}
- } ensuring(_ => allEval(jobi) &&
- time <= ? * (jobi + 1))
+ } ensuring (_ => allEval(jobi) &&
+ time <= ? * (jobi + 1))
+
+ @ignore
+ def main(args: Array[String]) {
+ // note: we can run only one test in each run as the cache needs to be cleared between the tests,
+ // which is not currently supported by the api's (note: the methods access a mutable field)
+ test1()
+ //test2()
+ }
+
+ @ignore
+ def test1() {
+ jobs = Array((0, 0, 0), (1, 2, 5), (3, 4, 2), (3, 8, 5), (6, 7, 10), (8, 11, 11), (10, 13, 20))
+ p = Array(0 /* anything */ , 0, 1, 1, 2, 4, 4)
+ println("Schedule for 5 jobs of set 1: " + schedBU(6))
+ }
+
+ @ignore
+ def test2() {
+ jobs = Array((0, 0, 0), (1, 3, 5), (3, 4, 2), (3, 8, 5), (6, 7, 10), (8, 11, 11), (10, 13, 20))
+ p = Array(0 /* anything */ , 0, 0, 0, 2, 4, 4)
+ println("Schedule for 5 jobs of set 2: " + schedBU(6))
+ }
}
diff --git a/testcases/lazy-datastructures/BottomUpMegeSort.scala b/testcases/lazy-datastructures/withconst/BottomUpMegeSort.scala
similarity index 92%
rename from testcases/lazy-datastructures/BottomUpMegeSort.scala
rename to testcases/lazy-datastructures/withconst/BottomUpMegeSort.scala
index 255da6e09da79b1c05db01e37becdaae70f9a754..1f4672599a487d19f80b0ebae1f5382ebf53f30c 100644
--- a/testcases/lazy-datastructures/BottomUpMegeSort.scala
+++ b/testcases/lazy-datastructures/withconst/BottomUpMegeSort.scala
@@ -1,11 +1,11 @@
package lazybenchmarks
-import leon.lazyeval._
-import leon.lazyeval.$._
-import leon.lang._
-import leon.annotation._
-import leon.instrumentation._
-//import leon.invariant._
+import leon._
+import lazyeval._
+import lang._
+import annotation._
+import instrumentation._
+//import invariant._
/**
* TODO Multiple instantiations of type parameters is not supported yet,
@@ -43,9 +43,9 @@ object BottomUpMergeSort {
}
} ensuring (_ >= 0)
}
- case class SCons(x: BigInt, tail: $[IStream]) extends IStream
+ case class SCons(x: BigInt, tail: Lazy[IStream]) extends IStream
case class SNil() extends IStream
- def ssize(l: $[IStream]): BigInt = (l*).size
+ def ssize(l: Lazy[IStream]): BigInt = (l*).size
/**
* A list of suspensions
@@ -72,7 +72,7 @@ object BottomUpMergeSort {
}
} ensuring (_ >= 0)
}
- case class LCons(x: $[IStream], tail: LList) extends LList
+ case class LCons(x: Lazy[IStream], tail: LList) extends LList
case class LNil() extends LList
/**
@@ -120,7 +120,8 @@ object BottomUpMergeSort {
* Note: the sorted stream of integers may by recursively constructed using merge.
* Takes time linear in the size of the streams (non-trivial to prove due to cascading of lazy calls)
*/
- def merge(a: $[IStream], b: $[IStream]): IStream = {
+ @usePost
+ def merge(a: Lazy[IStream], b: Lazy[IStream]): IStream = {
require(((a*) != SNil() || b.isEvaluated) && // if one of the arguments is Nil then the other is evaluated
((b*) != SNil() || a.isEvaluated) &&
((a*) != SNil() || (b*) != SNil())) // at least one of the arguments is not Nil
diff --git a/testcases/lazy-datastructures/Deque.scala b/testcases/lazy-datastructures/withconst/Deque.scala
similarity index 100%
rename from testcases/lazy-datastructures/Deque.scala
rename to testcases/lazy-datastructures/withconst/Deque.scala
diff --git a/testcases/lazy-datastructures/Esop15Benchmarks.scala b/testcases/lazy-datastructures/withconst/Esop15Benchmarks.scala
similarity index 100%
rename from testcases/lazy-datastructures/Esop15Benchmarks.scala
rename to testcases/lazy-datastructures/withconst/Esop15Benchmarks.scala
diff --git a/testcases/lazy-datastructures/LazyMegeSort.scala b/testcases/lazy-datastructures/withconst/LazyMegeSort.scala
similarity index 100%
rename from testcases/lazy-datastructures/LazyMegeSort.scala
rename to testcases/lazy-datastructures/withconst/LazyMegeSort.scala
diff --git a/testcases/lazy-datastructures/LazyNumericalRep.scala b/testcases/lazy-datastructures/withconst/LazyNumericalRep.scala
similarity index 100%
rename from testcases/lazy-datastructures/LazyNumericalRep.scala
rename to testcases/lazy-datastructures/withconst/LazyNumericalRep.scala
diff --git a/testcases/lazy-datastructures/RealTimeQueue.scala b/testcases/lazy-datastructures/withconst/RealTimeQueue.scala
similarity index 100%
rename from testcases/lazy-datastructures/RealTimeQueue.scala
rename to testcases/lazy-datastructures/withconst/RealTimeQueue.scala
diff --git a/testcases/lazy-datastructures/SortingnConcat.scala b/testcases/lazy-datastructures/withconst/SortingnConcat.scala
similarity index 100%
rename from testcases/lazy-datastructures/SortingnConcat.scala
rename to testcases/lazy-datastructures/withconst/SortingnConcat.scala
diff --git a/testcases/orb-testcases/amortized/BigNums.scala b/testcases/orb-testcases/amortized/BigNums.scala
index 883d1f45ab8752668070699c840edd7a3de160b9..e4860ff5af743e01eb6530018bf93bde5ca53932 100644
--- a/testcases/orb-testcases/amortized/BigNums.scala
+++ b/testcases/orb-testcases/amortized/BigNums.scala
@@ -1,37 +1,66 @@
-import leon.invariant._
-import leon.instrumentation._
+package orb
+
+import leon._
+import annotation._
+import invariant._
+import instrumentation._
object BigNums {
+ sealed abstract class Digit
+ case class Zero() extends Digit {
+ @ignore
+ override def toString = "0"
+ }
+ case class One() extends Digit {
+ @ignore
+ override def toString = "1"
+ }
+
sealed abstract class BigNum
- case class Cons(head: BigInt, tail: BigNum) extends BigNum
+ case class Cons(head: Digit, tail: BigNum) extends BigNum
case class Nil() extends BigNum
- def incrTime(l: BigNum) : BigInt = {
+ /**
+ * Time taken by the increment method
+ * The number of leading one's
+ */
+ def leadingOnes(l: BigNum) : BigInt = {
l match {
case Nil() => 1
- case Cons(x, tail) =>
- if(x == 0) 1
- else 1 + incrTime(tail)
+ case Cons(Zero(), tail) => 1
+ case Cons(_, tail) => 1 + leadingOnes(tail)
}
}
- def potentialIncr(l: BigNum) : BigInt = {
+ /**
+ * Total number of one's in the number
+ */
+ def numOnes(l: BigNum) : BigInt = {
l match {
case Nil() => 0
- case Cons(x, tail) =>
- if(x == 0) potentialIncr(tail)
- else 1 + potentialIncr(tail)
+ case Cons(Zero(), tail) => numOnes(tail)
+ case Cons(_, tail) => 1 + numOnes(tail)
}
}
-
+
+ /**
+ * Increments a number
+ */
def increment(l: BigNum) : BigNum = {
l match {
- case Nil() => Cons(1,l)
- case Cons(x, tail) =>
- if(x == 0) Cons(1, tail)
- else Cons(0, increment(tail))
+ case Nil() => Cons(One(), l)
+ case Cons(Zero(), tail) => Cons(One(), tail)
+ case Cons(_, tail) =>
+ Cons(Zero(), increment(tail))
}
- } ensuring (res => time <= ? * incrTime(l) + ? && incrTime(l) + potentialIncr(res) - potentialIncr(l) <= ?)
+ } ensuring (res => time <= ? * leadingOnes(l) + ? && leadingOnes(l) + numOnes(res) - numOnes(l) <= ?)
+
+ def firstDigit(l: BigNum): Digit = {
+ require(l != Nil())
+ l match {
+ case Cons(d, _) => d
+ }
+ }
/**
* Nop is the number of operations
@@ -41,7 +70,7 @@ object BigNums {
else {
incrUntil(nop-1, increment(l))
}
- } ensuring (res => time <= ? * nop + ? * potentialIncr(l) + ?)
+ } ensuring (res => time <= ? * nop + ? * numOnes(l) + ?)
def count(nop: BigInt) : BigNum = {
incrUntil(nop, Nil())
diff --git a/testcases/orb-testcases/timing/AmortizedQueue.scala b/testcases/orb-testcases/timing/AmortizedQueue.scala
index 23b5c35726d4e40f152e5d80878a96952266cbfb..8aece6a669c4fe6dd51d764efb40529731666a66 100644
--- a/testcases/orb-testcases/timing/AmortizedQueue.scala
+++ b/testcases/orb-testcases/timing/AmortizedQueue.scala
@@ -1,88 +1,83 @@
-import leon.invariant._
-import leon.instrumentation._
+package orb
-object AmortizedQueue {
- sealed abstract class List
- case class Cons(head : BigInt, tail : List) extends List
- case class Nil() extends List
-
- case class Queue(front : List, rear : List)
+import leon._
+import invariant._
+import instrumentation._
- def size(list : List) : BigInt = (list match {
- case Nil() => 0
- case Cons(_, xs) => 1 + size(xs)
- })
-
- def sizeList(list: List): BigInt = {
- list match {
- case Nil() => BigInt(0)
- case Cons(_, xs) => 1 + sizeList(xs)
+object AmortizedQueue {
+ sealed abstract class List {
+ val size: BigInt = this match {
+ case Nil() => 0
+ case Cons(_, xs) => 1 + xs.size
}
- }ensuring((res : BigInt) => res >= 0 && tmpl((a, b) => time <= a * size(list) + b))
-
- def qsize(q : Queue) : BigInt = size(q.front) + size(q.rear)
-
- def asList(q : Queue) : List = concat(q.front, reverse(q.rear))
-
- def concat(l1 : List, l2 : List) : List = (l1 match {
- case Nil() => l2
- case Cons(x,xs) => Cons(x, concat(xs, l2))
+ }
+ case class Cons(head: BigInt, tail: List) extends List
+ case class Nil() extends List
- }) ensuring (res => size(res) == size(l1) + size(l2) && tmpl((a,b,c) => time <= a*size(l1) + b))
+ def concat(l1: List, l2: List): List = (l1 match {
+ case Nil() => l2
+ case Cons(x, xs) => Cons(x, concat(xs, l2))
- def isAmortized(q : Queue) : Boolean = sizeList(q.front) >= sizeList(q.rear)
-
- def isEmpty(queue : Queue) : Boolean = queue match {
- case Queue(Nil(), Nil()) => true
- case _ => false
- }
+ }) ensuring (res => res.size == l1.size + l2.size && time <= ? * l1.size + ?)
def reverseRec(l1: List, l2: List): List = (l1 match {
- case Nil() => l2
+ case Nil() => l2
case Cons(x, xs) => reverseRec(xs, Cons(x, l2))
+ }) ensuring (res => l1.size + l2.size == res.size && time <= ? * l1.size + ?)
- }) ensuring (res => size(l1) + size(l2) == size(res) && tmpl((a,b) => time <= a*size(l1) + b))
-
- def reverse(l: List): List = {
+ def listRev(l: List): List = {
reverseRec(l, Nil())
- } ensuring (res => size(l) == size(res) && tmpl((a,b) => time <= a*size(l) + b))
+ } ensuring (res => l.size == res.size && time <= ? * l.size + ?)
- def amortizedQueue(front : List, rear : List) : Queue = {
- if (sizeList(rear) <= sizeList(front))
- Queue(front, rear)
- else
- Queue(concat(front, reverse(rear)), Nil())
- }
+ def removeLast(l: List): List = {
+ require(l != Nil())
+ l match {
+ case Cons(x, Nil()) => Nil()
+ case Cons(x, xs) => Cons(x, removeLast(xs))
+ case _ => Nil()
+ }
+ } ensuring (res => res.size <= l.size && tmpl((a, b) => time <= a * l.size + b))
- def enqueue(q : Queue, elem : BigInt) : Queue = ({
+ case class Queue(front: List, rear: List) {
+ def qsize: BigInt = front.size + rear.size
- amortizedQueue(q.front, Cons(elem, q.rear))
+ def asList: List = concat(front, listRev(rear))
- }) ensuring(res => true && tmpl((a,b) => time <= a*qsize(q) + b))
+ def isAmortized: Boolean = front.size >= rear.size
- def dequeue(q : Queue) : Queue = {
- require(isAmortized(q) && !isEmpty(q))
- q match {
- case Queue(Cons(f, fs), rear) => amortizedQueue(fs, rear)
- case _ => Queue(Nil(),Nil())
+ def isEmpty: Boolean = this match {
+ case Queue(Nil(), Nil()) => true
+ case _ => false
}
- } ensuring(res => true && tmpl((a,b) => time <= a*qsize(q) + b))
- def removeLast(l : List) : List = {
- require(l != Nil())
- l match {
- case Cons(x,Nil()) => Nil()
- case Cons(x,xs) => Cons(x, removeLast(xs))
- case _ => Nil()
+ def amortizedQueue(front: List, rear: List): Queue = {
+ if (rear.size <= front.size)
+ Queue(front, rear)
+ else
+ Queue(concat(front, listRev(rear)), Nil())
}
- } ensuring(res => size(res) <= size(l) && tmpl((a,b) => time <= a*size(l) + b))
- def pop(q : Queue) : Queue = {
- require(isAmortized(q) && !isEmpty(q))
- q match {
- case Queue(front, Cons(r,rs)) => Queue(front, rs)
- case Queue(front, rear) => Queue(removeLast(front), rear)
- case _ => Queue(Nil(),Nil())
+ def enqueue(elem: BigInt): Queue = ({
+ amortizedQueue(front, Cons(elem, rear))
+ }) ensuring (_ => time <= ? * qsize + ?)
+
+ def dequeue: Queue = {
+ require(isAmortized && !isEmpty)
+ front match {
+ case Cons(f, fs) => amortizedQueue(fs, rear)
+ case _ => Queue(Nil(), Nil())
+ }
+ } ensuring (_ => time <= ? * qsize + ?)
+
+ def head: BigInt = {
+ require(isAmortized && !isEmpty)
+ front match {
+ case Cons(f, _) => f
+ }
}
- } ensuring(res => true && tmpl((a,b) => time <= a*size(q.front) + b))
+
+ def reverse: Queue = { // this lets the queue perform deque operation (but they no longer have efficient constant time amortized bounds)
+ amortizedQueue(rear, front)
+ }
+ }
}
diff --git a/testcases/verification/list-algorithms/BasicMergeSort.scala b/testcases/verification/list-algorithms/BasicMergeSort.scala
index 55e632ff8f68307ba24cff691bde6b45fa206842..67fadf7dd7e7569107c4a6802b849f7844b66bd1 100644
--- a/testcases/verification/list-algorithms/BasicMergeSort.scala
+++ b/testcases/verification/list-algorithms/BasicMergeSort.scala
@@ -1,12 +1,16 @@
-import leon.lang._
-import leon.collection._
+package listalgorithms
+
+import leon._
+import lang._
+import collection._
+
object MergeSort {
def merge[T](less: (T, T) => Boolean)(xs: List[T], ys: List[T]): List[T] = {
(xs, ys) match {
case (Nil(), _) => ys
case (_, Nil()) => xs
- case (Cons(x,xtail), Cons(y,ytail)) =>
+ case (Cons(x, xtail), Cons(y, ytail)) =>
if (less(x, y))
x :: merge(less)(xtail, ys)
else
@@ -15,12 +19,23 @@ object MergeSort {
} ensuring { res => res.content == xs.content ++ ys.content &&
res.size == xs.size + ys.size }
+ def split[T](list: List[T]): (List[T], List[T]) = {
+ list match {
+ case Nil() => (Nil(), Nil())
+ case Cons(x, Nil()) => (Cons(x, Nil()), Nil())
+ case Cons(x1, Cons(x2, xs)) =>
+ val (s1, s2) = split(xs)
+ (Cons(x1, s1), Cons(x2, s2))
+ }
+ }
+
def msort[T](less: (T, T) => Boolean)(l: List[T]): List[T] = {
- if (l.size <= 1) l
- else {
- val c = l.length/2
- val (first, second) = l.splitAtIndex(c) // evenSplit
- merge(less)(msort(less)(first), msort(less)(second))
+ l match {
+ case Nil() => Nil[T]()
+ case Cons(x, Nil()) => Cons(x, Nil())
+ case _ =>
+ val (first, second) = split(l)
+ merge(less)(msort(less)(first), msort(less)(second))
}
} ensuring { res => res.content == l.content && res.size == l.size }
}
diff --git a/testcases/verification/list-algorithms/MergeSort.scala b/testcases/verification/list-algorithms/MergeSort.scala
index 5fc80d117c9eae3bddec01377683eac54f0c37cd..4b494b62d40b24f5ad660fbe17ea215054509168 100644
--- a/testcases/verification/list-algorithms/MergeSort.scala
+++ b/testcases/verification/list-algorithms/MergeSort.scala
@@ -1,5 +1,6 @@
-import leon.lang._
-import leon.annotation._
+import leon._
+import lang._
+import annotation._
object MergeSort {
sealed abstract class List