Finding all non-monotonically increasing sequences of four numbers in range 1..4

z3-mono-seq.py

from z3 import *

if __name__ == '__main__':
   s = Solver()
   a1 = Int('a1')
   a2 = Int('a2')
   a3 = Int('a3')
   a4 = Int('a4')
   s.add(a1 <= a2, a2 <= a3, a3 <= a4)
   s.add(a1 <= 4, a2 <= 4, a3 <= 4, a4 <= 4)
   s.add(a1 >= 1, a2 >= 1, a3 >= 1, a4 >= 1)

   while s.check() == sat:
       m = s.model()
       print m
       s.add(Not(And(a1 == m[a1], a2 == m[a2], a3 == m[a3], a4 == m[a4])))