From df73de9390f4e0f26bac3314e189c76b561543f7 Mon Sep 17 00:00:00 2001
From: Viktor Kuncak <viktor.kuncak@epfl.ch>
Date: Wed, 30 Sep 2015 14:13:08 +0200
Subject: [PATCH] Improved the date conversion benchmark
---
testcases/synthesis/ZuneBug.scala | 31 +++++++++++++++++++++++++++++--
1 file changed, 29 insertions(+), 2 deletions(-)
diff --git a/testcases/synthesis/ZuneBug.scala b/testcases/synthesis/ZuneBug.scala
index c6ea3522b..fd4da9441 100644
--- a/testcases/synthesis/ZuneBug.scala
+++ b/testcases/synthesis/ZuneBug.scala
@@ -7,20 +7,24 @@ import leon.lang.synthesis._
*/
object ZuneBug {
+ @inline
def leapsTill(year: BigInt): BigInt = {
require(year >= 0)
val y1 = year - 1
y1/4 + y1/100 + y1/400
}
+
+ @inline
def isLeap(year: BigInt): Boolean = {
require(year >= 0)
leapsTill(year+1) > leapsTill(year)
}
- def yearDay(daysSince1980: BigInt): (BigInt, BigInt) = {
+ // wrong, accidentaly underspecified
+ def yearDayConfused(daysSince1980: BigInt): (BigInt, BigInt) = {
require(daysSince1980 >= 0)
???[(BigInt,BigInt)]
- } ensuring (res => {
+ } ensuring (res => {
val (year, day) = res
year >= 1980 &&
0 <= day && day <= 366 &&
@@ -28,4 +32,27 @@ object ZuneBug {
daysSince1980 == (year - 1980)*365 +
leapsTill(year) - leapsTill(1980) + day
})
+
+ // should be correct
+ def yearDay(daysSince1980: BigInt): (BigInt, BigInt) = {
+ require(daysSince1980 >= 0)
+ ???[(BigInt,BigInt)]
+ } ensuring (res => {
+ val (year, day) = res
+ year >= 1980 &&
+ 0 <= day && day <= 365 &&
+ (day == 365 ==> isLeap(year)) &&
+ daysSince1980 == (year - 1980)*365 +
+ leapsTill(year) - leapsTill(1980) + day
+ })
+
+ // test run-time constraint solving. smt-cvc4 seems fastest
+ def testYearDay = {
+ (yearDay(364),
+ yearDay(365),
+ yearDay(366),
+ yearDay(366+364),
+ yearDay(366+365))
+ }
+
}
--
GitLab