Proposal to lift nested array restriction on array logics

17 views
Skip to first unread message

Mathias Preiner

unread,
May 22, 2025, 9:01:08 PMMay 22
to smt...@googlegroups.com
Dear SMT-LIB community,

As you may know, some of the array logics defined at
https://smt-lib.org/logics-all.shtml
contain certain restriction on the array sort to disallow nested
(multi-dimensional) arrays.
Specifically, the logics AUFLIA, AUFLIRA, QF_ABV, QF_AUFBV, and
QF_AUFLIA have this restriction.

In recent years, we received multiple benchmark submissions to the
SMT-LIB benchmark library that encode problems over nested arrays
arrays. However, due to this restriction, the majority of these
benchmarks were not included in an SMT-LIB benchmark library release.
Some of these benchmarks were not caught by our checking process during
benchmark submission and are already included some of those in QF_ABV
and AUFLIA. The majority of newly submitted benchmarks, however, are
kept in a separate repository since they are considered "non-standard"
right now.

We SMT-LIB maintainers propose to lift this restriction
on all array logics to allow arbitrarily nested arrays. If I remember
correctly this restriction was set in place in the past to make it
easier on solver developers to support a certain array logic. However,
we believe the restriction should not be on the logic since this
prevents users to submit benchmarks that require nested arrays to the
SMT-LIB benchmark library. Solver developers are still free to choose
whether they want to support nested array or not and the SMT-COMP
organizers can decide whether they want to include such benchmarks in
the competition.

Please feel free to comment until end of June 2025. If there are no
objections we will lift this restriction in the above logics and we will
include the currently pending benchmarks in next year's SMT-LIB release.


Cheers,
Mathias (on behalf of the SMT-LIB maintainers)
OpenPGP_0xA4AF2BDE778B2463.asc
OpenPGP_signature.asc

BOBOT François

unread,
May 23, 2025, 3:25:03 AMMay 23
to smt...@googlegroups.com
Hi Mathias,

Le jeudi 22 mai 2025 à 18:00 -0700, Mathias Preiner a écrit :
Solver developers are still free to choose
whether they want to support nested array or not and the SMT-COMP
organizers can decide whether they want to include such benchmarks in
the competition.

Sorry I'm not answering your primary question first. But I would rather not add another question on the plate of the SMT-COMP organizers about whether accepting or not those benchmarks.
Moreover, and it is my primary concern without the logic to differentiate the benchmarks, another mechanism would be needed to filter them if they are not included in the competition.
In the same way two papers could experiment with the same logic but without really the same benchmarks.

The restrictions in the different theories are still a problem for sending benchmarks.  For example `(ite (forall x. x > x + 1) ... ...)` is refused by some solvers (and perhaps it the definition of the logics requires it?) when the logic `ALL` is not selected. In fact the only way to be sure that a file that uses all the features of the language is often to use this `ALL` logic.

We can also make the change with the 2.7 update (we already have some in BV). AUFLIA 2.6 no nesting AUFLIA 2.7 nesting. The competition/papers will need to make the distinction in any case.

Best,

-- 
François

Jochen Hoenicke

unread,
May 23, 2025, 8:07:14 AMMay 23
to smt...@googlegroups.com
Hello,

As a solver author, I would favor removing the restriction for arrays.  It always felt quite arbitrary, especially since AUFLIRA allows nested arrays (but only one nesting). We never had any restriction on the element type (except cardinality >= 2), so you can nest the arrays arbitrarily deep.   And it's also useful for program analysis to support nested arrays directly for modelling two dimensional arrays or arrays on the heap.

For the index type it may be useful to still restrict the type to Int in AUFLIRA and BitVec in ABV.   Although our solver has no problems using uninterpreted sorts, reals or even arrays as index value, it may be easier for solver authors if they can rely on the index type.

For the competition, I think it's okay to just run those benchmarks (starting next year).  I think it is not a huge burden to support nested arrays and most solvers already do it.  And if some solver chooses not to support it, it can still compete. It will just not be able to solve all benchmarks in the logic.

Best,
  Jochen
Reply all
Reply to author
Forward
0 new messages