使用Z3的c++ api创建一个长Sum

Create a long Sum using the C++ api of Z3?

本文关键字：一个 Sum Z3 c++ api 创建 使用      更新时间：2023-10-16

创建具有可变数量的int的长Sum的首选方法是什么?

我猜是这样的:

expr mk_add(expr_vector args) {
    vector<Z3_ast> arr;
    for (int i = 0; i < (int)args.size(); i++)
        arr.push_back(args[i]);
    return to_expr(args.ctx(), Z3_mk_add(args.ctx(), arr.size(), &arr[0]));
}

这是正确的吗?

是的，看起来是正确的。只要记住要小心Z3_ast对象，因为它们的引用计数不会自动更新(这里to_expr应该负责)。

另一个不需要翻译的解决方案是:

expr mk_add(expr_vector args) {
    expr r = args[0];
    for (int i = 1; i < (int)args.size(); i++)
        r = to_expr(args.ctx(), r + args[i]);
    return r;
}
相关文章：