在 Z3 中使用位向量文字

【问题标题】：Using Bit-Vector Literal in Z3在 Z3 中使用位向量文字
【发布时间】：2020-01-27 20:38:51
【问题描述】：

我开始使用带有 C++ API 的 Z3，我主要对使用它对位向量的支持感兴趣。

但是，我完全无法弄清楚如何将位向量文字与表达式结合使用。

这是我想要完成的基本任务：

context z3_ctx;
solver  z3_solver(z3_ctx);
optimize z3_optimizer(z3_ctx);
expr x = z3_ctx.bv_const("x", 256);
z3_solver.add(x == "#x4123"); // Need help here

没有在线示例显示我如何完成这个简单的任务。如果我的位向量只有 64 位或更少，这不会有问题，但我需要支持更大的位向量长度。

【问题讨论】：

标签： c++ constraints z3 constraint-programming

【解决方案1】：

使用bv_val：https://z3prover.github.io/api/html/classz3_1_1context.html#a2bda3f1857cc76d49ca6f3653c02ff44

它带有 6 种重载，适用于您可能开始的各种事情。 int、unsigned、int64_t、uint64_t 甚至 char const * 等。在这种情况下，您希望 char const * 重载，将值作为十进制字符串。

【讨论】：

有没有办法立即输入十六进制或二进制字符串？好像我需要一个十六进制到整数字符串转换器。
除非它适合重载之一。最重要的是，您必须调用 bv_val 之类的东西，以便它可以确定您希望该文字的宽度。您可以为您的用例（128 位等）编写一些辅助函数，但有时您必须自己进行字符串转换。
总比没有好，我猜。感谢您的帮助。