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

[Tinelli, Cesare]

Dejan and all,

On 31 Jul 2014, at 02:03, Dejan Jovanović <dejan.jovanovic at sri.com> wrote:

> Cesare,
>
> On 07/30/2014 04:30 PM, Martin Brain wrote:
>> On Wed, 2014-07-30 at 22:33 +0000, Evgeny Roubinchtein wrote:
>> selection is somewhat unusual.  The proposals for a new approach to
>> logics are all a lot more regular.
> For those of us who missed out on the SMT workshop, could you send out the slides you presented on SMT-LIB, or any notes on new proposals such as this one.
>
Sure, the slides are attached.

Following up the meeting at SMT'14, we are working on two separate things related to the standard right now:

1) A draft of a new version of the language which includes several additions requested over the years and discussed in various smaller forums than this list.

2) A new mechanism for defining logics.

The draft is almost ready. I will circulate it to this list soon for additional comments and feedback before we officialize it.

The new mechanisms for logics needs more internal discussion. I will report in a month or so, realistically, since many people, me included, are on vacation.

For a brief overview, the idea floated at SMT'14 was to decouple the reference to the theories used in a logic from the restrictions on the logic's language. The latter is what makes the current approach problematic because it is not modular. (For instance, QF_AX is *not* a sublogic of QF_AUFLIA because of the latter restricts array sorts to integer arrays only.) We discussed the possibility of defining logics almost only in terms of the theories they refer to, and then adding additional language restrictions directly to benchmarks using the set-info command. Both theories and restrictions would have a short name, for ease of reference, with the full definition of the restriction on the SMT-LIB web site.

For instance, QF_AUFLIA would become something like QF(AX,IA,UF) where QF represents the main restriction to quantifier-free formulas. Then the linearity restrictions and additional restrictions on the allowed sorts would be added separately with, say,

(set-info :logic-restrictions (linear-1 array-sort-1))

where linear-1 and array-sort-1 are defined separately.
Anyway, this is all very rough. More on it later.

Cheers,


Cesare










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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smt-14.pdf
Type: application/pdf
Size: 52850 bytes
Desc: smt-14.pdf
URL: </pipermail/smt-lib/attachments/20140801/241d0ea5/attachment-0001.pdf>