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

[Martin Brain]

On Wed, 2014-07-30 at 21:50 +0000, Evgeny Roubinchtein wrote:
> Dear friends of SMT-Lib,
> 
> For my summer internship here at Mathworks, I am helping evaluate the feasibility of using an off-the-shelf SMT solver as part of automated test generation tool chain (presently, an internally-developed solver is used).
> I would like to use SMT-Lib format to interface with the solver (I am presently using CVC4  via its SMT-Lib interface).   We (the folks I am working with here at Mathworks and yours truly) feel that, in order to handle some of our test generation tasks,  we really need to work in a logic that includes _both_ fixed-size bit vectors and some manner of non-integer numbers (either rationals or floating point).
Rationals and floating-point are very different from an implementation
point of view.  One is undecideable, the other is in NP.  A number of
solvers have implementations for floating-point but I do not know of any
that have rational solvers (as distinct from real).

>   However, such a logic doesn't seem to be part of the standard (http://smtlib.cs.uiowa.edu/logics.shtml).
Yes; this is my fault.  I had been waiting until the new system for
describing logics was finished.  After the discussion at the SMT
workshop, it seems this may be a little way off so I really should be
getting the proposals ready ASAP.

>     Does my description of the problem make sense?
Yes, although depending on what your input format is, the solver
interface may be a greater or lesser part of the problem.

>   If so, would you have some suggestions on possible ways to proceed?
Yes but it's probably best if I mail them offlist to avoid filling the
list with irrelevant info.

Cheers,
 - Martin