Search code examples
c++constraintsz3constraint-programming

Using Bit-Vector Literal in Z3

I'm getting started using Z3 with the C++ API, and I'm primarily interested in using its support for bit-vectors.

However, I'm completely stumped in trying to figure out how I can make use of bit-vector literals with expressions.

Here's the basics of what I'm trying to accomplish:

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

There's no online examples showing how I can accomplish this simple task. If my bit vectors were merely 64-bits or less, this wouldn't be a problem, but I require support for greater bit vector lengths.

Solution

  • Use bv_val: https://z3prover.github.io/api/html/classz3_1_1context.html#a2bda3f1857cc76d49ca6f3653c02ff44

    It comes with 6 overloadings, for all sorts of things you might start from. int, unsigned, int64_t, uint64_t, and even char const * etc. In this case, you want the char const * overloading, putting the value as a decimal string.