SMT-Lib标准是否支持理论的结合？

Question

我知道有几部著作正在尝试处理SMT中的理论组合。然而，SMT-LIB2.0语言(http://smtlib.cs.uiowa.edu/docs.html)并没有提到这一点。我的问题是，它是否支持这一点，以及什么求解器提供了同时使用几个理论的能力？

谢谢,

Answer 1

你可以看一下这个页面：http://en.wikipedia.org/wiki/Satisfiability_Modulo_Theories，看看不同的SMT求解器支持哪些(组合)理论。

Answer 2

SMTLIB语句设置set-logic实例的逻辑。每个逻辑都支持一组不同的理论。此页包含SMTLIB2中当前支持的所有逻辑的列表：

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

例如，使用QF_AUFLIA逻辑，您可以在一个SMT实例中同时使用Ints和ArraysEx理论。