From 7b4600e566e12f4ef59a6ed91feb6192ab4a3a82 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Fri, 6 Nov 2015 17:58:46 +0100
Subject: [PATCH] Set cardinality is a bigint, and we map it to CVC4's card
---
library/lang/Set.scala | 1 +
src/main/java/leon/codegen/runtime/Set.java | 6 +++---
src/main/scala/leon/codegen/CodeGeneration.scala | 2 +-
src/main/scala/leon/evaluators/RecursiveEvaluator.scala | 2 +-
.../scala/leon/frontends/scalac/CodeExtraction.scala | 9 ++++++++-
src/main/scala/leon/purescala/Expressions.scala | 2 +-
.../scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala | 3 +++
7 files changed, 18 insertions(+), 7 deletions(-)
diff --git a/library/lang/Set.scala b/library/lang/Set.scala
index 36c70a837..8f4595d33 100644
--- a/library/lang/Set.scala
+++ b/library/lang/Set.scala
@@ -17,6 +17,7 @@ case class Set[T](val theSet: scala.collection.immutable.Set[T]) {
def ++(a: Set[T]): Set[T] = new Set[T](theSet ++ a.theSet)
def -(a: T): Set[T] = new Set[T](theSet - a)
def --(a: Set[T]): Set[T] = new Set[T](theSet -- a.theSet)
+ def size: BigInt = theSet.size
def contains(a: T): Boolean = theSet.contains(a)
def isEmpty: Boolean = theSet.isEmpty
def subsetOf(b: Set[T]): Boolean = theSet.subsetOf(b.theSet)
diff --git a/src/main/java/leon/codegen/runtime/Set.java b/src/main/java/leon/codegen/runtime/Set.java
index 965aa20df..522dbe658 100644
--- a/src/main/java/leon/codegen/runtime/Set.java
+++ b/src/main/java/leon/codegen/runtime/Set.java
@@ -49,8 +49,8 @@ public final class Set {
return true;
}
- public int size() {
- return _underlying.size();
+ public BigInt size() {
+ return new BigInt(""+_underlying.size());
}
public Set union(Set s) {
@@ -84,7 +84,7 @@ public final class Set {
Set other = (Set)that;
- return this.size() == other.size() && this.subsetOf(other);
+ return this.size().equals(other.size()) && this.subsetOf(other);
}
@Override
diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index 6543da029..85ed5eb0b 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -654,7 +654,7 @@ trait CodeGeneration {
case SetCardinality(s) =>
mkExpr(s, ch)
- ch << InvokeVirtual(SetClass, "size", "()I")
+ ch << InvokeVirtual(SetClass, "size", s"()$BigIntClass;")
case SubsetOf(s1, s2) =>
mkExpr(s1, ch)
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index 216f51c5d..fccda2aea 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -504,7 +504,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case SetCardinality(s) =>
val sr = e(s)
sr match {
- case FiniteSet(els, _) => IntLiteral(els.size)
+ case FiniteSet(els, _) => InfiniteIntegerLiteral(els.size)
case _ => throw EvalError(typeErrorMsg(sr, SetType(Untyped)))
}
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 0a75dfebc..77a6c719f 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -1623,6 +1623,9 @@ trait CodeExtraction extends ASTExtractors {
or(a1, a2)
// Set methods
+ case (IsTyped(a1, SetType(b1)), "size", Nil) =>
+ SetCardinality(a1)
+
//case (IsTyped(a1, SetType(b1)), "min", Nil) =>
// SetMin(a1)
@@ -1842,7 +1845,11 @@ trait CodeExtraction extends ASTExtractors {
case AnnotatedType(_, tpe) => extractType(tpe)
case _ =>
- outOfSubsetError(tpt.typeSymbol.pos, "Could not extract type as PureScala: "+tpt+" ("+tpt.getClass+")")
+ if (tpt ne null) {
+ outOfSubsetError(tpt.typeSymbol.pos, "Could not extract type as PureScala: "+tpt+" ("+tpt.getClass+")")
+ } else {
+ outOfSubsetError(NoPosition, "Tree with null-pointer as type found")
+ }
}
private def getClassType(sym: Symbol, tps: List[LeonType])(implicit dctx: DefContext) = {
diff --git a/src/main/scala/leon/purescala/Expressions.scala b/src/main/scala/leon/purescala/Expressions.scala
index b834eb9f1..6e9adae5f 100644
--- a/src/main/scala/leon/purescala/Expressions.scala
+++ b/src/main/scala/leon/purescala/Expressions.scala
@@ -765,7 +765,7 @@ object Expressions {
}
/** $encodingof `set.length` */
case class SetCardinality(set: Expr) extends Expr {
- val getType = Int32Type
+ val getType = IntegerType
}
/** $encodingof `set.subsetOf(set2)` */
case class SubsetOf(set1: Expr, set2: Expr) extends Expr {
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
index cb1c3246d..3173dd652 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
@@ -138,6 +138,9 @@ trait SMTLIBCVC4Target extends SMTLIBTarget {
case ElementOfSet(e, s) =>
FunctionApplication(SSymbol("member"), Seq(toSMT(e), toSMT(s)))
+ case SetCardinality(s) =>
+ FunctionApplication(SSymbol("card"), Seq(toSMT(s)))
+
case SetDifference(a, b) =>
FunctionApplication(SSymbol("setminus"), Seq(toSMT(a), toSMT(b)))
--
GitLab