对于Z3中的所有量词

我想在Z3中看到一个C-API Z3_mk_forall_const()的例子。

我想编码 –

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

我尝试的是跟随，但我得到type error

 #include  #include  #include  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 xy) (ite (< yx) xy))) 

这是修改后的例子。 请注意，我还将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; }