z3 - 在 Z3 中的索引 i 处设置位

Question

我正在尝试在 z3 中的位向量中的特定索引处设置位。

目前，我使用按位或来完成此操作。我正在处理大位向量(超过 1000 位)，并且相信这是导致求解器花费大量时间的原因。我希望他们是一种比这更快的方式来设置位向量中的任意位(类似于数组使用的存储)。

有没有更好的方法来做到这一点，还是我只能使用按位或？

Answer 1

我不确定它是否会更快，但你总是可以像这样做一个断言:

(assert (= ((_ extract i i) bv) #b1))

告诉求解器 bv 的第 i 位为高。当然，这在您的特定应用程序中是否可用取决于这些新表达式的传递方式。如果这个技巧对你不起作用，我认为你被按位或困住了。