Z3Py: анализ выражений с использованием eval или z3.parse_smt2_string

Я пишу программу на Python, которая, помимо прочего, должна преобразовывать большие пропозициональные формулы в экземпляры z3. Например, формула f, которая может быть создана моей программой через

a = my_atomic_proposition("a") # Bool
b = my_atomic_proposition("b", operator.ge, 42) # Real: c >= 42
c = my_atomic_proposition("c") # Bool
f = my_and(a, my_or(b, my_not(c)))

должен быть преобразован в экземпляр z3 g, т.е.

a = z3.Bool("a")
b = z3.Real("b")
c = z3.Bool("c")
g = z3.And(a, z3.Or(b >= 42, z3.Not(c)))

Пожалуйста, имейте в виду, что я говорю о формулах, содержащих в основном более 100 терминов.

Следуя сообщению Z3 со строковыми выражениями, я сначала попытался создать свой собственный парсер ( Вариант 1, предложенный Леорнардо де Моура в посте), который просто рекурсивно прошел через все операнды моей формулы и по пути создал экземпляр z3. Этот вариант был довольно медленным, поэтому вместо этого я попытался рекурсивно построить строки, которые были намного быстрее, а затем вызвать для них eval (вариант 3, описанный в посте выше). Это решение было намного быстрее, однако не работало всякий раз, когда мои формулы становились слишком большими (выбрасывалось MemoryError).

Итак, теперь я собираюсь попробовать третий вариант: использование z3.parse_smt2_string для создания экземпляра z3 из строки (не тот, который я использовал выше с eval, он должен иметь другой синтаксис). Я бы поступил так же, как это делается в проблемах использования Z3_parse_smtlib_string. Однако я хотел бы знать, могу ли я столкнуться с такими же проблемами с памятью, используя z3.parse_smt2_string, как и с eval? С тех пор я, вероятно, буду искать другой способ, прежде чем прилагать к этому слишком много усилий.

Кроме того, если у кого-то есть другая (надеюсь, даже более разумная) идея о том, как я могу достичь своей цели, я был бы рад любому комментарию. Спасибо за помощь!

ИЗМЕНИТЬ — пример ошибки памяти:

Я приведу пример одного случая, когда выбрасывается MemoryError: Предположим, у меня есть следующая формула в виде строки:

f = 'z3.Or(a___0,z3.And(True,z3.Or(a___1,z3.And(True,z3.Or(a___2,z3.And(True,z3.Or(a___3,z3.And(True,z3.Or(a___4,z3.And(True,z3.Or(a___5,z3.And(True,z3.Or(a___6,z3.And(True,z3.Or(a___7,z3.And(True,z3.Or(a___8,z3.And(True,z3.Or(a___9,z3.And(True,z3.Or(a___10,z3.And(True,z3.Or(a___11,z3.And(True,z3.Or(a___12,z3.And(True,z3.Or(a___13,z3.And(True,z3.Or(a___14,z3.And(True,z3.Or(a___15,z3.And(True,z3.Or(a___16,z3.And(True,z3.Or(a___17,z3.And(True,z3.Or(a___18,z3.And(True,z3.Or(a___19,z3.And(True,z3.Or(a___20,z3.And(True,z3.Or(a___21,z3.And(True,z3.Or(a___22,z3.And(True,z3.Or(a___23,z3.And(True,z3.Or(a___24,z3.And(True,z3.Or(a___25,z3.And(True,z3.Or(a___26,z3.And(True,z3.Or(a___27,z3.And(True,z3.Or(a___28,z3.And(True,z3.Or(a___29,z3.And(True,z3.Or(a___30,z3.And(True,z3.Or(a___31,z3.And(True,z3.Or(a___32,z3.And(True,z3.Or(a___33,z3.And(True,z3.Or(a___34,z3.And(True,z3.Or(a___35,z3.And(True,z3.Or(a___36,z3.And(True,z3.Or(a___37,z3.And(True,z3.Or(a___38,z3.And(True,z3.Or(a___39,z3.And(True,z3.Or(a___40,z3.And(True,z3.Or(a___41,z3.And(True,z3.Or(a___42,z3.And(True,z3.Or(a___43,z3.And(True,z3.Or(a___44,z3.And(True,z3.Or(a___45,z3.And(True,z3.Or(a___46,z3.And(True,z3.Or(a___47,z3.And(True,z3.Or(a___48,z3.And(True,z3.Or(a___49,z3.And(True,a___50))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))'

