Move smartPos function to use it in Stainless + Portfolio solver fix

[jad-hamza]

I added a fix for https://github.com/epfl-lara/stainless/issues/980

I found these links that discuss behavior changes for Future.find, it's probably safer to implement our own: https://github.com/scala/bug/issues/11827 https://stackoverflow.com/questions/53759765/scala-future-find https://stackoverflow.com/questions/35961330/scala-future-list-first-completed-with-condition

However I'm not used to using Future or Promise, does the code look ok? @samarion @vkuncak I tested it on a small example and it seems to work well, and it also seems to fix the Stainless issue:

import scala.util._
import scala.concurrent._
import scala.concurrent.duration._
import scala.concurrent.ExecutionContext.Implicits.global

object Timeout {
  def findFirst[T](futures: Seq[Future[T]])(cond: T => Boolean): Option[T] = {
    val p = Promise[Option[T]]()
    val n = futures.length
    var i = 0

    for (future <- futures) {
      future.onComplete((result: Try[T]) => result match {
        case Success(res) if cond(res) =>
          p.trySuccess(Some(res))
        case _ =>
          synchronized { i += 1 }
          if (i == n) p.trySuccess(None)
      })
    }
    Await.result(p.future, Duration.Inf)
  }

  def main(args: Array[String]): Unit = {
    val times = Seq(4, 6, 10)
    val futures = times.map(i =>
      Future({
        println("waiting",i)
        Thread.sleep(i * 1000)
        println("waited i",i)
        i
      })
    )
    val res = findFirst(futures)(_ == 6)
    res match {
      case None => println("none")
      case Some(res) => println("result", res)
    }
  }
}

[samarion]

Looks reasonable to me. You might want to use an AtomicInteger instead of the synchronized block because it's immune to thread starvation deadlocks. Also maybe add a dedicated FutureUtils.scala file?

[jad-hamza]

Thanks I did the change. The StringSuite failed because I tried to change to CVC4 1.8, I reverted to 1.7 and restarted the build

[jad-hamza]

I moved CVC4 back to 1.8 for larabot, and added here some decoding for strings produced by CVC4 1.8, which contain characters of the form \u{ff} and u{f}.