Fix the printing of bit-vectors and floating-point numbers

[hra687261]

This is an extension to #432, and it ensures that bit-vectors and floats can be printed in a way that can be parsed, this comes down to adding the type information to the constants of these sorts (e.g. (i32 n) instead of just n).

In the case of floats to be more precise we might have to change the format to something like like %.nf, to make sure that we can print n decimals in floats but I am not sure if that is necessary and how many decimals we want.

[filipeom]

In the case of floats to be more precise we might have to change the format to something like like %.nf, to make sure that we can print n decimals in floats but I am not sure if that is necessary and how many decimals we want.

Couldn't we just use the pp_hex instead? It allows use to parse the exact layout of 32- and 64-bit floats.

I think we should also temporarily set the `WithType printers in the Expr.pp_smtml function because the parser expects formulas printed by this function. And, it also allows the human readable format when using Expr.pp.

[hra687261]

Couldn't we just use the pp_hex instead? It allows use to parse the exact layout of 32- and 64-bit floats.

The parser currently does not seem to parse floats in hexadecimal, but I agree, the hexadecimal format is definitely better readability and size wise, in fact bit-vectors should also probably be written in the binary format for the same reason.
I will look into it and see if it is easy to add. (It should be easy)

I think we should also temporarily set the `WithType printers in the Expr.pp_smtml function because the parser expects formulas printed by this function. And, it also allows the human readable format when using Expr.pp.

I agree, I will change that, currently the printer choice is made in cmd_to_smt2.ml but it would be better to do it in the pp_smtml function so that we don't have to change the printer when we call from Owi or from something else.

[filipeom]

LGTM! Thanks!

[filipeom]

On Fri Oct 24, 2025 at 3:41 PM WEST, Hichem R. A. wrote: @hra687261 requested your review on: formalsec/smtml#433 Fix the printing of bit-vectors and floating-point numbers.

Approved