Day 24 2023 (#254)

* Day 24 2023

* variable rename

* newline

build.gradle.kts

@@ -32,6 +32,7 @@ dependencies {
     implementation("org.apache.commons:commons-geometry-core:1.0")
     implementation("org.apache.commons:commons-geometry-euclidean:1.0")
     implementation("org.jetbrains.kotlinx:kotlinx-coroutines-core:1.7.3")
+    implementation("tools.aqua:z3-turnkey:4.12.2.1")
 
     // used for generating skeletons
     implementation("com.squareup:kotlinpoet:1.15.3")

src/main/kotlin/me/peckb/aoc/_2023/calendar/day24/Day24.kt

@@ -0,0 +1,106 @@
+package me.peckb.aoc._2023.calendar.day24
+
+import com.microsoft.z3.*
+import me.peckb.aoc.generators.CombinationsGenerator
+import javax.inject.Inject
+import me.peckb.aoc.generators.InputGenerator.InputGeneratorFactory
+import org.apache.commons.geometry.euclidean.threed.Vector3D
+import org.apache.commons.geometry.euclidean.twod.*
+import org.apache.commons.numbers.core.Precision
+
+class Day24 @Inject constructor(
+  private val generatorFactory: InputGeneratorFactory,
+) {
+  fun partOne(filename: String) = generatorFactory.forFile(filename).readAs(::hailstone) { input ->
+    val hail = input.toList().toTypedArray()
+
+    val combinations = CombinationsGenerator.findCombinations(hail, 2)
+
+    val min = 200000000000000.0
+    val max = 400000000000000.0
+    val range = min .. max
+
+    combinations.count { (hailA, hailB) ->
+      hailA.intersect2D(hailB)?.let {
+        hailA.isFutureValue(it.x) && hailB.isFutureValue(it.x) && range.contains(it.x) && range.contains(it.y)
+      } ?: false
+    }
+  }
+
+  fun partTwo(filename: String) = generatorFactory.forFile(filename).readAs(::hailstone) { input ->
+    val ctx = Context()
+    val solver = ctx.mkSolver()
+
+    val longType = ctx.mkBitVecSort(64)
+
+    fun variableOf(name: String) = ctx.mkConst(name, longType)
+
+    fun valueOf(value: Long) = ctx.mkNumeral(value, longType)
+
+    operator fun Expr<BitVecSort>.times(t: Expr<BitVecSort>) = ctx.mkBVMul(this, t)
+
+    operator fun Expr<BitVecSort>.plus(t: Expr<BitVecSort>) = ctx.mkBVAdd(this, t)
+
+    val zero = valueOf(0)
+
+    val x = variableOf("x")
+    val y = variableOf("y")
+    val z = variableOf("z")
+    val dx = variableOf("dx")
+    val dy = variableOf("dy")
+    val dz = variableOf("dz")
+
+    input.take(3).forEachIndexed { index, hail ->
+      val t = variableOf("t_$index")
+
+      val posX = valueOf(hail.position.x.toLong())
+      val posY = valueOf(hail.position.y.toLong())
+      val posZ = valueOf(hail.position.z.toLong())
+
+      val velX = valueOf(hail.velocity.x.toLong())
+      val velY = valueOf(hail.velocity.y.toLong())
+      val velZ = valueOf(hail.velocity.z.toLong())
+
+      solver.add(ctx.mkBVSGT(t, zero))
+      solver.add(ctx.mkEq(x + dx * t, posX + velX * t))
+      solver.add(ctx.mkEq(y + dy * t, posY + velY * t))
+      solver.add(ctx.mkEq(z + dz * t, posZ + velZ * t))
+    }
+
+    solver.check()
+    val model = solver.model
+
+    val xEval = model.eval(x, true)
+    val yEval = model.eval(y, true)
+    val zEval = model.eval(z, true)
+
+    (xEval as BitVecNum).long + (yEval as BitVecNum).long + (zEval as BitVecNum).long
+  }
+
+  private fun hailstone(line: String) : Hailstone {
+    return line.split(" @ ").let { (pos, vel) ->
+      val (x, y, z) = pos.split(", ").map { it.trim().toDouble() }
+      val (dx, dy, dz) = vel.split(", ").map { it.trim().toDouble() }
+
+      Hailstone(Vector3D.of(x, y, z), Vector3D.of(dx, dy, dz))
+    }
+  }
+
+  data class Hailstone(val position: Vector3D, val velocity: Vector3D) {
+    fun intersect2D(hailB: Hailstone): Vector2D? {
+      return line2D.intersection(hailB.line2D)
+    }
+
+    private val line2D by lazy {
+      Lines.fromPointAndDirection(
+        Vector2D.of(position.x, position.y),
+        Vector2D.of(velocity.x, velocity.y),
+        Precision.doubleEquivalenceOfEpsilon(1e-14)
+      )
+    }
+
+    fun isFutureValue(x: Double): Boolean {
+      return !(velocity.x < 0.0 && x > position.x || velocity.x > 0.0 && x < position.x)
+    }
+  }
+}

src/main/kotlin/me/peckb/aoc/_2023/calendar/day24/README.md

@@ -0,0 +1 @@
+## [Day 24: Never Tell Me The Odds](https://adventofcode.com/2023/day/24)

src/main/kotlin/me/peckb/aoc/generators/CombinationsGenerator.kt

@@ -28,7 +28,7 @@ internal object CombinationsGenerator {
     }
   }
 
-  fun <T> findCombinations(A: Array<T>, k: Int): Set<List<T>?> {
+  fun <T> findCombinations(A: Array<T>, k: Int): Set<List<T>> {
     val subarrays: MutableSet<List<T>> = HashSet()
     findCombinations(A, 0, k, subarrays, ArrayList())
     return subarrays

src/main/kotlin/me/peckb/aoc/generators/skeleton/DayClass.kt

@@ -65,11 +65,17 @@ object DayClass {
     file.writeTo(File(SRC_DIRECTORY))
 
     // remove all the extraneous `public` modifiers
+    // and the extraneous (and incorrect) `Unit` return types
     // and the safety import of `kotlin.String`
+    // and the safety import of `kotlin.Unit`
     val path = Paths.get("$SRC_DIRECTORY/me/peckb/aoc/_$year/calendar/day$day/Day$day.kt")
     val content = String(Files.readAllBytes(path))
       .replace("public ".toRegex(), "")
-      .replace("import kotlin.String".toRegex(), "")
+      .replace(": Unit".toRegex(), "")
+      .split("\n")
+      .filterNot { it == "import kotlin.String" }
+      .filterNot { it == "import kotlin.Unit" }
+      .joinToString("\n")
     Files.write(path, content.toByteArray())
   }
 }

src/test/kotlin/me/peckb/aoc/_2023/TestDayComponent.kt

@@ -23,6 +23,7 @@ import me.peckb.aoc._2023.calendar.day20.Day20Test
 import me.peckb.aoc._2023.calendar.day21.Day21Test
 import me.peckb.aoc._2023.calendar.day22.Day22Test
 import me.peckb.aoc._2023.calendar.day23.Day23Test
+import me.peckb.aoc._2023.calendar.day24.Day24Test
 import javax.inject.Singleton
 
 import me.peckb.aoc.DayComponent
@@ -55,4 +56,5 @@ internal interface TestDayComponent : DayComponent {
   fun inject(day21Test: Day21Test)
   fun inject(day22Test: Day22Test)
   fun inject(day23Test: Day23Test)
+  fun inject(day24Test: Day24Test)
 }

src/test/kotlin/me/peckb/aoc/_2023/calendar/day24/Day24Test.kt

@@ -0,0 +1,32 @@
+package me.peckb.aoc._2023.calendar.day24
+
+import javax.inject.Inject
+
+import me.peckb.aoc._2023.DaggerTestDayComponent
+import org.junit.jupiter.api.Assertions.assertEquals
+import org.junit.jupiter.api.BeforeEach
+import org.junit.jupiter.api.Test
+
+internal class Day24Test {
+  @Inject
+  lateinit var day24: Day24
+
+  @BeforeEach
+  fun setup() {
+    DaggerTestDayComponent.create().inject(this)
+  }
+
+  @Test
+  fun testDay24PartOne() {
+    assertEquals(17244, day24.partOne(DAY_24))
+  }
+
+  @Test
+  fun testDay24PartTwo() {
+    assertEquals(1025019997186820, day24.partTwo(DAY_24))
+  }
+
+  companion object {
+    private const val DAY_24: String = "advent-of-code-input/2023/day24.input"
+  }
+}