1

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

在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的功能吗？（看起来没有。）bv2intBitVec
  • CVC4有什么功能bv2int吗？（我没有任何线索。）
  • 是否有记录这些转换功能的地方？（关于逻辑/理论的 SMT-LIB 网页似乎没有任何关于它们的信息。）

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

4

1 回答 1

1

SMTLib 确实定义了bv2natand nat2bv：

bv2nat，它接受一个位向量 b: [0, m) → {0, 1} with 0 < m, 返回一个 [0, 2^m) 范围内的整数，定义如下：

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

o nat2bv[m]，其中 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）

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

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

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

于 2020-05-07T20:20:09.150 回答