z3 - C API for Quantifiers

Question

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?

Thanks. Kaustubh.

Answer 1

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

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

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

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

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

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

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

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

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