使用C++ API進行數組選擇和存儲

我正在使用z3 v 4.1。我正在使用C++ API，我正試圖在上下文中添加一些數組約束。使用C++ API進行數組選擇和存儲

我沒有看到C++ API中的選擇和排序功能。我嘗試了C和C++ API的混合。在設置有C API如果我改變從Z3_Context（即C API）的上下文變量來context（即C++ API）的例子array_example1()我得到在「創建先行詞」分割故障聲明

void array_example1(){ 

context ctx; //Z3_context ctx; 
Z3_sort int_sort, array_sort; 
Z3_ast a1, a2, i1, v1, i2, v2, i3; 
Z3_ast st1, st2, sel1, sel2; 
Z3_ast antecedent, consequent; 
Z3_ast ds[3]; 
Z3_ast thm; 

printf("\narray_example1\n"); 
LOG_MSG("array_example1"); 

//ctx = mk_context(); 

int_sort = Z3_mk_int_sort(ctx); 
array_sort = Z3_mk_array_sort(ctx, int_sort, int_sort); 

a1   = mk_var(ctx, "a1", array_sort); 
a2   = mk_var(ctx, "a2", array_sort); 
i1   = mk_var(ctx, "i1", int_sort); 
i2   = mk_var(ctx, "i2", int_sort); 
i3   = mk_var(ctx, "i3", int_sort); 
v1   = mk_var(ctx, "v1", int_sort); 
v2   = mk_var(ctx, "v2", int_sort); 

st1   = Z3_mk_store(ctx, a1, i1, v1); 
st2   = Z3_mk_store(ctx, a2, i2, v2); 

sel1  = Z3_mk_select(ctx, a1, i3); 
sel2  = Z3_mk_select(ctx, a2, i3); 

/* create antecedent */ 
antecedent = Z3_mk_eq(ctx, st1, st2); 

/* create consequent: i1 = i3 or i2 = i3 or select(a1, i3) = select(a2, i3) */ 
ds[0]  = Z3_mk_eq(ctx, i1, i3); 
ds[1]  = Z3_mk_eq(ctx, i2, i3); 
ds[2]  = Z3_mk_eq(ctx, sel1, sel2); 
consequent = Z3_mk_or(ctx, 3, ds); 

/* prove store(a1, i1, v1) = store(a2, i2, v2) implies (i1 = i3 or i2 = i3 or select(a1, i3) = select(a2, i3)) */ 
thm   = Z3_mk_implies(ctx, antecedent, consequent); 
printf("prove: store(a1, i1, v1) = store(a2, i2, v2) implies (i1 = i3 or i2 = i3 or select(a1, i3) = select(a2, i3))\n"); 
printf("%s\n", Z3_ast_to_string(ctx, thm)); 
prove(ctx, thm, Z3_TRUE); 

}

我還嘗試將st1和st2從Z3_AST轉換爲expr，然後將它們等同，但仍然出現分段錯誤。如何使用C++ API使用select和store？

來源

2012-10-21 sarvesh prabhu

Z3有兩種內存管理模式：push/pop和引用計數。引用計數很晚才引入。用於創建Z3_Context的C API方法定義將使用哪種內存管理模式。 API Z3_mk_context創建使用push/pop策略的上下文。也就是說，當調用Z3_pop時，AST對象被刪除。在匹配的Z3_push之間創建的任何AST對象都將被刪除。此策略使用起來很簡單，但它可能會阻止您的應用程序釋放未使用的內存。 API Z3_mk_context_rc創建了一個使用引用計數來回收內存的上下文。這是Z3 4.x中的官方方法。此外，Z3 4.x中引入的新對象（例如戰術，解算器，目標）僅支持這種方法。如果您使用C++，C＃，OCaml或Python API。然後，使用新的引用計數策略非常簡單。另一方面，C API很難使用，因爲我們必須明確調用Z3_*inc_ref和Z3_*dec_ref API。如果我們錯過其中一個，我們可能會崩潰（如你的例子）或內存泄漏。在C++ API中，我們提供了幾個可自動管理引用計數器的「智能指針」。

您的示例崩潰，因爲您用context ctx替換Z3_context ctx。類context的構造函數使用Z3_mk_context_rc而不是Z3_context。 C++目錄中的文件example.cpp演示瞭如何組合C++和C API（請參閱函數capi_example()）。在這個例子中，C++智能指針用於包裝C API返回的C對象。

inline expr select(expr const & a, expr const & i) { 
    check_context(a, i); 
    Z3_ast r = Z3_mk_select(a.ctx(), a, i); 
    a.check_error(); 
    return expr(a.ctx(), r); 
} 
inline expr select(expr const & a, int i) { return select(a, a.ctx().num_val(i, a.get_sort().array_domain())); } 
inline expr store(expr const & a, expr const & i, expr const & v) { 
    check_context(a, i); check_context(a, v); 
    Z3_ast r = Z3_mk_store(a.ctx(), a, i, v); 
    a.check_error(); 
    return expr(a.ctx(), r); 
} 
inline expr store(expr const & a, int i, expr const & v) { return store(a, a.ctx().num_val(i, a.get_sort().array_domain()), v); } 
inline expr store(expr const & a, expr i, int v) { return store(a, i, a.ctx().num_val(v, a.get_sort().array_range())); } 
inline expr store(expr const & a, int i, int v) { 
    return store(a, a.ctx().num_val(i, a.get_sort().array_domain()), a.ctx().num_val(v, a.get_sort().array_range())); 
}

：

最後，C++ API用於創建數組表達式提供以下功能

來源

2012-10-21 06:05:21

使用C++ API進行數組選擇和存儲

回答

相關問題