Untitled

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)
}

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:
            variables_dict[(i,v,j)] = Bool(f"({i},{v},{j})")

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))
        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 one
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 different clusters
        if(c_i != c_j):
            #If not higher level -> false
            if(not (h_i < h_j)):
                for v in possible_v:
                    ri_v_rj = get_ri_v_rj((i, v, j))
                    S.add(Not(ri_v_rj))

if __name__ == "__main__":
    if S.check() == sat:
        m = S.model()
        r = []
        for x in m:
            if(is_true(m[x])):
                r.append(x)
        print(r)