1 files changed, 71 insertions, 0 deletions
diff --git a/homemade/generate-room-scheduling.py b/homemade/generate-room-scheduling.py
new file mode 100644
index 0000000..ffd101e
--- /dev/null
+++ b/homemade/generate-room-scheduling.py
@@ -0,0 +1,71 @@
+#!/bin/python
+import sys
+import math
+
+nr_of_classes = 10
+nr_of_rooms = math.ceil(nr_of_classes * 0.7)
+hours_per_week = 26
+time_slots_per_day = 8
+days_per_week = 5
+nr_of_courses = 10
+
+literals = []
+predicates = []
+
+for d in range(days_per_week):
+    for h in range(time_slots_per_day):
+        for c in range(nr_of_classes):
+            literals.append('(day_%i_hour_%i_class_%i_room Int)' % (d, h, c))     # (0, nr_of_rooms]
+            predicates.append('(and (<= day_%i_hour_%i_class_%i_room %i) (>= day_%i_hour_%i_class_%i_room 0))' %
+                              (d, h, c, nr_of_rooms, d, h, c))
+            literals.append('(day_%i_hour_%i_class_%i_lecture Int)' % (d, h, c))  # (0, hours_per_week]
+            predicates.append('(and (<= day_%i_hour_%i_class_%i_lecture %i) (>= day_%i_hour_%i_class_%i_lecture 0))' %
+                              (d, h, c, hours_per_week, d, h, c))
+
+# Every lecture must be followed in a given week
+for co in range(hours_per_week):
+    for c in range(nr_of_classes):
+        tmp = '(xor\n'
+        for d in range(days_per_week):
+            for h in range(time_slots_per_day):
+                tmp += ' (= day_%i_hour_%i_class_%i_lecture %i)\n' % (d, h, c, co + 1)
+        tmp += ')'
+        predicates.append(tmp)
+
+# If a lecture is being followed at a specific time, a room needs to be scheduled
+for d in range(days_per_week):
+    for h in range(time_slots_per_day):
+        for c in range(nr_of_classes):
+            predicates.append('(ite (> day_%i_hour_%i_class_%i_lecture 0) (> day_%i_hour_%i_class_%i_room 0) (= '
+                              'day_%i_hour_%i_class_%i_room 0))' % (d, h, c, d, h, c, d, h, c))
+
+# Rooms may not be scheduled double
+for d in range(days_per_week):
+    for h in range(time_slots_per_day):
+        for c1 in range(nr_of_classes):
+            for c2 in range(nr_of_classes):
+                if c2 > c1:
+                    predicates.append('(not (= day_%i_hour_%i_class_%i_room day_%i_hour_%i_class_%i_room))' %
+                                      (d, h, c1, d, h, c2))
+
+s = """(benchmark test.smt
+:logic QF_UFLIA
+:extrafuns (
+"""
+s += "\n".join("%s" % x for x in literals)
+s += """
+)
+:formula (and
+"""
+s += "\n".join(predicates)
+s += """
+))
+"""
+
+try:
+    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