z3 - 计算最大值的宏

Question

我找到了计算最大值的宏Z3 Sat Solver。

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

如何在 中使用 C-API 进行相同的编程Z3 Sat Solver？

谢谢你，

Answer 1

该define-fun命令只是创建一个宏。请注意，SMT 2.0 标准不允许递归定义。Z3 将扩展max_integ解析期间的每一次出现。该命令define-fun可能用于使输入文件更简单、更易于阅读，但在内部它并不能真正帮助 Z3。这个问题在以下帖子中讨论：

• 相当于 Z3 API 中的 define-fun

• Z3 SMT 2.0 与 Z3 py 实施