From bc39cd20f552e875c262a5060781f0d068adf2dc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <a-mikmay@microsoft.com>
Date: Fri, 27 Nov 2015 16:14:19 +0100
Subject: [PATCH] Added variable name for the case class when considering
 dependent types - There can be two options of the same type now as fields of
 the case class. Now work for Jad's example. Corrected bug when using Z3
 Corrected bug when using infinite stream not lazily.

---
 .../scala/leon/solvers/SolverFactory.scala    | 28 +++++++++++----
 .../leon/solvers/string/StringSolver.scala    |  2 +-
 .../leon/synthesis/rules/StringRender.scala   | 36 +++++++++++--------
 src/main/scala/leon/utils/StreamUtils.scala   |  4 +--
 .../solvers/StringSolverSuite.scala           |  6 ++--
 testcases/stringrender/Example-Stack.scala    | 12 +++++++
 6 files changed, 62 insertions(+), 26 deletions(-)

diff --git a/src/main/scala/leon/solvers/SolverFactory.scala b/src/main/scala/leon/solvers/SolverFactory.scala
index 99d5abc48..f59087bee 100644
--- a/src/main/scala/leon/solvers/SolverFactory.scala
+++ b/src/main/scala/leon/solvers/SolverFactory.scala
@@ -134,14 +134,30 @@ object SolverFactory {
 
   // Fast solver used by simplifications, to discharge simple tautologies
   def uninterpreted(ctx: LeonContext, program: Program): SolverFactory[TimeoutSolver] = {
-    if (hasNativeZ3) {
-      SolverFactory(() => new UninterpretedZ3Solver(ctx, program) with TimeoutSolver)
-    } else {
-      if (!reported) {
-        ctx.reporter.warning("The Z3 native interface is not available, falling back to smt-based solver.")
-        reported = true
+    val names = ctx.findOptionOrDefault(SharedOptions.optSelectedSolvers)
+    
+    if ((names contains "fairz3") && !hasNativeZ3) {
+      if (hasZ3) {
+        if (!reported) {
+          ctx.reporter.warning("The Z3 native interface is not available, falling back to smt-z3.")
+          reported = true
+        }
+        SolverFactory(() => new SMTLIBZ3Solver(ctx, program) with TimeoutSolver)
+      } else if (hasCVC4) {
+        if (!reported) {
+          ctx.reporter.warning("The Z3 native interface is not available, falling back to smt-cvc4.")
+          reported = true
+        }
+        SolverFactory(() => new SMTLIBCVC4Solver(ctx, program) with TimeoutSolver)
+      } else {
+        ctx.reporter.fatalError("No SMT solver available: native Z3 api could not load and 'cvc4' or 'z3' binaries were not found in PATH.")
       }
+    } else if(names contains "smt-cvc4") {
+      SolverFactory(() => new SMTLIBCVC4Solver(ctx, program) with TimeoutSolver)
+    } else if(names contains "smt-z3") {
       SolverFactory(() => new SMTLIBZ3Solver(ctx, program) with TimeoutSolver)
+    } else {
+      ctx.reporter.fatalError("No SMT solver available: native Z3 api could not load and 'cvc4' or 'z3' binaries were not found in PATH.")
     }
   }
 
diff --git a/src/main/scala/leon/solvers/string/StringSolver.scala b/src/main/scala/leon/solvers/string/StringSolver.scala
index b1b93568a..55ad7cf6c 100644
--- a/src/main/scala/leon/solvers/string/StringSolver.scala
+++ b/src/main/scala/leon/solvers/string/StringSolver.scala
@@ -459,7 +459,7 @@ object StringSolver {
   /** Solves the problem and returns all possible satisfying assignment */
   def solve(p: Problem): Stream[Assignment] = {
     val realProblem = forwardStrategy(p, Map())
-    /*if(realProblem.nonEmpty) {
+    /*if(realProblem.nonEmpty && realProblem.get._1.nonEmpty) {
       println("Problem:\n"+renderProblem(p))
       println("Solutions:\n"+realProblem.get._2)
       println("Real problem:\n"+renderProblem(realProblem.get._1))
diff --git a/src/main/scala/leon/synthesis/rules/StringRender.scala b/src/main/scala/leon/synthesis/rules/StringRender.scala
index 3c02166e8..1aebc53d7 100644
--- a/src/main/scala/leon/synthesis/rules/StringRender.scala
+++ b/src/main/scala/leon/synthesis/rules/StringRender.scala
@@ -145,8 +145,10 @@ case object StringRender extends Rule("StringRender") {
     }
     gatherEquations(examples.valids.collect{ case io:InOutExample => io }.toList) match {
       case Some(problem) =>
-        hctx.reporter.ifDebug(printer => printer("Problem: ["+StringSolver.renderProblem(problem)+"]"))
-        StringSolver.solve(problem)
+        hctx.reporter.debug("Problem: ["+StringSolver.renderProblem(problem)+"]")
+        val res = StringSolver.solve(problem)
+        hctx.reporter.debug("Solution found:"+res.nonEmpty)
+        res
       case None => 
         hctx.reporter.ifDebug(printer => printer("No problem found"))
         Stream.empty
@@ -188,16 +190,22 @@ case object StringRender extends Rule("StringRender") {
   
   object StringTemplateGenerator extends TypedTemplateGenerator(StringType)
   
-  case class DependentType(caseClassParent: Option[TypeTree], typeToConvert: TypeTree)
+  case class DependentType(caseClassParent: Option[TypeTree], inputName: String, typeToConvert: TypeTree)
   
   
   /** Creates an empty function definition for the dependent type */
   def createEmptyFunDef(tpe: DependentType)(implicit hctx: SearchContext): FunDef = {
+    def defaultFunName(t: TypeTree) = t match {
+      case AbstractClassType(c, d) => c.id.asString(hctx.context)
+      case CaseClassType(c, d) => c.id.asString(hctx.context)
+      case t => t.asString(hctx.context)
+    }
+    
     val funName2 = tpe.caseClassParent match {
-      case None => tpe.typeToConvert.asString(hctx.context) + "ToString" 
-      case Some(t) => tpe.typeToConvert.asString(hctx.context)+"In"+t.asString(hctx.context) + "ToString" 
+      case None => defaultFunName(tpe.typeToConvert) + "_" + tpe.inputName + "_s" 
+      case Some(t) => defaultFunName(tpe.typeToConvert) + "In"+defaultFunName(t) + "_" + tpe.inputName + "_s" 
     }
-    val funName3 = funName2.replace("]","").replace("[","")
+    val funName3 = funName2.replaceAll("[^a-zA-Z0-9_]","")
     val funName = funName3(0).toLower + funName3.substring(1) 
     val funId = FreshIdentifier(funName, alwaysShowUniqueID = true)
     val argId= FreshIdentifier(tpe.typeToConvert.asString(hctx.context).toLowerCase()(0).toString, tpe.typeToConvert)
@@ -226,12 +234,12 @@ case object StringRender extends Rule("StringRender") {
       adtToString: Map[DependentType, (FunDef, Stream[Expr])],
       inputs: Seq[Identifier])(implicit hctx: SearchContext): (Stream[Expr], Map[DependentType, (FunDef, Stream[Expr])]) = {
     
-    def extractCaseVariants(caseClassParent: TypeTree, cct: CaseClassType, assignments2: Map[DependentType, (FunDef, Stream[Expr])]) = cct match {
+    def extractCaseVariants(cct: CaseClassType, assignments2: Map[DependentType, (FunDef, Stream[Expr])]) = cct match {
       case CaseClassType(ccd@CaseClassDef(id, tparams, parent, isCaseObject), tparams2) =>
         val typeMap = tparams.zip(tparams2).toMap
         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(caseClassParent), assignments2, fields) // Invoke functions for each of the fields.
+        val (rhs, assignments2tmp2) = createFunDefsTemplates(Some(cct), assignments2, fields) // Invoke functions for each of the fields.
         val newCases = rhs.map(MatchCase(pattern, None, _))
         (assignments2tmp2, newCases)
     }
@@ -275,7 +283,7 @@ case object StringRender extends Rule("StringRender") {
         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)
+        val dependentType = DependentType(currentCaseClassParent, input.asString(hctx.program)(hctx.context), input.getType)
         assignments1.get(dependentType) match {
         case Some(fd) =>
           gatherInputs(currentCaseClassParent, assignments1, q, result += Stream(functionInvocation(fd._1, Seq(Variable(input)))))
@@ -307,7 +315,7 @@ case object StringRender extends Rule("StringRender") {
                   //TODO: Test other templates not only with Wilcard patterns, but more cases options for non-recursive classes (e.g. Option, Boolean, Finite parameterless case classes.)
                   val (assignments3, cases) = ((assignments2, ListBuffer[Stream[MatchCase]]()) /: act.knownCCDescendants) {
                     case ((assignments2, acc), cct@CaseClassType(ccd@CaseClassDef(id, tparams, parent, isCaseObject), tparams2)) =>
-                      val (assignments2tmp2, newCases) = extractCaseVariants(t, cct, assignments2)
+                      val (assignments2tmp2, newCases) = extractCaseVariants(cct, assignments2)
                       (assignments2tmp2, acc += newCases)
                     case ((adtToString, acc), e) => hctx.reporter.fatalError("Could not handle this class definition for string rendering " + e)
                   }
@@ -319,7 +327,7 @@ case object StringRender extends Rule("StringRender") {
                   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 (assignments3, newCases) = extractCaseVariants(t, cct, assignments2)
+                  val (assignments3, newCases) = extractCaseVariants(cct, assignments2)
                   val allMatchExprs = newCases.map(acase => mergeMatchCases(fd)(Seq(acase)))
                   val assignments4 = assignments3 + (dependentType -> (fd, allMatchExprs))
                   gatherInputs(currentCaseClassParent, assignments4, q, result += Stream(functionInvocation(fd, Seq(Variable(input)))))
@@ -350,7 +358,7 @@ case object StringRender extends Rule("StringRender") {
   }
   
   def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
-    hctx.reporter.debug("StringRender:Output variables="+p.xs+", their types="+p.xs.map(_.getType))
+    //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"
@@ -365,9 +373,9 @@ case object StringRender extends Rule("StringRender") {
           val (expr, funDefs) = createFunDefsTemplates(None, Map(), p.as)
           
           val toDebug: String = (("\nInferred functions:" /: funDefs)( (t, s) =>
-                t + "\n" + s.toString
+                t + "\n" + s._2._1.toString
               ))
-          hctx.reporter.ifDebug(printer => printer("Inferred expression:\n" + expr + toDebug))
+          hctx.reporter.debug("Inferred expression:\n" + expr + toDebug)
           
           findSolutions(examples, expr, funDefs.values.toSeq)
         }
diff --git a/src/main/scala/leon/utils/StreamUtils.scala b/src/main/scala/leon/utils/StreamUtils.scala
index 09a09ce40..521e98aa6 100644
--- a/src/main/scala/leon/utils/StreamUtils.scala
+++ b/src/main/scala/leon/utils/StreamUtils.scala
@@ -17,7 +17,7 @@ object StreamUtils {
       if(streams.isEmpty) Stream() else {
         val (take, leave) = streams.splitAt(diag)
         val (nonEmpty, empty) = take partition (_.nonEmpty)
-        nonEmpty.map(_.head) ++ rec(nonEmpty.map(_.tail) ++ leave, diag + 1 - empty.size)
+        nonEmpty.map(_.head) #::: rec(nonEmpty.map(_.tail) ++ leave, diag + 1 - empty.size)
       }
     }
     rec(streams, 1)
@@ -27,7 +27,7 @@ object StreamUtils {
   def interleave[T](streams : Seq[Stream[T]]) : Stream[T] = {
     if (streams.isEmpty) Stream() else {
       val nonEmpty = streams filter (_.nonEmpty)
-      nonEmpty.toStream.map(_.head) ++ interleave(nonEmpty.map(_.tail))
+      nonEmpty.toStream.map(_.head) #::: interleave(nonEmpty.map(_.tail))
     }
   }
 
diff --git a/src/test/scala/leon/integration/solvers/StringSolverSuite.scala b/src/test/scala/leon/integration/solvers/StringSolverSuite.scala
index 8d5530578..3045ea0dc 100644
--- a/src/test/scala/leon/integration/solvers/StringSolverSuite.scala
+++ b/src/test/scala/leon/integration/solvers/StringSolverSuite.scala
@@ -184,8 +184,8 @@ class StringSolverSuite extends FunSuite with Matchers {
     firstSolution(idMap("const8")) should equal("List(")
   }
   
-  /*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"""
+  test("solveJadProblem") {
+    val lhs = """const38+const34+const7+"T1"+const8+const3+const9+const5+"5"+const6+const10+const35+const30+const13+"T1"+const14+const31+const30+const7+"T2"+const8+const2+const9+const4+const10+const31+const30+const25+"T1"+const26+"Push"+const27+const20+"5"+const21+const28+const22+const29+const31+const30+const13+"T2"+const14+const31+const30+const25+"T2"+const26+"Pop"+const27+const19+const28+const23+"5"+const24+const29+const31+const33+const32+const32+const32+const32+const32+const36+const39=="T1: call Push(5)"""
     implicit val idMap = MMap[String, Identifier]()
     val lhsSf = makeSf(lhs)
     
@@ -200,5 +200,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/Example-Stack.scala b/testcases/stringrender/Example-Stack.scala
index bb9f64d1f..b01dd6f26 100644
--- a/testcases/stringrender/Example-Stack.scala
+++ b/testcases/stringrender/Example-Stack.scala
@@ -357,6 +357,18 @@ object AtomicStack {
     }
   }
   
+  def threadToStringSimple2(p: List[Event[StackTid,StackMethodName,Option[BigInt],Option[BigInt]]]): String = {
+    ???[String]
+  } ensuring {
+    res => (p, res) passes {
+      case Cons(RetEvent(T1(), Push(), Some(BigInt(5)), None()),
+           Cons(InternalEvent(T2()),
+           Cons(RetEvent(T2(), Pop(), None(), Some(BigInt(5))), Nil())))
+      =>
+     "T1: ret Push(5)\nT2: internal\nT2: ret Pop() -> 5"
+    }
+  }
+  
   
   /** This is THE method we want to render */
   def threadToString(p: List[Event[StackTid,StackMethodName,Option[BigInt],Option[BigInt]]]): String = {
-- 
GitLab