Плохая производительность при использовании `str.indexof` с` int2bv`

Question

Я пытаюсь ограничить битовый вектор равным индексу нулевого байта в строке. Тем не менее, у меня возникают проблемы с производительностью int2bv.

В качестве простого примера проблемы, эта проблема (без int2bv) решается мгновенно:

; Solve time: 0m0.065s
(declare-const s String)
(declare-const len Int)
(assert (= (str.indexof s "\00") len))
(assert (>= len 256)) ; 0x100
(assert (<= len 4095)) ; 0xFFF
(check-sat)
(get-model)

С другой стороны, «та же» проблема (она позволяет строго больше решений) использование int2bv занимает почти 2 минуты:

; Solve time: 1m54.861s
(declare-const s String)
(declare-const len Int)
(assert (= (str.indexof s "\00") len))
(assert (>= len 0))
(assert (not (= (bvand ((_ int2bv 12) len) #xF00) #x000)))
(check-sat)
(get-model)

Есть ли лучший способ кодировать этот тип операции длины строки битового вектора в z3? Эти слайды на z3strBV утверждают, что имеют лучшую поддержку, но их расширения, кажется, не реализованы в стандартном дистрибутиве z3.

Я использую z3 версии 4.8.0 - 64-битная иработает с smt.string_solver=z3str3.

Answer 1

Методом проб и ошибок я обнаружил, что опция smt.str.use_binary_search=true уменьшает время решения для второй проблемы до 2 секунд! Не уверен, почему значение по умолчанию для этого параметра равно false.