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
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
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
|
