Difference between `Z3_mk_forall` and `Z3_mk_forall_const` in C API for Z3?

Question

I am confused by the 2 functions. They seem to take about the same set of arguments (one straightforwardly convertible to another) and each returns an AST. Do the functions do the same thing? If not, when do I need each?

Signatures of the 2:

Z3_ast Z3_mk_forall (Z3_context c,
                     unsigned weight,
                     unsigned num_patterns,
                     Z3_pattern const patterns[],
                     unsigned num_decls,
                     Z3_sort const sorts[],
                     Z3_symbol const decl_names[],
                     Z3_ast body)

Z3_ast Z3_mk_forall_const (Z3_context c,
                           unsigned weight,
                           unsigned num_bound,
                           Z3_app const bound[],
                           unsigned num_patterns,
                           Z3_pattern const patterns[],
                           Z3_ast body)

Answer 1

Yes, the Z3 team has provided multiple ways to do the same thing. The principle difference is that Z3_mk_forall_const takes a list of constants that have been defined using the normal mechanisms, while Z3_mk_forall requires a list of bound variables created using Z3_mk_bound.

Which mechanism is easier to use will depend on your specific application. In particular, it seems to me that Z3_mk_forall_const will be more natural when there is a small, fixed number of symbols over which you want to build a quantifier. Conversely, Z3_mk_forall will probably be more natural in the situation where the number of symbols in the quantifier might vary, in which case it's quite natural to generate an array of bound variables that you'll address with indices.

There are other advantages and disadvantages as well. For example, see this question: "How to declare constants to use as bound variables in Z3_mk_forall_const?" In that question, the asker wants to avoid introducing a lot of variables into their global context, which will be necessary to use Z3_mk_forall_const. The answerer (Christoph) suggests using Z3_mk_forall instead, but this is not ideal either, because for nested quantifiers this will result in each quantifier being indexed differently. Christoph also reveals in that answer that internally, the approach based on Z3_mk_forall_const is translated to something equivalent to Z3_mk_forall, so under the hood there is really no difference. The API differences, however, can make a big difference to the programmer.

There is also a (much simpler) mechanism provided to the programmer in the C++ API, if you are able to use that. Here are examples using the three different methods:

// g++ --std=c++11 z3-quantifier-support.cpp -I../src/api/ -I../src/api/c++/ libz3.so

#include <stdio.h>
#include "z3.h"

#include <iostream>
#include "z3++.h"

using namespace z3;

/**
 * This is by far the most concise and easiest to use if the C++ API is available to you.
 */
void example_cpp_forall() {
    context c;
    expr a = c.int_const("a");
    expr b = c.int_const("b");
    expr x = c.int_const("x");
    expr axiom = forall(x, implies(x <= a, x < b));
    std::cout << "Result obtained using the C++ API with forall:\n" << axiom << "\n\n";
}

/**
 * Example using Z3_mk_forall_const. Not as clean as the C++ example, but this was still
 * significantly easier for me to get working than the example using Z3_mk_forall().
 */
void example_c_Z3_mk_forall_const() {
    // Get the context
    Z3_config cfg;
    Z3_context ctx;
    cfg = Z3_mk_config();
    ctx = Z3_mk_context(cfg);

    // Declare integers a, b, and x
    Z3_sort I = Z3_mk_int_sort(ctx);
    Z3_symbol a_S = Z3_mk_string_symbol(ctx, "a");
    Z3_symbol b_S = Z3_mk_string_symbol(ctx, "b");
    Z3_symbol x_S = Z3_mk_string_symbol(ctx, "x");
    Z3_ast a_A = Z3_mk_const(ctx, a_S, I);
    Z3_ast b_A = Z3_mk_const(ctx, b_S, I);
    Z3_ast x_A = Z3_mk_const(ctx, x_S, I);

    // Build the AST (x <= a) --> (x < b)
    Z3_ast x_le_a = Z3_mk_le(ctx, x_A, a_A);
    Z3_ast x_lt_b = Z3_mk_lt(ctx, x_A, b_A);
    Z3_ast f = Z3_mk_implies(ctx, x_le_a, x_lt_b);
    Z3_app vars[] = {(Z3_app) x_A};
    Z3_ast axiom = Z3_mk_forall_const(ctx, 0, 1, vars, 0, 0, f);

    printf("Result obtained using the C API with Z3_mk_forall_const:\n");
    printf("%s\n\n", Z3_ast_to_string(ctx, axiom));
}

/**
 * Example using Z3_mk_forall. For the example, this is the most cumbersome.
 */
void example_c_Z3_mk_forall() {

    // Get the context
    Z3_config cfg;
    Z3_context ctx;
    cfg = Z3_mk_config();
    ctx = Z3_mk_context(cfg);

    // Declare integers a and b
    Z3_sort I = Z3_mk_int_sort(ctx);
    Z3_symbol a_S = Z3_mk_string_symbol(ctx, "a");
    Z3_symbol b_S = Z3_mk_string_symbol(ctx, "b");
    Z3_ast a_A = Z3_mk_const(ctx, a_S, I);
    Z3_ast b_A = Z3_mk_const(ctx, b_S, I);

    // Declare bound variables, in this case, just x
    Z3_symbol x_S = Z3_mk_string_symbol(ctx, "x");
    Z3_ast x_A = Z3_mk_bound(ctx, 0, I);

    // Z3_mk_forall requires all names, types, and bound variables to be provided in
    // arrays. In this example, where there is only one quantified variable, this seems a
    // bit cumbersome. If we were dealing with an varying number of quantified variables,
    // then this would seem more reasonable.
    const unsigned sz = 1;
    const Z3_sort types[] = {I};
    const Z3_symbol names[] = {x_S};
    const Z3_ast xs[] = {x_A};

    // Build the AST (x <= a) --> (x < b)
    Z3_ast x_le_a = Z3_mk_le(ctx, x_A, a_A);
    Z3_ast x_lt_b = Z3_mk_lt(ctx, x_A, b_A);
    Z3_ast f = Z3_mk_implies(ctx, x_le_a, x_lt_b);

    // In the Z3 docs for Z3_mk_pattern, the following sentence appears: "If a pattern is
    // not provided for a quantifier, then Z3 will automatically compute a set of
    // patterns for it." So I tried supplying '0' for the number of patterns, and 'NULL'
    // for the list of patterns, and Z3_mk_forall still seems to function.
    Z3_ast axiom = Z3_mk_forall(ctx, 0, 0, NULL, sz, types, names, f);

    printf("Result obtained using the C API with Z3_mk_forall:\n");
    printf("%s\n", Z3_ast_to_string(ctx, axiom));
}

int main() {
    example_cpp_forall();
    example_c_Z3_mk_forall_const();
    example_c_Z3_mk_forall();
}

I also found these questions helpful:

• "for all quantifier in Z3"
  
• "C API for Quantifiers"
  
• "Z3 quantifier support"
  

The examples and comments provided in the Z3 source were also helpful, expecially in examples/c/test_capi.c, examples/c++/example.cpp, and src/api/z3_api.h.