diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index 4aee2f2411567d5432be77a84de31cee7c29ed18..8abed0de05d65641950383323658ab37aaae195e 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -380,9 +380,6 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case (FiniteMap(ss), e) => BooleanLiteral(ss.exists(_._1 == e))
case (l, r) => throw EvalError(typeErrorMsg(l, m.getType))
}
- case Distinct(args) =>
- val newArgs = args.map(e(_))
- BooleanLiteral(newArgs.distinct.size == newArgs.size)
case gv: GenericValue =>
gv
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index c7bd6778b5c8330b1fa0eac42fc197ee191dc5b1..763986c39c386e51d557014dfefe1f0903e451f2 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -1569,9 +1569,6 @@ trait CodeExtraction extends ASTExtractors {
case (IsTyped(a1, at: ArrayType), "length", Nil) =>
ArrayLength(a1)
- case (IsTyped(a1, at: ArrayType), "clone", Nil) =>
- ArrayClone(a1)
-
case (IsTyped(a1, at: ArrayType), "updated", List(k, v)) =>
ArrayUpdated(a1, k, v)
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index 6df0021863297f20ecb5c5b6b3e8e5f389ea57c2..6cf4e1bbe3cf193e21276981e89bf64046c17b3c 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -27,8 +27,6 @@ object Extractors {
case CaseClassInstanceOf(cd, e) => Some((e, CaseClassInstanceOf(cd, _)))
case TupleSelect(t, i) => Some((t, tupleSelect(_, i)))
case ArrayLength(a) => Some((a, ArrayLength))
- case ArrayClone(a) => Some((a, ArrayClone))
- case ArrayMake(t) => Some((t, ArrayMake))
case Lambda(args, body) => Some((body, Lambda(args, _)))
case Forall(args, body) => Some((body, Forall(args, _)))
case (ue: UnaryExtractable) => ue.extract
@@ -126,7 +124,6 @@ object Extractors {
val tpe = leastUpperBound(as.map(_.getType)).map(ArrayType(_)).getOrElse(expr.getType)
FiniteArray(as).setType(tpe)
}))
- case Distinct(args) => Some((args, Distinct))
case Tuple(args) => Some((args, Tuple))
case IfExpr(cond, thenn, elze) => Some((Seq(cond, thenn, elze), (as: Seq[Expr]) => IfExpr(as(0), as(1), as(2))))
case MatchExpr(scrut, cases) =>
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index c34da78b44ca90edbaf2d27cb0dc3915e5495656..fe01a181b1467baa492ee9149521b5f31de6c13e 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -363,13 +363,10 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
case MapGet(m,k) => p"$m($k)"
case MapIsDefinedAt(m,k) => p"$m.isDefinedAt($k)"
case ArrayLength(a) => p"$a.length"
- case ArrayClone(a) => p"$a.clone"
case ArrayFill(size, v) => p"Array.fill($size)($v)"
- case ArrayMake(v) => p"Array.make($v)"
case ArraySelect(a, i) => p"$a($i)"
case ArrayUpdated(a, i, v) => p"$a.updated($i, $v)"
case FiniteArray(exprs) => p"Array($exprs)"
- case Distinct(exprs) => p"distinct($exprs)"
case Not(expr) => p"\u00AC$expr"
case ValDef(id, tpe) => p"${typed(id)}"
case This(_) => p"this"
diff --git a/src/main/scala/leon/purescala/ScalaPrinter.scala b/src/main/scala/leon/purescala/ScalaPrinter.scala
index d4e366d9ab35450e394232441183b89a44f1c476..b48def12d12d13469e11c178f642f1c5062c2f10 100644
--- a/src/main/scala/leon/purescala/ScalaPrinter.scala
+++ b/src/main/scala/leon/purescala/ScalaPrinter.scala
@@ -50,7 +50,6 @@ class ScalaPrinter(opts: PrinterOptions, sb: StringBuffer = new StringBuffer) ex
case SetIntersection(l,r) => p"$l & $r"
case SetCardinality(s) => p"$s.size"
case FiniteArray(exprs) => p"Array($exprs)"
- case Distinct(exprs) => p"distinct($exprs)"
case Not(expr) => p"!$expr"
case _ =>
super.pp(tree)
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index 2af53e1bf8c34ecbb7512288ff64652980374230..a6dd02d2d0e1f1bcdadee8de98e87a1ada5a4ebe 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -1173,7 +1173,6 @@ object TreeOps {
None
}
}
- case ListType(t) => mapType(t).map(ListType(_))
case SetType(t) => mapType(t).map(SetType(_))
case MultisetType(t) => mapType(t).map(MultisetType(_))
case ArrayType(t) => mapType(t).map(ArrayType(_))
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index 232786e969fb1b8c471ba260e258f500a73d12b6..94a79ca5773610ce8023f59b7f7555a56ddfd426 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -402,49 +402,6 @@ object Trees {
def getType = leastUpperBound(Seq(set1, set2).map(_.getType)).getOrElse(Untyped)
}
- @deprecated("SetMin is not supported by any solver", "2.3")
- case class SetMin(set: Expr) extends Expr {
- val getType = Int32Type
- }
-
- @deprecated("SetMax is not supported by any solver", "2.3")
- case class SetMax(set: Expr) extends Expr {
- val getType = Int32Type
- }
-
- /* Multiset expressions !!! UNSUPPORTED / DEPRECATED !!! */
- case class EmptyMultiset(baseType: TypeTree) extends Expr with Terminal {
- val getType = MultisetType(baseType)
- }
- case class FiniteMultiset(elements: Seq[Expr]) extends Expr {
- assert(elements.size > 0)
- def getType = MultisetType(leastUpperBound(elements.map(_.getType)).getOrElse(Untyped))
- }
- case class Multiplicity(element: Expr, multiset: Expr) extends Expr {
- val getType = Int32Type
- }
- case class MultisetCardinality(multiset: Expr) extends Expr {
- val getType = Int32Type
- }
- case class MultisetIntersection(multiset1: Expr, multiset2: Expr) extends Expr {
- def getType = leastUpperBound(Seq(multiset1, multiset2).map(_.getType)).getOrElse(Untyped)
- }
- case class MultisetUnion(multiset1: Expr, multiset2: Expr) extends Expr {
- def getType = leastUpperBound(Seq(multiset1, multiset2).map(_.getType)).getOrElse(Untyped)
- }
- case class MultisetPlus(multiset1: Expr, multiset2: Expr) extends Expr { // disjoint union
- def getType = leastUpperBound(Seq(multiset1, multiset2).map(_.getType)).getOrElse(Untyped)
- }
- case class MultisetDifference(multiset1: Expr, multiset2: Expr) extends Expr {
- def getType = leastUpperBound(Seq(multiset1, multiset2).map(_.getType)).getOrElse(Untyped)
- }
- case class MultisetToSet(multiset: Expr) extends Expr {
- def getType = multiset.getType match {
- case MultisetType(base) => SetType(base)
- case _ => Untyped
- }
- }
-
/* Map operations. */
case class FiniteMap(singletons: Seq[(Expr, Expr)]) extends Expr with MutableTyped
case class MapGet(map: Expr, key: Expr) extends Expr {
@@ -462,15 +419,6 @@ object Trees {
}
/* Array operations */
- @deprecated("Unsupported Array operation with most solvers", "Leon 2.3")
- case class ArrayFill(length: Expr, defaultValue: Expr) extends Expr {
- def getType = ArrayType(defaultValue.getType)
- }
-
- @deprecated("Unsupported Array operation with most solvers", "Leon 2.3")
- case class ArrayMake(defaultValue: Expr) extends Expr {
- def getType = ArrayType(defaultValue.getType)
- }
case class ArraySelect(array: Expr, index: Expr) extends Expr {
def getType = array.getType match {
@@ -496,15 +444,6 @@ object Trees {
case class FiniteArray(exprs: Seq[Expr]) extends Expr with MutableTyped
- @deprecated("Unsupported Array operation with most solvers", "Leon 2.3")
- case class ArrayClone(array: Expr) extends Expr {
- def getType = array.getType
- }
-
- case class Distinct(exprs: Seq[Expr]) extends Expr {
- val getType = BooleanType
- }
-
/* Special trees */
// Provide an oracle (synthesizable, all-seeing choose)
@@ -534,6 +473,53 @@ object Trees {
}
}
+ /**
+ * DEPRECATED TREES
+ * These trees are not guaranteed to be supported by Leon.
+ **/
+ case class ArrayFill(length: Expr, defaultValue: Expr) extends Expr {
+ def getType = ArrayType(defaultValue.getType)
+ }
+
+ case class SetMin(set: Expr) extends Expr {
+ val getType = Int32Type
+ }
+
+ case class SetMax(set: Expr) extends Expr {
+ val getType = Int32Type
+ }
+
+ case class EmptyMultiset(baseType: TypeTree) extends Expr with Terminal {
+ val getType = MultisetType(baseType)
+ }
+ case class FiniteMultiset(elements: Seq[Expr]) extends Expr {
+ assert(elements.size > 0)
+ def getType = MultisetType(leastUpperBound(elements.map(_.getType)).getOrElse(Untyped))
+ }
+ case class Multiplicity(element: Expr, multiset: Expr) extends Expr {
+ val getType = Int32Type
+ }
+ case class MultisetCardinality(multiset: Expr) extends Expr {
+ val getType = Int32Type
+ }
+ case class MultisetIntersection(multiset1: Expr, multiset2: Expr) extends Expr {
+ def getType = leastUpperBound(Seq(multiset1, multiset2).map(_.getType)).getOrElse(Untyped)
+ }
+ case class MultisetUnion(multiset1: Expr, multiset2: Expr) extends Expr {
+ def getType = leastUpperBound(Seq(multiset1, multiset2).map(_.getType)).getOrElse(Untyped)
+ }
+ case class MultisetPlus(multiset1: Expr, multiset2: Expr) extends Expr { // disjoint union
+ def getType = leastUpperBound(Seq(multiset1, multiset2).map(_.getType)).getOrElse(Untyped)
+ }
+ case class MultisetDifference(multiset1: Expr, multiset2: Expr) extends Expr {
+ def getType = leastUpperBound(Seq(multiset1, multiset2).map(_.getType)).getOrElse(Untyped)
+ }
+ case class MultisetToSet(multiset: Expr) extends Expr {
+ def getType = multiset.getType match {
+ case MultisetType(base) => SetType(base)
+ case _ => Untyped
+ }
+ }
}
diff --git a/src/main/scala/leon/purescala/TypeTrees.scala b/src/main/scala/leon/purescala/TypeTrees.scala
index 38074b978feb50eff0ffc43d9edaf4bcd1fa7981..bf448e739c3a953e8f32bb78157493b4724e46b5 100644
--- a/src/main/scala/leon/purescala/TypeTrees.scala
+++ b/src/main/scala/leon/purescala/TypeTrees.scala
@@ -76,7 +76,6 @@ object TypeTrees {
}
}
- case class ListType(base: TypeTree) extends TypeTree
case class SetType(base: TypeTree) extends TypeTree
case class MultisetType(base: TypeTree) extends TypeTree
case class MapType(from: TypeTree, to: TypeTree) extends TypeTree
@@ -143,7 +142,6 @@ object TypeTrees {
case CaseClassType(ccd, ts) => Some((ts, ts => CaseClassType(ccd, ts)))
case AbstractClassType(acd, ts) => Some((ts, ts => AbstractClassType(acd, ts)))
case TupleType(ts) => Some((ts, TupleType(_)))
- case ListType(t) => Some((Seq(t), ts => ListType(ts.head)))
case ArrayType(t) => Some((Seq(t), ts => ArrayType(ts.head)))
case SetType(t) => Some((Seq(t), ts => SetType(ts.head)))
case MultisetType(t) => Some((Seq(t), ts => MultisetType(ts.head)))
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 28b86d8f3ea9c291a7b4ee9f036890f0eb8ae910..1ee056af437a7a0ab03c6e9abf07ac0001a90a89 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -669,7 +669,6 @@ trait AbstractZ3Solver
val u = exprs.zipWithIndex.foldLeft(a)((array, expI) => ArrayUpdated(array, IntLiteral(expI._2), expI._1))
rec(u)
}
- case Distinct(exs) => z3.mkDistinct(exs.map(rec(_)): _*)
case gv @ GenericValue(tp, id) =>
z3.mkApp(genericValueToDecl(gv))
diff --git a/src/main/scala/leon/xlang/ArrayTransformation.scala b/src/main/scala/leon/xlang/ArrayTransformation.scala
index e6f31d739ced12dac775ec26de5a8b8cdb9d1178..a66541178b7e0bd962d842d005454d3a5ee1c786 100644
--- a/src/main/scala/leon/xlang/ArrayTransformation.scala
+++ b/src/main/scala/leon/xlang/ArrayTransformation.scala
@@ -41,10 +41,6 @@ object ArrayTransformation extends TransformationPhase {
val Variable(id) = ra
Assignment(id, ArrayUpdated(ra, ri, rv).setPos(up))
}
- case ArrayClone(a) => {
- val ra = transform(a)
- ra
- }
case Let(i, v, b) => {
v.getType match {
case ArrayType(_) => {
diff --git a/src/main/scala/leon/xlang/TreeOps.scala b/src/main/scala/leon/xlang/TreeOps.scala
index 40c23677e51a9eea40c40368c5409869b65df12f..b3de6e91aa99dcc0246339719cd3f24371ff254c 100644
--- a/src/main/scala/leon/xlang/TreeOps.scala
+++ b/src/main/scala/leon/xlang/TreeOps.scala
@@ -23,8 +23,6 @@ object TreeOps {
case LetVar(_, _, _) => true
case LetDef(_, _) => true
case ArrayUpdate(_, _, _) => true
- case ArrayMake(_) => true
- case ArrayClone(_) => true
case Epsilon(_) => true
case _ => false
}}(expr)
diff --git a/src/test/resources/regression/termination/valid/BubbleSort.scala b/src/test/resources/regression/termination/valid/BubbleSort.scala
deleted file mode 100644
index ff7f58e9f941d52ab981ccf014e9589e7c6542ec..0000000000000000000000000000000000000000
--- a/src/test/resources/regression/termination/valid/BubbleSort.scala
+++ /dev/null
@@ -1,76 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-import leon.lang._
-
-/* The calculus of Computation textbook */
-
-object BubbleSort {
-
- def sort(a: Array[Int]): Array[Int] = ({
- require(a.length >= 1)
- var i = a.length - 1
- var j = 0
- val sa = a.clone
- (while(i > 0) {
- j = 0
- (while(j < i) {
- if(sa(j) > sa(j+1)) {
- val tmp = sa(j)
- sa(j) = sa(j+1)
- sa(j+1) = tmp
- }
- j = j + 1
- }) invariant(
- j >= 0 &&
- j <= i &&
- i < sa.length &&
- sa.length >= 0 &&
- partitioned(sa, 0, i, i+1, sa.length-1) &&
- sorted(sa, i, sa.length-1) &&
- partitioned(sa, 0, j-1, j, j)
- )
- i = i - 1
- }) invariant(
- i >= 0 &&
- i < sa.length &&
- sa.length >= 0 &&
- partitioned(sa, 0, i, i+1, sa.length-1) &&
- sorted(sa, i, sa.length-1)
- )
- sa
- }) ensuring(res => sorted(res, 0, a.length-1))
-
- def sorted(a: Array[Int], l: Int, u: Int): Boolean = {
- require(a.length >= 0 && l >= 0 && u < a.length && l <= u)
- var k = l
- var isSorted = true
- (while(k < u) {
- if(a(k) > a(k+1))
- isSorted = false
- k = k + 1
- }) invariant(k <= u && k >= l)
- isSorted
- }
-
- def partitioned(a: Array[Int], l1: Int, u1: Int, l2: Int, u2: Int): Boolean = {
- require(a.length >= 0 && l1 >= 0 && u1 < l2 && u2 < a.length)
- if(l2 > u2 || l1 > u1)
- true
- else {
- var i = l1
- var j = l2
- var isPartitionned = true
- (while(i <= u1) {
- j = l2
- (while(j <= u2) {
- if(a(i) > a(j))
- isPartitionned = false
- j = j + 1
- }) invariant(j >= l2 && i <= u1)
- i = i + 1
- }) invariant(i >= l1)
- isPartitionned
- }
- }
-
-}
diff --git a/src/test/resources/regression/verification/xlang/valid/Array10.scala b/src/test/resources/regression/verification/xlang/valid/Array10.scala
deleted file mode 100644
index a36e980fdeadd8a82c76a8858aedcff1cb0f15aa..0000000000000000000000000000000000000000
--- a/src/test/resources/regression/verification/xlang/valid/Array10.scala
+++ /dev/null
@@ -1,11 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-object Array10 {
-
- def foo(a: Array[Int]): Int = {
- require(a.length > 0)
- val b = a.clone
- b(0)
- } ensuring(res => res == a(0))
-
-}