From 92493830c0c3c0991a1538329bf66bf3d66ca821 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <a-mikmay@microsoft.com>
Date: Thu, 19 Nov 2015 17:36:31 +0100
Subject: [PATCH] Converted foldLefts and for comprehensions to tailrec
methods, better suited for the task
---
.../leon/solvers/string/StringSolver.scala | 104 +++++++++---------
.../leon/synthesis/rules/StringRender.scala | 45 ++++----
2 files changed, 75 insertions(+), 74 deletions(-)
diff --git a/src/main/scala/leon/solvers/string/StringSolver.scala b/src/main/scala/leon/solvers/string/StringSolver.scala
index 1276a6813..b953b8cb1 100644
--- a/src/main/scala/leon/solvers/string/StringSolver.scala
+++ b/src/main/scala/leon/solvers/string/StringSolver.scala
@@ -8,6 +8,7 @@ import leon.utils.Interruptible
import leon.LeonContext
import scala.collection.mutable.ListBuffer
import vanuatoo.Pattern
+import scala.annotation.tailrec
/**
* @author Mikael
@@ -25,14 +26,14 @@ object StringSolver {
type Problem = List[Equation]
/** Evaluates a String form. Requires the solution to have an assignment to all identifiers. */
- def evaluate(s: Assignment, acc: StringBuffer = new StringBuffer(""))(sf: StringForm): String = sf match {
+ @tailrec def evaluate(s: Assignment, acc: StringBuffer = new StringBuffer(""))(sf: StringForm): String = sf match {
case Nil => acc.toString
case Left(constant)::q => evaluate(s, acc append constant)(q)
case Right(identifier)::q => evaluate(s, acc append s(identifier))(q)
}
/** Assigns the new values to the equations and simplify them at the same time. */
- def reduceStringForm(s: Assignment, acc: ListBuffer[StringFormToken] = ListBuffer())(sf: StringForm): StringForm = sf match {
+ @tailrec def reduceStringForm(s: Assignment, acc: ListBuffer[StringFormToken] = ListBuffer())(sf: StringForm): StringForm = sf match {
case Nil => acc.toList
case (l@Left(constant))::(l2@Left(constant2))::q => reduceStringForm(s, acc)(Left(constant + constant2)::q)
case (l@Left(constant))::(r2@Right(id))::q =>
@@ -65,57 +66,57 @@ object StringSolver {
/** Concatenates constants together */
def reduceStringForm(s: StringForm): StringForm = {
- def rec(s: StringForm, acc: StringForm): StringForm = s match {
- case Nil => acc
+ @tailrec def rec(s: StringForm, acc: ListBuffer[StringFormToken] = ListBuffer()): StringForm = s match {
+ case Nil => acc.toList
case Left(c)::Left(d)::q => rec(Left(c+d)::q, acc)
- case a::q => rec(q, a::acc)
+ case a::q => rec(q, acc += a)
}
- rec(s, Nil).reverse
+ rec(s)
}
/** returns a simplified version of the problem. If it is not satisfiable, returns None. */
- def simplifyProblem(p: Problem, s: Assignment): Option[(Problem, Assignment)] = {
+ @tailrec def simplifyProblem(p: Problem, s: Assignment): Option[(Problem, Assignment)] = {
// Invariant: Every assigned var does not appear in the problem.
-
// 1. Merge constant in string forms
- val constantMerge: Option[Problem] = ((Option(List[Equation]()) /: p){
- case (None, eq) => None
- case (Some(building_problem), (sf, rhs)) => Some((reduceStringForm(sf), rhs)::building_problem)
- }).map(_.reverse)
-
- if(constantMerge == None) return None
+ @tailrec def mergeConstants(p: Problem, acc: ListBuffer[Equation] = ListBuffer()): Option[Problem] = p match {
+ case Nil => Some(acc.toList)
+ case (sf, rhs)::q => mergeConstants(q, acc += ((reduceStringForm(sf), rhs)))
+ }
// 2. Unsat if Const1 = Const2 but constants are different.
// 2bis. if Const1 = Const2 and constants are same, remove equality.
- val simplified = (((Some(Nil): Option[Problem]) /: constantMerge.get){
- case (None, eq) => None
- case (Some(building_problem), (Nil, rhs)) => if("" != rhs) None else Some(building_problem)
- case (Some(building_problem), (List(Left(c)), rhs)) => if(c != rhs) None else Some(building_problem)
- case (Some(building_problem), sentence) => Some(sentence::building_problem)
- }).map(_.reverse)
-
- if(simplified == None) return None
+ @tailrec def simplifyConstants(p: Problem, acc: ListBuffer[Equation] = ListBuffer()): Option[Problem] = p match {
+ case Nil => Some(acc.toList)
+ case (Nil, rhs)::q => if("" != rhs) None else simplifyConstants(q, acc)
+ case (List(Left(c)), rhs)::q => if(c != rhs) None else simplifyConstants(q, acc)
+ case sentence::q => simplifyConstants(q, acc += sentence)
+ }
// 3. Get new assignments from equations such as id = Const.
- val newAssignments = (Option(Map[Identifier, String]()) /: p){
- case (None, _) => None
- case (Some(assignments), (List(Right(id)), rhs)) =>
+ @tailrec def obtainAssignments(p: Problem, assignments: Assignment = Map()): Option[Assignment] = p match {
+ case Nil => Some(assignments)
+ case (List(Right(id)), rhs)::q =>
assignments.get(id) match { // It was assigned already.
case Some(v) =>
- if(rhs != v) None else Some(assignments)
- case _ =>
- Some(assignments + (id -> rhs))
+ if(rhs != v) None else obtainAssignments(q, assignments)
+ case None =>
+ obtainAssignments(q, assignments + (id -> rhs))
}
- case (s@Some(assignments), sentence) => s
+ case sentence::q => obtainAssignments(q, assignments)
}
+ val simplifiedOpt = mergeConstants(p)
+ .flatMap(simplifyConstants(_))
- if(newAssignments == None) return None
-
- // 4. If there are new assignments, forward them to the equation and relaunch the simplification.
- if(newAssignments.get.nonEmpty)
- simplifyProblem(reduceProblem(newAssignments.get)(simplified.get), s ++ newAssignments.get)
- else { // No new assignments, simplification over.
- Option((simplified.get, s))
+ simplifiedOpt match {
+ case None => None
+ case Some(simplified) =>
+ // 4. If there are new assignments, forward them to the equation and relaunch the simplification.
+ val newAssignmentsOpt = obtainAssignments(simplified)
+ newAssignmentsOpt match {
+ case Some(newAssignments) if newAssignments.nonEmpty =>
+ simplifyProblem(reduceProblem(newAssignments)(simplified), s ++ newAssignments)
+ case _ => Some((simplified, s))
+ }
}
}
@@ -128,28 +129,27 @@ object StringSolver {
// Removes all constants from the left and right of the equations
def noLeftRightConstants(p: Problem): Option[Problem] = {
- val noLeftConstants: Option[Problem] = ((Option(List[Equation]()) /: p){
- case (None, eq) => None
- case (Some(building_problem), (Left(constant)::q, rhs)) =>
+ @tailrec def removeLeftconstants(p: Problem, acc: ListBuffer[Equation] = ListBuffer()): Option[Problem] = p match {
+ case Nil => Some(acc.toList)
+ case ((Left(constant)::q, rhs))::ps =>
if(rhs.startsWith(constant)) {
- Some((q, rhs.substring(constant.length))::building_problem)
+ removeLeftconstants(ps, acc += ((q, rhs.substring(constant.length))))
} else None
- case (Some(building_problem), (q, rhs)) =>
- Some((q, rhs)::building_problem)
- }).map(_.reverse)
- if(noLeftConstants == None) return None
+ case (t@(q, rhs))::ps =>
+ removeLeftconstants(ps, acc += t)
+ }
- val noRightConstants: Option[Problem] = ((Option(List[Equation]()) /: noLeftConstants.get){
- case (None, eq) => None
- case (Some(building_problem), (ConsReverse(q, Left(constant)), rhs)) =>
+ @tailrec def removeRightConstants(p: Problem, acc: ListBuffer[Equation] = ListBuffer()): Option[Problem] = p match {
+ case Nil => Some(acc.toList)
+ case (ConsReverse(q, Left(constant)), rhs)::ps =>
if(rhs.endsWith(constant)) {
- Some((q, rhs.substring(0, rhs.length - constant.length))::building_problem)
+ removeRightConstants(ps, acc += ((q, rhs.substring(0, rhs.length - constant.length))))
} else None
- case (Some(building_problem), (q, rhs)) =>
- Some((q, rhs)::building_problem)
- }).map(_.reverse)
+ case (t@(q, rhs))::ps =>
+ removeRightConstants(ps, acc += t)
+ }
- noRightConstants
+ removeLeftconstants(p).flatMap(removeRightConstants(_))
}
/** Composition of simplifyProble and noLeftRightConstants */
diff --git a/src/main/scala/leon/synthesis/rules/StringRender.scala b/src/main/scala/leon/synthesis/rules/StringRender.scala
index d2cfd2060..f32546a02 100644
--- a/src/main/scala/leon/synthesis/rules/StringRender.scala
+++ b/src/main/scala/leon/synthesis/rules/StringRender.scala
@@ -23,6 +23,7 @@ import leon.evaluators.DefaultEvaluator
import leon.solvers.Model
import leon.solvers.ModelBuilder
import leon.solvers.string.StringSolver
+import scala.annotation.tailrec
/** A template generator for a given type tree.
@@ -113,7 +114,7 @@ case object StringRender extends Rule("StringRender") {
Stream.Empty
}
}
- import StringSolver.{StringFormToken, StringForm, Problem => SProblem}
+ import StringSolver.{StringFormToken, StringForm, Problem => SProblem, Equation}
/** Converts an expression to a stringForm, suitable for StringSolver */
def toStringForm(e: Expr, acc: List[StringFormToken] = Nil): Option[StringForm] = e match {
@@ -137,25 +138,26 @@ case object StringRender extends Rule("StringRender") {
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)
+
+ @tailrec def gatherEquations(s: List[InOutExample], acc: ListBuffer[Equation] = ListBuffer()): Option[SProblem] = s match {
+ case Nil => Some(acc.toList)
+ case InOutExample(in, rhExpr)::q =>
+ if(rhExpr.length == 1) {
+ val model = new ModelBuilder
+ model ++= inputs.zip(in)
+ e.eval(template, model.result()).result match {
+ case None => None
+ case Some(sfExpr) =>
+ val sf = toStringForm(sfExpr)
+ val rhs = toStringLiteral(rhExpr.head)
+ if(sf.isEmpty || rhs.isEmpty) None
+ else gatherEquations(q, acc += ((sf.get, rhs.get)))
+ }
+ } else None
}
- if(!invalid) {
- StringSolver.solve(equations)
- } else {
- Stream.empty
+ gatherEquations(examples.valids.collect{ case io:InOutExample => io }.toList) match {
+ case Some(problem) => StringSolver.solve(problem)
+ case None => Stream.empty
}
}
@@ -176,7 +178,8 @@ case object StringRender extends Rule("StringRender") {
* If the input is constant
* - just a variable to compute a constant.
* If there are several variables
- * - All possible ways of linearly unbuilding the structure
+ * - All possible ways of linearly unbuilding the structure.
+ * - Or maybe try to infer top-bottom the order of variables from examples?
* if a variable is a primitive
* - Introduce an ordered string containing the content.
*
@@ -184,8 +187,6 @@ 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.
*/
-
-
object StringTemplateGenerator extends TypedTemplateGenerator(StringType)
val booleanTemplate = (a: Identifier) => StringTemplateGenerator(Hole => IfExpr(Variable(a), Hole, Hole))
--
GitLab