Использование битового вектора в Z3

Question

Я начинаю использовать Z3 с C ++ API, и я в первую очередь заинтересован в использовании его поддержки битовых векторов.

Однако я совершенно туп, пытаясь понять, как я может использовать битовые векторные литералы с выражениями.

Вот основы того, что я пытаюсь выполнить sh:

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

Нет онлайн-примеров, показывающих, как я могу выполнить sh это простое задание. Если бы мои битовые векторы были просто 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 * et c. В этом случае вы хотите перегрузку char const *, поместив значение в виде десятичной строки.