How to set constraints for all elements in z3py sequence?

Question

I am continuing to explore z3py sequences. Here I want to create a sequence of only positive values. Here's the code:

from z3 import *

s = Solver()

# declare a sequence of integers
seq = Const('seq', SeqSort(IntSort()))

# assert the sequence have at least 5 elements
s.add(Length(seq) >= 5)

# get a model and print it:
if s.check() == sat:
    print(s.model()) 
    

So here the output values are not limited in any way. How can I set constraints for all elements in seq to make them positive?

Thanks!

Answer 1

To assert such constraints, you use universal quantification. The following shows how to make sure all elements are > -5, < 0:

from z3 import *

s = Solver()

# declare a sequence of integers
seq = Const('seq', SeqSort(IntSort()))

# assert the sequence have at least 5 elements
s.add(Length(seq) >= 5)

dummyIndex = FreshInt('dummyIndex')
s.add(ForAll(dummyIndex, Implies(dummyIndex < Length(seq), And(seq[dummyIndex] > -5, seq[dummyIndex] < 0))))

# get a model and print it:
if s.check() == sat:
    print(s.model()[seq])

When run, this prints:

Concat(Unit(-1),
       Concat(Unit(-3),
              Concat(Unit(-2), Concat(Unit(-3), Unit(-4)))))

Note that adding quantifiers to the logic make it semi-decidable; i.e., in the presence of complicated constraints z3 can return unknown, or loop forever.