当前位置：文江博客话题详情

是否可以选择将位向量漂亮地打印为有符号小数？

发布于 2024-12-17 17:01:05 字数 31 浏览 2 评论 0原文

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

原文

分享到QQ

分享到微博

如果你对这篇内容有疑问，欢迎到本站社区发帖提问参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。

发布评论

需要登录才能够评论，你可以免费注册一个本站的账号。

你怎么这么可爱啊 2024-12-24 17:01:05

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

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

Z3 将打印

#x00f8
(_ bv248 16)

Z3 不支持有符号小数。我们可以添加一个选项，如果 n 的最高有效位为 (bvneg (_ bv)，则将位向量 n 显示为 (bvneg (_ bv) 是 1。这足以满足您的目的吗？

You can use the command (set-option :pp-bv-literals false) to force Z3 to display the bit-vector literals in a decimal based format. Actually, it will display them using the SMT 2.0 format: (_ bv<decimal> <size>). Consider the following example:

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

Z3 will print

#x00f8
(_ bv248 16)

Z3 has no support for signed decimals. We can add an option to display a bit-vector n as (bvneg (_ bv<decimal> <size>) if the most significant bit of n is 1. Is this enough for your purposes?

回复收藏 0 原文

~没有更多了~