diff --git a/testcases/Addresses.scala b/testcases/Addresses.scala
index 82e354d7681c246bf3467a4061407d3a4e9de2f2..0eff2a4c1f472ba4dd03a0b2ae3e496ad577616d 100644
--- a/testcases/Addresses.scala
+++ b/testcases/Addresses.scala
@@ -8,10 +8,8 @@ object Addresses {
case class Cons(a:Int,b:Int,c:Int, tail:List) extends List
case class Nil() extends List
- def empty() = Set.empty[Int]
-
def setA(l:List) : Set[Int] = l match {
- case Nil() => empty
+ case Nil() => Set.empty[Int]
case Cons(a,b,c,l1) => Set(a) ++ setA(l1)
}
@@ -32,8 +30,9 @@ object Addresses {
theseAunique2(as,l1) && !(as contains a) && containsA(a,l1)
}) ensuring (res => res==theseAunique1(as,l))
- def disjoint(x:Set[Int],y:Set[Int]):Boolean =
- x.intersect(y).isEmpty
+ def disjoint(x:Set[Int],y:Set[Int]):Boolean = {
+ x ** y == Set.empty[Int]
+ }
def uniqueAbsentAs(unique:Set[Int],absent:Set[Int],l:List) : Boolean = (l match {
case Nil() => true
@@ -49,6 +48,11 @@ object Addresses {
case Cons(a,b,c,l1) => 0 <= a && 0 <= b && 0 <= c && allPos(l1)
}
+ def allEq(l:List,k:Int) : Boolean = l match {
+ case Nil() => true
+ case Cons(a,b,c,l1) => c==k && allEq(l1,k)
+ }
+
def max(x:Int,y:Int) = if (x <= y) x else y
def collectA(x:Int,l:List) : (Int,Int,List) = (l match {
@@ -66,9 +70,76 @@ object Addresses {
!setA(l1).contains(x)
})
+/*
def makeUniqueA(x:Int,l:List) : List = {
require(allPos(l))
val (b,c,l1) = collectA(x,l)
Cons(x,b,c,l1)
} ensuring(res => theseAunique1(Set(x),res))
+*/
+
+ case class AddressBook(business : List, pers : List)
+ def isValidAB(ab:AddressBook) : Boolean = {
+ allEq(ab.business,0) && allEq(ab.pers,1)
+ }
+ def setAB(l:List) : Set[(Int,Int)] = l match {
+ case Nil() => Set.empty[(Int,Int)]
+ case Cons(a,b,c,l1) => Set((a,b)) ++ setAB(l1)
+ }
+
+ def removeA(x:Int,l:List) : List = (l match {
+ case Nil() => Nil()
+ case Cons(a,b,c,l1) =>
+ if (a==x) removeA(x,l1)
+ else Cons(a,b,c,removeA(x,l1))
+ }) ensuring(res => !(setA(res) contains x))
+
+ def removeAg(x:Int,l:List,bg:Int) : List = (l match {
+ case Nil() => Nil()
+ case Cons(a,b,c,l1) =>
+ if (a==x) removeAg(x,l1,bg)
+ else Cons(a,b,c,removeAg(x,l1,bg))
+ }) ensuring (res => !(setAB(res) contains (x,bg)))
+
+ def removeA1(x:Int,l:List) : List = removeAg(x,l,0)
+
+ @induct
+ def removeAspec1(x:Int,l:List,bg:Int) : Boolean = {
+ removeAg(x,l,bg) == removeA(x,l)
+ } holds
+
+ def removeAspec2(x:Int,l:List,k:Int) : Boolean = {
+ require(allEq(l,k))
+ allEq(removeA(x,l),k)
+ } holds
+
+ def updateABC(a:Int,b:Int,c:Int,l:List) : List = ({
+ Cons(a,b,c,removeA(a,l))
+ }) ensuring (res => setAB(res) contains (a,b))
+
+ def lookupA(x:Int,l:List) : (Int,Int,Int) = {
+ require(setA(l) contains x)
+ l match {
+ case Cons(a,b,c,l1) => {
+ if (a==x) (a,b,c)
+ else lookupA(x,l1)
+ }
+ }
+ } ensuring((res:(Int,Int,Int)) => {
+ val (a,b,c) = res
+ setAB(l) contains (a,b)
+ })
+
+ def makePers(ab:AddressBook, x:Int) : AddressBook = {
+ require(isValidAB(ab) && (setA(ab.business) contains x))
+ val (a,b,c) = lookupA(x,ab.business)
+ val business1 = removeA(x, ab.business)
+ // assert(allEq(business1,0))
+ val pers1 = Cons(a,b,1,ab.pers)
+ // assert(allEq(pers1,1))
+ AddressBook(business1,pers1)
+ } ensuring (res => isValidAB(res) &&
+ (setA(ab.pers) contains x) &&
+ !(setA(ab.business) contains x))
+
}
diff --git a/testcases/TreeListSetNoDup.scala b/testcases/TreeListSetNoDup.scala
index 2a208d3d0d270a2bad6d0648bc4ce8160100bf33..b4579410996da95c5690b8ab63c357ddcd35827c 100644
--- a/testcases/TreeListSetNoDup.scala
+++ b/testcases/TreeListSetNoDup.scala
@@ -14,15 +14,6 @@ object BinaryTree {
case Cons(i, t) => Set(i) ++ l2s(t)
}
- // list of t, in order, in from of l0
- def seqWith(t:Tree,l0:List) : List = (t match {
- case Leaf() => l0
- case Node(l, v, r) => seqWith(l,Cons(v,seqWith(r,l0)))
- }) ensuring (res => l2s(res) == t2s(t) ++ l2s(l0))
-
- // list of tree t
- def t2l(t:Tree) : List = seqWith(t,Nil())
-
// l has no duplicates, nor elements from s
def noDupWith(l:List,s:Set[Int]) : Boolean = l match {
case Nil() => true
@@ -76,6 +67,15 @@ object BinaryTree {
case Node(l, v, r) => t2s(l) ++ Set(v) ++ t2s(r)
}
+ // list of t, in order, in from of l0
+ def seqWith(t:Tree,l0:List) : List = (t match {
+ case Leaf() => l0
+ case Node(l, v, r) => seqWith(l,Cons(v,seqWith(r,l0)))
+ }) ensuring (res => l2s(res) == t2s(t) ++ l2s(l0))
+
+ // list of tree t
+ def t2l(t:Tree) : List = seqWith(t,Nil())
+
// list of elements of t, in order, without duplicates, in front of l0
def seqNoDup(t:Tree,l0:List,s0:Set[Int]) : (List,Set[Int]) = ({
require(l2s(l0).subsetOf(s0) && noDup(l0))
diff --git a/testcases/synthesis/NewYearsSong.scala b/testcases/synthesis/NewYearsSong.scala
new file mode 100644
index 0000000000000000000000000000000000000000..175be9add2a58ceb0a2a866e0163edb952a5143a
--- /dev/null
+++ b/testcases/synthesis/NewYearsSong.scala
@@ -0,0 +1,28 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object NewYearSong {
+
+ def computeLines(eLines: Int,
+ iLines: Int,
+ iSyls: Int,
+ nSyls: Int) : (Int,Int,Int,Int,Int,Int) = {
+ choose((line7: Int,
+ line8: Int,
+ nsLines: Int,
+ nLines: Int,
+ tLines: Int,
+ tLinesFact: Int) => (
+ tLines == eLines + nLines
+ && nLines == iLines + nsLines
+ && nLines == line7 + line8
+ && nSyls + iSyls == 7 * line7 + 8 * line8
+ && tLines == 4 * tLinesFact // expresses (4 | tLines)
+ && line8 >= 0
+ && line7 >= 0
+ && tLines >= 0
+ ))
+ }
+
+}
diff --git a/testcases/synthesis/cav2013/SynAddresses.scala b/testcases/synthesis/cav2013/SynAddresses.scala
new file mode 100644
index 0000000000000000000000000000000000000000..b1fb6cf2f3b7b7ecb9f8f7a9f71bc7d3574376ce
--- /dev/null
+++ b/testcases/synthesis/cav2013/SynAddresses.scala
@@ -0,0 +1,86 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object Addresses {
+ // list of integers
+ sealed abstract class List
+ case class Cons(a:Int,b:Int,c:Int, tail:List) extends List
+ case class Nil() extends List
+
+ def setA(l:List) : Set[Int] = l match {
+ case Nil() => Set.empty[Int]
+ case Cons(a,b,c,l1) => Set(a) ++ setA(l1)
+ }
+
+ def allEq(l:List,k:Int) : Boolean = l match {
+ case Nil() => true
+ case Cons(a,b,c,l1) => c==k && allEq(l1,k)
+ }
+
+ def containsA(x:Int,l:List) : Boolean = (l match {
+ case Nil() => false
+ case Cons(a,b,c,t) => a==x || containsA(x,t)
+ }) ensuring (res => res == (setA(l) contains x))
+
+ def containsA_syn(x:Int,l:List) : Boolean = choose((res:Boolean) =>
+ res == (setA(l) contains x)
+ )
+
+ case class AddressBook(business : List, pers : List)
+ def isValidAB(ab:AddressBook) : Boolean = {
+ allEq(ab.business,0) && allEq(ab.pers,1)
+ }
+ def setAB(l:List) : Set[(Int,Int)] = l match {
+ case Nil() => Set.empty[(Int,Int)]
+ case Cons(a,b,c,l1) => Set((a,b)) ++ setAB(l1)
+ }
+
+ def removeA(x:Int,l:List) : List = (l match {
+ case Nil() => Nil()
+ case Cons(a,b,c,l1) =>
+ if (a==x) removeA(x,l1)
+ else Cons(a,b,c,removeA(x,l1))
+ }) ensuring(res => !(setA(res) contains x))
+
+ def lookupA(x:Int,l:List) : (Int,Int,Int) = {
+ require(setA(l) contains x)
+ l match {
+ case Cons(a,b,c,l1) => {
+ if (a==x) (a,b,c)
+ else lookupA(x,l1)
+ }
+ }
+ } ensuring((res:(Int,Int,Int)) => {
+ val (a,b,c) = res
+ (a==x) && (setAB(l) contains (a,b))
+ })
+
+ def lookupA_syn(x:Int,l:List) : (Int,Int,Int) = {
+ require(setA(l) contains x)
+ choose((res:(Int,Int,Int)) => {
+ val (a,b,c) = res
+ (x == a) && (setAB(l) contains (a,b))
+ })
+ }
+
+ def makePers(ab:AddressBook, x:Int) : AddressBook = {
+ require(isValidAB(ab) && (setA(ab.business) contains x))
+ val (a,b,c) = lookupA(x,ab.business)
+ val business1 = removeA(x, ab.business)
+ // assert(allEq(business1,0))
+ val pers1 = Cons(a,b,1,ab.pers)
+ // assert(allEq(pers1,1))
+ AddressBook(business1,pers1)
+ } ensuring (res => isValidAB(res) &&
+ (setA(res.pers) contains x) &&
+ !(setA(res.business) contains x))
+
+ def makePers_syn(ab:AddressBook, x:Int) : AddressBook = {
+ require(isValidAB(ab) && (setA(ab.business) contains x))
+ choose((res:AddressBook) => isValidAB(res) &&
+ (setA(res.pers) contains x) &&
+ !(setA(res.business) contains x))
+ }
+
+}
diff --git a/testcases/synthesis/cav2013/SynTreeListSet.scala b/testcases/synthesis/cav2013/SynTreeListSet.scala
new file mode 100644
index 0000000000000000000000000000000000000000..5639d9799cad085df44a05953daade15125a1102
--- /dev/null
+++ b/testcases/synthesis/cav2013/SynTreeListSet.scala
@@ -0,0 +1,103 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object BinaryTree {
+ // list of integers
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case class Nil() extends List
+
+ def size(l:List): Int = (l match {
+ case Nil() => 0
+ case Cons(h,t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def size_syn(l:List):Int = choose((k:Int) =>
+ k >= 0 &&
+ (l match {
+ case Nil() => k==0
+ case Cons(_,Nil()) => k==1
+ case Cons(_,Cons(_,Nil())) => k==2
+ case Cons(_,Cons(_,Cons(_,Nil()))) => k > 2
+ case _ => true
+ })
+ )
+
+ // set of elements from l
+ def l2s(l: List): Set[Int] = l match {
+ case Nil() => Set()
+ case Cons(i, t) => Set(i) ++ l2s(t)
+ }
+
+ def l2s_syn(l:List):Set[Int] = {
+ choose((res:Set[Int]) =>
+ l match {
+ case Nil() => (res==Set.empty[Int])
+ case Cons(x,Nil()) => res==Set(x)
+ case Cons(x,Cons(y,Nil())) => res==Set(x,y)
+ case Cons(x1,Cons(x2,Cons(x3,Cons(x4,Nil())))) => res==Set(x1,x2,x3,x4)
+ case _ => true
+ }
+ )
+ }
+
+/* // For this, use the passes branch.
+ def l2s_syn(l:List):Set[Int] = {
+ choose((res:Set[Int]) =>
+ passes(Map[List,Set[Int]](
+ Nil() -> Set.empty[Int],
+ Cons(100,Nil()) -> Set(100),
+ Cons(200,Nil()) -> Set(200),
+ Cons(300,Nil()) -> Set(300),
+ Cons(1,Cons(2,Nil())) -> Set(1,2),
+ Cons(100,Cons(200,Nil())) -> Set(100,200),
+ Cons(1,Cons(2,Cons(3,Cons(4,Nil())))) -> Set(1,2,3,4)),
+ l, res))
+ }
+*/
+
+ def l2s_syn2(l:List):Set[Int] = {
+ choose((res:Set[Int]) => l2s(l)==res)
+ }
+
+ // tree of integers
+ sealed abstract class Tree
+ case class Node(left : Tree, value : Int, right : Tree) extends Tree
+ case class Leaf() extends Tree
+
+ // set of elements from t
+ def t2s(t : Tree): Set[Int] = t match {
+ case Leaf() => Set.empty[Int]
+ case Node(l, v, r) => t2s(l) ++ Set(v) ++ t2s(r)
+ }
+
+ def t2s_syn(t:Tree) : Set[Int] = choose((res:Set[Int]) =>
+ t match {
+ case Leaf() => res==Set.empty[Int]
+ case Node(Leaf(),v,Leaf()) => res==Set(v)
+ case Node(Node(Leaf(),v1,Leaf()),v2,Leaf()) => res==Set(v1,v2)
+ case Node(Leaf(),v1,Node(Leaf(),v2,Leaf())) => res==Set(v1,v2)
+ case _ => true
+ }
+ )
+
+ // list of t, in order, in from of l0
+ // list of t, in order, in from of l0
+ def seqWith(t:Tree,l0:List) : List = (t match {
+ case Leaf() => l0
+ case Node(l, v, r) => seqWith(l,Cons(v,seqWith(r,l0)))
+ }) ensuring (res => l2s(res) == t2s(t) ++ l2s(l0))
+
+ def seqWith_syn(t:Tree,l0:List) : List =
+ choose((res:List) =>
+ l2s(res) == t2s(t) ++ l2s(l0))
+
+ // list of tree t
+ def t2l(t:Tree) : List = ({
+ seqWith(t,Nil())
+ }) ensuring (res => l2s(res)==t2s(t))
+
+ def t2l_syn(t:Tree) : List =
+ choose((res:List) => l2s(res)==t2s(t))
+}