From a3e44cf33e3f2b1c640e0890c3b94b63251858ff Mon Sep 17 00:00:00 2001
From: Viktor Kuncak <vkuncak@gmail.com>
Date: Fri, 11 Jan 2013 14:24:43 +0100
Subject: [PATCH] Benchmark: Incremen Time, or Sequence of Times. Combine ADTs
and Int
---
testcases/synthesis/cav2013/ManyTimeSec.scala | 77 +++++++++++++++++++
1 file changed, 77 insertions(+)
create mode 100644 testcases/synthesis/cav2013/ManyTimeSec.scala
diff --git a/testcases/synthesis/cav2013/ManyTimeSec.scala b/testcases/synthesis/cav2013/ManyTimeSec.scala
new file mode 100644
index 000000000..ef521e146
--- /dev/null
+++ b/testcases/synthesis/cav2013/ManyTimeSec.scala
@@ -0,0 +1,77 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object ManyTimeSec {
+ case class Time(h:Int,m:Int,s:Int)
+ case class Seconds(total:Int)
+
+ def timeAndSec(t:Time,seconds:Seconds) : Boolean = {
+ 3600*t.h + 60*t.m + t.s == seconds.total &&
+ t.h >= 0 && t.m >= 0 && t.m < 60 && t.s >= 0 && t.s < 60
+ }
+ def time2sec(t:Time) : Seconds =
+ choose((seconds:Seconds) => timeAndSec(t,seconds))
+ def sec2time(seconds:Seconds):Time =
+ choose((t:Time) => timeAndSec(t,seconds))
+ def incTime(t0:Time,k:Int) : Time =
+ choose((t1:Time) => time2sec(t1).total == time2sec(t0).total + k)
+
+ def incTime2(h1:Int,m1:Int,s1:Int,k:Int) : (Int,Int,Int) = {
+ require(0 <= k && 0 <= h1 && 0 <= m1 && m1 < 60 && 0 <= s1 && s1 < 60)
+ choose((h2:Int,m2:Int,s2:Int) =>
+ 0 <= m2 && m2 < 60 && 0 <= s2 && s2 < 60 &&
+ 3600*h2+60*m2+s2 == 3600*h1+60*m1+s1 + k)
+ }
+
+ def incTime2one(h1:Int,m1:Int,s1:Int) : (Int,Int,Int) = {
+ require(0 <= h1 && 0 <= m1 && m1 < 60 && 0 <= s1 && s1 < 60)
+ choose((h2:Int,m2:Int,s2:Int) =>
+ 0 <= m2 && m2 < 60 && 0 <= s2 && s2 < 60 &&
+ 3600*h2+60*m2+s2 == 3600*h1+60*m1+s1 + 1)
+ }
+
+ // Yes, we can, do it without multiply and divide
+ def incTime3one(h1:Int,m1:Int,s1:Int) : (Int,Int,Int) = {
+ require(0 <= h1 && 0 <= m1 && m1 < 60 && 0 <= s1 && s1 < 60)
+ if (s1 + 1 < 60)
+ (h1,m1,s1+1)
+ else
+ if (m1 + 1 < 60)
+ (h1,m1+1,0)
+ else
+ (h1+1,0,0)
+ } ensuring(res => {
+ val (h2,m2,s2) = res
+ 0 <= m2 && m2 < 60 && 0 <= s2 && s2 < 60 &&
+ 3600*h2+60*m2+s2 == 3600*h1+60*m1+s1 + 1
+ })
+
+ case class RedundantTime(t:Time, s:Seconds)
+ def isOkRT(rt:RedundantTime) : Boolean = timeAndSec(rt.t, rt.s)
+
+ def incRT(rt0:RedundantTime, k:Int) : RedundantTime = {
+ require(isOkRT(rt0))
+ choose((rt1:RedundantTime) => isOkRT(rt1) && rt1.s.total == rt0.s.total + k)
+ }
+
+ abstract class RedundantTimeList
+ case class Nil() extends RedundantTimeList
+ case class Cons(head:RedundantTime,tail:RedundantTimeList) extends RedundantTimeList
+
+ def isInced(l1:RedundantTimeList, k:Int, l2:RedundantTimeList) : Boolean = {
+ (l1,l2) match {
+ case (Nil(),Nil()) => true
+ case (Cons(rt1,rest1),Cons(rt2,rest2)) => {
+ isOkRT(rt1) && isOkRT(rt2) &&
+ (rt2.s.total == rt2.s.total + k) &&
+ isInced(rest1,k,rest2)
+ }
+ case _ => false
+ }
+ }
+
+ def incAll(l:RedundantTimeList, k:Int) : RedundantTimeList =
+ choose((res:RedundantTimeList) => isInced(l,k,res))
+
+}
--
GitLab