在 BitVectors 中设置位域答案

【问题标题】：Setting bit fields in BitVectors在 BitVectors 中设置位域
【发布时间】：2021-12-06 11:50:23
【问题描述】：

假设您有一个 64 位的 BitVector，并希望用其他值来表示第 8 到 15 位的替换。哪种方法最有效？

【问题讨论】：

标签： z3

【解决方案1】：

最好的方法是提取顶部和底部部分，并将替换件直接拼接在里面。像这样：

(set-option :produce-models true)
(set-logic QF_BV)

(declare-fun original    () (_ BitVec 64))
(declare-fun replacement () (_ BitVec 8))

(define-fun result () (_ BitVec 64) (concat ((_ extract 63 16) original)
                                            replacement
                                            ((_ extract 7 0) original)))

(assert (= (bvadd original #x0000000000000100) result))
(check-sat)
(get-value (original replacement result))

打印出来：

sat
((original #x0000000000000000)
 (replacement #x01)
 (result #x0000000000000100))

请注意，移位和屏蔽的替代方法也可以工作，但根据我的经验，如果可以的话，避免算术是可行的方法。（也就是说，and-mask 在正确的位置使用 0 字节，将您的替换向左移动并按位或。）但是对于任何询问“最佳方式”的问题，答案是尝试不同的选项并对它们进行基准测试。对于不同的问题，不同的编码可能会表现得更好。

【讨论】：