Почему z3.And() работает медленно?

Question

Почему z3.And() работает медленно?

Я использую привязки Z3 Python для создания выражения And через z3.And(exprs) где exprs список питонов из 48000 ограничений на равенство по логическим переменным Эта операция занимает 2 секунды на MBP с процессором 2,6 ГГц.

Что я могу делать не так? Это проблема с привязками z3 Python? Есть идеи, как оптимизировать такие конструкции?

Кстати, в моих экспериментах на построение таких выражений уходит больше времени, чем на решение получающихся формул:)

4

python z3 z3py

Источник

user1366696 15 окт '14 в 06:21

1 ответ

Решение

Другие вопросы по тегам python z3 z3py

user1096362 15 окт '14 в 15:07 2014-10-15 15:07 · Accepted Answer · 2014-10-15 15:07

Использование Z3 поверх Python обычно довольно медленное. Он включает в себя проверку параметров и маршалинг (_coerce_expr среди других). Для масштабируемости вам лучше использовать одну из других привязок или по возможности обходить среду исполнения Python.