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

function to get nibbles using Z3 and bitvector theory

我正在尝试学习一些有关 z3 和位向量理论的知识。 我的意图是创建一个函数来从位向量

的位置获取半字节

此代码returns半字节:

(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) 之类的东西,但它不起作用。

谢谢

P.S:想法是从命令行使用 z3(不使用任何库)。

extract函数只接受数字作为参数,不接受任意表达式。然而,我们可以将表达式向一个方向移动,然后提取前四位或后四位,例如按照

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

(其中 idx 和 four 是大小为 12 的位向量表达式)。