From 1971c980fdb5b4260b48db664f513ee3e49ed796 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Mon, 26 Aug 2013 16:09:52 +0200
Subject: [PATCH] Add a couple of tests
---
.../leon/test/synthesis/SynthesisSuite.scala | 76 +++++++++++++++++++
1 file changed, 76 insertions(+)
diff --git a/src/test/scala/leon/test/synthesis/SynthesisSuite.scala b/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
index 610ceb3d6..0f512690d 100644
--- a/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
+++ b/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
@@ -280,4 +280,80 @@ object SortedList {
))
))
}
+
+ synthesize("Church")("""
+import leon.Utils._
+object ChurchNumerals {
+ sealed abstract class Num
+ case object Z extends Num
+ case class S(pred: Num) extends Num
+
+ def value(n:Num) : Int = {
+ n match {
+ case Z => 0
+ case S(p) => 1 + value(p)
+ }
+ } ensuring (_ >= 0)
+
+ // def add(x : Num, y : Num) : Num = (x match {
+ // case Z => y
+ // case S(p) => add(p, S(y))
+ // }) ensuring (value(_) == value(x) + value(y))
+
+ def add(x: Num, y: Num): Num = {
+ choose { (r : Num) =>
+ value(r) == value(x) + value(y)
+ }
+ }
+}
+ """) {
+ case "add" =>
+ Apply("ADT Induction on 'y'", List(
+ Apply("CEGIS"),
+ Apply("CEGIS")
+ ))
+ }
+
+ synthesize("Church")("""
+import leon.Utils._
+object ChurchNumerals {
+ sealed abstract class Num
+ case object Z extends Num
+ case class S(pred: Num) extends Num
+
+ def value(n:Num) : Int = {
+ n match {
+ case Z => 0
+ case S(p) => 1 + value(p)
+ }
+ } ensuring (_ >= 0)
+
+ def add(x : Num, y : Num) : Num = (x match {
+ case Z => y
+ case S(p) => add(p, S(y))
+ }) ensuring (value(_) == value(x) + value(y))
+
+ //def distinct(x : Num, y : Num) : Num = (x match {
+ // case Z =>
+ // S(y)
+
+ // case S(p) =>
+ // y match {
+ // case Z =>
+ // S(x)
+ // case S(p) =>
+ // Z
+ // }
+ //}) ensuring (res => res != x && res != y)
+
+ def distinct(x: Num, y: Num): Num = {
+ choose { (r : Num) =>
+ r != x && r != y
+ }
+ }
+}
+ """) {
+ case "distinct" =>
+ Apply("CEGIS")
+ }
}
--
GitLab