z3 - Z3 と SMT-LIB を使用して、最大 2 つの値を取得します

Question

smt-lib2 を使用して数式の最大値を取得するにはどうすればよいですか?

私はこのようなものが欲しい：

(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun z () Int)
(assert (= x 2))
(assert (= y 4))
(assert (= z (max x y))
(check-sat)
(get-model)
(exit)

もちろん、'max' は smtlibv2 にはわかりません。では、どうすればこれを行うことができますか？

Answer 1

Z3では、マクロを簡単に定義し、maxそれを使用して最大2つの値を取得できます。

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

解釈されていない関数を使用してモデル化する別のトリックがありmaxます。これは、Z3APIで使用すると便利です。

(declare-fun max (Int Int) Int)
(assert (forall ((x Int) (y Int))
    (= (max x y) (ite (< x y) y x))))

を設定する必要があることに注意してください(set-option :macro-finder true)。これにより、Z3は、充足可能性をチェックするときに全称記号を関数の本体に置き換えることができます。

Answer 2

あなたが持っているabs、および基本的な数学ごとにmax(a,b) = (a+b+abs(a-b))/2