我想要一个布尔变量来测试,例如,位向量的第三位是否为 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 供以后使用。你能给我一个提示吗?谢谢。