为了通过 z3 c++ api 创建一个数组,我在互联网上进行了一些搜索。我能找到的最好的方法是:
context c;
sort I = c.int_sort();
sort A = c.array_sort(I, I);
expr a1 = to_expr(c, mk_var(c, "a1", A)); //this is wrapper to use the C api in my C++ code
expr b1 = store(a1, 3, 4); //then I can apply to a1 the store and select functions provided in the C++ api.
我的问题是:是否有另一种方法来创建数组 a1,而不使用 C api?C++ api 是否提供从 A 创建 a1 的函数?