diff --git a/src/integration/scala/leon/test/solvers/ModelEnumerationSuite.scala b/src/integration/scala/leon/test/solvers/ModelEnumerationSuite.scala
new file mode 100644
index 0000000000000000000000000000000000000000..9d1b16019f563a42e86ba695a65bf75530ca12c9
--- /dev/null
+++ b/src/integration/scala/leon/test/solvers/ModelEnumerationSuite.scala
@@ -0,0 +1,152 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon.test.purescala
+
+import leon.test._
+import leon._
+import leon.solvers._
+import leon.purescala.Definitions._
+import leon.purescala.Common._
+import leon.evaluators._
+import leon.purescala.Expressions._
+
+class ModelEnumeratorSuite extends LeonTestSuiteWithProgram with helpers.ExpressionsDSL {
+ val sources = List(
+ """|import leon.lang._
+ |import leon.annotation._
+ |
+ |object List1 {
+ | abstract class List
+ | case class Cons(h: BigInt, t: List) extends List
+ | case object Nil extends List
+ |
+ | def size(l: List): BigInt = {
+ | l match {
+ | case Cons(h, t) => BigInt(1) + size(t)
+ | case Nil => BigInt(0)
+ | }
+ | } ensuring { _ >= 0 }
+ |
+ | def sum(l: List): BigInt = l match {
+ | case Cons(h, t) => h + size(t)
+ | case Nil => 0
+ | }
+ |
+ | def sumAndSize(l: List) = (size(l), sum(l))
+ |
+ |} """.stripMargin
+ )
+
+ def getModelEnum(implicit ctx: LeonContext, pgm: Program) = {
+ new ModelEnumerator(ctx, pgm, SolverFactory.getFromSettings)
+ }
+
+ test("Simple model enumeration 1") { implicit fix =>
+ val tpe = classDef("List1.List").typed
+ val l = FreshIdentifier("l", tpe)
+
+ val cnstr = GreaterThan(fcall("List1.size")(l.toVariable), bi(2))
+
+ val me = getModelEnum
+ try {
+ val models = me.enumSimple(Seq(l), cnstr).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()
+ }
+ }
+
+ test("Simple model enumeration 2") { implicit fix =>
+ val tpe = classDef("List1.List").typed
+ val l = FreshIdentifier("l", tpe)
+
+ val cnstr = Equals(fcall("List1.size")(l.toVariable), bi(0))
+
+ val me = getModelEnum
+
+ try {
+ val models = me.enumSimple(Seq(l), cnstr).take(5).toList
+
+ assert(models.size === 1, "We can only enumerate one list of size 0")
+ } finally {
+ me.shutdown()
+ }
+ }
+
+ test("Varying model enumeration 1") { implicit fix =>
+ val tpe = classDef("List1.List").typed
+ val l = FreshIdentifier("l", tpe)
+
+ // 0 < list.size < 3
+ val cnstr = And(GreaterThan(fcall("List1.size")(l.toVariable), bi(0)),
+ LessThan(fcall("List1.size")(l.toVariable), bi(3)))
+
+ val car = fcall("List1.size")(l.toVariable)
+
+ 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")
+
+ // 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")
+
+
+ val car2 = fcall("List1.sum")(l.toVariable)
+
+ // 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")
+
+ // 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")
+
+ 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 =>
+ val tpe = classDef("List1.List").typed
+ val l = FreshIdentifier("l", tpe)
+
+ // 0 < list.size < 3
+ val cnstr = And(GreaterThan(fcall("List1.size")(l.toVariable), bi(0)),
+ LessThan(fcall("List1.size")(l.toVariable), bi(3)))
+
+ val car = Equals(fcall("List1.size")(l.toVariable), bi(1))
+
+ 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 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()
+ }
+ }
+
+}
diff --git a/src/main/scala/leon/solvers/ModelEnumerator.scala b/src/main/scala/leon/solvers/ModelEnumerator.scala
new file mode 100644
index 0000000000000000000000000000000000000000..b22dc921031c1067659a5bd91df3418d6c4461bb
--- /dev/null
+++ b/src/main/scala/leon/solvers/ModelEnumerator.scala
@@ -0,0 +1,85 @@
+package leon
+package solvers
+
+import purescala.Definitions._
+import purescala.Common._
+import purescala.Expressions._
+import purescala.Constructors._
+import purescala.ExprOps._
+import purescala.Types._
+import evaluators._
+
+
+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], cnstr: Expr): Iterator[Map[Identifier, Expr]] = {
+ enumVarying0(ids, cnstr, None, -1)
+ }
+
+ /**
+ * Enumerate at most `nPerCaracteristic` models with the same value for
+ * `caracteristic`.
+ *
+ * Note: there is no guarantee that the models enumerated consecutively share the
+ * same `caracteristic`.
+ */
+ def enumVarying(ids: Seq[Identifier], cnstr: Expr, caracteristic: Expr, nPerCaracteristic: Int = 1) = {
+ enumVarying0(ids, cnstr, Some(caracteristic), nPerCaracteristic)
+ }
+
+ def enumVarying0(ids: Seq[Identifier], cnstr: Expr, caracteristic: Option[Expr], nPerCaracteristic: Int = 1): Iterator[Map[Identifier, Expr]] = {
+ val s = sf.getNewSolver
+ reclaimPool ::= s
+
+ s.assertCnstr(cnstr)
+
+ val c = caracteristic match {
+ case Some(car) =>
+ val c = FreshIdentifier("car", car.getType)
+ s.assertCnstr(Equals(c.toVariable, car))
+ c
+ case None =>
+ FreshIdentifier("noop", BooleanType)
+ }
+
+ var perCarRemaining = Map[Expr, Int]()
+
+ new Iterator[Map[Identifier, Expr]] {
+ def hasNext = {
+ s.check == Some(true)
+ }
+
+ def next = {
+ val sm = s.getModel
+ val m = (ids.map { id =>
+ id -> sm.getOrElse(id, simplestValue(id.getType))
+ }).toMap
+
+
+ // Vary the model
+ s.assertCnstr(not(andJoin(m.toSeq.sortBy(_._1).map { case (k,v) => equality(k.toVariable, v) })))
+
+ caracteristic match {
+ case Some(car) =>
+ val cValue = evaluator.eval(car, m).result.get
+
+ perCarRemaining += (cValue -> (perCarRemaining.getOrElse(cValue, nPerCaracteristic) - 1))
+ if (perCarRemaining(cValue) == 0) {
+ s.assertCnstr(not(equality(c.toVariable, cValue)))
+ }
+
+ case None =>
+ }
+
+ m
+ }
+ }
+ }
+
+ def shutdown() = {
+ reclaimPool.foreach{sf.reclaim(_)}
+ }
+
+}
diff --git a/src/main/scala/leon/solvers/SolverFactory.scala b/src/main/scala/leon/solvers/SolverFactory.scala
index a43dc966456363f50f2b7c9c4b1d74bbbca8f738..90fc5411051a441b732d23dbf19987f70fe4632d 100644
--- a/src/main/scala/leon/solvers/SolverFactory.scala
+++ b/src/main/scala/leon/solvers/SolverFactory.scala
@@ -47,7 +47,7 @@ object SolverFactory {
case (name, desc) => f"\n $name%-14s : $desc"
}.mkString("")
- def getFromSettings(ctx: LeonContext, program: Program): SolverFactory[TimeoutSolver] = {
+ def getFromSettings(implicit ctx: LeonContext, program: Program): SolverFactory[TimeoutSolver] = {
val names = ctx.findOptionOrDefault(SharedOptions.optSelectedSolvers)
if (((names contains "fairz3") || (names contains "unrollz3")) && !hasNativeZ3) {