在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有用于签名BitVec的bv2int函数吗？(似乎没有)
• 是否有任何bv2int函数？(我一点也不知道)H 220H 121是否有记录这些转换函数的地方？( SMT-LIB关于逻辑/理论的网页似乎没有关于它们的任何信息。)H 222/code>f 223

注意：i受基于文本的SMT接口(没有解决方案)的限制.

Answer 1

SMTLib确实定义了bv2nat和nat2bv

bv2nat，它接受0< m的位向量b：[0，m)→{0，1}，并返回范围[0，2^m]中的整数，定义如下：

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

O nat2bvm，0< m，它接受一个非负整数n并返回(唯一)位向量b：[0，m)→{0，1}

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，则只需使用

• 转换它。(您可以跳过顶部位，因为您知道它是0，作为一个小optimization.)
• If，顶部位是1，然后通过跳过顶部位来转换值，然后从其中减去128 (= 2^(8-1))。通常，您将减去2^(m-1)，其中m是位向量的大小。

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

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