SMT-LIB 2.6 declare-datatypesステートメントのSMTソルバーのサポート

SMT-LIBバージョン2.6のdraftは、(declare-datatypes)ステートメントを指定します。この機能のoriginal announcementでは、提案された構文がその時点でZ3とCVC4でサポートされている構文と異なることに言及しています。SMT-LIB 2.6 declare-datatypesステートメントのSMTソルバーのサポート

現在、SMT-LIB 2.6ドラフトの提案構文をサポートするSMT-LIBサポートを持つSMTソルバー、または提案された構文のサポートをソルバーに追加するパッチはありますか？

私が興味を持っているのは、QF_ABVと単純なnタプルのデータ型です。再帰的なデータ型やパラメトリックなデータ型などの高度なデータ型の機能は必要ありません。

出典

2017-03-13 CliffordVienna

Z3はまだから構文を実装していません。ドラフト仕様。パターンマッチングの導入はパターンマッチングコンパイラを使用してコンパイルすることができます（またはLISPプログラマが手作業で行うように）。 –

最新のCVC4開発版（コミット594301e6f2893ebe9baba5083ff084933b1e9da9）に、SMT LIBバージョン2.6のデータ型のサポートが追加されました。 2.6構文は、デフォルトで有効になっていませんが、あなたは使用することができます。

cvc4 --lang = smt2.6 [入力]このことができます

希望、アンドリュー

出典

2017-03-16 18:32:37 user7723234

ありがとう！ JFYI：Yosysのwrite_smt2コマンド（したがってyosys-smtbmc）は、SMT-LIB 2.6のデータ型を使用できるようになりました。次に例を示します。http://scratch.clifford.at/datatypedemo.smt2 – CliffordVienna

SMT-LIB 2.6 declare-datatypesステートメントのSMTソルバーのサポート

答えて

関連する問題