量词的 C API [英] C API for Quantifiers

问题描述

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

I want to solve constraints that contain quantifiers using Z3 C API. I am struggling to use the functions like "Z3_mk_exists()" as I don't find any example either online or in the test examples in the tar file. I don't exactly understand all the arguments required by these functions and exact significance of them. Can anyone help?

谢谢.考斯图布.

推荐答案

这里是一个带有全称量词的完整示例.评论是内联的:

Here is a complete example with universal quantifiers. Comments are inline:

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

我们为 fibonacci 创建了一个未解释的函数:fib(n).我们将使用全称量词指定其含义.

We create an uninterpreted function for fibonacci: fib(n). We'll specify its meaning with a universal quantifier.

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.

We're starting to specify the meaning of fib(n). The base cases don't require quantifiers. We have fib(0) = 0 and fib(1) = 1.

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

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

This is a bound variable. They're used within quantified expressions. Indices should start from 0. We have only one in this case.

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

这表示 fib(_)，其中 _ 是绑定变量.

This represents fib(_), where _ is the bound variable.

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

模式将触发实例化.我们再次使用 fib(_).这意味着(或多或少)Z3 会在看到 fib("some term") 时实例化公理.

The pattern is what will trigger the instantiation. We use fib(_) again. This means (more or less) that Z3 will instantiate the axiom whenever it sees fib("some term").

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

据我所知，此符号仅用于调试.它为 _ 命名.

This symbol is only used for debugging as far as I understand. It gives a name to the _.

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

This is now the body of the axiom. It says: _ > 1 => (fib(_) = fib(_ - 1) + fib(_ - 2), where _ is the bound variable.

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

最后我们可以构建一个量词树，使用模式、绑定变量、它的名称和公理体.(Z3_TRUE 说它是一个 forall 量词).参数列表中的 0 指定优先级.如果您不知道该放什么，Z3 文档建议使用 0.

At last we can build a quantifier tree, using the pattern, the bound variable, its name and the axiom body. (Z3_TRUE says its a forall quantifier). The 0 in the argument list specifies the priority. The Z3 doc recommends to use 0 if you don't know what to put.

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

我们最终将公理添加到上下文中.

We finally add the axiom(s) the to context.

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

这篇关于量词的 C API的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！