For anyone wishing to try this without having to install z3, or just to see a more rudimentary way of doing this, here is a self-contained (hopefully just as readable) solution in JS:
const num = findNum();
const bin = num.toString(2);
const byteStrings = toChunks(bin, 7).map(chunk => chunk.join(''));
const bytes = byteStrings.map(str => parseInt(str, 2));
const str = bytes.map(String.fromCharCode).join('');
console.log(num, bin, byteStrings, bytes, str);
function findNum(i=0, lim=1e1000000000) {
while (i < lim) {
if (i % 611939 === 145767 && i % 598463 === 109572) return i;
i += 1;
}
}
function toChunks(iterable, chunkSize) {
const chunks = [];
for (const el of iterable) {
let buf = chunks[chunks.length - 1];
if (!buf || buf.length >= chunkSize) {
buf = [];
chunks.push(buf);
}
buf.push(el);
}
return chunks;
}
243085550 1110011111010011000011101110 [ '1110011', '1110100', '1100001', '1101110' ] [ 115, 116, 97, 110 ] <xxx>
Sorry about not getting a response from the poster of the job, by the way. It's a very unhealthy attitude and it's sad to see this on HN of all places.
Sorry about not getting a response from the poster of the job, by the way. It's a very unhealthy attitude and it's sad to see this on HN of all places.