Constant array values in the model #525
Description
Hello everyone,
while working on #520 I've noticed that most of our solver backends have issue when generating model values for arrays. Specifically, Z3 will often "forget" an index, CVC4/5 just returns the Store expression, and Bitwuzla doesn't produce any assignments at all. These are issues with our backend as the solvers do return correct values.
Most of this could be fixed, but I think there is another issue with the way we represent arrays in our model: Solvers will generally return a Store expression for the array value, which is then translated into a set of assignments. So,for instance, if the solver returns
array: (store (store ((as const (Array Int Int)) 0) 1 10) 2 20)
we would generate the following assignments:
array(1): 10
array(2): 20
Here the array is treated similar to an uninterpreted function and we just list all the mappings. The advantage is that we now only have constant terms for the arguments (= indices) and value (= element) that can be easily represented in Java. However, this conversion breaks down if we also have to consider constant array values. We already had this case in the example, where ((as const (Array Int Int)) 0) is not represented by any assignment and simply gets dropped. This is the reason why Z3 will sometimes forget an index: The solver simplifies (store (store ((as const (Array Int Int)) 0) 1 10) 2 20) to (store (as const (Array Int Int)) 10) 2 20), however, since we can't represent the const term we "forget" that 1 was supposed to map to 10
There are probably ways around this issue if the terms only contain store and select expression. In that case the const statement can be replaced by a new variable and we may just have to add a few more mappings for indices that used to be covered by the default case. However, since it's now also possible to create const terms in JavaSMT, there are cases where this simply won't work. As a trivial example, take
(assert (= arr ((as const (Array Int Int)) 0)))
Here we would currently return an empty set of assignments. However, this isn't correct as arr really needs to be ((as const (Array Int Int)) for the formula to be true, but an empty set of assignments means that any array will do. If we wanted to list all assignments for const we would get an infinite set:
...
arr(-2) = 0
arr(-1) = 0
arr(0) = 0
arr(1) = 0
arr(2) = 0
...
One ways to fix this is to represent const arrays as the "default" branch of the function. In our example we would then get something like this:
array(1): 10
array(2): 20
array(x): 0
This can be read just as in programming languages like Haskell: We try to match the cases from top to bottom, and if none of them match we wind up in the default branch
This can also be extended to more than one index:
array2(1,1): 10
array2(1,7): 20
array2(1,y): 0
array2(2,3): 30
array2(2,4): 40
array2(2,y): 1
array2(x,y): 2
Notice that we now have 3 different "default" values. The first two are for specific values of the first argument, and the third one is for the function in general
The downside of this approach is that there are now variables on the left side, and pattern matching needs to be used to figure out which of the definitions applies for any given input. It's also difficult to translate these assignments back into a formula without using some special logic. Normal assignments like array(1): 10 can be expressed as (= (select array 1) 10). However, for the default case array(x): 0 we would have to write (forall ((x Int)) (and (distinct x 1 2) (= (select array x) 0))). Having to use quantifiers seems a bit unfortunate, and users may simply not know how to handle such assignments
Another way of fixing this is to simply return the value the solver gave us in the model. This is what CVC4/5 are currently doing:
array: (store (store ((as const (Array Int Int)) 0) 1 10) 2 20)
However, this means that we can no longer easily represent these values in Java, and users don't get easy access to the index or the values of the array
@baierd , @kfriedberger:
What's your opinion on this? Do you see an easy way to represent const arrays in the model?