我试图在z3中的位向量中的特定索引处设置位。
目前，我使用逐位或完成此操作。我正在使用大位向量（超过1000位），并认为这导致求解器花费大量时间。我希望它们是一种比在位向量中设置任意位更快的方法（类似于Arrays使用的存储）。
有没有更好的方法可以做到这一点，还是我只是按位使用还是？
最佳答案
我不确定是否会更快，但是您始终可以执行如下断言：
(assert (= ((_ extract i i) bv) #b1))
告诉求解器
i的第bv位为高。当然，这在您的特定应用程序中是否可用取决于这些新表达式如何传递。如果这个技巧对您不起作用，那么我认为您会陷入按位“或”的困境。