diff --git a/src/main/scala/leon/synthesis/rules/Tegis.scala b/src/main/scala/leon/synthesis/rules/Tegis.scala index 0238bc6435da175c57f07909cdeb11343390148f..f17f75c960319464ba0fac0eae2e7f5a9ac65661 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 }