z3 - 是否可以将位向量打印为有符号小数？

Question

如何在 Z3 中将位向量漂亮地打印为带符号的小数？

Answer 1

您可以使用该命令(set-option :pp-bv-literals false)强制 Z3 以基于十进制的格式显示位向量文字。实际上，它将使用 SMT 2.0 格式显示它们：(_ bv<decimal> <size>). 考虑以下示例：

(simplify #x00f8)
(set-option :pp-bv-literals false)
(simplify #x00f8)

Z3 将打印

#x00f8
(_ bv248 16)

Z3 不支持有符号小数。我们可以添加一个选项来显示位向量n，就(bvneg (_ bv<decimal> <size>)好像最高有效位n是 1。这足以满足您的目的吗？