smtlib parser: Unknown logic UF about dolmen HOT 20 CLOSED

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

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).

from dolmen.

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.

from dolmen.

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

from dolmen.

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, :/

from dolmen.

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

My intuition would be that RealsInts is the right default.

from dolmen.

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.

from dolmen.

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

from dolmen.

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

from dolmen.

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.

from dolmen.

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

from dolmen.

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

from dolmen.

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.

from dolmen.

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

from dolmen.

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?

from dolmen.

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.

from dolmen.

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).

from dolmen.

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) ?

from dolmen.

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 🤷‍♂️

from dolmen.

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

from dolmen.

The last commit should have closed this issue, ^^

from dolmen.