diff --git a/library/lang/StrOps.scala b/library/lang/StrOps.scala
index 3a6cfdc324b14c175062cd49ba4fc5473cfaa011..0c4d480eeb5ac0ccc1021c7bac1cf37b07520424 100644
--- a/library/lang/StrOps.scala
+++ b/library/lang/StrOps.scala
@@ -18,22 +18,4 @@ object StrOps {
def substring(a: String, start: BigInt, end: BigInt): String = {
if(start > end || start >= length(a) || end <= 0) "" else a.substring(start.toInt, end.toInt)
}
- @library
- def bigIntToString(a: BigInt): String = {
- a.toString
- }
- @library
- def intToString(a: Int): String = {
- a.toString
- }
- @library
- def booleanToString(a: Boolean): String = {
- if(a) "true" else "false"
- }
- @library
- def charToString(a: Char): String = {
- a.toString
- }
- @ignore
- def realToString(a: Real): String = ???
}
\ No newline at end of file
diff --git a/src/main/scala/leon/synthesis/FileInterface.scala b/src/main/scala/leon/synthesis/FileInterface.scala
index 25edd338fd2111314dd050d55da9ca14209a62d1..cba6629dad2aab1cddc0b857bc0fbe7bd4d66d76 100644
--- a/src/main/scala/leon/synthesis/FileInterface.scala
+++ b/src/main/scala/leon/synthesis/FileInterface.scala
@@ -45,14 +45,37 @@ class FileInterface(reporter: Reporter) {
}
}
- def substitute(str: String, fromTree: Tree, printer: (Int) => String): String = {
+ def substitute(originalCode: String, fromTree: Tree, printer: (Int) => String): String = {
fromTree.getPos match {
case rp: RangePosition =>
val from = rp.pointFrom
val to = rp.pointTo
- val before = str.substring(0, from)
- val after = str.substring(to, str.length)
+ val before = originalCode.substring(0, from)
+ val after = originalCode.substring(to, originalCode.length)
+
+ // Get base indentation of last line:
+ val lineChars = before.substring(before.lastIndexOf('\n')+1).toList
+
+ val indent = lineChars.takeWhile(_ == ' ').size
+
+ val res = printer(indent/2)
+
+ before + res + after
+
+ case p =>
+ sys.error("Substitution requires RangePos on the input tree: "+fromTree +": "+fromTree.getClass+" GOT" +p)
+ }
+ }
+
+ def insertAfter(originalCode: String, fromTree: Tree, printer: (Int) => String): String = {
+ fromTree.getPos match {
+ case rp: RangePosition =>
+ val from = rp.pointFrom
+ val to = rp.pointTo
+
+ val before = originalCode.substring(0, to)
+ val after = originalCode.substring(to, originalCode.length)
// Get base indentation of last line:
val lineChars = before.substring(before.lastIndexOf('\n')+1).toList
diff --git a/src/main/scala/leon/synthesis/disambiguation/ExamplesAdder.scala b/src/main/scala/leon/synthesis/disambiguation/ExamplesAdder.scala
index 42e3e6d99bb5cd804ff753f9d32225c63196898b..51e88cfef72acddc85c2ee503a5ba4e68d1adcba 100644
--- a/src/main/scala/leon/synthesis/disambiguation/ExamplesAdder.scala
+++ b/src/main/scala/leon/synthesis/disambiguation/ExamplesAdder.scala
@@ -44,7 +44,7 @@ class ExamplesAdder(ctx0: LeonContext, program: Program) {
} else {
val newPasses = exprs(i) match {
case Passes(in, out, cases) =>
- Passes(in, out, cases ++ newCases )
+ Passes(in, out, (cases ++ newCases).distinct )
case _ => ???
}
val newPost = and(exprs.updated(i, newPasses) : _*)
diff --git a/src/main/scala/leon/synthesis/disambiguation/QuestionBuilder.scala b/src/main/scala/leon/synthesis/disambiguation/QuestionBuilder.scala
index 08d2daabc8ef1ddb6416830d94265e9ce8acdfa9..7b0de3e68d992de2c5f5d3fc7d37568b77f325a1 100644
--- a/src/main/scala/leon/synthesis/disambiguation/QuestionBuilder.scala
+++ b/src/main/scala/leon/synthesis/disambiguation/QuestionBuilder.scala
@@ -77,6 +77,7 @@ object QuestionBuilder {
* [element of r.solution]
* }}}
*
+ * @tparam T A subtype of Expr that will be the type used in the Question[T] results.
* @param input The identifier of the unique function's input. Must be typed or the type should be defined by setArgumentType
* @param ruleApplication The set of solutions for the body of f
* @param filter A function filtering which outputs should be considered for comparison.
@@ -90,17 +91,20 @@ class QuestionBuilder[T <: Expr](input: Seq[Identifier], solutions: Stream[Solut
private var _alternativeSortMethod: AlternativeSortingType[T] = AlternativeSortingType.BalancedParenthesisIsBetter[T]() && AlternativeSortingType.ShorterIsBetter[T]()
private var solutionsToTake = 15
private var expressionsToTake = 15
-
+ private var keepEmptyAlternativeQuestions: T => Boolean = Set()
+
/** Sets the way to sort questions. See [[QuestionSortingType]] */
- def setSortQuestionBy(questionSorMethod: QuestionSortingType) = _questionSorMethod = questionSorMethod
+ def setSortQuestionBy(questionSorMethod: QuestionSortingType) = { _questionSorMethod = questionSorMethod; this }
/** Sets the way to sort alternatives. See [[AlternativeSortingType]] */
- def setSortAlternativesBy(alternativeSortMethod: AlternativeSortingType[T]) = _alternativeSortMethod = alternativeSortMethod
+ def setSortAlternativesBy(alternativeSortMethod: AlternativeSortingType[T]) = { _alternativeSortMethod = alternativeSortMethod; this }
/** Sets the argument type. Not needed if the input identifier is already assigned a type. */
- def setArgumentType(argTypes: List[TypeTree]) = _argTypes = argTypes
+ def setArgumentType(argTypes: List[TypeTree]) = { _argTypes = argTypes; this }
/** Sets the number of solutions to consider. Default is 15 */
- def setSolutionsToTake(n: Int) = solutionsToTake = n
+ def setSolutionsToTake(n: Int) = { solutionsToTake = n; this }
/** Sets the number of expressions to consider. Default is 15 */
- def setExpressionsToTake(n: Int) = expressionsToTake = n
+ def setExpressionsToTake(n: Int) = { expressionsToTake = n; this }
+ /** Sets if when there is no alternative, the question should be kept. */
+ def setKeepEmptyAlternativeQuestions(b: T => Boolean) = {keepEmptyAlternativeQuestions = b; this }
private def run(s: Solution, elems: Seq[(Identifier, Expr)]): Option[Expr] = {
val newProgram = DefOps.addFunDefs(p, s.defs, p.definedFunctions.head)
@@ -135,7 +139,7 @@ class QuestionBuilder[T <: Expr](input: Seq[Identifier], solutions: Stream[Solut
alternative_output_filtered <- filter(alternative_output)
if alternative_output != current_output
} yield alternative_output_filtered).distinct
- if(alternative_outputs.nonEmpty) {
+ if(alternative_outputs.nonEmpty || keepEmptyAlternativeQuestions(current_output)) {
questions += Question(possible_input.map(_._2), current_output, alternative_outputs.sortWith((e,f) => _alternativeSortMethod.compare(e, f) <= 0))
}
}
diff --git a/src/main/scala/leon/synthesis/rules/StringRender.scala b/src/main/scala/leon/synthesis/rules/StringRender.scala
index b950213ce5a86fbbf9e0c7e164265e2c6b6cb8f0..3604808df22992888cb7ed9b01843530ad690f95 100644
--- a/src/main/scala/leon/synthesis/rules/StringRender.scala
+++ b/src/main/scala/leon/synthesis/rules/StringRender.scala
@@ -471,10 +471,10 @@ case object StringRender extends Rule("StringRender") {
val (expr, synthesisResult) = createFunDefsTemplates(StringSynthesisContext.empty, p.as.map(Variable))
val funDefs = synthesisResult.adtToString
- val toDebug: String = (("\nInferred functions:" /: funDefs)( (t, s) =>
+ /*val toDebug: String = (("\nInferred functions:" /: funDefs)( (t, s) =>
t + "\n" + s._2._1.toString
- ))
- hctx.reporter.debug("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/verification/VerificationReport.scala b/src/main/scala/leon/verification/VerificationReport.scala
index 50f8f6f8b08f59080941fcb34b0a49e152206cbe..9ee17c76ee82a7112a735c6d4a2ca11a06acb695 100644
--- a/src/main/scala/leon/verification/VerificationReport.scala
+++ b/src/main/scala/leon/verification/VerificationReport.scala
@@ -24,11 +24,12 @@ import purescala.Definitions._
import leon.solvers.{ HenkinModel, Model, SolverFactory }
object VerificationReport {
- /** If it can be computed, returns a user defined string for the given expression */
- def userDefinedString(v: Expr, orElse: =>String)(ctx: LeonContext, program: Program): String = {
+ /** If it can be computed, returns a user defined string for the given expression
+ * @param The list of functions which should be excluded from pretty-printing (to avoid rendering counter-examples of toString methods using the method itself) */
+ def userDefinedString(v: Expr, orElse: =>String, excluded: FunDef => Boolean = Set())(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 =>
+ case fd if !excluded(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)
@@ -38,7 +39,6 @@ object VerificationReport {
//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/web/synthesis/23_String_Grammar.scala b/testcases/web/synthesis/23_String_Grammar.scala
index 4bed0c51edf372134aa3531567f2bdb35e7cc85b..dceeba92a3b3680c593af79d5cc5f77d14afd8ee 100644
--- a/testcases/web/synthesis/23_String_Grammar.scala
+++ b/testcases/web/synthesis/23_String_Grammar.scala
@@ -78,34 +78,71 @@ S0 -> S0 t1"""
//////////////////////////////////////////////
// Non-incremental examples: pure synthesis //
//////////////////////////////////////////////
- def synthesizeStandard(s: Grammar): String = {
+ /*def synthesizeStandard(s: Grammar): String = {
???[String]
- } ensuring psStandard(s)
+ } ensuring psStandard(s)*/
- def synthesizeRemoveNames(s: Grammar): String = {
+ /*def synthesizeRemoveNames(s: Grammar): String = {
???[String]
- } ensuring psRemoveNames(s)
+ } ensuring psRemoveNames(s)*/
- def synthesizeArrowRules(s: Grammar): String = {
+ /*def synthesizeArrowRules(s: Grammar): String = {
???[String]
- } ensuring psArrowRules(s)
+ } ensuring psArrowRules(s)*/
- def synthesizeListRules(s: Grammar): String = {
+ /*def synthesizeListRules(s: Grammar): String = {
???[String]
- } ensuring psListRules(s)
+ } ensuring psListRules(s)*/
- def synthesizeSpaceRules(s: Grammar): String = {
+ /*def synthesizeSpaceRules(s: Grammar): String = {
???[String]
- } ensuring psSpaceRules(s)
+ } ensuring psSpaceRules(s)*/
- def synthesizeHTMLRules(s: Grammar): String = {
+ /*def synthesizeHTMLRules(s: Grammar): String = {
???[String]
- } ensuring psHTMLRules(s)
+ } ensuring psHTMLRules(s)*/
- def synthesizePlainTextRulesToString(s: Grammar): String = {
+ /*def synthesizePlainTextRulesToString(s: Grammar): String = {
???[String]
- } ensuring psPlainTextRules(s)
+ } ensuring psPlainTextRules(s)*/
- def allGrammarsAreIdentical(g: Grammar, g2: Grammar) = (g == g2 || g.rules == g2.rules) holds
-
+ def isTerminal(s: Symbol) = s match {
+ case Terminal(_) => true
+ case _ => false
+ }
+
+ def isGrammarRule(r: Rule) = !isTerminal(r.left)
+
+ def noEpsilon(r: Rule) = r.right match {
+ case Nil() => false
+ case Cons(_, _) => true
+ }
+
+ def areGrammarRule(lr: List[Rule]): Boolean = lr match {
+ case Nil() => true
+ case Cons(r, q) => isGrammarRule(r) && areGrammarRule(q)
+ }
+
+ def noEpsilons(lr: List[Rule]): Boolean = lr match {
+ case Nil() => true
+ case Cons(r, q) => noEpsilon(r) && noEpsilons(q)
+ }
+
+ def isGrammar(g: Grammar) = !isTerminal(g.start) && areGrammarRule(g.rules)
+
+ def isReasonableRule(r: List[Symbol], excluded: Symbol): Boolean = r match {
+ case Nil() => true
+ case Cons(rs, q) if rs == excluded => false
+ case Cons(_, q) => isReasonableRule(q, excluded)
+ }
+
+ def isReasonable(lr: List[Rule]): Boolean = lr match {
+ case Nil() => true
+ case Cons(r, q) => isReasonableRule(r.right, r.left) && isReasonable(q)
+ }
+
+ def allGrammarsAreIdentical(g: Grammar, g2: Grammar) = {
+ require(isGrammar(g) && isGrammar(g2) && noEpsilons(g.rules) && noEpsilons(g2.rules) && isReasonable(g.rules) && isReasonable(g2.rules))
+ (g == g2 || g.rules == g2.rules)
+ } holds
}
\ No newline at end of file