From 51a4db480329ac3c4565755bacebaecc8933d7c0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <mikael.mayer@epfl.ch>
Date: Wed, 20 Apr 2016 10:25:23 +0200
Subject: [PATCH] Corrected type cardinality
---
src/main/scala/leon/purescala/TypeOps.scala | 14 ++++++++++++--
1 file changed, 12 insertions(+), 2 deletions(-)
diff --git a/src/main/scala/leon/purescala/TypeOps.scala b/src/main/scala/leon/purescala/TypeOps.scala
index 8715767c9..546e57263 100644
--- a/src/main/scala/leon/purescala/TypeOps.scala
+++ b/src/main/scala/leon/purescala/TypeOps.scala
@@ -268,10 +268,20 @@ object TypeOps extends GenTreeOps[TypeTree] {
Math.pow(t + 1, f).toInt
}
case cct: CaseClassType =>
- Some(cct.fields.map { field =>
- typeCardinality(field.getType).getOrElse(return None)
+ Some(cct.fieldsTypes.map { tpe =>
+ typeCardinality(tpe).getOrElse(return None)
}.product)
case act: AbstractClassType =>
+ val possibleChildTypes = leon.utils.fixpoint((tpes: Set[TypeTree]) => {
+ tpes.flatMap(tpe =>
+ Set(tpe) ++ (tpe match {
+ case cct: CaseClassType => cct.fieldsTypes
+ case act: AbstractClassType => Set(act) ++ act.knownCCDescendants
+ case _ => Set.empty
+ })
+ )
+ })(act.knownCCDescendants.toSet)
+ if(possibleChildTypes(act)) return None
Some(act.knownCCDescendants.map(typeCardinality).map(_.getOrElse(return None)).sum)
case _ => None
}
--
GitLab