import matplotlib.pyplot as plt
from z3 import *
import networkx as nx

def colorIt(n,F):
    #colors=[0]*n
    #colors = [Int('color_%s' % i) for i in range(n)]
    colors=[]
    colors.append(Int('color_0'))
    colors.append(Int('color_1'))
    colors.append(Int('color_2'))
    colors.append(Int('color_3'))
    colorCondition1 = []
    colorCondition1.append(And(0 <= colors[0], colors[0] < n))
    colorCondition1.append(And(0 <= colors[1], colors[1] < n))
    colorCondition1.append(And(0 <= colors[2], colors[2] < n))
    colorCondition1.append(And(0 <= colors[3], colors[3] < n))


    colorCondition2 = []
    for f in F:
        if f[1] > f[0]:
            temp = f[1]
            f[1] = f[0]
            f[0] = temp

    colorCondition2.append(And(1 <= (colors[F[0][1]] - colors[F[0][0]])))
    colorCondition2.append(And(1 <= (colors[F[1][1]] - colors[F[1][0]])))
    colorCondition2.append(And(1 <= (colors[F[2][1]] - colors[F[2][0]])))
    colorCondition2.append(And(1 <= (colors[F[3][1]] - colors[F[3][0]])))
    colorCondition2.append(And(1 <= (colors[F[4][1]] - colors[F[4][0]])))
    colorCondition2.append(And(1 <= (colors[F[5][1]] - colors[F[5][0]])))
    s=Solver()
    s.add(colorCondition1 + colorCondition2)
    if s.check() == sat:
        for n in range(n):
            print("%s" % (s.model()[colors[n]]))
    print(s.check())
    return colors

#
# n = int(raw_input("Enter the nodes in the graph: "))
# print(n)
# G = nx.Graph()
# for i in range(0,n):
#     G.add_node(i)
# x1 = int(raw_input("Enter the number of edges in the graph: "))
# E=[]
# for i in range(0,x1):
#         e1=int(raw_input("Enter the first node: "))
#         e2=int(raw_input("Enter the second node: "))
#         E.append([e1,e2])
#         G.add_edge(e1,e2)
# print(E)
# F = sorted(E)
E = [(0, 1), (2, 0), (0, 3),(1, 2), (1, 3), (2, 3)]
n = 4

print(colorIt(n,E))