Datagens should respect interrupts

src/main/scala/leon/datagen/GrammarDataGen.scala

@@ -55,7 +55,7 @@ class GrammarDataGen(evaluator: Evaluator, grammar: ExpressionGrammar = ValueGra
 
   def generate(tpe: TypeTree): Iterator[Expr] = {
     val enum = new MemoizedEnumerator[Label, Expr, ProductionRule[Label, Expr]](grammar.getProductions)
-    enum.iterator(Label(tpe)).flatMap(expandGenerics)
+    enum.iterator(Label(tpe)).flatMap(expandGenerics).takeWhile(_ => !interrupted.get)
   }
 
   def generateFor(ins: Seq[Identifier], satisfying: Expr, maxValid: Int, maxEnumerated: Int): Iterator[Seq[Expr]] = {
@@ -82,6 +82,7 @@ class GrammarDataGen(evaluator: Evaluator, grammar: ExpressionGrammar = ValueGra
       detupled.take(maxEnumerated)
               .filter(filterCond)
               .take(maxValid)
+              .takeWhile(_ => !interrupted.get)
     }
   }
 

src/main/scala/leon/datagen/SolverDataGen.scala

@@ -15,7 +15,7 @@ class SolverDataGen(ctx: LeonContext, pgm: Program, sf: SolverFactory[Solver]) e
   implicit val ctx0 = ctx
 
   def generate(tpe: TypeTree): FreeableIterator[Expr] = {
-    generateFor(Seq(FreshIdentifier("tmp", tpe)), BooleanLiteral(true), 20, 20).map(_.head)
+    generateFor(Seq(FreshIdentifier("tmp", tpe)), BooleanLiteral(true), 20, 20).map(_.head).takeWhile(_ => !interrupted.get)
   }
 
   def generateFor(ins: Seq[Identifier], satisfying: Expr, maxValid: Int, maxEnumerated: Int): FreeableIterator[Seq[Expr]] = {
@@ -76,7 +76,7 @@ class SolverDataGen(ctx: LeonContext, pgm: Program, sf: SolverFactory[Solver]) e
 
       val enum = modelEnum.enumVarying(ins, satisfying, sizeOf, 5)
 
-      enum.take(maxValid).map(model => ins.map(model))
+      enum.take(maxValid).map(model => ins.map(model)).takeWhile(_ => !interrupted.get)
     }
   }
 

src/main/scala/leon/utils/FreeableIterator.scala

@@ -4,6 +4,8 @@ package leon
 package utils
 
 abstract class FreeableIterator[T] extends Iterator[T] {
+  orig =>
+
   private[this] var nextElem: Option[T] = None
 
   def hasNext = {
@@ -20,8 +22,6 @@ abstract class FreeableIterator[T] extends Iterator[T] {
   def free()
 
   override def map[B](f: T => B): FreeableIterator[B] = {
-    val orig = this
-
     new FreeableIterator[B] {
       def computeNext() = orig.computeNext.map(f)
       def free() = orig.free()
@@ -29,10 +29,8 @@ abstract class FreeableIterator[T] extends Iterator[T] {
   }
 
   override def take(n: Int): FreeableIterator[T] = {
-    val orig = this
-
     new FreeableIterator[T] {
-      private var c = 0;
+      private var c = 0
 
       def computeNext() = {
         if (c < n) {
@@ -47,6 +45,13 @@ abstract class FreeableIterator[T] extends Iterator[T] {
     }
   }
 
+  override def takeWhile(p: T => Boolean) = {
+    new FreeableIterator[T] {
+      def computeNext(): Option[T] = orig.computeNext.filter(p)
+      def free(): Unit = orig.free()
+    }
+  }
+
   override def toList: List[T] = {
     val res = super.toList
     free()

src/test/scala/leon/regression/verification/XLangVerificationSuite.scala

@@ -2,7 +2,6 @@
 
 package leon.regression.verification
 
-import smtlib.interpreters.Z3Interpreter
 import leon.solvers.SolverFactory
 
 // If you add another regression test, make sure it contains exactly one object, whose name matches the file name.