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 条

[1]

Abbott J, 2010, LECT NOTES COMPUT SC, V6327, P73, DOI 10.1007/978-3-642-15582-6_15

[2] MetiTarski: An Automatic Theorem Prover for Real-Valued Special Functions [J].

Akbarpour, Behzad ;

Paulson, Lawrence Charles .

JOURNAL OF AUTOMATED REASONING, 2010, 44 (03) :175-205

[3]

[Anonymous], 2007, Journal on Satisfiability, Boolean Modeling and Computation, DOI [10.3233/SAT190034, 10.3233/sat190034]

[4]

Barrett Clark, 2011, Computer Aided Verification. Proceedings 23rd International Conference, CAV 2011, P171, DOI 10.1007/978-3-642-22110-1_14

[5]

Basu S., 2010, Algorithms in Real Algebraic Geometry

[6] Introduction to the GiNaC framework for symbolic computation within the C++ programming language [J].

Bauer, C ;

Frink, A ;

Kreckel, R .

JOURNAL OF SYMBOLIC COMPUTATION, 2002, 33 (01) :1-12

[7]

Bruttomesso R, 2010, LECT NOTES COMPUT SC, V6015, P150, DOI 10.1007/978-3-642-12002-2_12

[8]

Chauhan P, 2009, DES AUT CON, P460

[9]

Cimatti A, 2013, LECT NOTES COMPUT SC, V7795, P93

[10]

Codish M., 2013, EPIC SERIES, V20, P88

← 1 2 3 4 →