c++ - 使用 C++ API 创建数组 expr

Question

为了通过 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.

我的问题是:是否有另一种方法可以在不使用 C api 的情况下创建数组 a1？ C++ api 是否提供从 A 创建 a1 的函数？

Answer 1

可以使用方法

expr constant(char const * name, sort const & s);

它可用于创建给定类别的常量(又名变量)。这是一个例子:

expr a1 = c.constant("a1", A);