diff --git a/src/main/scala/leon/synthesis/disambiguation/QuestionBuilder.scala b/src/main/scala/leon/synthesis/disambiguation/QuestionBuilder.scala index c4fd02c0266cf5e9e29602404301bd05b2d15800..bb3dc45ffd8d3a0fa4a3dd87fc436a7b3dfde113 100644 --- a/src/main/scala/leon/synthesis/disambiguation/QuestionBuilder.scala +++ b/src/main/scala/leon/synthesis/disambiguation/QuestionBuilder.scala @@ -144,18 +144,33 @@ class QuestionBuilder[T <: Expr]( /** Make all generic values unique. * Duplicate generic values are not suitable for disambiguating questions since they remove an order. */ def makeGenericValuesUnique(a: Expr): Expr = { - var genVals = Set[GenericValue]() - @tailrec @inline def freshGenericValue(g: GenericValue): GenericValue = { - if(genVals contains g) - freshGenericValue(GenericValue(g.tp, g.id + 1)) - else { - genVals += g - g - } + var genVals = Set[Expr with Terminal]() + def freshenValue(g: Expr with Terminal): Option[Expr with Terminal] = g match { + case g: GenericValue => Some(GenericValue(g.tp, g.id + 1)) + case StringLiteral(s) => + val i = s.lastIndexWhere { c => c < '0' || c > '9' } + val prefix = s.take(i+1) + val suffix = s.drop(i+1) + Some(StringLiteral(prefix + (if(suffix == "") "0" else (suffix.toInt + 1).toString))) + case InfiniteIntegerLiteral(i) => Some(InfiniteIntegerLiteral(i+1)) + case IntLiteral(i) => if(i == Integer.MAX_VALUE) None else Some(IntLiteral(i+1)) + case CharLiteral(c) => if(c == Char.MaxValue) None else Some(CharLiteral((c+1).toChar)) + case otherLiteral => None + } + @tailrec @inline def freshValue(g: Expr with Terminal): Expr with Terminal = { + if(genVals contains g) + freshenValue(g) match { + case None => g + case Some(v) => freshValue(v) + } + else { + genVals += g + g + } } ExprOps.postMap{ e => e match { - case g@GenericValue(tpe, i) => - Some(freshGenericValue(g)) + case g:Expr with Terminal => + Some(freshValue(g)) case _ => None }}(a) } diff --git a/testcases/web/synthesis/25_String_OutOfOrder.scala b/testcases/web/synthesis/25_String_OutOfOrder.scala index 72785cf605cfbfe26bb70abd37651c32d5eddd42..ec855caeee8e2f2eb67b0743438d85c7902dc47d 100644 --- a/testcases/web/synthesis/25_String_OutOfOrder.scala +++ b/testcases/web/synthesis/25_String_OutOfOrder.scala @@ -5,13 +5,13 @@ import leon.collection.ListOps._ import leon.lang.synthesis._ object OutOfOrderToString { - def argumentsToString(i: Int, j: Int): String = { + def arguments(i: Int, j: Int): String = { ??? } ensuring { (res: String) => ((i, j), res) passes { case (1, 2) => "2, 1" } } - def tupleToString(i: (Int, Int)): String = { + def tuple(i: (Int, Int)): String = { ??? } ensuring { (res: String) => (i, res) passes { case (1, 2) => "2, 1" @@ -27,7 +27,7 @@ object OutOfOrderToString { } } - def listPairToString(l : List[(Int, Int)]): String = { + def listPair(l : List[(Int, Int)]): String = { ???[String] } ensuring { (res : String) => (l, res) passes { @@ -36,7 +36,7 @@ object OutOfOrderToString { } } - def reverselistPairToString(l: List[(Int, Int)]): String = { + def reverselistPair(l: List[(Int, Int)]): String = { ??? } ensuring { (res: String) => (l, res) passes { case Cons((1, 2), Cons((3,4), Nil())) => "4 -> 3, 2 -> 1" @@ -44,7 +44,7 @@ object OutOfOrderToString { case class Rule(input: Int, applied: Option[Int]) - def ruleToString(r : Rule): String = { + def rule(r : Rule): String = { ??? } ensuring { (res : String) => (r, res) passes {