Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays

Autor:	Robert Brummayer, Armin Biere
Rok vydání:	2009
Předmět:	TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Computer Science::Logic in Computer Science Satisfiability modulo theories On demand Computer Science::Programming Languages Parallel computing Rewriting Term (logic) Algorithm Satisfiability Logical formula Mathematics
Zdroj:	Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783642007675 TACAS
DOI:	10.1007/978-3-642-00768-2_16
Popis:	Satisfiability Modulo Theories (SMT) is the problem of deciding satisfiability of a logical formula, expressed in a combination of first-order theories. We present the architecture and selected features of Boolector, which is an efficient SMT solver for the quantifier-free theories of bit-vectors and arrays. It uses term rewriting, bit-blasting to handle bit-vectors, and lemmas on demand for arrays.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::f94367c9f5e761fe6adc596a69b8f6a0 https://doi.org/10.1007/978-3-642-00768-2_16 Zobrazit plný text záznamu