宏來計算最大值

Question

我發現宏來計算Z3 Sat Solver中的最大值。

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

如何在Z3 Sat Solver中使用C-API編程？

謝謝你，

Answer 1

的define-fun命令只是創建宏。請注意，SMT 2.0標準不允許遞歸定義。在解析時，Z3將擴展每次出現的max_integ。可以使用命令define-fun使輸入文件更簡單易讀，但在內部它並不能真正幫助Z3。 這個問題在下面的帖子討論：

• Equivalent of define-fun in Z3 API

• Z3 SMT 2.0 vs Z3 py implementation