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 標準では、再帰的な定義が許可されていないことに注意してください。max_integZ3 は、解析時にが出現するたびに展開します。このコマンドdefine-funは、入力ファイルを単純にして読みやすくするために使用できますが、内部的には Z3 にはあまり役立ちません。この問題については、次の投稿で説明しています。

• Z3 API の define-fun に相当

• Z3 SMT 2.0 と Z3 py の実装