diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala index 5e958d2383017446b145e6403c3bd39acc5e5145..0e1082ab83aa090743a377daa1c0d1466ade236b 100644 --- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala +++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala @@ -797,6 +797,10 @@ abstract class CEGISLike[T <: Typed](name: String) extends Rule(name) { // We keep number of failures per test to pull the better ones to the front val failedTestsStats = new MutableMap[Example, Int]().withDefaultValue(0) + // This is the starting test-base + val gi = new GrowableIterable[Example](baseExampleInputs, inputGenerator) + def hasInputExamples = gi.nonEmpty + var n = 1 try { @@ -811,12 +815,8 @@ abstract class CEGISLike[T <: Typed](name: String) extends Rule(name) { def nPassing = ndProgram.prunedPrograms.size - def programsReduced() = nPassing <= 10 || nInitial / nPassing > testReductionRatio - - // This is the starting test-base - val gi = new GrowableIterable[Example](baseExampleInputs, inputGenerator, programsReduced) - - def hasInputExamples = gi.nonEmpty + def programsReduced() = nPassing <= 10 || nInitial / nPassing > testReductionRatio + gi.canGrow = programsReduced def allInputExamples() = { if (n == 10 || n == 50 || n % 500 == 0) { diff --git a/src/main/scala/leon/synthesis/rules/unused/TEGISLike.scala b/src/main/scala/leon/synthesis/rules/unused/TEGISLike.scala index cd6382864163d11c770386f09804d0504d2702fa..0f0a76a964bd7f847bc8f59a099c5ed2249d5b38 100644 --- a/src/main/scala/leon/synthesis/rules/unused/TEGISLike.scala +++ b/src/main/scala/leon/synthesis/rules/unused/TEGISLike.scala @@ -47,7 +47,7 @@ abstract class TEGISLike[T <: Typed](name: String) extends Rule(name) { new GrammarDataGen(evaluator, ValueGrammar).generateFor(p.as, p.pc, nTests, 1000) } - val gi = new GrowableIterable[Seq[Expr]](p.eb.examples.map(_.ins).distinct, inputGenerator, () => true) + val gi = new GrowableIterable[Seq[Expr]](p.eb.examples.map(_.ins).distinct, inputGenerator) val failedTestsStats = new MutableMap[Seq[Expr], Int]().withDefaultValue(0) diff --git a/src/main/scala/leon/utils/GrowableIterable.scala b/src/main/scala/leon/utils/GrowableIterable.scala index 884f499c2b3a73702974a0e94893bd9efd35ec11..1ef76649a6d22abdbb1d6032683f4ce1fac1a0e0 100644 --- a/src/main/scala/leon/utils/GrowableIterable.scala +++ b/src/main/scala/leon/utils/GrowableIterable.scala @@ -4,9 +4,11 @@ package leon.utils import scala.collection.mutable.ArrayBuffer -class GrowableIterable[T](init: Seq[T], growth: Iterator[T], canGrow: () => Boolean) extends Iterable[T] { +class GrowableIterable[T](init: Seq[T], growth: Iterator[T]) extends Iterable[T] { private var buffer = new ArrayBuffer[T]() ++ init + var canGrow = () => true + private val cachingIterator = new Iterator[T] { def hasNext = canGrow() && growth.hasNext