from z3 import *

# Partition range [1, N) evenly into P sub-ranges

N = 10
P = 4

sz = [Int('sz' + str(i)) for i in range(P)]

s = Solver()

# Similar:
for i in range(P):
  for j in range(P):
    s.add (sz[i] - sz[j] <= 1)
    
# Add up to N:
s.add(Sum([sz[i] for i in range(P)]) == N)    
                 
if s.check() == sat:
  print [s.model().evaluate(sz[i]) for i in range(P)]
else:
  print 'No solution'