2

秒によると。The SMT- LIBv2 Language and Tools: A Tutorialの 3.9.3 では、SMT-LIBv2 で次のような複合ソートを宣言できます。

(set-logic QF_UF)
(declare-sort Triple 3)
(declare-fun state () (Triple Bool Bool Bool))

私は CVC4 を使用していますが、この構文を受け入れるようです。しかし、要素にアクセスするにはどうすればよいでしょうか? 私は次のことを試しました（およびそのさまざまなバリエーションと、オンラインで見つけた他のもの）：

(assert (_ state 1))
(assert (select 1 state))

しかし、これらの演算子はベクトルと配列でしか機能しないようです。このような複合ソートを使用する例は見つかりませんし、チュートリアルや言語標準でそれらの要素へのアクセスについて何も見つけることができません。それはどのように行われますか？それとも、この機能の目的を完全に誤解していましたか?

私のアプリケーション: 一時的な問題をエンコードし、古い状態を新しい状態に変換する状態遷移関数の形式でそれを実行したいので、システムで実験するときに次のようなものを書くことができます:

....
(declare-fun initial_state () MyStateSort)
(declare-fun state_after_step_1 () MyStateSort)
(declare-fun state_after_step_2 () MyStateSort)
(assert (= (MyTransitionFunc initial_state) state_after_step_1)
(assert (= (MyTransitionFunc state_after_step_1) state_after_step_2)
4

1 に答える 1

0

これは私自身の質問に対する答えです。アリティ> 0のユーザー定義ソートのユースケースの例を誰かが投稿できる場合は、それを答えとして喜んで受け入れます。

SMT-LIBv2 標準をより注意深く読んだ後、アリティ > 0 のソート宣言Arrayは、ユーザー提供のコードではなく、理論定義 (のようなソートを宣言するため) にのみ適用されると考えています。David Cok のチュートリアルの例は、これを使用して複合ソートを宣言できることを示唆しているため、誤解を招くようです。他のどこにもその兆候は見つかりませんでした。これには、アリティ > 0 のソート宣言が 1 つも含まれていない完全な SMT-LIB ベンチマークが含まれます。

「複合ソート」の代わりに、解釈されない関数を使用して、複雑なデータ構造と同等のものを作成する必要があります。例：

(set-logic QF_UF)
(declare-sort CONTAINER_SORT 0)
(declare-fun CONTAINER_MEMBER_1 (CONTAINER_SORT) Bool)
(declare-fun CONTAINER_MEMBER_2 (CONTAINER_SORT) Bool)
(declare-fun INSTANCE_1 () CONTAINER_SORT)
(declare-fun INSTANCE_2 () CONTAINER_SORT)

これにより、次の 4 つの独立した Bool 式が効果的に宣言されます。

(CONTAINER_MEMBER_1 INSTANCE_1)
(CONTAINER_MEMBER_2 INSTANCE_1)

(CONTAINER_MEMBER_1 INSTANCE_2)
(CONTAINER_MEMBER_2 INSTANCE_2)
于 2014-12-24T15:53:36.820 に答える