Разница между `Z3_mk_forall` и`Z3_mk_forall_const` в C API для Z3?

Question

Я смущен 2 функциями. Кажется, что они принимают примерно один и тот же набор аргументов (один напрямую преобразуется в другой), и каждый возвращает AST. Функции делают то же самое? Если нет, то когда мне каждый нужен?

Подписи 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

Да, команда Z3 предоставила несколько способов сделать то же самое. Принципиальное отличие состоит в том, что Z3_mk_forall_const принимает список констант, которые были определены с использованием обычных механизмов, в то время как Z3_mk_forall требуется список связанных переменных, созданных с использованием Z3_mk_bound,

Какой механизм проще использовать, зависит от вашего конкретного применения. В частности, мне кажется, что Z3_mk_forall_const будет более естественным, когда есть небольшое фиксированное количество символов, над которыми вы хотите построить квантификатор. Наоборот, Z3_mk_forall вероятно, будет более естественным в ситуации, когда число символов в квантификаторе может изменяться, и в этом случае вполне естественно генерировать массив связанных переменных, к которым вы будете обращаться с индексами.

Есть и другие преимущества и недостатки. Например, посмотрите на этот вопрос: "Как объявить константы для использования в качестве связанных переменных в Z3_mk_forall_const?" В этом вопросе спрашивающий хочет избежать введения большого количества переменных в их глобальный контекст, который будет необходимо использовать Z3_mk_forall_const, Ответчик (Кристоф) предлагает использовать Z3_mk_forall вместо этого, но это также не идеально, потому что для вложенных квантификаторов это приведет к тому, что каждый квантификатор будет проиндексирован по-разному. Кристоф также показывает в этом ответе, что внутренне подход, основанный на Z3_mk_forall_const переводится на что-то эквивалентное Z3_mk_forall так что под капотом действительно нет разницы. Различия в API, однако, могут иметь большое значение для программиста.

Существует также (гораздо более простой) механизм, предоставляемый программисту в C++ API, если вы можете использовать его. Вот примеры использования трех разных методов:

// 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();
}

Я также нашел эти вопросы полезными:

• "для всех квантификаторов в Z3"
  
• "C API для квантификаторов"
  
• "Поддержка квантификатора Z3"
  

Примеры и комментарии, представленные в источнике Z3, также были полезны, особенно в examples/c/test_capi.c, examples/c++/example.cpp, а также src/api/z3_api.h,