z3 - SMT 2.0 で 4 つのパラメーターの最小値を返す関数を定義する方法

Question

最小の 4 つの整数値を返す関数を SMT 2.0 で定義したいと考えています。

Answer 1

関数 (4 つの整数値のmin4最小値) は、SMT 2.0 言語で次のように定義できます。

(define-fun min2 ((a Int) (b Int)) Int
    (ite (<= a b) a b))

(define-fun min3 ((a Int) (b Int) (c Int)) Int
    (min2 a (min2 b c)))

(define-fun min4 ((a Int) (b Int) (c Int) (d Int)) Int
    (min2 a (min3 b c d)))

次のリンクには、この関数を使用した例が含まれています: http://rise4fun.com/Z3/wuyU

SMT 2.0 では、define-fun基本的にはマクロ定義です。SMT 2.0 言語は、任意の数の引数を期待する関数の定義をサポートしていません。Scala^Z3、SBV、Z3Pyなどの SMT ソルバーにプログラム API を使用することを検討してください。SMT 2.0 よりもはるかに便利に使用できます。Z3Py での同じ例を次に示します: http://rise4fun.com/Z3Py/2vy