Update requirement 3

from z3 import *


real_values = \
    {
    1: (None,1,2), #VLAN 100, cluster 2, hierachy 0
        2: (None,2,1),
        3:(None,3,1),
        4:(110,2,0),
        5:(120,2,0),
        6:(130,3,0),
        7:(140,3,0)
}

def a(i):
    return []

variables_dict = dict()
possible_v = [110,120,130,140]
nr_routers = [x for x in range(1,8)]
print(nr_routers)
S = Solver()




for i in nr_routers:

    for j in nr_routers:
        for v in possible_v:
            ri_v_j_bool = Bool(f"({i},{v},{j})")
            variables_dict[(i,v,j)] = ri_v_j_bool

def add_edge_between(i,j):
    bools = []
    bools += [Bool(f"({i},{v},{j})") for v in possible_v]
    bools += [Bool(f"({j},{v},{i})") for v in possible_v]
    return Or(bools)

big_or = Or([ri_v_j_bool for ri_v_j_bool in variables_dict.values()])
S.add(big_or)

def get_ri_v_rj(ivj_tuple):
    return variables_dict[ivj_tuple]

#No router send to itself unless it is in the same VLAN
for i in nr_routers:
    v_i = real_values[i][0] #The VLAN of router i
    for v in possible_v:
        ri_v_ri = get_ri_v_rj((i, v, i)) #Ri sends to Ri using VLAN v
        if(v_i == v):
            S.add(Or(ri_v_ri,Not(ri_v_ri))) #(!(ri,v,ri) V (ri,v,ri))
            a = 2
        else:
            S.add(Not(ri_v_ri))

#Two routers in the same cluster and on the same level must route to the same destination and target
for i in nr_routers:
    for j in nr_routers:
        #c_i = cluster I
        #h_i = Hiearchy of i
        c_i = real_values[i][1]
        h_i = real_values[i][2]

        c_j = real_values[j][1]
        h_j = real_values[j][2]

        if((i != j) and (c_i == c_j) and (h_i == h_j)):

            #The target router
            for k in nr_routers:
                for v in possible_v:
                    ri_v_rk = get_ri_v_rj((i,v,k))
                    rj_v_rk = get_ri_v_rj((j,v,k))
                    S.add(Implies(ri_v_rk,rj_v_rk))


#Traffic to a different cluster has to be to a higher hierachy level than the target addres
for i in nr_routers:

    c_i = real_values[i][1]
    h_i = real_values[i][2]


    for v in possible_v:

        #Find the owner
        for k,(v_k,c_k,h_k) in real_values.items():
            if(v_k == v):
                # c_i = cluster I
                # h_i = Hiearchy of i
                c_owner = c_k
                h_owner = h_k
                r_owner = k

        for j in nr_routers:
            c_j = real_values[j][1]
            h_j = real_values[j][2]

            if((c_owner != c_i)):
                if(not(h_j > h_owner)):
                    i_v_j = get_ri_v_rj((i,v,j))
                    S.add(Not(i_v_j))






def get_solutions(s: z3.z3.Solver):
    result = s.check()
    # While we still get solutions
    while (result == z3.sat):
      m = s.model()
      yield m
      # Add new solution as a constraint
      block = []
      for var in m:
          block.append(var() != m[var])
      s.add(z3.Or(block))
      # Look for new solution
      result = s.check()

if __name__ == "__main__":
    if S.check() == sat:
        solutions = get_solutions(S)
        upper_bound = 100
        r = set()
        for m, _ in zip(solutions, range(upper_bound)):
            for x in m:
                if(is_true(m[x])):
                    r.add(x)
            print(r)