olveMinChange for StringSolver (incremental)

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

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