在 z3 中使用位向量文本

Question

我正在通过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 位或更少，这不会有问题，但我需要支持更大的位向量长度。

Answer 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 *，将值作为十进制字符串。