[SMT-LIB] Naming of SMTLIB logics

[Martin Brain]

On Thu, 2014-05-22 at 05:13 -0700, cok at frontiernet.net wrote:
> SMT-LIB community: (resend, this time to smt-lib)
> 
> 
> My second question, prompted by the SMTEVAL and the proposal of a new 
> theory concerns the naming of logics.
> 
> The names of logics are essentially a combination of 
> characteristics/theories that are largely but not completely 
> independent. Current names have a syntax something like
>    [QF_] [UF] [A|AX] [BV] [ ([N|L][IA|RA|IRA]) | IDL | RDL ]
> Not nearly all combinations currently exist, but most of them could. 
> Now we are adding S (for Separation Logic) into the mix. But we may also 
> soon have a String theory and a Floating Point theory to include.

The current proposal is for an additional five logics using the
Floating-Point theory, although I suspect a case could be made for more.


> I don't have a proposal on this point, but it seems to me that creating 
> logics in this fashion is becoming unwieldy.

Likewise.

>  At least the naming might 
> be simplified, standardized, with a clear means for expansion as new 
> theories are proposed and combined with existing theories.

Given that there is currently an automata for parsing these, perhaps the
minimum that could be done is to document this and try to minimise the
increase in complexity created by new logics.

> I would welcome some discussion and a path to resolution on this.

One approach might be to look at what these are used for and then
evaluate proposals (including the status-quo) against these.  As I
understand it, there are four uses of the logics:

1. Categorising benchmarks, including users who want to find "benchmarks
that use ..."

2. User tools communicating to the solvers what features they require.

3. Solvers that use them to enable of disable components / stages of
solving.

4. Creating decideable subsets of theories.

I suppose the complicating factors is that logics are not just a
combination of theories but also additional defined symbols and
restrictions on how functions can be used.

HTH

Cheers,
 - Martin