Solver-based enumeration of models

- enumSimple allows to enumerate distinct models (models will typically
  only slightly differ , e.g. only w.r.t one integer)

- enumVarying allows to specify a caracteristic (i.e. `size`) and
  enumerate `N` models of each size.

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

+/* 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()
+    }
+  }
+
+}

src/main/scala/leon/solvers/ModelEnumerator.scala

+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(_)}
+  }
+
+}

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) {