@@ -7,30 +7,24 @@ import scala.jdk.CollectionConverters.*
77
88object Day17 {
99
10- case class Registers (a : Int , b : Int , c : Int )
10+ case class Registers (a : Long , b : Long , c : Long ) // Long registers for simulating part 2
1111
12- type Program = Seq [Int ]
12+ type Program = Seq [Byte ]
1313
1414 case class Input (registers : Registers , program : Program )
1515
16- def runOutput0 (input : Input ): Seq [Int ] = {
17- val Input (registers, program) = input
16+ def runOutputs (registers : Registers , program : Program ): LazyList [Byte ] = {
1817
19- def helper (ip : Int , registers : Registers ): LazyList [Int ] = {
20- // println(ip)
21- // println(registers)
18+ def helper (ip : Int , registers : Registers ): LazyList [Byte ] = {
2219
23- def combo (operand : Int ): Int = operand match {
20+ def combo (operand : Byte ): Long = operand match {
2421 case 0 | 1 | 2 | 3 => operand
2522 case 4 => registers.a
2623 case 5 => registers.b
2724 case 6 => registers.c
2825 case 7 => throw new IllegalArgumentException (" illegal combo operand" )
2926 }
3027
31- // 0, 5, 3
32- // 2 1 7 4
33-
3428 if (program.indices.contains(ip)) {
3529 lazy val literalOperand = program(ip + 1 )
3630 lazy val comboOperand = combo(literalOperand)
@@ -48,7 +42,7 @@ object Day17 {
4842 case 4 => // bxc
4943 helper(ip + 2 , registers.copy(b = registers.b ^ registers.c))
5044 case 5 => // out
51- (comboOperand & 0b111 ) #:: helper(ip + 2 , registers)
45+ (comboOperand & 0b111 ).toByte #:: helper(ip + 2 , registers)
5246 case 6 => // bdv
5347 // helper(ip + 2, registers.copy(b = registers.a / (1 << comboOperand)))
5448 helper(ip + 2 , registers.copy(b = registers.a >> comboOperand))
@@ -65,22 +59,24 @@ object Day17 {
6559 helper(0 , registers)
6660 }
6761
68- def runOutput (input : Input ): String = runOutput0(input).mkString(" ," )
62+ def runOutputsString (input : Input ): String =
63+ runOutputs(input.registers, input.program).mkString(" ," )
6964
7065 trait Part2Solution {
7166 def findQuineA (input : Input ): Long
7267 }
7368
7469 object NaivePart2Solution extends Part2Solution {
7570 override def findQuineA (input : Input ): Long = {
71+ val Input (registers, program) = input
7672 Iterator .from(0 )
77- .find(newA => runOutput0( Input (input. registers.copy(a = newA), input. program)) == input. program)
73+ .find(newA => runOutputs( registers.copy(a = newA), program) == program) // TODO: does equality check stop running on first mismatch?
7874 .get
7975 }
8076 }
8177
8278 object SemiNaivePart2Solution extends Part2Solution {
83- def myProg (initialA : Int , expectedOutputs : Iterator [Int ]): Boolean = {
79+ def myProg (initialA : Int , expectedOutputs : Iterator [Byte ]): Boolean = {
8480 var a : Int = initialA
8581 var b : Int = 0
8682 var c : Int = 0
@@ -106,14 +102,15 @@ object Day17 {
106102
107103 object ReverseEngineeredZ3Part2Solution extends Part2Solution {
108104 override def findQuineA (input : Input ): Long = {
109- val Seq (2 ,4 , 1 , bxl1,7 , 5 , 1 , bxl2,4 , 5 , 0 , 3 , 5 , 5 , 3 , 0 ) = input.program
105+ val Seq (2 , 4 , 1 , bxl1, 7 , 5 , 1 , bxl2, 4 , 5 , 0 , 3 , 5 , 5 , 3 , 0 ) = input.program // TODO: doesn't support other orders of some operations
110106
111107 val ctx = new Context (Map (" model" -> " true" ).asJava)
112108 import ctx ._
113- val s = mkSolver ()
109+ val s = mkOptimize ()
114110
115111 val bits = input.program.size * 3
116112 val initialA = mkBVConst(" initialA" , bits)
113+ s.MkMinimize (initialA)
117114
118115 for ((instruction, i) <- input.program.zipWithIndex) {
119116 val a = mkBVLSHR(initialA, mkBV(i * 3 , bits))
@@ -123,11 +120,10 @@ object Day17 {
123120 b = mkBVXOR(b, mkBV(bxl2, bits))
124121 b = mkBVXOR(b, c)
125122 val out = mkBVAND(b, mkBV(0b111 , bits))
126- s.add (mkEq(out, mkBV(instruction, bits)))
123+ s.Add (mkEq(out, mkBV(instruction, bits)))
127124 }
128125
129- assert(s.check() == Status .SATISFIABLE )
130- // TODO: minimize
126+ assert(s.Check () == Status .SATISFIABLE )
131127 s.getModel.evaluate(initialA, false ).toString.toLong
132128 }
133129 }
@@ -137,22 +133,22 @@ object Day17 {
137133 */
138134 object GenericZ3Part2Solution extends Part2Solution {
139135 override def findQuineA (input : Input ): Long = {
136+ val Input (registers, program) = input
137+
140138 val ctx = new Context (Map (" model" -> " true" ).asJava)
141139 import ctx ._
142140 val s = mkOptimize()
143141
144142 case class Registers (a : BitVecExpr , b : BitVecExpr , c : BitVecExpr )
145143
146- val Input (registers, program) = input
147144 val bits = input.program.size * 3
148-
149145 val zeroBV = mkBV(0 , bits)
150146 val threeBitBV = mkBV(0b111 , bits)
151147
152148 // copied & modified from part 1
153- def helper (ip : Int , registers : Registers , expectedOutputs : List [Int ]): BoolExpr = {
149+ def helper (ip : Int , registers : Registers , expectedOutputs : List [Byte ]): BoolExpr = {
154150
155- def combo (operand : Int ): BitVecExpr = operand match {
151+ def combo (operand : Byte ): BitVecExpr = operand match {
156152 case 0 | 1 | 2 | 3 => mkBV(operand, bits)
157153 case 4 => registers.a
158154 case 5 => registers.b
@@ -180,7 +176,7 @@ object Day17 {
180176 helper(ip + 2 , registers.copy(b = mkBVXOR(registers.b, registers.c)), expectedOutputs)
181177 case 5 => // out
182178 expectedOutputs match {
183- case Nil => mkFalse()
179+ case Nil => mkFalse() // does not expect more outputs
184180 case expectedOutput :: newExpectedOutputs =>
185181 mkAnd(
186182 mkEq(mkBVAND(comboOperand, threeBitBV), mkBV(expectedOutput, bits)),
@@ -197,16 +193,17 @@ object Day17 {
197193 else {
198194 expectedOutputs match {
199195 case Nil => mkTrue()
200- case _ :: _ => mkFalse()
196+ case _ :: _ => mkFalse() // expects more outputs
201197 }
202198 }
203199 }
204200
205201 val initialA = mkBVConst(" initialA" , bits)
206- val constraint = helper(0 , Registers (initialA, zeroBV, zeroBV), program.toList)
207- s.Add (constraint)
208202 s.MkMinimize (initialA)
209203
204+ val constraint = helper(0 , Registers (initialA, mkBV(registers.b, bits), mkBV(registers.c, bits)), program.toList)
205+ s.Add (constraint)
206+
210207 assert(s.Check () == Status .SATISFIABLE )
211208 s.getModel.evaluate(initialA, false ).toString.toLong
212209 }
@@ -217,38 +214,37 @@ object Day17 {
217214 val iterProgram :+ 3 :+ 0 = input.program
218215
219216 @ tailrec
220- def helper (as : Set [Long ], expectedOutputsRev : List [Int ]): Set [Long ] = expectedOutputsRev match {
217+ def helper (as : Set [Long ], expectedOutputsRev : List [Byte ]): Set [Long ] = expectedOutputsRev match {
221218 case Nil => as
222219 case expectedOutput :: newExpectedOutputsRev =>
223220 val newAs =
224221 for {
225222 a <- as
226- aStep <- 0 to 7
227- newA = (a << 3 ) | aStep
228- out = runOutput0( Input ( Registers ((newA & 0b1111111111 ).toInt, 0 , 0 ), iterProgram) )
229- if out == Seq (expectedOutput)
223+ iterA <- 0 to 7
224+ newA = (a << 3 ) | iterA
225+ outputs = runOutputs(input.registers.copy(a = newA), iterProgram)
226+ if outputs == Seq (expectedOutput)
230227 } yield newA
231228 helper(newAs, newExpectedOutputsRev)
232229 }
233230
234231 val as = helper(Set (0 ), input.program.reverse.toList)
235- // as.foreach(println)
236232 as.min
237233 }
238234 }
239235
240236 def parseInput (input : String ): Input = input match {
241237 case s " Register A: $a\n Register B: $b\n Register C: $c\n\n Program: $programStr" =>
242238 val registers = Registers (a.toInt, b.toInt, c.toInt)
243- val program = programStr.split(" ," ).map(_.toInt ).toSeq
239+ val program = programStr.split(" ," ).map(_.toByte ).toSeq
244240 Input (registers, program)
245241 }
246242
247243 lazy val input : String = scala.io.Source .fromInputStream(getClass.getResourceAsStream(" day17.txt" )).mkString.trim
248244
249245 def main (args : Array [String ]): Unit = {
250- import GenericZ3Part2Solution ._
251- println(runOutput (parseInput(input)))
246+ import ReverseEngineeredPart2Solution ._
247+ println(runOutputsString (parseInput(input)))
252248 println(findQuineA(parseInput(input)))
253249
254250 // part 1: 4,5,0,4,7,4,3,0,0 - wrong (bst used literal not combo operand)
0 commit comments