smtlib parser: Unknown logic UF

[quicquid]

Hello! Please consider the following smtlib script:

(set-logic UF)

(declare-const x Bool)

(assert (and x (not x)))
(check-sat)

Calling dolmen aua.smt2 leads to:

Error Unhandled exception: Dolmen_type.Base.Unknown_logic("UF")

I assume there are two issues here: dolmen exits due to the exception but the error message is hard to read. Also, UF is a valid smtlib logic. Using QF_UF instead works (but is only the quantifier-free fragment) and UFX gives the same exception. Could you have a look?

cheers, Martin

[Gbury]

You're absolutely right: there are some smtlib logics which are missing from this list :

dolmen/src/typecheck/base.ml

Line 25 in ba9aab5

| "AUFLIA" -> merge [core; ints; arrays]

I wrote the list using the smtlib website as reference, mainly:

• http://smtlib.cs.uiowa.edu/logics.shtml
• http://smtlib.cs.uiowa.edu/logics-all.shtml
  In these pages, UF does not appear, which is why it's not currently handled. I'll fix that as soon as possible.

Dolmen exits because it cannot set the correct typing environment when trying to typecheck the assert, due to the logic missing from the list of known logics, but clearly the error message can and will be improved. That being said, I think this is the right behaviour (i.e. failing if the logic is not known), compared to setting no theory at all, or setting all (which is quite not possible because the three arithmetic theories are mutually exclusive).

[c-cube]

do you mean LIA and LRA are exclusive? or the nonlinear ones?

I think issuing a warning and defaulting to "all logics supported" would be best.

[quicquid]

There's also (set-logic ALL) which selects all supported logics. Unfortunately, this depends on the solver.

[Gbury]

do you mean LIA and LRA are exclusive? or the nonlinear ones?

Smtlib makes a difference between logics (e.g. UF, etc..), and theories (e.g. Arrays, Core, FixedSixeBitVectors, etc...). Basically, logics describe a set of theories (+ some extensions and restrictions).

In the case of arithmetics, there are three logics:

• Ints
• Reals
• RealsInts
  See http://smtlib.cs.uiowa.edu/theories.shtml for more details.

Unfortunately, these three logics cannot be used concurrently because they overlap and define different syntactic sugar. Which is a problem for choosing a "default" theory, :/

[c-cube]

Where is the sugar different between Ints and RealsInts, for example?

My intuition would be that RealsInts is the right default.

[Gbury]

There's also (set-logic ALL) which selects all supported logics. Unfortunately, this depends on the solver.

Oh, I forgot that one. In that case I guess the default could be to use the RealsInts theory which is bigger than Ints or Reals.

[quicquid]

Wouldn't it require something like merge [core; reals_ints; arrays; bv] (and depending on what other theories are supported)?

[Gbury]

Where is the sugar different between Ints and RealsInts, for example?

Well, that's the annoying part about the spec of the SMTLIB, a lot of things are hidden in the :extensions descriptions of the logics rather than the theories, but you can for isntance look at the extension of AUFLIRA for some of the syntactic sugar of RealsInts : http://smtlib.cs.uiowa.edu/logics-all.shtml#AUFLIRA

[Gbury]

Wouldn't it require something like merge [core; reals_ints; arrays; bv] (and depending on what other theories are supported)?

Yes, the default case could look like this rather than throwing an exception, though it would probably be done on the side of the caller to better emit a warning.

[Gbury]

Also, does anyone have access to an exhasutive list of the smtlib logics somewhere ? that would be useful to avoid similar problems, :)

[quicquid]

Unfortunately not - moreover, the logic declaration is supposed to change significantly with smtlib 3.0 (which is still a while away).

[c-cube]

SMTLIB 3.0 is not there yet, and dolmen is versioned anyway. A lot of smt2 files will stay there for a long time imho.

[Gbury]

Well, the parser are now versioned (as soon as I merge the relevant PR), but I haven't yet versioned the typechecker theories.

[c-cube]

If there's still a unique typechecker that is configured depending on the input format, I imagine it'd be more about mappings from (smt2.set-logic …) and (smt3.set-logic …) to a set of theories to be merged, than actual versioning?

[Gbury]

Yes, the core of the typechecker is unlikely to change (after all, it basically type-checks first order which will not change), only the theories need to be versioned, which should be doable reasonably.

[quicquid]

I ran dolmen on some of my hand-written files and saw that other logics are also missing: ALIA, UFDT, AUFDTLIA. They do not occur in Cesare's all logics lists though - I'm mostly composing features from QF_, A, UF, DT, LIA, LRA, NIA, NRA and BV where the order in the string is the order given here (I'm not sure about BV though).

[Gbury]

I'm not seing instances of the DT theory ina any logic described on the smtlib website (excluding that one, what is missing is mainly some combination I just hadn't seen on the list), is it an official theory/logic component, or just a convenient way to activate datatype reasoning (according to the standard the typechecking of datatypes seems to always be mandatory) ?

[c-cube]

I think the combinatorial explosion of logics has been made too clear with the addition of DT, so no one tried to name all the combinations of old logics with DT 🤷‍♂️

[Gbury]

Right... would there be a nice enough algorithm for splitting a logic into a list of theories ?

[Gbury]

The last commit should have closed this issue, ^^