z3 — создание массива expr с использованием API C ++

Question

z3 — создание массива expr с использованием API C ++

Чтобы создать массив с помощью API z3 c ++, я провел поиск в Интернете. Лучший подход, который я могу найти:

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? Предоставляет ли API C ++ функцию для создания a1 из A?

1

c++z3

Решение

Другие решения

Других решений пока нет …

Источник

Accepted Answer

Вы можете использовать метод

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

Он может быть использован для создания констант (или переменных) данного вида. Вот пример:

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

1