From 5ea6796fa4c3f3d09aa90f2fe9bc5015bc77da33 Mon Sep 17 00:00:00 2001
From: "Emmanouil (Manos) Koukoutos" <emmanouil.koukoutos@epfl.ch>
Date: Tue, 2 Dec 2014 17:58:16 +0100
Subject: [PATCH] Synthesis from examples
---
.../scala/leon/purescala/Extractors.scala | 6 ++
.../scala/leon/purescala/PrettyPrinter.scala | 1 -
src/main/scala/leon/synthesis/Problem.scala | 64 +++++++++++++++++--
.../synthesis/SynthesisRegressionSuite.scala | 4 ++
4 files changed, 70 insertions(+), 5 deletions(-)
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index 439d0888c..bfbcf0267 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -262,4 +262,10 @@ object Extractors {
}
}
+ object UnwrapTuplePattern {
+ def unapply(p : Pattern) : Option[Seq[Pattern]] = Option(p) map {
+ case TuplePattern(_,subs) => subs
+ case other => Seq(other)
+ }
+ }
}
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index b8ebf7c95..08dee1c71 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -321,7 +321,6 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
p"($args)"
}
-
case FunctionInvocation(tfd, args) =>
p"${tfd.id}"
diff --git a/src/main/scala/leon/synthesis/Problem.scala b/src/main/scala/leon/synthesis/Problem.scala
index d13b70d44..e56eb59a8 100644
--- a/src/main/scala/leon/synthesis/Problem.scala
+++ b/src/main/scala/leon/synthesis/Problem.scala
@@ -5,13 +5,15 @@ package synthesis
import leon.purescala.Trees._
import leon.purescala.TreeOps._
+import leon.purescala.TypeTrees.TypeTree
import leon.purescala.Common._
import leon.purescala.Constructors._
// Defines a synthesis triple of the form:
// ⟦ as ⟨ C | phi ⟩ xs ⟧
case class Problem(as: List[Identifier], pc: Expr, phi: Expr, xs: List[Identifier]) {
- override def toString = "⟦ "+as.mkString(";")+", "+(if (pc != BooleanLiteral(true)) pc+" ≺ " else "")+" ⟨ "+phi+" ⟩ "+xs.mkString(";")+" ⟧ "
+ override def toString =
+ "⟦ "+as.mkString(";")+", " + (if (pc != BooleanLiteral(true)) pc+" ≺ " else "") + " ⟨ "+phi+" ⟩ " + xs.mkString(";") + " ⟧ "
def getTests(sctx: SynthesisContext): Seq[Example] = {
import purescala.Extractors._
@@ -81,13 +83,67 @@ case class Problem(as: List[Identifier], pc: Expr, phi: Expr, xs: List[Identifie
case Tuple(is) => is.collect { case Variable(i) => i }.toList
case _ => Nil
}
+
+
+ def toIOExamples(in: Expr, out : Expr, cs : MatchCase) : Seq[(Expr,Expr)] = {
+ import utils.ExpressionGrammars
+ import bonsai._
+ import bonsai.enumerators._
+
+ val examplesPerVariable = 5
+
+ def doSubstitute(subs : Seq[(Identifier, Expr)], e : Expr) =
+ subs.foldLeft(e) {
+ case (from, (id, to)) => replaceFromIDs(Map(id -> to), from)
+ }
+
+ // The trivial example
+ if (cs.rhs == out)
+ Seq()
+ else {
+ // The pattern as expression (input expression)(may contain free variables)
+ val (pattExpr, ieMap) = patternToExpression(cs.pattern, in.getType)
+ val freeVars = variablesOf(pattExpr).toSeq
+
+ if (freeVars.isEmpty) {
+ // The input contains no free vars. Trivially return input-output pair
+ Seq((pattExpr, doSubstitute(ieMap,cs.rhs)))
+ } 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 grammar = ExpressionGrammars.BaseGrammar
+ val enum = new MemoizedEnumerator[TypeTree, Expr](grammar.getProductions _)
+ val types = freeVars.map{ _.getType }
+ val typesWithValues = types.map { tp => (tp, enum.iterator(tp).take(examplesPerVariable).toSeq) }.toMap
+ val values = freeVars map { v => typesWithValues(v.getType) }
+ // Make all combinations of all possible instantiations
+ def combinations[A](s : Seq[Seq[A]]) : Seq[Seq[A]] = {
+ if (s.isEmpty) Seq(Seq())
+ else for {
+ h <- s.head
+ t <- combinations(s.tail)
+ } yield (h +: t)
+ }
+ val instantiations = combinations(values) map { freeVars.zip(_).toMap }
+ instantiations map { inst =>
+ (replaceFromIDs(inst, pattExpr), replaceFromIDs(inst, doSubstitute(ieMap, cs.rhs)))
+ }
+ }
+
+ }
+ }
+
val evaluator = new DefaultEvaluator(sctx.context, sctx.program)
val testClusters = collect[Map[Identifier, Expr]] {
- case FunctionInvocation(tfd, List(in, out, FiniteMap(inouts))) if tfd.id.name == "passes" =>
- val infos = extractIds(Tuple(Seq(in, out)))
- val exs = inouts.map{ case (i, o) =>
+
+ //case FunctionInvocation(tfd, List(in, out, FiniteMap(inouts))) if tfd.id.name == "passes" =>
+ case p@Passes(ins, out, cases) =>
+
+ val ioPairs = cases flatMap { toIOExamples(ins,out,_) }
+ val infos = extractIds(p.scrutinee)
+ val exs = ioPairs.map{ case (i, o) =>
val test = Tuple(Seq(i, o))
val ids = variablesOf(test)
evaluator.eval(test, ids.map { (i: Identifier) => i -> i.toVariable }.toMap) match {
diff --git a/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala b/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala
index eeeadde94..89fe46ea0 100644
--- a/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala
+++ b/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala
@@ -53,6 +53,10 @@ class SynthesisRegressionSuite extends LeonTestSuite {
testSynthesis("Church", f, 200)
}
+ forEachFileIn("regression/synthesis/Examples/") { f =>
+ testSynthesis("IOExamples", f, 200)
+ }
+
forEachFileIn("regression/synthesis/List/") { f =>
testSynthesis("List", f, 200)
}
--
GitLab