# Beaver: An SMT Solver for Quantifier-free Bit-vector Logic

### Rhishikesh Shrikant Limaye and Sanjit A. Seshia

###
EECS Department

University of California, Berkeley

Technical Report No. UCB/EECS-2010-67

May 13, 2010

### http://www.eecs.berkeley.edu/Pubs/TechRpts/2010/EECS-2010-67.pdf

This thesis presents Beaver -- an efficient SMT solver for the quantifier-free fixed-size bit-vector logic (QF_BV). Beaver is an eager solver, that is, given an SMT formula, it first performs word-level simplications and then bitblasts the simplified formula to a Boolean formula, which is then solved using any SAT solver. Several engineering techniques are behind its efficiency: 1) efficient constant/constraint propagation using event-driven approach, 2) several word-level rewrite rules, 3) efficient bitblasting to SAT, by first converting to and-inverter-graph (AIG) representation and using Boolean simplication techniques of ABC logic synthesis system.

In this thesis, we highlight the implementation details of Beaver that distinguishes it from other solvers. We also present an experimental evaluation and analysis of the effectiveness of our solver against all available QF_BV solvers on the SMT-LIB benchmark suite.

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.

**Advisor:** Sanjit A. Seshia

BibTeX citation:

@mastersthesis{Limaye:EECS-2010-67, Author = {Limaye, Rhishikesh Shrikant and Seshia, Sanjit A.}, Title = {Beaver: An SMT Solver for Quantifier-free Bit-vector Logic}, School = {EECS Department, University of California, Berkeley}, Year = {2010}, Month = {May}, URL = {http://www.eecs.berkeley.edu/Pubs/TechRpts/2010/EECS-2010-67.html}, Number = {UCB/EECS-2010-67}, Abstract = {<p>This thesis presents Beaver -- an efficient SMT solver for the quantifier-free fixed-size bit-vector logic (QF_BV). Beaver is an eager solver, that is, given an SMT formula, it first performs word-level simplications and then bitblasts the simplified formula to a Boolean formula, which is then solved using any SAT solver. Several engineering techniques are behind its efficiency: 1) efficient constant/constraint propagation using event-driven approach, 2) several word-level rewrite rules, 3) efficient bitblasting to SAT, by first converting to and-inverter-graph (AIG) representation and using Boolean simplication techniques of ABC logic synthesis system. </p> <p>In this thesis, we highlight the implementation details of Beaver that distinguishes it from other solvers. We also present an experimental evaluation and analysis of the effectiveness of our solver against all available QF_BV solvers on the SMT-LIB benchmark suite. </p> <p>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. </p>} }

EndNote citation:

%0 Thesis %A Limaye, Rhishikesh Shrikant %A Seshia, Sanjit A. %T Beaver: An SMT Solver for Quantifier-free Bit-vector Logic %I EECS Department, University of California, Berkeley %D 2010 %8 May 13 %@ UCB/EECS-2010-67 %U http://www.eecs.berkeley.edu/Pubs/TechRpts/2010/EECS-2010-67.html %F Limaye:EECS-2010-67