diff --git a/.gitignore b/.gitignore index aeaf5ce..3fbe85e 100644 --- a/.gitignore +++ b/.gitignore @@ -20,3 +20,6 @@ imgui.log imgui.log.* imgui.log.lck replay_pid*.log + +/advents/z3/*.lib +/advents/z3/*.dll diff --git a/advents/build.gradle.kts b/advents/build.gradle.kts index d5b1f28..a6d2d5f 100644 --- a/advents/build.gradle.kts +++ b/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 { diff --git a/advents/src/main/kotlin/net/fish/maths/z3.kt b/advents/src/main/kotlin/net/fish/maths/z3.kt new file mode 100644 index 0000000..9f490dd --- /dev/null +++ b/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 +} + +class Z3Int( + override val ctx: Context, + override val expr: IntExpr, +) : Z3Expr + +class Z3ArithExpr( + override val ctx: Context, + override val expr: Expr +) : Z3Expr + +class Z3BoolExpr( + val ctx: Context, + val expr: Expr +) + +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) { + 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 z3(fn: Z3Context.() -> R): R { + return Context().use { + Z3Context(it).fn() + } +} \ No newline at end of file diff --git a/advents/src/main/kotlin/net/fish/y2023/Day24.kt b/advents/src/main/kotlin/net/fish/y2023/Day24.kt index 794e747..2e7a281 100644 --- a/advents/src/main/kotlin/net/fish/y2023/Day24.kt +++ b/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): HailstoneSim { @@ -151,8 +66,32 @@ object Day24 : Day { } fun doPart2(data: List): 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 diff --git a/advents/z3/README.md b/advents/z3/README.md new file mode 100644 index 0000000..9233bcb --- /dev/null +++ b/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) \ No newline at end of file diff --git a/advents/z3/com.microsoft.z3.jar b/advents/z3/com.microsoft.z3.jar new file mode 100644 index 0000000..b1f425b Binary files /dev/null and b/advents/z3/com.microsoft.z3.jar differ