z3py: почему время проверки так сильно меняется после переименования переменной?

Я заметил, что время проверки моих логических формул, написанных в z3py, сильно изменилось (с ~ 60 с до ~ 30 с, около 50%) после того, как я удалил «-» в именах переменных, которые я определил.

E.g.,

vec = IntVector('vec-1',10)

to

vec = IntVector('vec1',10)

Это что-то ожидаемое? Если да, то почему?


z3 smt z3py
person Zhongjun 'Mark' Jin    schedule 19.09.2015    source источник
comment
Вероятно, одна из этих форм имеет коллизию имен. В этом случае Z3 дважды ссылается на одну и ту же константу вместо того, чтобы выдавать ошибку. Значит, вы решаете другую формулу.   -  person usr    schedule 19.09.2015
comment
Ха, это интересно. Спасибо!   -  person Zhongjun 'Mark' Jin    schedule 20.09.2015

Ответы (1)


arrow_upward
2
arrow_downward

Вероятно, одна из этих форм имеет коллизию имен. В этом случае Z3 дважды ссылается на одну и ту же константу вместо того, чтобы выдавать ошибку. Значит, вы решаете другую формулу.

person usr    schedule 20.09.2015
comment
Это звучит интересно. Не могли бы вы привести пример (SMTLib или Z3Py), иллюстрирующий проблему? - person Malte Schwerhoff; 23.09.2015
comment
Могу попробовать синтезировать. - person Zhongjun 'Mark' Jin; 24.09.2015
comment
Я думаю, что этот билет объясняет причину z3-временная вариация/ - person Zhongjun 'Mark' Jin; 09.10.2015
comment
@Zhongjun'Mark'Jin Хорошо! Спасибо - person Malte Schwerhoff; 13.10.2015