1

为了通过 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 的函数?

4

1 回答 1

1

您可以使用该方法

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

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

expr a1 = c.constant("a1", A);
于 2013-07-22T10:06:59.887 回答