Add solution day 17

day_17/example.txt

@@ -0,0 +1,5 @@
+Register A: 729
+Register B: 0
+Register C: 0
+
+Program: 0,1,5,4,3,0

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

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

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

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]);
+});

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<VmInitalStateData> {
+    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<string, number> = {};
+    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(","));
+}

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;
+    }
+}
+```

day_17/solve_2/.python-version

@@ -0,0 +1 @@
+3.12

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()

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",
+]

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()

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 },
+]

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(","));
+}
+
+