From 019e5db7b5ba002d7a6467ef34aa18fcbdcfa8e5 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Mon, 28 Sep 2015 14:29:54 +0200
Subject: [PATCH] Add new sygus testcases
---
testcases/synthesis/sygus/duration.scala | 65 ++++++++++++++++++++++++
testcases/synthesis/sygus/mirror.scala | 42 +++++++++++++++
2 files changed, 107 insertions(+)
create mode 100644 testcases/synthesis/sygus/duration.scala
create mode 100644 testcases/synthesis/sygus/mirror.scala
diff --git a/testcases/synthesis/sygus/duration.scala b/testcases/synthesis/sygus/duration.scala
new file mode 100644
index 000000000..06a9b9cd5
--- /dev/null
+++ b/testcases/synthesis/sygus/duration.scala
@@ -0,0 +1,65 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+
+object Times {
+ case class Hour(v: BigInt) {
+ def isValid = v >= 0// && v < 24
+ def toSeconds = v*3600
+ }
+
+ case class Minute(v: BigInt) {
+ def isValid = v >= 0 && v < 60
+ def toSeconds = v*60
+ }
+
+ case class Second(v: BigInt) {
+ def isValid = v >= 0 && v < 60
+ def toSeconds = v
+ }
+
+ case class Time(h: Hour, m: Minute, s: Second) {
+ def isValid = {
+ h.isValid && m.isValid && s.isValid
+ }
+
+ def toSeconds = h.toSeconds + m.toSeconds + s.toSeconds
+ }
+
+ def incTime(t: Time, k: BigInt) = {
+ choose((tres: Time, seconds: BigInt) => seconds == t.toSeconds && seconds + k == tres.toSeconds && tres.isValid)
+ }
+
+ def incTimeInlined(h: BigInt, m: BigInt, s: BigInt, inc: BigInt) = {
+ require(
+ h >= 0 &&
+ m >= 0 && m < 60 &&
+ s >= 0 && s < 60 &&
+ inc > 0
+ )
+
+ choose { (hres: BigInt, mres: BigInt, sres: BigInt) =>
+ hres >= 0 &&
+ mres >= 0 && mres < 60 &&
+ sres >= 0 && sres < 60 &&
+ ((hres*3600+mres*60+sres) == ((h*3600 + m*60 + s) + inc))
+ }
+ }
+
+ def incTime2(m: BigInt, s: BigInt, inc: BigInt) = {
+ require(
+ m >= 0 &&
+ s >= 0 && s < 60 &&
+ inc > 0
+ )
+
+ ???[(BigInt, BigInt)]
+
+ } ensuring { (res: (BigInt, BigInt)) =>
+ val (mres, sres) = res
+
+ mres >= 0 &&
+ sres >= 0 && sres < 60 &&
+ ((mres*60+sres) == ((m*60 + s) + inc))
+ }
+}
diff --git a/testcases/synthesis/sygus/mirror.scala b/testcases/synthesis/sygus/mirror.scala
new file mode 100644
index 000000000..79528809a
--- /dev/null
+++ b/testcases/synthesis/sygus/mirror.scala
@@ -0,0 +1,42 @@
+import leon._
+import leon.lang._
+import leon.collection._
+import leon.lang.synthesis._
+
+object Mirror {
+
+ def inttuple(a: BigInt, b: BigInt): (BigInt, BigInt) = {
+ ???[(BigInt, BigInt)]
+ } ensuring {
+ out => out._1+1 == a && out._2-1 == b
+ }
+
+ def tuple(a: List[BigInt], b: List[BigInt]): (List[BigInt], List[BigInt]) = {
+ ???[(List[BigInt], List[BigInt])]
+ } ensuring {
+ out => out._1 == a && out._2 == b
+ }
+
+ def mirror1(a: List[BigInt], b: List[BigInt]): (List[BigInt], List[BigInt]) = {
+ ???[(List[BigInt], List[BigInt])]
+ } ensuring {
+ out => out._1 == b && out._2 == a
+ }
+
+ def mirror2[T](a: List[T], b: List[T]): (List[T], List[T]) = {
+ ???[(List[T], List[T])]
+ } ensuring {
+ out => out._1 == b && out._2 == a
+ }
+
+ def transfer(a: List[BigInt], b: List[BigInt]): (List[BigInt], List[BigInt]) = {
+ ???[(List[BigInt], List[BigInt])]
+ } ensuring {
+ out =>
+ (a, b) match {
+ case (Cons(ah, at), b) => (out._2.head == (ah + 1)) && (out._2.tail == b)
+ case _ => true
+ }
+ }
+
+}
--
GitLab