z3 — выбор и сохранение массива с использованием API C ++
Я использую z3 v 4.1. Я использую C ++ API, и я пытаюсь добавить некоторые ограничения массива в контексте.
Я не вижу функций выбора и сортировки в C ++ API. Я попытался смешать C и C ++ API. В примере array_example1() предоставляется с C API, если я изменяю переменную контекста с Z3_Context (т.е. C API) для context (т.е. C ++ API) Я получаю ошибку сегментации в операторе «create antecedent»
void array_example1(){
context ctx; //Z3_context ctx;
Z3_sort int_sort, array_sort;
Z3_ast a1, a2, i1, v1, i2, v2, i3;
Z3_ast st1, st2, sel1, sel2;
Z3_ast antecedent, consequent;
Z3_ast ds[3];
Z3_ast thm;
printf("\narray_example1\n");
LOG_MSG("array_example1");
//ctx = mk_context();
int_sort = Z3_mk_int_sort(ctx);
array_sort = Z3_mk_array_sort(ctx, int_sort, int_sort);
a1 = mk_var(ctx, "a1", array_sort);
a2 = mk_var(ctx, "a2", array_sort);
i1 = mk_var(ctx, "i1", int_sort);
i2 = mk_var(ctx, "i2", int_sort);
i3 = mk_var(ctx, "i3", int_sort);
v1 = mk_var(ctx, "v1", int_sort);
v2 = mk_var(ctx, "v2", int_sort);
st1 = Z3_mk_store(ctx, a1, i1, v1);
st2 = Z3_mk_store(ctx, a2, i2, v2);
sel1 = Z3_mk_select(ctx, a1, i3);
sel2 = Z3_mk_select(ctx, a2, i3);
/* create antecedent */
antecedent = Z3_mk_eq(ctx, st1, st2);
/* create consequent: i1 = i3 or i2 = i3 or select(a1, i3) = select(a2, i3) */
ds[0] = Z3_mk_eq(ctx, i1, i3);
ds[1] = Z3_mk_eq(ctx, i2, i3);
ds[2] = Z3_mk_eq(ctx, sel1, sel2);
consequent = Z3_mk_or(ctx, 3, ds);
/* prove store(a1, i1, v1) = store(a2, i2, v2) implies (i1 = i3 or i2 = i3 or select(a1, i3) = select(a2, i3)) */
thm = Z3_mk_implies(ctx, antecedent, consequent);
printf("prove: store(a1, i1, v1) = store(a2, i2, v2) implies (i1 = i3 or i2 = i3 or select(a1, i3) = select(a2, i3))\n");
printf("%s\n", Z3_ast_to_string(ctx, thm));
prove(ctx, thm, Z3_TRUE);
}
Я также пытался конвертировать st1 а также st2 от Z3_AST в expr и затем приравнивая их, но я все еще получаю ошибку сегментации. Как использовать выбор и сохранение с использованием API C ++?
Решение
Z3 имеет два режима управления памятью: push / pop и подсчет ссылок. Подсчет ссылок был введен гораздо позже. Метод C API, используемый для создания Z3_Context определяет, какой режим управления памятью будет использоваться. API Z3_mk_context создает контекст, в котором push/pop политика используется. То есть объекты AST удаляются при Z3_pop вызывается. Любой объект AST, созданный между соответствующими Z3_push будут удалены. Эта политика проста в использовании, но она может помешать вашему приложению освободить неиспользуемую память. API Z3_mk_context_rc создает контекст, в котором подсчет ссылок используется для восстановления памяти. Это официальный подход в Z3 4.x. Более того, новые объекты (например, тактика, решатели, цели), представленные в Z3 4.x, только поддерживают этот подход.
Если вы используете API C ++, C #, OCaml или Python. Тогда очень просто использовать новую политику подсчета ссылок. С другой стороны, C API труднее использовать, потому что мы должны явно вызывать Z3_*inc_ref а также Z3_*dec_ref API-интерфейсы. Если мы пропустим один из них, у нас могут произойти сбои (как в вашем примере) или утечки памяти.
В C ++ API мы предоставляем несколько «умных указателей», которые автоматически управляют счетчиками ссылок для нас.
Ваш пример вылетает, потому что вы заменили Z3_context ctx с context ctx, Конструктор класса context использования Z3_mk_context_rc вместо Z3_context, Файл example.cpp в каталоге c ++ демонстрирует, как комбинировать API C ++ и C (см. функцию capi_example()). В этом примере интеллектуальный указатель C ++ используется для переноса объектов C, возвращаемых API C.
Наконец, API C ++ предоставил следующие функции для создания выражений массива:
inline expr select(expr const & a, expr const & i) {
check_context(a, i);
Z3_ast r = Z3_mk_select(a.ctx(), a, i);
a.check_error();
return expr(a.ctx(), r);
}
inline expr select(expr const & a, int i) { return select(a, a.ctx().num_val(i, a.get_sort().array_domain())); }
inline expr store(expr const & a, expr const & i, expr const & v) {
check_context(a, i); check_context(a, v);
Z3_ast r = Z3_mk_store(a.ctx(), a, i, v);
a.check_error();
return expr(a.ctx(), r);
}
inline expr store(expr const & a, int i, expr const & v) { return store(a, a.ctx().num_val(i, a.get_sort().array_domain()), v); }
inline expr store(expr const & a, expr i, int v) { return store(a, i, a.ctx().num_val(v, a.get_sort().array_range())); }
inline expr store(expr const & a, int i, int v) {
return store(a, a.ctx().num_val(i, a.get_sort().array_domain()), a.ctx().num_val(v, a.get_sort().array_range()));
}
Другие решения
Других решений пока нет …