From 7c9386d5cfdd032df0028740a1e8e1970d025bbc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <mikael.mayer@epfl.ch>
Date: Fri, 15 Jan 2016 12:48:08 +0100
Subject: [PATCH] Leon can handle abstract examples if the flag
`keepAbstractExamples` is set to true in ExamplesFinder. (It means that
examples will not be enumerated if they have free unassigned variables, but
kept as it.) input/output examples can now match only a part of the inputs,
but the output is still compulsory This is now used in StringRender.scala.
The functional example works.
---
.../evaluators/StringTracingEvaluator.scala | 10 +++
.../scala/leon/synthesis/ExamplesFinder.scala | 80 +++++++++++--------
.../leon/synthesis/rules/StringRender.scala | 12 +--
3 files changed, 64 insertions(+), 38 deletions(-)
diff --git a/src/main/scala/leon/evaluators/StringTracingEvaluator.scala b/src/main/scala/leon/evaluators/StringTracingEvaluator.scala
index 62cde913f..ab8b14055 100644
--- a/src/main/scala/leon/evaluators/StringTracingEvaluator.scala
+++ b/src/main/scala/leon/evaluators/StringTracingEvaluator.scala
@@ -66,6 +66,16 @@ class StringTracingEvaluator(ctx: LeonContext, prog: Program) extends Contextual
case _ =>
StringConcat(es1, es2)
}
+ case Application(caller, args) =>
+ val ecaller = e(caller)
+ ecaller match {
+ case l @ Lambda(params, body) =>
+ super.e(Application(ecaller, args))
+ case PartialLambda(mapping, dflt, _) =>
+ super.e(Application(ecaller, args))
+ case f =>
+ Application(f, args.map(e))
+ }
case expr =>
super.e(expr)
}
diff --git a/src/main/scala/leon/synthesis/ExamplesFinder.scala b/src/main/scala/leon/synthesis/ExamplesFinder.scala
index 3cc97f4f5..524642874 100644
--- a/src/main/scala/leon/synthesis/ExamplesFinder.scala
+++ b/src/main/scala/leon/synthesis/ExamplesFinder.scala
@@ -25,6 +25,10 @@ class ExamplesFinder(ctx0: LeonContext, program: Program) {
implicit val ctx = ctx0
val reporter = ctx.reporter
+
+ private var keepAbstractExamples = false
+
+ def setKeepAbstractExamples(b: Boolean) = { this.keepAbstractExamples = b; this}
def extractFromFunDef(fd: FunDef, partition: Boolean): ExamplesBank = fd.postcondition match {
case Some(Lambda(Seq(ValDef(id, _)), post)) =>
@@ -41,6 +45,8 @@ class ExamplesFinder(ctx0: LeonContext, program: Program) {
Some(InOutExample(fd.params.map(p => t(p.id)), Seq(t(id))))
} else if ((ids & insIds) == insIds) {
Some(InExample(fd.params.map(p => t(p.id))))
+ } else if((ids & outsIds) == outsIds) { // Examples provided on a part of the inputs.
+ Some(InOutExample(fd.params.map(p => t.getOrElse(p.id, Variable(p.id))), Seq(t(id))))
} else {
None
}
@@ -67,27 +73,31 @@ class ExamplesFinder(ctx0: LeonContext, program: Program) {
case None =>
ExamplesBank(Nil, Nil)
}
-
- // Extract examples from the passes found in expression
+
+ /** Extract examples from the passes found in expression */
def extractFromProblem(p: Problem): ExamplesBank = {
val testClusters = extractTestsOf(and(p.pc, p.phi))
// Finally, we keep complete tests covering all as++xs
val allIds = (p.as ++ p.xs).toSet
val insIds = p.as.toSet
-
+ val outsIds = p.xs.toSet
+
val examples = testClusters.toSeq.flatMap { t =>
val ids = t.keySet
if ((ids & allIds) == allIds) {
Some(InOutExample(p.as.map(t), p.xs.map(t)))
} else if ((ids & insIds) == insIds) {
Some(InExample(p.as.map(t)))
+ } else if((ids & outsIds) == outsIds) { // Examples provided on a part of the inputs.
+ Some(InOutExample(p.as.map(p => t.getOrElse(p, Variable(p))), p.xs.map(t)))
} else {
None
}
}
def isValidExample(ex: Example): Boolean = {
+ if(this.keepAbstractExamples) return true // TODO: Abstract interpretation here ?
val (mapping, cond) = ex match {
case io: InOutExample =>
(Map((p.as zip io.ins) ++ (p.xs zip io.outs): _*), And(p.pc, p.phi))
@@ -117,6 +127,7 @@ class ExamplesFinder(ctx0: LeonContext, program: Program) {
ExamplesBank(generatedExamples.toSeq ++ solverExamples.toList, Nil)
}
+ /** Extracts all passes constructs from the given postcondition, merges them if needed */
private def extractTestsOf(e: Expr): Set[Map[Identifier, Expr]] = {
val allTests = collect[Map[Identifier, Expr]] {
case Passes(ins, outs, cases) =>
@@ -135,7 +146,7 @@ class ExamplesFinder(ctx0: LeonContext, program: Program) {
}
// Check whether we can extract all ids from example
- val results = exs.collect { case e if infos.forall(_._2.isDefinedAt(e)) =>
+ val results = exs.collect { case e if infos.forall(_._2.isDefinedAt(e)) || this.keepAbstractExamples =>
infos.map{ case (id, f) => id -> f(e) }.toMap
}
@@ -149,7 +160,8 @@ class ExamplesFinder(ctx0: LeonContext, program: Program) {
consolidateTests(allTests)
}
-
+ /** Processes ((in, out) passes {
+ * cs[=>Case pattExpr if guard => outR]*/
private def caseToExamples(in: Expr, out: Expr, cs: MatchCase, examplesPerCase: Int = 5): Seq[(Expr,Expr)] = {
def doSubstitute(subs : Seq[(Identifier, Expr)], e : Expr) =
@@ -180,34 +192,38 @@ class ExamplesFinder(ctx0: LeonContext, program: Program) {
case (a, b, c) =>
None
}) 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 values = enum.iterator(tupleTypeWrap(freeVars.map { _.getType }))
- val instantiations = values.map {
- v => freeVars.zip(unwrapTuple(v, freeVars.size)).toMap
- }
-
- def filterGuard(e: Expr, mapping: Map[Identifier, Expr]): Boolean = cs.optGuard match {
- case Some(guard) =>
- // in -> e should be enough. We shouldn't find any subexpressions of in.
- evaluator.eval(replace(Map(in -> e), guard), mapping) match {
- case EvaluationResults.Successful(BooleanLiteral(true)) => true
- case _ => false
- }
-
- case None =>
- true
+ if(this.keepAbstractExamples) {
+ Seq((pattExpr, 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 enum = new MemoizedEnumerator[TypeTree, Expr](ValueGrammar.getProductions)
+ val values = enum.iterator(tupleTypeWrap(freeVars.map { _.getType }))
+ val instantiations = values.map {
+ v => freeVars.zip(unwrapTuple(v, freeVars.size)).toMap
+ }
+
+ def filterGuard(e: Expr, mapping: Map[Identifier, Expr]): Boolean = cs.optGuard match {
+ case Some(guard) =>
+ // in -> e should be enough. We shouldn't find any subexpressions of in.
+ evaluator.eval(replace(Map(in -> e), guard), mapping) match {
+ case EvaluationResults.Successful(BooleanLiteral(true)) => true
+ case _ => false
+ }
+
+ case None =>
+ true
+ }
+
+ if(cs.optGuard == Some(BooleanLiteral(false))) {
+ Nil
+ } else (for {
+ inst <- instantiations.toSeq
+ inR = replaceFromIDs(inst, pattExpr)
+ outR = replaceFromIDs(inst, doSubstitute(ieMap, cs.rhs))
+ if filterGuard(inR, inst)
+ } yield (inR, outR)).take(examplesPerCase)
}
-
- if(cs.optGuard == Some(BooleanLiteral(false))) {
- Nil
- } else (for {
- inst <- instantiations.toSeq
- inR = replaceFromIDs(inst, pattExpr)
- outR = replaceFromIDs(inst, doSubstitute(ieMap, cs.rhs))
- if filterGuard(inR, inst)
- } yield (inR, outR)).take(examplesPerCase)
}
}
}
diff --git a/src/main/scala/leon/synthesis/rules/StringRender.scala b/src/main/scala/leon/synthesis/rules/StringRender.scala
index 1f62ec67b..e8a78e143 100644
--- a/src/main/scala/leon/synthesis/rules/StringRender.scala
+++ b/src/main/scala/leon/synthesis/rules/StringRender.scala
@@ -190,7 +190,7 @@ case object StringRender extends Rule("StringRender") {
val evalResult = e.eval(template, modelResult)
evalResult.result match {
case None =>
- hctx.reporter.debug("Eval = None : ["+template+"] in ["+inputs.zip(in)+"]")
+ hctx.reporter.info("Eval = None : ["+template+"] in ["+inputs.zip(in)+"]")
None
case Some((sfExpr, abstractSfExpr)) =>
//ctx.reporter.debug("Eval = ["+sfExpr+"] (from "+abstractSfExpr+")")
@@ -202,16 +202,16 @@ case object StringRender extends Rule("StringRender") {
case Some(equations) =>
gatherEquations(q, acc ++= equations)
case None =>
- hctx.reporter.debug("Could not extract equations from ["+sfget+"] == ["+rhsget+"]")
+ hctx.reporter.info("Could not extract equations from ["+sfget+"] == ["+rhsget+"]")
None
}
case _ =>
- hctx.reporter.debug("sf empty or rhs empty ["+sfExpr+"] => ["+sf+"] in ["+rhs+"]")
+ hctx.reporter.info("sf empty or rhs empty ["+sfExpr+"] => ["+sf+"] in ["+rhs+"]")
None
}
}
} else {
- hctx.reporter.debug("RHS.length != 1 : ["+rhExpr+"]")
+ hctx.reporter.info("RHS.length != 1 : ["+rhExpr+"]")
None
}
}
@@ -237,7 +237,7 @@ case object StringRender extends Rule("StringRender") {
def computeSolutions(funDefsBodies: Seq[(FunDef, WithIds[Expr])], template: WithIds[Expr]): Stream[Assignment] = {
val funDefs = for((funDef, body) <- funDefsBodies) yield { funDef.body = Some(body._1); funDef }
val newProgram = DefOps.addFunDefs(hctx.program, funDefs, hctx.sctx.functionContext)
- findAssignments(newProgram, p.as, examples, template._1)
+ findAssignments(newProgram, p.as.filter{ x => !x.getType.isInstanceOf[FunctionType] }, examples, template._1)
}
val tagged_solutions =
@@ -573,7 +573,7 @@ case object StringRender extends Rule("StringRender") {
val defaultToStringFunctions = defaultMapTypeToString()
- val examplesFinder = new ExamplesFinder(hctx.context, hctx.program)
+ val examplesFinder = new ExamplesFinder(hctx.context, hctx.program).setKeepAbstractExamples(true)
val examples = examplesFinder.extractFromProblem(p)
val definedStringConverters: StringConverters =
--
GitLab