z3 - 使用 Z3 和位向量理论获取半字节的函数

Question

我正在尝试学习一些关于 z3 和位向量理论的知识。我的意图是创建一个函数来从位向量的位置获取半字节

此代码返回半字节：

(define-fun g_nibble(
   (l ( _ BitVec 12))
   (idx (Int))
) ( _ BitVec 4)

(ite
    (= idx 1) ((_ extract 11 8) l)
    (ite
        (= idx 2) ((_ extract 7 4) l)
        (ite
            (= idx 3) ((_ extract 3 0) l)     
            (_ bv0 4)
        )
    )
))

问题是我想避免多次ite调用。我试图将 ((_ extract 3 0) l) 替换为 ((_ extract (+ 4 idx) idx l) 之类的东西，但它不起作用。

谢谢

PS：这个想法是从命令行使用z3（不使用任何库）。

Answer 1

extract 函数只接受数字作为参数，而不是任意表达式。但是，我们可以将表达式转移到一个方向，然后提取第一个或最后四个位，例如沿着

((_ extract 11 8) (bvshl l (bvmul idx four)))

（其中 idx 和 4 是大小为 12 的位向量表达式）。