使用 SMT 2 输入格式在 Z3 中的 BitVec 中计数 [英] Count ones in BitVec in Z3 with SMT 2 input format

问题描述

是否有一种紧凑的方法可以使用 SMT 2 输入格式计算 Z3 中的 BitVec 中设置为 1 的位数?

Is there a compact way of counting the number of bits that are set to 1 in a BitVec in Z3 using SMT 2 input format?

这个问题的公认答案:位向量中所有位的总和Z3展示了一种使用 Python 实现的方法.

The accepted answer for this question: Sum of all the bits in a Bit Vector of Z3 shows a way to do it using Python.

推荐答案

目前确实没有简单的方法可以直接在 SMTLib 中执行此操作.您真正能做的最好的事情就是为每个位滚动您自己的 -矢量大小；相当丑陋，但易于生成代码:

There's really no easy way to do this directly in SMTLib for the time being.The best you can really do is to roll-your-own for each bit-vector size; rather ugly, but easy to generate code:

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

(define-fun popCount8 ((x (_ BitVec 8))) (_ BitVec 8)
                      (bvadd (ite (= #b1 ((_ extract 0 0) x)) #x01 #x00)
                             (ite (= #b1 ((_ extract 1 1) x)) #x01 #x00)
                             (ite (= #b1 ((_ extract 2 2) x)) #x01 #x00)
                             (ite (= #b1 ((_ extract 3 3) x)) #x01 #x00)
                             (ite (= #b1 ((_ extract 4 4) x)) #x01 #x00)
                             (ite (= #b1 ((_ extract 5 5) x)) #x01 #x00)
                             (ite (= #b1 ((_ extract 6 6) x)) #x01 #x00)
                             (ite (= #b1 ((_ extract 7 7) x)) #x01 #x00)))


; test
(define-fun x () (_ BitVec 8) #xAB)
(declare-fun result () (_ BitVec 8))
(assert (= result (popCount8 x)))
(check-sat)
; Should be 5!
(get-value (result))

打印:

sat
((result #x05))

使用递归

最近版本的 SMTLib 标准允许使用递归函数来以编程方式"执行此操作，但当涉及递归函数时，求解器支持仍然相当粗略.以下适用于 z3，但其他求解器可能效果不佳.有了这个警告，这里有一种使用递归的奇特方式:

Using recursion

Recent versions of the SMTLib standard allow for recursive functions which might be employed to do this "programmatically," but solver support remains rather sketchy when recursive functions are involved. The following works with z3, but other solvers may not fare so well. With that warning, here's a fancy way of doing it using recursion:

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

(define-fun-rec popCount8_rec ((x (_ BitVec 8)) (i (_ BitVec 8)) (accum (_ BitVec 8))) (_ BitVec 8)
    (ite (= i #x08)
         accum
         (popCount8_rec (bvshl x #x01)
                        (bvadd i #x01)
                        (bvadd accum (ite (= #b1 ((_ extract 7 7) x)) #x01 #x00)))))

(define-fun popCount8 ((x (_ BitVec 8))) (_ BitVec 8) (popCount8_rec x #x00 #x00))

; test
(define-fun x () (_ BitVec 8) #xAB)
(declare-fun result () (_ BitVec 8))
(assert (= result (popCount8 x)))
(check-sat)
; Should be 5!
(get-value (result))

这也打印:

sat
((result #x05))

参数多态性

请注意，无论您选择哪种方法，都必须在 popCountN 中为每个大小 N 编写一个单独的函数.SMTLib 不允许用户定义适用于参数"类型的函数.这是逻辑的基本限制，也是为什么许多人更喜欢使用高级语言编写 SMT 求解器脚本以避免此类样板代码的主要原因之一(尽管绝对不是唯一的！).

Parametric Polymorphism

Note that whichever method you choose, you have to write a separate function for each size N, in popCountN. SMTLib doesn't allow users to define functions that work on "parametric" types. This is a fundamental limitation of the logic, and also one of the main reasons (though definitely not the only one!) why many people prefer scripting SMT solvers from higher level languages to avoid such boilerplate code.

您最好的办法是按照上述方法展开您自己的版本.在 Z3 中使用的一个常见技巧是，您可以使用您链接的 Python 程序并在某个时候print s.sexpr() 并查看生成器生成的内容.如果您愿意，您可以将其剪切粘贴到 SMTLib 中；当然要注意通常的剪切和粘贴错误.

Your best bet is to unroll your own version as outlined above. A common trick to use in Z3 is that you can use the Python program you linked and print s.sexpr() at some point and look at what the generator produced. You can then cut-paste that into SMTLib if you like; though of course beware the usual cut-and-paste errors.

这篇关于使用 SMT 2 输入格式在 Z3 中的 BitVec 中计数的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！