AdibSurani

from z3 import *

# each block of code is identical, except for the parameters on lines 4, 5, and 15, so we cache these
lst = open('day24.txt', 'r').read().splitlines()
lst = [[int(y.split()[-1]) for y in [lst[i+4],lst[i+5],lst[i+15]]] for i in range(0,len(lst),18)]

def solve(max):
    s = Optimize()
    z = 0  # this is our running z, which has to be zero at the start and end
    v = 0  # this is the value from concatenating our digits

AdibSurani

var bytes = File.ReadAllBytes("vt1.file1.proper.bin");
$"Uncompressed size is {bytes.Length}".Dump();
var compressed = Compress(bytes);
$"Compressed size is {compressed.Length} ({100.0 * compressed.Length / bytes.Length:0.0}%)".Dump();
$"Round-trip decompression succeeded: {Decompress(compressed).SequenceEqual(bytes)}".Dump();

// run with LINQPad 6
///////////////////////

byte[] Compress(byte[] input)