1

私は3つの変数、、を持ってaいbますc。計算する必要がありますc = absolute(b-a)。

このステートメントをZ3で次のようにエンコードします

(assert (>= c 0))
(assert (or (= c (- a b) (= c (- b a))))

私は考えていました、Z3でそれを書くより効率的な方法はありますか？
Z3は絶対値を計算するための内部サポートを持っていますか？
また、他の方法を使用するのではなく、このようなコードを記述してもパフォーマンスが低下しないことを願っています。

4

1 に答える 1

3

エンコーディングは正しいです。ただし、ユーザーは通常、を使用して絶対値関数をエンコードします

(define-fun absolute ((x Int)) Int
  (ite (>= x 0) x (- x)))

次に、次のような制約を記述できます。

(assert (= c (absolute (- a b))))

完全な例は次のとおりです（rise4funでもオンラインで入手できます）。

(define-fun absolute ((x Int)) Int
  (ite (>= x 0) x (- x)))

(declare-const a Int)
(declare-const b Int)
(declare-const c Int)

(assert (= a 3))
(assert (= b 4))

(assert (= c (absolute (- a b))))

(check-sat)
(get-model)
于 2013-02-27T14:43:08.773 に答える