Our implementation of ArrayEx is complete but we do not split on literals a = b where a and b are any arrays of the problem. Doing these splits during the search proof would be a bad idea because we do not need them to be complete. In the example of the issue #929, we obtain an equality of the form (store a1 x y) = (store a2 x y) and we know that (select a1 x) = (select a2 x). We never try to decide a1 = a2.
Notice that I update the set of arrays by tracking literals Eq of origin Subst. We know that this design is fragile because it could happen that substitutions are not sent to theories. The worst that can happen is to produced wrong models for arrays in very tricky cases. A better implementation consists in using our new global domains system to track selects in Adt_rel and use the keys of this map instead of arrays. I did not opt to this implementation to keep this PR simple and atomic.
This PR fixes the issue #929 about model arrays.
Our implementation of
ArrayExis complete but we do not split on literalsa = bwhereaandbare any arrays of the problem. Doing these splits during the search proof would be a bad idea because we do not need them to be complete. In the example of the issue #929, we obtain an equality of the form(store a1 x y) = (store a2 x y)and we know that(select a1 x) = (select a2 x). We never try to decidea1 = a2.Notice that I update the set of arrays by tracking literals
Eqof originSubst. We know that this design is fragile because it could happen that substitutions are not sent to theories. The worst that can happen is to produced wrong models for arrays in very tricky cases. A better implementation consists in using our new global domains system to trackselectsinAdt_reland use the keys of this map instead ofarrays. I did not opt to this implementation to keep this PR simple and atomic.