Solve using Z3 solver a condition with a length of an arbitrary size array

Question

I'm learning Z3 solver. I have a question about Arrays and related conditions. In particular, I have to create Z3py code to solve the if condition below:

totalAccounts = [ 1, 2, 3, 4, 5 ]    

def (myAccounts):
   cnt = len(myAccounts)
   if (cnt > 10) doSomething()

myAccounts is a list of Integers, subset of the list totalAccounts. The condition to pass is cnt > 10 which depends on the length of myAccounts list.

I think I need to represent myAccounts as a Z3's Array and copy the values in totalAccounts on it using the function Store.

MYACCOUNTS = Array ('MYACCOUNTS', IntSort(), IntSort())
I = Int('I')
i = 0
for elem in totalAccounts:
  MYACCOUNTS = Store(MYACCOUNTS, i, elem)
  i = i + 1

But I don't know how to represent the length of such array in creating the condition to add to the solver:

solver = Solver()
solver.add( ??? > 10 )

Am I doing it right?

Answer 1

SMTLib arrays (and consequently z3 and z3py arrays) are indexed by their entire domain type. In your example, the index type is Int(), so the array has an element for any integer value. Note that this is different than the usual treatment of arrays in programming languages where you usually get a "length" of an array. You can read more about SMTLib arrays here: http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf (page 39, in particular.)

To model any notion of array length, one typically keeps track of it in a separate symbolic variable, and whenever properties are expressed, it's typically done in reference to that variable. Asking exactly what problem you're trying to solve will get you further.

You might also want to review the Z3 guide (https://rise4fun.com/z3/tutorial/guide), which also has a section on arrays. Stack-overflow also has similar questions regarding array usage in z3py, here's one example answer, relevant to the current context: https://stackoverflow.com/a/23743450/936310