Beaver: Engineering an Efficient SMT Solver for Bit-Vector Arithmetic
Beaver: Engineering an Efficient SMT Solver for Bit-Vector Arithmetic
复制标题
Beaver：为位向量算术设计高效的 SMT 求解器
DOI：
10.1007/978-3-642-02658-4_53
复制
发表时间：
2009
影响因子：
--
通讯作者：
S. Seshia
中科院分区：
文献类型：
--
作者：
Susmit Jha;Rhishikesh Limaye;S. Seshia
我们介绍了Beaver的设计和实现的关键想法，Beaver是一种用于无量词的有限次数位矢量逻辑（QF_BV）的SMT求解器。 Beaver使用急切的方法，将原始SMT问题编码为布尔值满意度（SAT）问题，并使用一系列单词级别和位级别的转换。在本文中，我们描述了最有效的转换，例如在单词级别上传播常数和平等性，以及使用位级别的使用和逆变器图重写技术。我们重点介绍了这些转换的实现细节，这些详细信息将海狸与其他求解器区分开。我们对海狸技术在硬件和软件基准测试中的有效性进行了实验分析，并选择了许多后端SAT求解器。
Beaver是在OCAML中实施的开源工具，可与任何后端SAT引擎一起使用，并具有有据可查的可扩展代码库，可用于尝试新算法和技术。
We present the key ideas in the design and implementation of Beaver, an SMT solver for quantifier-free finite-precision bit-vector logic (QF_BV). Beaver uses an eager approach, encoding the original SMT problem into a Boolean satisfiability (SAT) problem using a series of word-level and bit-level transformations. In this paper, we describe the most effective transformations, such as propagating constants and equalities at the word-level, and using and-inverter graph rewriting techniques at the bit-level. We highlight implementation details of these transformations that distinguishes Beaver from other solvers. We present an experimental analysis of the effectiveness of Beaver's techniques on both hardware and software benchmarks with a selection of back-end SAT solvers.
Beaver is an open-source tool implemented in Ocaml, usable with any back-end SAT engine, and has a well-documented extensible code base that can be used to experiment with new algorithms and techniques.