from z3 import *

def eval(x,m):
  return str(x) + "=" + str(m[x]) + " "

x1 = Bool("x1")
x2 = Bool("x2")
x3 = Bool("x3")
x4 = Bool("x4")
x5 = Bool("x5")
x6 = Bool("x6")
x7 = Bool("x7")
x8 = Bool("x8")
x9 = Bool("x9")
x10 = Bool("x10")

chi = [
  Or(Not(x1), x3),\
  Or(Not(x7), x2),\
  Or(x7, x2),\
  Or(x1, Not(x2))]

phi = [
  Or(Not(x1), Not(x2)),\
  Or(Not(x1), x2),\
  Or(Not(x1), x7),\
  x1,\
  Or(Not(x3), x4),\
  x3,\
  Or(Not(x3), Not(x4)),\
  Or(x5, x4),\
  Or(Not(x4), x5),\
  Or(x1, Not(x5), x6),\
  Or(x5, Not(x6)),\
  x7,\
  Or(Not(x7), x8),\
  Or(Not(x7), Not(x8), x6),\
  Or(Not(x7), Not(x8), Not(x6)),\
  Or(Not(x1), Not(x3))]

solver = Solver()
solver.set(unsat_core=True)
def assertAll(phi, pre):
  print("assert all:")
  i=0
  m = {}
  for c in phi:
    solver.assert_and_track(c, pre + str(i))
    print " " + pre + str(i) + ": " + str(c)
    m[pre + str(i)] = c
    i = i + 1
  return m 

chi_map = assertAll(chi,"c")
phi_map = assertAll(phi,"p")
phi0 = phi
print(phi_map)
res = solver.check()
i = 0
cost = 0
while res == z3.unsat and i < 15:
  print(str(i) + " unsatisfiable:")
  uc = solver.unsat_core()
  print(uc)
  bs = []
  for cid in uc:
    #print "UC contains ", cid, str(cid) in phi_map
    if str(cid) in phi_map:
       b = FreshBool("b"+str(i)+"_")
       c = phi_map[str(cid)]
       phi = [Or(c,b) if c == d else d for d in phi ]
       bs.append(b)
  solver = Solver()
  solver.set(unsat_core=True)
  card = sum(If(b,1,0) for b in bs) == 1
  #print "card constraint: ", card
  solver.assert_and_track(card, "card")
  phi_map = assertAll(phi,"p")
  chi_map = assertAll(chi,"c")
  res = solver.check()
  i = i + 1
  cost = cost + 1
m = solver.model()
print i, " iterations"
print m[x1], m[x2], m[x3], m[x4], m[x5], m[x6],m[x7], m[x8], m[x9]

ms = 0
for c in phi0:
  if m.evaluate(c) == True:
    print " true: ", c
    ms = ms + 1

print "cost ", cost, " max sat", ms, "size ", len(phi)