It turns out you can make a really fast instruction decoder in Scrap Mechanic if only you can figure out a special bit mask for each ALU operation. It turns out this is really frickity fucking hard to do by hand so I told a SAT solver to do it and it was fine until I asked for all the combinations I wanted and then... This.
out.dimacs is 36MB
c CNF file written by RustSAT
p cnf 217953 1366264
Also dimacs uses "c" for comments lol (it's just a huge file of numbers).
Also also it turns out using 100% of all 24 cores on a laptop for 8 hours makes for some heat issues so I had to limit each core to 50% utilization so it will take twice as long yay.
UPDATE: it's been 18 hours and the best it's got it 3.925%. If I linearly extrapolate, it will take 400-500 hours โ 2.5-3 weeks.
UPDATE 2: I've turned it off, as I don't have more than a weekend to just leave my laptop sitting around.
I'm just excited that Z3 has a parallel mode now. Last time I was using it much, it was only single core.