Для всего квантификатора в Z3

Question

Я хотел бы увидеть пример C-API Z3_mk_forall_const() в Z3.

Я пытаюсь кодировать -

(define-fun max_integ ((x Int) (y Int)) Int 
    (ite (< x y) y x)) 

То, что я пробовал, это следующее, но я получаю type error

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


void error_handler(Z3_context c, Z3_error_code e)
{
    printf("Error code: %d\n", e);
    printf("Error msg : %s\n", Z3_get_error_msg(e));
    exit(0);
}

Z3_context mk_context_custom(Z3_config cfg, Z3_error_handler err)
{
    Z3_context ctx;

    Z3_set_param_value(cfg, "MODEL", "true");
    ctx = Z3_mk_context(cfg);
    Z3_set_error_handler(ctx, err);

    return ctx;
}

Z3_context mk_context()
{
    Z3_config  cfg;
    Z3_context ctx;
    cfg = Z3_mk_config();
    ctx = mk_context_custom(cfg, error_handler);
    Z3_del_config(cfg);
    return ctx;
}

Z3_ast mk_var(Z3_context ctx, const char * name, Z3_sort ty)  
{
    Z3_symbol   s  = Z3_mk_string_symbol(ctx, name);
    return Z3_mk_const(ctx, s, ty); 
}

Z3_ast mk_int_var(Z3_context ctx, const char * name)
{
    Z3_sort ty = Z3_mk_int_sort(ctx);
    return mk_var(ctx, name, ty);
}

int main()
{
    Z3_context      ctx;
    Z3_func_decl    f;
    Z3_sort         int_sort;
    Z3_symbol       f_name;
    Z3_ast xVar, yVar;
    Z3_app bound[2];
    Z3_ast implication;
    Z3_sort       f_domain[2];

    // Make context.
    ctx = mk_context();

    int_sort    = Z3_mk_int_sort(ctx);
    f_name      = Z3_mk_string_symbol(ctx, "max_integer");
    f_domain[0] = int_sort;
    f_domain[1] = int_sort;
    f = Z3_mk_func_decl(ctx, f_name, 2, f_domain, int_sort);

    xVar = mk_int_var(ctx, "x");
    yVar = mk_int_var(ctx, "y");

    bound[0] = (Z3_app)xVar;
    bound[1] = (Z3_app)yVar;

    implication = Z3_mk_ite(ctx, Z3_mk_lt(ctx, xVar, yVar), xVar, yVar);

    Z3_mk_forall_const(ctx, 0, 2, bound, 0, 0, implication);

    // Delete the context.
    Z3_del_context(ctx);

    return 0;
}

Answer 1

Вы получаете ошибку типа, потому что implication является целочисленным выражением. Аргумент forall выражение должно быть логическим выражением. Я предполагаю, что вы пытаетесь создать формулу

(forall ((x Int) (y Int)) (= (max_int x y) (ite (< y x) x y)))

Вот модифицированный пример. Обратите внимание, что я также изменил Z3_mk_lt(ctx, xVar, yVar) в Z3_mk_lt(ctx, yVar, xVar), В противном случае вы будете определять min функция.

int main()
{
    Z3_context      ctx;
    Z3_func_decl    f;
    Z3_sort         int_sort;
    Z3_symbol       f_name;
    Z3_ast xVar, yVar;
    Z3_app bound[2];
    Z3_ast ite;
    Z3_sort f_domain[2];
    Z3_ast f_app;
    Z3_ast eq;
    Z3_ast q;

    // Make context.
    ctx = mk_context();

    int_sort    = Z3_mk_int_sort(ctx);
    f_name      = Z3_mk_string_symbol(ctx, "max_integer");
    f_domain[0] = int_sort;
    f_domain[1] = int_sort;
    f = Z3_mk_func_decl(ctx, f_name, 2, f_domain, int_sort);

    xVar = mk_int_var(ctx, "x");
    yVar = mk_int_var(ctx, "y");

    bound[0] = (Z3_app)xVar;
    bound[1] = (Z3_app)yVar;

    // Create the application f(x, y)
    { Z3_ast args[2] = {xVar, yVar}; 
      f_app = Z3_mk_app(ctx, f, 2, args);
    }

    // Create the expression ite(y < x, x, y)
    ite = Z3_mk_ite(ctx, Z3_mk_lt(ctx, yVar, xVar), xVar, yVar);

    // Create the equality
    eq = Z3_mk_eq(ctx, f_app, ite);

    // Create quantifier
    q = Z3_mk_forall_const(ctx, 0, 2, bound, 0, 0, eq);

    printf("%s\n", Z3_ast_to_string(ctx, q));

    // Delete the context.
    Z3_del_context(ctx);

    return 0;
}