In this talk we present our SMT solver named SMT-RAT, a tool for the automated check of quantifier-free real and integer arithmetic formulas for satisfiability. As a distinguishing feature, SMT-RAT provides a set of decision procedures and supports their strategic combination. We describe our CArL C++ library for arithmetic computations, the available modules implemented on top of CArL, and how modules can be combined to satisfiability-modulo-theories (SMT) solvers. Besides the traditional SMT approach, some new modules support also the recently proposed and highly promising model-constructing satisfiability calculus approach.
展开▼
机译：在本次演讲中，我们将介绍名为SMT-RAT的SMT求解器，该工具用于自动检查无量词的实数和整数算术公式的可满足性。作为一项显着特征，SMT-RAT提供了一组决策程序并支持其战略组合。我们描述了用于算术计算的CArL C ++库，在CArL之上实现的可用模块，以及如何将模块组合到可满足性模理论（SMT）求解器。除了传统的SMT方法外，一些新模块还支持最近提出的，很有前途的模型构建可满足性计算方法。
展开▼
