Satisfiability modulo theories solver is a decision procedure for the satisfiabilily of formulas of the first-order logics. It is the verification engine for many formalization methods. Theory solvers solve problems with different theoretical backgrounds; however, the problems in the real-world applications often are supported by multiple theories. This paper mainly introduces the methods of theory combination, summarizes the status quo of the SMT solvers. Besides,it analyzes several major techniques on the theoretical combination for SMT solvers. Testing with the industrial cases, we finally evaluate methods of combination theory with experimental results, and compare the performances of several popular SMT solvers which support theoretical combination techniques.%可满足模理论(SMT)求解器是计算机科学中用来判定一阶逻辑公式可满足性的程序,是许多形式化方法的验证引擎.理论求解器实现了SMT基于不同理论背景的求解过程,然而实际问题常以多个理论为背景.因此,本文重点介绍理论组合判定方法,概述SMT求解器的发展现状,并分析了几个主流SMT求解器理论组合判定关键技术.通过对照实验,评估各组合判定方法的优缺点以及目前流行的支持理论组合SMT求解器在工业应用中的性能.
展开▼
