diff --git a/src/main/scala/leon/Evaluator.scala b/src/main/scala/leon/Evaluator.scala index e8409aa317356679938accb064985c284e1e0e23..004d03d6159e07d78dc0b508af3196a5970b66d6 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