diff --git a/src/integration/scala/leon/integration/solvers/ModelEnumerationSuite.scala b/src/integration/scala/leon/integration/solvers/ModelEnumerationSuite.scala
index e17ce6d713fac45ca05c90129918da5f4296ba7c..eccec9b245d698f7de22a80166a95a0ffec71b89 100644
--- a/src/integration/scala/leon/integration/solvers/ModelEnumerationSuite.scala
+++ b/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")
}
}
diff --git a/src/main/scala/leon/utils/ModelEnumerator.scala b/src/main/scala/leon/utils/ModelEnumerator.scala
index 7429c247f78d69e4a70036d88d3b29471127d14f..d492826396674077a9351d5c771aebe0c056875c 100644
--- a/src/main/scala/leon/utils/ModelEnumerator.scala
+++ b/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)
- }
-
}