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

[David Cok]

Two additional points:

1) Evgeny - any benchmarks that represent the kinds of problems in which 
you are interested would be very welcome. They should be standard 
SMT_LIBv2, in a proposed new logic that combines existing theories, but 
without get-value, get-model, get-assignments - and with just a single 
check-sat. If at all possible, include a set-info :status if you know 
whether the result should be sat or unsat. I'd be happy to work with you 
on this, along with the coordinators for these benchmarks.

2) Enabling solvers for both integers/reals and bit-vectors at the same 
time is not so hard. But applications (at least mine) also want a 
conversion function between the two. That I think is harder. But I'd be 
interested in some discussion on the topic.

- David


On 7/30/2014 7:30 PM, Martin Brain wrote:
> 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
>
>
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib