@AoKSolution
object Day10 {
    val machines = LineParser { line ->
        val parts = line.split(" ")
        val lights = parts.first().removeSurrounding("[", "]").reversed()
            .fold(0L) { acc, ch -> acc shl 1 or if (ch == '#') 1 else 0 }
        val buttons = parts.subList(1, parts.lastIndex)
            .map { s -> s.removeSurrounding("(", ")").splitInts(',').fold(0L) { acc, i -> acc or (1L shl i) } }
        val joltage = parts.last().removeSurrounding("{", "}").splitInts(',')
        Triple(lights, buttons, joltage)
    }

    context(_: PuzzleInput)
    fun part1() =
        machines().sumOf { (lights, buttons) -> bfs(0L, lights::equals) { buttons.map(it::xor) } }

    context(_: PuzzleInput)
    fun part2() =
        machines().sumOf { (_, buttons, joltages) ->
            withZ3 {
                val buttonPresses = buttons.withIndex().associate { (idx, button) -> button to mkIntConst("p$idx") }
                val totalPresses = mkAdd(*buttonPresses.values.toTypedArray())
                fun sumPresses(idx: Int) =
                    mkAdd(*buttonPresses.filterKeys { it ushr idx and 1L == 1L }.values.toTypedArray())

                minimizeInt(totalPresses) {
                    // such that each joltage is the sum of presses of matching buttons
                    for ((i, joltage) in joltages.withIndex()) Add(mkEq(sumPresses(i), mkInt(joltage)))
                    // and that all presses are non-negative
                    for (it in buttonPresses) Add(mkLe(mkInt(0), it.value))
                }
            }
        }

    inline fun <A> withZ3(f: Context.() -> A): A = Context().use { f(it) }
    inline fun Context.minimizeInt(target: Expr<IntSort>, constraints: Optimize.() -> Unit): Int = with(mkOptimize()) {
        val result = MkMinimize(target)
        constraints()
        check(Check() == Status.SATISFIABLE) { "constraints not satisfiable" }
        (result.value as IntNum).int
    }
}