使用C++ API創建數組exprr

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. 

我的問題是：有沒有創建一個數組A1的另一種方式，不使用C API？ C++ api是否提供了從A創建a1的功能？

Answer 1

您可以使用該方法

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

它可以被用來創建給定類的常量（也稱爲變量）。這裏是一個例子：

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