Почему создание объектов И / ИЛИ в Z3py занимает больше времени, чем ожидалось?

Я использую Z3py, где мне нужно создать тысячи объектов And () и Or () для подачи в Z3 Solver. Кажется, что большую часть времени уходит на создание этих объектов (добавление их в решатель и их решение происходит намного быстрее). В крайнем случае попробовал вот что:

assertion = True
for i in range(10000):
    assertion = Or(assertion, True)

Это занимает около 0,8 секунды (в том числе для And ()), что довольно много для простого создания объектов утверждения Or.

Выполняет ли Z3 какую-либо предварительную обработку при создании объектов And / Or или такое поведение является неожиданным? Я запускаю Z3 с помощью Z3py на Macbook Pro (Intel i5 2,4 ГГц, 8 ГБ ОЗУ).


performance z3 z3py
person Kausik Subramanian    schedule 17.12.2015    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Функции

   def And(..):
       ...
   def Or(..):
       ...

В файле z3.py выполните ряд проверок аргументов для вычисляемых типов. Они также включают некоторые отладочные утверждения. Вы можете отключить отладочные утверждения в python, установив встроенный параметр или вызвав python с флагом -O.

В конце концов, эти функции вызывают функции Z3_mk_and и Z3_mk_or. Вы также можете вызывать их прямо из python и обходить дополнительные проверки и принуждения. Например, вы можете определить что-то в следующих строках, реализующее функцию, которая обходит несколько проверок работоспособности, поэтому, если в вашем коде есть ошибки, сообщения об ошибках не будут такими информативными.

  def myAnd(es):       
      if es = []:
         return BoolVal(True, get_ctx())    
      num = len(es)
      ctx = es[0].ctx()
      _es = (Ast * num)()
      for I in range(num):
          _es[I] = es[I].as_ast()
      return BoolRef(Z3_mk_and(ctx.ref(), num, _es), ctx)
person Nikolaj Bjorner    schedule 17.12.2015
comment
Спасибо за ответ. Я просмотрел код в z3.py. Должны ли эти проверки происходить, когда z3 построен в режиме выпуска (версия, которую я использовал)? Также вы бы порекомендовали использовать z3py или создать строку / файл SMT-lib со всеми ограничениями и передать их анализаторам Z3? Мне приходится запускать Z3 на экземплярах, решение которых обычно занимает несколько минут. - person Kausik Subramanian; 18.12.2015