Optimization Modulo the Theories of Signed Bit-Vectors and Floating-Point Numbers

Optimization modulo theories (OMT) is an important extension of SMT which allows for finding models that optimize given objective functions, typically consisting in linear-arithmetic or Pseudo-Boolean terms. However, many SMT and OMT applications, in particular from SW and HW verification, require handling bit-precise representations of numbers, which in SMT are handled by means of the theory of bit-vectors ( ℬ𝒱 ) for the integers and that of floating-point numbers ( ℱ𝒫 ) for the reals respectively. Whereas an approach for OMT with (unsigned) ℬ𝒱 objectives has been proposed by Nadel Ryvchin, unfortunately we are not aware of any existing approach for OMT with ℱ𝒫 objectives. In this paper we fill this gap, and we address for the first time OMT with ℱ𝒫 objectives. We present a novel OMT approach, based on the novel concept of attractor and dynamic attractor , which extends the work of Nadel and Ryvchin to work with signed- ℬ𝒱 objectives and, most importantly, with ℱ𝒫 objectives. We have implemented some novel OMT procedures on top of OptiMathSAT and tested them on modified problems from the SMT-LIB repository. The empirical results support the validity and feasibility of our novel approach.