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

Question

Я хочу решить ограничения, содержащие кванторы, используя API Z3 C. Я изо всех сил пытаюсь использовать такие функции, как «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 говорит, что его квантификатор forall). В списке аргументов 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);