2023 Day 24 P2 with z3 library

.gitignore

@@ -20,3 +20,6 @@ imgui.log
 imgui.log.*
 imgui.log.lck
 replay_pid*.log
+
+/advents/z3/*.lib
+/advents/z3/*.dll

advents/build.gradle.kts

@@ -60,7 +60,7 @@ dependencies {
     testImplementation("io.mockk:mockk:$mockkVersion")
     testImplementation("org.junit.jupiter:junit-jupiter:5.8.1")
 
-    //implementation(rootProject.files("z3/com.microsoft.z3.jar"))
+    implementation(rootProject.files("advents/z3/com.microsoft.z3.jar"))
 }
 
 kotlin {

advents/src/main/kotlin/net/fish/maths/z3.kt

@@ -0,0 +1,108 @@
+package net.fish.maths
+
+import com.microsoft.z3.ArithSort
+import com.microsoft.z3.BoolSort
+import com.microsoft.z3.Context
+import com.microsoft.z3.Expr
+import com.microsoft.z3.IntExpr
+import com.microsoft.z3.Model
+import com.microsoft.z3.Status
+
+interface Z3Expr {
+    val ctx: Context
+    val expr: Expr<out ArithSort>
+}
+
+class Z3Int(
+    override val ctx: Context,
+    override val expr: IntExpr,
+) : Z3Expr
+
+class Z3ArithExpr(
+    override val ctx: Context,
+    override val expr: Expr<out ArithSort>
+) : Z3Expr
+
+class Z3BoolExpr(
+    val ctx: Context,
+    val expr: Expr<BoolSort>
+)
+
+operator fun Z3Expr.minus(other: Long): Z3Expr {
+    return Z3ArithExpr(ctx, ctx.mkSub(expr, ctx.mkInt(other)))
+}
+
+operator fun Long.minus(other: Z3Expr): Z3Expr {
+    return Z3ArithExpr(other.ctx, other.ctx.mkSub(other.ctx.mkInt(this), other.expr))
+}
+
+operator fun Z3Expr.minus(other: Z3Expr): Z3Expr {
+    return Z3ArithExpr(other.ctx, other.ctx.mkSub(expr, other.expr))
+}
+
+operator fun Z3Expr.plus(other: Long): Z3Expr {
+    return Z3ArithExpr(ctx, ctx.mkAdd(expr, ctx.mkInt(other)))
+}
+
+operator fun Long.plus(other: Z3Expr): Z3Expr {
+    return Z3ArithExpr(other.ctx, other.ctx.mkAdd(other.ctx.mkInt(this), other.expr))
+}
+
+operator fun Z3Expr.plus(other: Z3Expr): Z3Expr {
+    return Z3ArithExpr(ctx, ctx.mkAdd(expr, other.expr))
+}
+
+operator fun Z3Expr.times(other: Long): Z3Expr {
+    return Z3ArithExpr(ctx, ctx.mkMul(expr, ctx.mkInt(other)))
+}
+
+operator fun Long.times(other: Z3Expr): Z3Expr {
+    return Z3ArithExpr(other.ctx, other.ctx.mkMul(other.ctx.mkInt(this), other.expr))
+}
+
+operator fun Z3Expr.times(other: Z3Expr): Z3Expr {
+    return Z3ArithExpr(ctx, ctx.mkMul(expr, other.expr))
+}
+
+operator fun Z3Expr.div(other: Long): Z3Expr {
+    return Z3ArithExpr(ctx, ctx.mkDiv(expr, ctx.mkInt(other)))
+}
+
+operator fun Long.div(other: Z3Expr): Z3Expr {
+    return Z3ArithExpr(other.ctx, other.ctx.mkDiv(other.ctx.mkInt(this), other.expr))
+}
+
+operator fun Z3Expr.div(other: Z3Expr): Z3Expr {
+    return Z3ArithExpr(other.ctx, other.ctx.mkDiv(expr, other.expr))
+}
+
+infix fun Z3Expr.eq(other: Z3Expr): Z3BoolExpr {
+    return Z3BoolExpr(ctx, ctx.mkEq(this.expr, other.expr))
+}
+
+class Z3Context(private val ctx: Context) {
+    lateinit var model: Model
+
+    fun int(name: String) = Z3Int(ctx, ctx.mkIntConst(name))
+
+    fun solve(equations: List<Z3BoolExpr>) {
+        val solver = ctx.mkSolver()
+        solver.add(*equations.map { it.expr }.toTypedArray())
+
+        require(solver.check() == Status.SATISFIABLE) {
+            "Equation set not satisfiable"
+        }
+
+        this.model = solver.model
+    }
+
+    fun eval(expr: Z3Expr): String {
+        return model.eval(expr.expr, true).toString()
+    }
+}
+
+fun <R> z3(fn: Z3Context.() -> R): R {
+    return Context().use {
+        Z3Context(it).fn()
+    }
+}

advents/src/main/kotlin/net/fish/y2023/Day24.kt

@@ -3,6 +3,11 @@ package net.fish.y2023
 import kotlin.math.min
 import net.fish.Day
 import net.fish.maths.combinations
+import net.fish.maths.eq
+import net.fish.maths.minus
+import net.fish.maths.plus
+import net.fish.maths.times
+import net.fish.maths.z3
 import net.fish.resourceLines
 import org.joml.Intersectiond
 import org.joml.Vector2d
@@ -13,46 +18,20 @@ object Day24 : Day {
     private val data by lazy { resourceLines(2023, 24) }
 
     override fun part1() = doPart1(data, 200000000000000L, 400000000000000L)
-    // TBD: override fun part2() = doPart2(data)
-    override fun part2() = 558415252330828L
+    override fun part2() = 558415252330828L // takes a couple of seconds: doPart2(data)
 
     data class Hailstone(val p: Vector3d, val v: Vector3d) {
-        var axis = Vector3d()
         fun doesIntersectXYInPositiveTime(other: Hailstone, intersection: Vector2d): Boolean {
             val intersects = Intersectiond.intersectLineLine(
                 p.x, p.y, p.x + v.x, p.y + v.y,
                 other.p.x, other.p.y, other.p.x + other.v.x, other.p.y + other.v.y,
                 intersection
             )
-            val t = if (!intersects) -1.0 else {
+            return if (!intersects) false else {
                 val tH1 = (intersection.x - p.x) / v.x
                 val tH2 = (intersection.x - other.p.x) / other.v.x
-                min(tH1, tH2)
+                min(tH1, tH2) > 0
             }
-            return t > 0
-        }
-
-        fun adjust(a: Vector3d) {
-            v.x -= a.x - axis.x
-            v.y -= a.y - axis.y
-            v.z -= a.z - axis.z
-            axis = a
-        }
-
-        fun intersectTime(other: Vector2d): Double {
-            if (v.x == 0.0 && v.y == 0.0) throw Exception("No time possible for $this with $other")
-            val t = if (v.x == 0.0) (other.y - p.y) / v.y else (other.x - p.x) / v.x
-            //println("intersectTime for self: $this, other: $other = $t")
-            return t
-        }
-
-        fun getZ(other: Hailstone, intersection: Vector2d): Double? {
-            val tS = intersectTime(intersection)
-            val tO = other.intersectTime(intersection)
-            return if (tS == tO) {
-                assert(p.z + tS * v.z == other.p.z + tO * other.v.z)
-                null
-            } else (p.z - other.p.z + tS * v.z - tO * other.v.z) / (tS - tO)
         }
 
         override fun toString(): String {
@@ -66,74 +45,10 @@ object Day24 : Day {
                 val intersection = Vector2d()
                 val t = pair[0].doesIntersectXYInPositiveTime(pair[1], intersection)
                 val intersectInRegion = t && (intersection.x >= minXY && intersection.x <= maxXY) && (intersection.y >= minXY && intersection.y <= maxXY)
-                // println("($p1, $d1), ($p2, $d2) : $intersectInRegion at $p, t: $t")
                 total + if (intersectInRegion) 1 else 0
             }
         }
 
-        fun findStartOfAllIntersection(): Vector3d {
-            var n = 0
-            while(true) {
-                // println("NEW LOOP")
-                for (x in 0..n) {
-                    val y = n - x
-                    for (negX in listOf(-1, 1)) {
-                        for (negY in listOf(-1, 1)) {
-                            val aX = x * negX
-                            val aY = y * negY
-                            // println("checking v=<$aX,$aY,?>")
-                            var h1 = hailstones[0]
-                            val adjust = Vector3d(aX.toDouble(), aY.toDouble(), 0.0)
-                            h1.adjust(adjust)
-                            var intersection: Vector2d? = null
-                            var doesIntersect = false
-                            val p = Vector2d()
-                            //println("comparing v $h1")
-                            for (h2 in hailstones.subList(1, hailstones.size)) {
-                                h2.adjust(adjust)
-                                doesIntersect = h1.doesIntersectXYInPositiveTime(h2, p)
-                                //println("p: $p, inter: $intersection")
-                                if (!doesIntersect) {
-                                    //println("v $h2 - NONE (!doesIntersect)")
-                                    break
-                                }
-                                if (intersection == null) {
-                                    //println("v $h2 setting to $p")
-                                    intersection = Vector2d(p)
-                                    continue
-                                }
-                                if (p != intersection) {
-                                    //println("v $h2 - NOT SAME $p")
-                                    break
-                                }
-                                //println("v $h2 - continuing $p")
-                            }
-                            if (!doesIntersect || p != intersection) {
-                                continue
-                            }
-                            var aZ: Double? = null
-                            h1 = hailstones[0]
-                            for (h2 in hailstones.subList(1, hailstones.size)) {
-                                val nZ = h1.getZ(h2, intersection)
-                                if (aZ == null) {
-                                    aZ = nZ
-                                    continue
-                                } else if (nZ != aZ) {
-                                    throw Exception("invalidated by $nZ from $h1")
-                                }
-                            }
-                            if (aZ != null) {
-                                val h1 = hailstones[0]
-                                val z = h1.p.z + h1.intersectTime(intersection) * (h1.v.z - aZ)
-                                //println("start: (${intersection.x}, ${intersection.y}, $z)")
-                                return Vector3d(intersection.x, intersection.y, z)
-                            }
-                        }
-                    }
-                }
-                n += 1
-            }
-        }
     }
 
     fun toHailstoneSimulator(data: List<String>): HailstoneSim {
@@ -151,8 +66,32 @@ object Day24 : Day {
     }
     fun doPart2(data: List<String>): Long {
         val sim = toHailstoneSimulator(data)
-        val start = sim.findStartOfAllIntersection()
-        return (start.x + start.y + start.z).toLong()
+        return z3 {
+            val x_t = int("x_t")
+            val y_t = int("y_t")
+            val z_t = int("z_t")
+            val xvel_t = int("xvel_t")
+            val yvel_t = int("yvel_t")
+            val zvel_t = int("zvel_t")
+            val dt1 = int("dt1")
+            val dt2 = int("dt2")
+            val dt3 = int("dt3")
+
+            val dt = listOf(dt1, dt2, dt3)
+
+
+            val eqs = sim.hailstones.take(3).flatMapIndexed { idx, hs ->
+                listOf(
+                    (x_t - hs.p.x.toLong()) eq (dt[idx] * (hs.v.x.toLong() - xvel_t)),
+                    (y_t - hs.p.y.toLong()) eq (dt[idx] * (hs.v.y.toLong() - yvel_t)),
+                    (z_t - hs.p.z.toLong()) eq (dt[idx] * (hs.v.z.toLong() - zvel_t)),
+                )
+            }
+
+            solve(eqs)
+
+            eval(x_t + y_t + z_t).toLong()
+        }
     }
 
     @JvmStatic

advents/z3/README.md

@@ -0,0 +1,12 @@
+Add Z3 java bindings here.
+Obtained from [https://github.com/Z3Prover/z3/releases](https://github.com/Z3Prover/z3/releases).
+
+Files needed:
+
+- `com.microsoft.z3.jar`
+- `libz3.dll`
+- `libz3.lib`
+- `libz3java.dll`
+- `libz3java.lib`
+
+Copy them to a system directory (e.g. c:\msys64\usr\local\bin in this project)