[SMT-LIB] A theory for quantifier free theory for arrays of floating point numbers and bitvectors
Florian Schanda
florian.schanda at altran.com
Mon Jan 30 11:03:36 EST 2017
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
More information about the SMT-LIB
mailing list