Создайте длинную сумму, используя C++ api Z3?

Question

Что было бы предпочтительным способом создания длинной суммы с переменным числом int s?

Я думаю, что-то вроде этого:

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

Правильно ли это?

Answer 1

Да, это выглядит правильно. Не забывайте быть осторожным с объектами Z3_ast, так как их подсчет ссылок не обновляется автоматически (здесь to_expr должен позаботиться об этом).

Другим решением, которое остается в пределах API C++ и не требует громоздких перевода заключается в следующем:

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