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

[Christoph Wintersteiger]

Absolutely, please do keep any benchmarks you generate and send them to us if possible! I'm currently preparing the first set of benchmarks for FP and it would be fantastic if we could include yours.

Cheers,
Christoph

Side note: Z3 also has support for floats and bit-vectors, the logics are called QF_FPA and QF_FPABV at the moment.

Christoph M. Wintersteiger | Researcher | Tel: +44 1223 479724 | Fax: +44 1223 479999 | research.microsoft.com/people/cwinter


Microsoft Research Limited (company number 03369488) is a company registered in England and Wales whose registered office is at 21 Station Road, Cambridge, CB1 2FB 

-----Original Message-----
From: smt-lib-bounces at cs.nyu.edu [mailto:smt-lib-bounces at cs.nyu.edu] On Behalf Of David Cok
Sent: Thursday, July 31, 2014 06:55
To: Martin Brain; Evgeny Roubinchtein
Cc: smt-lib at cs.nyu.edu
Subject: Re: [SMT-LIB] An SMT-Lib logic with fixed-size bit vectors _and_ rationals/floating-point numbers?

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

_______________________________________________
SMT-LIB mailing list
SMT-LIB at cs.nyu.edu
http://www.cs.nyu.edu/mailman/listinfo/smt-lib