Converting different widths of floating-point numbers

Question

I want to compare two different widths of floating-point numbers by giving an assert to z3. For example, I want to compare between an IEEE 32-bit and an IEEE 64-bit floating-point number.

My try is shown as follows:

(set-logic QF_FPA)
(set-option :produce-models true)
(declare-fun x_64 () (_ FP 11 53))
(declare-fun x_32 () (_ FP 8 24))
(assert (== ((_ asFloat 11 53) roundNearestTiesToEven x_64 ) x_64))
(check-sat)

But I got an error message:

(error "line 5 column 59: sort mismatch")

What is the correct way to compare a 32-bit and a 64-bit number?

The z3 version I am using is 4.3.1 (linux version).

Answer 1

In general, these conversions are non-trivial, e.g., when converting from 64-bit down to 32-bit some precision may be lost. This is why the conversion functions take a rounding mode. The SMT standard for floating-point numbers does contain conversion functions of the following type:

; from another floating point sort
((_ to_fp eb sb) RoundingMode (_ FloatingPoint m n) (_ FloatingPoint eb sb))

So, the correct way to convert between floating-point numbers is to use the to_fp function. [Previously, the asFloat function served this purpose as well; I don't get an error using the latest unstable version of Z3 when using it.] A full example would be this:

(set-logic QF_FPA)
(set-option :produce-models true)
(declare-fun x_64 () (_ FP 11 53))
(declare-fun x_32 () (_ FP 8 24))
(assert (== ((_ to_fp 11 53) roundNearestTiesToEven x_32) x_64))
(check-sat)

which Z3 (latest unstable) accepts without errors and solves instantly. Alternatively, we could also think of casting x_64 down to 32 bit, in which case the assertion would look like this:

(assert (== ((_ to_fp 8 24) roundNearestTiesToEven x_64) x_32))