Bad performance when using `str.indexof` with `int2bv`

Question

I am trying to constrain a bitvector to be equal to the index of a null byte in a string. However, I am getting performance issues with int2bv.

As a simple example of the issue, this problem (without int2bv) solves instantly:

; 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)

On the other hand, the "same" problem (it allows strictly more solutions) using int2bv takes almost 2 minutes:

; 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)

Is there a better way to encode this kind of bitvector string length operation in z3? These slides on z3strBV claim to have better support, but their extensions don't seem to be implemented in the standard z3 distribution.

I am using z3 version 4.8.0 - 64 bit and running with smt.string_solver=z3str3.

You're really at the mercy of the heuristics here. I'm sure if you asserted the disjunction that len converted to a 12-bit BV and is equal to one of 256, 257 ... 4095 would be solved quickly. Would you consider a faithful translation? It's really hard to predict performance when you combine theories in arbitrary ways, unfortunately. — alias
@alias That would be faithful, but of course a huge encoding. I did find that if I do (set-option :smt.str.use_binary_search true) the solve time for the long one drops to under 2 seconds! — Elliot Gorokhovsky
Not sure why the default setting is false for that, it's a godsend! — Elliot Gorokhovsky
Cool, I didn't know that option. The problem is, of course, you can always concoct a program where the binary-search performs horribly while the regular solver can get really quickly. You can try using "tactics," and run them in parallel perhaps. See here for the tactic language; cs.tau.ac.il/~msagiv/courses/asv/z3py/strategies-examples.htm (It's in Python, but you can express similar things using the SMTLib interface as well.) — alias
Looks like the option you found does the trick. You can answer your own question and accept it, that way it'll be more easily accessible to others on stack-overflow. — alias

Elliot Gorokhovsky Elliot Gorokhovsky · Accepted Answer · 2019-11-04T16:47:56

Through trial and error I found that the option smt.str.use_binary_search=true drops the solve time for the second problem to under 2 seconds! Not sure why the default value for this option is false, though.

Bad performance when using `str.indexof` with `int2bv`

1 Answers