Fix issue where portfolio solver waits for all solvers

Author: jad-hamza

src/main/scala/inox/solvers/combinators/PortfolioSolver.scala

@@ -58,11 +58,7 @@ trait PortfolioSolver extends Solver { self =>
       }
     }
 
-    tasks = Future.sequence(fs).map(_ => ())
-
-    val result = Future.find(fs.toList)(_._2 != Unknown)
-
-    val res = Await.result(result, Duration.Inf) match {
+    inox.utils.findFirst(fs)(_._2 != Unknown) match {
       case Some((s, r)) =>
         resultSolver = s.getResultSolver
         resultSolver.foreach { solv =>
@@ -72,14 +68,13 @@ trait PortfolioSolver extends Solver { self =>
         r
       case None =>
         reporter.debug("No solver succeeded")
-        //fs.foreach(f => println(f.value))
         config.cast(Unknown)
     }
 
     // TODO: Decide if we really want to wait for all the solvers.
     // I understand we interrupt them, but what if one gets stuck
     // fs foreach { Await.ready(_, Duration.Inf) }
-    res
+    // res
   }
 
 

src/main/scala/inox/utils/package.scala

@@ -1,7 +1,12 @@
-/* Copyright 2009-2018 EPFL, Lausanne */
+/* Copyright 2009-2021 EPFL, Lausanne */
 
 package inox
 
+import scala.util._
+import scala.concurrent._
+import scala.concurrent.duration._
+import scala.concurrent.ExecutionContext.Implicits.global
+
 /** Various utilities used throughout the Inox system */
 package object utils {
 
@@ -26,5 +31,22 @@ package object utils {
     }
     v2
   }
-  
+
+  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)
+  }
+
 }