[SMT-LIB] An SMT-Lib logic with fixed-size bit vectors _and_ rationals/floating-point numbers?

[Martin Brain]

On Wed, 2014-07-30 at 22:33 +0000, Evgeny Roubinchtein wrote:
> Hi, Dejan,
> 
> Thank you for a lightning-fast reply.   I did take a look at the input parsing code in CVC4, and noticed the *ALL_SUPPORTED logic names.  Pragmatically, I will certainly try running with QF_ALL_SUPPORTED and see what happens.  From a more abstract viewpoint, I am curious whether the reason such logics didn't make it into the current version of the standard has to do more with history/resource limitations, or if there is some deeper technical reason (from the viewpoint of logic) for why combining those theories might not be a great idea.

The theory of floating-point was only (officially) added to the standard
a few months ago and I / we have simply not got around to it.  There are
no technical reasons that make them impossible.

It might be worth pointing out that historically, logics were only
created when there was a significant number of benchmarks for them,
rather than attempting any kind of completeness.  This is why the
selection is somewhat unusual.  The proposals for a new approach to
logics are all a lot more regular.

Cheers,
 - Martin