From 542dea5c580c6878d7da952a4b036c5f792f80ba Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Fri, 8 Jan 2016 16:28:45 +0100
Subject: [PATCH] Update bonsai to latest version
---
build.sbt | 3 +--
src/main/scala/leon/datagen/GrammarDataGen.scala | 2 +-
.../scala/leon/grammars/ExpressionGrammar.scala | 2 --
src/main/scala/leon/grammars/Generator.scala | 16 ++++++++++++++++
src/main/scala/leon/repair/Repairman.scala | 2 +-
.../scala/leon/synthesis/ExamplesFinder.scala | 2 +-
.../disambiguation/QuestionBuilder.scala | 6 ++----
.../leon/synthesis/rules/BottomUpTegis.scala | 6 ++----
.../scala/leon/synthesis/rules/TEGISLike.scala | 2 +-
9 files changed, 25 insertions(+), 16 deletions(-)
create mode 100644 src/main/scala/leon/grammars/Generator.scala
diff --git a/build.sbt b/build.sbt
index feada3374..b825fa5ba 100644
--- a/build.sbt
+++ b/build.sbt
@@ -144,8 +144,7 @@ fork in IsabelleTest := true
def ghProject(repo: String, version: String) = RootProject(uri(s"${repo}#${version}"))
-lazy val bonsai = ghProject("git://github.com/colder/bonsai.git", "0fec9f97f4220fa94b1f3f305f2e8b76a3cd1539")
-
+lazy val bonsai = ghProject("git://github.com/colder/bonsai.git", "10eaaee4ea0ff6567f4f866922cb871bae2da0ac")
lazy val scalaSmtLib = ghProject("git://github.com/regb/scala-smtlib.git", "372bb14d0c84953acc17f9a7e1592087adb0a3e1")
lazy val root = (project in file(".")).
diff --git a/src/main/scala/leon/datagen/GrammarDataGen.scala b/src/main/scala/leon/datagen/GrammarDataGen.scala
index 8cf1044ef..cd86c707d 100644
--- a/src/main/scala/leon/datagen/GrammarDataGen.scala
+++ b/src/main/scala/leon/datagen/GrammarDataGen.scala
@@ -20,7 +20,7 @@ class GrammarDataGen(evaluator: Evaluator, grammar: ExpressionGrammar[TypeTree]
implicit val ctx = evaluator.context
def generate(tpe: TypeTree): Iterator[Expr] = {
- val enum = new MemoizedEnumerator[TypeTree, Expr](grammar.getProductions)
+ val enum = new MemoizedEnumerator[TypeTree, Expr, Generator[TypeTree, Expr]](grammar.getProductions)
enum.iterator(tpe)
}
diff --git a/src/main/scala/leon/grammars/ExpressionGrammar.scala b/src/main/scala/leon/grammars/ExpressionGrammar.scala
index 01a3524d1..ac394ab84 100644
--- a/src/main/scala/leon/grammars/ExpressionGrammar.scala
+++ b/src/main/scala/leon/grammars/ExpressionGrammar.scala
@@ -3,8 +3,6 @@
package leon
package grammars
-import bonsai._
-
import purescala.Expressions._
import purescala.Types._
import purescala.Common._
diff --git a/src/main/scala/leon/grammars/Generator.scala b/src/main/scala/leon/grammars/Generator.scala
new file mode 100644
index 000000000..18d132e2c
--- /dev/null
+++ b/src/main/scala/leon/grammars/Generator.scala
@@ -0,0 +1,16 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package grammars
+
+import bonsai.{Generator => Gen}
+
+object GrammarTag extends Enumeration {
+ val Top = Value
+}
+import GrammarTag._
+
+class Generator[T, R](subTrees: Seq[T], builder: Seq[R] => R, tag: Value) extends Gen[T,R](subTrees, builder)
+object Generator {
+ def apply[T, R](subTrees: Seq[T], builder: Seq[R] => R, tag: Value = Top) = new Generator(subTrees, builder, tag)
+}
\ No newline at end of file
diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index 6523a1104..37f187679 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -242,7 +242,7 @@ class Repairman(ctx0: LeonContext, initProgram: Program, fd: FunDef, verifTimeou
val maxValid = 400
val evaluator = new CodeGenEvaluator(ctx, program, CodeGenParams.default)
- val enum = new MemoizedEnumerator[TypeTree, Expr](ValueGrammar.getProductions)
+ val enum = new MemoizedEnumerator[TypeTree, Expr, Generator[TypeTree, Expr]](ValueGrammar.getProductions)
val inputs = enum.iterator(tupleTypeWrap(fd.params map { _.getType})).map(unwrapTuple(_, fd.params.size))
diff --git a/src/main/scala/leon/synthesis/ExamplesFinder.scala b/src/main/scala/leon/synthesis/ExamplesFinder.scala
index 3cc97f4f5..3f144d88f 100644
--- a/src/main/scala/leon/synthesis/ExamplesFinder.scala
+++ b/src/main/scala/leon/synthesis/ExamplesFinder.scala
@@ -182,7 +182,7 @@ class ExamplesFinder(ctx0: LeonContext, program: Program) {
}) getOrElse {
// If the input contains free variables, it does not provide concrete examples.
// We will instantiate them according to a simple grammar to get them.
- val enum = new MemoizedEnumerator[TypeTree, Expr](ValueGrammar.getProductions)
+ val enum = new MemoizedEnumerator[TypeTree, Expr, Generator[TypeTree, Expr]](ValueGrammar.getProductions)
val values = enum.iterator(tupleTypeWrap(freeVars.map { _.getType }))
val instantiations = values.map {
v => freeVars.zip(unwrapTuple(v, freeVars.size)).toMap
diff --git a/src/main/scala/leon/synthesis/disambiguation/QuestionBuilder.scala b/src/main/scala/leon/synthesis/disambiguation/QuestionBuilder.scala
index e8205da76..bfa6a6212 100644
--- a/src/main/scala/leon/synthesis/disambiguation/QuestionBuilder.scala
+++ b/src/main/scala/leon/synthesis/disambiguation/QuestionBuilder.scala
@@ -1,7 +1,6 @@
package leon
package synthesis.disambiguation
-import synthesis.RuleClosed
import synthesis.Solution
import evaluators.DefaultEvaluator
import purescala.Expressions._
@@ -14,10 +13,9 @@ import purescala.Definitions.Program
import purescala.DefOps
import grammars.ValueGrammar
import bonsai.enumerators.MemoizedEnumerator
-import solvers.Model
import solvers.ModelBuilder
import scala.collection.mutable.ListBuffer
-import leon.grammars.ExpressionGrammar
+import grammars._
object QuestionBuilder {
/** Sort methods for questions. You can build your own */
@@ -142,7 +140,7 @@ class QuestionBuilder[T <: Expr](
def result(): List[Question[T]] = {
if(solutions.isEmpty) return Nil
- val enum = new MemoizedEnumerator[TypeTree, Expr](value_enumerator.getProductions)
+ val enum = new MemoizedEnumerator[TypeTree, Expr, Generator[TypeTree,Expr]](value_enumerator.getProductions)
val values = enum.iterator(tupleTypeWrap(_argTypes))
val instantiations = values.map {
v => input.zip(unwrapTuple(v, input.size))
diff --git a/src/main/scala/leon/synthesis/rules/BottomUpTegis.scala b/src/main/scala/leon/synthesis/rules/BottomUpTegis.scala
index 97b810ac3..2f3869af1 100644
--- a/src/main/scala/leon/synthesis/rules/BottomUpTegis.scala
+++ b/src/main/scala/leon/synthesis/rules/BottomUpTegis.scala
@@ -8,15 +8,13 @@ import purescala.Expressions._
import purescala.Common._
import purescala.Types._
import purescala.Constructors._
-import purescala.Quantification._
import evaluators._
import codegen.CodeGenParams
-import utils._
import grammars._
-import bonsai._
import bonsai.enumerators._
+import bonsai.{Generator => Gen}
case object BottomUpTEGIS extends BottomUpTEGISLike[TypeTree]("BU TEGIS") {
def getGrammar(sctx: SynthesisContext, p: Problem) = {
@@ -110,7 +108,7 @@ abstract class BottomUpTEGISLike[T <: Typed](name: String) extends Rule(name) {
val targetType = tupleTypeWrap(p.xs.map(_.getType))
val wrappedTests = tests.map { case (is, os) => (is, tupleWrap(os))}
- val enum = new BottomUpEnumerator[T, Expr, Expr](
+ val enum = new BottomUpEnumerator[T, Expr, Expr, Generator[T, Expr]](
grammar.getProductions,
wrappedTests,
{ (vecs, gen) =>
diff --git a/src/main/scala/leon/synthesis/rules/TEGISLike.scala b/src/main/scala/leon/synthesis/rules/TEGISLike.scala
index 164e396be..91084ae4f 100644
--- a/src/main/scala/leon/synthesis/rules/TEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/TEGISLike.scala
@@ -71,7 +71,7 @@ abstract class TEGISLike[T <: Typed](name: String) extends Rule(name) {
val evalParams = CodeGenParams.default.copy(maxFunctionInvocations = 2000)
val evaluator = new DualEvaluator(sctx.context, sctx.program, evalParams)
- val enum = new MemoizedEnumerator[T, Expr](grammar.getProductions)
+ val enum = new MemoizedEnumerator[T, Expr, Generator[T, Expr]](grammar.getProductions)
val targetType = tupleTypeWrap(p.xs.map(_.getType))
--
GitLab