From 6d1da6a137a44cfd76af01009e6f8df1f3d83875 Mon Sep 17 00:00:00 2001 From: Etienne Kneuss Date: Wed, 8 Jun 2016 16:11:16 +0200 Subject: [PATCH] Size bound TEGIS --- .../leon/synthesis/rules/HOFDecomp.scala | 17 +- .../scala/leon/synthesis/rules/TEGIS.scala | 5 +- .../leon/synthesis/rules/TEGISLike.scala | 37 ++-- testcases/synthesis/current/HOFs/List.scala | 18 +- testcases/synthesis/current/HOFs/Tree.scala | 166 ++++++++++++++++++ 5 files changed, 217 insertions(+), 26 deletions(-) create mode 100644 testcases/synthesis/current/HOFs/Tree.scala diff --git a/src/main/scala/leon/synthesis/rules/HOFDecomp.scala b/src/main/scala/leon/synthesis/rules/HOFDecomp.scala index ac6d84cc3..32bf5da09 100644 --- a/src/main/scala/leon/synthesis/rules/HOFDecomp.scala +++ b/src/main/scala/leon/synthesis/rules/HOFDecomp.scala @@ -79,7 +79,7 @@ case object HOFDecomp extends Rule("HOFDecomp") { var freeVariables = Set[Identifier]() - val altsPerArgs = tfd.params.map { vd => + val altsPerArgs = tfd.params.zipWithIndex.map { case (vd, i) => if (isHOFParam(vd)) { // Only one possibility for the HOF argument Seq(hofId) @@ -87,8 +87,17 @@ case object HOFDecomp extends Rule("HOFDecomp") { // For normal arguments, we either map to a free variable (and // then ask solver for a model), or to an input - val free = FreshIdentifier("v", vd.getType, true) - freeVariables += free + val optFree = if (i > 0) { + // Hack: First argument is the most important, we should not + // obtain its value from a model. We don't want: + // Nil.fold(..) + + Some(FreshIdentifier("v", vd.getType, true)) + } else { + None + } + + freeVariables ++= optFree // Note that this is an over-approximation, since // Int <: T and @@ -100,7 +109,7 @@ case object HOFDecomp extends Rule("HOFDecomp") { p.as.filter(a => canBeSupertypeOf(vd.getType, a.getType).nonEmpty) } - compatibleInputs :+ free + compatibleInputs ++ optFree } } diff --git a/src/main/scala/leon/synthesis/rules/TEGIS.scala b/src/main/scala/leon/synthesis/rules/TEGIS.scala index 150a7419a..16ab7bf04 100644 --- a/src/main/scala/leon/synthesis/rules/TEGIS.scala +++ b/src/main/scala/leon/synthesis/rules/TEGIS.scala @@ -5,12 +5,13 @@ package synthesis package rules import leon.grammars._ +import leon.grammars.aspects._ case object TEGIS extends TEGISLike("TEGIS") { def getParams(sctx: SynthesisContext, p: Problem) = { TegisParams( - grammar = grammars.default(sctx, p), - rootLabel = Label(_) + grammar = Grammars.default(sctx, p), + rootLabel = Label(_).withAspect(Tagged(Tags.Top, 0, None)) ) } } diff --git a/src/main/scala/leon/synthesis/rules/TEGISLike.scala b/src/main/scala/leon/synthesis/rules/TEGISLike.scala index f7ec4700a..bdfaec04a 100644 --- a/src/main/scala/leon/synthesis/rules/TEGISLike.scala +++ b/src/main/scala/leon/synthesis/rules/TEGISLike.scala @@ -12,6 +12,7 @@ import datagen._ import evaluators._ import codegen.CodeGenParams import leon.grammars._ +import leon.grammars.aspects.Sized import leon.utils.GrowableIterable import scala.collection.mutable.{HashMap => MutableMap} @@ -22,8 +23,8 @@ abstract class TEGISLike(name: String) extends Rule(name) { case class TegisParams( grammar: ExpressionGrammar, rootLabel: TypeTree => Label, - enumLimit: Int = 10000, - reorderInterval: Int = 50 + minSize: Int = 3, + maxSize: Int = 3 ) def getParams(sctx: SynthesisContext, p: Problem): TegisParams @@ -46,6 +47,8 @@ abstract class TEGISLike(name: String) extends Rule(name) { p.qebFiltered.examples } + ci.reporter.debug(ExamplesBank(baseExamples, Nil).asString("Tests")) + val exampleGenerator: Iterator[Example] = if (p.isTestBased) { Iterator.empty } else if (useVanuatoo) { @@ -79,17 +82,20 @@ abstract class TEGISLike(name: String) extends Rule(name) { val timers = hctx.timers.synthesis.rules.tegis - val allExprs = enum.iterator(params.rootLabel(targetType)) - var candidate: Option[Expr] = None + val streams = for(size <- (params.minSize to params.maxSize).toIterator) yield { + println("Size: "+size) + val label = params.rootLabel(targetType).withAspect(Sized(size)) + + val allExprs = enum.iterator(label) - def findNext(): Option[Expr] = { - candidate = None timers.generating.start() - allExprs.take(params.enumLimit).takeWhile(e => candidate.isEmpty).foreach { e => + + val candidates: Iterator[Expr] = allExprs.flatMap { e => val exprToTest = letTuple(p.xs, e, p.phi) //sctx.reporter.debug("Got expression "+e.asString) + timers.testing.start() if (allExamples().forall{ case InExample(ins) => @@ -99,20 +105,23 @@ abstract class TEGISLike(name: String) extends Rule(name) { println("Evaluating "+e.asString+" with "+ins.map(_.asString)) evaluator.eval(e, p.as.zip(ins).toMap).result == Some(tupleWrap(outs)) }) { - candidate = Some(tupleWrap(Seq(e))) + timers.testing.stop() + Some(tupleWrap(Seq(e))) + } else { + timers.testing.stop() + None } - timers.testing.stop() } timers.generating.stop() - candidate + candidates } - val toStream = Stream.continually(findNext()).takeWhile(_.nonEmpty).map( e => - Solution(BooleanLiteral(true), Set(), e.get, isTrusted = p.isTestBased) - ) + val solutions = streams.flatten.map { e => + Solution(BooleanLiteral(true), Set(), e, isTrusted = p.isTestBased) + } - RuleClosed(toStream) + RuleClosed(solutions.toStream) } else { hctx.reporter.debug("No test available") RuleFailed() diff --git a/testcases/synthesis/current/HOFs/List.scala b/testcases/synthesis/current/HOFs/List.scala index 11a565ba5..2b1b78877 100644 --- a/testcases/synthesis/current/HOFs/List.scala +++ b/testcases/synthesis/current/HOFs/List.scala @@ -209,20 +209,26 @@ object HOFDecomp1 { def adultsNames(in: List[Person]): List[String] = { // in.filter(_.age >= 18).map(_.name) + // + // in.collect { p => + // if (p.age >= 18) Some(p.name) else None + //} ???[List[String]] } ensuring { out => (in, out) passes { - case Cons(Person("Alice", 17), Cons(Person("Bob", 18), Cons(Person("Jane", 12), Cons(Person("Arnold", 22), Nil())))) => Cons("Bob", Cons("Arnold", Nil())) - case Cons(Person("Alice", 22), Cons(Person("Bob", 12), Cons(Person("Jane", 32), Cons(Person("Arnold", 42), Nil())))) => Cons("Alice", Cons("Jane", Cons("Arnold", Nil()))) - - case Cons(Person(a, 23), Cons(Person(b, 11), Cons(Person(c, 19), Cons(Person(d, 17), Nil())))) => Cons(a, Cons(c, Nil())) - case Cons(Person(a, 9), Cons(Person(b, 18), Cons(Person(c, 15), Cons(Person(d, 25), Nil())))) => Cons(b, Cons(d, Nil())) - case Nil() => Nil() + case Cons(Person(a, 18), Cons(Person(b, 19), Cons(Person(c, 42), Cons(Person(d, 20), Nil())))) => Cons(a, Cons(b, Cons(c, Cons(d, Nil())))) + case Cons(Person(a, -5), Cons(Person(b, 19), Cons(Person(c, 17), Cons(Person(d, 18), Nil())))) => Cons(b, Cons(d, Nil())) + case Cons(Person(a, -2), Cons(Person(b, 17), Cons(Person(c, 16), Cons(Person(d, 0), Nil())))) => Nil() + case Nil() => Nil() } } def posNames(in: List[Person]): List[String] = { // in.filter(_.age >= 0).map(_.name) + // + // in.collect { p => + // if (p.age >= 0) Some(p.name) else None + //} ???[List[String]] } ensuring { out => (in, out) passes { diff --git a/testcases/synthesis/current/HOFs/Tree.scala b/testcases/synthesis/current/HOFs/Tree.scala new file mode 100644 index 000000000..1ce2a6150 --- /dev/null +++ b/testcases/synthesis/current/HOFs/Tree.scala @@ -0,0 +1,166 @@ +import leon.lang._ +import leon.lang.synthesis._ + +object HOFDecomp1 { + abstract class Tree[T] { + def map[B](f: T => B): Tree[B] = { + this match { + case Node(v, l, r) => Node(f(v), l.map(f), r.map(f)) + case Leaf() => Leaf() + } + } + + def fold[B](z: B)(f: (T, B, B) => B): B = { + this match { + case Node(v, l, r) => f(v, l.fold(z)(f), r.fold(z)(f)) + case Leaf() => z + } + } + } + + case class Node[T](v: T, l: Tree[T], r: Tree[T]) extends Tree[T] + case class Leaf[T]() extends Tree[T] + + abstract class List[T] { + def filter(f: T => Boolean): List[T] = { + this match { + case Cons(h, t) => + if (f(h)) { + Cons(h, t.filter(f)) + } else { + t.filter(f) + } + + case Nil() => Nil() + } + } + + def map[B](f: T => B): List[B] = { + this match { + case Cons(h, t) => Cons(f(h), t.map(f)) + case Nil() => Nil[B]() + } + } + + def foldr[B](z: B)(f: (B, T) => B): B = { + this match { + case Cons(h, t) => f(t.foldr(z)(f), h) + case Nil() => z + } + } + + def foldl[B](z: B)(f: (B, T) => B): B = { + this match { + case Cons(h, t) => t.foldl(f(z, h))(f) + case Nil() => z + } + } + + def ++(l: List[T]): List[T] = { + this match { + case Cons(h, t) => Cons(h, t ++ l) + case Nil() => l + } + } + } + + case class Cons[T](h: T, t: List[T]) extends List[T] + case class Nil[T]() extends List[T] + + def countLeaves(in: Tree[Int]): Int = { + // in.fold(1){ (v,l,r) => l+r } + ???[Int] + } ensuring { + out => (in, out) passes { + case Leaf() => 1 + case Node(13, Leaf(), Leaf()) => 2 + case Node(13, Leaf(), Node(13, Leaf(), Leaf())) => 3 + case Node(13, Node(13, Leaf(), Leaf()), Node(13, Leaf(), Node(13, Leaf(), Leaf()))) => 5 + } + } + + def countNodes(in: Tree[Int]): Int = { + // in.fold(0){ (v,l,r) => 1+l+r } + ???[Int] + } ensuring { + out => (in, out) passes { + case Leaf() => 0 + case Node(13, Leaf(), Leaf()) => 1 + case Node(13, Leaf(), Node(13, Leaf(), Leaf())) => 2 + case Node(13, Node(13, Leaf(), Leaf()), Node(13, Leaf(), Node(13, Leaf(), Leaf()))) => 4 + } + } + + def flatten(in: Tree[Int]): List[Int] = { + // in.fold(Nil) { (v, l, r) => Cons(v, Nil) ++ l ++ r } + ???[List[Int]] + } ensuring { + out => (in, out) passes { + case Leaf() => Nil[Int]() + case Node(13, Leaf(), Leaf()) => Cons(13, Nil()) + case Node(12, Leaf(), Node(13, Leaf(), Leaf())) => Cons(12, Cons(13, Nil())) + case Node(12, Node(13, Leaf(), Leaf()), Leaf()) => Cons(12, Cons(13, Nil())) + case Node(12, Node(13, Leaf(), Leaf()), Node(12, Leaf(), Node(13, Leaf(), Leaf()))) => Cons(12, Cons(13, Cons(12, Cons(13, Nil())))) + } + } + + def max(a: Int, b: Int): Int = { + if (a > b) a else b + } + + def height(in: Tree[Int]): Int = { + // in.fold(0) { (v, l, r) => 1+max(l, r) } + ???[Int] + } ensuring { + out => (in, out) passes { + case Leaf() => 0 + case Node(13, Leaf(), Leaf()) => 1 + case Node(13, Leaf(), Node(13, Leaf(), Leaf())) => 2 + case Node(13, Node(13, Leaf(), Leaf()), Leaf()) => 2 + case Node(13, Node(13, Leaf(), Leaf()), Node(13, Leaf(), Node(13, Leaf(), Leaf()))) => 3 + } + } + + def incr(in: Tree[Int]): Tree[Int] = { + // in.map{ _ + 1 } + ???[Tree[Int]] + } ensuring { + out => (in, out) passes { + case Leaf() => Leaf() + case Node(13, Leaf(), Leaf()) => Node(14, Leaf(), Leaf()) + case Node(-4, Leaf(), Node(13, Leaf(), Leaf())) => Node(-3, Leaf(), Node(14, Leaf(), Leaf())) + case Node(10, Node(11, Leaf(), Leaf()), Leaf()) => Node(11, Node(12, Leaf(), Leaf()), Leaf()) + } + } + + def maxt(in: Tree[Int]): Int = { + require(in != Leaf[Int]()) + // in.fold(in.v) { (v, l, r) => max(v, max(l, r)) } + ???[Int] + } ensuring { + out => (in, out) passes { + case Node(13, Leaf(), Leaf()) => 13 + case Node(11, Leaf(), Leaf()) => 11 + case Node(-4, Leaf(), Node(13, Leaf(), Leaf())) => 13 + case Node(16, Leaf(), Node(11, Leaf(), Leaf())) => 16 + case Node(9, Node(11, Leaf(), Leaf()), Leaf()) => 11 + case Node(12, Node(13, Leaf(), Leaf()), Leaf()) => 13 + case Node(12, Node(13, Leaf(), Leaf()), Node(11, Leaf(), Leaf())) => 13 + } + } + + def member(in: Tree[Int], v: Int): Boolean = { + // in.fold(false) { (v2, l, r) => v == v2 || l || r } + ???[Boolean] + } ensuring { + out => ((in, v), out) passes { + case (Leaf(), 10) => false + case (Node(10, Leaf(), Leaf()), 10) => true + case (Node(11, Leaf(), Leaf()), 10) => false + case (Node(11, Node(10, Leaf(), Leaf()), Leaf()), 10) => true + case (Node(11, Leaf(), Node(10, Leaf(), Leaf())), 10) => true + case (Node(11, Node(12, Leaf(), Leaf()), Leaf()), 10) => false + case (Node(11, Leaf(), Node(12, Leaf(), Leaf())), 10) => false + } + } +}