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

Question

我正在尝试学习一些有关 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（不使用任何库）。

Answer 1

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

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

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

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

function to get nibbles using Z3 and bitvector theory

z3

smt

sat-solvers