3

を生成しているz3の実数の乗算を含むいくつかの単純な制約がありunknownます。問題は、ラップされていないバージョンがを生成するため、データ型でラップされていることのようsatです。

簡略化したケースを次に示します。

(declare-datatypes () ((T (NUM (n Real)))))

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

(assert (is-NUM a))
(assert (is-NUM b))
(assert (is-NUM c))

(assert (= c (NUM (* (n a) (n b)))))

(check-sat)
;unknown

そしてデータ型なし：

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

(assert (= c (* a b)))

(check-sat)
;sat

私はz33.2を使用していますが、これはWebインターフェースでも再現可能です。

4

2 に答える 2

8

はい、Z3 はunknown量指定子のない問題で返すことができます。主な理由は次のとおりです。

  • 時間またはメモリが不足しています

  • 量指定子のないフラグメントは決定できません (例: 非線形整数演算)

  • 量指定子のないフラグメントはコストが高すぎるか、Z3 で実装されている手順が不完全です。

あなたの問題は決定可能な断片にあり、未知のものは Z3 で使用される非線形演算の不完全な手順によるものです。Z3 4.0 には、非線形実数演算の完全な手順がありますが、他の理論とはまだ統合されていません。したがって、最初の問題では役に立ちません。

1 番目と 2 番目のクエリで動作が異なるのは、各クエリで使用される戦略が異なるためです。Z3 には、カスタム戦略を定義するための新しいフレームワークがあります。satコマンドを使用して最初のクエリを取得できます

(check-sat-using (then simplify solve-eqs smt))

それ以外の

(check-sat)

最初のコマンドは、等式を解くことによって Z3 に変数を消去させます (つまり、 tactic solve-eqs)。平等をなくし(= c (NUM (* (n a) (n b))))ます。この戦術は、Z3 3.x の 2 番目の問題で自動的に使用されます。等式を に置き換えると、この戦術は役に立たないことに注意してください(>= c (NUM (* (n a) (n b))))。

さらに、2 番目の問題には非線形演算しか含まれていません。そのため、Z3 4.0 では、非線形実数演算用の新しい (そして完全な) ソルバーが自動的に使用されます。

新しい戦略フレームワークについては、http://rise4fun.com/Z3/tutorial/strategies、http://rise4fun.com/Z3Py/tutorial/strategiesで学習できます。

于 2012-06-25T21:19:29.633 に答える
2

あなたの例は非線形演算にあります。Z3 4.0 は、非線形算術アサーションのみで問題を解決できますが、解釈されていない関数やその他の理論では解決できません。unknownこれが、最初の例で生成される理由を説明しています。この制限は、Z3 の将来のバージョンで対処される可能性があります。

于 2012-06-25T21:19:27.453 に答える