Why Is Z3 Slow For Tiny Search Space?

I'm trying to make a Z3 program (in Python) that generates boolean circuits that do certain tasks (e.g. adding two n-bit numbers) but the performance is terrible to the point where

Solution 1:

You have a duplicated __xor__ in your op_list; but that's not really the major problem. The slowdown is inevitable as you increase bit-size, but on a first look you can (and should) avoid mixing integer reasoning with booleans here. I'd code your chooseFunc as follows:

defchooseFunc(i, x, y):
    res = False;
    for ind, op inenumerate(op_list):
        res = If(ind == i, op (x, y), res)
    return res

See if that improves run-times in any meaningful way. If not, the next thing to do would be to get rid of arrays as much as possible.