SMT における理論の組み合わせを扱おうとしている研究がいくつかあることは知っています。ただし、SMT-Lib 2.0 言語 ( http://smtlib.cs.uiowa.edu/docs.html ) は、この点に関して何も述べていません。私の質問は、それがサポートされているかどうかです。また、複数の理論を同時に処理する機能を提供するソルバーは何ですか?
ありがとう、
質問する
171 次
2 に答える
0
このページを見ることができます: http://en.wikipedia.org/wiki/Satisfiability_Modulo_Theoriesで、どの (組み合わせた) 理論がさまざまな SMT ソルバーによってサポートされているかを確認できます。
于 2013-06-23T06:09:18.860 に答える
0
SMTLIBset-logicステートメントは、SMT インスタンスのロジックを設定します。各ロジックは、異なる一連の理論をサポートしています。このページには、SMTLIB2 で現在サポートされているすべてのロジックのリストがあります。
たとえば、QF_AUFLIAロジックを使用すると、IntsとArraysEx理論を 1 つの SMT インスタンスで一緒に使用できます。
于 2014-12-22T07:33:27.117 に答える