From 9267248b5d99dfe915bf5425f5c43476ea86b65a Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Fri, 15 Apr 2016 17:27:31 +0200
Subject: [PATCH] Type cardinality
---
src/main/scala/leon/purescala/TypeOps.scala | 27 +++++++++++++++++++++
1 file changed, 27 insertions(+)
diff --git a/src/main/scala/leon/purescala/TypeOps.scala b/src/main/scala/leon/purescala/TypeOps.scala
index bd95a8e4f..8715767c9 100644
--- a/src/main/scala/leon/purescala/TypeOps.scala
+++ b/src/main/scala/leon/purescala/TypeOps.scala
@@ -249,4 +249,31 @@ object TypeOps extends GenTreeOps[TypeTree] {
transformer.transform(e)(ids)
}
}
+
+ def typeCardinality(tp: TypeTree): Option[Int] = tp match {
+ case Untyped => Some(0)
+ case BooleanType => Some(2)
+ case UnitType => Some(1)
+ case SetType(base) =>
+ typeCardinality(base).map(b => Math.pow(2, b).toInt)
+ case FunctionType(from, to) =>
+ val t = typeCardinality(to).getOrElse(return None)
+ val f = from.map(typeCardinality).map(_.getOrElse(return None)).product
+ Some(Math.pow(t, f).toInt)
+ case MapType(from, to) =>
+ for {
+ t <- typeCardinality(to)
+ f <- typeCardinality(from)
+ } yield {
+ Math.pow(t + 1, f).toInt
+ }
+ case cct: CaseClassType =>
+ Some(cct.fields.map { field =>
+ typeCardinality(field.getType).getOrElse(return None)
+ }.product)
+ case act: AbstractClassType =>
+ Some(act.knownCCDescendants.map(typeCardinality).map(_.getOrElse(return None)).sum)
+ case _ => None
+ }
+
}
--
GitLab