Skip to content

Commit

Permalink
Generate better tests
Browse files Browse the repository at this point in the history
  • Loading branch information
@colder @manoskouk
colder authored and manoskouk committed Jul 11, 2016
1 parent c9ca54f commit ee790fe
Show file tree
Hide file tree
Showing 5 changed files with 114 additions and 12 deletions.
59 changes: 59 additions & 0 deletions src/main/scala/leon/datagen/DistinctGrammarDataGen.scala
View file
@@ -0,0 +1,59 @@
/* Copyright 2009-2016 EPFL, Lausanne */

package leon
package datagen

import purescala.Expressions._
import purescala.Types._
import purescala.Common._
import purescala.Constructors._
import purescala.Extractors._
import purescala.ExprOps._
import evaluators._
import bonsai.enumerators._

import grammars._
import utils.UniqueCounter
import utils.StreamUtils.cartesianProduct

/** Utility functions to generate values of a given type.
* In fact, it could be used to generate *terms* of a given type,
* e.g. by passing trees representing variables for the "bounds". */
class VaryingGrammarDataGen(eval: Evaluator, grammar: ExpressionGrammar = ValueGrammar) extends GrammarDataGen(eval, grammar) {

def generateN(tpe: TypeTree, n: Int): Iterator[Seq[Expr]] = {
if (n == 1) {
generate(tpe).map(Seq(_))
} else {
generate(tpe).sliding(n).filter(_.size == n)
}
}

override def generateFor(ins: Seq[Identifier], satisfying: Expr, maxValid: Int, maxEnumerated: Int): Iterator[Seq[Expr]] = {
require(satisfying == BooleanLiteral(true))

if (ins.isEmpty) {
Iterator(Seq[Expr]())
} else {
// From id1: A, id2: B, id3: A
// We get: (id1, id3), (id2)
val groups = ins.groupBy(_.getType).values.toSeq

// id1 -> 0, id2 -> 2, id3 -> 1
val indices = groups.flatten.zipWithIndex.toMap

// Generate distinct values for each group
var streams = groups map { g =>
generateN(g.head.getType, g.size).toStream
}

// Group1 x Group2 ...
val values = cartesianProduct(streams).map(_.flatten).map { vs =>
// obtain Seq(v1, v2, v3) where v1 is value of id1 ...
ins.map(in => vs(indices(in)))
}.toIterator

values.take(maxValid).takeWhile(_ => !interrupted.get)
}
}
}
21 changes: 18 additions & 3 deletions src/main/scala/leon/grammars/ValueGrammar.scala
View file
Expand Up @@ -20,13 +20,25 @@ case object ValueGrammar extends SimpleExpressionGrammar {
List(
terminal(IntLiteral(0), Tags.Zero),
terminal(IntLiteral(1), Tags.One),
terminal(IntLiteral(5), Tags.Constant)
terminal(IntLiteral(5), Tags.Constant),
terminal(IntLiteral(-1), Tags.Constant, 3),
terminal(IntLiteral(2), Tags.Constant, 3),
terminal(IntLiteral(3), Tags.Constant, 3),
terminal(IntLiteral(-2), Tags.Constant, 5),
terminal(IntLiteral(4), Tags.Constant, 5),
terminal(IntLiteral(10), Tags.Constant, 5)
)
case IntegerType =>
List(
terminal(InfiniteIntegerLiteral(0), Tags.Zero),
terminal(InfiniteIntegerLiteral(1), Tags.One),
terminal(InfiniteIntegerLiteral(5), Tags.Constant)
terminal(InfiniteIntegerLiteral(5), Tags.Constant),
terminal(InfiniteIntegerLiteral(-1), Tags.Constant, 3),
terminal(InfiniteIntegerLiteral(2), Tags.Constant, 3),
terminal(InfiniteIntegerLiteral(3), Tags.Constant, 3),
terminal(InfiniteIntegerLiteral(-2), Tags.Constant, 5),
terminal(InfiniteIntegerLiteral(4), Tags.Constant, 5),
terminal(InfiniteIntegerLiteral(10), Tags.Constant, 5)
)
case CharType =>
List(
Expand All @@ -46,7 +58,10 @@ case object ValueGrammar extends SimpleExpressionGrammar {
terminal(StringLiteral(""), Tags.Constant),
terminal(StringLiteral("a"), Tags.Constant),
terminal(StringLiteral("foo"), Tags.Constant),
terminal(StringLiteral("bar"), Tags.Constant)
terminal(StringLiteral("bar"), Tags.Constant),
terminal(StringLiteral("b"), Tags.Constant, 3),
terminal(StringLiteral("c"), Tags.Constant, 3),
terminal(StringLiteral("d"), Tags.Constant, 3)
)

case tp: TypeParameter =>
Expand Down
26 changes: 23 additions & 3 deletions src/main/scala/leon/synthesis/ExamplesFinder.scala
View file
Expand Up @@ -224,11 +224,26 @@ class ExamplesFinder(ctx0: LeonContext, program: Program) {
} else {
// 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 dataGen = new GrammarDataGen(evaluator)

val theGuard = replace(Map(in -> pattExpr), cs.optGuard.getOrElse(BooleanLiteral(true)))
val exs = cs.optGuard match {
case Some(g) =>
// We have a guard constraining the freeVars, we generate them together
val theGuard = replace(Map(in -> pattExpr), g)

dataGen.generateFor(freeVars, theGuard, examplesPerCase, 1000).toSeq map { vals =>
val dataGen = new GrammarDataGen(evaluator)
dataGen.generateFor(freeVars, theGuard, examplesPerCase, 1000)

case None =>
// We have no guard, it boils down to generate bunch of values
// per types of freevars and building tuples.
//println(s"Found simple in/out testcase: $cs")
//println("Free: "+freeVars)

val dataGen = new VaryingGrammarDataGen(evaluator)
dataGen.generateFor(freeVars, BooleanLiteral(true), examplesPerCase, examplesPerCase)
}

exs.toSeq map { vals =>
val inst = freeVars.zip(vals).toMap
val inR = replaceFromIDs(inst, pattExpr)
val outR = replaceFromIDs(inst, doSubstitute(ieMap, cs.rhs))
Expand All @@ -237,6 +252,11 @@ class ExamplesFinder(ctx0: LeonContext, program: Program) {
}
}
}

//println("Case: "+cs.asString)
//val eb = ExamplesBank(res.map(c => InOutExample(Seq(c._1), Seq(c._2))), Nil)
//println(eb.asString("Tests"))


if(this.keepAbstractExamples) res.map(expand) else res
}
Expand Down
13 changes: 10 additions & 3 deletions src/main/scala/leon/synthesis/rules/HOFDecomp.scala
View file
Expand Up @@ -185,15 +185,15 @@ case object HOFDecomp extends Rule("HOFDecomp") {

val cnstr = andJoin(cnstrs)

println("Constraint: "+cnstr.asString)
//println("Constraint: "+cnstr.asString)

val solver = solverf.getNewSolver()
try {
solver.assertCnstr(cnstr)
solver.check match {
case Some(true) =>
val model = solver.getModel
println("Model: "+model.asString)
//println("Model: "+model.asString)

val freeValuations = free.flatMap { id =>
model.get(id).map {
Expand All @@ -209,6 +209,8 @@ case object HOFDecomp extends Rule("HOFDecomp") {
case (envValuation, FiniteLambda(values, _, _)) =>
values.flatMap {
case (ins, out) =>
//println("Test:")
//println(s"$ins ---> $out")

/* Given a model with Fgen(env*)(X) -> Y,
* we check if we can use ''(env*, X) -> Y'' as
Expand All @@ -223,6 +225,10 @@ case object HOFDecomp extends Rule("HOFDecomp") {
solver2.assertCnstr(not(equality(Application(f, ins), out)))

val isUnique = solver2.check == Some(false)
//println("IsUnique? "+isUnique)
//if (!isUnique) {
// println("Alternative: "+solver2.getModel.asString)
//}
solverf.reclaim(solver2)

if (isUnique) {
Expand All @@ -232,7 +238,8 @@ case object HOFDecomp extends Rule("HOFDecomp") {
}
}
}
case _ =>
case res =>
//println("Model of "+fgen+": "+res)
Nil
}

Expand Down
7 changes: 4 additions & 3 deletions testcases/synthesis/current/HOFs/List.scala
View file
Expand Up @@ -226,9 +226,10 @@ object HOFDecomp1 {
???[List[String]]
} ensuring {
out => (in, out) passes {
case Cons(Person(a, 0), Cons(Person(b, -1), Cons(Person(c, 3), Cons(Person(d, -2), Nil())))) => Cons(a, Cons(c, Nil()))
case Cons(Person(a, -5), Cons(Person(b, 2), Cons(Person(c, -2), Cons(Person(d, 3), Nil())))) => Cons(b, Cons(d, Nil()))
case Nil() => Nil()
case Cons(Person(a, 0), Cons(Person(b, 10), Cons(Person(c, 3), Cons(Person(d, 5), Nil())))) => Cons(a, Cons(b, Cons(c, Cons(d, Nil()))))
case Cons(Person(a, -5), Cons(Person(b, 2), Cons(Person(c, -2), Cons(Person(d, 3), Nil())))) => Cons(b, Cons(d, Nil()))
case Cons(Person(a, -2), Cons(Person(b, -1), Cons(Person(c, -3), Cons(Person(d, -2), Nil())))) => Nil()
case Nil() => Nil()
}
}
}

0 comments on commit ee790fe

Please sign in to comment.