C++中如何获取Z3 bit-vector表达式运算后的整数值

你当前的output是未简化的加法表达式，要得到对应的整数值，按照以下步骤操作即可：

常量表达式求值（你当前的场景适用） #

你的代码里两个操作数都是常量，直接调用simplify方法简化后即可转成整数：

// 简化表达式，得到常量形式的结果
expr simplified_output = output.simplify();
// 转换为无符号64位整数，预期得到8
uint64_t result = simplified_output.get_numeral_uint64();

如果你的bitvector是有符号类型，改用get_numeral_int64()方法即可。

完整可运行示例：

#include <z3++.h>
#include <cstdio>
using namespace z3;

int main() {
    context z3_ctx;
    expr Z3_LHS = z3_ctx.bv_val(0, 64);
    expr Z3_RHS = z3_ctx.bv_val(8, 64);
    expr output = Z3_LHS + Z3_RHS;

    expr simplified_res = output.simplify();
    // 先判断是否为数值常量，避免抛出异常
    if (simplified_res.is_numeral()) {
        uint64_t res = simplified_res.get_numeral_uint64();
        printf("计算结果：%llu\n", res);
    }
    return 0;
}

含符号变量的表达式求值 #

如果你的表达式中包含未赋值的符号变量，需要通过求解器得到满足约束的模型后再取值：

context z3_ctx;
// 定义符号变量x
expr x = z3_ctx.bv_const("x", 64);
expr y = z3_ctx.bv_val(8, 64);
expr output = x + y;

solver s(z3_ctx);
// 添加约束x=0
s.add(x == z3_ctx.bv_val(0, 64));

if (s.check() == sat) {
    model m = s.get_model();
    // 对output表达式在当前模型下求值
    expr res_expr = m.eval(output, true);
    uint64_t res = res_expr.get_numeral_uint64();
    // res的值为8
}

注意事项 #

• 调用get_numeral_uint64()/get_numeral_int64()前必须确保表达式是数值常量，你可以通过is_numeral()方法提前判断，避免触发异常
• 如果bitvector长度超过64位，可调用get_numeral_string()获取字符串格式的数值，再自行解析处理

内容的提问来源于stack exchange，提问作者hany erfan