Merge branch 'master' of laragit.epfl.ch:projects/leon-2.0

src/test/scala/leon/test/solvers/z3/BugWithEmptySet.scala

+package leon.test.solvers.z3
+
+import leon.purescala.Common._
+import leon.purescala.Definitions._
+import leon.purescala.Trees._
+import leon.purescala.TreeOps._
+import leon.purescala.TypeTrees._
+
+import leon.SilentReporter
+
+import leon.solvers.Solver
+import leon.solvers.z3.UninterpretedZ3Solver
+
+import org.scalatest.FunSuite
+
+class BugWithEmptySet extends FunSuite {
+  private val emptyProgram = Program(FreshIdentifier("empty"), ObjectDef(FreshIdentifier("empty"), Nil, Nil))
+
+  test("No distinction between Set() and Set.empty") {
+    val tInt = Int32Type
+    val tIntSet = SetType(Int32Type)
+
+    val e1 = EmptySet(tInt).setType(tIntSet)
+    assert(e1.getType === tIntSet)
+
+    val e2 = FiniteSet(Nil).setType(tIntSet)
+    assert(e2.getType === tIntSet)
+
+    val s0 = FiniteSet(Seq(IntLiteral(0))).setType(tIntSet)
+
+    val f1 = Equals(e1, e2)
+
+    val silentReporter = new SilentReporter
+    val solver : Solver = new UninterpretedZ3Solver(silentReporter)
+    solver.setProgram(emptyProgram)
+
+    assert(solver.solve(f1) === Some(true),
+           "Z3 should prove the equivalence between Ø and {}.")
+
+    val f2 = Equals(e1, SetDifference(e1, s0))
+
+    assert(solver.solve(f2) === Some(true),
+           """Z3 should prove Ø = Ø \ {0}""")
+
+    val f3 = Equals(e2, SetDifference(e2, s0))
+
+    assert(solver.solve(f3) === Some(true),
+           """Z3 should prove {} = {} \ {0}""")
+  } 
+}

testcases/synthesis/BinaryTree.scala

+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object BinaryTree {
+  sealed abstract class Tree
+  case class Node(left : Tree, value : Int, right : Tree) extends Tree
+  case class Leaf() extends Tree
+
+  def content(t : Tree): Set[Int] = t match {
+    case Leaf() => Set.empty[Int]
+    case Node(l, v, r) => content(l) ++ Set(v) ++ content(r)
+  }
+
+  def delete(in : Tree, v : Int) = choose { (out : Tree) =>
+    content(out) == (content(in) -- Set(v))
+  }
+}