C API для квантификаторов

Question

Я хочу решить ограничения, которые содержат квантификаторы, используя Z3 C API. Я изо всех сил пытаюсь использовать такие функции, как "Z3_mk_exists()", так как я не нахожу никаких примеров ни в сети, ни в тестовых примерах в файле tar. Я не совсем понимаю все аргументы, требуемые этими функциями, и их точное значение. Кто-нибудь может помочь?

Благодарю. Kaustubh.

Answer 1

Вот полный пример с универсальными квантификаторами. Комментарии встроены:

Z3_config cfg = Z3_mk_config();
Z3_set_param_value(cfg, "MODEL", "true");
Z3_context ctx = Z3_mk_context(cfg);
Z3_sort intSort = Z3_mk_int_sort(ctx);
/* Some constant integers */
Z3_ast zero  = Z3_mk_int(ctx, 0, intSort);
Z3_ast one   = Z3_mk_int(ctx, 1, intSort);
Z3_ast two   = Z3_mk_int(ctx, 2, intSort);
Z3_ast three = Z3_mk_int(ctx, 3, intSort);
Z3_ast four  = Z3_mk_int(ctx, 4, intSort);
Z3_ast five  = Z3_mk_int(ctx, 5, intSort);

Мы создаем неинтерпретированную функцию для Фибоначчи: fib(n), Мы уточним его значение с помощью универсального квантификатора.

Z3_func_decl fibonacci = Z3_mk_fresh_func_decl(ctx, "fib", 1, &intSort, intSort);

/* fib(0) and fib(1) */
Z3_ast fzero = Z3_mk_app(ctx, fibonacci, 1, &zero);
Z3_ast fone  = Z3_mk_app(ctx, fibonacci, 1, &one);

Мы начинаем указывать значение fib(n), Базовые случаи не требуют квантификаторов. У нас есть fib(0) = 0 а также fib(1) = 1,

Z3_ast fib0 = Z3_mk_eq(ctx, fzero, zero);
Z3_ast fib1 = Z3_mk_eq(ctx, fone,  one);

Это связанная переменная. Они используются в количественных выражениях. Индексы должны начинаться с 0, У нас есть только один в этом случае.

Z3_ast x = Z3_mk_bound(ctx, 0, intSort);

Это представляет fib(_), где _ является связанной переменной.

Z3_ast fibX = Z3_mk_app(ctx, fibonacci, 1, &x);

Шаблон - это то, что вызовет реализацию. Мы используем fib(_) снова. Это означает (более или менее), что Z3 будет создавать аксиому всякий раз, когда он видит fib("some term"),

Z3_pattern pattern = Z3_mk_pattern(ctx, 1, &fibX);

Насколько я понимаю, этот символ используется только для отладки. Это дает имя _,

Z3_symbol someName = Z3_mk_int_symbol(ctx, 0);

/* _ > 1 */
Z3_ast xGTone = Z3_mk_gt(ctx, x, one);
Z3_ast xOne[2] = { x, one };
Z3_ast xTwo[2] = { x, two };
/* _ - 1 */
Z3_ast fibXminusOne = Z3_mk_sub(ctx, 2, xOne);
/* _ - 2 */
Z3_ast fibXminusTwo = Z3_mk_sub(ctx, 2, xTwo);
Z3_ast toSum[2] = { Z3_mk_app(ctx, fibonacci, 1, &fibXminusOne), Z3_mk_app(ctx, fibonacci, 1, &fibXminusTwo) };
/* f(_ - 1) + f(_ - 2) */
Z3_ast fibSum = Z3_mk_add(ctx, 2, toSum);

Это теперь тело аксиомы. Это говорит: _ > 1 => (fib(_) = fib(_ - 1) + fib(_ - 2)где _ - связанная переменная.

Z3_ast axiomTree = Z3_mk_implies(ctx, xGTone, Z3_mk_eq(ctx, fibX, fibSum));

Наконец, мы можем построить дерево кванторов, используя шаблон, связанную переменную, ее имя и тело аксиомы. (Z3_TRUE говорит, что это полный квантификатор). 0 в списке аргументов указывается приоритет. Документ Z3 рекомендует использовать 0 если не знаешь что поставить.

Z3_ast fibN = Z3_mk_quantifier(ctx, Z3_TRUE, 0, 1, &pattern, 1, &intSort, &someName, axiomTree);

Наконец, мы добавляем аксиому (ы) в контекст.

Z3_assert_cnstr(ctx, fib0);
Z3_assert_cnstr(ctx, fib1);
Z3_assert_cnstr(ctx, fibN);