z3 - 将 `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.

标签： z3smt

Answer 1

通过反复试验，我发现该选项smt.str.use_binary_search=true将第二个问题的解决时间降至 2 秒以下！不过，不确定为什么此选项的默认值为 false。