我正在尝试在 z3 中的位向量中的特定索引处设置位。
目前,我使用按位或来完成此操作。我正在处理大位向量(超过 1000 位),并且相信这是导致求解器花费大量时间的原因。我希望他们是一种比这更快的方式来设置位向量中的任意位(类似于数组使用的存储)。
有没有更好的方法来做到这一点,还是我只能使用按位或?
最佳答案
我不确定它是否会更快,但你总是可以像这样做一个断言:
(assert (= ((_ extract i i) bv) #b1))
告诉求解器 bv
的第 i
位为高。当然,这在您的特定应用程序中是否可用取决于这些新表达式的传递方式。如果这个技巧对你不起作用,我认为你被按位或困住了。
关于z3 - 在 Z3 中的索引 i 处设置位,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/45112375/