diff --git a/build.sbt b/build.sbt index feada3374002c48ce63ee6c491869ba12317e9fa..b825fa5ba9146d4bb9e2c23f41edf3e6f756188f 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 8cf1044ef0dcf3429c8df805dc6a51f18fc17a4d..cd86c707ddb893918e512f6d7101cc4cc92b6405 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 01a3524d18b24e35f6912fdae034f4988fb7779e..ac394ab840bddf0d498080a04e447ce66de07caa 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 0000000000000000000000000000000000000000..18d132e2c25ea222324dc05809220f12d0fb7100 --- /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 6523a1104127c174edf5c1e9d994be27b797d421..37f187679897bbec908ffeaf18f5385198f915c9 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 3cc97f4f5d39c9c512800162371c3b6eaac173f1..3f144d88f805016c9d2dbc63c57cb73255a098b2 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 e8205da76abfc0076eaa0b0fd5de861e81185079..bfa6a62120af6171d001b6a026630734eb6c10fd 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 97b810ac367de8e0843ffb78a50f61f694966d43..2f3869af16b71f9635e36d27774f55a7cee7140c 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 164e396be5f77ea109828921b5f3157d8c85fa43..91084ae4f6d69d055c36f0ce2c75bc4b41bfa763 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))