From f32a1e50c07fe5117bd3ffa33c16d0cf52a9c6eb Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <etienne.kneuss@epfl.ch>
Date: Thu, 18 Sep 2014 14:09:04 +0200
Subject: [PATCH] Generate Sets as well
---
src/main/scala/leon/synthesis/rules/Tegis.scala | 8 ++++++++
1 file changed, 8 insertions(+)
diff --git a/src/main/scala/leon/synthesis/rules/Tegis.scala b/src/main/scala/leon/synthesis/rules/Tegis.scala
index 0238bc643..f17f75c96 100644
--- a/src/main/scala/leon/synthesis/rules/Tegis.scala
+++ b/src/main/scala/leon/synthesis/rules/Tegis.scala
@@ -69,6 +69,14 @@ case object TEGIS extends Rule("TEGIS") {
Generator[TypeTree, Expr](cct.fields.map(_.getType), { case rs => CaseClass(cct, rs)} )
}
+ case st @ SetType(base) =>
+ List(
+ Generator(List(base), { case elems => FiniteSet(elems).setType(st) }),
+ Generator(List(st, st), { case Seq(a, b) => SetUnion(a, b) }),
+ Generator(List(st, st), { case Seq(a, b) => SetIntersection(a, b) }),
+ Generator(List(st, st), { case Seq(a, b) => SetDifference(a, b) })
+ )
+
case _ =>
Nil
}
--
GitLab