[SMT-LIB] A theory for quantifier free theory for arrays of floating point numbers and bitvectors

[Florian Schanda]

On Saturday 08 Oct 2016 12:43:40 Delcypher wrote:
> I was wondering if there was any interest in having another a logic
> and accompanying benchmark category for QF_AFPBV (quantifier free
> arrays of floating point numbers and bitvectors).

Since we're potentially adding new things... How about AUFBVFPDTLIRA :)

In all seriousness, the SPARK 2014 tools produce SMTLIB with basically these 
features for at least Z3 and CVC4; it may relevant to the SMTLIB project to at 
least capture some of these?

Theory combination is a thing and we pretty much exercise everything possible.


Side question: should floating point benchmarks that contain real literals be 
in QF_FP or should there be a QF_FPLRA or similar? For example:

   (define-const x Float32 ((_ to_fp 8 24) RNE (/ 1 10)))

Thanks,

	Florian