在 SMT 中表示无关位向量

Question

我想定义一个函数，它接受一个位向量，如果某个位置的位满足某些值，则返回 true。 例如：如果位向量为 1x00x01x，其中 x 表示不关心，我需要返回 true。

我目前的实现是：

(define-fun function_i ((i (_ BitVec 8))) Bool
    (and true
        (= #b1 ((_ extract 1 1) i))
        (= #b0 ((_ extract 2 2) i))
        (= #b0 ((_ extract 4 4) i))
        (= #b0 ((_ extract 5 5) i))
        (= #b1 ((_ extract 7 7) i))
    )
)

这是针对一个变量的，并且可能有许多具有 32 个大小的位向量的变量。我担心这种实现会减慢 z3 的速度。提取函数会减慢求解器的速度吗？有没有更好的方法来实现这一点？

Answer 1

没关系。更紧凑的方式是 (i & 1101) == 1000 （强制第一位 1、第二位 0 和最后一位 0，第三位可以是 0 或 1）