constraint-programming - SMT-Lib标准是否支持理论组合？

Question

我知道有几部作品试图处理 SMT 中的理论组合。但是，SMT-Lib 2.0 语言 ( http://smtlib.cs.uiowa.edu/docs.html ) 没有说明这一点。我的问题是它是否支持这一点，以及什么 Solvers 提供了同时处理多种理论的能力？

谢谢，

Answer 1

SMTLIBset-logic语句为您的 SMT 实例设置逻辑。每个逻辑都支持一组不同的理论。此页面列出了 SMTLIB2 中所有当前支持的逻辑：

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

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

Answer 2

您可以查看此页面：http ://en.wikipedia.org/wiki/Satisfiability_Modulo_Theories以查看不同 SMT 求解器支持哪些（组合）理论。