【发布时间】：2013-05-31 19:19:26
【问题描述】：
我知道有几部作品正在尝试处理 SMT 中的理论组合。但是，SMT-Lib 2.0 语言 (http://smtlib.cs.uiowa.edu/docs.html) 没有说明这一点。 我的问题是它是否支持这一点，以及什么 Solvers 提供了同时处理多种理论的能力？
谢谢，
【问题讨论】：
标签： constraint-programming smt satisfiability
【发布时间】：2013-05-31 19:19:26
【问题描述】：
您可以查看此页面：http://en.wikipedia.org/wiki/Satisfiability_Modulo_Theories，了解不同 SMT 求解器支持哪些（组合）理论。
【讨论】：
-
感谢您的回复。但是，该链接不包含任何信息！有支持的理论/逻辑列表，但没有关于它们组合的信息。
SMTLIB set-logic 语句为您的 SMT 实例设置逻辑。每个逻辑都支持一组不同的理论。此页面列出了 SMTLIB2 中当前支持的所有逻辑：
例如，通过QF_AUFLIA 逻辑，您可以在一个SMT 实例中同时使用Ints 和ArraysEx 理论。
【讨论】：