Tags:bit-vectors, bv2nat and nat2bv, int-blasting, SMT, translation from bit-vectors to integers and translation of quantified formulas and arrays
Abstract:
In this paper we present a translation from bit-vector formulas to integer formulas. The translation uses the function symbols function symbols bv2nat and nat2bv_k which are both utilized in the theory of fixed-width bit-vectors of the SMT-LIB language to define the semantics of bit-vector operations. Our translation replaces bit-vector operations with their semantic definition. This facilitates a more modular application as bit-vector operations and their semantic definition have the same sort. As a postprocessing our translation replaces the composition of bv2nat and nat2bv_k with a modulo operation, and removes redundant modulo operations from the translation result. The evaluation of our translation shows that we are able to solve 9% more tasks, 10% faster and with 23% less memory usage compared to a closely related, up-to-date translation approach. Additionally, our translation supports the translation of quantified formulas and arrays over bit-vectors.
A Bit-Vector to Integer Translation with Bv2nat and Nat2bv