使用Z3的C++ api創建一個長和？

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應該注意這一點）。

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