SMT-RAT: An Open Source C plus plus Toolbox for Strategic and Parallel SMT Solving

被引：51

作者：

Corzilius, Florian ^{[1
]}

Kremer, Gereon ^{[1
]}

Junges, Sebastian ^{[1
]}

Schupp, Stefan ^{[1
]}

Abraham, Erika ^{[1
]}

机构：

[1] Rhein Westfal TH Aachen, Aachen, Germany

来源：

THEORY AND APPLICATIONS OF SATISFIABILITY TESTING - SAT 2015 | 2015年 / 9340卷

关键词：

COMPLEXITY;

D O I：

10.1007/978-3-319-24318-4_26

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

During the last decade, popular SMT solvers have been extended step-by-step with a wide range of decision procedures for different theories. Some SMT solvers also support the user-defined tuning and combination of such procedures, typically via command-line options. However, configuring solvers this way is a tedious task with restricted options. In this paper we present our modular and extensible C++ library SMT-RAT, which offers numerous parameterized procedure modules for different logics. These modules can be configured and combined into an SMT solver using a comprehensible whilst powerful strategy, which can be specified via a graphical user interface. This makes it easier to construct a solver which is tuned for a specific set of problem instances. Compared to a previous version, we have extended our library with a number of new modules and support for parallelization in strategies. An additional contribution is our thread-safe and generic C++ library CArL, offering efficient data structures and basic operations for real arithmetic, which can be used for the fast implementation of new theory-solving procedures.

引用

页码：360 / 368

页数：9

共 34 条

[31] Quantifier elimination for real algebra - The quadratic case and beyond [J].