Lack of a minimal logic for some problems (related to logic restrictions such as linearity)

[Gbury]

This is the natural follow-up of my talk at the SMT workshop (cf https://ceur-ws.org/Vol-3725/short6.pdf ).

While working on Dolmen, I found out that some problems in the SMT-LIB do not have a minimum (single minimal) logic and/or it is not clear how to assign a logic to a given problem. This mainly comes from the fact that a logic is actually a pair of a set of theories, and a set of restrictions on said theories. Additionally, some of these restrictions appear more strict that they need (or should) be, particularly around linear arithmetic.

As far as I'm aware, there are two instances of that problem: one with arrays, and and one with linear arithmetic.

The case of arrays

Some array theories restrict the types of arrays that can be used, specifically:

• QF_ABV, QF_AUFBV only allows arrays from bitvectors to bitvectors
• QF_AUFLIA, AUFLIA only allows arrays from integers to integers
• QF_AUFLIRA, AUFLIRAonly allows arrays of the form(Array Int Int)or(Array Int (Array Int Real))`

First, one can note some irregularity in the application of restrictions: for instance QF_ABV has a restriction, but not ABV, more on that at the end of this issue.

Now, the question is, what should be the logic of the following problem:

(set-logic ALL)
(declare-const a (Array Bool Bool))
(declare-const b (_ BitVec 5))
(assert (and (= a a) (= b b)))
(check-sat)

If looking only at the set of theories used, one would give that problem the logic QF_ABV, however the restrictions on the type of arrays prevent that classification. So one question that should be clarified is what is the recommended logic for such a problem (and more generally, problems that could belong to a logic if not for its restrictions) ?

The two different kind of linear arithmetic

The same problem applies to arithmetic, but in a subtly different way. Indeed, compared to arrays, there is always the option to use non-linear arithmetic which does not have any restriction. That being said, the current specification of linearity in arithmetic is ... less than ideal I'd say, as I often show during my dolmen talks, ^^

For the context: there are actually two different specifications of what is "linear" in the smtlib. Most of the linear arithmetic logics (e.g. AUFLIRA, LIA, LRA, QF_LIA, QF_UFLIA, QF_UFLRA, QF_LRA, UFLRA) specify linear terms as terms of the form c, ( * x c), ( * c x) where:

• x is a free constant of sort Int or Real and
• c is an integer or rational coefficient, respectively.
  Whereas some logics (e.g. AUFLIA, QF_AUFLIA), use the following:
• x is a free constant or a term with top symbol not in Ints, and
• c is a term of the form n or (- n) for some numeral n.

There are a few unfortunate consequences of these definitions:

• the term (* 2 3) is not linear (i.e. not allowed) in any of the linear arithmetic logics
• the term (* 2 (f x)) is linear (i.e. allowed) in (QF_)AUFLIA but not linear/allowed in (QF_)UFLIA, because (f x) is not a free constant of sort Int or Real.

This has unfortunate side consequences: consider the following smtlib problem:

(set-logic ALL)
(declare-const x Int)
(declare-fun f (Int) Int)
(assert (= 0 (* 2 (f x))))
(check-sat)
(exit)

Even though it would be the most natural choice, this problem does not belong to the QF_UFLIA logic (as explained above). This problem can be given the QF_AUFLIA logic, but it seems weird and unnecessary that the addition of the Array theory (which is not used at all by the problem) would suddenly make it acceptable. Similarly, we could give the QF_UFNIA logic to the problem, but it would be unfortunate that this is considered non-linear arithmetic.

This is a concrete problem, because we rely on the logic of a problem to interpret benchmarks of solvers (among other things). Misclassifying problems therefore would make it much harder to interpret the result of e.g. the SMT-COMP. Additionally, solvers that rely on the logic to tune their proof search (by enabling/disabling some decision procedures and/or heuristics) would suffer from an imprecision in logic classification.

To be a bit constructive, here is a proposal for a new definition of linearity, that should capture most (if not all) the realistic cases of linear expressions:

A term of the form (* a b) would be allowed in linear arithmetic if at least a or b is a literal expression, where a literal expression is either:

• an integer or rational coefficient
• an arithmetic operator (+, -, *, /, div, mod, abs, to_real, to_int) applied to literal expressions

More general issues about the current specification

More generally, there is a more pervasive and underlying issue that I think participates to the two situations described above: each logic is described as a set of theory, as well as restrictions specified as free text. This together with the natural and historical evolution of the SMT-LIB may have given rise to the existence of two different linearity specification. This also makes it annoying and painful to have an overview of the specification. I would propose that, much in the same way that each logic does not redefine its theories independently, the restrictions that a logic imposes could be defined separately, in a section that properly defines all restrictions, and then each logic would refer to one (or more) restriction that are imposed.

Conclusion

To sum it up, this issue actually raises the following questions/problems:

• the current specification of linearity is overly restrictive and should be improved
• specification of restrictions in logics could/should be defined separately from logics, so that they can be shared to ensure better coherence
• there is an issue where it is unclear what logic to assign to problems using arrays but not respecting the restrictions of their "natural" logic