Pedro Souto Pedro Souto - 21 days ago 5
C++ Question

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

What would be the preferred way to create a long Sum with a variable number of

int
s?

My guess is something like this:

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]));
}


Is this Correct?

Answer

Yes, that looks correct. Just remember to be careful with Z3_ast' objects as their reference counts are not updated automatically (hereto_expr' should take care of that).

Another solution that stays within the C++ API and doesn't need awkward translations is this:

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;
}