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

---

Q：

• z3是否对带符号的bv2int具有BitVec功能？ （似乎没有。）
• CVC4完全没有任何bv2int功能吗？ （我不知道。）
• 在哪些地方记录了这些转换功能？ （关于逻辑/理论的SMT-LIB网页似乎没有关于它们的任何信息。）>] >>

  [note：

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

我正在编写问题的BV编码，该问题需要将一些Int转换为BitVec，反之亦然。在mathsat / optimathsat中，可以使用：（（（_ to_bv BITS））; Int => BitVec（...

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不允许用户定义大小多态函数。但是，您可以通过动态声明它们来生成任意数量的此类函数，或者在需要时仅生成相应的表达式。

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