如何使用 BitVector 建模有符号整数? [英] How to model signed integer with BitVector?

问题描述

假设a是254的8位整数.如果a 是一个有符号整数，它实际上被认为是-2.相反，如果 a 是无符号的，它仍然是 254.

Suppose that a is an integer of 8-bit of value 254. If a is a signed integer, it is actually considered -2. In contrary, if a is unsigned, it remains 254.

我试图用 Z3 用 BitVector 理论来模拟这个有符号/无符号整数问题，但似乎 BitVector 不允许这样做.这是真的?那么关于如何在 Z3py 中对此建模有什么想法吗?

I am trying to model this signed/unsigned integer problem with BitVector theory with Z3, but it seems BitVector doesnt allow this. Is this true? Then any idea on how to model this in Z3py?

非常感谢.

推荐答案

Z3 具有用于签名和未签名解释的 API.例如，在 C API 中，Z3_mk_bvslt 创建有符号的小于，Z3_mk_bvult 创建无符号的小于.在 Z3Py 中，我们重载了 <, <=, ... 使用签名的.对于创建，未签名的 a ，我们必须使用ULT(a,b).以下是无符号运算符的列表:ULE (<=), ULT (<), UGE (>=), UGT (>), UDiv (无符号除法)，URem(无符号余数).您可以在此处找到更多信息:

Z3 has APIs for the signed and unsigned interpretations. For example, in the C API, Z3_mk_bvslt creates the signed less than, and Z3_mk_bvult the unsigned one. In Z3Py, we overloaded <, <=, ... using the signed ones. For creating, the unsigned a < b, we have to use ULT(a,b). Here is the list of unsigned operators: ULE (<=), ULT (<), UGE (>=), UGT (>), UDiv (unsigned division), URem (unsigned remainder). You can find more information here:

http://research.microsoft.com/en-us/um/redmond/projects/z3/namespacez3py.html

这篇关于如何使用 BitVector 建模有符号整数?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！