SMT-Lib標準是否支持理論的組合？

Question

我知道有幾件作品正在試圖處理SMT理論的結合。但是，SMT-Lib 2.0語言（http://smtlib.cs.uiowa.edu/docs.html）在這一點上並沒有提到任何問題。 我的問題是它是否支持這一點，以及Solvers提供瞭如何同時使用多種理論的能力？

感謝，

Answer 1

你可以看看這個頁面：http://en.wikipedia.org/wiki/Satisfiability_Modulo_Theories，看看哪些（組合）理論是由型動物SMT求解器的支持。

Answer 2

SMTLIB set-logic語句爲您的SMT實例設置邏輯。每個邏輯支持一組不同的理論。此頁面有SMTLIB2所有目前支持的邏輯列表：

• http://smtlib.cs.uiowa.edu/logics.shtml

例如，與QF_AUFLIA邏輯，你可以在一個SMT例如使用Ints和ArraysEx理論在一起。