5

基本的に、私はZ3に、値が10より大きい任意の整数を与えるように依頼したいと思います。したがって、次のステートメントを記述します。

(declare-const x (Int))
(assert (forall ((i Int)) (> i 10)))
(check-sat)
(get-value(x))

この数量詞をモデルに適用するにはどうすればよいですか？これを達成するために（assert（> x 10））と書くことができることを私は知っています。ただし、モデルに数量詞が必要なので、値が10を超えることが保証されている整数定数を宣言するたびに、整数定数ごとにステートメント（assert（> x 10））を挿入する必要はありません。宣言しました。

4

1 に答える 1

5

を使用する(assert (forall ((i Int)) (> i 10)))と、iは有界変数であり、数量化された式は真理値と同等falseです。この場合です。

量指定子を使用してマクロを定義したいと思います。

(declare-fun greaterThan10 (Int) Bool)
(assert (forall ((i Int)) (= (greaterThan10 i) (> i 10))))

そして、それらを使用してコードの繰り返しを避けることができます:

(declare-const x (Int))
(declare-const y (Int))
(assert (greaterThan10 x))
(assert (greaterThan10 y))
(check-sat)

これは、Z3 API を使用しているときに、解釈されない関数を使用してマクロを定義する基本的な方法です。(set-option :macro-finder true)Z3 が全称量指定子をそれらの関数の本体に置き換えるように設定する必要があることに注意してください。

ただし、テキスト インターフェイスを使用している場合はdefine-fun、SMT-LIB v2 のマクロを使用すると、必要なことを簡単に行うことができます。

(define-fun greaterThan10 ((i Int)) Bool
  (> i 10))
于 2012-02-16T16:23:32.083 に答える