From 8f5e5f7674d6a0035f3446566926e9abb12c7324 Mon Sep 17 00:00:00 2001
From: Viktor Kuncak <vkuncak@gmail.com>
Date: Sat, 15 Dec 2012 17:26:22 +0100
Subject: [PATCH] Church numeral benchmark for synthesis based on abstraction
functions
---
testcases/synthesis/ChurchNumerals.scala | 21 +++++++++++++++++++++
1 file changed, 21 insertions(+)
create mode 100644 testcases/synthesis/ChurchNumerals.scala
diff --git a/testcases/synthesis/ChurchNumerals.scala b/testcases/synthesis/ChurchNumerals.scala
new file mode 100644
index 000000000..229d79945
--- /dev/null
+++ b/testcases/synthesis/ChurchNumerals.scala
@@ -0,0 +1,21 @@
+import leon.Utils._
+object ChurchNumerals {
+ sealed abstract class Num
+ case class Zero() extends Num
+ case class Succ(pred:Num) extends Num
+
+ def value(n:Num) : Int = {
+ n match {
+ case Zero() => 0
+ case Succ(p) => 1 + value(p)
+ }
+ } ensuring (_ >= 0)
+
+ def succ(n:Num) : Num = Succ(n) ensuring(value(_) == value(n) + 1)
+
+ def add(x:Num, y:Num):Num = {
+ choose { (r : Num) =>
+ value(r) == value(x) + value(y)
+ }
+ }
+}
--
GitLab