Update tests to new API

src/integration/scala/leon/integration/solvers/ModelEnumerationSuite.scala

@@ -52,13 +52,15 @@ class ModelEnumeratorSuite extends LeonTestSuiteWithProgram with ExpressionsDSL
     val cnstr = GreaterThan(fcall("List1.size")(l.toVariable), bi(2))
 
     val me = getModelEnum
+    val enum = me.enumSimple(Seq(l), cnstr)
+
     try {
-      val models = me.enumSimple(Seq(l), cnstr).take(5).toList
+      val models = enum.take(5).toList
 
       assert(models.size === 5, "We can enumerate at least 5 lists of size 3+")
       assert(models.toSet.size === 5, "Models are distinct")
     } finally {
-      me.shutdown()
+      enum.free()
     }
   }
 
@@ -70,13 +72,11 @@ class ModelEnumeratorSuite extends LeonTestSuiteWithProgram with ExpressionsDSL
 
     val me = getModelEnum
 
-    try {
-      val models = me.enumSimple(Seq(l), cnstr).take(5).toList
+    val enum = me.enumSimple(Seq(l), cnstr)
+    val models = enum.take(5).toList
+    enum.free()
 
-      assert(models.size === 1, "We can only enumerate one list of size 0")
-    } finally {
-      me.shutdown()
-    }
+    assert(models.size === 1, "We can only enumerate one list of size 0")
   }
 
   test("Varying model enumeration 1") { implicit fix =>
@@ -92,38 +92,45 @@ class ModelEnumeratorSuite extends LeonTestSuiteWithProgram with ExpressionsDSL
     val evaluator = new DefaultEvaluator(fix._1, fix._2)
     val me = getModelEnum
 
-    try {
-      // 1 model of each size
-      val models1 = me.enumVarying(Seq(l), cnstr, car).toList
-      assert(models1.size === 2, "We can enumerate 2 lists of varying size 0 < .. < 3")
+    // 1 model of each size
+    val enum1 = me.enumVarying(Seq(l), cnstr, car)
+    val models1 = enum1.toList
+    enum1.free()
 
-      // 3 models of each size
-      val models2 = me.enumVarying(Seq(l), cnstr, car, 3).toList
-      assert(models2.size === 6, "We can enumerate 6 lists of varying size 0 < .. < 3 with 3 per size")
+    assert(models1.size === 2, "We can enumerate 2 lists of varying size 0 < .. < 3")
 
+    // 3 models of each size
+    val enum2 = me.enumVarying(Seq(l), cnstr, car, 3)
+    val models2 = enum2.toList
+    enum2.free()
 
-      val car2   = fcall("List1.sum")(l.toVariable)
+    assert(models2.size === 6, "We can enumerate 6 lists of varying size 0 < .. < 3 with 3 per size")
 
-      // 1 model of each sum
-      val models3 = me.enumVarying(Seq(l), cnstr, car2).take(4).toList
-      assert(models3.size === 4, "We can enumerate >=4 lists of varying sum, with 0 < .. < 3")
 
-      val carResults3 = models3.groupBy(m => evaluator.eval(car2, m).result.get)
-      assert(carResults3.size === 4, "We should have 4 distinct sums")
-      assert(carResults3.forall(_._2.size === 1), "We should have 1 model per sum")
+    val car2   = fcall("List1.sum")(l.toVariable)
 
-      // 2 model of each sum
-      val models4 = me.enumVarying(Seq(l), cnstr, car2, 2).take(4).toList
-      assert(models4.size === 4, "We can enumerate >=4 lists of varying sum, with 0 < .. < 3")
+    // 1 model of each sum
+    val enum3 = me.enumVarying(Seq(l), cnstr, car2)
+    val models3 = enum3.take(4).toList
+    enum3.free()
 
-      val carResults4 = models4.groupBy(m => evaluator.eval(car2, m).result.get)
-      assert(carResults4.size >= 2, "We should have at least 2 distinct sums")
-      assert(carResults4.forall(_._2.size <= 2), "We should have at most 2 models per sum")
+    assert(models3.size === 4, "We can enumerate >=4 lists of varying sum, with 0 < .. < 3")
 
+    val carResults3 = models3.groupBy(m => evaluator.eval(car2, m).result.get)
+    assert(carResults3.size === 4, "We should have 4 distinct sums")
+    assert(carResults3.forall(_._2.size === 1), "We should have 1 model per sum")
+
+    // 2 model of each sum
+    val enum4 = me.enumVarying(Seq(l), cnstr, car2, 2)
+    val models4 = enum4.take(4).toList
+    enum4.free()
+
+    assert(models4.size === 4, "We can enumerate >=4 lists of varying sum, with 0 < .. < 3")
+
+    val carResults4 = models4.groupBy(m => evaluator.eval(car2, m).result.get)
+    assert(carResults4.size >= 2, "We should have at least 2 distinct sums")
+    assert(carResults4.forall(_._2.size <= 2), "We should have at most 2 models per sum")
 
-    } finally {
-      me.shutdown()
-    }
   }
 
   test("Varying model enumeration 2") { implicit fix =>
@@ -138,19 +145,19 @@ class ModelEnumeratorSuite extends LeonTestSuiteWithProgram with ExpressionsDSL
 
     val me = getModelEnum
 
-    try {
-      // 1 model of each caracteristic (which is a boolean, so only two possibilities)
-      val models3 = me.enumVarying(Seq(l), cnstr, car).take(10).toList
-      assert(models3.size === 2, "We can enumerate only 2 lists of varying size==0")
+    // 1 model of each caracteristic (which is a boolean, so only two possibilities)
+    val enum3 = me.enumVarying(Seq(l), cnstr, car)
+    val models3 = enum3.take(10).toList
+    enum3.free()
 
+    assert(models3.size === 2, "We can enumerate only 2 lists of varying size==0")
 
-      // 1 model of each caracteristic (which is a boolean, so only two possibilities)
-      val models4 = me.enumVarying(Seq(l), cnstr, car, 2).take(10).toList
-      assert(models4.size === 4, "We can enumerate only 4 lists of varying size==0 (2 each)")
 
-    } finally {
-      me.shutdown()
-    }
+    // 1 model of each caracteristic (which is a boolean, so only two possibilities)
+    val enum4 = me.enumVarying(Seq(l), cnstr, car, 2)
+    val models4 = enum4.take(10).toList
+    enum4.free()
+    assert(models4.size === 4, "We can enumerate only 4 lists of varying size==0 (2 each)")
   }
 
   test("Maximizing size") { implicit fix =>
@@ -164,20 +171,20 @@ class ModelEnumeratorSuite extends LeonTestSuiteWithProgram with ExpressionsDSL
     val evaluator = new DefaultEvaluator(fix._1, fix._2)
     val me = getModelEnum
 
-    try {
-      val models1 = me.enumMaximizing(Seq(l), cnstr, car).take(5).toList
+    val enum1 = me.enumMaximizing(Seq(l), cnstr, car)
+    val models1 = enum1.take(5).toList
+    enum1.free()
 
-      assert(models1.size < 5, "It took less than 5 models to reach max")
-      assert(evaluator.eval(car, models1.last).result === Some(bi(4)), "Max should be 4")
+    assert(models1.size < 5, "It took less than 5 models to reach max")
+    assert(evaluator.eval(car, models1.last).result === Some(bi(4)), "Max should be 4")
 
-      val models2 = me.enumMaximizing(Seq(l), BooleanLiteral(true), car).take(4).toList
+    val enum2 = me.enumMaximizing(Seq(l), BooleanLiteral(true), car)
+    val models2 = enum2.take(4).toList
+    enum2.free()
 
-      assert(models2.size == 4, "Unbounded search yields models")
-      // in 4 steps, it should reach lists of size > 10
-      assert(evaluator.eval(GreaterThan(car, bi(10)), models2.last).result === Some(T), "Progression should be efficient")
-    } finally {
-      me.shutdown()
-    }
+    assert(models2.size == 4, "Unbounded search yields models")
+    // in 4 steps, it should reach lists of size > 10
+    assert(evaluator.eval(GreaterThan(car, bi(10)), models2.last).result === Some(T), "Progression should be efficient")
   }
 
   test("Minimizing size") { implicit fix =>
@@ -191,15 +198,12 @@ class ModelEnumeratorSuite extends LeonTestSuiteWithProgram with ExpressionsDSL
     val evaluator = new DefaultEvaluator(fix._1, fix._2)
     val me = getModelEnum
 
-    try {
-      val models1 = me.enumMinimizing(Seq(l), cnstr, car).take(5).toList
-
-      assert(models1.size < 5, "It took less than 5 models to reach min")
-      assert(evaluator.eval(car, models1.last).result === Some(bi(0)), "Min should be 0")
+    val enum1 = me.enumMinimizing(Seq(l), cnstr, car)
+    val models1 = enum1.take(5).toList
+    enum1.free()
 
-    } finally {
-      me.shutdown()
-    }
+    assert(models1.size < 5, "It took less than 5 models to reach min")
+    assert(evaluator.eval(car, models1.last).result === Some(bi(0)), "Min should be 0")
   }
 
 }

