Added synthesis template for boolean.

Created the template generators.
Conversions from problems given as examples to a problem for StringSolver
Added a file for dealing with multiple input variables.

src/main/scala/leon/synthesis/Rules.scala

@@ -82,6 +82,14 @@ abstract class RuleInstantiation(val description: String,
   def asString(implicit ctx: LeonContext) = description
 }
 
+object RuleInstantiation {
+  def apply(description: String)(f: => RuleApplication)(implicit problem: Problem, rule: Rule): RuleInstantiation = {
+    new RuleInstantiation(description) {
+      def apply(hctx): RuleApplication = f
+    }
+  }
+}
+
 /**
   * Wrapper class for a function returning a recomposed solution from a list of
   * subsolutions

src/main/scala/leon/synthesis/rules/StringRender.scala

@@ -9,14 +9,49 @@ import purescala.ExprOps._
 import purescala.Extractors._
 import purescala.Constructors._
 import purescala.Types._
+import purescala.Definitions._
 import leon.utils.DebugSectionSynthesis
 import leon.purescala.Common.{Identifier, FreshIdentifier}
 import leon.purescala.Definitions.FunDef
 import leon.utils.IncrementalMap
 import leon.purescala.Definitions.FunDef
 import leon.purescala.Definitions.ValDef
+import scala.collection.mutable.ListBuffer
+import leon.purescala.ExprOps
+import leon.evaluators.Evaluator
+import leon.evaluators.DefaultEvaluator
+import leon.solvers.Model
+import leon.solvers.ModelBuilder
+import leon.solvers.string.StringSolver
 
 
+/** A template generator for a given type tree. 
+  * Extend this class using a concrete type tree,
+  * Then use the apply method to get a hole which can be a placeholder for holes in the template.
+  * Each call to the ``.instantiate` method of the subsequent Template will provide different instances at each position of the hole.
+  */
+abstract class TypedTemplateGenerator(t: TypeTree) {
+  /** Provides a hole which can be */
+  def apply(f: Expr => Expr): TemplateGenerator = {
+    val id = FreshIdentifier("ConstToInstantiate", t, true)
+    new TemplateGenerator(f(Variable(id)), id, t)
+  }
+  class TemplateGenerator(template: Expr, varId: Identifier, t: TypeTree) {
+    private val optimizationVars = ListBuffer[Identifier]()
+    private def Const: Variable = {
+      val res = FreshIdentifier("const", t, true)
+      optimizationVars += res
+      Variable(res)
+    }
+    def instantiate = {
+      ExprOps.postMap({
+        case Variable(id) if id == varId => Some(Const)
+        case _ => None
+      })(template)
+    }
+  }
+}
+
 /**
  * @author Mikael
  */
@@ -78,6 +113,51 @@ case object StringRender extends Rule("StringRender") {
         Stream.Empty
     }
   }
