z3 - 量词的 C API

Question

我想使用 Z3 C API 解决包含量词的约束。
我正在努力使用诸如“Z3_mk_exists()”之类的函数，因为我在网上或 tar 文件的测试示例中都找不到任何示例。
我并不完全理解这些函数所需的所有参数以及它们的确切意义。
任何人都可以帮忙吗？

谢谢。
考斯图布。

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);

这是一个绑定(bind)变量。它们在量化表达式中使用。索引应从 0 开始.在这种情况下，我们只有一个。

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

这代表 fib(_) , 其中 _是绑定(bind)变量。

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) ，其中 _ 是绑定(bind)变量。

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

最后，我们可以构建一个量词树，使用模式、绑定(bind)变量、它的名称和公理体。 ( 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);