问用Z3实现位智能？
EN

Stack Overflow用户

提问于 2012-12-27 13:38:43

回答 1查看 2.5K关注 0票数 4

我编写了以下Z3 python代码

x, y = Ints('x y')
F = (x == y & 16)      # x has the value of (y & 16)
print F

但是我得到了下面的错误：

TypeError: unsupported operand type(s) for &: 'instance' and 'int'

如何在Z3方程中进行位运算(本例中为&)？

谢谢。

回答已采纳

发布于 2012-12-27 13:50:58

x和y应该是位向量：

x, y = BitVecs('x y', 32)
F = (x == y & 16)      # x has the value of (y & 16)
print F

请参阅http://rise4fun.com/Z3/tutorial/guide下的位向量部分

票数 7

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

原文链接：

https://stackoverflow.com/questions/14049877

复制

相似问题

问用Z3实现位智能？EN