From 1cbb8bee2f95a2de628bfd4ea74ec1de8e4d7064 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <a-mikmay@microsoft.com>
Date: Wed, 25 Nov 2015 17:15:01 +0100
Subject: [PATCH] Better support for splitting at word boundaries. Added
corresponding test case
---
.../leon/solvers/string/StringSolver.scala | 38 +++++++++-
.../solvers/StringSolverSuite.scala | 69 ++++++++++---------
2 files changed, 72 insertions(+), 35 deletions(-)
diff --git a/src/main/scala/leon/solvers/string/StringSolver.scala b/src/main/scala/leon/solvers/string/StringSolver.scala
index 2ac5e49e6..b1b93568a 100644
--- a/src/main/scala/leon/solvers/string/StringSolver.scala
+++ b/src/main/scala/leon/solvers/string/StringSolver.scala
@@ -120,7 +120,7 @@ object StringSolver {
}
case sentence::q => obtainAssignments(q, assignments)
}
- val simplifiedOpt = mergeConstants(p)
+ val simplifiedOpt = mergeConstants(p.distinct)
.flatMap(simplifyConstants(_))
simplifiedOpt match {
@@ -338,6 +338,8 @@ object StringSolver {
val pos = prioritizedPositions(rhs)
val numBestVars = ids.count { x => x == bestVar }
+
+
if(worstScore == bestScore) {
for{
i <- pos // Prioritization on positions which are separators.
@@ -348,9 +350,33 @@ object StringSolver {
if !remaining_split.contains(x) || remaining_split(x) == xvalue
} yield (remaining_split + (x -> xvalue))
} else { // A variable appears more than others in the same equation, so its changes are going to propagate more.
- val strings = (for{ i <- pos
+ val indexBestVar = ids.indexOf(bestVar)
+ val strings = if(indexBestVar == 0) { // Test only string prefixes or empty string
+ (for{j <- (rhs.length to 1 by -1).toStream
+ if pos contains j} yield rhs.substring(0, j)) #:::
+ (for{j <- (rhs.length to 1 by -1).toStream
+ if !(pos contains j)} yield rhs.substring(0, j)) #:::
+ Stream("")
+ } else {
+ val lastIndexBestVar = ids.lastIndexOf(bestVar)
+ if(lastIndexBestVar == ids.length - 1) {
+ (for{ i <- pos.toStream // Try to maximize the size of the string from the start
+ if i != rhs.length
+ } yield rhs.substring(i)) #:::
+ Stream("")
+ } else { // Inside, can be anything.
+ (for{ i <- pos.toStream // Try to maximize the size of the string from the start
+ if i != rhs.length
+ j <- rhs.length to (i+1) by -1
+ if pos contains j} yield rhs.substring(i, j)) #:::
+ (for{ i <- pos.toStream
if i != rhs.length
- j <- (i + 1) to rhs.length} yield rhs.substring(i, j)) #::: Stream("")
+ j <- rhs.length to (i+1) by -1
+ if !(pos contains j)} yield rhs.substring(i, j)) #:::
+ Stream("")
+ }
+ }
+ //println("Best variable:" + bestVar + " going to test " + strings.toList)
(for(str <- strings.distinct
if java.util.regex.Pattern.quote(str).r.findAllMatchIn(rhs).length >= numBestVars
@@ -433,6 +459,12 @@ object StringSolver {
/** Solves the problem and returns all possible satisfying assignment */
def solve(p: Problem): Stream[Assignment] = {
val realProblem = forwardStrategy(p, Map())
+ /*if(realProblem.nonEmpty) {
+ println("Problem:\n"+renderProblem(p))
+ println("Solutions:\n"+realProblem.get._2)
+ println("Real problem:\n"+renderProblem(realProblem.get._1))
+ }*/
+
realProblem match {
case None =>
Stream.Empty
diff --git a/src/test/scala/leon/integration/solvers/StringSolverSuite.scala b/src/test/scala/leon/integration/solvers/StringSolverSuite.scala
index dc34901da..8d5530578 100644
--- a/src/test/scala/leon/integration/solvers/StringSolverSuite.scala
+++ b/src/test/scala/leon/integration/solvers/StringSolverSuite.scala
@@ -6,6 +6,7 @@ import leon.test.helpers.ExpressionsDSL
import leon.solvers.string.StringSolver
import leon.purescala.Common.FreshIdentifier
import leon.purescala.Common.Identifier
+import scala.collection.mutable.{HashMap => MMap}
/**
* @author Mikael
@@ -74,9 +75,9 @@ class StringSolverSuite extends FunSuite with Matchers {
simpleSplit(List(x, y, x), "aba").toList should equal (List(Map(x -> "", y -> "aba"), Map(x -> "a", y -> "b")))
}
- test("simpleSplitPriority") {
+ test("simpleSplitPriority") { // Just guesses some values for y.
implicit val stats = Map(x -> 1, y -> 2)
- simpleSplit(List(x, y, y, y), "a121212").toList should equal (List(Map(y -> "1"), Map(y -> "12"), Map(y -> "2"), Map(y -> "")))
+ simpleSplit(List(x, y, y, y), "a121212").toList should equal (List(Map(y -> "12"), Map(y -> "2"), Map(y -> "")))
}
@@ -141,23 +142,23 @@ class StringSolverSuite extends FunSuite with Matchers {
x -> complexString2,
z -> complexString3)))
}
-
- test("ListInt") {
- var idMap = Map[String, Identifier]()
- def makeSf(lhs: String): StringForm = {
- for(elem <- lhs.split("\\+").toList) yield {
- if(elem.startsWith("\"")) {
- Left(elem.substring(1, elem.length - 1))
- } else {
- val id = idMap.getOrElse(elem, {
- val res = FreshIdentifier(elem)
- idMap += elem -> res
- res
- })
- Right(id)
- }
+ def makeSf(lhs: String)(implicit idMap: MMap[String, Identifier]): StringForm = {
+ for(elem <- lhs.split("\\+").toList) yield {
+ if(elem.startsWith("\"")) {
+ Left(elem.substring(1, elem.length - 1))
+ } else {
+ val id = idMap.getOrElse(elem, {
+ val res = FreshIdentifier(elem)
+ idMap += elem -> res
+ res
+ })
+ Right(id)
}
}
+ }
+
+ test("ListInt") {
+ implicit val idMap = MMap[String, Identifier]()
val lhs1 = makeSf("""const8+const4+"12"+const5+const+"-1"+const1+const3+const2+const6+const9""")
val lhs2 = makeSf("""const8+const4+"1"+const5+const3+const6+const9""")
val lhs3 = makeSf("""const8+const7+const9""")
@@ -168,21 +169,25 @@ class StringSolverSuite extends FunSuite with Matchers {
solve(problem) should not be 'empty
}
- test("solveJadProblem") {
+ test("ListInt as List(...)") {
+ implicit val idMap = MMap[String, Identifier]()
+ val lhs1 = makeSf("const8+const7+const9")
+ val rhs1 = "List()"
+ val lhs2 = makeSf("""const8+const4+"1"+const5+const3+const6+const9""")
+ val rhs2 = "List(1)"
+ val lhs3 = makeSf("""const8+const4+"12"+const5+const+"-1"+const1+const3+const2+const6+const9""")
+ val rhs3 = "List(12, -1)"
+ val problem = List((lhs1, rhs1), (lhs2, rhs2), (lhs3, rhs3))
+ val solution = solve(problem)
+ solution should not be 'empty
+ val firstSolution = solution(0)
+ firstSolution(idMap("const8")) should equal("List(")
+ }
+
+ /*test("solveJadProblem") {
val lhs = """const26+const22+const7+const+const8+const3+const9+const5+"5"+const6+const10+const23+const18+const11+const+const12+const19+const18+const7+const1+const8+const2+const9+const4+const10+const19+const18+const13+const+const14+const3+const15+const5+"5"+const6+const16+const4+const17+const19+const18+const11+const1+const12+const19+const18+const13+const1+const14+const2+const15+const4+const16+const5+"5"+const6+const17+const19+const21+const20+const20+const20+const20+const20+const24+const27"""
- var idMap = Map[String, Identifier]()
- val lhsSf = for(elem <- lhs.split("\\+")) yield {
- if(elem.startsWith("\"")) {
- Left(elem.substring(1, elem.length - 1))
- } else {
- val id = idMap.getOrElse(elem, {
- val res = FreshIdentifier(elem)
- idMap += elem -> res
- res
- })
- Right(id)
- }
- }
+ implicit val idMap = MMap[String, Identifier]()
+ val lhsSf = makeSf(lhs)
val expected = """T1: call Push(5)
T1: internal
@@ -195,5 +200,5 @@ T2: ret Pop() -> 5"""
println("Problem to solve:" + StringSolver.renderProblem(problem))
solve(problem) should not be 'empty
- }
+ }*/
}
\ No newline at end of file
--
GitLab