diff --git a/project/Build.scala b/project/Build.scala index f8eddd0bd3b4a53d80e58d8d702b7d43c56d7688..70c01e8e7ebb819bb3db49e5331b41d570de7d76 100644 --- a/project/Build.scala +++ b/project/Build.scala @@ -79,7 +79,7 @@ object Leon extends Build { object Github { def project(repo: String, version: String) = RootProject(uri(s"${repo}#${version}")) - lazy val bonsai = project("git://github.com/colder/bonsai.git", "8f485605785bda98ac61885b0c8036133783290a") + lazy val bonsai = project("git://github.com/colder/bonsai.git", "0fec9f97f4220fa94b1f3f305f2e8b76a3cd1539") lazy val scalaSmtLib = project("git://github.com/regb/scala-smtlib.git", "e721cf606f73c6ba41f7622c141a1eefef2c712d") } } diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala index b5a701579a407b3d7f5f361f9d46581c0a454395..7e5e20ea970985138bee90243fe3326d09d689ef 100644 --- a/src/main/scala/leon/synthesis/Rules.scala +++ b/src/main/scala/leon/synthesis/Rules.scala @@ -26,6 +26,7 @@ object Rules { InequalitySplit, CEGIS, TEGIS, + //BottomUpTEGIS, rules.Assert, DetupleOutput, DetupleInput, diff --git a/src/main/scala/leon/synthesis/rules/BottomUpTegis.scala b/src/main/scala/leon/synthesis/rules/BottomUpTegis.scala new file mode 100644 index 0000000000000000000000000000000000000000..e409b4d1b72fe0acbd3817693aecb3f7d9ed2a67 --- /dev/null +++ b/src/main/scala/leon/synthesis/rules/BottomUpTegis.scala @@ -0,0 +1,149 @@ +/* Copyright 2009-2014 EPFL, Lausanne */ + +package leon +package synthesis +package rules + +import solvers._ +import solvers.z3._ + +import purescala.Trees._ +import purescala.Common._ +import purescala.Definitions._ +import purescala.TypeTrees._ +import purescala.TreeOps._ +import purescala.TypeTreeOps._ +import purescala.Extractors._ +import purescala.ScalaPrinter +import purescala.Constructors._ + +import scala.collection.mutable.{Map=>MutableMap, ArrayBuffer} + +import evaluators._ +import datagen._ +import codegen.CodeGenParams + +import utils._ + +import bonsai._ +import bonsai.enumerators._ + +case object BottomUpTEGIS extends BottomUpTEGISLike[TypeTree]("BU TEGIS") { + def getGrammar(sctx: SynthesisContext, p: Problem) = { + ExpressionGrammars.default(sctx, p) + } + + def getRootLabel(tpe: TypeTree): TypeTree = tpe +} + +abstract class BottomUpTEGISLike[T <% Typed](name: String) extends Rule(name) { + def getGrammar(sctx: SynthesisContext, p: Problem): ExpressionGrammar[T] + + def getRootLabel(tpe: TypeTree): T + + def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = { + var tests = p.getTests(sctx).collect { + case io: InOutExample => (io.ins, io.outs) + } + + if (tests.nonEmpty) { + List(new RuleInstantiation(p, this, SolutionBuilder.none, this.name, this.priority) { + def apply(sctx: SynthesisContext): RuleApplication = { + + val evalParams = CodeGenParams(maxFunctionInvocations = 2000, checkContracts = true) + //val evaluator = new CodeGenEvaluator(sctx.context, sctx.program, evalParams) + //val evaluator = new DefaultEvaluator(sctx.context, sctx.program) + val evaluator = new DualEvaluator(sctx.context, sctx.program, evalParams) + + val interruptManager = sctx.context.interruptManager + + val grammar = getGrammar(sctx, p) + + val nTests = tests.size + + var compiled = Map[Generator[T, Expr], Vector[Vector[Expr]] => Option[Vector[Expr]]]() + + /** + * Compile Generators to functions from Expr to Expr. The compiled + * generators will be passed to the enumerator + */ + def compile(gen: Generator[T, Expr]): Vector[Vector[Expr]] => Option[Vector[Expr]] = { + compiled.getOrElse(gen, { + val executor = if (gen.subTrees.isEmpty) { + + { (vecs: Vector[Vector[Expr]]) => + val expr = gen.builder(Nil) + val res = tests.map { case (is, o) => (p.as zip is).toMap }.flatMap { case inputs => + evaluator.eval(expr, inputs) match { + case EvaluationResults.Successful(out) => Some(out) + case _ => None + } + }.toVector + + if (res.size == nTests) { + Some(res) + } else { + None + } + } + } else { + val args = gen.subTrees.map(t => FreshIdentifier("arg", true).setType(t.getType)) + val argsV = args.map(_.toVariable) + val expr = gen.builder(argsV) + val ev = evaluator.compile(expr, args).get + + { (vecs: Vector[Vector[Expr]]) => + val res = (0 to nTests-1).toVector.flatMap { i => + val inputs = vecs.map(_(i)) + ev(inputs) match { + case EvaluationResults.Successful(out) => Some(out) + case _ => + None + } + } + + if (res.size == nTests) { + Some(res) + } else { + None + } + } + } + + compiled += gen -> executor + executor + }) + } + + val (targetType, isWrapped, wrappedTests) = if (p.xs.size == 1) { + (p.xs.head.getType, false, tests.map{ case (i, o) => (i, o.head) }) + } else { + (TupleType(p.xs.map(_.getType)), true, tests.map{ case (i, o) => (i, Tuple(o)) }) + } + + val enum = new BottomUpEnumerator[T, Expr, Expr]( + grammar.getProductions, + wrappedTests, + { (vecs, gen) => + compile(gen)(vecs) + }, + 3 + ) + + + val timers = sctx.context.timers.synthesis.rules.tegis; + + val matches = enum.iterator(getRootLabel(targetType)) + + if (matches.hasNext) { + RuleClosed(Solution(BooleanLiteral(true), Set(), matches.next, isTrusted = false)) + } else { + RuleFailed() + } + } + }) + } else { + Nil + } + } +}