diff --git a/src/main/scala/leon/synthesis/rules/StringRender.scala b/src/main/scala/leon/synthesis/rules/StringRender.scala
index 3416a9851adf79d88771cb838a96f564894bcccf..4153edee5650342eb75d38d656e5f0c96ae86602 100644
--- a/src/main/scala/leon/synthesis/rules/StringRender.scala
+++ b/src/main/scala/leon/synthesis/rules/StringRender.scala
@@ -151,7 +151,7 @@ case object StringRender extends Rule("StringRender") {
None
}
}
- gatherEquations(examples.valids.collect{ case io:InOutExample => io }.toList) match {
+ gatherEquations((examples.valids ++ examples.invalids).collect{ case io:InOutExample => io }.toList) match {
case Some(problem) =>
hctx.reporter.debug("Problem: ["+StringSolver.renderProblem(problem)+"]")
val res = StringSolver.solve(problem)
@@ -279,21 +279,21 @@ case object StringRender extends Rule("StringRender") {
(assignments2tmp2, newCases)
}
- /** Returns a constant pattern matching in which all classes are rendered using their proper name
- * For example:
- * {{{
- * sealed abstract class Thread
- * case class T1() extends Thread()
- * case Class T2() extends Thread()
- * }}}
- * Will yield the following expression:
- * {{{t match {
- * case T1() => "T1"
- * case T2() => "T2"
- * }
- * }}}
- *
- * */
+ /* Returns a constant pattern matching in which all classes are rendered using their proper name
+ * For example:
+ * {{{
+ * sealed abstract class Thread
+ * case class T1() extends Thread()
+ * case Class T2() extends Thread()
+ * }}}
+ * Will yield the following expression:
+ * {{{t match {
+ * case T1() => "T1"
+ * case T2() => "T2"
+ * }
+ * }}}
+ *
+ */
def constantPatternMatching(fd: FunDef, act: AbstractClassType): WithIds[MatchExpr] = {
val cases = (ListBuffer[WithIds[MatchCase]]() /: act.knownCCDescendants) {
case (acc, cct@CaseClassType(ccd@CaseClassDef(id, tparams, parent, isCaseObject), tparams2)) =>
@@ -372,8 +372,7 @@ case object StringRender extends Rule("StringRender") {
}
}
val (exprs, assignments) = gatherInputs(currentCaseClassParent, adtToString, inputs.toList)
- /** Add post, pre and in-between holes, and returns a single expr along with the new assignments. */
-
+ /* Add post, pre and in-between holes, and returns a single expr along with the new assignments. */
val template: Stream[WithIds[Expr]] = exprs match {
case Nil =>
Stream(StringTemplateGenerator(Hole => Hole).instantiateWithVars)
diff --git a/src/main/scala/leon/verification/VerificationReport.scala b/src/main/scala/leon/verification/VerificationReport.scala
index cffc4bae21bcd5267850fb0676d1c0b5eedb32c6..50f8f6f8b08f59080941fcb34b0a49e152206cbe 100644
--- a/src/main/scala/leon/verification/VerificationReport.scala
+++ b/src/main/scala/leon/verification/VerificationReport.scala
@@ -28,12 +28,17 @@ object VerificationReport {
def userDefinedString(v: Expr, orElse: =>String)(ctx: LeonContext, program: Program): String = {
//println("Functions available:" + program.definedFunctions.map(fd => fd.id.name + "," + (fd.returnType == StringType) + ", " + (fd.params.length == 1) + "," + (fd.params.length == 1 && TypeOps.isSubtypeOf(v.getType, fd.params.head.getType)) + ", " + (if(fd.params.length == 1) fd.params.head.getType + " == " + v.getType else "")).mkString("\n"))
(program.definedFunctions find {
- case fd => fd.returnType == StringType && fd.params.length == 1 && TypeOps.isSubtypeOf(v.getType, fd.params.head.getType) && fd.id.name.toLowerCase().endsWith("tostring")
+ case fd =>
+ fd.returnType == StringType && fd.params.length == 1 && TypeOps.isSubtypeOf(v.getType, fd.params.head.getType) && fd.id.name.toLowerCase().endsWith("tostring") &&
+ program.callGraph.transitiveCallees(fd).forall { fde =>
+ !purescala.ExprOps.exists( _.isInstanceOf[Choose])(fde.fullBody)
+ }
}) match {
case Some(fd) =>
//println("Found fd: " + fd.id.name)
val ste = new StringTracingEvaluator(ctx, program)
try {
+ println("Function to test: " + fd)
val result = ste.eval(FunctionInvocation(fd.typed, Seq(v)))
result.result match {
diff --git a/testcases/stringrender/GrammarRender.scala b/testcases/stringrender/GrammarRender.scala
index fefe85e94c153c0ba638200f444902936bebf601..59928dceb1bc7ba620b7f84dbdddecf59f7b83f3 100644
--- a/testcases/stringrender/GrammarRender.scala
+++ b/testcases/stringrender/GrammarRender.scala
@@ -6,13 +6,12 @@
*/
import leon.lang._
-import string.String
import leon.annotation._
import leon.collection._
import leon.collection.ListOps._
import leon.lang.synthesis._
-object Gra��arRender {
+object GrammarRender {
abstract class Symbol
case class Terminal(i: Int) extends Symbol
case class NonTerminal(i: Int) extends Symbol
@@ -21,7 +20,7 @@ object Gra��arRender {
case class Grammar(start: Symbol, rules: List[Rule])
/** Synthesis by example specs */
- @inline def psStandard(s: Grammar)(res: String) = (s, res) passes {
+ @inline def psStandard(s: Grammar) = (res: String) => (s, res) passes {
case Grammar(NonTerminal(0), Nil()) => "Grammar(NonTerminal(0), Nil())"
case Grammar(NonTerminal(0), Cons(Rule(NonTerminal(0), Cons(Terminal(1), Nil())), Nil())) =>
"Grammar(NonTerminal(0), Cons(Rule(NonTerminal(0), Cons(Terminal(1), Nil())), Nil()))"
@@ -29,58 +28,58 @@ object Gra��arRender {
"Grammar(NonTerminal(0), Cons(Rule(NonTerminal(0), Cons(Terminal(1), Nil())), Cons(Rule(NonTerminal(0), Cons(NonTerminal(0), Cons(Terminal(1), Nil()))), Nil())))"
}
- @inline def psRemoveNames(s: Grammar)(res: String) = (s, res) passes {
+ @inline def psRemoveNames(s: Grammar) = (res: String) => (s, res) passes {
case Grammar(NonTerminal(0), Nil()) => "(S0, ())"
- case Grammar(NonTerminal(0), Cons(Rule(NonTerminal(0), Cons(Terminal(1), Nil())), Nil)) =>
+ case Grammar(NonTerminal(0), Cons(Rule(NonTerminal(0), Cons(Terminal(1), Nil())), Nil())) =>
"(S0, ((S0, (t1, ())), ()))"
case Grammar(NonTerminal(0), Cons(Rule(NonTerminal(0), Cons(Terminal(1), Nil())), Cons(Rule(NonTerminal(0), Cons(NonTerminal(0), Cons(Terminal(1), Nil()))), Nil()))) =>
"(S0, ((S0, (t1, ())), ((S0, (S0, (t1, ()))), ())))"
}
- @inline def psArrowRules(s: Grammar)(res: String) = (s, res) passes {
+ @inline def psArrowRules(s: Grammar) = (res: String) => (s, res) passes {
case Grammar(NonTerminal(0), Nil()) => "(S0, ())"
- case Grammar(NonTerminal(0), Cons(Rule(NonTerminal(0), Cons(Terminal(1), Nil())), Nil)) =>
+ case Grammar(NonTerminal(0), Cons(Rule(NonTerminal(0), Cons(Terminal(1), Nil())), Nil())) =>
"(S0, ((S0 -> (t1, ())), ()))"
case Grammar(NonTerminal(0), Cons(Rule(NonTerminal(0), Cons(Terminal(1), Nil())), Cons(Rule(NonTerminal(0), Cons(NonTerminal(0), Cons(Terminal(1), Nil()))), Nil()))) =>
"(S0, ((S0 -> (t1, ())), ((S0 -> (S0, (t1, ()))), ())))"
}
- @inline def psListRules(s: Grammar)(res: String) = (s, res) passes {
+ @inline def psListRules(s: Grammar) = (res: String) => (s, res) passes {
case Grammar(NonTerminal(0), Nil()) => "(S0, [])"
- case Grammar(NonTerminal(0), Cons(Rule(NonTerminal(0), Cons(Terminal(1), Nil())), Nil)) =>
+ case Grammar(NonTerminal(0), Cons(Rule(NonTerminal(0), Cons(Terminal(1), Nil())), Nil())) =>
"(S0, [S0 -> [t1]])"
case Grammar(NonTerminal(0), Cons(Rule(NonTerminal(0), Cons(Terminal(1), Nil())), Cons(Rule(NonTerminal(0), Cons(NonTerminal(0), Cons(Terminal(1), Nil()))), Nil()))) =>
"(S0, [S0 -> [t1], S0 -> [S0, t1])"
}
// The difficulty here is that two lists have to be rendered differently.
- @inline def psSpaceRules(s: Grammar)(res: String) = (s, res) passes {
+ @inline def psSpaceRules(s: Grammar) = (res: String) => (s, res) passes {
case Grammar(NonTerminal(0), Nil()) => "(S0, [])"
- case Grammar(NonTerminal(0), Cons(Rule(NonTerminal(0), Cons(Terminal(1), Nil())), Nil)) =>
+ case Grammar(NonTerminal(0), Cons(Rule(NonTerminal(0), Cons(Terminal(1), Nil())), Nil())) =>
"(S0, [S0 -> t1])"
case Grammar(NonTerminal(0), Cons(Rule(NonTerminal(0), Cons(Terminal(1), Nil())), Cons(Rule(NonTerminal(0), Cons(NonTerminal(0), Cons(Terminal(1), Nil()))), Nil()))) =>
"(S0, [S0 -> t1, S0 -> S0 t1)"
}
// Full HTML generation
- @inline def psHTMLRules(s: Grammar)(res: String) = (s, res) passes {
+ @inline def psHTMLRules(s: Grammar) = (res: String) => (s, res) passes {
case Grammar(NonTerminal(0), Nil()) => "<b>Start:</b> S0<br><pre></pre>"
- case Grammar(NonTerminal(0), Cons(Rule(NonTerminal(0), Cons(Terminal(1), Nil())), Nil)) =>
+ case Grammar(NonTerminal(0), Cons(Rule(NonTerminal(0), Cons(Terminal(1), Nil())), Nil())) =>
"<b>Start:</b> S0<br><pre>S0 -> t1</pte>"
case Grammar(NonTerminal(0), Cons(Rule(NonTerminal(0), Cons(Terminal(1), Nil())), Cons(Rule(NonTerminal(0), Cons(NonTerminal(0), Cons(Terminal(1), Nil()))), Nil()))) =>
"<b>Start:</b> S0<br><pre>S0 -> t1<br>S0 -> S0 t1</pte>"
}
- // Full HTML generation
- @inline def psPlainTextRules(s: Grammar)(res: String) = (s, res) passes {
+ //Render in plain text.
+ @inline def psPlainTextRules(s: Grammar) = (res: String) => (s, res) passes {
case Grammar(NonTerminal(0), Nil()) =>
"""Start:S0"""
- case Grammar(NonTerminal(0), Cons(Rule(NonTerminal(0), Cons(Terminal(1), Nil())), Nil)) =>
+ case Grammar(NonTerminal(0), Cons(Rule(NonTerminal(0), Cons(Terminal(1), Nil())), Nil())) =>
"""Start:S0
- |S0 -> t1""".stripMargin
+S0 -> t1"""
case Grammar(NonTerminal(0), Cons(Rule(NonTerminal(0), Cons(Terminal(1), Nil())), Cons(Rule(NonTerminal(0), Cons(NonTerminal(0), Cons(Terminal(1), Nil()))), Nil()))) =>
"""Start:S0
- |S0 -> t1
- |S0 -> S0 t1""".stripMargin
+S0 -> t1
+S0 -> S0 t1"""
}
/** Each function's body is the solution of the previous problem.
@@ -150,7 +149,7 @@ object Gra��arRender {
def renderRule(r: Rule): String = {
def renderListSymbol(s: List[Symbol]): String = s match {
case Nil() => ""
- case Cons(a, Nil) => rendersymbol(a)
+ case Cons(a, Nil()) => rendersymbol(a)
case Cons(a, q) => rendersymbol(a) + ", " + renderListsymbol(q)
}
renderSymbol(r.left) + " -> [" + renderListSymbol(r.right) + "]"
@@ -171,7 +170,7 @@ object Gra��arRender {
def renderRule(r: Rule): String = {
def renderListSymbol(s: List[Symbol]): String = s match {
case Nil() => ""
- case Cons(a, Nil) => rendersymbol(a)
+ case Cons(a, Nil()) => rendersymbol(a)
case Cons(a, q) => rendersymbol(a) + " " + renderListsymbol(q)
}
renderSymbol(r.left) + " -> " + renderListSymbol(r.right) + ""
@@ -196,7 +195,7 @@ object Gra��arRender {
def renderRule(r: Rule): String = {
def renderListSymbol(s: List[Symbol]): String = s match {
case Nil() => ""
- case Cons(a, Nil) => rendersymbol(a)
+ case Cons(a, Nil()) => rendersymbol(a)
case Cons(a, q) => rendersymbol(a) + " " + renderListsymbol(q)
}
renderSymbol(r.left) + " -> " + renderListSymbol(r.right) + ""