+  import StringSolver.{StringFormToken, StringForm, Problem => SProblem}
+  
+  /** Converts an expression to a stringForm, suitable for StringSolver */
+  def toStringForm(e: Expr, acc: List[StringFormToken] = Nil): Option[StringForm] = e match {
+    case StringLiteral(s) => Some(Left(s)::acc)
+    case Variable(id) => Some(Right(id)::acc)
+    case StringConcat(lhs, rhs) => 
+      toStringForm(rhs, acc).flatMap(toStringForm(lhs, _))
+    case _ => None
+  }
+  
+  /** Returns the string associated to the expression if it is computable */
+  def toStringLiteral(e: Expr): Option[String] = e match {
+    case StringLiteral(s) => Some(s)
+    case StringConcat(lhs, rhs) => toStringLiteral(lhs).flatMap(k => toStringLiteral(rhs).map(l => k + l))
+    case _ => None
+  }
+  
+  /** Returns a stream of assignments compatible with input/output examples */
+  def findAssignments(ctx: LeonContext, p: Program, inputs: Seq[Identifier], examples: ExamplesBank, template: Expr): Stream[Map[Identifier, String]] = {
+    //new Evaluator()
+    val e = new DefaultEvaluator(ctx, p)
+    
+    var invalid = false
+    val equations: SProblem = for{
+      (in, rhsExpr) <- examples.valids.collect{ case InOutExample(in, out) => (in, out) }.toList
+      if !invalid || rhsExpr.length != 1
+      model = new ModelBuilder 
+  _ = model ++= inputs.zip(in)
+      result = e.eval(template, model.result()).result
+  _ = invalid ||= result.isEmpty
+      if !invalid
+      sf = toStringForm(result.get)
+      rhs = toStringLiteral(rhsExpr.head)
+  _ = invalid ||= sf.isEmpty || rhs.isEmpty
+      if !invalid
+    } yield {
+      (sf.get, rhs.get)
+    }
+    if(!invalid) {
+      StringSolver.solve(equations)
+    } else {
+      Stream.empty
+    }
+  }
   
   def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
     p.xs match {
@@ -89,7 +169,7 @@ case object StringRender extends Rule("StringRender") {
         val examplesFinder = new ExamplesFinder(hctx.context, hctx.program)
         val examples = examplesFinder.extractFromProblem(p)
         
-        /** Possible strategies.
+        /*  Possible strategies.
           * If data structure is recursive on at least one variable (see how Induction works)
           * then
           *   - Inserts a new rec function deconstructing it and put it into the available preconditions to use.
@@ -104,26 +184,38 @@ case object StringRender extends Rule("StringRender") {
           * If there are multiple solutions, we generate one deeper example and ask the user which one should be better.
           */
         
-        /* All input variables which are inductive in the post condition, along with their abstract data type. */
-
         
+        
+        object StringTemplateGenerator extends TypedTemplateGenerator(StringType)
+        val booleanTemplate = (a: Identifier) => StringTemplateGenerator(Hole => IfExpr(Variable(a), Hole, Hole))
+        
+        /* All input variables which are inductive in the post condition, along with their abstract data type. */
         p.as match {
-          case List(IsTyped(a, WithStringconverter(converter))) => // Standard conversions if they work.
-
-            List(new RuleInstantiation(description) { // TODO: Use a VSA to ask questions.
-              def apply(hctx: SearchContext): RuleApplication = {
-                // TODO: Test if the straightforward solution works ! This is wrong for now.
-                RuleClosed(Solution(pre=p.pc, defs=Set(), term=converter(Variable(a))))
+          case List(IsTyped(a, tpe@WithStringconverter(converter))) => // Standard conversions if they work.
+            
+            val ruleInstantiations = ListBuffer[RuleInstantiation]()
+            if(tpe == BooleanType) {
+              ruleInstantiations += RuleInstantiation("Boolean split render") {
+                val template = booleanTemplate(a).instantiate
+                val solutions = findAssignments(hctx.context, hctx.program, p.as, examples, template)
+                if(solutions.isEmpty) RuleFailed() else {
+                  RuleClosed(solutions.map((assignment: Map[Identifier, String]) => {
+                    Solution(pre=p.pc, defs=Set(), term=ExprOps.replaceFromIDs(assignment.mapValues(StringLiteral), template))
+                  }))
+                }
               }
-            })
-          /*case List(IsTyped(a, tpe)) =>
-            List(new RuleInstantiation(description) {
-              def apply(hctx: SearchContext): RuleApplication = {
-                val examplesFinder = new ExamplesFinder(hctx.context, hctx.program)
-                val examples = examplesFinder.extractFromProblem(p)
-                RuleFailed()
+            }
+            
+            ruleInstantiations += RuleInstantiation("String conversion with pre and post") {
+                val template = StringTemplateGenerator(Hole => StringConcat(StringConcat(Hole, converter(Variable(a))), Hole)).instantiate
+                val solutions = findAssignments(hctx.context, hctx.program, p.as, examples, template)
+                if(solutions.isEmpty) RuleFailed() else {
+                  RuleClosed(solutions.map((assignment: Map[Identifier, String]) => {
+                    Solution(pre=p.pc, defs=Set(), term=ExprOps.replaceFromIDs(assignment.mapValues(StringLiteral), template))
+                  }))
+                }
               }
-            })*/
+            ruleInstantiations.toList
           case _ =>
             Nil
         }

testcases/stringrender/TupleWrapperRender.scala

@@ -6,7 +6,6 @@
   */
 
 import leon.lang._
-import string.String
 import leon.annotation._
 import leon.collection._
 import leon.collection.ListOps._
@@ -15,49 +14,49 @@ import leon.lang.synthesis._
 object TupleWrapperRender {
   case class TupleWrapper(i: Int, j: Int)
 
-  def psStandard(s: TupleWrapper)(res: String) = (s, res) passes {
+  def psStandard(s: TupleWrapper) = (res: String) => (s, res) passes {
     case TupleWrapper(0, 0) => "TupleWrapper(0, 0)"
     case TupleWrapper(-1, 2) => "TupleWrapper(-1, 2)"
     case TupleWrapper(12, 5) => "TupleWrapper(12, 5)"
   }
   
-  def psUnwrapped(s: TupleWrapper)(res: String) = (s, res) passes {
+  def psUnwrapped(s: TupleWrapper) = (res: String) => (s, res) passes {
     case TupleWrapper(0, 0) => "0, 0"
     case TupleWrapper(-1, 2) => "-1, 2"
-    case TupleWrapper(12, 5) => "(12, 5)"
+    case TupleWrapper(12, 5) => "12, 5"
   }
   
-  def psNameChangedPrefix(s: TupleWrapper)(res: String) = (s, res) passes {
+  def psNameChangedPrefix(s: TupleWrapper) = (res: String) => (s, res) passes {
     case TupleWrapper(0, 0) => "x = 0, y = 0"
     case TupleWrapper(-1, 2) => "x = -1, y = 2"
     case TupleWrapper(12, 5) => "x = 12, y = 5"
   }
   
-  def psNameChangedSuffix(s: TupleWrapper)(res: String) = (s, res) passes {
+  def psNameChangedSuffix(s: TupleWrapper) = (res: String) => (s, res) passes {
     case TupleWrapper(0, 0) => "0.0,0.0"
     case TupleWrapper(-1, 2) => "-1.0,2.0" // Here there should be an ambiguity before this line.
     case TupleWrapper(12, 5) => "12.0,5.0"
   }
   
-  def psDuplicate(s: TupleWrapper)(res: String) = (s, res) passes {
+  def psDuplicate(s: TupleWrapper) = (res: String) => (s, res) passes {
     case TupleWrapper(0, 0) => "d 0,0 0,15 15,15 15,0"
     case TupleWrapper(-1, 2) => "d -1,-2 -1,15 15,15 15,2"
     case TupleWrapper(12, 5) => "d 12,5 12,15 15,15 15,5"
   }
   
-  def repairUnWrapped(s: IntWrapper): String = {
+  def repairUnWrapped(s: TupleWrapper): String = {
     "TupleWrapper(" + s.i + ", " + s.j + ")""
   } ensuring psUnWrapped(s)
   
-  def repairNameChangedPrefix(s: IntWrapper): String = {
+  def repairNameChangedPrefix(s: TupleWrapper): String = {
     "TupleWrapper(" + s.i + ", " + s.j + ")""
   } ensuring psNameChangedPrefix(s)
   
-  def repairNameChangedSuffix(s: IntWrapper): String = {
+  def repairNameChangedSuffix(s: TupleWrapper): String = {
     "TupleWrapper(" + s.i + ", " + s.j + ")""
   } ensuring psNameChangedSuffix(s)
   
-  def repairDuplicate(s: IntWrapper): String = {
+  def repairDuplicate(s: TupleWrapper): String = {
     "TupleWrapper(" + s.i + ", " + s.j + ")""
   } ensuring psDuplicate(s)
   

testcases/stringrender/TwoArgsWrapperRender.scala

+/**
+  * Name:     TupleWrapperRender.scala
+  * Creation: 15.10.2015
+  * Author:   Mikaël Mayer (mikael.mayer@epfl.ch)
+  * Comments: Tuple rendering specifications.
+  */
+
+import leon.annotation._
+import leon.collection._
+import leon.collection.ListOps._
+import leon.lang.synthesis._
+
+object TwoArgsWrapperRender {
+  def psStandard(s: Int, t: Int) = (res: String) => ((s, t), res) passes {
+    case (0, 0) => "TupleWrapper(0, 0)"
+    case (-1, 2) => "TupleWrapper(-1, 2)"
+    case (12, 5) => "TupleWrapper(12, 5)"
+  }
+  
+  def psUnwrapped(s: Int, t: Int) = (res: String) => ((s, t), res) passes {
+    case (0, 0) => "0, 0"
+    case (-1, 2) => "-1, 2"
+    case (12, 5) => "12, 5"
+  }
+  
+  def psNameChangedPrefix(s: Int, t: Int) = (res: String) => ((s, t), res) passes {
+    case (0, 0) => "x = 0, y = 0"
+    case (-1, 2) => "x = -1, y = 2"
+    case (12, 5) => "x = 12, y = 5"
+  }
+  
+  def psNameChangedSuffix(s: Int, t: Int) = (res: String) => ((s, t), res) passes {
+    case (0, 0) => "0.0,0.0"
+    case (-1, 2) => "-1.0,2.0" // Here there should be an ambiguity before this line.
+    case (12, 5) => "12.0,5.0"
+  }
+  
+  def psDuplicate(s: Int, t: Int) = (res: String) => ((s, t), res) passes {
+    case (0, 0) => "d 0,0 0,15 15,15 15,0"
+    case (-1, 2) => "d -1,-2 -1,15 15,15 15,2"
+    case (12, 5) => "d 12,5 12,15 15,15 15,5"
+  }
+  
+  def repairUnWrapped(s: Int, t: Int): String = {
+    "(" + s + ", " + t + ")""
+  } ensuring psUnWrapped(s)
+  
+  def repairNameChangedPrefix(s: Int, t: Int): String = {
+    "(" + s + ", " + t + ")""
+  } ensuring psNameChangedPrefix(s)
+  
+  def repairNameChangedSuffix(s: Int, t: Int): String = {
+    "(" + s + ", " + t + ")""
+  } ensuring psNameChangedSuffix(s)
+  
+  def repairDuplicate(s: Int, t: Int): String = {
+    "(" + s + ", " + t + ")""
+  } ensuring psDuplicate(s)
+  
+  
+  def synthesisStandard(s: Int, t: Int): String = {
+     ???[String]
+  } ensuring psStandard(s)
+  
+  def synthesisUnwrapped(s: Int, t: Int): String = {
+     ???[String]
+  } ensuring psUnwrapped(s)
+  
+  def synthesisNameChangedPrefix(s: Int, t: Int): String = {
+     ???[String]
+  } ensuring psNameChangedPrefix(s)
+  
+  def synthesisNameChangedSuffix(s: Int, t: Int): String = {
+     ???[String]
+  } ensuring psNameChangedSuffix(s)
+  
+  def synthesisDuplicate(s: Int, t: Int): String = {
+     ???[String]
+  } ensuring psDuplicate(s)
+}
\ No newline at end of file

testcases/stringrender/runRepair.sh

@@ -25,6 +25,11 @@ echo "#           Category,                 File,             function, p.S, fuS
 ./leon --repair --timeout=30 --solvers=smt-cvc4 --functions=repairNameChangedSuffix  testcases/stringrender/IntWrapperRender.scala     | tee -a $fullLog
 ./leon --repair --timeout=30 --solvers=smt-cvc4 --functions=repairDuplicate          testcases/stringrender/IntWrapperRender.scala     | tee -a $fullLog
 
+./leon --repair --timeout=30 --solvers=smt-cvc4 --functions=repairUnwrapped          testcases/stringrender/TwoArgsWrapperRender.scala   | tee -a $fullLog
+./leon --repair --timeout=30 --solvers=smt-cvc4 --functions=repairNameChangedPrefix  testcases/stringrender/TwoArgsWrapperRender.scala   | tee -a $fullLog
+./leon --repair --timeout=30 --solvers=smt-cvc4 --functions=repairNameChangedSuffix  testcases/stringrender/TwoArgsWrapperRender.scala   | tee -a $fullLog
+./leon --repair --timeout=30 --solvers=smt-cvc4 --functions=repairDuplicate          testcases/stringrender/TwoArgsWrapperRender.scala   | tee -a $fullLog
+
 ./leon --repair --timeout=30 --solvers=smt-cvc4 --functions=repairUnwrapped          testcases/stringrender/TupleWrapperRender.scala   | tee -a $fullLog
 ./leon --repair --timeout=30 --solvers=smt-cvc4 --functions=repairNameChangedPrefix  testcases/stringrender/TupleWrapperRender.scala   | tee -a $fullLog
 ./leon --repair --timeout=30 --solvers=smt-cvc4 --functions=repairNameChangedSuffix  testcases/stringrender/TupleWrapperRender.scala   | tee -a $fullLog