From dbd24fd7e165c08dc1e3d220bf37cf4d02eada6b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <a-mikmay@microsoft.com>
Date: Mon, 23 Nov 2015 16:50:46 +0100
Subject: [PATCH] Better prioritization for string splitting.
---
src/main/scala/leon/solvers/string/StringSolver.scala | 11 ++++++++++-
1 file changed, 10 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/leon/solvers/string/StringSolver.scala b/src/main/scala/leon/solvers/string/StringSolver.scala
index b953b8cb1..9e87d53d0 100644
--- a/src/main/scala/leon/solvers/string/StringSolver.scala
+++ b/src/main/scala/leon/solvers/string/StringSolver.scala
@@ -198,6 +198,15 @@ object StringSolver {
res
}
+ def prioritizedPositions(s: String): Stream[Int] = {
+ val separations = "\\b".r.findAllMatchIn(s).map(m => m.start)
+ separations.toStream #::: {
+ val done = separations.toSet
+ for( i <- (0 to s.length).toStream if !done(i)) yield i
+ }
+ }
+
+
/** Solves the equation x1x2x3...xn = CONSTANT */
def simpleSplit(ids: List[Identifier], rhs: String): Stream[Assignment] = {
ids match {
@@ -205,7 +214,7 @@ object StringSolver {
case List(x) =>
Stream(Map(x -> rhs))
case x :: ys => for{
- i <- (0 to rhs.length).toStream
+ i <- prioritizedPositions(rhs) // Prioritization on positions which are separators.
xvalue = rhs.substring(0, i)
rvalue = rhs.substring(i)
remaining_splits = simpleSplit(ys, rvalue)
--
GitLab