数组的选择和存储使用C ++ API [英] Array select and store using the C++ API

问题描述

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

I am using z3 v 4.1. I am using the C++ API and I am trying to add some array constraints in the context.

我没有看到C ++ API中的选择和排序功能。我试过混合C和C ++ API。在例如从 Z3_Context （即C API）更改上下文变量的C API中提供的 array_example1（） 上下文（即C ++ API）在创建先行语句中获得分段错误

I dont see the select and sort functions in the C++ API. I tried mixing of the C and C++ API. In the example array_example1() provided with the C API if I change the context variable from Z3_Context (i.e. C API) to context (i.e. C++ API) I get a segmentation fault at the "create antecedent" statement

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进行选择和存储？

I also tried converting st1 and st2 from Z3_AST to expr and then equating them but I still get the segmentation fault. How do I use select and store using the C++ API?

推荐答案

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 has two memory management modes: push/pop and reference counting. Reference counting was introduced much later. The C API method used to create the Z3_Context defines which memory management mode will be used. The API Z3_mk_context creates a context where a push/pop policy is used. That is, AST objects are deleted when Z3_pop is invoked. Any AST object created between the matching Z3_push will be deleted. This policy is simple to use, but it may prevent your application from freeing unused memory. The API Z3_mk_context_rc creates a context where reference counting is used to reclaim memory. This is the official approach in Z3 4.x. Moreover, new objects (e.g., tactics, solvers, goals) introduced in Z3 4.x only support this approach. If you are using C++, C#, OCaml, or Python APIs. Then, it is very simple to use the new reference counting policy. On the other hand, the C API is harder to use because we have to explicitly invoke the Z3_*inc_ref and Z3_*dec_ref APIs. If we miss one of them, we can have crashes (as in your example) or memory leaks. In the C++ API, we provide several "smart pointers" that manage the reference counters automatically for us.

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

Your example crashes because you replaced Z3_context ctx with context ctx. The constructor of the class context uses Z3_mk_context_rc instead of Z3_context. The file example.cpp in the c++ directory demonstrates how to combine the C++ and C APIs (see function capi_example()). In this example, the C++ smart pointer are used to wrap the C objects returned by the C API.

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

Finally, the C++ API provided the following functions for creating array expressions:

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的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！