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 功能吗？ （我不知道。）
• 这些转换函数是否有文档记录？ （关于逻辑/理论的 SMT-LIB 网页似乎没有任何关于它们的信息。）

注意：我受限于基于文本的 SMT-LIB 接口（没有 API 解决方案）。

Answer 1

SMTLib 确实定义了bv2nat 和nat2bv：

bv2nat，它接受一个位向量 b：[0, m) → {0, 1} 0

   bv2nat(b) := b(m-1)*2^{m-1} + b(m-2)*2^{m-2} + ⋯ + b(0)*2^0

o nat2bv[m], 0

   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 绝对不知道位向量的“符号”；它不给给定向量赋予符号，而是在算术运算符不同时提供有符号和无符号版本的算术运算符。 （例如，只有一个版本的加法，因为对于该操作您是否有带符号或无符号位向量并不重要，但对于比较我们得到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 不允许用户定义大小多态函数。但是，您可以通过动态声明它们来生成任意数量的此类函数，或者在需要时简单地生成相应的表达式。

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