Создать длинную сумму, используя C ++ API Z3?
Что было бы предпочтительным способом создания длинной суммы с переменным числом ints?
Я думаю, что-то вроде этого:
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 должен позаботиться об этом).
Другое решение, которое остается в C ++ API и не нуждается в неловких переводах:
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;
}
Другие решения
Других решений пока нет …