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

[Evgeny Roubinchtein]

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.

Thank you again.
-- 
Best,
Evgeny

-----Original Message-----
From: Dejan Jovanović [mailto:dejan.jovanovic at sri.com] 
Sent: Wednesday, July 30, 2014 6:05 PM
To: Evgeny Roubinchtein
Subject: Re: [SMT-LIB] An SMT-Lib logic with fixed-size bit vectors _and_ rationals/floating-point numbers?

Hi Evgeny,

Using CVC4, you can use the logic QF_ALL_SUPPORTED for the quantifier-free fragment, or ALL_SUPPORTED to include quantifiers too.

Most other solver have a way to support what you need, it's just the standard that's not very flexible with this.

Best, Dejan

On 07/30/2014 02:50 PM, 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).  However, such a logic doesn't seem to be part of the standard (http://smtlib.cs.uiowa.edu/logics.shtml).    Does my description of the problem make sense?  If so, would you have some suggestions on possible ways to proceed?
>
> Thank you in advance!
>