Represent array's length using Z3 interface for Java

Jan 15, 2015 at 4:31 PM
Hi,

I am using Z3 interface for Java for my Java project. There is a formula that I have to translate to an Expr instance containing array's elements and array's length. To represent array's elements I use MkSelect and MkStore method but I don't know how to represent for array's length. Could anyone please help me?

Thank you very much in advance!
Coordinator
Jan 16, 2015 at 1:40 PM
Arrays in SMT and in Z3 are conceptually of variable (potentially infinite) size, so there is no size or length operation. If your application needs only small arrays then it might be worth trying to encode them without the theory of arrays in an if-then-else type of constraint. We've answered a similar question on stackoverflow in the past, which might help you too: Create an array with fixed size and initialize it
Jan 19, 2015 at 9:18 AM
Hi wintersteiger,

The array embedded in my formula is quantified by forall quantifier, so I don't know how to encode it without the theory of arrays but loosing no information. For example, the constraint looks like below:

..&& (\forall int i; 0<=i<length(arr); arr[i]<=max;) && length(arr)>5 &&..

Could you please give me some suggestions for this case?
Thank you very much!
Coordinator
Jan 19, 2015 at 12:37 PM
Hmm, I don't think I have a good suggestion for this case. The property is essentially a property of the set of arrays (length>5) and, depending on the rest of what's in the property, it may be highly non-linear and/or undecidable. Personally, I would go for a stratification of this set, i.e., fix the size of the array to some specific size (e.g., length = 6) and prove the property just for that case. If it doesn't work, we're done, but if it does work, we increase length to 7. If you expect to find violations of the property, you will find them at some point (and we could do a binary-search like algorithm to speed it up). If you're actually trying to get a proof, we'll need some sort of induction argument that allows us to generalize from one array length to another.

Maybe someone else reading this has a better idea? Thanks!