Почему Z3 медленный для крошечного пространства поиска?

Я пытаюсь создать программу Z3 (на Python), которая генерирует логические схемы, которые выполняют определенные задачи (например, добавление двух n-битных чисел), но производительность ужасна до такой степени, что поиск грубой силы всего пространства решений будет будь быстрее. Я впервые использую Z3, поэтому могу делать что-то, что влияет на мою производительность, но мой код кажется нормальным.

Следующее скопировано из моего кода здесь:

from z3 import *

BITLEN = 1 # Number of bits in input
STEPS = 1 # How many steps to take (e.g. time)
WIDTH = 2 # How many operations/values can be stored in parallel, has to be at least BITLEN * #inputs

# Input variables
x = BitVec('x', BITLEN)
y = BitVec('y', BITLEN)

# Define operations used
op_list = [BitVecRef.__and__, BitVecRef.__or__, BitVecRef.__xor__, BitVecRef.__xor__]
unary_op_list = [BitVecRef.__invert__]
for uop in unary_op_list:
    op_list.append(lambda x, y : uop(x))

# Chooses a function to use by setting all others to 0
def chooseFunc(i, x, y):
    res = 0
    for ind, op in enumerate(op_list):
        res = res + (ind == i) * op(x, y)
    return res

s = Solver()
steps = []

# First step is just the bits of the input padded with constants
firststep = Array("firststep", IntSort(), BitVecSort(1))
for i in range(BITLEN):
    firststep = Store(firststep, i * 2, Extract(i, i, x))
    firststep = Store(firststep, i * 2 + 1, Extract(i, i, y))
for i in range(BITLEN * 2, WIDTH):
    firststep = Store(firststep, i, BitVec("const_0_%d" % i, 1))
steps.append(firststep)

# Generate remaining steps
for i in range(1, STEPS + 1):
    this_step = Array("step_%d" % i, IntSort(), BitVecSort(1))
    last_step = steps[-1]

    for j in range(WIDTH):
        func_ind = Int("func_%d_%d" % (i,j))
        s.add(func_ind >= 0, func_ind < len(op_list))

        x_ind = Int("x_%d_%d" % (i,j))
        s.add(x_ind >= 0, x_ind < WIDTH)

        y_ind = Int("y_%d_%d" % (i,j))
        s.add(y_ind >= 0, y_ind < WIDTH)

        node = chooseFunc(func_ind, Select(last_step, x_ind), Select(last_step, y_ind))
        this_step = Store(this_step, j, node)

    steps.append(this_step)

# Set the result to the first BITLEN bits of the last step
if BITLEN == 1:
    result = Select(steps[-1], 0)
else:
    result = Concat(*[Select(steps[-1], i) for i in range(BITLEN)])

# Set goal
goal = x | y
s.add(ForAll([x, y], goal == result))

print(s)
print(s.check())
print(s.model())

Код в основном представляет входные данные как отдельные биты, затем на каждом «шаге» одна из 5 логических функций может работать со значениями из предыдущего шага, где последний шаг представляет конечный результат.

В этом примере я создаю схему для вычисления логического ИЛИ двух 1-битных входов, и в схеме доступна функция ИЛИ, поэтому решение тривиально.

У меня есть пространство решений всего 5 * 5 * 2 * 2 * 2 * 2 = 400:

• 5 Возможные функции (два функциональных узла)
• 2 входа для каждой функции, каждая из которых имеет два возможных значения

Этот код запускается за несколько секунд и дает правильный ответ, но я чувствую, что он должен запускаться мгновенно, поскольку существует только 400 возможных решений, из которых довольно много действительных. Если я увеличу входные данные до двух битов, пространство решений будет иметь размер (5 ^ 4) * (4 ^ 8) = 40 960 000 и никогда не завершится на моем компьютере, хотя я считаю, что это должно быть легко выполнимо с Z3.

Я также эффективно попробовал тот же код, но заменил Arrays / Store / Select на списки Python и «выбрал» переменные, используя тот же трюк, который я использовал в selectFunc (). Код находится здесь и выполняется примерно в то же время, что и исходный код делает, поэтому нет ускорения.

Я делаю что-то, что резко замедлит работу решателя? Спасибо!