Extensional vs. Non-extensional Theory of Arrays

[Brandon King]

Hi All,

Maybe I missed something, but I can't seem to figure out the difference between the Extensional vs. Non-extensional aspect of the theory of arrays. Is the extensional aspect just the assumption about (= t3 mt) being equal if all elements of t3 are equal to mt? 

-Brandon

[Tikhon Jelvis]

I think that is the only difference, yes. This is important because not relying on = for arrays could speed your search up. Of course, you would then have to check it yourself by writing equality assertions for each element manually (or generating them, as the case may be).

-Brandon

--
 
 

[Ras Bodik]

In other words, if you replace (= t3 mt) with a conjunction of equalities over individual array elements, the search will be faster.  It’s interesting to consider why this is so.

 

--
 
 

[CUONG ANH NGUYEN]

That's weird because doing that didn't seem to give any significant performance improvement on my machine unless my encoding wasn't correct. Does it have anything to do with BitVector, or if we do the same thing for Integer, we will gain performance improvement as well?

Thanks.

--
 
 

 

[Tikhon Jelvis]

BitVectors are inherently bounded where integers are not. For integers, specifying the comparisons you need to do explicitly essentially adds one piece of information: the size of the array. (If you use a bunch of non-contiguous indices, I suppose it adds more information.) Using BitVectors of some particular size adds exactly the same information. So your results seem to make sense--the difference should intuitively be far more important with integer indices than BitVector indices. 

--