On Solving Quantified Bit-Vectors using Invertibility Conditions

TL;DR

This paper introduces a new method for solving quantified bit-vector formulas in SMT by computing symbolic inverses, improving solver performance through invertibility conditions and counterexample-guided instantiation.

Contribution

The paper develops a novel approach using invertibility conditions and syntax-guided synthesis to enhance SMT solving of quantified bit-vector formulas, with experimental validation.

Findings

Performance improvements over state-of-the-art solvers

Effective embedding of invertibility conditions into quantifier instantiations

Verification of conditions using multiple SMT solvers

Abstract

We present a novel approach for solving quantified bit-vector formulas in Satisfiability Modulo Theories (SMT) based on computing symbolic inverses of bit-vector operators. We derive conditions that precisely characterize when bit-vector constraints are invertible for a representative set of bit-vector operators commonly supported by SMT solvers. We utilize syntax-guided synthesis techniques to aid in establishing these conditions and verify them independently by using several SMT solvers. We show that invertibility conditions can be embedded into quantifier instantiations using Hilbert choice expressions, and give experimental evidence that a counterexample-guided approach for quantifier instantiation utilizing these techniques leads to performance improvements with respect to state-of-the-art solvers for quantified bit-vector constraints.