我想要一个布尔变量来测试，例如，位向量的第三位是否为 0。位向量的理论允许提取 1 位作为位向量，但不是布尔类型。我想知道我是否可以出演这个角色。谢谢。
===更新===
如果我的问题不清楚，我很抱歉。但 Nikolaj Bjorner 的答案是如何测试位向量的某一位。虽然我想将位向量的第一位的值分配给变量。我尝试将示例修改如下：
(declare-fun x () (_ BitVec 5))
(declare-fun bit0 () Bool)
(assert (= (= #b1 ((_ extract 0 0) x)) bit0 ))
(check-sat)
z3 抱怨道：
(error "line 2 column 25: invalid declaration, builtin symbol bit0")
(error "line 3 column 44: invalid function application, sort mismatch on argument at position 2")
我需要该变量 bit0 供以后使用。你能给我一个提示吗？谢谢。
创建第三位的提取与值为 1（和一位）的位向量之间的等式。
E.g,
(declare-const x (_ BitVec 5))
(assert (= #b1 ((_ extract 2 2) x)))
(check-sat)
(get-model)
produces
sat
(model
(define-fun x () (_ BitVec 5)
#b00100)
)
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
