Revert "Z3 implementation using ints"

This reverts commit 7024da9.

Author: peckb1

src/main/kotlin/me/peckb/aoc/_2025/calendar/day10/Day10.kt

@@ -1,80 +1,111 @@
 package me.peckb.aoc._2025.calendar.day10
 
-import com.microsoft.z3.ArithExpr
+import com.microsoft.z3.BitVecNum
+import com.microsoft.z3.BitVecSort
 import com.microsoft.z3.Context
-import com.microsoft.z3.IntExpr
-import com.microsoft.z3.IntNum
-import com.microsoft.z3.IntSort
+import com.microsoft.z3.Expr
+import com.microsoft.z3.Optimize
 import com.microsoft.z3.Status
 import javax.inject.Inject
 import me.peckb.aoc.generators.InputGenerator.InputGeneratorFactory
-import kotlin.collections.component1
-import kotlin.collections.component2
+import org.apache.commons.math3.stat.inference.TestUtils.g
 import kotlin.math.min
+import kotlin.use
 
 class Day10 @Inject constructor(
   private val generatorFactory: InputGeneratorFactory,
 ) {
   fun partOne(filename: String) = generatorFactory.forFile(filename).readAs(::day10) { input ->
-    input.sumOf { machine -> flipLights(machine.indicatorLights, machine.buttonSchematics) }
+    input.sumOf { machine ->
+       thing(".".repeat(machine.indicatorLights.length), machine.indicatorLights, machine.buttonSchematics)
+    }
   }
 
   fun partTwo(filename: String) = generatorFactory.forFile(filename).readAs(::day10) { input ->
-    input.sumOf { machine -> enableJoltages(machine) }
-  }
-
-  private fun enableJoltages(machine: Machine) : Int {
-    return Context().use { ctx ->
-      val opt = ctx.mkOptimize()
-
-      fun intVariableOf(name: String) = ctx.mkIntConst(name)
-
-      fun intValueOf(value: Int) = ctx.mkInt(value)
-
-      infix fun IntExpr.gte(t: IntExpr) = ctx.mkGe(this, t)
-
-      operator fun ArithExpr<IntSort>.plus(t: IntExpr) = ctx.mkAdd(this, t)
-
-      infix fun ArithExpr<IntSort>.equalTo(t: IntExpr) = ctx.mkEq(this, t)
-
-      fun List<IntExpr>.sum() = ctx.mkAdd(*this.toTypedArray())
-
-      val ZERO = intValueOf(0)
-
-      val affectedJoltages = mutableMapOf<Int, MutableList<IntExpr>>()
-      val buttonVariables = machine.buttonSchematics.mapIndexed { index, schematic ->
-        // create button variable
-        intVariableOf(index.toString()).also { buttonVariable ->
-          // track the joltages if affects
-          schematic.affectedIndices.forEach { affectedIndex ->
-            affectedJoltages.computeIfAbsent(affectedIndex) { _ -> mutableListOf() }.add(buttonVariable)
-          }
-          // add it to the optimizer
-          opt.Add(buttonVariable gte ZERO)
-        }
-      }
-
-      affectedJoltages.forEach { (joltageIndex, buttonsAffecting) ->
-        val targetValue = intValueOf(machine.joltages[joltageIndex])
-        val sumOfButtonPresses = buttonsAffecting.sum()
-        opt.Add(sumOfButtonPresses equalTo targetValue)
-      }
-
-      opt.MkMinimize(buttonVariables.sum())
-
-      val status = opt.Check()
-
-      if (status == Status.SATISFIABLE) {
-        val model = opt.getModel()
-        ((model.evaluate(buttonVariables.sum(), true) as IntNum).int)
-      } else {
-        throw IllegalStateException("No Solution Found")
+    input.sumOf { machine ->
+
+      Context().use { ctx ->
+        var bestFound = Int.MAX_VALUE
+
+        val bits = 64 // the answer will fit inside a long
+
+        fun valueOf(value: Int) = ctx.mkBV(value, bits)
+
+        fun variableOf(name: String) = ctx.mkBVConst(name, bits)
+
+        infix fun Expr<BitVecSort>.equalTo(t: Expr<BitVecSort>) = ctx.mkEq(this, t)
+
+        infix fun Expr<BitVecSort>.notEqual(t: Expr<BitVecSort>) = ctx.mkNot(this equalTo t)
+
+        operator fun Expr<BitVecSort>.plus(t: Expr<BitVecSort>) = ctx.mkBVAdd(this, t)
+
+        operator fun Expr<BitVecSort>.times(t: Expr<BitVecSort>) = ctx.mkBVMul(this, t)
+
+        infix fun Expr<BitVecSort>.lessThan(t: Expr<BitVecSort>) = ctx.mkBVSLT(this, t)
+
+        infix fun Expr<BitVecSort>.gte(t: Expr<BitVecSort>) = ctx.mkBVSGE(this, t)
+
+        val a = variableOf("a")
+        val b = variableOf("b")
+        val c = variableOf("c")
+        val d = variableOf("d")
+        val e = variableOf("e")
+        val f = variableOf("f")
+
+        val optimizer = ctx.mkOptimize()
+
+        optimizer.Add(e + f equalTo valueOf(3))
+        optimizer.Add(b + f equalTo valueOf(5))
+        optimizer.Add(c + d + e equalTo valueOf(4))
+        optimizer.Add(a + b + d equalTo valueOf(7))
+//        optimizer.Add(a lessThan valueOf(10000))
+//        optimizer.Add(b lessThan valueOf(10000))
+//        optimizer.Add(c lessThan valueOf(10000))
+//        optimizer.Add(d lessThan valueOf(10000))
+//        optimizer.Add(e lessThan valueOf(10000))
+//        optimizer.Add(f lessThan valueOf(10000))
+        optimizer.Add(a gte valueOf(0))
+        optimizer.Add(b gte valueOf(0))
+        optimizer.Add(c gte valueOf(0))
+        optimizer.Add(d gte valueOf(0))
+        optimizer.Add(e gte valueOf(0))
+        optimizer.Add(f gte valueOf(0))
+
+        optimizer.MkMinimize(a + b + c + d + e + f)
+
+        optimizer.Check()
+//        while(optimizer.Check() == Status.SATISFIABLE) {
+          val model = optimizer.model
+
+          val aEval = (model.evaluate(a, true) as BitVecNum)
+          val bEval = (model.evaluate(b, true) as BitVecNum)
+          val cEval = (model.evaluate(c, true) as BitVecNum)
+          val dEval = (model.evaluate(d, true) as BitVecNum)
+          val eEval = (model.evaluate(e, true) as BitVecNum)
+          val fEval = (model.evaluate(f, true) as BitVecNum)
+
+          bestFound = min(bestFound, aEval.int + bEval.int + cEval.int + dEval.int + eEval.int + fEval.int)
+
+//          optimizer.Add(
+//            ctx.mkOr(
+//            a notEqual aEval,
+//              b notEqual bEval,
+//              c notEqual cEval,
+//              d notEqual dEval,
+//              e notEqual eEval,
+//              f notEqual fEval,
+//            )
+//          )
+//        }
+//        println(bestFound)
+        bestFound
       }
     }
   }
 
-  fun flipLights(goal: String, buttonSchematics: List<ButtonSchematic>): Long {
-    val minPressesForState = mutableMapOf(".".repeat(goal.length) to 0L)
+
+  fun thing(current: String, goal: String, buttonSchematics: List<ButtonSchematic>): Long {
+    val minPressesForState = mutableMapOf(current to 0L)
     while(!minPressesForState.containsKey(goal)) {
       minPressesForState.entries.toList().forEach { (light, cost) ->
         val nextStates = possibleLights(light, buttonSchematics)
@@ -97,7 +128,7 @@ class Day10 @Inject constructor(
 
   private fun applyLightPress(current: String, buttonSchematic: ButtonSchematic): String {
     return current.mapIndexed { index, c ->
-      if (buttonSchematic.affectedIndices.contains(index)) {
+      if (buttonSchematic.lightsAffected.contains(index)) {
         if (c == '#') { '.' } else { '#' }
       } else { c }
     }.joinToString("")
@@ -122,4 +153,6 @@ data class Machine(
   val joltages: List<Int>,
 )
 
-data class ButtonSchematic(val affectedIndices: List<Int>)
+/** zero indexed */
+// TODO rename
+data class ButtonSchematic(val lightsAffected: List<Int>)

src/main/kotlin/me/peckb/aoc/_2025/calendar/day10/README.md

@@ -1 +1 @@
-## [Day 10: Factory](https://adventofcode.com/2025/day/10)
+## [](https://adventofcode.com/2025/day/10)

src/test/kotlin/me/peckb/aoc/_2025/calendar/day10/Day10Test.kt

@@ -23,7 +23,7 @@ internal class Day10Test {
 
   @Test
   fun testDay10PartTwo() {
-    assertEquals(19810, day10.partTwo(DAY_10))
+    assertEquals(-1, day10.partTwo(DAY_10))
   }
 
   companion object {