Skip to content
Snippets Groups Projects
Commit 019e5db7 authored by Etienne Kneuss's avatar Etienne Kneuss
Browse files

Add new sygus testcases

parent b0289e1f
Branches
No related tags found
No related merge requests found
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))
}
}
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
}
}
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment