From baa60750b30f0142b2fc2519432cc1036d8dd4a5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <a-mikmay@microsoft.com>
Date: Wed, 25 Nov 2015 14:07:26 +0100
Subject: [PATCH] Added support for stream of templates. Now the Boolean
problem is solved. Removed duplicate methods already present in
StreamUtils.scala Added benchmark JsonRender.scala
---
.../leon/programsets/DirectProgramSet.scala | 5 +-
.../leon/programsets/JoinProgramSet.scala | 55 +++-----
.../scala/leon/programsets/ProgramSet.scala | 4 +-
.../leon/programsets/UnionProgramset.scala | 20 +--
.../scala/leon/purescala/PrettyPrinter.scala | 13 +-
.../scala/leon/purescala/ScalaPrinter.scala | 8 ++
src/main/scala/leon/purescala/Types.scala | 2 +-
src/main/scala/leon/synthesis/Rules.scala | 4 +-
.../leon/synthesis/rules/StringRender.scala | 123 ++++++++++++------
src/main/scala/leon/utils/StreamUtils.scala | 32 +++++
.../solvers/StringSolverSuite.scala | 4 +-
testcases/stringrender/JsonRender.scala | 42 ++++++
12 files changed, 210 insertions(+), 102 deletions(-)
create mode 100644 testcases/stringrender/JsonRender.scala
diff --git a/src/main/scala/leon/programsets/DirectProgramSet.scala b/src/main/scala/leon/programsets/DirectProgramSet.scala
index e9d45d4f6..1a08a98dd 100644
--- a/src/main/scala/leon/programsets/DirectProgramSet.scala
+++ b/src/main/scala/leon/programsets/DirectProgramSet.scala
@@ -6,10 +6,13 @@ import purescala.Extractors._
import purescala.Constructors._
import purescala.Types._
+object DirectProgramSet {
+ def apply[T](p: Stream[T]): DirectProgramSet[T] = new DirectProgramSet(p)
+}
/**
* @author Mikael
*/
-class DirectProgramSet(val p: Stream[Expr]) extends ProgramSet {
+class DirectProgramSet[T](val p: Stream[T]) extends ProgramSet[T] {
def programs = p
}
\ No newline at end of file
diff --git a/src/main/scala/leon/programsets/JoinProgramSet.scala b/src/main/scala/leon/programsets/JoinProgramSet.scala
index 9f5045050..e12442c9e 100644
--- a/src/main/scala/leon/programsets/JoinProgramSet.scala
+++ b/src/main/scala/leon/programsets/JoinProgramSet.scala
@@ -1,4 +1,5 @@
-package leon.programsets
+package leon
+package programsets
import leon.purescala
import purescala.Expressions._
@@ -6,46 +7,30 @@ import purescala.Extractors._
import purescala.Constructors._
import purescala.Types._
+/**
+ * @author Mikael
+ */
object JoinProgramSet {
- def cantorPair(x: Int, y: Int): Int = {
- ((x + y) * (x + y + 1)) / 2 + y
+ def apply[T, U1, U2](sets: (ProgramSet[U1], ProgramSet[U2]), recombine: (U1, U2) => T): Join2ProgramSet[T, U1, U2] = {
+ new Join2ProgramSet(sets, recombine)
}
-
-
- def reverseCantorPair(z: Int): (Int, Int) = {
- val t = Math.floor((-1.0f + Math.sqrt(1.0f + 8.0f * z))/2.0f).toInt;
- val x = t * (t + 3) / 2 - z;
- val y = z - t * (t + 1) / 2;
- (x, y)
+ def apply[T, U](sets: Seq[ProgramSet[U]], recombine: Seq[U] => T): JoinProgramSet[T, U] = {
+ new JoinProgramSet(sets, recombine)
}
-
- /** Combines two streams into one using cantor's unparining function.
- * Ensures that the stream terminates if both streams terminate */
- def combine[A, B](sa: Stream[A], sb: Stream[B]): Stream[(A, B)] = {
- def combineRec[A, B](sa: Stream[A], sb: Stream[B])(i: Int): Stream[(A, B)] = {
- val (x, y) = reverseCantorPair(i)
- if(!sa.isDefinedAt(x) && !sb.isDefinedAt(y)) Stream.Empty
- else if(sa.isDefinedAt(x) && sb.isDefinedAt(y)) (sa(x), sb(y)) #:: combineRec(sa, sb)(i+1)
- else combineRec(sa, sb)(i+1)
- }
- combineRec(sa, sb)(0)
+ def direct[U1, U2](sets: (ProgramSet[U1], ProgramSet[U2])): Join2ProgramSet[(U1, U2), U1, U2] = {
+ new Join2ProgramSet(sets, (u1: U1, u2: U2) => (u1, u2))
}
-
- /** Combines an arbitrary number of streams together. */
- def combine[A](sa: Seq[Stream[A]]): Stream[Seq[A]] = {
- if(sa.length == 0) Stream(Seq()) else
- if(sa.length == 1) sa(0).map(k => Seq(k)) else
- if(sa.length == 2) combine(sa(0), sa(1)).map(k => Seq(k._1, k._2)) else // Optimization
- combine(combine(sa.take(sa.length / 2)), combine(sa.drop(sa.length / 2))).map(k => k._1 ++ k._2)
+ def direct[U](sets: Seq[ProgramSet[U]]): JoinProgramSet[Seq[U], U] = {
+ new JoinProgramSet(sets, (id: Seq[U]) => id)
}
}
+class Join2ProgramSet[T, U1, U2](sets: (ProgramSet[U1], ProgramSet[U2]), recombine: (U1, U2) => T) extends ProgramSet[T] {
+ def programs: Stream[T] = utils.StreamUtils.cartesianProduct(sets._1.programs, sets._2.programs).map(recombine.tupled)
+}
+
+class JoinProgramSet[T, U](sets: Seq[ProgramSet[U]], recombine: Seq[U] => T) extends ProgramSet[T] {
+ def programs: Stream[T] = utils.StreamUtils.cartesianProduct(sets.map(_.programs)).map(recombine)
+}
-/**
- * @author Mikael
- */
-class JoinProgramSet(sets: Seq[ProgramSet], recombine: Seq[Expr] => Expr) extends ProgramSet {
-
- def programs: Stream[Expr] = JoinProgramSet.combine(sets.map(_.programs)).map(recombine)
-}
\ No newline at end of file
diff --git a/src/main/scala/leon/programsets/ProgramSet.scala b/src/main/scala/leon/programsets/ProgramSet.scala
index 453aeb4bc..04025f016 100644
--- a/src/main/scala/leon/programsets/ProgramSet.scala
+++ b/src/main/scala/leon/programsets/ProgramSet.scala
@@ -9,6 +9,6 @@ import purescala.Types._
/**
* @author Mikael
*/
-abstract class ProgramSet {
- def programs: Stream[Expr]
+abstract class ProgramSet[T] {
+ def programs: Stream[T]
}
\ No newline at end of file
diff --git a/src/main/scala/leon/programsets/UnionProgramset.scala b/src/main/scala/leon/programsets/UnionProgramset.scala
index 8fdc39d4c..2e089b6bb 100644
--- a/src/main/scala/leon/programsets/UnionProgramset.scala
+++ b/src/main/scala/leon/programsets/UnionProgramset.scala
@@ -1,4 +1,5 @@
-package leon.programsets
+package leon
+package programsets
import leon.purescala
import purescala.Expressions._
@@ -7,23 +8,14 @@ import purescala.Constructors._
import purescala.Types._
object UnionProgramSet {
-
- /** Interleaves two streams, ensuring that if both terminate, the resulting stream terminates. */
- def combine[A](sa: Stream[A], sb: Stream[A]): Stream[A] = {
- if(sa.isEmpty) sb else if(sb.isEmpty) sa else sa.head #:: combine(sb, sa.tail)
- }
-
- /** Interleaves an arbitrary number of streams, ensuring that if all of them terminate, the resulting stream terminates. */
- def combine[A](s: Seq[Stream[A]]): Stream[A] = {
- if(s.isEmpty) Stream.Empty else
- if(s.head.isEmpty) combine(s.tail) else
- s.head.head #:: combine(s.tail ++ Seq(s.head.tail))
+ def apply[T](sets: Seq[ProgramSet[T]]): UnionProgramSet[T] = {
+ new UnionProgramSet(sets)
}
}
/**
* @author Mikael
*/
-class UnionProgramset(sets: Seq[ProgramSet]) extends ProgramSet {
- def programs = UnionProgramSet.combine(sets.map(_.programs))
+class UnionProgramSet[T](sets: Seq[ProgramSet[T]]) extends ProgramSet[T] {
+ def programs = utils.StreamUtils.interleave(sets.map(_.programs))
}
\ No newline at end of file
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index dd62e8b85..f77fc57bd 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -50,6 +50,8 @@ class PrettyPrinter(opts: PrinterOptions,
p"${df.id}"
}
}
+
+ private val dbquote = "\""
def pp(tree: Tree)(implicit ctx: PrinterContext): Unit = {
@@ -167,7 +169,7 @@ class PrettyPrinter(opts: PrinterOptions,
case IntegerToString(expr) => p"StrOps.bigIntToString($expr)"
case CharToString(expr) => p"StrOps.charToString($expr)"
case RealToString(expr) => p"StrOps.realToString($expr)"
- case StringConcat(lhs, rhs) => p"$lhs + $rhs"
+ case StringConcat(lhs, rhs) => optP { p"$lhs + $rhs" }
case SubString(expr, start, end) => p"StrOps.substring($expr, $start, $end)"
case StringLength(expr) => p"StrOps.length($expr)"
@@ -180,7 +182,13 @@ class PrettyPrinter(opts: PrinterOptions,
case CharLiteral(v) => p"$v"
case BooleanLiteral(v) => p"$v"
case UnitLiteral() => p"()"
- case StringLiteral(v) => p""""$v""""
+ case StringLiteral(v) =>
+ if(v.indexOf("\n") != -1 && v.indexOf("\"\"\"") == -1) {
+ p"$dbquote$dbquote$dbquote$v$dbquote$dbquote$dbquote"
+ } else {
+ val escaped = v.replaceAll(dbquote, "\\\\\"").replaceAll("\n","\\n").replaceAll("\r","\\r")
+ p"$dbquote$escaped$dbquote"
+ }
case GenericValue(tp, id) => p"$tp#$id"
case Tuple(exprs) => p"($exprs)"
case TupleSelect(t, i) => p"$t._$i"
@@ -623,6 +631,7 @@ class PrettyPrinter(opts: PrinterOptions,
case (_, Some(_: Require)) => false
case (_, Some(_: Definition)) => false
case (_, Some(_: MatchExpr | _: MatchCase | _: Let | _: LetDef | _: IfExpr | _ : CaseClass | _ : Lambda)) => false
+ case (ex: StringConcat, Some(_: StringConcat)) => false
case (b1 @ BinaryMethodCall(_, _, _), Some(b2 @ BinaryMethodCall(_, _, _))) if precedence(b1) > precedence(b2) => false
case (BinaryMethodCall(_, _, _), Some(_: FunctionInvocation)) => true
case (_, Some(_: FunctionInvocation)) => false
diff --git a/src/main/scala/leon/purescala/ScalaPrinter.scala b/src/main/scala/leon/purescala/ScalaPrinter.scala
index e030086b9..8ef0cc52f 100644
--- a/src/main/scala/leon/purescala/ScalaPrinter.scala
+++ b/src/main/scala/leon/purescala/ScalaPrinter.scala
@@ -15,6 +15,7 @@ class ScalaPrinter(opts: PrinterOptions,
opgm: Option[Program],
sb: StringBuffer = new StringBuffer) extends PrettyPrinter(opts, opgm, sb) {
+ private val dbquote = "\""
override def pp(tree: Tree)(implicit ctx: PrinterContext): Unit = {
tree match {
@@ -39,6 +40,13 @@ class ScalaPrinter(opts: PrinterOptions,
case m @ FiniteMap(els, k, v) => p"Map[$k,$v]($els)"
case InfiniteIntegerLiteral(v) => p"BigInt($v)"
+ case StringLiteral(v) =>
+ if(v.indexOf("\n") != -1 && v.indexOf("\"\"\"") == -1) {
+ p"$dbquote$dbquote$dbquote$v$dbquote$dbquote$dbquote"
+ } else {
+ val escaped = v.replaceAll(dbquote, "\\\\\"").replaceAll("\n","\\n").replaceAll("\r","\\r")
+ p"$dbquote$escaped$dbquote"
+ }
case a@FiniteArray(elems, oDef, size) =>
import ExprOps._
diff --git a/src/main/scala/leon/purescala/Types.scala b/src/main/scala/leon/purescala/Types.scala
index e69678d1f..654971373 100644
--- a/src/main/scala/leon/purescala/Types.scala
+++ b/src/main/scala/leon/purescala/Types.scala
@@ -110,7 +110,7 @@ object Types {
def knownDescendants = classDef.knownDescendants.map( _.typed(tps) )
- def knownCCDescendants = classDef.knownCCDescendants.map( _.typed(tps) )
+ def knownCCDescendants: Seq[CaseClassType] = classDef.knownCCDescendants.map( _.typed(tps) )
lazy val fieldsTypes = fields.map(_.getType)
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 0f5894259..5565aa4e5 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -37,6 +37,7 @@ abstract class PreprocessingRule(name: String) extends Rule(name) {
object Rules {
/** Returns the list of all available rules for synthesis */
def all = List[Rule](
+ StringRender,
Unification.DecompTrivialClash,
Unification.OccursCheck, // probably useless
Disunification.Decomp,
@@ -61,8 +62,7 @@ object Rules {
//IntegerEquation,
//IntegerInequalities,
IntInduction,
- InnerCaseSplit,
- StringRender
+ InnerCaseSplit
//new OptimisticInjection(_),
//new SelectiveInlining(_),
//ADTLongInduction,
diff --git a/src/main/scala/leon/synthesis/rules/StringRender.scala b/src/main/scala/leon/synthesis/rules/StringRender.scala
index a53084a00..140de9f11 100644
--- a/src/main/scala/leon/synthesis/rules/StringRender.scala
+++ b/src/main/scala/leon/synthesis/rules/StringRender.scala
@@ -27,6 +27,7 @@ import leon.solvers.ModelBuilder
import leon.solvers.string.StringSolver
import scala.annotation.tailrec
import leon.purescala.DefOps
+import leon.programsets.{UnionProgramSet, DirectProgramSet, JoinProgramSet}
/** A template generator for a given type tree.
@@ -139,9 +140,9 @@ case object StringRender extends Rule("StringRender") {
}
/** Returns a stream of assignments compatible with input/output examples */
- def findAssignments(ctx: LeonContext, p: Program, inputs: Seq[Identifier], examples: ExamplesBank, template: Expr)(implicit hctx: SearchContext): Stream[Map[Identifier, String]] = {
+ def findAssignments(p: Program, inputs: Seq[Identifier], examples: ExamplesBank, template: Expr)(implicit hctx: SearchContext): Stream[Map[Identifier, String]] = {
//new Evaluator()
- val e = new StringTracingEvaluator(ctx, p)
+ val e = new StringTracingEvaluator(hctx.context, p)
@tailrec def gatherEquations(s: List[InOutExample], acc: ListBuffer[Equation] = ListBuffer()): Option[SProblem] = s match {
case Nil => Some(acc.toList)
@@ -154,45 +155,66 @@ case object StringRender extends Rule("StringRender") {
val evalResult = e.eval(template, modelResult)
evalResult.result match {
case None =>
- ctx.reporter.debug("Eval = None : ["+template+"] in ["+inputs.zip(in)+"]")
+ hctx.reporter.debug("Eval = None : ["+template+"] in ["+inputs.zip(in)+"]")
None
case Some((sfExpr, abstractSfExpr)) =>
//ctx.reporter.debug("Eval = ["+sfExpr+"] (from "+abstractSfExpr+")")
val sf = toStringForm(sfExpr)
val rhs = toStringLiteral(rhExpr.head)
if(sf.isEmpty || rhs.isEmpty) {
- ctx.reporter.ifDebug(printer => printer("sf empty or rhs empty ["+sfExpr+"] => ["+sf+"] in ["+rhs+"]"))
+ hctx.reporter.ifDebug(printer => printer("sf empty or rhs empty ["+sfExpr+"] => ["+sf+"] in ["+rhs+"]"))
None
} else gatherEquations(q, acc += ((sf.get, rhs.get)))
}
} else {
- ctx.reporter.ifDebug(printer => printer("RHS.length != 1 : ["+rhExpr+"]"))
+ hctx.reporter.ifDebug(printer => printer("RHS.length != 1 : ["+rhExpr+"]"))
None
}
}
gatherEquations(examples.valids.collect{ case io:InOutExample => io }.toList) match {
case Some(problem) =>
- ctx.reporter.ifDebug(printer => printer("Problem: ["+StringSolver.renderProblem(problem)+"]"))
+ //hctx.reporter.ifDebug(printer => printer("Problem: ["+StringSolver.renderProblem(problem)+"]"))
StringSolver.solve(problem)
case None =>
- ctx.reporter.ifDebug(printer => printer("No problem found"))
+ hctx.reporter.ifDebug(printer => printer("No problem found"))
Stream.empty
}
}
- def findSolutions(examples: ExamplesBank, program: Program, template: Expr, templateWithInlineDefs: Expr)(implicit hctx: SearchContext, p: Problem): RuleApplication = {
- val solutions = findAssignments(hctx.context, program, p.as, examples, template)
- //hctx.reporter.ifDebug(printer => printer("Solutions: ["+solutions.toList+"]"))
+ def findSolutions(examples: ExamplesBank, template: Stream[Expr], funDefs: Seq[(FunDef, Stream[Expr])])(implicit hctx: SearchContext, p: Problem): RuleApplication = {
+ // Fun is a stream of many function applications.
+ val funs= JoinProgramSet.direct(funDefs.map(fbody => fbody._2.map((fbody._1, _))).map(d => DirectProgramSet(d)))
- solutionStreamToRuleApplication(p, templateWithInlineDefs, solutions)
+ val wholeTemplates = JoinProgramSet.direct(funs, DirectProgramSet(template))
+
+ /*val newProgram = DefOps.addFunDefs(hctx.program, funDefs.values, hctx.sctx.functionContext)
+ val newExpr = (expr /: funDefs.values) {
+ case (e, fd) => LetDef(fd, e)
+ }*/
+ def computeSolutions(funDefsBodies: Seq[(FunDef, Expr)], template: Expr): Stream[Assignment] = {
+ val funDefs = for((funDef, body) <- funDefsBodies) yield { funDef.body = Some(body); funDef }
+ val newProgram = DefOps.addFunDefs(hctx.program, funDefs, hctx.sctx.functionContext)
+ findAssignments(newProgram, p.as, examples, template)
+ }
+
+ val tagged_solutions =
+ for{(funDefs, template) <- wholeTemplates.programs} yield computeSolutions(funDefs, template).map((funDefs, template, _))
+
+ solutionStreamToRuleApplication(p, leon.utils.StreamUtils.interleave(tagged_solutions))
}
- def solutionStreamToRuleApplication(p: Problem, template: Expr, solutions: Stream[Assignment]): RuleApplication = {
+ def solutionStreamToRuleApplication(p: Problem, solutions: Stream[(Seq[(FunDef, Expr)], Expr, Assignment)]): RuleApplication = {
if(solutions.isEmpty) RuleFailed() else {
- RuleClosed(solutions.map((assignment: Map[Identifier, String]) => {
- val term = ExprOps.simplifyString(ExprOps.replaceFromIDs(assignment.mapValues(StringLiteral), template))
- Solution(pre=p.pc, defs=Set(), term=term)
- }))
+ RuleClosed(
+ for((funDefsBodies, singleTemplate, assignment) <- solutions) yield {
+ val template = (singleTemplate /: funDefsBodies) {
+ case (e, (fd, body)) =>
+ fd.body = Some(body)
+ LetDef(fd, e)
+ }
+ val term = ExprOps.simplifyString(ExprOps.replaceFromIDs(assignment.mapValues(StringLiteral), template))
+ Solution(pre=p.pc, defs=Set(), term=term)
+ })
}
}
@@ -216,9 +238,9 @@ case object StringRender extends Rule("StringRender") {
}
/** Pre-updates of the function definition */
- def preUpdateFunDefBody(tpe: DependentType, fd: FunDef, assignments: Map[DependentType, FunDef]): Map[DependentType, FunDef] = {
+ def preUpdateFunDefBody(tpe: DependentType, fd: FunDef, assignments: Map[DependentType, (FunDef, Stream[Expr])]): Map[DependentType, (FunDef, Stream[Expr])] = {
assignments.get(tpe) match {
- case None => assignments + (tpe -> fd)
+ case None => assignments + (tpe -> ((fd, Stream.Empty)))
case Some(_) => assignments
}
}
@@ -230,29 +252,36 @@ case object StringRender extends Rule("StringRender") {
**/
def createFunDefsTemplates(
currentCaseClassParent: Option[TypeTree],
- adtToString: Map[DependentType, FunDef],
- inputs: Seq[Identifier])(implicit hctx: SearchContext): (Expr, Map[DependentType, FunDef]) = {
+ adtToString: Map[DependentType, (FunDef, Stream[Expr])],
+ inputs: Seq[Identifier])(implicit hctx: SearchContext): (Stream[Expr], Map[DependentType, (FunDef, Stream[Expr])]) = {
/* Returns a list of expressions converting the list of inputs to string.
* Holes should be inserted before, after and in-between for solving concatenation.
* @return Along with the list, an updated function definitions to transform (parent-dependent) types to strings */
@tailrec def gatherInputs(
currentCaseClassParent: Option[TypeTree],
- assignments1: Map[DependentType, FunDef],
+ assignments1: Map[DependentType, (FunDef, Stream[Expr])],
inputs: List[Identifier],
- result: ListBuffer[Expr] = ListBuffer()): (List[Expr], Map[DependentType, FunDef]) = inputs match {
+ result: ListBuffer[Stream[Expr]] = ListBuffer()): (List[Stream[Expr]], Map[DependentType, (FunDef, Stream[Expr])]) = inputs match {
case Nil => (result.toList, assignments1)
case input::q =>
val dependentType = DependentType(currentCaseClassParent, input.getType)
assignments1.get(dependentType) match {
case Some(fd) =>
- gatherInputs(currentCaseClassParent, assignments1, q, result += functionInvocation(fd, Seq(Variable(input))))
+ // TODO : Maybe find other functions.
+ gatherInputs(currentCaseClassParent, assignments1, q, result += Stream(functionInvocation(fd._1, Seq(Variable(input)))))
case None => // No function can render the current type.
input.getType match {
- case BooleanType => // Special case.
- gatherInputs(currentCaseClassParent, assignments1, q, result += booleanTemplate(input).instantiate)
+ case StringType =>
+ gatherInputs(currentCaseClassParent, assignments1, q, result += Stream(Variable(input)))
+ case BooleanType =>
+ // Special case. But might be overkill.
+ // It should be possible to have generic conversion instead, else it needs two examples, which might be cu
+ // gatherInputs(currentCaseClassParent, assignments1, q, result += booleanTemplate(input).instantiate)
+ // OR
+ gatherInputs(currentCaseClassParent, assignments1, q, result += Stream(BooleanToString(Variable(input)), booleanTemplate(input).instantiate))
case WithStringconverter(converter) => // Base case
- gatherInputs(currentCaseClassParent, assignments1, q, result += converter(Variable(input)))
+ gatherInputs(currentCaseClassParent, assignments1, q, result += Stream(converter(Variable(input))))
case t: ClassType =>
// Create the empty function body and updates the assignments parts.
val fd = createEmptyFunDef(dependentType)
@@ -260,26 +289,32 @@ case object StringRender extends Rule("StringRender") {
t.root match {
case act@AbstractClassType(acd@AbstractClassDef(id, tparams, parent), tps) =>
// Create a complete FunDef body with pattern matching
- val (assignments3, cases) = ((assignments2, ListBuffer[MatchCase]()) /: act.knownCCDescendants) {
+ val (assignments3, cases) = ((assignments2, ListBuffer[Stream[MatchCase]]()) /: act.knownCCDescendants) {
case ((assignments2tmp, acc), CaseClassType(ccd@CaseClassDef(id, tparams, parent, isCaseObject), tparams2)) =>
val typeMap = tparams.zip(tparams2).toMap
def resolveType(t: TypeTree): TypeTree = TypeOps.instantiateType(t, typeMap)
val fields = ccd.fields.map(vd => ( TypeOps.instantiateType(vd, typeMap).id ))
val pattern = CaseClassPattern(None, ccd.typed(tparams2), fields.map(k => WildcardPattern(Some(k))))
val (rhs, assignments2tmp2) = createFunDefsTemplates(Some(t), assignments2tmp, fields) // Invoke functions for each of the fields.
- (assignments2tmp2, acc += MatchCase(pattern, None, rhs))
+ (assignments2tmp2, acc += rhs.map(MatchCase(pattern, None, _)))
case ((adtToString, acc), e) => hctx.reporter.fatalError("Could not handle this class definition for string rendering " + e)
}
- fd.body = Some(MatchExpr(Variable(fd.params(0).id), cases))
- gatherInputs(currentCaseClassParent, assignments3, q, result += functionInvocation(fd, Seq(Variable(input))))
+ val recombine = (cases: Seq[MatchCase]) => MatchExpr(Variable(fd.params(0).id), cases)
+ val allMatchExprs = JoinProgramSet(cases.map(DirectProgramSet(_)), recombine).programs
+ val assignments4 = assignments3 + (dependentType -> (fd, allMatchExprs))
+ gatherInputs(currentCaseClassParent, assignments4, q, result += Stream(functionInvocation(fd, Seq(Variable(input)))))
case cct@CaseClassType(ccd@CaseClassDef(id, tparams, parent, isCaseObject), tparams2) =>
val typeMap = tparams.zip(tparams2).toMap
def resolveType(t: TypeTree): TypeTree = TypeOps.instantiateType(t, typeMap)
val fields = ccd.fields.map(vd => TypeOps.instantiateType(vd, typeMap).id)
val pattern = CaseClassPattern(None, ccd.typed(tparams2), fields.map(k => WildcardPattern(Some(k))))
val (rhs, assignments3) = createFunDefsTemplates(Some(t), assignments2, fields) // Invoke functions for each of the fields.
- fd.body = Some(MatchExpr(Variable(fd.params(0).id), Seq(MatchCase(pattern, None, rhs))))
- gatherInputs(currentCaseClassParent, assignments3, q, result += functionInvocation(fd, Seq(Variable(input))))
+
+ val recombine = (cases: Seq[MatchCase]) => MatchExpr(Variable(fd.params(0).id), cases)
+ val cases = rhs.map(MatchCase(pattern, None, _))
+ val allMatchExprs = cases.map(acase => recombine(Seq(acase)))
+ val assignments4 = assignments3 + (dependentType -> (fd, allMatchExprs))
+ gatherInputs(currentCaseClassParent, assignments4, q, result += Stream(functionInvocation(fd, Seq(Variable(input)))))
}
case TypeParameter(t) =>
hctx.reporter.fatalError("Could not handle type parameter for string rendering " + t)
@@ -291,21 +326,23 @@ case object StringRender extends Rule("StringRender") {
val (exprs, assignments) = gatherInputs(currentCaseClassParent, adtToString, inputs.toList)
/** Add post, pre and in-between holes, and returns a single expr along with the new assignments. */
- val template = exprs match {
+ val template: Stream[Expr] = exprs match {
case Nil =>
- StringTemplateGenerator(Hole => Hole).instantiate
+ Stream(StringTemplateGenerator(Hole => Hole).instantiate)
case exprList =>
- StringTemplateGenerator(Hole => {
- StringConcat((StringConcat(Hole, exprs.head) /: exprs.tail) {
- case (finalExpr, expr) => StringConcat(StringConcat(finalExpr, Hole), expr)
- }, Hole)
- }).instantiate
+ JoinProgramSet(exprList.map(DirectProgramSet(_)), (exprs: Seq[Expr]) =>
+ StringTemplateGenerator(Hole => {
+ StringConcat((StringConcat(Hole, exprs.head) /: exprs.tail) {
+ case (finalExpr, expr) => StringConcat(StringConcat(finalExpr, Hole), expr)
+ }, Hole)
+ }).instantiate
+ ).programs
}
(template, assignments)
}
def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
-
+ hctx.reporter.debug("StringRender:Output variables="+p.xs+", their types="+p.xs.map(_.getType))
p.xs match {
case List(IsTyped(v, StringType)) =>
val description = "Creates a standard string conversion function"
@@ -344,11 +381,11 @@ case object StringRender extends Rule("StringRender") {
))
hctx.reporter.ifDebug(printer => printer("Inferred expression:\n" + expr + toDebug))
- val newProgram = DefOps.addFunDefs(hctx.program, funDefs.values, hctx.sctx.functionContext)
+ /*val newProgram = DefOps.addFunDefs(hctx.program, funDefs.values, hctx.sctx.functionContext)
val newExpr = (expr /: funDefs.values) {
case (e, fd) => LetDef(fd, e)
- }
- findSolutions(examples, newProgram, expr, newExpr)
+ }*/
+ findSolutions(examples, expr, funDefs.values.toSeq)
}
ruleInstantiations.toList
diff --git a/src/main/scala/leon/utils/StreamUtils.scala b/src/main/scala/leon/utils/StreamUtils.scala
index 2ea08a593..09a09ce40 100644
--- a/src/main/scala/leon/utils/StreamUtils.scala
+++ b/src/main/scala/leon/utils/StreamUtils.scala
@@ -4,6 +4,14 @@ package leon.utils
object StreamUtils {
+ /** Interleaves a stream of streams.
+ * {{{
+ * If streams = ((1,2,3),(4,5),(6,7,8,9),(10...),
+ * Order taken 0 1 2
+ * Order taken 3 4 5 6 7
+ * Order taken 8 9}}}
+ * interleave(streams) = (1, 2, 4, 3, 5, 6, 7, 10, 8, 9...
+ **/
def interleave[T](streams: Stream[Stream[T]]): Stream[T] = {
def rec(streams: Stream[Stream[T]], diag: Int): Stream[T] = {
if(streams.isEmpty) Stream() else {
@@ -15,6 +23,7 @@ object StreamUtils {
rec(streams, 1)
}
+ /** Applies the interleaving to a finite sequence of streams. */
def interleave[T](streams : Seq[Stream[T]]) : Stream[T] = {
if (streams.isEmpty) Stream() else {
val nonEmpty = streams filter (_.nonEmpty)
@@ -22,6 +31,29 @@ object StreamUtils {
}
}
+ private def cantorPair(x: Int, y: Int): Int = {
+ ((x + y) * (x + y + 1)) / 2 + y
+ }
+
+ private def reverseCantorPair(z: Int): (Int, Int) = {
+ val t = Math.floor((-1.0f + Math.sqrt(1.0f + 8.0f * z))/2.0f).toInt;
+ val x = t * (t + 3) / 2 - z;
+ val y = z - t * (t + 1) / 2;
+ (x, y)
+ }
+
+ /** Combines two streams into one using cantor's unpairing function.
+ * Ensures that the stream terminates if both streams terminate */
+ def cartesianProduct[A, B](sa: Stream[A], sb: Stream[B]): Stream[(A, B)] = {
+ def combineRec[A, B](sa: Stream[A], sb: Stream[B])(i: Int): Stream[(A, B)] = {
+ val (x, y) = reverseCantorPair(i)
+ if(!sa.isDefinedAt(x) && !sb.isDefinedAt(y)) Stream.Empty
+ else if(sa.isDefinedAt(x) && sb.isDefinedAt(y)) (sa(x), sb(y)) #:: combineRec(sa, sb)(i+1)
+ else combineRec(sa, sb)(i+1)
+ }
+ combineRec(sa, sb)(0)
+ }
+
def cartesianProduct[T](streams : Seq[Stream[T]]) : Stream[List[T]] = {
val dimensions = streams.size
val vectorizedStreams = streams.map(new VectorizedStream(_))
diff --git a/src/test/scala/leon/integration/solvers/StringSolverSuite.scala b/src/test/scala/leon/integration/solvers/StringSolverSuite.scala
index fcb7d3080..dc34901da 100644
--- a/src/test/scala/leon/integration/solvers/StringSolverSuite.scala
+++ b/src/test/scala/leon/integration/solvers/StringSolverSuite.scala
@@ -168,7 +168,7 @@ class StringSolverSuite extends FunSuite with Matchers {
solve(problem) should not be 'empty
}
- /*test("solveJadProblem") {
+ test("solveJadProblem") {
val lhs = """const26+const22+const7+const+const8+const3+const9+const5+"5"+const6+const10+const23+const18+const11+const+const12+const19+const18+const7+const1+const8+const2+const9+const4+const10+const19+const18+const13+const+const14+const3+const15+const5+"5"+const6+const16+const4+const17+const19+const18+const11+const1+const12+const19+const18+const13+const1+const14+const2+const15+const4+const16+const5+"5"+const6+const17+const19+const21+const20+const20+const20+const20+const20+const24+const27"""
var idMap = Map[String, Identifier]()
val lhsSf = for(elem <- lhs.split("\\+")) yield {
@@ -195,5 +195,5 @@ T2: ret Pop() -> 5"""
println("Problem to solve:" + StringSolver.renderProblem(problem))
solve(problem) should not be 'empty
- }*/
+ }
}
\ No newline at end of file
diff --git a/testcases/stringrender/JsonRender.scala b/testcases/stringrender/JsonRender.scala
new file mode 100644
index 000000000..2b8587845
--- /dev/null
+++ b/testcases/stringrender/JsonRender.scala
@@ -0,0 +1,42 @@
+/**
+ * Name: ListRender.scala
+ * Creation: 14.10.2015
+ * Author: Mika�l Mayer (mikael.mayer@epfl.ch)
+ * Comments: First benchmark ever for solving string transformation problems. List specifications.
+ */
+
+import leon.lang._
+import leon.annotation._
+import leon.collection._
+import leon.collection.ListOps._
+import leon.lang.synthesis._
+
+object JsonRender {
+ /** Synthesis by example specs */
+ @inline def psStandard(x: Int, y: String, z: Boolean) = (res: String) =>((x, y, z), res) passes {
+ case (31, "routed", true) => """{ field1: 31, field2: "routed", field3: true }"""
+ }
+
+ @inline def psTupled1(xy: (Int, String), z: Boolean) = (res: String) =>((xy, z), res) passes {
+ case ((31, "routed"), true) => """{ field1: 31, field2: "routed", field3: true }"""
+ }
+
+ @inline def psTupled2(x: Int, yz: (String, Boolean)) = (res: String) =>((x, yz), res) passes {
+ case (31, ("routed", true)) => """{ field1: 31, field2: "routed", field3: true }"""
+ }
+
+ //////////////////////////////////////////////
+ // Non-incremental examples: pure synthesis //
+ //////////////////////////////////////////////
+ def synthesizeStandard(x: Int, y: String, z: Boolean): String = {
+ ???[String]
+ } ensuring psStandard(x, y, z)
+
+ def synthesizeTupled1(xy: (Int, String), z: Boolean): String = {
+ ???[String]
+ } ensuring psTupled1(xy, z)
+
+ def synthesizeTupled2(x: Int, yz: (String, Boolean)): String = {
+ ???[String]
+ } ensuring psTupled2(x, yz)
+}
\ No newline at end of file
--
GitLab