From 7c70cd3ae822364968d96eda728f8252dcf04492 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Mon, 7 May 2012 19:37:20 +0200
Subject: [PATCH] evaluate set cardinality in evaluator
---
src/main/scala/leon/Evaluator.scala | 8 ++++++++
1 file changed, 8 insertions(+)
diff --git a/src/main/scala/leon/Evaluator.scala b/src/main/scala/leon/Evaluator.scala
index e8409aa31..004d03d61 100644
--- a/src/main/scala/leon/Evaluator.scala
+++ b/src/main/scala/leon/Evaluator.scala
@@ -242,6 +242,14 @@ object Evaluator {
case (e, f @ FiniteSet(els)) => BooleanLiteral(els.contains(e))
case (l,r) => throw TypeErrorEx(TypeError(r, SetType(l.getType)))
}
+ case SetCardinality(s) => {
+ val sr = rec(ctx, s)
+ sr match {
+ case EmptySet(_) => IntLiteral(0)
+ case FiniteSet(els) => IntLiteral(els.size)
+ case _ => throw TypeErrorEx(TypeError(sr, SetType(AnyType)))
+ }
+ }
case f @ FiniteSet(els) => FiniteSet(els.map(rec(ctx,_)).distinct).setType(f.getType)
case e @ EmptySet(_) => e
--
GitLab