и следующий список строк, представляющих переменные f:

variables = ['a___2', 'a___31', 'a___34', 'a___46', 'a___29', 'a___12', 'a___9', 'a___32', 'a___41', 'a___24', 'a___38', 'a___23', 'a___19', 'a___50', 'a___3', 'a___6', 'a___35', 'a___28', 'a___13', 'a___16', 'a___0', 'a___33', 'a___36', 'a___40', 'a___45', 'a___10', 'a___39', 'a___43', 'a___22', 'a___27', 'a___7', 'a___49', 'a___21', 'a___17', 'a___1', 'a___4', 'a___37', 'a___44', 'a___11', 'a___14', 'a___30', 'a___42', 'a___47', 'a___8', 'a___26', 'a___48', 'a___20', 'a___25', 'a___5', 'a___15', 'a___18']

то я использую eval следующим образом:

# Declare z3 variables for all strings in my list 'variables'
for x in variables:
    globals()[x] = z3.Bool(x)
# Create z3 object from string 'f'
z3f = eval(f)

и получите ошибку:

---------------------------------------------------------------------------
MemoryError                               Traceback (most recent call last)
<ipython-input-71-b7421db475e5> in <module>()
      3     globals()[x] = z3.Bool(x)
      4 # Create z3 object from string 'f'
----> 5 z3f = eval(f)

MemoryError: 

Для аналогичного, но более короткого f код выше работает нормально. Например для:

f = 'z3.Or(a___0,z3.And(True,z3.Or(a___1,z3.And(True,z3.Or(a___2,z3.And(True,z3.Or(a___3,z3.And(True,z3.Or(a___4,z3.And(True,z3.Or(a___5,z3.And(True,z3.Or(a___6,z3.And(True,z3.Or(a___7,z3.And(True,z3.Or(a___8,z3.And(True,z3.Or(a___9,z3.And(True,z3.Or(a___10,z3.And(True,z3.Or(a___11,z3.And(True,z3.Or(a___12,z3.And(True,z3.Or(a___13,z3.And(True,z3.Or(a___14,z3.And(True,z3.Or(a___15,z3.And(True,z3.Or(a___16,z3.And(True,z3.Or(a___17,z3.And(True,z3.Or(a___18,z3.And(True,z3.Or(a___19,z3.And(True,z3.Or(a___20,z3.And(True,z3.Or(a___21,z3.And(True,z3.Or(a___22,z3.And(True,z3.Or(a___23,z3.And(True,z3.Or(a___24,z3.And(True,z3.Or(a___25,z3.And(True,z3.Or(a___26,z3.And(True,z3.Or(a___27,z3.And(True,z3.Or(a___28,z3.And(True,z3.Or(a___29,z3.And(True,z3.Or(a___30,z3.And(True,z3.Or(a___31,z3.And(True,z3.Or(a___32,z3.And(True,z3.Or(a___33,z3.And(True,z3.Or(a___34,z3.And(True,z3.Or(a___35,z3.And(True,z3.Or(a___36,z3.And(True,z3.Or(a___37,z3.And(True,z3.Or(a___38,z3.And(True,z3.Or(a___39,z3.And(True,a___40))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))'
variables = ['a___2', 'a___31', 'a___34', 'a___29', 'a___12', 'a___9', 'a___32', 'a___24', 'a___38', 'a___23', 'a___19', 'a___3', 'a___6', 'a___35', 'a___28', 'a___13', 'a___16', 'a___0', 'a___33', 'a___36', 'a___40', 'a___10', 'a___39', 'a___22', 'a___27', 'a___7', 'a___21', 'a___17', 'a___1', 'a___4', 'a___37', 'a___11', 'a___14', 'a___30', 'a___8', 'a___26', 'a___20', 'a___25', 'a___5', 'a___15', 'a___18']

Я получаю:

z3f = Or(a___0,
And(True,
   Or(a___1,
      And(True,
          Or(a___2,
             And(True,
                 Or(a___3,
                    And(True,
                        Or(a___4,
                           And(True,
                               Or(a___5,
                                  And(True,
                                    Or(a___6,
                                    And(True,
                                    Or(a___7,
                                    And(True,
                                    Or(a___8,
                                    And(True,
                                    Or(a___9,
                                    And(True,
                                    Or(..., ...)))))))))))))))))))))