1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
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
|
