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

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

我在 C++ API 中没有看到选择和排序函数。我尝试混合使用 C 和 C++ API。在示例中array_example1()如果我将上下文变量从Z3_Context（即 C API）到context（即 C++ API）我在“创建先行词”语句中遇到分段错误

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 and st2 from Z3_AST to expr然后将它们等同，但我仍然遇到分段错误。如何使用 C++ API 进行选择和存储？

Z3有两种内存管理模式：push/pop和引用计数。引用计数是很晚才引入的。用于创建的 C API 方法Z3_Context定义将使用哪种内存管理模式。应用程序编程接口Z3_mk_context创建一个上下文，其中push/pop使用策略。也就是说，AST 对象在以下情况下被删除：Z3_pop被调用。匹配之间创建的任何 AST 对象Z3_push将被删除。此策略使用起来很简单，但它可能会阻止您的应用程序释放未使用的内存。应用程序编程接口Z3_mk_context_rc创建一个上下文，其中引用计数用于回收内存。这是 Z3 4.x 中的官方方法。此外，Z3 4.x 中引入的新对象（例如，战术、求解器、目标）仅支持这种方法。 如果您使用 C++、C#、OCaml 或 Python API。然后，使用新的引用计数策略就非常简单了。另一方面，C API 更难使用，因为我们必须显式调用Z3_*inc_ref and Z3_*dec_ref蜜蜂。如果我们错过其中之一，我们可能会发生崩溃（如您的示例）或内存泄漏。 在C++ API中，我们提供了几个“智能指针”来自动为我们管理引用计数器。

你的例子崩溃了，因为你替换了Z3_context ctx with context ctx。类的构造函数context uses Z3_mk_context_rc代替Z3_context。文件example.cppc++ 目录中演示了如何结合 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())); 
}