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理论在一起。