From 22c2c20d887e9726e5ac8be76bd5539b8b0a138f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <mikael.mayer@epfl.ch>
Date: Mon, 9 May 2016 19:33:37 +0200
Subject: [PATCH] Support of string synthesis for Set, Map, List and Bag
---
.gitignore | 2 +
library/leon/lang/package.scala | 2 +-
.../leon/purescala/SelfPrettyPrinter.scala | 1 -
.../leon/synthesis/rules/StringRender.scala | 11 +++-
.../stringrender/MapSetBagListMkString.scala | 51 +++++++++++++++++++
5 files changed, 63 insertions(+), 4 deletions(-)
create mode 100644 testcases/stringrender/MapSetBagListMkString.scala
diff --git a/.gitignore b/.gitignore
index ef2d597a5..391915fd7 100644
--- a/.gitignore
+++ b/.gitignore
@@ -63,3 +63,5 @@ out-classes
/scalaz3.lib
/vcomp100.dll
/z3.exe
+/libz3java.dll
+/libz3java.lib
diff --git a/library/leon/lang/package.scala b/library/leon/lang/package.scala
index 9c3c72d42..12e18c523 100644
--- a/library/leon/lang/package.scala
+++ b/library/leon/lang/package.scala
@@ -92,7 +92,7 @@ package object lang {
}
}
- @extern
+ @extern @library
def print(x: String): Unit = {
scala.Predef.print(x)
}
diff --git a/src/main/scala/leon/purescala/SelfPrettyPrinter.scala b/src/main/scala/leon/purescala/SelfPrettyPrinter.scala
index bba231525..cc142d858 100644
--- a/src/main/scala/leon/purescala/SelfPrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/SelfPrettyPrinter.scala
@@ -64,7 +64,6 @@ trait PrettyPrinterFinder[T, U >: T] {
def buildLambda(inputType: TypeTree, fd: FunDef, slu: Stream[List[U]]): Stream[T]
def prettyPrinterFromCandidate(fd: FunDef, inputType: TypeTree)(implicit ctx: LeonContext, program: Program): Stream[T] = {
- println("Considering pretty printer " + fd.id.name + " with arg " + fd.params.head.getType + " for type " + inputType)
TypeOps.canBeSubtypeOf(inputType, fd.tparams.map(_.tp), fd.params.head.getType) match {
case Some(genericTypeMap) =>
println("Found a mapping")
diff --git a/src/main/scala/leon/synthesis/rules/StringRender.scala b/src/main/scala/leon/synthesis/rules/StringRender.scala
index 57b56f24a..b0bb9d505 100644
--- a/src/main/scala/leon/synthesis/rules/StringRender.scala
+++ b/src/main/scala/leon/synthesis/rules/StringRender.scala
@@ -416,8 +416,8 @@ case object StringRender extends Rule("StringRender") {
val exprs1s = (new SelfPrettyPrinter)
.allowFunction(hctx.functionContext)
.excludeFunction(hctx.functionContext)
- .prettyPrintersForType(input.getType)(hctx, hctx.program)
- .map(l => (application(l, Seq(input)), List[Identifier]())) // Use already pre-defined pretty printers.
+ .withPossibleParameters.prettyPrintersForType(input.getType)(hctx, hctx.program)
+ .map{ case (l, identifiers) => (application(l, Seq(input)), identifiers) } // Use already pre-defined pretty printers.
val exprs1 = exprs1s.toList.sortBy{ case (Lambda(_, FunctionInvocation(tfd, _)), _) if tfd.fd == hctx.functionContext => 0 case _ => 1}
val exprs2 = ctx.abstractStringConverters.getOrElse(input.getType, Nil).map(f => (f(input), List[Identifier]()))
val defaultConverters: Stream[WithIds[Expr]] = exprs1.toStream #::: exprs2.toStream
@@ -493,6 +493,13 @@ case object StringRender extends Rule("StringRender") {
} else {
gatherInputs(ctx, q, result += mergeResults(Stream.empty))
}
+
+ case t: SetType =>
+ gatherInputs(ctx, q, result += defaultConverters)
+ case t: BagType =>
+ gatherInputs(ctx, q, result += defaultConverters)
+ case t: MapType =>
+ gatherInputs(ctx, q, result += defaultConverters)
case tpe =>
hctx.reporter.fatalError("Could not handle class type for string rendering " + tpe)
}
diff --git a/testcases/stringrender/MapSetBagListMkString.scala b/testcases/stringrender/MapSetBagListMkString.scala
new file mode 100644
index 000000000..3d79aad59
--- /dev/null
+++ b/testcases/stringrender/MapSetBagListMkString.scala
@@ -0,0 +1,51 @@
+import leon.lang._
+import leon.collection._
+import leon.annotation._
+import leon.lang.synthesis._
+
+object StringTest {
+
+ def listToString(in : List[String]): String = {
+ ???[String]
+ } ensuring {
+ (res : String) => (in, res) passes {
+ case s if s == List("1", "2", "0") =>
+ "[1 ## 2 ## 0]"
+ case s if s == List[String]() =>
+ "[]"
+ }
+ }
+
+ def setToString(in : Set[String]): String = {
+ ???[String]
+ } ensuring {
+ (res : String) => (in, res) passes {
+ case s if s == Set[String]("1", "2", "0") =>
+ "{0 | 1 | 2}"
+ case s if s == Set[String]() =>
+ "{}"
+ }
+ }
+
+ def mapToString(in : Map[String, String]): String = {
+ ???[String]
+ } ensuring {
+ (res : String) => (in, res) passes {
+ case s if s == Map[String,String]("Title" -> "Modular Printing", "Abstract" -> "We discuss...", "Year" -> "2016") =>
+ "[Abstract --> We discuss..., Title --> Modular Printing, Year --> 2016]"
+ case s if s == Map[String,String]() =>
+ "[]"
+ }
+ }
+
+ def bagToString(in : Bag[String]): String = {
+ ???[String]
+ } ensuring {
+ (res : String) => (in, res) passes {
+ case s if s == Bag[String]("3" -> BigInt(2), "2" -> BigInt(1), "5" -> BigInt(3)) =>
+ "2*3*3*5*5*5"
+ case s if s == Bag[String]() =>
+ ""
+ }
+ }
+}
--
GitLab