Maybe you should play with heuristics to get a good enough solution quickly. Or change solver to something more appropriate for what you are modelling
Programmer Humor
Welcome to Programmer Humor!
This is a place where you can post jokes, memes, humor, etc. related to programming!
For sharing awful code theres also Programming Horror.
Rules
- Keep content in english
- No advertisements
- Posts must be related to programming or programmer topics
- If the mod doesn't find it funny, you're banned. Ha-ha!... For real: do not use the community for "statements". There are other places for such content. Keep it chill and funny.
Based on my other comment, do you have any in mind that would be more appropriate?
What, specifically, are you trying to solve?
For each operation my CPU's ALU can do, I need to find a bit mask that turns it on only for the desired set of 8 bit opcodes. The bit mask is of the form [01_].[01_][01_][01_][01_][01_][01_][01_][01_] where 0 and 1 mean the bit has to match and _ means it doesn't matter. The bit before the . is the xor of all the other bits in the opcode.
The solver has to figure out both which opcodes represent each instruction and what bit masks are needed to give them the desired operations.
I'm just excited that Z3 has a parallel mode now. Last time I was using it much, it was only single core.