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
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
|
#!/usr/bin/env python
# Usage for 1a (where -1 is the number of prittles, -1 means unrestricted)
# $0 -1 | z3 -smt -in
# Usage for 1b:
# $0 -1 b | z3 -smt -in
import sys
number_of_prittles = int(sys.argv[1])
prtl = None if number_of_prittles == -1 else number_of_prittles
is_b = len(sys.argv) >= 3 and sys.argv[2] == 'b'
# List of m types ("m types"):
# - exact number of items needed (or None for no restriction)
# - Name (first letter is used for variable)
# - Weight (in kg)
stuff = [
(4, "Nuzzles", 700),
(prtl, "Prittles", 400),
(8, "Skipples", 1000),
(10, "Crottles", 2500),
(20, "Dupples", 200),
]
# T trucks ("n trucks")
n_trucks = 8
# Capacity C_T
truck_capacity = 8000
# Maximum pallets p_T
max_pallets = 8
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 = []
# For each truck,
# define the number of pallets of each type that will be contained in.
for i in range(1, n_trucks + 1):
for needed, name, weight in stuff:
name = "{name[0]}{i}".format(name=name, i=i)
literals.append(name)
# Cannot have negative number of items...
preds += fillin([
"(>= {name} 0)"
], vars())
# For each item, require exact as many items spread over all trucks
for needed, name, weight in stuff:
if needed is None:
continue
# total_items = item_in_truck0 + ... + item_in_truckN
items_in_truckX = " ".join(
"{name[0]}{i}".format(name=name, i=i)
for i in range(1, n_trucks + 1)
)
preds += fillin([
"(= {needed} (+ {items_in_truckX}))",
], vars())
# Each truck may hold a maximum number of pallets.
# and a maximum weight.
for i in range(1, n_trucks + 1):
# max_pallets >= item0_in_truck + ... + itemM_in_truck
itemX_in_truck = " ".join(
"{name[0]}{i}".format(name=name, i=i)
for needed, name, weight in stuff
)
total_weight_in_truck = " ".join(
"(* {name[0]}{i} {weight})".format(name=name, i=i, weight=weight)
for needed, name, weight in stuff
)
preds += fillin([
"(>= {max_pallets} (+ {itemX_in_truck}))",
"(>= {truck_capacity} (+ {total_weight_in_truck}))",
], vars())
# Skipples must be distributed over at most three trucks.
# So, Any combination of n-3 trucks must have zero skipples.
number_of_skipples = None
for needed, name, weight in stuff:
if name[0] == 'S':
number_of_skipples = needed
assert number_of_skipples is not None
skipple_preds = []
for x in range(1, n_trucks + 1):
for y in range(1, n_trucks + 1):
if x == y:
# Require unique pairs (x, y, 0, ..., 0) as optimization.
# This is weaker than (x, 0, ... 0)
continue
for z in range(1, n_trucks + 1):
if x == z or y == z:
# Same as above, require unique x, y, z such that
# (x, y, z, 0, ..., 0)
continue
# "These threee trucks hold all available skipples"
#items_all_in_these_trucks = [
# "S{i}".format(i=i)
# for i in (x, y, z)
#]
#skipple_preds += fillin([
# "(= {number_of_skipples} (+ %s))" % " ".join(items_all_in_these_trucks)
#], vars())
# "All other n-3" trucks have no skipples
items_in_other_trucks_zero = [
"(= 0 S{i})".format(i=i)
for i in range(1, n_trucks + 1)
if i not in (x, y, z)
]
preds += [
"(or %s)" % " ".join(items_in_other_trucks_zero)
]
#preds += [
# "(or\n%s\n)" % "\n".join(skipple_preds)
#]
# Nuzzles: max 1 per truck
for i in range(1, n_trucks + 1):
preds += fillin([
"(>= 1 N{i})"
], vars())
# 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
|
