Description:
<jats:title>Abstract</jats:title><jats:p>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 <jats:italic>bit-precise</jats:italic> representations of numbers, which in SMT are handled by means of the theory of bit-vectors (<jats:inline-formula><jats:alternatives><jats:tex-math>$${{\mathcal {B}}}{{\mathcal {V}}}$$</jats:tex-math><mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML">
<mml:mrow>
<mml:mi>B</mml:mi>
<mml:mi>V</mml:mi>
</mml:mrow>
</mml:math></jats:alternatives></jats:inline-formula>) for the integers and that of floating-point numbers (<jats:inline-formula><jats:alternatives><jats:tex-math>$$\mathcal {FP}$$</jats:tex-math><mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML">
<mml:mi>FP</mml:mi>
</mml:math></jats:alternatives></jats:inline-formula>) for the reals respectively. Whereas an approach for OMT with (unsigned) <jats:inline-formula><jats:alternatives><jats:tex-math>$${{\mathcal {B}}}{{\mathcal {V}}}$$</jats:tex-math><mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML">
<mml:mrow>
<mml:mi>B</mml:mi>
<mml:mi>V</mml:mi>
</mml:mrow>
</mml:math></jats:alternatives></jats:inline-formula> objectives has been proposed by Nadel & Ryvchin, unfortunately we are not aware of any existing approach for OMT with <jats:inline-formula><jats:alternatives><jats:tex-math>$$\mathcal {FP}$$</jats:tex-math><mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML">
<mml:mi>FP</mml:mi>
</mml:math></jats:alternatives></jats:inline-formula> objectives. In this paper we fill this gap, and we address for the first time <jats:inline-formula><jats:alternatives><jats:tex-math>$$\text {OMT}$$</jats:tex-math><mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML">
<mml:mtext>OMT</mml:mtext>
</mml:math></jats:alternatives></jats:inline-formula> with <jats:inline-formula><jats:alternatives><jats:tex-math>$$\mathcal {FP}$$</jats:tex-math><mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML">
<mml:mi>FP</mml:mi>
</mml:math></jats:alternatives></jats:inline-formula> objectives. We present a novel OMT approach, based on the novel concept of <jats:italic>attractor</jats:italic> and <jats:italic>dynamic attractor</jats:italic>, which extends the work of Nadel and Ryvchin to work with signed-<jats:inline-formula><jats:alternatives><jats:tex-math>$${{\mathcal {B}}}{{\mathcal {V}}}$$</jats:tex-math><mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML">
<mml:mrow>
<mml:mi>B</mml:mi>
<mml:mi>V</mml:mi>
</mml:mrow>
</mml:math></jats:alternatives></jats:inline-formula> objectives and, most importantly, with <jats:inline-formula><jats:alternatives><jats:tex-math>$$\mathcal {FP}$$</jats:tex-math><mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML">
<mml:mi>FP</mml:mi>
</mml:math></jats:alternatives></jats:inline-formula> objectives. We have implemented some novel <jats:inline-formula><jats:alternatives><jats:tex-math>$$\text {OMT}$$</jats:tex-math><mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML">
<mml:mtext>OMT</mml:mtext>
</mml:math></jats:alternatives></jats:inline-formula> procedures on top of <jats:sc>OptiMathSAT</jats:sc> and tested them on modified problems from the SMT-LIB repository. The empirical results support the validity and feasibility of our novel approach.</jats:p>