Z3 和 CVC4 中哪些转换运算符可用于位向量？

Question

我正在编写一个需要转换的问题的 BV 编码一些 Int 到 BitVec，反之亦然。

在mathsat/optimathsat中可以使用：

((_ to_bv BITS) <int_term>) ; Int => BitVec
(sbv_to_int <bv_term>)      ; Signed BitVec => Int
(ubv_to_int <bv_term>)      ; Unsigned BitVec => Int

在z3中可以使用：

((_ int2bv BITS) <int_term>) ; Int => BitVec
???                          ; Signed BitVec => Int   
(bv2int <bv_term>)           ; Unsigned BitVec => Int

在CVC4中可以使用：

((_ int2bv BITS) <int_term>) ; Int => BitVec
???                          ; Signed BitVec => Int   
???                          ; Unsigned BitVec => Int

问：

z3 是否具有签名 BitVec 的 bv2int 功能？ (好像没有。)
CVC4 有任何 bv2int 功能吗？ （我不知道。）
是否有一些地方记录了这些转换函数？ （关于 Logics/Theories 的 SMT-LIB 网页似乎没有关于它们的任何信息。）

注意：我受限于基于文本的SMT-LIB界面（无API解决方案）

Answer 1

SMTLib 确实定义了 bv2nat 和 nat2bv:

bv2nat, which takes a bitvector b: [0, m) → {0, 1} with 0 < m, and returns an integer in the range [0, 2^m), and is defined as follows:
   bv2nat(b) := b(m-1)*2^{m-1} + b(m-2)*2^{m-2} + ⋯ + b(0)*2^0
o nat2bv[m], with 0 < m, which takes a non-negative integer n and returns the (unique) bitvector b: [0, m) → {0, 1} such that
   b(m-1)*2^{m-1} + ⋯ + b(0)*2^0 = n rem 2^m

看这里：http://smtlib.cs.uiowa.edu/theories-FixedSizeBitVectors.shtml

CVC4和z3应该都支持这两个操作。（如果没有，你应该向他们报告！）

对于其他所有内容，您必须自己计算。 SMTLib 对位向量的 "sign" 绝对不可知；它没有给给定的向量赋予符号，而是提供不同的算术运算符的有符号和无符号版本。（例如，只有一个版本的加法，因为对于该操作您是否已签名或未签名的位向量并不重要，但为了进行比较，我们得到 bvult、bvslt 等）

从这两个函数，您可以定义您的其他变体。例如，要将长度为 8 的有符号位向量 x 转换为整数，我会去：

(ite (= ((_ extract 7 7) x) #b0)
           (bv2nat ((_ extract 6 0) x))
        (- (bv2nat ((_ extract 6 0) x)) 128)))

也就是你检查x的最高位：

如果是0，那么你用bv2nat转换就可以了。（你可以跳过最高位，因为你知道它是 0，作为一个小的优化。）
如果最高位是1，那么这个值就是你跳过最高位转换的值，你减去128(=2^(8-1))，从它。通常，您将减去 2^(m-1)，其中 m 是位向量的大小。

一个问题：您不能创建一个 SMTLib 函数来为所有位向量大小执行此操作。这是因为 SMTLib 不允许用户定义大小多态函数。但是，您可以通过动态声明来生成任意数量的此类函数，或者在需要时简单地生成相应的表达式。

其他操作也可以使用类似的技巧进行类似的编码。如果您运行遇到问题，请提出具体问题。

Z3 和 CVC4 中哪些转换运算符可用于位向量？

What conversion operators are available in Z3 and CVC4 for Bit-Vectors?

smt

z3

cvc4

mathsat

optimathsat