gistfile1.txt

from z3 import *

# find autobiographical numbers                                                                                                

def auto(lim):
  if lim < 1 or lim > 10:
    raise Exception('only 1..10 are valid arguments')

  print str(lim) + " : ",

  s = Solver()
  vars = []

  for x in range(0, lim):
    v = Int('X' + str(x))
    s.add(v >= 0, v < lim)
    vars.append(v)

  for x in range(0, lim):
    sum = 0
    for y in range(0, lim):
      sum = sum + If(vars[y] == x, 1, 0)
    s.add(vars[x] == sum)

  s.add(vars[0] != 0)

  r = s.check()
  if r == sat:
    m = s.model()
    for x in range(0, lim):
      z = m[vars[x]]
      print z.as_string(),
    print
  else:
    print r

for i in range(1, 11):
  auto(i)