From 88d78c28f7020f5254ddef207fe63ab34c43bde1 Mon Sep 17 00:00:00 2001 From: monoid Date: Wed, 18 Dec 2024 14:11:55 +0900 Subject: [PATCH] Add solution day 17 --- day_17/example.txt | 5 + day_17/example_2.txt | 5 + day_17/example_3.txt | 5 + day_17/input.txt | 5 + day_17/solve_1.test.ts | 116 +++++++++++++++++++ day_17/solve_1.ts | 199 +++++++++++++++++++++++++++++++++ day_17/solve_2.md | 66 +++++++++++ day_17/solve_2/.python-version | 1 + day_17/solve_2/README.md | 0 day_17/solve_2/example.py | 49 ++++++++ day_17/solve_2/pyproject.toml | 9 ++ day_17/solve_2/solve.py | 58 ++++++++++ day_17/solve_2/uv.lock | 27 +++++ day_17/solve_2_print.ts | 64 +++++++++++ 14 files changed, 609 insertions(+) create mode 100644 day_17/example.txt create mode 100644 day_17/example_2.txt create mode 100644 day_17/example_3.txt create mode 100644 day_17/input.txt create mode 100644 day_17/solve_1.test.ts create mode 100644 day_17/solve_1.ts create mode 100644 day_17/solve_2.md create mode 100644 day_17/solve_2/.python-version create mode 100644 day_17/solve_2/README.md create mode 100644 day_17/solve_2/example.py create mode 100644 day_17/solve_2/pyproject.toml create mode 100644 day_17/solve_2/solve.py create mode 100644 day_17/solve_2/uv.lock create mode 100644 day_17/solve_2_print.ts diff --git a/day_17/example.txt b/day_17/example.txt new file mode 100644 index 0000000..36fbf8d --- /dev/null +++ b/day_17/example.txt @@ -0,0 +1,5 @@ +Register A: 729 +Register B: 0 +Register C: 0 + +Program: 0,1,5,4,3,0 \ No newline at end of file diff --git a/day_17/example_2.txt b/day_17/example_2.txt new file mode 100644 index 0000000..2ed9dda --- /dev/null +++ b/day_17/example_2.txt @@ -0,0 +1,5 @@ +Register A: 2024 +Register B: 0 +Register C: 0 + +Program: 0,3,5,4,3,0 \ No newline at end of file diff --git a/day_17/example_3.txt b/day_17/example_3.txt new file mode 100644 index 0000000..2ed9dda --- /dev/null +++ b/day_17/example_3.txt @@ -0,0 +1,5 @@ +Register A: 2024 +Register B: 0 +Register C: 0 + +Program: 0,3,5,4,3,0 \ No newline at end of file diff --git a/day_17/input.txt b/day_17/input.txt new file mode 100644 index 0000000..863040a --- /dev/null +++ b/day_17/input.txt @@ -0,0 +1,5 @@ +Register A: 23999685 +Register B: 0 +Register C: 0 + +Program: 2,4,1,1,7,5,1,5,0,3,4,4,5,5,3,0 \ No newline at end of file diff --git a/day_17/solve_1.test.ts b/day_17/solve_1.test.ts new file mode 100644 index 0000000..ba9c5cc --- /dev/null +++ b/day_17/solve_1.test.ts @@ -0,0 +1,116 @@ +import { assertEquals } from "jsr:@std/assert"; +import { VM } from "./solve_1.ts"; +import { readData } from "./solve_1.ts"; + +Deno.test("C=9", () => { + const vm = new VM({ + registers: { + A: 0, + B: 0, + C: 9, + }, + programs: [ + 2, 6 + ] + }); + vm.run(); + assertEquals(vm.registers["C"], 9); +}); + +Deno.test("A=10", () => { + const vm = new VM({ + registers: { + A: 10, + B: 0, + C: 0, + }, + programs: [ + 5,0,5,1,5,4 + ] + }); + const outputs: number[] = []; + vm.on("out", (a) => { + outputs.push(a); + }); + vm.run(); + assertEquals(outputs, [ + 0,1,2 + ]); +}); + +Deno.test("A=2024", ()=>{ + const vm = new VM({ + registers: { + A: 2024, + B: 0, + C: 0, + }, + programs: [ + 0,1,5,4,3,0 + ] + }); + const outputs: number[] = []; + vm.on("out", (a) => { + outputs.push(a); + }); + vm.run(); + assertEquals(outputs, [4,2,5,6,7,7,7,7,3,1,0]); + // leave a 0 + assertEquals(vm.registers["A"], 0); +}); + +Deno.test("B=29", ()=> { + const vm = new VM({ + registers: { + A: 0, + B: 29, + C: 0, + }, + programs: [ + 1,7 + ] + }); + vm.run(); + assertEquals(vm.registers["B"], 26); +}); + +Deno.test("B=2024, C=43690", ()=>{ + const vm = new VM({ + registers: { + A: 0, + B: 2024, + C: 43690, + }, + programs: [ + 4,0 + ] + }); + vm.run(); + assertEquals(vm.registers["B"], 44354); +}); + +Deno.test("B store test", ()=>{ + const vm = new VM({ + registers: { + A: 0, + B: 0, + C: 0, + }, + programs: [ + 2,1 + ] + }); + vm.run(); + assertEquals(vm.registers["B"], 1); +}) + +Deno.test("example.txt", async () => { + const data = await readData(import.meta.dirname + "/example.txt"); + const vm = new VM(data); + const outputs: number[] = []; + vm.on("out", (a) => { + outputs.push(a); + }); + vm.run(); + assertEquals(outputs, [4,6,3,5,6,3,5,2,1,0]); +}); \ No newline at end of file diff --git a/day_17/solve_1.ts b/day_17/solve_1.ts new file mode 100644 index 0000000..0c0b7a5 --- /dev/null +++ b/day_17/solve_1.ts @@ -0,0 +1,199 @@ +export type VmInitalStateData = { + registers: { + A: number; + B: number; + C: number; + }; + programs: number[]; +}; + +export async function readData(path: string): Promise { + const data = await Deno.readTextFile(path); + const lines = data.split("\n").map((x) => x.trim()); + const registerRegex = /Register ([ABC]): (\d+)/; + const programRegex = /Program: ((?:\d)(?:,\d)*)/; + const registers: Record = {}; + const programs: number[] = []; + // Parse registers + for (let i = 0; i < 3; i++) { + const match = lines[i].match(registerRegex); + if (match) { + registers[match[1]] = parseInt(match[2]); + } + } + // Parse programs + const match = lines[4].match(programRegex); + if (match) { + programs.push(...match[1].split(",").map((x) => parseInt(x))); + } + return { + registers: { + A: registers["A"], + B: registers["B"], + C: registers["C"], + }, + programs, + }; +} + +const opCodeNameList = [ + "adv", + "bxl", + "bst", + "jnz", + "bxc", + "out", + "bdv", + "cdv", +]; +const operandNameList = [ + "0", + "1", + "2", + "3", + "A", + "B", + "C", + "Invalid", +]; +export function opCodeToName(opCode: number): string { + return opCodeNameList[opCode]; +} +export function operandToName(operand: number): string { + return operandNameList[operand]; +} + +function dv(a: number, b: number): number { + // const denom = Math.pow(2, b); + // return Math.floor(a / denom); + return a >> b; +} + +export class VM { + pc: number; + registers: { + A: number; + B: number; + C: number; + }; + programs: number[]; + + #outHandlers: ((a: number) => void)[] = []; + + constructor(data: VmInitalStateData) { + this.pc = 0; + this.registers = data.registers; + this.programs = data.programs; + } + + comboOperand(operand: number): number { + if (operand < 4) { + return operand; + } + switch (operand) { + case 4: + return this.registers["A"]; + case 5: + return this.registers["B"]; + case 6: + return this.registers["C"]; + default: + throw new Error("Invalid operand"); + } + } + + on(name: "out", cb: (a: number) => void): void { + if (name === "out") { + this.#outHandlers.push(cb); + } + } + off(name: "out", cb: (a: number) => void): void { + if (name === "out") { + this.#outHandlers = this.#outHandlers.filter((x) => x !== cb); + } + } + + runSingleInstruction(): void { + const opCode = this.programs[this.pc]; + const operand = this.programs[this.pc + 1]; + switch (opCode) { + case 0: // adv : a register division + { + const comboOperand = this.comboOperand(operand); + this.registers["A"] = dv(this.registers["A"], comboOperand); + this.pc += 2; + } + break; + case 1: { // bxl : bitwise xor literal + this.registers["B"] = this.registers["B"] ^ operand; + this.pc += 2; + } + break; + case 2: // bst : b register store + { + const comboOperand = this.comboOperand(operand); + this.registers["B"] = comboOperand % 8; // keep only 3 bits + this.pc += 2; + } + break; + case 3: // jnz : jump if not zero + { + if (this.registers["A"] !== 0) { + this.pc = operand; + } else { + this.pc += 2; + } + } + break; + case 4: // bxc : bitwise xor register + { + // for legacy reasons, operand is ignored + this.registers["B"] = this.registers["B"] ^ this.registers["C"]; + this.pc += 2; + } + break; + case 5: // out : output + { + const comboOperand = this.comboOperand(operand) % 8; + this.#outHandlers.forEach((cb) => cb(comboOperand)); + this.pc += 2; + } + break; + case 6: // bdv : b register division + { + const comboOperand = this.comboOperand(operand); + this.registers["B"] = dv(this.registers["A"], comboOperand); + this.pc += 2; + } + break; + case 7: // cdv : c register division + { + const comboOperand = this.comboOperand(operand); + this.registers["C"] = dv(this.registers["A"], comboOperand); + this.pc += 2; + } + } + } + run(): void { + while (this.pc < this.programs.length) { + this.runSingleInstruction(); + } + } +} + +if (import.meta.main) { + const data = await readData("input.txt"); + console.log(data.registers); + for (let i = 0; i < data.programs.length; i += 2) { + const opCode = data.programs[i]; + const operand = data.programs[i + 1]; + console.log(opCodeToName(opCode), operandToName(operand)); + } + const vm = new VM(data); + const outputs: number[] = []; + vm.on("out", (a) => { + outputs.push(a); + }); + vm.run(); + console.log(outputs.join(",")); +} diff --git a/day_17/solve_2.md b/day_17/solve_2.md new file mode 100644 index 0000000..fc86cc6 --- /dev/null +++ b/day_17/solve_2.md @@ -0,0 +1,66 @@ +```js +function l(A: number,B: number, C: number, out: (o: number)=> void) { + do { + B = A % 8 + B = B ^ 1 + C = Math.floor(A / Math.pow(2,B)) + B = B ^ 5; + A = Math.floor(A / 8); + B = B ^ C; + out(B % 8) + } + while (A !== 0); +} +``` +프로그램은 이렇다. +바꿔보자. +```js +function l(A: number, out: (o: number)=> void) { + do { + out(((((A & 7) ^ 1) ^ 5) ^ (A >> ((A & 7) ^ 1))) & 7); + A = A >> 3; + } + while (A !== 0); +} +``` +0b001 +0b101 + +0b100 + +(((A & 7) ^ 4) ^ (A >> ((A & 7) ^ 1) )) & 7 + +((A ^ 4) & 7) ^ ((A >> ((A & 7) ^ 1)) & 7) = k + +```js +function l(A: number,B: number, C: number, out: (o: number)=> void) { + do { + B = A & 7 + B = B ^ 1 + C = A >> B + B = B ^ 5; + B = B ^ C; + out(B & 7) + A = A >> 3; + } + while (A !== 0); +} +``` + +B: 0..7 as +A: 3bit array + +```js +function l(A: number[], out: (o:number) => void) { + let i = 0; + do { + B = A[i + 2] * 4 + A[i+1] * 2 + A[i] + B ^= 1 + C = A[i + B + 2] * 4 + A[i + B + 1] * 2 + A[i + B] + B = B ^ 5; + B ^= C; + out(B); + i += 3; + } +} +``` diff --git a/day_17/solve_2/.python-version b/day_17/solve_2/.python-version new file mode 100644 index 0000000..e4fba21 --- /dev/null +++ b/day_17/solve_2/.python-version @@ -0,0 +1 @@ +3.12 diff --git a/day_17/solve_2/README.md b/day_17/solve_2/README.md new file mode 100644 index 0000000..e69de29 diff --git a/day_17/solve_2/example.py b/day_17/solve_2/example.py new file mode 100644 index 0000000..3ece873 --- /dev/null +++ b/day_17/solve_2/example.py @@ -0,0 +1,49 @@ +import z3 + +# label0: A = (A >> 3); +# label0: out(A % 8); +# label0: if (A !== 0) goto label0; + +# available A 117440: 0b11100101011000000 + +program = [0,3,5,4,3,0] +# program = [3] + +def main(): + solver = z3.Solver() + # bitvector of length len(program) * 3 + A = z3.BitVec('A', len(program) * 3 + 3) + + i = 0 + loopA = A + while i < len(program): + AShift = loopA >> 3 + AMask = AShift & 7 + solver.add(AMask == program[i]) + loopA = AShift + i += 1 + + # print(solver.sexpr()) + + if solver.check() == z3.sat: + model = solver.model() + print(model) + else: + print("unsat") + + +def test(): + solver = z3.Solver() + A = z3.BitVec('A', 5) # 3비트 비트벡터로 'A' 선언 + A = A >> 1 # A를 오른쪽으로 1비트 시프트한 결과를 새로운 변수에 저장 + A = A & 7 # 시프트 결과를 7(0b111)로 마스크 + solver.add(A == 3) # 최종적으로 MaskedA가 3이어야 한다는 제약 추가 + + print(solver.sexpr()) # 제약을 SMT-LIB2 형식으로 출력 + print(solver.check()) # SAT 여부 확인 + if solver.check() == z3.sat: + print(solver.model()) # 모델 출력 + +if __name__ == "__main__": + test() + main() \ No newline at end of file diff --git a/day_17/solve_2/pyproject.toml b/day_17/solve_2/pyproject.toml new file mode 100644 index 0000000..844cf43 --- /dev/null +++ b/day_17/solve_2/pyproject.toml @@ -0,0 +1,9 @@ +[project] +name = "solve-2" +version = "0.1.0" +description = "Add your description here" +readme = "README.md" +requires-python = ">=3.12" +dependencies = [ + "z3-solver>=4.13.4.0", +] diff --git a/day_17/solve_2/solve.py b/day_17/solve_2/solve.py new file mode 100644 index 0000000..a9da347 --- /dev/null +++ b/day_17/solve_2/solve.py @@ -0,0 +1,58 @@ +import z3 + +# function l(A: number,B: number, C: number, out: (o: number)=> void) { +# do { +# B = A & 7 +# B = B ^ 1 +# C = (A >> B) & 7 +# B = B ^ 5; +# B = B ^ C; +# out(B) +# A = A >> 3; +# } +# while (A !== 0); +# } + +def models(formula, max=10): + solver = z3.Solver() + solver.add(formula) + for i in range(max): + if solver.check() == z3.sat: + model = solver.model() + yield model + solver.add(z3.Not(z3.And([d() == model[d] for d in model.decls()]))) + else: + break + +program = [2,4,1,1,7,5,1,5,0,3,4,4,5,5,3,0] + +def main(): + solver = z3.Solver() + # bitvector of length len(program) * 3 + orgA = z3.BitVec('A', len(program) * 3 + 2) + + A = orgA + i = 0 + while i < len(program): + B = A & 7 + B = B ^ 1 + C = (A >> B) & 7 + B = B ^ 5 + B = B ^ C + A = A >> 3 + solver.add(B == program[i]) + i += 1 + + # print(solver.sexpr()) + + if solver.check() == z3.sat: + lst = [] + for model in models(solver.assertions(), max=999): + lst.append(model[orgA].as_long()) + lst.sort() + print(lst) + else: + print("unsat") + +if __name__ == "__main__": + main() diff --git a/day_17/solve_2/uv.lock b/day_17/solve_2/uv.lock new file mode 100644 index 0000000..8901d46 --- /dev/null +++ b/day_17/solve_2/uv.lock @@ -0,0 +1,27 @@ +version = 1 +requires-python = ">=3.12" + +[[package]] +name = "solve-2" +version = "0.1.0" +source = { virtual = "." } +dependencies = [ + { name = "z3-solver" }, +] + +[package.metadata] +requires-dist = [{ name = "z3-solver", specifier = ">=4.13.4.0" }] + +[[package]] +name = "z3-solver" +version = "4.13.4.0" +source = { registry = "https://pypi.org/simple" } +sdist = { url = "https://files.pythonhosted.org/packages/cd/4e/91d92ce676a6b1e8be0805983f5cea3f087702da2eb934e7b04a1925a4c2/z3_solver-4.13.4.0.tar.gz", hash = "sha256:66944689398d19f831f94524e95e99961d998afa27cfef1918a5a441029ea73f", size = 4969872 } +wheels = [ + { url = "https://files.pythonhosted.org/packages/88/a5/dfde6aa22f66e5b5daac29e2b139533558a6535e3d7d790fa94635675ec5/z3_solver-4.13.4.0-py3-none-macosx_13_0_arm64.whl", hash = "sha256:39ba75b867d6afadabc4812b999c9d96656da07d152510452e71ae9374e98926", size = 36887361 }, + { url = "https://files.pythonhosted.org/packages/27/09/5344531552faf759dfdd318309810c68b6f95142d3b77dd402c35e62336e/z3_solver-4.13.4.0-py3-none-macosx_13_0_x86_64.whl", hash = "sha256:6f3d3eff878b5b3c0d6e7f4237c869a489288fbdd8a2d878046ce977339a1a7a", size = 39646865 }, + { url = "https://files.pythonhosted.org/packages/03/53/928b21d33618c86b290408883323dbae27c307951385a634498d3507abbd/z3_solver-4.13.4.0-py3-none-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:2fb8a857adf1064f89581c424fd729ee3e8bad95f4ebf0fb4c1210f65b831f37", size = 28964810 }, + { url = "https://files.pythonhosted.org/packages/a3/db/46e8b8c862e1fb0fd388f31c24b2d7e6dea9e689d9ed0b61c98a8470251f/z3_solver-4.13.4.0-py3-none-manylinux_2_34_aarch64.whl", hash = "sha256:f674d758c199006fa0a527bdf78cb31b4ba5baaaef6c6c0fa80fb063d3834a6c", size = 26990815 }, + { url = "https://files.pythonhosted.org/packages/85/43/8a8119345e17671c62d3c9c4e4482aab5e89095fb57e0977f3388c45466b/z3_solver-4.13.4.0-py3-none-win32.whl", hash = "sha256:d23cb6d7c67ce3a4e57b8715e2be0c0fa350a282e641475e5e559521651471a0", size = 13099333 }, + { url = "https://files.pythonhosted.org/packages/3c/4b/5626ed801d6fb4b383628a544af6cc0c53b3ef00451e2e524c5013a39316/z3_solver-4.13.4.0-py3-none-win_amd64.whl", hash = "sha256:fafb65d7bb04db93e4a46f4357042fd53b420b412db66f0a0053612ed15024ca", size = 16080751 }, +] diff --git a/day_17/solve_2_print.ts b/day_17/solve_2_print.ts new file mode 100644 index 0000000..b9ca0e5 --- /dev/null +++ b/day_17/solve_2_print.ts @@ -0,0 +1,64 @@ +import { opCodeToName, operandToName, readData, VM } from "./solve_1.ts"; + +class VMCompiler extends VM { + compileSingleInstruction(pc: number): string { + const opCode = this.programs[pc]; + const operand = this.programs[pc + 1]; + switch (opCode) { + case 0: + return `label${this.pc}: A = (A >> ${operandToName(operand)});`; + case 1: + return `label${this.pc}: B = B ^ ${operand};`; + case 2: + return `label${this.pc}: B = ${operandToName(operand)} % 8;`; + case 3: + return `label${this.pc}: if (A !== 0) goto label${operand};`; + case 4: + return `label${this.pc}: B = B ^ C;`; + case 5: + return `label${this.pc}: out(${operandToName(operand)} % 8);`; + case 6: + return `label${this.pc}: B = (A >> ${operandToName(operand)});`; + case 7: + return `label${this.pc}: C = (A >> ${operandToName(operand)});`; + default: + throw new Error(`Unknown opCode: ${opCode}`); + } + } + compile(): string { + let code = ""; + let pc = 0; + while (pc < this.programs.length) { + code += this.compileSingleInstruction(pc) + "\n"; + pc += 2; + } + return code; + } +} + +if (import.meta.main) { + const data = await readData("example_3.txt"); + console.log(data.registers); + data.registers.A = 0b11100101011000000; + console.log(data.programs.join(",")); + const vm = new VMCompiler(data); + const text = vm.compile(); + console.log(text); + const out: number[] = []; + console.log(out.join(",")); + // vm.registers.A = 3; + vm.pc = 0; + const outputs: number[] = []; + vm.on("out", (value) => { + outputs.push(value); + }); + // print code and registers + while (vm.pc < vm.programs.length) { + const code = vm.compileSingleInstruction(vm.pc); + vm.runSingleInstruction(); + console.log(code, vm.registers, vm.registers.C & 7); + } + console.log(outputs.join(",")); +} + +