用於量詞的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)); 

最後我們可以使用模式，綁定變量，名稱和公理體建立一個量詞樹。 （​​稱其爲量子）。參數列表中的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);