[SMT-LIB] How to submit benchmarks to smtlib

[Levent Erkok]

David:

This is an excellent point that comes up quite often for upstream tools,
i.e., those that use SMT-Solvers as backend engines. How you name the
required logic for the problem at hand sounds like a trivial task, but it's
actually quite tricky. There are a few problems:

   - If the SMTLib is generated "on the fly," the tool may not know ahead
of time which logic it will need until the entire problem gets translated.
This is usually not a big deal as there's usually a two-pass process to
patch the required info, but it would be nice if the "set-logic" command
wasn't required to be pretty-much the first thing.

    - The choice of combinations is ever-increasing, and how to abbreviate
properly becomes an issue; like you mentioned. Why AUFBVNIRA, as opposed to
AUFNIRABV? What combinations are allowed? And different solvers seem to
allow "ALL" as a fall-back logic too.

To that end, I think we can look to the programming language community for
a proper solution. From a tool perspective, setting the logic is really
about what set of names are brought into the scope. In that sense, it's
akin to import statements of regular languages. So, perhaps a better
approach would be to allow multiple import statements in a benchmark to
determine what logical constants are available:

      (import Quantifiers)
      (import BitVectors)
      (import LinearIntegerArithmetic)

That way, instead of picking a logic, upstream tools can declare what
"features" they need, by a sequence of import statements that bring the
relevant parts to scope. If these import statements can be placed anywhere
in the file, that'd be fantastic; but even if we require them to be at the
very top, it'd still be an improvement.

If the imported features have a name conflict (i.e., if two imports define
the same logical constant) that'd lead to ambiguity and we'd expect the
solver to reject the benchmark. If that is the case, some sort of a
"qualified" name approach might be taken; but we can cross that bridge when
we come to it.

Of course, I'm not prescribing any syntax and/or chosen names here; just
advocating an approach based on importing names into scope as opposed to
actual selection of the logic. The SMTLib competition might have some
issues with this regarding classification, but I think those can be worked
around by a simple scan of the "features" as well.

-Levent.

On Tue, Mar 17, 2015 at 6:38 AM, David R. Cok <dcok at grammatech.com> wrote:

> This brings to the fore the outstanding issue of standardized naming of
> logics, even before they are accepted as standard.
>
> - David
>
> On 3/17/2015 9:22 AM, Florian Schanda wrote:
>
>> I will also have benchmarks that combine pretty much everything
>> (AUFBVFPNIRA);
>> where should something like that go?
>>
>
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>