Reducing an integer set in z3 over addition

I'm experimenting with (and failing at) reducing sets in z3 over operations like addition. The idea is eventually to prove stuff about arbitrary reductions over reasonably-sized fixed-sized sets.

The first of the two examples below seems like it should yield unsat, but it doesn't. The second does work, but I would prefer not to use it as it requires incrementally fiddling with the model.

def test_reduce():
  LIM = 5
  VARS = 10
  poss = [Int('i%d'%x) for x in range(VARS)]
  i = Int('i')
  s = Solver()
  arr = Array('arr', IntSort(), BoolSort())
  s.add(arr == Lambda(i, And(i < LIM, i >= 0)))
  a = arr
  for x in range(len(poss)):
    s.add(Implies(a != EmptySet(IntSort()), arr[poss[x]]))
    a = SetDel(a, poss[x])
  def final_stmt(l):
    if len(l) == 0: return 0
    return If(Not(arr[l[0]]), 0, l[0] + (0 if len(l) == 1 else final_stmt(l[1:])))
  sm = final_stmt(poss)
  s.push()
  s.add(sm == 1)
  assert s.check() == unsat

Interestingly, the example below works much better, but I'm not sure why...

def test_reduce_with_loop_model():
  s = Solver()
  i = Int('i')
  arr = Array('arr', IntSort(), BoolSort())
  LIM = 1000
  s.add(arr == Lambda(i, And(i < LIM, i >= 0)))
  sm = 0
  f = Int(str(uuid4()))
  while True:
    s.push()
    s.add(arr[f])
    chk = s.check()
    if chk == unsat:
      s.pop()
      break
    tmp = s.model()[f]
    sm = sm + tmp
    s.pop()
    s.add(f != tmp)
  s.push()
  s.add(sm == sum(range(LIM)))
  assert s.check() == sat
  s.pop()
  s.push()
  s.add(sm == 11)
  assert s.check() == unsat

Solution

Note that your call to:

    f = Int(str(uuid4()))

Is inside the loop in the first case, and is outside the loop in the second case. So, the second case simply works on one variable, and thus converges quickly. While the first one keeps creating variables and creates a much harder problem for z3. It's not surprising at all that these two behave significantly differently, as they encode entirely different constraints.

As a general note, reducing an array of elements with an operation is just not going to be an easy problem for z3. First, you have to assume an upper bound on the elements. And if that's the case, then why bother with Lambda or Array at all? Simply create a Python list of that many variables, and ignore the array logic completely. That is:

elts = [Int("s%d"%i) for i in range(100)]

And then to access the elements of your 'array', simply use Python accessor notation elts[12].

Note that this only works if all your accesses are with a constant integer; i.e., your index cannot be symbolic. But if you're looking for proving reduction properties, that should suffice; and would be much more efficient.