Support for Multi-Dimensional Arrays in QF_AUFBV?

Question

I am currently working on code that translates a "path" through a C program into the corresponding SMT query to test the feasibility of this path. I have working code that create a SMT-LIB v1.2 query, and that uses Z3 2.11 and the QF_AUFBV logic to solve the query. I am currently porting this code over to Z3 4.3, to take advantage of any speed advances that may have happened since then, especially since my former code seems to take a long time (around 22 minutes) on a query that merely assigns 24 values to a three-dimensional array and checks the value of a certain location in the array.

However, it seems that the QF_AUFBV logic (as of the SMT-LIB v2.0 standard) no longer supports multi-dimensional arrays, or rather arrays whose values are also arrays (potentially deeper). Once I take out the line "(set-logic QF_AUFBV)" from my query, Z3 4.3 is able to process the query, but it still takes a long time.

I was wondering if anyone knew why support for multi-dimensional arrays was stopped in the SMT-LIB v2.0 standard, and what alternative logics I could use. I was also wondering what logic Z3 was anyway using when I took out the line that specified the QF_AUFBV theory.

Thanks!

Answer 1

The SMT-LIB standard never had support for multi-dimensional arrays. Z3 could process them, but they were not part of the standard. SMT-LIB 1.0 is a very restrictive format, that is why Z3 had several extensions for accommodating user needs. On the other hand, SMT-LIB 2.0 is a very rich input format and fixes the main issues users had with SMT-LIB 1.0. In Z3 4.x, when the logic is specified in the input file, Z3 tries to be compliant with the SMT-LIB 2.0 standard. When the set-logic is removed, all Z3 specific extensions are enabled.

As you described, an array sorrt (Array I1 I2 R) can be encoded as (Array I1 (Array I2 R)).

Regarding performance, Z3 3.x and 4.x do not have performance improvements for the array theory. They have many improvements for bit-vectors, but they are not available when the problem mixes arrays and bit-vectors. A new array theory is in TODO list, but nobody in the Z3 team is currently working on that.