对于 Z3 中的所有量词 [英] for all quantifier in Z3

问题描述

我想在 Z3 中看到 C-API Z3_mk_forall_const() 的示例.

I would like to see an example of C-API Z3_mk_forall_const() in Z3.

我正在尝试编码 -

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

我尝试的是以下内容，但出现类型错误

What I tried is following, but I get 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;
}

推荐答案

您收到类型错误，因为 implication 是一个整数表达式.forall 表达式的参数必须是布尔表达式.我假设您正在尝试创建公式

You are getting a type error because implication is an integer expression. The argument of a forall expression must be a Boolean expression. I'm assuming you are trying to create the formula

(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 函数.

Here is the modified example. Note that I also modified Z3_mk_lt(ctx, xVar, yVar) to Z3_mk_lt(ctx, yVar, xVar). Otherwise, you would be defining the min function.

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

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