Z3 c ++ api массив подстановки

Question

Z3 c ++ api массив подстановки

Я пытаюсь использовать подстановку в выражении, содержащем массив и целое число. Я получаю ошибку сегментации после замены.

Вот код:

    context cxt;
vector<Z3_ast> vars_ast,primed_vars_ast;

sort Int = cxt.int_sort();
sort Array = cxt.array_sort(Int,Int);

expr arr =cxt.constant("arr",Array);
vars_ast.push_back(arr);expr i =cxt.int_const("i");
vars_ast.push_back(i);expr test_expr = select(arr,i)==0 ;

primed_vars_ast.push_back(cxt.constant("arr_primed",Array));
primed_vars_ast.push_back(cxt.int_const("i_primed"));

expr cstr_expr (cxt,
ast(cxt,
Z3_substitute(cxt,
ast(test_expr),
vars_ast.size(),
vars_ast.data(),
primed_vars_ast.data())));

Однако, если я удалю переменную i из массивов ast, и вместо этого проверить подстановку на выражение test_expr = select(arr,1)==0, это удается.
Я что-то пропустил?

1

arrays c++substitution z3

Решение

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

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

Источник

Accepted Answer

Проблема в том, что вы смешиваете код на C и C ++ (z3.h и z3 ++. H). Z3 C-API не будет подсчитывать ссылки за вас, поэтому вам нужно позвонить Z3_inc_ref каждый раз, когда вы создаете Z3_ast а также Z3_dec_ref каждый раз Z3_ast выходит за рамки / использование.

Основная цель C ++ API (z3 ++. H) — абстрагировать код подсчета ссылок, но это работает только до тех пор, пока вы не смешиваете код на C. Основное правило: если функция называется «Z3_ *», то это функция C, и если она возвращает Z3_astположить его в expr сразу, например, так:

expr q(cxt, Z3_mk_select(cxt, arr, i));

В этом конкретном примере мы можем изменить vector<Z3_ast> для expr_vector (поставляется с z3 ++. h). Пример можно затем изменить на

context cxt;
expr_vector vars_ast(cxt), primed_vars_ast(cxt);

sort Int = cxt.int_sort();
sort Array = cxt.array_sort(Int,Int);

expr arr = cxt.constant("arr",Array);
vars_ast.push_back(arr);

expr i = cxt.int_const("i");
vars_ast.push_back(i);

expr test_expr = select(arr,i)==0;

primed_vars_ast.push_back(cxt.constant("arr_primed",Array));
primed_vars_ast.push_back(cxt.int_const("i_primed"));

test_expr.substitute(vars_ast, primed_vars_ast);

3