在 Z3 中的索引 i 处设置位

【问题标题】：Set Bit at Index i in Z3在 Z3 中的索引 i 处设置位
【发布时间】：2017-07-14 22:21:23
【问题描述】：

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

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

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

【问题讨论】：

标签： z3

【解决方案1】：

我不确定它是否会更快，但你总是可以做这样的断言：

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

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

【讨论】：

【解决方案2】：

此外，对于位向量，可以使用提取和连接的组合从旧的位向量形成新的位向量。例如

   (concat ((_ extract n-1 k+1) x) y ((_ extract k-1 0) x))

其中 y 是长度为 1 的位向量，应该具有形成一个等于 x 的位向量的效果，除了位置 k，它由 y 定义。

【讨论】：