2023-24 - Moved to external Z3

.github/workflows/scala2.yml

@@ -19,12 +19,17 @@ jobs:
 
     steps:
     - uses: actions/checkout@v3
+
     - name: Set up JDK 17
       uses: actions/setup-java@v3
       with:
         java-version: '17'
         distribution: 'temurin'
         cache: 'sbt'
+
+    - name: Install Z3
+      run: sudo apt-get update && sudo apt-get install -y z3
+
     - name: Run tests
       working-directory: ./scala2
       run: sbt test

scala2/src/main/scala/jurisk/adventofcode/y2018/Advent23.scala

@@ -11,6 +11,8 @@ import jurisk.optimization.Optimizer
 import jurisk.utils.FileInput._
 import jurisk.utils.Parsing.StringOps
 
+import scala.annotation.nowarn
+
 object Advent23 {
   type Input = List[Nanobot]
 
@@ -87,12 +89,17 @@ object Advent23 {
     val objective1 = maximize(nanobotsInRange)
     val objective2 = minimize(distanceFromOrigin)
 
+    @nowarn("cat=deprecation")
     val model = checkAndGetModel()
 
     println(model)
 
     val List(xc, yc, zc, nir, dor) =
-      List(x, y, z, nanobotsInRange, distanceFromOrigin).map(extractInt)
+      List(x, y, z, nanobotsInRange, distanceFromOrigin).map { v =>
+        @nowarn("cat=deprecation")
+        val result = extractInt(v)
+        result
+      }
 
     val found = Coords3D(xc, yc, zc)
     println(s"$found: nanobots in range: $nir, distance from origin: $dor")

scala2/src/main/scala/jurisk/adventofcode/y2022/Advent21.scala

@@ -184,10 +184,8 @@ object Advent21 {
       }
     }
 
-    val model = checkAndGetModel()
-    println(model)
-
-    extractLong(calculate.labeledInt)
+    val List(result) = runExternal(calculate)
+    resultToLong(result)
   }
 
   private def solvePart1Optimizer(

scala2/src/main/scala/jurisk/adventofcode/y2023/Advent16.scala

@@ -20,6 +20,7 @@ import jurisk.utils.Parsing.StringOps
 import jurisk.utils.Simulation
 import mouse.all.booleanSyntaxMouse
 
+import scala.annotation.nowarn
 import scala.collection.immutable.ArraySeq
 
 object Advent16 {
@@ -250,9 +251,9 @@ object Advent16 {
       println(s"Upper:\n${objective.getUpper}")
     }
 
-    val model = checkAndGetModel()
-
     if (debug) {
+      @nowarn("cat=deprecation")
+      val model = checkAndGetModel()
       println(s"Model:\n$model")
 
       val debugField = field
@@ -261,7 +262,10 @@ object Advent16 {
             val incoming = incomingBool(c, d)
             val outgoing = outgoingBool(c, d)
 
+            @nowarn("cat=deprecation")
             val incm = extractBoolean(incoming).getOrElse("Unknown".fail)
+
+            @nowarn("cat=deprecation")
             val outg = extractBoolean(outgoing).getOrElse("Unknown".fail)
 
             (incm, outg) match {
@@ -288,7 +292,8 @@ object Advent16 {
       Field2D.printCharField(debugField)
     }
 
-    extractLong(energizedVar)
+    val List(result) = runExternal("energized")
+    resultToLong(result)
   }
 
   private def edgeIncomings(

scala2/src/main/scala/jurisk/adventofcode/y2023/Advent24.scala

@@ -1,7 +1,6 @@
 package jurisk.adventofcode.y2023
 
 import cats.implicits._
-import com.microsoft.z3.Version
 import jurisk.geometry.Area2D
 import jurisk.geometry.Coordinates2D
 import jurisk.geometry.Coords3D
@@ -131,7 +130,6 @@ object Advent24 {
     (cp dotProduct pDiff) == 0
   }
 
-  // TODO: You can rewrite using determinants, possibly change the signature too
   private def vectorIntersection2D(
     a: PositionAndVelocity2D,
     b: PositionAndVelocity2D,
@@ -326,7 +324,6 @@ object Advent24 {
     println()
   }
 
-  // TODO: `z3-turnkey` doesn't work here, switch to the command line version
   def solvePart2Optimizer(
     data: List[PositionAndVelocity3D]
   ): PositionAndVelocity3D = {
@@ -340,8 +337,7 @@ object Advent24 {
     //    py + t[n] * vy == py[n] + t[n] * vy[n]
     //    pz + t[n] * vz == pz[n] + t[n] * vz[n]
 
-    implicit val o = Optimizer.z3()
-    println(Version.getFullVersion)
+    implicit val o: Optimizer = Optimizer.z3()
     import o._
 
     val px = o.labeledInt("px")
@@ -370,26 +366,13 @@ object Advent24 {
       )
     }
 
-    println(o.optimize)
-
-    println("""
-              |(echo "position:")
-              |(eval px) (eval py) (eval pz)
-              |
-              |(echo "velocity:")
-              |(eval vx) (eval vy) (eval vz)
-              |
-              |(echo "answer:")
-              |(eval (+ px py pz))
-              |""".stripMargin)
-
-    val model = o.checkAndGetModel()
-
-    println(model)
+    val List(pxS, pyS, pzS, vxS, vyS, vzS) = o
+      .runExternal("px", "py", "pz", "vx", "vy", "vz")
+      .map(r => resultToLong(r))
 
     val result = PositionAndVelocity3D(
-      Coords3D[Long](o.extractInt(px), o.extractInt(py), o.extractInt(pz)),
-      Coords3D[Long](o.extractInt(vx), o.extractInt(vy), o.extractInt(vz)),
+      Coords3D[Long](pxS, pyS, pzS),
+      Coords3D[Long](vxS, vyS, vzS),
     )
 
     println(result)

scala2/src/main/scala/jurisk/optimization/Optimizer.scala

@@ -17,8 +17,14 @@ import com.microsoft.z3.RealExpr
 import com.microsoft.z3.Sort
 import com.microsoft.z3.Status
 import com.microsoft.z3.enumerations.Z3_lbool
+import jurisk.process.Runner
 import jurisk.utils.Parsing.StringOps
+import org.scalatest.matchers.should.Matchers.convertToAnyShouldWrapper
 
+// The https://github.com/tudo-aqua/z3-turnkey distribution did not work on task 2023-24 while the same program
+// worked from the command line. Thus, some methods have ended up being deprecated, and this class is mostly
+// a way to generate SMT-LIB programs (see https://smtlib.cs.uiowa.edu/language.shtml).
+// TODO: Consider removing the Z3 dependency and just generating SMT-LIB format directly.
 trait Optimizer {
   val context: Context
   val optimize: Optimize
@@ -35,10 +41,13 @@ trait Optimizer {
 
   def addConstraints(expressions: Expr[BoolSort]*): Unit
 
-  // TODO:  Should probably discontinue this, at least deprecate, as it was not working well compared to the command
-  //        line version
+  @deprecated("Use `runExternal` instead", "2023-12-24")
   def checkAndGetModel(): Model
 
+  // TODO: Make type-safe?
+  def runExternal(evaluate: String*): List[String]
+  def resultToLong(result: String): Long
+
   def debugPrint(): Unit
 
   def maximize[R <: Sort](expr: Expr[R]): Optimize.Handle[R]
@@ -81,8 +90,13 @@ trait Optimizer {
   def and(expressions: Expr[BoolSort]*): BoolExpr
   def or(expressions: Expr[BoolSort]*): BoolExpr
 
+  @deprecated("Use `runExternal` instead", "2023-12-24")
   def extractBoolean(b: BoolExpr): Option[Boolean]
+
+  @deprecated("Use `runExternal` instead", "2023-12-24")
   def extractInt(n: IntExpr): Int
+
+  @deprecated("Use `runExternal` instead", "2023-12-24")
   def extractLong(n: IntExpr): Long
 }
 
@@ -152,6 +166,38 @@ private class Z3Optimizer(val context: Context, val optimize: Optimize)
     optimize.getModel
   }
 
+  def runExternal(evaluate: String*): List[String] = {
+    val debug = false
+
+    val programStart = optimize.toString
+
+    // Note - `get-value` is SMT-LIB spec, but `eval` works with Z3
+    val programEnd = evaluate
+      .map { what =>
+        s"(eval $what)"
+      }
+      .mkString("\n")
+
+    val program = s"$programStart\n$programEnd\n(exit)"
+
+    if (debug) println(program)
+
+    val results = Runner.runSync("z3", "-in")(program)
+
+    if (debug) println(results)
+
+    val lines = results.splitLines
+    lines.head.trim shouldEqual "sat"
+    lines.tail.size shouldEqual evaluate.length
+    lines.tail
+  }
+
+  def resultToLong(result: String): Long =
+    result.trim match {
+      case s"(- $n)" => -n.toLong
+      case other     => other.toLong
+    }
+
   def debugPrint(): Unit =
     println(optimize)
 

scala2/src/main/scala/jurisk/process/Runner.scala

@@ -0,0 +1,28 @@
+package jurisk.process
+
+import org.scalatest.matchers.should.Matchers.convertToAnyShouldWrapper
+
+import scala.io.Source
+import scala.sys.process.ProcessIO
+import scala.sys.process.stringSeqToProcess
+
+object Runner {
+  def runSync(command: String*)(input: String): String = {
+    val outputBuilder = new StringBuilder
+    val io            = new ProcessIO(
+      in => {
+        in.write(input.getBytes)
+        in.close()
+      },
+      out => {
+        val output = Source.fromInputStream(out).mkString
+        outputBuilder.append(output)
+        out.close()
+      },
+      _.close(),
+    )
+    val process       = command.run(io)
+    process.exitValue() shouldEqual 0
+    outputBuilder.toString()
+  }
+}

scala2/src/test/scala/jurisk/adventofcode/y2023/Advent24Spec.scala

@@ -45,14 +45,12 @@ class Advent24Spec extends AnyFreeSpec {
     }
   }
 
-  // TODO:  The embedded `z3-turnkey` seems to be broken as it is much slower than command line `z3`.
-  //        Switch to the command line one.
   "part 2 Z3" - {
-    "test optimizer" ignore {
+    "test optimizer" in {
       solvePart2Optimizer(testData) shouldEqual expectedTestAnswer
     }
 
-    "real optimizer" ignore {
+    "real optimizer" in {
       solvePart2Optimizer(realData) shouldEqual expectedRealAnswer
     }
   }