From 31db0f47f268df4a08b75b52d1f4227a51e4c9ab Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Fri, 28 Aug 2015 16:47:11 +0200
Subject: [PATCH] Enrich FreeableIterator's API, define GrowableIterable
---
.../scala/leon/datagen/SolverDataGen.scala | 12 ++---
.../scala/leon/synthesis/ExamplesFinder.scala | 2 +-
.../leon/synthesis/rules/CEGISLike.scala | 36 ++++++++-------
.../leon/synthesis/rules/TEGISLike.scala | 46 +++++++++++++++----
.../scala/leon/utils/FreeableIterator.scala | 41 +++++++++++++++++
.../scala/leon/utils/GrowableIterable.scala | 25 ++++++++++
.../solvers/ModelEnumerationSuite.scala | 32 ++++---------
7 files changed, 136 insertions(+), 58 deletions(-)
create mode 100644 src/main/scala/leon/utils/GrowableIterable.scala
diff --git a/src/main/scala/leon/datagen/SolverDataGen.scala b/src/main/scala/leon/datagen/SolverDataGen.scala
index 027cc41e0..6f7479f48 100644
--- a/src/main/scala/leon/datagen/SolverDataGen.scala
+++ b/src/main/scala/leon/datagen/SolverDataGen.scala
@@ -15,13 +15,13 @@ import utils._
class SolverDataGen(ctx: LeonContext, pgm: Program, sff: ((LeonContext, Program) => SolverFactory[Solver])) extends DataGenerator {
implicit val ctx0 = ctx
- def generate(tpe: TypeTree): Iterator[Expr] = {
+ def generate(tpe: TypeTree): FreeableIterator[Expr] = {
generateFor(Seq(FreshIdentifier("tmp", tpe)), BooleanLiteral(true), 20, 20).map(_.head)
}
- def generateFor(ins: Seq[Identifier], satisfying: Expr, maxValid: Int, maxEnumerated: Int): Iterator[Seq[Expr]] = {
+ def generateFor(ins: Seq[Identifier], satisfying: Expr, maxValid: Int, maxEnumerated: Int): FreeableIterator[Seq[Expr]] = {
if (ins.isEmpty) {
- Iterator.empty
+ FreeableIterator.empty
} else {
var fds = Map[ClassDef, FunDef]()
@@ -81,11 +81,7 @@ class SolverDataGen(ctx: LeonContext, pgm: Program, sff: ((LeonContext, Program)
val enum = modelEnum.enumVarying(ins, satisfying, sizeOf, 5)
- try {
- enum.take(maxValid).map(model => ins.map(model)).toList.iterator
- } finally {
- enum.free()
- }
+ enum.take(maxValid).map(model => ins.map(model))
}
}
diff --git a/src/main/scala/leon/synthesis/ExamplesFinder.scala b/src/main/scala/leon/synthesis/ExamplesFinder.scala
index 9ef46ec5a..45f399b1b 100644
--- a/src/main/scala/leon/synthesis/ExamplesFinder.scala
+++ b/src/main/scala/leon/synthesis/ExamplesFinder.scala
@@ -114,7 +114,7 @@ class ExamplesFinder(ctx0: LeonContext, program: Program) {
val solverExamples = solverDataGen.generateFor(ids, pc, maxValid, maxEnumerated).map(InExample(_))
- ExamplesBank(generatedExamples.toSeq ++ solverExamples.toSeq, Nil)
+ ExamplesBank(generatedExamples.toSeq ++ solverExamples.toList, Nil)
}
private def extractTestsOf(e: Expr): Set[Map[Identifier, Expr]] = {
diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
index 03feccf9e..480960777 100644
--- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
@@ -20,6 +20,7 @@ import scala.collection.mutable.{HashMap=>MutableMap, ArrayBuffer}
import evaluators._
import datagen._
+import leon.utils._
import codegen.CodeGenParams
abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
@@ -698,36 +699,37 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
*/
val nTests = if (p.pc == BooleanLiteral(true)) 50 else 20
- val inputIterator: Iterator[Seq[Expr]] = if (useVanuatoo) {
- new VanuatooDataGen(sctx.context, sctx.program).generateFor(p.as, p.pc, nTests, 3000)
+ /*
+ val inputGenerator: FreeableIterator[Example] = {
+ val sff = {
+ (ctx: LeonContext, pgm: Program) =>
+ SolverFactory.default(ctx, pgm).withTimeout(exSolverTo)
+ }
+ new SolverDataGen(sctx.context, sctx.program, sff).generateFor(p.as, p.pc, nTests, nTests).map {
+ InExample(_)
+ }
+ } */
+
+ val inputGenerator: Iterator[Example] = if (useVanuatoo) {
+ new VanuatooDataGen(sctx.context, sctx.program).generateFor(p.as, p.pc, nTests, 3000).map(InExample)
} else {
val evaluator = new DualEvaluator(sctx.context, sctx.program, CodeGenParams.default)
- new GrammarDataGen(evaluator, ValueGrammar).generateFor(p.as, p.pc, nTests, 1000)
+ new GrammarDataGen(evaluator, ValueGrammar).generateFor(p.as, p.pc, nTests, 1000).map(InExample)
}
- val cachedInputIterator = new Iterator[Example] {
- def next() = {
- val i = InExample(inputIterator.next())
- baseExampleInputs += i
- i
- }
-
- def hasNext = {
- inputIterator.hasNext
- }
- }
+ val gi = new GrowableIterable[Example](baseExampleInputs, inputGenerator)
val failedTestsStats = new MutableMap[Example, Int]().withDefaultValue(0)
- def hasInputExamples = baseExampleInputs.nonEmpty || cachedInputIterator.hasNext
+ def hasInputExamples = gi.nonEmpty
var n = 1
def allInputExamples() = {
if (n == 10 || n == 50 || n % 500 == 0) {
- baseExampleInputs = baseExampleInputs.sortBy(e => -failedTestsStats(e))
+ gi.sortBufferBy(e => -failedTestsStats(e))
}
n += 1
- baseExampleInputs.iterator ++ cachedInputIterator
+ gi.iterator
}
try {
diff --git a/src/main/scala/leon/synthesis/rules/TEGISLike.scala b/src/main/scala/leon/synthesis/rules/TEGISLike.scala
index 2fe03e7af..9d9e360e2 100644
--- a/src/main/scala/leon/synthesis/rules/TEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/TEGISLike.scala
@@ -5,16 +5,23 @@ package synthesis
package rules
import purescala.Expressions._
+import purescala.Definitions._
import purescala.Types._
import purescala.Constructors._
+import solvers._
+import datagen._
+
import evaluators._
import codegen.CodeGenParams
import utils._
+import leon.utils._
import grammars._
+import scala.collection.mutable.{HashMap => MutableMap}
+
import bonsai.enumerators._
abstract class TEGISLike[T <% Typed](name: String) extends Rule(name) {
@@ -34,6 +41,8 @@ abstract class TEGISLike[T <% Typed](name: String) extends Rule(name) {
def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
+ return Nil;
+
List(new RuleInstantiation(this.name) {
def apply(hctx: SearchContext): RuleApplication = {
val sctx = hctx.sctx
@@ -43,9 +52,35 @@ abstract class TEGISLike[T <% Typed](name: String) extends Rule(name) {
val params = getParams(sctx, p)
val grammar = params.grammar
+ val nTests = if (p.pc == BooleanLiteral(true)) 50 else 20
+
+ val useVanuatoo = sctx.settings.cegisUseVanuatoo.getOrElse(false)
+
+ val inputGenerator: Iterator[Seq[Expr]] = if (useVanuatoo) {
+ new VanuatooDataGen(sctx.context, sctx.program).generateFor(p.as, p.pc, nTests, 3000)
+ } else {
+ val evaluator = new DualEvaluator(sctx.context, sctx.program, CodeGenParams.default)
+ new GrammarDataGen(evaluator, ValueGrammar).generateFor(p.as, p.pc, nTests, 1000)
+ }
+
+ val gi = new GrowableIterable[Seq[Expr]](p.eb.examples.map(_.ins).distinct, inputGenerator)
+
+ val failedTestsStats = new MutableMap[Seq[Expr], Int]().withDefaultValue(0)
+
+ def hasInputExamples = gi.nonEmpty
+
+ var n = 1
+ def allInputExamples() = {
+ if (n == 10 || n == 50 || n % 500 == 0) {
+ gi.sortBufferBy(e => -failedTestsStats(e))
+ }
+ n += 1
+ gi.iterator
+ }
+
var tests = p.eb.valids.map(_.ins).distinct.map(t => (t, new Counter(0)))
- if (tests.nonEmpty) {
+ if (gi.nonEmpty) {
val evalParams = CodeGenParams.default.copy(maxFunctionInvocations = 2000)
val evaluator = new DualEvaluator(sctx.context, sctx.program, evalParams)
@@ -69,14 +104,14 @@ abstract class TEGISLike[T <% Typed](name: String) extends Rule(name) {
//sctx.reporter.debug("Got expression "+e.asString)
timers.testing.start()
- if (tests.forall{ case (t, fc) =>
+ if (allInputExamples().forall{ t =>
val res = evaluator.eval(exprToTest, p.as.zip(t).toMap) match {
case EvaluationResults.Successful(BooleanLiteral(true)) =>
//sctx.reporter.debug("Test "+t.map(_.asString)+" passed!")
true
case _ =>
//sctx.reporter.debug("Test "+t.map(_.asString)+" failed!")
- fc.inc()
+ failedTestsStats += t -> (failedTestsStats(t)+1)
false
}
res
@@ -84,11 +119,6 @@ abstract class TEGISLike[T <% Typed](name: String) extends Rule(name) {
candidate = Some(tupleWrap(Seq(e)))
}
timers.testing.stop()
-
- if (n % params.reorderInterval == 0) {
- tests = tests.sortBy { case (t, fc) => -fc.value }
- }
- n += 1
}
timers.generating.stop()
diff --git a/src/main/scala/leon/utils/FreeableIterator.scala b/src/main/scala/leon/utils/FreeableIterator.scala
index f6ad42937..a790b2dbf 100644
--- a/src/main/scala/leon/utils/FreeableIterator.scala
+++ b/src/main/scala/leon/utils/FreeableIterator.scala
@@ -16,4 +16,45 @@ abstract class FreeableIterator[T] extends Iterator[T] {
def computeNext(): Option[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()
+ }
+ }
+
+ override def take(n: Int): FreeableIterator[T] = {
+ val orig = this
+
+ new FreeableIterator[T] {
+ private var c = 0;
+
+ def computeNext() = {
+ if (c < n) {
+ c += 1
+ orig.computeNext
+ } else {
+ None
+ }
+ }
+
+ def free() = orig.free()
+ }
+ }
+
+ override def toList: List[T] = {
+ val res = super.toList
+ free()
+ res
+ }
+}
+
+object FreeableIterator {
+ def empty[T] = new FreeableIterator[T] {
+ def computeNext() = None
+ def free() = {}
+ }
}
diff --git a/src/main/scala/leon/utils/GrowableIterable.scala b/src/main/scala/leon/utils/GrowableIterable.scala
new file mode 100644
index 000000000..d05a9f065
--- /dev/null
+++ b/src/main/scala/leon/utils/GrowableIterable.scala
@@ -0,0 +1,25 @@
+package leon
+
+import scala.collection.mutable.ArrayBuffer
+
+class GrowableIterable[T](init: Seq[T], growth: Iterator[T]) extends Iterable[T] {
+ var buffer = new ArrayBuffer[T]() ++ init
+
+ val cachingIterator = new Iterator[T] {
+ def hasNext = growth.hasNext
+
+ def next() = {
+ val res = growth.next()
+ buffer += res
+ res
+ }
+ }
+
+ def iterator: Iterator[T] = {
+ buffer.iterator ++ cachingIterator
+ }
+
+ def sortBufferBy[B](f: T => B)(implicit ord: math.Ordering[B]) = {
+ buffer = buffer.sortBy(f)
+ }
+}
diff --git a/src/test/scala/leon/integration/solvers/ModelEnumerationSuite.scala b/src/test/scala/leon/integration/solvers/ModelEnumerationSuite.scala
index 9a23fd600..38553d171 100644
--- a/src/test/scala/leon/integration/solvers/ModelEnumerationSuite.scala
+++ b/src/test/scala/leon/integration/solvers/ModelEnumerationSuite.scala
@@ -53,14 +53,10 @@ class ModelEnumeratorSuite extends LeonTestSuiteWithProgram with ExpressionsDSL
val me = getModelEnum
val enum = me.enumSimple(Seq(l), cnstr)
- try {
- 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 {
- enum.free()
- }
+ 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")
}
test("Simple model enumeration 2") { implicit fix =>
@@ -72,10 +68,8 @@ class ModelEnumeratorSuite extends LeonTestSuiteWithProgram with ExpressionsDSL
val me = getModelEnum
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")
+ assert(enum.take(5).toList.size === 1, "We can only enumerate one list of size 0")
}
test("Varying model enumeration 1") { implicit fix =>
@@ -93,17 +87,13 @@ class ModelEnumeratorSuite extends LeonTestSuiteWithProgram with ExpressionsDSL
// 1 model of each size
val enum1 = me.enumVarying(Seq(l), cnstr, car)
- val models1 = enum1.toList
- enum1.free()
- assert(models1.size === 2, "We can enumerate 2 lists of varying size 0 < .. < 3")
+ assert(enum1.toList.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()
- assert(models2.size === 6, "We can enumerate 6 lists of varying size 0 < .. < 3 with 3 per size")
+ assert(enum2.toList.size === 6, "We can enumerate 6 lists of varying size 0 < .. < 3 with 3 per size")
val car2 = fcall("List1.sum")(l.toVariable)
@@ -111,7 +101,6 @@ class ModelEnumeratorSuite extends LeonTestSuiteWithProgram with ExpressionsDSL
// 1 model of each sum
val enum3 = me.enumVarying(Seq(l), cnstr, car2)
val models3 = enum3.take(4).toList
- enum3.free()
assert(models3.size === 4, "We can enumerate >=4 lists of varying sum, with 0 < .. < 3")
@@ -122,7 +111,6 @@ class ModelEnumeratorSuite extends LeonTestSuiteWithProgram with ExpressionsDSL
// 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")
@@ -147,7 +135,6 @@ class ModelEnumeratorSuite extends LeonTestSuiteWithProgram with ExpressionsDSL
// 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")
@@ -155,7 +142,7 @@ class ModelEnumeratorSuite extends LeonTestSuiteWithProgram with ExpressionsDSL
// 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)")
}
@@ -172,14 +159,12 @@ class ModelEnumeratorSuite extends LeonTestSuiteWithProgram with ExpressionsDSL
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")
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
@@ -199,7 +184,6 @@ class ModelEnumeratorSuite extends LeonTestSuiteWithProgram with ExpressionsDSL
val enum1 = me.enumMinimizing(Seq(l), cnstr, car)
val models1 = enum1.take(5).toList
- enum1.free()
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")
--
GitLab