社区首页 >问答首页 >在Z3中的索引i处设置位

问在Z3中的索引i处设置位
EN

Stack Overflow用户

提问于 2017-07-14 22:21:23

回答 2查看 392关注 0票数 3

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

目前，我使用逐位or来完成此任务。我正在处理大的位向量(超过1000位)，我认为这是导致求解器花费大量时间的原因。我希望他们的方法比这更快地在位向量中设置任意位(类似于数组使用的存储)。

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

发布于 2017-07-15 00:29:44

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

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

告诉求解器bv的第i位是高电平。当然，这在您的特定应用程序中是否可用取决于这些新表达式是如何传递的。如果这个技巧对你不起作用，我认为你只能使用with or。

票数 2

发布于 2017-07-15 10:40:41

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

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

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

票数 2

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/45112375

复制

相似问题

问在Z3中的索引i处设置位EN