1 files changed, 121 insertions, 0 deletions
diff --git a/job_scheduling/generate-jobscheduling.py b/job_scheduling/generate-jobscheduling.py
new file mode 100755
index 0000000..5cf9b04
--- /dev/null
+++ b/job_scheduling/generate-jobscheduling.py
@@ -0,0 +1,121 @@
+#!/usr/bin/env python
+# Usage for 3a (first argument is the deadline):
+#   $0 -1 | z3 -smt -in
+# Usage for 3b:
+#   $0 90 b | z3 -smt -in
+
+import sys
+
+# Deadline
+deadline = int(sys.argv[1])
+is_b = len(sys.argv) >= 3 and sys.argv[2] == 'b'
+
+
+# Number of jobs
+n = 12
+
+# For i: (j, ...), job i must not start before jobs j have ended.
+job_dependencies_ended = {
+    3:  (1, 2),
+    5:  (3, 4),
+    7:  (3, 4, 6),
+    9:  (5, 8),
+    11: (10,),
+    12: (9, 11),
+}
+
+job_dependencies_started = {
+    8: (5,),
+}
+
+job_durations = {
+    i: i + 5 for i in range(1, n + 1)
+}
+
+
+def fillin(cases, template_vars):
+    if type(cases) == str:
+        return cases.format(**template_vars)
+    return [template.format(**template_vars) for template in cases]
+
+literals = []
+preds = []
+
+# Start time of all jobs
+# and their duration
+for i in range(1, n + 1):
+    literals += fillin([
+        "t{i}",
+        "d{i}",
+    ], vars())
+    # times must be positive and
+    # all jobs must finish before the deadline.
+    preds += fillin([
+        "(>= t{i} 0)",
+        "(<= (+ t{i} d{i}) {deadline})",
+    ], vars())
+
+# Define duration
+for i, duration in job_durations.items():
+    preds += fillin([
+        "(= d{i} {duration})"
+    ], vars())
+
+# Job i may not start before job(s) j have *ended*. Or:
+# for all j: t_j + d_j <= t_i
+for i, deps in job_dependencies_ended.items():
+    for j in deps:
+        preds += fillin([
+            "(<= (+ t{j} d{j}) t{i})"
+        ], vars())
+
+# Job i may not start before job(s) j have *started*. Or:
+# for all j: t_j <= t_i
+for i, deps in job_dependencies_started.items():
+    for j in deps:
+        preds += fillin([
+            "(<= t{j} t{i})"
+        ], vars())
+
+# Jobs 5, 7 en 10 require a special equipment of which only one copy is
+# available, so no two of these jobs may run at the same time.
+# Or:
+# There must exist a pair of jobs (i, j) s.t. one starts after another ended:
+# t_i + d_i <= t_j
+jobs_max2_for_3 = (5, 7, 10)
+altpreds = []
+for i in jobs_max2_for_3:
+    for j in jobs_max2_for_3:
+        if i == j:
+            continue
+        altpreds += fillin([
+            "(<= (+ t{i} d{i}) t{j})"
+        ], vars())
+
+preds += ["(or %s)" % " ".join(altpreds)]
+
+# Begin generator
+s = """(benchmark test.smt
+:logic QF_UFLIA
+:extrafuns
+(
+"""
+s += "\n".join("(%s Int)" % x for x in literals)
+s += """
+)
+:formula
+(and
+"""
+s += "\n".join(preds)
+s += """
+))
+"""
+
+try:
+    import sys
+    print(s)
+    # Hack to avoid printing a ugly error in case stdin of next pipe is closed.
+    sys.stdout.flush()
+    sys.stdout.close()
+except BrokenPipeError:
+    pass