Support of string synthesis for Set, Map, List and Bag

.gitignore

@@ -63,3 +63,5 @@ out-classes
 /scalaz3.lib
 /vcomp100.dll
 /z3.exe
+/libz3java.dll
+/libz3java.lib

library/leon/lang/package.scala

@@ -92,7 +92,7 @@ package object lang {
     }
   }
 
-  @extern
+  @extern @library
   def print(x: String): Unit = {
     scala.Predef.print(x)
   }

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")

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)
           }

testcases/stringrender/MapSetBagListMkString.scala

+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]() =>
+        ""
+    }
+  }
+}