From a34c7448956403d10d22f2df189a37d9f7ef25e8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <a-mikmay@microsoft.com>
Date: Sat, 12 Dec 2015 09:17:55 +0100
Subject: [PATCH] Added one more StringSolver benchmark and re-enabled the
equation propagation phase after correcting the bug.
---
.../leon/solvers/string/StringSolver.scala | 6 +++---
.../solvers/StringSolverSuite.scala | 21 ++++++++++++++++---
2 files changed, 21 insertions(+), 6 deletions(-)
diff --git a/src/main/scala/leon/solvers/string/StringSolver.scala b/src/main/scala/leon/solvers/string/StringSolver.scala
index df214ca45..d681d500f 100644
--- a/src/main/scala/leon/solvers/string/StringSolver.scala
+++ b/src/main/scala/leon/solvers/string/StringSolver.scala
@@ -163,7 +163,7 @@ object StringSolver {
def run(p: Problem, s: Assignment) = {
ProblemSimplicationPhase.this.run(p, s) match {
case Some((p, s)) =>
- println("Problem before " + other.getClass.getName.substring(33) + ":" + (renderProblem(p), s))
+ //println("Problem before " + other.getClass.getName.substring(33) + ":" + (renderProblem(p), s))
other.run(p, s)
case None =>
None
@@ -369,7 +369,7 @@ object StringSolver {
object PropagateEquations extends ProblemSimplicationPhase {
def run(p: Problem, s: Assignment): Option[(Problem, Assignment)] = {
var newP = p.distinct
- for((lhs, rhs) <- p if lhs.length >= 2) {
+ for((lhs, rhs) <- newP if lhs.length >= 2) { // Original distinct p.
var indexInP = 0
for(eq@(lhs2, rhs2) <- newP) {
if((!(lhs2 eq lhs) || !(rhs2 eq rhs))) {
@@ -401,7 +401,7 @@ object StringSolver {
/** Composition of simplifyProblem and noLeftRightConstants */
val forwardStrategy =
- loopUntilConvergence(simplifyProblem andThen noLeftRightConstants andThen PropagateMiddleConstants/* andThen PropagateEquations*/)
+ loopUntilConvergence(simplifyProblem andThen noLeftRightConstants andThen PropagateMiddleConstants andThen PropagateEquations)
/** Solves the equation x1x2x3...xn = CONSTANT
diff --git a/src/test/scala/leon/integration/solvers/StringSolverSuite.scala b/src/test/scala/leon/integration/solvers/StringSolverSuite.scala
index bb99cbb64..d64df7f8c 100644
--- a/src/test/scala/leon/integration/solvers/StringSolverSuite.scala
+++ b/src/test/scala/leon/integration/solvers/StringSolverSuite.scala
@@ -184,7 +184,10 @@ class StringSolverSuite extends FunSuite with Matchers with ScalaFutures {
"""const8+const4+"12"+const5+const+"-1"+const1+const3+const2+const6+const9""" === "(12, -1)",
"""const8+const4+"1"+const5+const3+const6+const9""" === "(1)",
"""const8+const7+const9""" === "()")
- solve(problem) should not be 'empty
+ val solutions = solve(problem)
+ solutions should not be 'empty
+ val solution = solutions.head
+ errorcheck(problem, solution) should be(None)
}
test("ListInt as List(...)") {
@@ -221,10 +224,22 @@ T2: ret Pop() -> 5"""
test("SolvePropagateEquationProblem") {
implicit val idMap = MMap[String, Identifier]()
val problem = List(
- "a+b+c+d" === "1234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890",
- "k+a+b+c+d" === "212345678912345678901234567890123456789012345678912345678901234567890123456789012345678901234567891"
+ "a+b+c+d" === "1234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890",
+ "k+a+b+c+d" === "21234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567891"
+ )
+ val p = Future { solve(problem) }
+ assert(p.isReadyWithin(2 seconds), "Could not solve propagate")
+ p.futureValue should be('empty)
+ }
+
+ test("SolveRightCheckingProblem") {
+ implicit val idMap = MMap[String, Identifier]()
+ val problem = List(
+ "u+v+w+a+b+c+d" === "123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789",
+ "u+v+w+k+a+k+b+c+d" === "21234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567892"
)
val p = Future { solve(problem) }
assert(p.isReadyWithin(2 seconds), "Could not solve propagate")
+ p.futureValue should not be('empty)
}
}
\ No newline at end of file
--
GitLab