diff --git a/src/main/java/leon/codegen/runtime/StrOps.java b/src/main/java/leon/codegen/runtime/StrOps.java
index d8a889101e9fd90e9208ad30ec9231d3264a36cf..7f6013501436079fbbc6a290604a98bb12cd99b6 100644
--- a/src/main/java/leon/codegen/runtime/StrOps.java
+++ b/src/main/java/leon/codegen/runtime/StrOps.java
@@ -4,39 +4,50 @@ import org.apache.commons.lang3.StringEscapeUtils;
public class StrOps {
public static String concat(String a, String b) {
- return a + b;
- }
+ return a + b;
+ }
+
public static BigInt length(String a) {
- return new BigInt(String.valueOf(a.length()));
- }
- public static String substring (String a, BigInt start, BigInt end) {
- if(start.greaterEquals(end) || start.greaterEquals(length(a)) || end.lessEquals(new BigInt("0")))
- return "";
- else
- return a.substring(start.underlying().intValue(), end.underlying().intValue());
- }
- public static String bigIntToString (BigInt a) {
- return a.toString();
- }
- public static String intToString (int a) {
- return String.valueOf(a);
- }
- public static String doubleToString (double a) {
- return String.valueOf(a);
- }
- public static String booleanToString (boolean a) {
- if(a)
- return "true";
- else
- return "false";
- }
- public static String charToString (char a) {
- return String.valueOf(a);
- }
- public static String realToString (Real a) {
- return ""; // TODO: Not supported at this moment.
+ return new BigInt(String.valueOf(a.length()));
}
+
+ public static String substring(String a, BigInt start, BigInt end) {
+ if (start.greaterEquals(end) || start.greaterEquals(length(a))
+ || end.lessEquals(new BigInt("0")))
+ throw new RuntimeError("Invalid substring indices : " + start + ", " + end + " for string \""+a+""\"");
+ else
+ return a.substring(start.underlying().intValue(), end.underlying()
+ .intValue());
+ }
+
+ public static String bigIntToString(BigInt a) {
+ return a.toString();
+ }
+
+ public static String intToString(int a) {
+ return String.valueOf(a);
+ }
+
+ public static String doubleToString(double a) {
+ return String.valueOf(a);
+ }
+
+ public static String booleanToString(boolean a) {
+ if (a)
+ return "true";
+ else
+ return "false";
+ }
+
+ public static String charToString(char a) {
+ return String.valueOf(a);
+ }
+
+ public static String realToString(Real a) {
+ return ""; // TODO: Not supported at this moment.
+ }
+
public static String escape(String s) {
- return StringEscapeUtils.escapeJava(s);
+ return StringEscapeUtils.escapeJava(s);
}
}
diff --git a/src/main/scala/leon/datagen/VanuatooDataGen.scala b/src/main/scala/leon/datagen/VanuatooDataGen.scala
index 7b259f2ea8fe20ab55f75c8fbce7dc34fbc7ee29..8b4846a3394c3c3ddd2326d24d23ce95e68f6b05 100644
--- a/src/main/scala/leon/datagen/VanuatooDataGen.scala
+++ b/src/main/scala/leon/datagen/VanuatooDataGen.scala
@@ -41,7 +41,7 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
(n, d) -> Constructor[Expr, TypeTree](List(), RealType, s => FractionalLiteral(n, d), "" + n + "/" + d)
}).toMap
- val strings = (for (b <- Set("", "a", "\"\t\n", "Abcd")) yield {
+ val strings = (for (b <- Set("", "a", "foo", "bar")) yield {
b -> Constructor[Expr, TypeTree](List(), StringType, s => StringLiteral(b), b)
}).toMap
diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index 561d267dfe7af1a3531d7a6b9c59c8a391628c5c..1016406b2b79e8f116208796e3e0a66cb0b4ec4d 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -244,11 +244,9 @@ trait ASTExtractors {
}
- /** Returns a string literal either from leon.lang.string.String or from a constant string literal. */
+ /** Returns a string literal from a constant string literal. */
object ExStringLiteral {
def unapply(tree: Tree): Option[String] = tree match {
- case Apply(ExSelected("leon", "lang", "string", "package", "strToStr"), (str: Literal) :: Nil) =>
- Some(str.value.stringValue)
case Literal(c @ Constant(i)) if c.tpe == StringClass.tpe =>
Some(c.stringValue)
case _ =>
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 4d6a1b113e10292b32ab91d0bd757fa6a0befc8e..7a575d8da21e1435b68197da1d14c3bbd1b8f534 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -1749,9 +1749,6 @@ trait CodeExtraction extends ASTExtractors {
val typea1 = a1.getType
val typea2 = a2.map(_.getType).mkString(",")
val sa2 = a2.mkString(",")
- try {
- println(Thread.currentThread().getStackTrace.take(5).mkString("\n"))
- } catch { case e: Throwable => }
outOfSubsetError(tr, "Unknown call to " + name + s" on $a1 ($typea1) with arguments $sa2 of type $typea2")
}
diff --git a/src/main/scala/leon/grammars/ValueGrammar.scala b/src/main/scala/leon/grammars/ValueGrammar.scala
index 7fa70729c68bfe1a3463e9f3b6ccc6e7de92517e..98850c8df4adcf3e776970c176cf37c251823917 100644
--- a/src/main/scala/leon/grammars/ValueGrammar.scala
+++ b/src/main/scala/leon/grammars/ValueGrammar.scala
@@ -29,8 +29,8 @@ case object ValueGrammar extends ExpressionGrammar[TypeTree] {
List(
terminal(StringLiteral("")),
terminal(StringLiteral("a")),
- terminal(StringLiteral("\"'\n\r\t")),
- terminal(StringLiteral("Lara 2007"))
+ terminal(StringLiteral("foo")),
+ terminal(StringLiteral("bar"))
)
case tp: TypeParameter =>
diff --git a/src/main/scala/leon/purescala/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala
index cd66e57d665ba5e310cc3b832772eae6af4e2c8c..f0b2a975b1517b2f9fd31422d3e9a911f9489d98 100644
--- a/src/main/scala/leon/purescala/Constructors.scala
+++ b/src/main/scala/leon/purescala/Constructors.scala
@@ -145,7 +145,7 @@ object Constructors {
resType match {
case Some(tpe) =>
- casesFiltered.filter(c => isSubtypeOf(c.rhs.getType, tpe) || isSubtypeOf(tpe, c.rhs.getType) || c.optGuard.nonEmpty)
+ casesFiltered.filter(c => isSubtypeOf(c.rhs.getType, tpe) || isSubtypeOf(tpe, c.rhs.getType))
case None =>
casesFiltered
}
diff --git a/src/main/scala/leon/purescala/ScalaPrinter.scala b/src/main/scala/leon/purescala/ScalaPrinter.scala
index 390e1af2c62ede0bc0bf934f582d248832650226..67cc994649e6b454ee8389fbfdd7674da4aebb6a 100644
--- a/src/main/scala/leon/purescala/ScalaPrinter.scala
+++ b/src/main/scala/leon/purescala/ScalaPrinter.scala
@@ -41,14 +41,6 @@ class ScalaPrinter(opts: PrinterOptions,
case m @ FiniteMap(els, k, v) => p"Map[$k,$v]($els)"
case InfiniteIntegerLiteral(v) => p"BigInt($v)"
- case StringLiteral(v) =>
- if(v.count(c => c == '\n') >= 1 && v.length >= 80 && v.indexOf("\"\"\"") == -1) {
- p"$dbquote$dbquote$dbquote$v$dbquote$dbquote$dbquote"
- } else {
- val escaped = StringEscapeUtils.escapeJava(v)
- p"$dbquote$escaped$dbquote"
- }
-
case a@FiniteArray(elems, oDef, size) =>
import ExprOps._
val ArrayType(underlying) = a.getType
diff --git a/src/main/scala/leon/synthesis/disambiguation/QuestionBuilder.scala b/src/main/scala/leon/synthesis/disambiguation/QuestionBuilder.scala
index a33b71ca435123c3ee8de9385bde72528a26b1b3..e8205da76abfc0076eaa0b0fd5de861e81185079 100644
--- a/src/main/scala/leon/synthesis/disambiguation/QuestionBuilder.scala
+++ b/src/main/scala/leon/synthesis/disambiguation/QuestionBuilder.scala
@@ -8,7 +8,7 @@ import purescala.Expressions._
import purescala.ExprOps
import purescala.Constructors._
import purescala.Extractors._
-import purescala.Types.TypeTree
+import purescala.Types.{StringType, TypeTree}
import purescala.Common.Identifier
import purescala.Definitions.Program
import purescala.DefOps
@@ -17,6 +17,7 @@ import bonsai.enumerators.MemoizedEnumerator
import solvers.Model
import solvers.ModelBuilder
import scala.collection.mutable.ListBuffer
+import leon.grammars.ExpressionGrammar
object QuestionBuilder {
/** Sort methods for questions. You can build your own */
@@ -67,6 +68,20 @@ object QuestionBuilder {
def compare(e: T, f: T): Int = convert(e) - convert(f)
}
}
+
+ /** Specific enumeration of strings, which can be used with the QuestionBuilder#setValueEnumerator method */
+ object SpecialStringValueGrammar extends ExpressionGrammar[TypeTree] {
+ def computeProductions(t: TypeTree)(implicit ctx: LeonContext): Seq[Gen] = t match {
+ case StringType =>
+ List(
+ terminal(StringLiteral("")),
+ terminal(StringLiteral("a")),
+ terminal(StringLiteral("\"'\n\t")),
+ terminal(StringLiteral("Lara 2007"))
+ )
+ case _ => ValueGrammar.computeProductions(t)
+ }
+ }
}
/**
@@ -97,6 +112,7 @@ class QuestionBuilder[T <: Expr](
private var solutionsToTake = 30
private var expressionsToTake = 30
private var keepEmptyAlternativeQuestions: T => Boolean = Set()
+ private var value_enumerator: ExpressionGrammar[TypeTree] = ValueGrammar
/** Sets the way to sort questions. See [[QuestionSortingType]] */
def setSortQuestionBy(questionSorMethod: QuestionSortingType) = { _questionSorMethod = questionSorMethod; this }
@@ -110,6 +126,8 @@ class QuestionBuilder[T <: Expr](
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 }
+ /** Sets the way to enumerate expressions */
+ def setValueEnumerator(v: ExpressionGrammar[TypeTree]) = value_enumerator = v
private def run(s: Solution, elems: Seq[(Identifier, Expr)]): Option[Expr] = {
val newProgram = DefOps.addFunDefs(p, s.defs, p.definedFunctions.head)
@@ -124,7 +142,7 @@ class QuestionBuilder[T <: Expr](
def result(): List[Question[T]] = {
if(solutions.isEmpty) return Nil
- val enum = new MemoizedEnumerator[TypeTree, Expr](ValueGrammar.getProductions)
+ val enum = new MemoizedEnumerator[TypeTree, Expr](value_enumerator.getProductions)
val values = enum.iterator(tupleTypeWrap(_argTypes))
val instantiations = values.map {
v => input.zip(unwrapTuple(v, input.size))
diff --git a/src/main/scala/leon/synthesis/rules/StringRender.scala b/src/main/scala/leon/synthesis/rules/StringRender.scala
index d2491d52f10a932b1c956c2b74f4f7690f68eed7..81b43f2ec5df8b278bdb4d7e25d20a9298ece61e 100644
--- a/src/main/scala/leon/synthesis/rules/StringRender.scala
+++ b/src/main/scala/leon/synthesis/rules/StringRender.scala
@@ -10,7 +10,6 @@ import scala.collection.mutable.ListBuffer
import bonsai.enumerators.MemoizedEnumerator
import leon.evaluators.DefaultEvaluator
import leon.evaluators.StringTracingEvaluator
-import leon.grammars.ValueGrammar
import leon.programsets.DirectProgramSet
import leon.programsets.JoinProgramSet
import leon.purescala.Common.FreshIdentifier