3

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

我在 C++ API 中看不到选择和排序函数。我尝试混合使用 C 和 C++ API。array_example1()在C API 提供的示例中，如果我将上下文变量从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 使用选择和存储？

4

1 回答 1

2

Z3 有两种内存管理模式：push/pop 和引用计数。引用计数是在很久以后才引入的。用于创建的 C API 方法Z3_Context定义将使用哪种内存管理模式。APIZ3_mk_context创建一个push/pop使用策略的上下文。也就是说，AST 对象在Z3_pop被调用时被删除。在匹配之间创建的任何 AST 对象Z3_push都将被删除。此策略易于使用，但它可能会阻止您的应用程序释放未使用的内存。APIZ3_mk_context_rc创建一个使用引用计数来回收内存的上下文。这是 Z3 4.x 中的官方方法。此外，Z3 4.x 中引入的新对象（例如，战术、求解器、目标）仅支持这种方法。如果您使用 C++、C#、OCaml 或 Python API。然后，使用新的引用计数策略就非常简单了。另一方面，C API 更难使用，因为我们必须显式调用Z3_*inc_refandZ3_*dec_refAPI。如果我们错过其中一个，我们可能会发生崩溃（如您的示例）或内存泄漏。在 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())); 
}
于 2012-10-21T06:05:21.947 回答