Unsigned int to FP conversion in FPBV

[Franck Cassez]

From @inkytonik:

One of the SVCOMP float benchmarks has this code:

  %2 = tail call zeroext i8 @__VERIFIER_nondet_uchar() #2, !dbg !11
  %3 = uitofp i8 %2 to float, !dbg !12

At the moment, it is unclear on how to represent the effect of the uitofp conversion. Does ScalaSMT have a way to encode this?

[Franck Cassez]

Implement conversion from bitStringBV to FPBV and signedBV to FPBV.

see #10 see #25

→ <<cset fd743d1be59c>>

[Franck Cassez]

Add term tests for conversion from bitStringBV to FPBV and signedBV to FPBV.

see #10 see #25

→ <<cset 8a3c1520e593>>

[Franck Cassez]

Fix tests using toFPBV for BVTerm as they now have to use either bitStringFPBV or signedFPBV (the latter requires a rounding mode).

see #10 see #25

→ <<cset 48c765f983a8>>

[Franck Cassez]

Add tests for conversion from BV to FPBV, bitStringToFPBv and signedToFPBV.

see #10 see #25

→ <<cset 405294c12079>>

[Franck Cassez]

Add support fro conversions from/to FPBV and other sorts.

see #10 see #25

→ <<cset 846dd69c236a>>

[Franck Cassez]

resolved. see #10.

[Franck Cassez]

see #10

[Franck Cassez]

Fix return type of toUBV/toSBV and add simple tests using them.

see #10 see #25 see #26

→ <<cset 1bac73d97524>>