Book chapter
Designing Theory Solvers with Extensions
Frontiers of Combining Systems, pp.22-40
Lecture Notes in Computer Science, Springer International Publishing
08/29/2017
DOI: 10.1007/978-3-319-66167-4_2
Abstract
Satisfiability Modulo Theories (SMT) solvers have been developed to natively support a wide range of theories, including linear arithmetic, bit-vectors, strings, algebraic datatypes and finite sets. They handle constraints in these theories using specialized theory solvers. In this paper, we overview the design of these solvers, specifically focusing on theories whose function symbols are partitioned into a base signature and an extended signature. We introduce generic techniques that can be used in solvers for extended theories, including a new context-dependent simplification technique and model-based refinement techniques. We provide case studies showing our techniques can be leveraged for reasoning in an extended theory of strings, for bit-vector approaches that rely on lazy bit-blasting and for new approaches to non-linear arithmetic.
Details
- Title: Subtitle
- Designing Theory Solvers with Extensions
- Creators
- Andrew Reynolds - Department of Computer Science, The University of Iowa, Iowa, USACesare Tinelli - Department of Computer Science, The University of Iowa, Iowa, USADejan Jovanović - SRI International, Menlo Park, USAClark Barrett - Department of Computer Science, Stanford University, Stanford, USA
- Resource Type
- Book chapter
- Publication Details
- Frontiers of Combining Systems, pp.22-40
- Publisher
- Springer International Publishing; Cham
- Series
- Lecture Notes in Computer Science
- DOI
- 10.1007/978-3-319-66167-4_2
- eISSN
- 1611-3349
- ISSN
- 0302-9743
- Language
- English
- Date published
- 08/29/2017
- Academic Unit
- Computer Science
- Record Identifier
- 9984002310002771
Metrics
14 Record Views