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.

[kfriedberger]

We catch other CVC5ApiExceptions as IllegalStateException, because it shows a bug in JavaSMT or a missed illegal usage of the API. Can we replace this plain RuntimeException?

[baierd]

Good question!

The documentation of CVC5 is a little sparse when it comes to the reason why exceptions are thrown:

/**
   * Create operator of Kind:
   * <ul>
   *   <li>BITVECTOR_EXTRACT</li>
   *   <li>FLOATINGPOINT_TO_FP_FROM_IEEE_BV</li>
   *   <li>FLOATINGPOINT_TO_FP_FROM_FP</li>
   *   <li>FLOATINGPOINT_TO_FP_FROM_REAL</li>
   *   <li>FLOATINGPOINT_TO_FP_FROM_SBV</li>
   *   <li>FLOATINGPOINT_TO_FP_FROM_UBV</li>
   * </ul>
   * See enum {@link Kind} for a description of the parameters.
   * @param kind The kind of the operator.
   * @param arg1 The first unsigned int argument to this operator.
   * @param arg2 The second unsigned int argument to this operator.
   * @return The operator.
   * @throws CVC5ApiException on error
   */

However, from the code it is clear that the reasons can be negative integer input, and whatever exception is thrown by native code is also thrown in the JNI wrapper. The native code checks that the given FP size arguments fit the bitvector size as far as i can see. We could/should just check the given FP precision against the BV size ourselves, and this exception is never thrown.

[baierd]

I've added a default check for the used sizes and extended the documentation in CVC5 and switched to an IllegalArgumentException.

[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.