title: How to use z3 Solver to solve Kirkman’s Schoolgirl Problem?
body: <p>I'm new to SMT problems and tried to copy how to solve Kirkman’s Schoolgirl Problem with z3/MK85 in SAT/SMT using an example written by Dennis Yurichev. But when I tried to get the model (what I used is Z3):</p>
  
  <p><code>m["%d_%d" % (person , day)]</code></p>
  
  <p>the Python has some errors :</p>
  
  <blockquote>
    <p>Traceback (most recent call last):</p>
    
    <p>File "", line 1, in </p>
    
    <p>File "D:\Z3\z3-master\z3-master\build\python\z3\z3.py", line 6138, in __getitem___z3_assert(False, "Integer, Z3 declaration, or Z3 constant expected")</p>
    
    <p>File "D:\Z3\z3-master\z3-master\build\python\z3\z3.py", line 92, in _z3_assert raise Z3Exception(msg) z3.z3types.Z3Exception: Integer, Z3 declaration, or Z3 constant expected</p>
  </blockquote>
  
  <p>I wonder if I got confused with the model's expression? .I'd love to debug it.
  Besides, I wonder if there is another way to solve it in Z3 and the expression difference between z3 and MK85.</p>
  
  <pre class="lang-py prettyprint-override"><code>from z3 import *
  import itertools
  PERSONS , DAYS , GROUPS = 15, 7, 5
  s=Solver()
  tbl=[[BitVec("%d_%d"%(person , day), 16) for day in range(DAYS)] for person in range(PERSONS)]
  for person in range(PERSONS):
     for day in range(DAYS):
        s.add(And(tbl[person][day]&gt;=0, tbl[person][day] &lt; GROUPS))
  def only_one_in_pair_can_be_equal(l1, l2):
     assert len(l1)==len(l2)
     expr=[]
     for pair_eq in range(len(l1)):
               tmp=[]
               for i in range(len(l1)):
                       if pair_eq==i:
                               tmp.append(l1[i]==l2[i])
                       else:
                               tmp.append(l1[i]!=l2[i])
               expr.append(And(*tmp))
     s.add(Or(*expr))
  for pair in itertools.combinations(range(PERSONS), r=2):
     only_one_in_pair_can_be_equal (tbl[pair[0]], tbl[pair[1]])
  assert s.check()
  m=s.model()
  print("group for each person:")
  print("person:"+"".join([chr(ord('A')+i)+" " for i in range(PERSONS)]))
  for day in range(DAYS):
     print("day=%d:" % day)
     for person in range(PERSONS):
        print(m["%d_%d" % (person , day)])  #error
     print("")
  
  def persons_in_group(day, group):
       rt=""
       for person in range(PERSONS):
               if m["%d_%d" % (person , day)]==group:#error
                       rt=rt+chr(ord('A')+person)
       return rt
  for day in range(DAYS):
       print( "day=%d:" % day)
       for group in range(GROUPS):
               print(persons_in_group(day, group)+" ")
       print(" ")
  </code></pre>
  
  <p>I expect to debug it or solve this question in another way.</p>