如何在c++中获取z3表达式的整数值

#include <z3++.h>

int main() {
    // 创建Z3上下文
    z3::context ctx;
    
    // 在这里编写代码
    // ...
    
    return 0;
}

// 创建整数常量表达式
z3::expr constant = ctx.int_val(42);

// 创建变量表达式
z3::expr x = ctx.int_const("x");

// 创建运算符表达式
z3::expr sum = x + constant;

// 创建求解器
z3::solver solver(ctx);

// 添加约束条件
solver.add(sum > 50);

// 检查约束是否可满足
if (solver.check() == z3::sat) {
    // 获取满足约束的模型
    z3::model model = solver.get_model();
    
    // 获取变量x的整数值
    z3::expr x_value = model.eval(x);
    
    // 打印整数值
    std::cout << "x = " << x_value << std::endl;
} else {
    std::cout << "No solution found." << std::endl;
}