量词的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说它是一个forall量词).在0参数列表中指定的优先级.0如果您不知道放什么,Z3 doc建议使用.

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