SMT-Lib标准是否支持理论的组合?

Question

我知道有几部作品正在尝试处理SMT中理论的结合。然而，SMT-Lib 2.0语言(http://smtlib.cs.uiowa.edu/docs.html)并没有说明这一点。我的问题是，它是否支持这一点，以及哪些解算器提供了同时处理多个理论的能力?

谢谢,

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理论。