Merge pull request #134 from jad-hamza/move-smartPos

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

Author: samarion

src/main/scala/inox/Reporter.scala

@@ -3,6 +3,7 @@
 package inox
 
 import utils._
+import Position.smartPos
 
 abstract class DebugSection(val name: String)
 
@@ -166,20 +167,6 @@ class DefaultReporter(debugSections: Set[DebugSection]) extends Reporter(debugSe
     case DEBUG(_) => "["+Console.MAGENTA          +" Debug  "+Console.RESET+"]"
   }
 
-  def smartPos(p: Position): String = {
-    if (p == NoPosition) {
-      ""
-    } else {
-      val target = p.file.getAbsolutePath()
-      val here   = new java.io.File(".").getAbsolutePath().stripSuffix(".")
-      val diff   = target.stripPrefix(here)
-
-      val filePos = diff+":"
-
-      filePos + p + ": "
-    }
-  }
-
   def emit(msg: Message) = synchronized {
     println(reline(severityToPrefix(msg.severity), smartPos(msg.position) + msg.msg.toString))
     printLineContent(msg.position, false)

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.FutureUtils.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/FutureUtils.scala

@@ -0,0 +1,30 @@
+/* Copyright 2009-2021 EPFL, Lausanne */
+
+package inox.utils
+
+import scala.util._
+import scala.concurrent._
+import scala.concurrent.duration._
+import scala.concurrent.ExecutionContext.Implicits.global
+import java.util.concurrent.atomic.AtomicInteger
+
+object FutureUtils {
+
+  def findFirst[T](futures: Seq[Future[T]])(cond: T => Boolean): Option[T] = {
+    val p = Promise[Option[T]]()
+    val n = futures.length
+    val i = new AtomicInteger(0)
+
+    for (future <- futures) {
+      future.onComplete((result: Try[T]) => result match {
+        case Success(res) if cond(res) =>
+          p.trySuccess(Some(res))
+        case _ =>
+          val finished = i.incrementAndGet()
+          if (finished == n) p.trySuccess(None)
+      })
+    }
+    Await.result(p.future, Duration.Inf)
+  }
+
+}

src/main/scala/inox/utils/Positions.scala

@@ -35,6 +35,21 @@ abstract class Position extends Ordered[Position] {
 }
 
 object Position {
+
+  def smartPos(p: Position): String = {
+    if (p == NoPosition) {
+      ""
+    } else {
+      val target = p.file.getAbsolutePath()
+      val here   = new java.io.File(".").getAbsolutePath().stripSuffix(".")
+      val diff   = target.stripPrefix(here)
+
+      val filePos = diff+":"
+
+      filePos + p + ": "
+    }
+  }
+
   def between(a: Position, b: Position): Position = {
     if (a.file == b.file) {
       if (a.line == b.line && a.col == b.col) {

src/main/scala/inox/utils/StringUtils.scala

@@ -17,15 +17,17 @@ object StringUtils {
   }
 
   def encodeByte(b: Byte): String = "\\x" + toHex((b >> 4) & 0xF) + toHex(b & 0xF)
-  def decodeHex(s: String): Byte = ((fromHex(s.charAt(2)) << 4) + fromHex(s.charAt(3))).toByte
+  def decodeHex(s: String): Byte = ((fromHex(s.charAt(0)) << 4) + fromHex(s.charAt(1))).toByte
 
   private val hex = """^\\x[0-9A-Fa-f]{2}""".r
+  private val uhex1 = """(?s)^\\u\{([0-9A-Fa-f])\}(.*)""".r
+  private val uhex2 = """(?s)^\\u\{([0-9A-Fa-f]{2})\}(.*)""".r
 
   object Hex {
     def unapply(s: String): Option[(Byte, String)] = {
       if (hex.findFirstIn(s).isDefined) {
         val (head, s2) = s.splitAt(4)
-        Some((decodeHex(head), s2))
+        Some((decodeHex(head.drop(2)), s2))
       } else {
         None
       }
@@ -44,6 +46,8 @@ object StringUtils {
   }
 
   def decode(s: String): String = if (s.isEmpty) s else (s match {
+    case uhex1(head, s2) => (fromHex(head.charAt(0)) & 0xF).toChar + decode(s2)
+    case uhex2(head, s2) => (decodeHex(head) & 0xFF).toChar + decode(s2)
     case JavaEncoded(b, s2) => (b & 0xFF).toChar + decode(s2)
     case _ => s.head + decode(s.tail)
   })

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

@@ -1,4 +1,4 @@
-/* Copyright 2009-2018 EPFL, Lausanne */
+/* Copyright 2009-2021 EPFL, Lausanne */
 
 package inox