src/main/scala/leon/utils/ModelEnumerator.scala

@@ -11,10 +11,9 @@ import evaluators._
 import solvers._
 
 class ModelEnumerator(ctx: LeonContext, pgm: Program, sf: SolverFactory[Solver]) {
-  private[this] var reclaimPool = List[Solver]()
   private[this] val evaluator = new DefaultEvaluator(ctx, pgm)
 
-  def enumSimple(ids: Seq[Identifier], satisfying: Expr): Iterator[Map[Identifier, Expr]] = {
+  def enumSimple(ids: Seq[Identifier], satisfying: Expr): FreeableIterator[Map[Identifier, Expr]] = {
     enumVarying0(ids, satisfying, None, -1)
   }
 
@@ -95,11 +94,10 @@ class ModelEnumerator(ctx: LeonContext, pgm: Program, sf: SolverFactory[Solver])
   case object Up   extends SearchDirection
   case object Down extends SearchDirection
 
-  private[this] def enumOptimizing(ids: Seq[Identifier], satisfying: Expr, measure: Expr, dir: SearchDirection): Iterator[Map[Identifier, Expr]] = {
+  private[this] def enumOptimizing(ids: Seq[Identifier], satisfying: Expr, measure: Expr, dir: SearchDirection): FreeableIterator[Map[Identifier, Expr]] = {
     assert(measure.getType == IntegerType)
 
     val s = sf.getNewSolver
-    reclaimPool ::= s
 
     s.assertCnstr(satisfying)
 
@@ -197,11 +195,4 @@ class ModelEnumerator(ctx: LeonContext, pgm: Program, sf: SolverFactory[Solver])
       }
     }
   }
-
-
-  def shutdown() = {
-    println("Terminating!")
-    reclaimPool.foreach(sf.reclaim)
-  }
-
 }