Use Solver Native Implementation of Bitvector to IEEE FP for CVC4 and CVC5

[baierd]

This PR changes the implementation of CVC4 and 5 to use their built-in version of fromIeeeBitvector().

[baierd]

@kfriedberger i think this branch is ready to be reviewed. The CI fails for some timeout reason and needs to be restarted.

[kfriedberger]

Overall, a good catch. We seem to have missed this simple operation in CVC4/CVC5 some years ago.

[baierd]

Overall, a good catch. We seem to have missed this simple operation in CVC4/CVC5 some years ago.

Their naming (especially in CVC4) seems a little counter-intuitive at first. I only noticed because i had the SMTLib2 standard and the CVC5 API documentation open while working on FP stuff.

Actually, we could add your implementation as a default implementation, then we would not have to worry about any future solvers not supporting this.

[baierd]

Actually, we could add your implementation as a default implementation, then we would not have to worry about any future solvers not supporting this.

OK, that's not possible in general. The solvers generally do not allow the creation of new FP numbers from 3 BV terms like CVC4/5. And since all solver support the BV to IEEE FP operation, i won't bother.