feat : add unusable python script because of exponential explosion

project2/gen_z3.py

+# -*- coding: utf-8 -*-
+import itertools
+import sys
+
+la05 = "/home/belazy/Desktop/Projects/logia/project2/job10"
+
+def name_job(worker,work) :
+    return "job" + str(worker) + "_" + str(work)
+
+def get_jobs(file):
+    res = []
+    f = open(file, "r")
+    worker = 0
+    lines = f.readlines()
+    fuck_this = lines[0].split(" ")
+    n_of_workers = fuck_this[0]
+    n_of_machines = fuck_this[1]
+    for str in lines[1:]:
+        line = []
+        split = str.removesuffix("\n").split(" ")
+        work = 0
+        for i in range(int(len(split)/2)):
+            line.append((
+                name_job(worker,work),
+                int(split[2*i]),
+                int(split[2*i+1])))
+            work +=1
+        res.append(line)
+        worker +=1
+    return res,int(n_of_workers),int(n_of_machines)
+
+def op(op,x,y):
+    return "(" + op + " " + str(x) + " " + str(y) + ")"
+
+def le(x,y):
+    return op("<=",x,y)
+
+def plus(x,y):
+    return op("+",x,y)
+
+def and_(args):
+    res = "(and "
+    for i in args:
+        res += i
+    res += ")\n"
+    return res
+
+def or_(args):
+    res = "(or "
+    for i in args:
+        res += i + " "
+    res += ")\n"
+    return res
+    
+def ass(x):
+    return "(assert " + x + " )\n"
+
+def define_job(str):
+    return "(declare-fun " + str + " () Int)\n"
+
+        
+def define_jobs(jobs):
+    res = ""
+    for worker in jobs:
+        for job in worker:
+            res += define_job(job[0])
+    return res
+    
+def define_positive_times(jobs):
+    res = ""
+    for worker in jobs:
+        for job in worker:
+            res +=ass(le(0,job[0]))
+    return res
+
+def define_order_constraints_worker(worker):
+    res = ""
+    for i in range(len(worker)-1):
+        res += ass(le(
+                   plus(worker[i][0],worker[i][2]),
+                   worker[i+1][0]))
+    return res    
+    
+def define_order_constraints(jobs):
+    res = ""
+    for worker in jobs:
+        res += define_order_constraints_worker(worker)
+    return res
+
+def get_machine_constraints(jobs,machine):
+    res = []
+    for worker in jobs:
+        for job in worker:
+           if job[1] == machine:
+               res.append((job[0],job[2]))
+    return res
+
+def get_machines_constraints(jobs,n_of_machines):
+    res = [[] for _ in range(n_of_machines)]
+    for worker in jobs:
+        for job in worker:
+            res[job[1]].append((job[0],job[2]))
+    return res    
+
+def define_machine_constraints(jobs):
+    perms = itertools.permutations(jobs)
+    print("generated permutations, len " + str(len(jobs)) +", " + str(type(perms)))
+    res = ""
+    n = 0
+    for jobs in perms:
+        constraints = []
+        for i in range(len(jobs)-1):
+            constraints += ass(le(
+                       plus(jobs[i][0],jobs[i][1]),
+                       jobs[i+1][0]))
+        res += and_(constraints)
+        print("generated " +str(n) +"th constraint" )
+        n +=1
+    return or_(res)
+
+def print_machine_constraints(jobs,file):
+    with open(file, 'w') as f:
+        perms = itertools.permutations(jobs)
+        print("generated permutations, len " + str(len(jobs)) +", " + str(type(perms)))
+        n = 0
+        print("(assert (or\n",file = f)
+        for jobs in perms:
+            constraints = []
+            for i in range(len(jobs)-1):
+                constraints += ass(le(
+                           plus(jobs[i][0],jobs[i][1]),
+                           jobs[i+1][0]))
+                print(and_(constraints),file = f)
+                print("generated " +str(n) +"th constraint" )
+                n +=1
+        print("))",file = f)
+
+
+read = get_jobs(la05)
+jobs = read[0]
+n_of_jobs = read[1]
+n_of_machines = read[2]
+
+test_output = "/home/belazy/Desktop/Projects/logia/project2/test_output"
+
+#print(get_machines_constraints(jobs,n_of_machines)[0])
+print(print_machine_constraints(get_machines_constraints(jobs,n_of_machines)[0],test_output))
+