Logic ALL OK?

[rod-chapman]

Is it acceptable to submit benchmarks with the logic set to "ALL"?

[mpreiner]

Hi @rod-chapman, I'd say no. In SMT-LIB the benchmarks should have specific logics, otherwise it will be hard to maintain them in the long run. It's also less useful for SMT-COMP as they'd have to manually go through these benchmarks and assign them a logic (or exclude them entirely for SMT-COMP).

[barrettcw]

Yes, please figure out exactly which theories are being used. This determines the logic. If you know the theories but are unsure about the logic string to use, I'm happy to help you figure that out.

[rod-chapman]

The Why3 drivers for CVC4 and CVC5 generate (set-logic AUFBVFPDTNIRA) which is rejected as "unsupported" by Z3.

The driver for Z3 generates no "set-logic" line at all, so I'm not sure what the correct setting is that will ensure compatibility with all 3... some experimentation may be required...

[rod-chapman]

The "FP" is red-herring, since there is definitely no floating point stuff going on here. From a user's point of view, what I really want is "everything" since I really don't care how the provers do it - I just want the best results possible please, and as fast as possible.

[barrettcw]

That's a lot of letters. Essentially you're telling the solver: this benchmark uses quantifiers, arrays, uninterpreted functions, bit-vectors, floating-point, datatypes, and non-linear integer and real arithmetic. Can you investigate a bit to see if the benchmarks are really using all of that? I have a feeling that this may just be Why3's version of "ALL". It shouldn't be too hard to determine what's actually being used. You can grep for the sorts for most theories.

[barrettcw]

The "FP" is red-herring, since there is definitely no floating point stuff going on here. From a user's point of view, what I really want is "everything" since I really don't care how the provers do it - I just want the best results possible please, and as fast as possible.

Yes, we understand that users prefer to not think about this. But you are offering a contribution to SMT-LIB, and SMT-LIB has a more ambitious goal to be a carefully curated catalog of benchmarks. One of the features of SMT-LIB is to get the logic string as precise as possible. This helps developers and also helps keep the library organized.

[rod-chapman]

Well... SPARK is a fully-fledged programming language, so it's certainly possible to write code that uses all of those things. In the case of LibMLKEM, I know there's no floating-point or real arithmetic going on, since this is all-integer cryptographic code.

What does the "DT" mean? What data-types? There are certainly data-types in the source code, or does this specifically refer to the SMTLib "declare-datatype[s]" commands?

[rod-chapman]

My best guess would be that it needs AUFBVDTNIA

But..Z3 still says "unsupported" on that, so we might just have to live with the fact that Z3 can't play. Which is a shame, because if you say "set-logic ALL", Z3 performs just fine...

[barrettcw]

Well, if that's the right categorization and we add it to SMT-LIB, then hopefully Z3 will update to reflect it.

[rod-chapman]

I'll run both CVC4 and CVC5 with "AUFBVDTNIA" and see what I get. If it's OK, then I will update the files accordingly.

[rod-chapman]

OK... results look good. All files and the directory name changed. I will update the pull request.

[Gbury]

@rod-chapman Since it seems relevant here: my recent work on dolmen will make it possible to use Dolmen to compute the correct (and minimal) logic for any given problem. There's still some more work and testing to be done, but this should be part of the next release of Dolmen.