使用 C++ API 选择和存储数组

Question

我正在使用 z3 v 4.1。我正在使用 C++ API，并尝试在上下文中添加一些数组约束。

我没有在 C++ API 中看到选择和排序函数。我尝试混合使用 C 和 C++ API。在 C API 提供的示例 array_example1() 中，如果我将上下文变量从 Z3_Context（即 C API）更改为 context（即 C++ API），我会在“create antecedent”语句中遇到分段错误

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？

Answer 1

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 中，我们提供了几个“智能指针”来自动为我们管理引用计数器。

您的示例崩溃了，因为您将 Z3_context ctx 替换为 context ctx。类context 的构造函数使用Z3_mk_context_rc 而不是Z3_context。 c++ 目录中的文件example.cpp 演示了如何组合C++ 和C API（参见函数capi_example()）。在此示例中，C++ 智能指针用于包装 C API 返回的 C 对象。

最后，C++ API 提供了以下用于创建数组表达式的函数：

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