2021: d25: ex2: add solution

2021/d24/ex1/ex1.py

@@ -92,12 +92,13 @@ def solve(input: List[str]) -> int:
 
         solver.add(registers["z"] == zero)
 
-        model_number = functools.reduce(lambda a, b: a * 10 + b, digits)
+        digits_to_num = lambda digits: functools.reduce(lambda a, b: a * 10 + b, digits)
 
-        solver.maximize(model_number)
+        solver.maximize(digits_to_num(digits))
         assert solver.check() == z3.sat  # Sanity check
 
-        return solver.model().eval(model_number)
+        model = solver.model()
+        return digits_to_num(model[d].as_long() for d in digits)
 
     return run_z3(parse())
 

2021/d24/ex2/ex2.py

@@ -92,12 +92,13 @@ def solve(input: List[str]) -> int:
 
         solver.add(registers["z"] == zero)
 
-        model_number = functools.reduce(lambda a, b: a * 10 + b, digits)
+        digits_to_num = lambda digits: functools.reduce(lambda a, b: a * 10 + b, digits)
 
-        solver.minimize(model_number)
+        solver.minimize(digits_to_num(digits))
         assert solver.check() == z3.sat  # Sanity check
 
-        return solver.model().eval(model_number)
+        model = solver.model()
+        return digits_to_num(model[d].as_long() for d in digits)
 
     return run_z3(parse())