Z3のC++ APIを使用して長いSumを作成しますか？

Question

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

これが正しい：

私の推測では、このようなものでしょうか？

Answer 1

はい、正しく表示されます。 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; 
} 

：

C++ API内に留まると厄介な翻訳を必要としない別の解決策はこれです