from z3 import *

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

N = 14
P = 4

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

s = Solver()

C = Int('C')

# Implementation
for i in range(P):
  s.add(sz[i] == 
    If(i < If(C == 0, 2,
           If(C == 1, N/P,
           N%P)), 
      N/P + 1, 
      N/P))

# 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)    
    
# print str(s)    

if s.check() == sat:
  print 'C =', s.model().evaluate(C)
else:
  print 'No solution'






























# s = Solver()

# # Add up to N:
# s.add(Sum([sz[i] for i in range(P)]) == N)

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


  
  
  
# # Precondition
# s.add (N >= P)

# # Implementation
# for i in range(P):
  # s.add (sz[i] == If(i < N%P,  N/P + 1, N/P))
  
# # Check if "Add up to N" can be violated:
# s.push()
# s.add(Not(Sum([sz[i] for i in range(P)]) == N))
# if s.check() == sat:
  # print 'Subranges might not add up to N'
  # print 'for N = ', s.model().evaluate(N)
  # exit()
# s.pop()
  

# # Check if "similar" can be violated
# for i in range(P):
  # for j in range(P):
    # s.push()
    # s.add (Not(sz[i] - sz[j] <= 1))
    # if s.check() == sat:
      # print 'Subranges', i, 'and', j, 'might not be similar!'
      # exit()
    # s.pop()
    
# print 'Verified for all N!'























# # Add up to N:
# s.add(Sum([sz[i] for i in range(P)]) == N)

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