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 (BV) for the integers and that of floating-point numbers (FP) for the reals respectively. Whereas an approach for OMT with (unsigned) BV objectives has been proposed by Nadel & Ryvchin, unfortunately we are not aware of any existing approach for OMT with FP objectives. In this paper we fill this gap, and we address for the first time OMT with FP 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-BV objectives and, most importantly, with FP 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.