在Z3中使用位向量立即数

Question

我正开始将Z3与C ++ API一起使用，并且我主要对使用其对位向量的支持感兴趣。

但是，我完全无法理解如何使用带表达式的位向量文字。

这是我要完成的工作的基础：

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