From 08a4c48c46fcad47459e2c41ad54bf9a07fd2354 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <mikael.mayer@epfl.ch>
Date: Thu, 21 Apr 2016 11:16:48 +0200
Subject: [PATCH] olveMinChange for StringSolver (incremental)
---
.../leon/solvers/string/StringSolver.scala | 28 +++++++++++++++++++
.../solvers/StringSolverSuite.scala | 17 +++++++++++
2 files changed, 45 insertions(+)
diff --git a/src/main/scala/leon/solvers/string/StringSolver.scala b/src/main/scala/leon/solvers/string/StringSolver.scala
index bc9ee8419..b717cccf5 100644
--- a/src/main/scala/leon/solvers/string/StringSolver.scala
+++ b/src/main/scala/leon/solvers/string/StringSolver.scala
@@ -628,4 +628,32 @@ object StringSolver {
solveGeneralProblem(unbounded.map(reduceGeneralEquation(assignment)(_))).map(assignment ++ _)
})
}
+
+
+ ////////////////////////////////////////////////
+ //// Incremental problem extension ////
+ ////////////////////////////////////////////////
+
+ /** Returns all subsets of i elements of a sequence. */
+ def take[A](i: Int, of: Seq[A]): Stream[Seq[A]] = {
+ if(i > of.size || i < 0) Stream.empty
+ if(i == of.size) Stream(of)
+ else if(i == 0) Stream(Seq.empty)
+ else {
+ take(i - 1, of.tail).map(of.head +: _) #::: take(i, of.tail)
+ }
+ }
+
+ /** Solves the problem while supposing that a minimal number of variables have been changed.*/
+ def solveMinChange(p: Problem, initialMapping: Assignment): Stream[Assignment] = {
+ // First try to see if the problem is solved. If yes, returns the initial mapping
+ val initKeys = initialMapping.keys.toSeq
+ for{
+ i <- (initialMapping.size to 0 by -1).toStream
+ kept <- take(i, initKeys)
+ ifKept = kept.toSet
+ newProblem = reduceProblem(initialMapping filterKeys ifKept)(p)
+ solution <- solve(newProblem)
+ } yield solution
+ }
}
\ No newline at end of file
diff --git a/src/test/scala/leon/integration/solvers/StringSolverSuite.scala b/src/test/scala/leon/integration/solvers/StringSolverSuite.scala
index 029bfb233..6faad419e 100644
--- a/src/test/scala/leon/integration/solvers/StringSolverSuite.scala
+++ b/src/test/scala/leon/integration/solvers/StringSolverSuite.scala
@@ -242,4 +242,21 @@ T2: ret Pop() -> 5"""
assert(p.isReadyWithin(2 seconds), "Could not solve propagate")
p.futureValue should not be('empty)
}
+
+ test("solveMinChange") {
+ implicit val idMap = MMap[String, Identifier]()
+ val problem = List(
+ "u+v+w" === "akbc"
+ )
+ val u = idMap("u")
+ val v = idMap("v")
+ val w = idMap("w")
+ val solutions = solveMinChange(problem, Map(u -> "a", v -> "b", w -> "c"))
+ solutions(0) should equal (Map(v -> "kb"))
+ solutions(1) should equal (Map(u -> "ak"))
+ (2 to 5).toSet.map((i: Int) => solutions(i)) should equal (Set(Map(v -> "", w -> "kbc")
+ , Map(v -> "k", w -> "bc")
+ , Map(v -> "kb", w -> "c")
+ , Map(v -> "kbc", w -> "")))
+ }
}
\ No newline at end of file
--
GitLab